Theory Succession_Poset

section‹A poset of successions›

theory Succession_Poset

text‹In this theory we define a separative poset. Its underlying set is the
set of finite binary sequences (that is, with codomain $2={0,1}$);
of course, one can see that set as
the set termω-||>2 or equivalently as the set of partial functions
termFn(ω,ω,2), i.e. the set of partial functions bounded by termω.

The order relation of the poset is that of being less defined as functions
(cf. termFnlerel(A⇗<ω)), so it could be surprising that we have not used
termFn(ω,ω,2) for the set. The only reason why we keep this alternative
definition is because we can prove termA⇗<ω M (and therefore
termFnlerel(A⇗<ω)  M) using only one instance of separation.›

definition seq_upd :: "i  i  i" where
  "seq_upd(f,a)  λ j  succ(domain(f)) . if j < domain(f) then f`j else a"

lemma seq_upd_succ_type :
  assumes "nnat" "fnA" "aA"
  shows "seq_upd(f,a) succ(n)  A"
proof -
  from assms
  have equ: "domain(f) = n"
    using domain_of_fun by simp
    fix j
    assume "jsucc(domain(f))"
    with equ n_
    have "jn"
      using ltI by auto
    with n_
    consider (lt) "j<n" | (eq) "j=n"
      using leD by auto
    have "(if j < n then f`j else a)  A"
    proof cases
      case lt
      with f_
      show ?thesis
        using apply_type ltD[OF lt] by simp
      case eq
      with a_
      show ?thesis
        by auto
  with equ
  show ?thesis
    unfolding seq_upd_def
    using lam_type[of "succ(domain(f))"]
    by auto

lemma seq_upd_type :
  assumes "fA⇗<ω⇖" "aA"
  shows "seq_upd(f,a)  A⇗<ω⇖"
proof -
  from f_
  obtain y where "ynat" "fyA"
    unfolding seqspace_def by blast
  with aA
  have "seq_upd(f,a)succ(y)A"
    using seq_upd_succ_type by simp
  with y_
  show ?thesis
    unfolding seqspace_def by auto

lemma seq_upd_apply_domain [simp]:
  assumes "f:nA" "nnat"
  shows "seq_upd(f,a)`n = a"
  unfolding seq_upd_def using assms domain_of_fun by auto

lemma zero_in_seqspace :
  shows "0  A⇗<ω⇖"
  unfolding seqspace_def
  by force

  seqlerel :: "i  i" where
  "seqlerel(A)  Fnlerel(A⇗<ω)"

  seqle :: "i" where
  "seqle  seqlerel(2)"

lemma seqleI[intro!]:
  "f,g  2⇗<ω×2⇗<ω g  f   f,g  seqle"
  unfolding seqle_def seqlerel_def seqspace_def Rrel_def Fnlerel_def
  by blast

lemma seqleD[dest!]:
  "z  seqle  x y. x,y  2⇗<ω×2⇗<ω y  x  z = x,y"
  unfolding Rrel_def seqle_def seqlerel_def Fnlerel_def
  by blast

lemma upd_leI :
  assumes "f2⇗<ω⇖" "a2"
  shows "seq_upd(f,a),fseqle"  (is "?f,__")
  show " ?f, f  2⇗<ω× 2⇗<ω⇖"
    using assms seq_upd_type by auto
  show  "f  seq_upd(f,a)"
    fix x
    assume "x  f"
    moreover from f  2⇗<ω⇖›
    obtain n where "nnat" "f : n  2"
      by blast
    moreover from calculation
    obtain y where "yn" "x=y,f`y"
      using Pi_memberD[of f n "λ_ . 2"]
      by blast
    moreover from f:n2
    have "domain(f) = n"
      using domain_of_fun by simp
    show "x  seq_upd(f,a)"
      unfolding seq_upd_def lam_def
      by (auto intro:ltI)

lemma preorder_on_seqle: "preorder_on(2⇗<ω,seqle)"
  unfolding preorder_on_def refl_def trans_on_def by blast

lemma zero_seqle_max: "x2⇗<ω x,0  seqle"
  using zero_in_seqspace
  by auto

interpretation sp:forcing_notion "2⇗<ω⇖" "seqle" "0"
  using preorder_on_seqle zero_seqle_max zero_in_seqspace
  by unfold_locales simp_all

notation sp.Leq (infixl "≼s" 50)
notation sp.Incompatible (infixl "⊥s" 50)

lemma seqspace_separative:
  assumes "f2⇗<ω⇖"
  shows "seq_upd(f,0) ⊥s seq_upd(f,1)" (is "?f ⊥s ?g")
  assume "sp.compat(?f, ?g)"
  obtain h where "h  2⇗<ω⇖" "?f  h" "?g  h"
    by blast
  moreover from f_
  obtain y where "ynat" "f:y2"
    by blast
  moreover from this
  have "?f: succ(y)  2" "?g: succ(y)  2"
    using seq_upd_succ_type by blast+
  moreover from this
  have "y,?f`y  ?f" "y,?g`y  ?g"
    using apply_Pair by auto
  have "y,0  h" "y,1  h"
    by auto
  moreover from h  2⇗<ω⇖›
  obtain n where "nnat" "h:n2"
    by blast
  show "False"
    using fun_is_function[of h n "λ_. 2"]
    unfolding seqspace_def function_def by auto

definition seqleR_fm :: "i  i" where
  "seqleR_fm(fg)  Exists(Exists(And(pair_fm(0,1,fg+ω2),subset_fm(1,0))))"

lemma type_seqleR_fm : "fg  nat  seqleR_fm(fg)  formula"
  unfolding seqleR_fm_def
  by simp

arity_theorem for "seqleR_fm"

lemma (in M_ctm1) seqleR_fm_sats :
  assumes "fgnat" "envlist(M)"
  shows "(M, env  seqleR_fm(fg))  (f[##M]. g[##M]. pair(##M,f,g,nth(fg,env))  f  g)"
  unfolding seqleR_fm_def
  using assms trans_M sats_subset_fm pair_iff_sats
  by auto

context M_ctm1

lemma seqle_in_M: "seqle  M"
  using arity_seqleR_fm seqleR_fm_sats type_seqleR_fm
    cartprod_closed seqspace_closed nat_into_M nat_in_M pair_in_M_iff
  unfolding seqle_def seqlerel_def Rrel_def Fnlerel_def
  by (rule_tac Collect_in_M[of "seqleR_fm(0)" "[]"],auto)

subsection‹Cohen extension is proper›

interpretation ctm_separative "2⇗<ω⇖" seqle 0
proof (unfold_locales)
  fix f
  let ?q="seq_upd(f,0)" and ?r="seq_upd(f,1)"
  assume "f  2⇗<ω⇖"
  have "?q ≼s f  ?r ≼s f  ?q ⊥s ?r"
    using upd_leI seqspace_separative by auto
  moreover from calculation
  have "?q  2⇗<ω⇖"  "?r  2⇗<ω⇖"
    using seq_upd_type[of f 2] by auto
  show "q2⇗<ω. r2⇗<ω. q ≼s f  r ≼s f  q ⊥s r"
    by (rule_tac bexI)+ ― ‹why the heck auto-tools don't solve this?›
  show "2⇗<ω M"
    using nat_into_M seqspace_closed by simp
  show "seqle  M"
    using seqle_in_M .

lemma cohen_extension_is_proper: "G. M_generic(G)  M  M[G]"
  using proper_extension generic_filter_existence zero_in_seqspace
  by force

end ― ‹localeM_ctm1