Theory Succession_Poset

theory Succession_Poset
imports Arities Proper_Extension
section‹A poset of successions›
theory Succession_Poset
  imports
    Arities
    Proper_Extension
    Synthetic_Definition
    Names
begin

subsection‹The set of finite binary sequences›

notation nat (‹ω›) ― ‹MOVE THIS to an appropriate place›

text‹We implement the poset for adding one Cohen real, the set 
$2^{<\omega}$ of finite binary sequences.›

definition
  seqspace :: "[i,i] ⇒ i" (‹_<_ [100,1]100) where
  "B ≡ ⋃n∈α. (n→B)"

lemma seqspaceI[intro]: "n∈α ⟹ f:n→B ⟹ f∈B"
  unfolding seqspace_def by blast

lemma seqspaceD[dest]: "f∈B ⟹ ∃n∈α. f:n→B"
  unfolding seqspace_def by blast

― ‹FIXME: Now this is too particular (only for \<^term>‹ω›-sequences.
  A relative definition for \<^term>‹seqspace› would be appropriate.›
schematic_goal seqspace_fm_auto:
  assumes 
    "nth(i,env) = n" "nth(j,env) = z"  "nth(h,env) = B" 
    "i ∈ nat" "j ∈ nat" "h∈nat" "env ∈ list(A)"
  shows 
    "(∃om∈A. omega(##A,om) ∧ n ∈ om ∧ is_funspace(##A, n, B, z)) ⟷ (A, env ⊨ (?sqsprp(i,j,h)))"
  unfolding is_funspace_def 
  by (insert assms ; (rule sep_rules | simp)+)

synthesize "seqspace_rep_fm" from_schematic seqspace_fm_auto
 
locale M_seqspace =  M_trancl +
  assumes 
    seqspace_replacement: "M(B) ⟹ strong_replacement(M,λn z. n∈nat ∧ is_funspace(M,n,B,z))"
begin

lemma seqspace_closed:
  "M(B) ⟹ M(B)"
  unfolding seqspace_def using seqspace_replacement[of B] RepFun_closed2 
  by simp

end (* M_seqspace *)


sublocale M_ctm  M_seqspace "##M"
proof (unfold_locales, simp)
  fix B
  have "arity(seqspace_rep_fm(0,1,2)) ≤ 3" "seqspace_rep_fm(0,1,2)∈formula" 
    unfolding seqspace_rep_fm_def 
    using arity_pair_fm arity_omega_fm arity_typed_function_fm nat_simp_union 
    by auto
  moreover
  assume "B∈M"
  ultimately
  have "strong_replacement(##M, λx y. M, [x, y, B] ⊨ seqspace_rep_fm(0, 1, 2))"
    using replacement_ax[of "seqspace_rep_fm(0,1,2)"]
    by simp
  moreover 
  note ‹B∈M›
  moreover from this
  have "univalent(##M, A, λx y. M, [x, y, B] ⊨ seqspace_rep_fm(0, 1, 2))" 
    if "A∈M" for A 
    using that unfolding univalent_def seqspace_rep_fm_def  
    by (auto, blast dest:transitivity)
  ultimately
  have "strong_replacement(##M, λn z. ∃om[##M]. omega(##M,om) ∧ n ∈ om ∧ is_funspace(##M, n, B, z))"
    using seqspace_fm_auto[of 0 "[_,_,B]" _ 1 _ 2 B M] unfolding seqspace_rep_fm_def strong_replacement_def
    by simp
  with ‹B∈M› 
  show "strong_replacement(##M, λn z. n ∈ nat ∧ is_funspace(##M, n, B, z))"
    using M_nat by simp
qed

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 "n∈nat" "f∈n→A" "a∈A"
  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 "j∈succ(domain(f))"
    with equ ‹n∈_›
    have "j≤n" 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 "f∈A" "a∈A"
  shows "seq_upd(f,a) ∈ A"
proof -
  from ‹f∈_›
  obtain y where "y∈nat" "f∈y→A"
    unfolding seqspace_def by blast
  with ‹a∈A›
  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:n→A" "n∈nat"
  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
  seqleR :: "i ⇒ i ⇒ o" where
  "seqleR(f,g) ≡ g ⊆ f"

definition
  seqlerel :: "i ⇒ i" where
  "seqlerel(A) ≡ Rrel(λx y. y ⊆ x,A)"

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

lemma seqleI[intro!]: 
  "⟨f,g⟩ ∈ 2×2 ⟹ g ⊆ f  ⟹ ⟨f,g⟩ ∈ seqle"
  unfolding  seqspace_def seqle_def seqlerel_def Rrel_def 
  by blast

lemma seqleD[dest!]: 
  "z ∈ seqle ⟹ ∃x y. ⟨x,y⟩ ∈ 2×2 ∧ y ⊆ x ∧ z = ⟨x,y⟩"
  unfolding seqle_def seqlerel_def Rrel_def 
  by blast

lemma upd_leI : 
  assumes "f∈2" "a∈2"
  shows "⟨seq_upd(f,a),f⟩∈seqle"  (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  "n∈nat" "f : n → 2"
      by blast
    moreover from calculation
    obtain y where "y∈n" "x=⟨y,f`y⟩" using Pi_memberD[of f n "λ_ . 2"] 
      by blast
    moreover from ‹f:n→2›
    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: "x∈2 ⟹ ⟨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 "f∈2"
  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 "y∈nat" "f:y→2" 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 "n∈nat" "h:n→2" by blast
  ultimately
  show "False"
    using fun_is_function[of h n "λ_. 2"] 
    unfolding seqspace_def function_def by auto
qed

definition is_seqleR :: "[i⇒o,i,i] ⇒ o" where
  "is_seqleR(Q,f,g) ≡ g ⊆ f"

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

lemma arity_seqleR_fm :
  "fg ∈ nat ⟹ arity(seqleR_fm(fg)) = succ(fg)"
  unfolding seqleR_fm_def 
  using arity_pair_fm arity_subset_fm nat_simp_union by simp

lemma (in M_basic) seqleR_abs: 
  assumes "M(f)" "M(g)"
  shows "seqleR(f,g) ⟷ is_seqleR(M,f,g)"
  unfolding seqleR_def is_seqleR_def 
  using assms apply_abs domain_abs domain_closed[OF ‹M(f)›]  domain_closed[OF ‹M(g)›]
  by auto

definition
  relP :: "[i⇒o,[i⇒o,i,i]⇒o,i] ⇒ o" where
  "relP(M,r,xy) ≡ (∃x[M]. ∃y[M]. pair(M,x,y,xy) ∧ r(M,x,y))"

lemma (in M_ctm) seqleR_fm_sats : 
  assumes "fg∈nat" "env∈list(M)" 
  shows "sats(M,seqleR_fm(fg),env) ⟷ relP(##M,is_seqleR,nth(fg, env))"
  unfolding seqleR_fm_def is_seqleR_def relP_def
  using assms trans_M sats_subset_fm pair_iff_sats
  by auto


lemma (in M_basic) is_related_abs :
  assumes "⋀ f g . M(f) ⟹ M(g) ⟹ rel(f,g) ⟷ is_rel(M,f,g)"
  shows "⋀z . M(z) ⟹ relP(M,is_rel,z) ⟷ (∃x y. z = ⟨x,y⟩ ∧ rel(x,y))"
  unfolding relP_def using pair_in_M_iff assms by auto

definition
  is_RRel :: "[i⇒o,[i⇒o,i,i]⇒o,i,i] ⇒ o" where
  "is_RRel(M,is_r,A,r) ≡ ∃A2[M]. cartprod(M,A,A,A2) ∧ is_Collect(M,A2, relP(M,is_r),r)"

lemma (in M_basic) is_Rrel_abs :
  assumes "M(A)"  "M(r)"
    "⋀ f g . M(f) ⟹ M(g) ⟹ rel(f,g) ⟷ is_rel(M,f,g)"
  shows "is_RRel(M,is_rel,A,r) ⟷  r = Rrel(rel,A)"
proof -
  from ‹M(A)› 
  have "M(z)" if "z∈A×A" for z
    using cartprod_closed transM[of z "A×A"] that by simp
  then
  have A:"relP(M, is_rel, z) ⟷ (∃x y. z = ⟨x, y⟩ ∧ rel(x, y))" "M(z)" if "z∈A×A" for z
    using that is_related_abs[of rel is_rel,OF assms(3)] by auto
  then
  have "Collect(A×A,relP(M,is_rel)) = Collect(A×A,λz. (∃x y. z = ⟨x,y⟩ ∧ rel(x,y)))"
    using Collect_cong[of "A×A" "A×A" "relP(M,is_rel)",OF _ A(1)] assms(1) assms(2)
    by auto
  with assms
  show ?thesis unfolding is_RRel_def Rrel_def using cartprod_closed
    by auto
qed

definition
  is_seqlerel :: "[i⇒o,i,i] ⇒ o" where
  "is_seqlerel(M,A,r) ≡ is_RRel(M,is_seqleR,A,r)"

lemma (in M_basic) seqlerel_abs :
  assumes "M(A)"  "M(r)"
  shows "is_seqlerel(M,A,r) ⟷ r = Rrel(seqleR,A)"
  unfolding is_seqlerel_def
  using is_Rrel_abs[OF ‹M(A)› ‹M(r)›,of seqleR is_seqleR] seqleR_abs
  by auto

definition RrelP :: "[i⇒i⇒o,i] ⇒ i" where
  "RrelP(R,A) ≡ {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ R(x,y)}"
  
lemma Rrel_eq : "RrelP(R,A) = Rrel(R,A)"
  unfolding Rrel_def RrelP_def by auto

context M_ctm
begin

lemma Rrel_closed:
  assumes "A∈M" 
    "⋀ a. a ∈ nat ⟹ rel_fm(a)∈formula"
    "⋀ f g . (##M)(f) ⟹ (##M)(g) ⟹ rel(f,g) ⟷ is_rel(##M,f,g)"
    "arity(rel_fm(0)) = 1" 
    "⋀ a . a ∈ M ⟹ sats(M,rel_fm(0),[a]) ⟷ relP(##M,is_rel,a)"
  shows "(##M)(Rrel(rel,A))" 
proof -
  have "z∈ M ⟹ relP(##M, is_rel, z) ⟷ (∃x y. z = ⟨x, y⟩ ∧ rel(x, y))" for z
    using assms(3) is_related_abs[of rel is_rel]
    by auto
  with assms
  have "Collect(A×A,λz. (∃x y. z = ⟨x,y⟩ ∧ rel(x,y))) ∈ M"
    using Collect_in_M_0p[of "rel_fm(0)" "λ A z . relP(A,is_rel,z)" "λ z.∃x y. z = ⟨x, y⟩ ∧ rel(x, y)" ]
        cartprod_closed
    by simp
  then show ?thesis
  unfolding Rrel_def by simp
qed

lemma seqle_in_M: "seqle ∈ M"
  using Rrel_closed seqspace_closed 
    transitivity[OF _ nat_in_M] type_seqleR_fm[of 0] arity_seqleR_fm[of 0]
    seqleR_fm_sats[of 0] seqleR_abs seqlerel_abs 
  unfolding seqle_def seqlerel_def seqleR_def
  by 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"
  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 "∃q∈2. ∃r∈2. 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 ≠ M2[G]"
  using proper_extension generic_filter_existence zero_in_seqspace
  by force

end (* M_ctm *)

end