Theory Cohen_Posets_Relative
section‹Cohen forcing notions›
theory Cohen_Posets_Relative
imports
Cohen_Posets
Delta_System_Relative
begin
locale M_cohen= M_delta +
assumes
separation_domain_pair: "M(A) ⟹ separation(M, λp. ∀x∈A. x ∈ snd(p) ⟷ domain(x) = fst(p))"
and
separation_restrict_eq_dom_eq:
"M(A) ⟹ M(B) ⟹ ∀x[M]. separation(M, λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r))"
and
separation_restrict_eq_dom_eq_pair:
"M(A) ⟹ M(B) ⟹ M(D) ⟹
separation(M, λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r)))"
and
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)⟩)"
and
domain_mem_separation: "M(A) ⟹ separation(M, λx . domain(x)∈A)"
and
domain_eq_separation: "M(p) ⟹ separation(M, λx . domain(x) = p)"
and
restrict_eq_separation: "M(r) ⟹ M(p) ⟹ separation(M, λx . restrict(x,r) = p)"
context M_cardinal_library
begin
lemma lesspoll_nat_imp_lesspoll_rel :
assumes "A ≺ ω" "M(A)"
shows "A ≺⇗M⇖ ω"
proof -
note assms
moreover from this
obtain f n where "f∈bij⇗M⇖(A,n)" "n∈ω" "A ≈⇗M⇖ n"
using lesspoll_nat_is_Finite using Finite_rel_def[of M A] by auto
moreover from calculation
have "A ≲⇗M⇖ ω"
using lesspoll_nat_is_Finite Infinite_imp_nats_lepoll_rel[of ω n]
nat_not_Finite eq_lepoll_rel_trans[of A n ω]
by auto
moreover from calculation
have "¬ g ∈ bij⇗M⇖(A,ω)" for g
using mem_bij_rel unfolding lesspoll_def by auto
ultimately
show ?thesis unfolding lesspoll_rel_def eqpoll_rel_def bij_rel_is_inj_rel rex_def
by auto
qed
lemma Finite_imp_lesspoll_rel_nat :
assumes "Finite(A)" "M(A)"
shows "A ≺⇗M⇖ ω"
using Finite_imp_lesspoll_nat assms lesspoll_nat_imp_lesspoll_rel by auto
lemma InfCard_rel_lesspoll_rel_Un :
includes Ord_dests
assumes "InfCard_rel(M,κ)" "A ≺⇗M⇖ κ" "B ≺⇗M⇖ κ"
and types: "M(κ)" "M(A)" "M(B)"
shows "A ∪ B ≺⇗M⇖ κ"
proof -
from assms
have "|A|⇗M⇖ < κ" "|B|⇗M⇖ < κ"
using lesspoll_rel_cardinal_rel_lt InfCard_rel_is_Card_rel by auto
show ?thesis
proof (cases "Finite(A) ∧ Finite(B)")
case True
with assms
show ?thesis
using lesspoll_rel_trans2[OF _ le_imp_lepoll_rel, of _ nat κ]
Finite_imp_lesspoll_rel_nat[OF Finite_Un]
unfolding InfCard_rel_def by simp
next
case False
with types
have "InfCard_rel(M,max(|A|⇗M⇖,|B|⇗M⇖))"
using Infinite_InfCard_rel_cardinal_rel InfCard_rel_is_Card_rel
le_trans[of nat] not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖"]
unfolding max_def InfCard_rel_def
by (auto)
with ‹M(A)› ‹M(B)›
have "|A ∪ B|⇗M⇖ ≤ max(|A|⇗M⇖,|B|⇗M⇖)"
using cardinal_rel_Un_le[of "max(|A|⇗M⇖,|B|⇗M⇖)" A B]
not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖" ]
unfolding max_def by simp
moreover from ‹|A|⇗M⇖ < κ› ‹|B|⇗M⇖ < κ›
have "max(|A|⇗M⇖,|B|⇗M⇖) < κ"
unfolding max_def by simp
ultimately
have "|A ∪ B|⇗M⇖ < κ"
using lt_trans1 by blast
moreover
note ‹InfCard_rel(M,κ)›
moreover from calculation types
have "|A ∪ B|⇗M⇖ ≺⇗M⇖ κ"
using lt_Card_rel_imp_lesspoll_rel InfCard_rel_is_Card_rel by simp
ultimately
show ?thesis
using cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[of "A ∪ B" "|A ∪ B|⇗M⇖" κ]
eqpoll_rel_sym types by simp
qed
qed
end
locale M_add_reals= M_cohen + add_reals
begin
lemmas zero_lesspoll_rel_kappa= zero_lesspoll_rel[OF zero_lt_kappa]
end
declare (in M_trivial) compat_in_abs[absolut]
definition
antichain_rel :: "[i⇒o,i,i,i] ⇒ o" (‹antichain⇗_⇖'(_,_,_')›) where
"antichain_rel(M,P,leq,A) ≡ subset(M,A,P) ∧ (∀p[M]. ∀q[M].
p∈A ⟶ q∈A ⟶ p ≠ q⟶ ¬ is_compat_in(M,P,leq,p,q))"
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
definition
ccc_rel :: "[i⇒o,i,i] ⇒ o" (‹ccc⇗_⇖'(_,_')›) where
"ccc_rel(M,P,leq) ≡ ∀A[M]. antichain_rel(M,P,leq,A) ⟶
(∀κ[M]. is_cardinal(M,A,κ) ⟶ (∃om[M]. omega(M,om) ∧ le_rel(M,κ,om)))"
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_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 separation_restrict_eq_dom_eq separation_restrict_eq_dom_eq_pair
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 :
notes Sep_and_Replace [simp]
assumes "M(I)"
shows "ccc⇗M⇖(Fn(nat,I,2), Fnle(nat,I,2))"
proof -
from assms
have "M(Fn(nat,I,2))" using Fn_nat_eq_FiniteFun by simp
{
fix A
assume "¬ |A|⇗M⇖ ≤ nat" "M(A)"
then
have "M({domain(p) . p ∈ A})"
using RepFun_closed domain_replacement_simp transM[OF _ ‹M(A)›]
by auto
assume "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))") (force dest: transM)+
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 "{p ∈ A . domain(p) = d} = 0"
using function_space_rel_char[of _ 2, OF transM, of _ A]
apply (intro equalityI)
apply (clarsimp)
apply (rule lesspoll_nat_imp_lesspoll_rel[of "domain(_)", THEN [2] swap])
apply (auto dest!: domain_of_fun[ of _ _ "λ_. 2"] dest:transM)
done
then
show ?thesis using empty_lepoll_relI by auto
qed
moreover
have "uncountable_rel(M,{domain(p) . p ∈ A})"
proof
have 1:"M({domain(p) . p ∈ A'})" if "M(A')" for A'
using that RepFun_closed domain_replacement_simp transM[OF _ that]
by auto
moreover
have " M(x) ⟹ x ∈ A ∧ domain(x) = i ⟹ M(i)" for A x i
by auto
moreover from calculation
interpret M_replacement_lepoll M dC_F
using lam_replacement_dC_F domain_eq_separation separation_domain_pair
lam_replacement_inj_rel
unfolding dC_F_def
apply unfold_locales apply(simp_all)
proof -
fix A b f
assume "M(A)" "M(b)" "M(f)"
with calculation[of A]
show "lam_replacement(M, λx. μ i. x ∈ if_range_F_else_F(λd. {p ∈ A . domain(p) = d}, b, f, i))"
using lam_replacement_dC_F separation_domain_pair domain_eq_separation
mem_F_bound3 countable_lepoll_assms2
unfolding dC_F_def
by (rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈A}"])
(auto)
qed
note ‹M({domain(p). p∈A})› ‹M(A)›
moreover from this
have "x ∈ A ⟹ M({p ∈ A . domain(p) = domain(x)})" for x
using separation_closed domain_eq_separation transM[OF _ ‹M(A)›] by simp
ultimately
interpret M_cardinal_UN_lepoll _ "dC_F(A)" "{domain(p). p∈A}"
using countable_lepoll_assms2
lepoll_assumptions transM[of _ A]
lepoll_assumptions1[OF ‹M(A)› ‹M({domain(p) . p ∈ A})›]
domain_eq_separation
lam_replacement_inj_rel lam_replacement_dC_F[OF _ _ separation_domain_pair]
unfolding dC_F_def
apply (unfold_locales)
apply(simp del:if_range_F_else_F_def,simp)
apply (rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈A}"], auto)
done
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 ‹M({domain(p). p∈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 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) . {domain(p) .. p∈A, restrict(p,r) = f ∧ 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 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({domain(p) .. p∈A, restrict(p,r) = f ∧ domain(p) ∈ D})" (is "M(?Y(A,f))")
if "M(f)" "M(A)" for f A
using that RepFun_closed domain_replacement_simp
separation_conj[OF restrict_eq_separation[OF ‹M(r)› ‹M(f)›]
domain_mem_separation[OF ‹M(D)›]]
transM[OF _ ‹M(D)›]
by simp
obtain f where "uncountable_rel(M,?Y(A,f))" "M(f)"
proof -
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
apply (unfold_locales, simp_all)
apply (rule_tac [2] lam_Least_assumption_drSR_Y)
apply(simp_all add:drSR_Y_def)
proof -
fix i A x
assume "∃xa∈A. restrict(xa, r) = i ∧ domain(xa) ∈ D ∧ x = domain(xa)" "M(A)" "M(r)"
moreover from this
obtain xa where "xa∈A" "restrict(xa, r) = i" by blast
ultimately
show "M(i)" by (auto dest:transM)
qed
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 lepoll_assumptions[where S="Pow_rel(M,r×2)", unfolded lepoll_assumptions_defs]
lam_replacement_drSR_Y
unfolding drSR_Y_def
apply unfold_locales apply (simp_all add:lam_replacement_inj_rel del:Sep_and_Replace if_range_F_else_F_def)
unfolding drSR_Y_def[symmetric]
apply (rule_tac lam_Least_assumption_drSR_Y)
by (simp_all add: del:Sep_and_Replace if_range_F_else_F_def)
((fastforce dest:transM[OF _ ‹M(A)›])+)[2]
{
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)›
moreover from calculation
have "p ∪ q ∈ Fn(nat, I, 2)"
using restrict_eq_imp_compat InfCard_nat by blast
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