section‹A poset of successions› theory Succession_Poset imports ZF_Trans_Interpretations Proper_Extension begin 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 \<^term>‹Fn(ω,ω,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. \<^term>‹Fnlerel(A⇗<ω⇖)›), so it could be surprising that we have not used \<^term>‹Fn(ω,ω,2)› for the set. The only reason why we keep this alternative definition is because we can prove \<^term>‹A⇗<ω⇖ ∈ M› (and therefore \<^term>‹Fnlerel(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 "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 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 "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 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 "fg∈nat" "env∈list(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) 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 ≠ M[G]" using proper_extension generic_filter_existence zero_in_seqspace by force end ― ‹\<^locale>‹M_ctm1›› end