Theory Succession_Poset

sectionA poset of successions

theory Succession_Poset
  imports
    ZF_Trans_Interpretations
    Proper_Extension
begin

textIn 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
    then
    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
    next
      case eq
      with a_
      show ?thesis
        by auto
    qed
  }
  with equ
  show ?thesis
    unfolding seq_upd_def
    using lam_type[of "succ(domain(f))"]
    by auto
qed

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
qed

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

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

definition
  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,__")
proof
  show " ?f, f  2⇗<ω× 2⇗<ω"
    using assms seq_upd_type by auto
next
  show  "f  seq_upd(f,a)"
  proof
    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
    ultimately
    show "x  seq_upd(f,a)"
      unfolding seq_upd_def lam_def
      by (auto intro:ltI)
  qed
qed

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")
proof
  assume "sp.compat(?f, ?g)"
  then
  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
  ultimately
  have "y,0  h" "y,1  h"
    by auto
  moreover from h  2⇗<ω
  obtain n where "nnat" "h:n2"
    by blast
  ultimately
  show "False"
    using fun_is_function[of h n "λ_. 2"]
    unfolding seqspace_def function_def by auto
qed

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
begin

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)

subsectionCohen 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⇗<ω"
  then
  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
  ultimately
  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?
next
  show "2⇗<ω M"
    using nat_into_M seqspace_closed by simp
next
  show "seqle  M"
    using seqle_in_M .
qed

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

end