Theory Cohen_Posets_Relative
section‹Cohen forcing notions›
theory Cohen_Posets_Relative
imports
Forcing_Notions
Transitive_Models.Delta_System_Relative
Transitive_Models.Partial_Functions_Relative
begin
locale cohen_data =
fixes κ I J::i
assumes zero_lt_kappa: "0<κ"
begin
lemmas zero_lesspoll_kappa = zero_lesspoll[OF zero_lt_kappa]
end
abbreviation
inj_dense :: "[i,i,i,i]⇒i" where
"inj_dense(I,J,w,x) ≡
{ p∈Fn(ω,I×ω,J) . (∃n∈ω. ⟨⟨w,n⟩,1⟩ ∈ p ∧ ⟨⟨x,n⟩,0⟩ ∈ p) }"
lemma dense_inj_dense:
assumes "w ∈ I" "x ∈ I" "w ≠ x" "p∈Fn(ω,I×ω,J)" "0∈J" "1∈J"
shows "∃d∈inj_dense(I,J,w,x). ⟨d ,p⟩ ∈ Fnle(ω,I×ω,J)"
proof -
obtain n where "⟨w,n⟩ ∉ domain(p)" "⟨x,n⟩ ∉ domain(p)" "n ∈ ω"
proof -
{
assume "⟨w,n⟩ ∈ domain(p) ∨ ⟨x,n⟩ ∈ domain(p)" if "n ∈ ω" for n
then
have "ω ⊆ range(domain(p))" by blast
then
have "¬ Finite(p)"
using Finite_range Finite_domain subset_Finite nat_not_Finite
by auto
with ‹p ∈ _›
have False
using Fn_nat_eq_FiniteFun FiniteFun.dom_subset[of "I×ω" J]
Fin_into_Finite by auto
}
with that
show ?thesis by auto
qed
moreover
note ‹p ∈ _› assms
moreover from calculation
have "cons(⟨⟨x,n⟩,0⟩, p) ∈ Fn(ω,I×ω,J)"
using FiniteFun.consI[of "⟨x,n⟩" "I×ω" 0 J p]
Fn_nat_eq_FiniteFun by auto
ultimately
have "cons(⟨⟨w,n⟩,1⟩, cons(⟨⟨x,n⟩,0⟩, p) ) ∈ Fn(ω,I×ω,J)"
using FiniteFun.consI[of "⟨w,n⟩" "I × ω" 1 J "cons(⟨⟨x,n⟩,0⟩, p)"]
Fn_nat_eq_FiniteFun by auto
with ‹n ∈ ω›
show ?thesis
using ‹p ∈ _› by (intro bexI) auto
qed
locale add_reals = cohen_data nat _ 2
subsection‹Combinatorial results on Cohen posets›
sublocale cohen_data ⊆ forcing_notion "Fn(κ,I,J)" "Fnle(κ,I,J)" 0
proof
show "0 ∈ Fn(κ, I, J)"
using zero_lt_kappa zero_in_Fn by simp
then
show "∀p∈Fn(κ, I, J). ⟨p, 0⟩ ∈ Fnle(κ, I, J)"
unfolding preorder_on_def refl_def trans_on_def
by auto
next
show "preorder_on(Fn(κ, I, J), Fnle(κ, I, J))"
unfolding preorder_on_def refl_def trans_on_def
by blast
qed
context cohen_data
begin
lemma compat_imp_Un_is_function:
assumes "G ⊆ Fn(κ, I, J)" "⋀p q. p ∈ G ⟹ q ∈ G ⟹ compat(p,q)"
shows "function(⋃G)"
unfolding function_def
proof (intro allI ballI impI)
fix x y y'
assume "⟨x, y⟩ ∈ ⋃G" "⟨x, y'⟩ ∈ ⋃G"
then
obtain p q where "⟨x, y⟩ ∈ p" "⟨x, y'⟩ ∈ q" "p ∈ G" "q ∈ G"
by auto
moreover from this and assms
obtain r where "r ∈ Fn(κ, I, J)" "r ⊇ p" "r ⊇ q"
using compatD[of p q] by force
moreover from this
have "function(r)"
using Fn_is_function by simp
ultimately
show "y = y'"
unfolding function_def by fastforce
qed
lemma Un_filter_is_function: "filter(G) ⟹ function(⋃G)"
using compat_imp_Un_is_function filter_imp_compat[of G]
filter_subset_notion
by simp
end
locale M_cohen = M_delta +
assumes
countable_lepoll_assms2:
"M(A') ⟹ M(A) ⟹ M(b) ⟹ M(f) ⟹ separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. {p ∈ A . domain(p) = a}, b, f, i)⟩)"
and
countable_lepoll_assms3:
"M(A) ⟹ M(f) ⟹ M(b) ⟹ M(D) ⟹ M(r') ⟹ M(A')⟹
separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(drSR_Y(r', D, A), b, f, i)⟩)"
lemma (in M_library) Fnle_rel_Aleph_rel1_closed[intro,simp]:
"M(Fnle⇗M⇖(ℵ⇘1⇙⇗M⇖, ℵ⇘1⇙⇗M⇖, ω →⇗M⇖ 2))"
by simp
locale M_add_reals = M_cohen + add_reals
begin
lemmas zero_lesspoll_rel_kappa = zero_lesspoll_rel[OF zero_lt_kappa]
end
relativize relational "compat_in" "is_compat_in" external
synthesize "compat_in" from_definition "is_compat_in" assuming "nonempty"
context
notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "compat_in_fm"
end
lemma (in M_trivial) compat_in_abs[absolut]:
assumes
"M(A)" "M(r)" "M(p)" "M(q)"
shows
"is_compat_in(M,A,r,p,q) ⟷ compat_in(A,r,p,q)"
using assms unfolding is_compat_in_def compat_in_def by simp
definition
antichain :: "i⇒i⇒i⇒o" where
"antichain(P,leq,A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A. p≠q ⟶ ¬compat_in(P,leq,p,q))"
relativize relational "antichain" "antichain_rel"
definition
ccc :: "i ⇒ i ⇒ o" where
"ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"
abbreviation
antichain_rel_abbr :: "[i⇒o,i,i,i] ⇒ o" (‹antichain⇗_⇖'(_,_,_')›) where
"antichain⇗M⇖(P,leq,A) ≡ antichain_rel(M,P,leq,A)"
abbreviation
antichain_r_set :: "[i,i,i,i] ⇒ o" (‹antichain⇗_⇖'(_,_,_')›) where
"antichain⇗M⇖(P,leq,A) ≡ antichain_rel(##M,P,leq,A)"
context M_trivial
begin
lemma antichain_abs [absolut]:
"⟦ M(A); M(P); M(leq) ⟧ ⟹ antichain⇗M⇖(P,leq,A) ⟷ antichain(P,leq,A)"
unfolding antichain_rel_def antichain_def by (simp add:absolut)
end
relativize relational "ccc" "ccc_rel"
abbreviation
ccc_rel_abbr :: "[i⇒o,i,i]⇒o" (‹ccc⇗_⇖'(_,_')›) where
"ccc_rel_abbr(M) ≡ ccc_rel(M)"
abbreviation
ccc_r_set :: "[i,i,i]⇒o" (‹ccc⇗_⇖'(_,_')›) where
"ccc_r_set(M) ≡ ccc_rel(##M)"
context M_cardinals
begin
lemma def_ccc_rel:
shows
"ccc⇗M⇖(P,leq) ⟷ (∀A[M]. antichain⇗M⇖(P,leq,A) ⟶ |A|⇗M⇖ ≤ ω)"
using is_cardinal_iff
unfolding ccc_rel_def by (simp add:absolut)
end
context M_FiniteFun
begin
lemma Fnle_nat_closed[intro,simp]:
assumes "M(I)" "M(J)"
shows "M(Fnle(ω,I,J))"
unfolding Fnle_def Fnlerel_def Rrel_def
using supset_separation FiniteFun_closed Fn_nat_eq_FiniteFun assms by simp
lemma Fn_nat_closed:
assumes "M(A)" "M(B)" shows "M(Fn(ω,A,B))"
using assms Fn_nat_eq_FiniteFun
by simp
end
context M_add_reals
begin
lemma lam_replacement_drSR_Y: "M(A) ⟹ M(D) ⟹ M(r') ⟹ lam_replacement(M, drSR_Y(r',D,A))"
using lam_replacement_drSR_Y
by simp
lemma (in M_trans) mem_F_bound3:
fixes F A
defines "F ≡ dC_F"
shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ {domain(x). x∈A})"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
lemma ccc_rel_Fn_nat:
assumes "M(I)"
shows "ccc⇗M⇖(Fn(nat,I,2), Fnle(nat,I,2))"
proof -
have repFun_dom_closed:"M({domain(p) . p ∈ A})" if "M(A)" for A
using RepFun_closed domain_replacement_simp transM[OF _ ‹M(A)›] that
by auto
from assms
have "M(Fn(nat,I,2))" using Fn_nat_eq_FiniteFun by simp
{
fix A
assume "¬ |A|⇗M⇖ ≤ nat" "M(A)" "A ⊆ Fn(nat, I, 2)"
moreover from this
have "countable_rel(M,{p∈A. domain(p) = d})" if "M(d)" for d
proof (cases "d≺⇗M⇖nat ∧ d ⊆ I")
case True
with ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
have "{p ∈ A . domain(p) = d} ⊆ d →⇗M⇖ 2"
using domain_of_fun function_space_rel_char[of _ 2]
by (auto,subgoal_tac "M(domain(x))",simp_all add:transM[of _ A],force)
moreover from True ‹M(d)›
have "Finite(d →⇗M⇖ 2)"
using Finite_Pi[THEN [2] subset_Finite, of _ d "λ_. 2"]
lesspoll_rel_nat_is_Finite_rel function_space_rel_char[of _ 2]
by auto
moreover from ‹M(d)›
have "M(d →⇗M⇖ 2)"
by simp
moreover from ‹M(A)›
have "M({p ∈ A . domain(p) = d})"
using separation_closed domain_eq_separation[OF ‹M(d)›] by simp
ultimately
show ?thesis using subset_Finite[of _ "d→⇗M⇖2" ]
by (auto intro!:Finite_imp_countable_rel)
next
case False
with ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
have "domain(p) ≠ d" if "p∈A" for p
proof -
note False that ‹M(A)›
moreover from this
obtain d' where "d' ⊆ I" "p∈d' → 2" "d' ≺ ω"
using FnD[OF subsetD[OF ‹A⊆_› ‹p∈A›]]
by auto
moreover from this
have "p ≈ d'" "domain(p) = d'"
using function_eqpoll Pi_iff
by auto
ultimately
show ?thesis
using lesspoll_nat_imp_lesspoll_rel transM[of p]
by auto
qed
then
show ?thesis
using empty_lepoll_relI by auto
qed
have 2:"M(x) ⟹ x ∈ dC_F(X, i) ⟹ M(i)" for x X i
unfolding dC_F_def
by auto
moreover
have "uncountable_rel(M,{domain(p) . p ∈ A})"
proof
interpret M_replacement_lepoll M dC_F
using lam_replacement_dC_F domain_eq_separation lam_replacement_inj_rel lam_replacement_minimum
unfolding dC_F_def
proof(unfold_locales,simp_all)
fix X b f
assume "M(X)" "M(b)" "M(f)"
with 2[of X]
show "lam_replacement(M, λx. μ i. x ∈ if_range_F_else_F(λd. {p ∈ X . domain(p) = d}, b, f, i))"
using lam_replacement_dC_F domain_eq_separation
mem_F_bound3 countable_lepoll_assms2 repFun_dom_closed
by (rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈X}"],auto)
qed (auto)
have "∃a∈A. x = domain(a) ⟹ M(dC_F(A,x))" for x
using ‹M(A)› transM[OF _ ‹M(A)›] by (auto)
moreover
have "w ∈ A ∧ domain(w) = x ⟹ M(x)" for w x
using transM[OF _ ‹M(A)›] by auto
ultimately
interpret M_cardinal_UN_lepoll _ "dC_F(A)" "{domain(p). p∈A}"
using lam_replacement_dC_F lam_replacement_inj_rel ‹M(A)›
lepoll_assumptions domain_eq_separation lam_replacement_minimum
countable_lepoll_assms2 repFun_dom_closed
lepoll_assumptions1[OF ‹M(A)› repFun_dom_closed[OF ‹M(A)›]]
apply(unfold_locales)
by(simp_all del:if_range_F_else_F_def,
rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈A}"])
(auto simp del:if_range_F_else_F_def simp add:dC_F_def)
from ‹A ⊆ Fn(nat, I, 2)›
have x:"(⋃d∈{domain(p) . p ∈ A}. {p∈A. domain(p) = d}) = A"
by auto
moreover
assume "countable_rel(M,{domain(p) . p ∈ A})"
moreover
note ‹⋀d. M(d) ⟹ countable_rel(M,{p∈A. domain(p) = d})›
moreover from ‹M(A)›
have "p∈A ⟹ M(domain(p))" for p
by (auto dest: transM)
ultimately
have "countable_rel(M,A)"
using countable_rel_imp_countable_rel_UN
unfolding dC_F_def
by auto
with ‹¬ |A|⇗M⇖ ≤ nat› ‹M(A)›
show False
using countable_rel_iff_cardinal_rel_le_nat by simp
qed
moreover from ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
have "p ∈ A ⟹ Finite(domain(p))" for p
using lesspoll_rel_nat_is_Finite_rel[of "domain(p)"]
lesspoll_nat_imp_lesspoll_rel[of "domain(p)"]
domain_of_fun[of p _ "λ_. 2"] by (auto dest:transM)
moreover
note repFun_dom_closed[OF ‹M(A)›]
ultimately
obtain D where "delta_system(D)" "D ⊆ {domain(p) . p ∈ A}" "D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(D)"
using delta_system_uncountable_rel[of "{domain(p) . p ∈ A}"] by auto
then
have delta:"∀d1∈D. ∀d2∈D. d1 ≠ d2 ⟶ d1 ∩ d2 = ⋂D"
using delta_system_root_eq_Inter
by simp
moreover from ‹D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(D)›
have "uncountable_rel(M,D)"
using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1 by auto
moreover from this and ‹D ⊆ {domain(p) . p ∈ A}›
obtain p1 where "p1 ∈ A" "domain(p1) ∈ D"
using uncountable_rel_not_empty[of D] by blast
moreover from this and ‹p1 ∈ A ⟹ Finite(domain(p1))›
have "Finite(domain(p1))"
using Finite_domain by simp
moreover
define r where "r ≡ ⋂D"
moreover from ‹M(D)›
have "M(r)" "M(r×2)"
unfolding r_def by simp_all
ultimately
have "Finite(r)" using subset_Finite[of "r" "domain(p1)"]
by auto
have "countable_rel(M,{restrict(p,r) . p∈A})"
proof -
note ‹M(Fn(nat, I, 2))› ‹M(r)›
moreover from this
have "f∈Fn(nat, I, 2) ⟹ M(restrict(f,r))" for f
by (blast dest: transM)
ultimately
have "f∈Fn(nat, I, 2) ⟹ restrict(f,r) ∈ Pow_rel(M,r × 2)" for f
using restrict_subset_Sigma[of f _ "λ_. 2" r] Pow_rel_char
by (auto del:FnD dest!:FnD simp: Pi_def) (auto dest:transM)
with ‹A ⊆ Fn(nat, I, 2)›
have "{restrict(f,r) . f ∈ A } ⊆ Pow_rel(M,r × 2)"
by fast
moreover from ‹M(A)› ‹M(r)›
have "M({restrict(f,r) . f ∈ A })"
using RepFun_closed restrict_strong_replacement transM[OF _ ‹M(A)›] by auto
moreover
note ‹Finite(r)› ‹M(r)›
ultimately
show ?thesis
using Finite_Sigma[THEN Finite_Pow_rel, of r "λ_. 2"]
by (intro Finite_imp_countable_rel) (auto intro:subset_Finite)
qed
moreover from ‹M(A)› ‹M(D)›
have "M({p∈A. domain(p) ∈ D})"
using domain_mem_separation by simp
have "uncountable_rel(M,{p∈A. domain(p) ∈ D})" (is "uncountable_rel(M,?X)")
proof
from ‹D ⊆ {domain(p) . p ∈ A}›
have "(λp∈?X. domain(p)) ∈ surj(?X, D)"
using lam_type unfolding surj_def by auto
moreover from ‹M(A)› ‹M(?X)›
have "M(λp∈?X. domain(p))"
using lam_closed[OF domain_replacement ‹M(?X)›] transM[OF _ ‹M(?X)›] by simp
moreover
note ‹M(?X)› ‹M(D)›
moreover from calculation
have surjection:"(λp∈?X. domain(p)) ∈ surj⇗M⇖(?X, D)"
using surj_rel_char by simp
moreover
assume "countable_rel(M,?X)"
moreover
note ‹uncountable_rel(M,D)›
ultimately
show False
using surj_rel_countable_rel[OF _ surjection] by auto
qed
moreover
have "D = (⋃f∈Pow_rel(M,r×2) . {y . p∈A, restrict(p,r) = f ∧ y=domain(p) ∧ domain(p) ∈ D})"
proof -
{
fix z
assume "z ∈ D"
with ‹M(D)›
have ‹M(z)› by (auto dest:transM)
from ‹z∈D› ‹D ⊆ _› ‹M(A)›
obtain p where "domain(p) = z" "p ∈ A" "M(p)"
by (auto dest:transM)
moreover from ‹A ⊆ Fn(nat, I, 2)› ‹M(z)› and this
have "p ∈ z →⇗M⇖ 2"
using domain_of_fun function_space_rel_char by (auto del:FnD dest!:FnD)
moreover from this ‹M(z)›
have "p ∈ z → 2"
using domain_of_fun function_space_rel_char by (auto)
moreover from this ‹M(r)›
have "restrict(p,r) ⊆ r × 2"
using function_restrictI[of p r] fun_is_function[of p z "λ_. 2"]
restrict_subset_Sigma[of p z "λ_. 2" r] function_space_rel_char
by (auto simp:Pi_def)
moreover from ‹M(p)› ‹M(r)›
have "M(restrict(p,r))" by simp
moreover
note ‹M(r)›
ultimately
have "∃p∈A. restrict(p,r) ∈ Pow_rel(M,r×2) ∧ domain(p) = z"
using Pow_rel_char by auto
}
then
show ?thesis
by (intro equalityI) (force)+
qed
from ‹M(D)›‹M(r)›
have "M({y . p∈A, restrict(p,r) = f ∧ y=domain(p) ∧ domain(p) ∈ D})" (is "M(?Y(A,f))")
if "M(f)" "M(A)" for f A
using drSR_Y_closed[unfolded drSR_Y_def] that
by simp
then
obtain f where "uncountable_rel(M,?Y(A,f))" "M(f)"
proof -
have 1:"M(i)"
if "M(B)" "M(x)"
"x ∈ {y . x ∈ B, restrict(x, r) = i ∧ y = domain(x) ∧ domain(x) ∈ D}"
for B x i
using that ‹M(r)›
by (auto dest:transM)
note ‹M(r)›
moreover from this
have "M(Pow⇗M⇖(r × 2))" by simp
moreover
note ‹M(A)› ‹⋀f A. M(f) ⟹ M(A) ⟹ M(?Y(A,f))› ‹M(D)›
moreover from calculation
interpret M_replacement_lepoll M "drSR_Y(r,D)"
using countable_lepoll_assms3 lam_replacement_inj_rel lam_replacement_drSR_Y
drSR_Y_closed lam_Least_assumption_drSR_Y lam_replacement_minimum
by (unfold_locales,simp_all add:drSR_Y_def,rule_tac 1,simp_all)
from calculation
have "x ∈ Pow⇗M⇖(r × 2) ⟹ M(drSR_Y(r, D, A, x))" for x
unfolding drSR_Y_def by (auto dest:transM)
ultimately
interpret M_cardinal_UN_lepoll _ "?Y(A)" "Pow_rel(M,r×2)"
using countable_lepoll_assms3 lam_replacement_drSR_Y
lepoll_assumptions[where S="Pow_rel(M,r×2)", unfolded lepoll_assumptions_defs]
lam_Least_assumption_drSR_Y[unfolded drSR_Y_def] lam_replacement_minimum
unfolding drSR_Y_def
apply unfold_locales
apply (simp_all add:lam_replacement_inj_rel del: if_range_F_else_F_def,rule_tac 1,simp_all)
by ((fastforce dest:transM[OF _ ‹M(A)›])+)
{
from ‹Finite(r)› ‹M(r)›
have "countable_rel(M,Pow_rel(M,r×2))"
using Finite_Sigma[THEN Finite_Pow_rel] Finite_imp_countable_rel
by simp
moreover
assume "M(f) ⟹ countable_rel(M,?Y(A,f))" for f
moreover
note ‹D = (⋃f∈Pow_rel(M,r×2) .?Y(A,f))› ‹M(r)›
moreover
note ‹uncountable_rel(M,D)›
ultimately
have "False"
using countable_rel_imp_countable_rel_UN by (auto dest: transM)
}
with that
show ?thesis
by auto
qed
moreover from this ‹M(A)› and ‹M(f) ⟹ M(A) ⟹ M(?Y(A,f))›
have "M(?Y(A,f))"
by blast
ultimately
obtain j where "j ∈ inj_rel(M,nat, ?Y(A,f))" "M(j)"
using uncountable_rel_iff_nat_lt_cardinal_rel[THEN iffD1, THEN leI,
THEN cardinal_rel_le_imp_lepoll_rel, THEN lepoll_relD]
by auto
with ‹M(?Y(A,f))›
have "j`0 ≠ j`1" "j`0 ∈ ?Y(A,f)" "j`1 ∈ ?Y(A,f)"
using inj_is_fun[THEN apply_type, of j nat "?Y(A,f)"]
inj_rel_char
unfolding inj_def by auto
then
obtain p q where "domain(p) ≠ domain(q)" "p ∈ A" "q ∈ A"
"domain(p) ∈ D" "domain(q) ∈ D"
"restrict(p,r) = restrict(q,r)" by auto
moreover from this and delta
have "domain(p) ∩ domain(q) = r"
unfolding r_def by simp
moreover
note ‹A ⊆ Fn(nat, I, 2)› Fn_nat_abs[OF ‹M(I)› nat_into_M[of 2],simplified]
moreover from calculation
have "p ∈ Fn⇗M⇖(nat, I, 2)" "q ∈ Fn⇗M⇖(nat, I, 2)"
by auto
moreover from calculation
have "p ∪ q ∈ Fn(nat, I, 2)"
using restrict_eq_imp_compat_rel InfCard_rel_nat
by simp
ultimately
have "∃p∈A. ∃q∈A. p ≠ q ∧ compat_in(Fn(nat, I, 2), Fnle(nat, I, 2), p, q)"
unfolding compat_in_def
by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
}
moreover from assms
have "M(Fnle(ω,I,2))"
by simp
moreover note ‹M(Fn(ω,I,2))›
ultimately
show ?thesis using def_ccc_rel by (auto simp:absolut antichain_def) fastforce
qed
end
end