Theory Succession_Poset
section‹A poset of successions›
theory Succession_Poset
imports
Arities Proper_Extension Synthetic_Definition
Names
begin
subsection‹The set of finite binary sequences›
text‹We implement the poset for adding one Cohen real, the set
$2^{<\omega}$ of of finite binary sequences.›
definition
seqspace :: "i ⇒ i" ("_^<ω" [100]100) where
"seqspace(B) ≡ ⋃n∈nat. (n→B)"
lemma seqspaceI[intro]: "n∈nat ⟹ f:n→B ⟹ f∈seqspace(B)"
unfolding seqspace_def by blast
lemma seqspaceD[dest]: "f∈seqspace(B) ⟹ ∃n∈nat. f:n→B"
unfolding seqspace_def by blast
lemma seqspace_type:
"f ∈ B^<ω ⟹ ∃n∈nat. f:n→B"
unfolding seqspace_def by auto
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
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"
using seqspace_type 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 forcing_notion "2^<ω" "seqle" "0"
using preorder_on_seqle zero_seqle_max zero_in_seqspace
by unfold_locales simp_all
abbreviation SEQle :: "[i, i] ⇒ o" (infixl "≼s" 50)
where "x ≼s y ≡ Leq(x,y)"
abbreviation SEQIncompatible :: "[i, i] ⇒ o" (infixl "⊥s" 50)
where "x ⊥s y ≡ Incompatible(x,y)"
lemma seqspace_separative:
assumes "f∈2^<ω"
shows "seq_upd(f,0) ⊥s seq_upd(f,1)" (is "?f ⊥s ?g")
proof
assume "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)+
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 ≠ GenExt(G)"
using proper_extension generic_filter_existence zero_in_seqspace
by force
end
end