Theory Succession_Poset
section‹A poset of successions›
theory Succession_Poset
imports
Replacement_Instances
Proper_Extension
FiniteFun_Relative
begin
sublocale M_ZF_trans ⊆ M_seqspace "##M"
by (unfold_locales, simp add:replacement_omega_funspace)
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 ord_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[OF assms(2),of 0 "[]"] 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)+
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⇗2⇗<ω⇖⇖[G]"
using proper_extension generic_filter_existence zero_in_seqspace
by force
end
end