# Theory Cardinal_Preservation

section‹Preservation of cardinals in generic extensions›

theory Cardinal_Preservation
imports
Forcing_Main
begin

context forcing_data1

begin

lemma antichain_abs' [absolut]:
" AM   antichain⇗M⇖(,leq,A)  antichain(,leq,A)"
unfolding antichain_rel_def antichain_def compat_def
using transitivity[of _ A]
by (auto simp add:absolut)

lemma inconsistent_imp_incompatible:
assumes "p  φ env" "q  Neg(φ) env" "p" "q"
"arity(φ)  length(env)" "φ  formula" "env  list(M)"
shows "p  q"
proof
assume "compat(p,q)"
then
obtain d where "d  p" "d  q" "d  " by blast
moreover
note assms
moreover from calculation
have "d  φ env" "d  Neg(φ) env"
using strengthening_lemma by simp_all
ultimately
show "False"
using Forces_Neg[of d env φ] refl_leq
by (auto dest:transitivity; drule_tac bspec; auto dest:transitivity)
qed

notation check (‹_v [101] 100)

end ― ‹localeforcing_data1

locale G_generic2 = G_generic1 + forcing_data2
locale G_generic2_AC = G_generic1_AC + G_generic2

locale G_generic3 = G_generic2 + forcing_data3
locale G_generic3_AC = G_generic2_AC + G_generic3

locale G_generic3_AC_CH = G_generic3_AC + M_ZFC2_ground_CH_trans

sublocale G_generic3_AC  ext:M_ZFC2_trans "M[G]"
using ground_replacements3 replacement_assm_MG
by unfold_locales simp_all

lemma (in forcing_data1) forces_neq_apply_imp_incompatible:
assumes
"p  0`1 is 2 [f,a,bv]"
"q  0`1 is 2 [f,a,b'v]"
"b  b'"
― ‹More general version: taking general names
termbv and termb'v, satisfying
termp  ⋅¬0 = 1 [bv, b'v] and
termq  ⋅¬0 = 1 [bv, b'v].›
and
types:"fM" "aM" "bM" "b'M" "p" "q"
shows
"p  q"
proof -
{
fix G
assume "M_generic(G)"
then
interpret G_generic1 _ _ _ _ _ G by unfold_locales
include G_generic1_lemmas
assume "qG"
with assms M_generic(G)
have "M[G], map(val(G),[f,a,b'v])  0`1 is 2"
using truth_lemma[of "0`1 is 2" "[f,a,b'v]"]
by (auto simp add:ord_simp_union arity_fun_apply_fm
fun_apply_type)
with b  b' types
have "M[G], map(val(G),[f,a,bv])  ⋅¬0`1 is 2"
using GenExtI by auto
}
with types
have "q  ⋅¬0`1 is 2 [f,a,bv]"
using definition_of_forcing[where φ= ]
by (auto simp add:ord_simp_union arity_fun_apply_fm)
with p  0`1 is 2 [f,a,bv] and types
show "p  q"
using inconsistent_imp_incompatible
by (simp add:ord_simp_union arity_fun_apply_fm fun_apply_type)
qed

context M_ctm2_AC
begin

― ‹Simplifying simp rules (because of the occurrence of
termsetclass)›
lemmas sharp_simps = Card_rel_Union Card_rel_cardinal_rel Collect_abs
Cons_abs Cons_in_M_iff Diff_closed Equal_abs Equal_in_M_iff Finite_abs
Forall_abs Forall_in_M_iff Inl_abs Inl_in_M_iff Inr_abs Inr_in_M_iff
Int_closed Inter_abs Inter_closed M_nat Member_abs Member_in_M_iff
Memrel_closed Nand_abs Nand_in_M_iff Nil_abs Nil_in_M Ord_cardinal_rel
Pow_rel_closed Un_closed Union_abs Union_closed and_abs and_closed
apply_abs apply_closed bij_rel_closed bijection_abs bool_of_o_abs
cardinal_rel_closed cardinal_rel_idem cartprod_abs cartprod_closed
cmult_rel_0 cmult_rel_1 cmult_rel_closed comp_closed composition_abs
cons_abs cons_closed converse_abs converse_closed csquare_lam_closed
csquare_rel_closed depth_closed domain_abs domain_closed eclose_abs
eclose_closed empty_abs field_abs field_closed finite_funspace_closed
finite_ordinal_abs fst_closed function_abs function_space_rel_closed
hd_abs image_abs image_closed inj_rel_closed injection_abs inter_abs
irreflexive_abs is_eclose_n_abs is_funspace_abs
iterates_closed length_closed lepoll_rel_refl
limit_ordinal_abs linear_rel_abs
mem_bij_abs mem_eclose_abs mem_inj_abs membership_abs
minimum_closed nat_case_abs nat_case_closed nonempty not_abs
not_closed number1_abs number2_abs number3_abs omega_abs
or_abs or_closed order_isomorphism_abs ordermap_closed
ordertype_closed ordinal_abs pair_abs pair_in_M_iff powerset_abs
pred_closed pred_set_abs quasilist_abs quasinat_abs radd_closed
rall_abs range_abs range_closed relation_abs restrict_closed
restriction_abs rex_abs rmult_closed rtrancl_abs rtrancl_closed
rvimage_closed separation_closed setdiff_abs singleton_abs
singleton_in_M_iff snd_closed strong_replacement_closed subset_abs
succ_in_M_iff successor_abs successor_ordinal_abs sum_abs sum_closed
surj_rel_closed surjection_abs tl_abs trancl_abs trancl_closed
transitive_rel_abs transitive_set_abs typed_function_abs union_abs
upair_abs upair_in_M_iff vimage_abs vimage_closed well_ord_abs
nth_closed Aleph_rel_closed csucc_rel_closed
Card_rel_Aleph_rel

declare sharp_simps[simp del, simplified setclass_iff, simp]

lemmas sharp_intros = nat_into_M Aleph_rel_closed Card_rel_Aleph_rel

declare sharp_intros[rule del, simplified setclass_iff, intro]

end ― ‹localeM_ctm2_AC

context G_generic3_AC begin

context
includes G_generic1_lemmas
begin

lemmas mg_sharp_simps = ext.Card_rel_Union ext.Card_rel_cardinal_rel
ext.Collect_abs ext.Cons_abs ext.Cons_in_M_iff ext.Diff_closed
ext.Equal_abs ext.Equal_in_M_iff ext.Finite_abs ext.Forall_abs
ext.Forall_in_M_iff ext.Inl_abs ext.Inl_in_M_iff ext.Inr_abs
ext.Inr_in_M_iff ext.Int_closed ext.Inter_abs ext.Inter_closed
ext.M_nat ext.Member_abs ext.Member_in_M_iff ext.Memrel_closed
ext.Nand_abs ext.Nand_in_M_iff ext.Nil_abs ext.Nil_in_M
ext.Ord_cardinal_rel ext.Pow_rel_closed ext.Un_closed
ext.Union_abs ext.Union_closed ext.and_abs ext.and_closed
ext.apply_abs ext.apply_closed ext.bij_rel_closed
ext.bijection_abs ext.bool_of_o_abs ext.bool_of_o_closed
ext.cardinal_rel_closed ext.cardinal_rel_idem ext.cartprod_abs
ext.cartprod_closed ext.cmult_rel_0 ext.cmult_rel_1
ext.cmult_rel_closed ext.comp_closed ext.composition_abs
ext.cons_abs ext.cons_closed ext.converse_abs ext.converse_closed
ext.csquare_lam_closed ext.csquare_rel_closed ext.depth_closed
ext.domain_abs ext.domain_closed ext.eclose_abs ext.eclose_closed
ext.empty_abs ext.field_abs ext.field_closed
ext.finite_funspace_closed ext.finite_ordinal_abs
ext.fst_closed ext.function_abs ext.function_space_rel_closed
ext.hd_abs ext.image_abs ext.image_closed ext.inj_rel_closed
ext.injection_abs ext.inter_abs ext.irreflexive_abs
ext.is_eclose_n_abs ext.is_funspace_abs
ext.iterates_closed ext.length_closed
ext.lepoll_rel_refl ext.limit_ordinal_abs ext.linear_rel_abs
ext.mem_bij_abs ext.mem_eclose_abs
ext.mem_inj_abs ext.membership_abs
ext.nat_case_abs ext.nat_case_closed
ext.nonempty ext.not_abs ext.not_closed
ext.number1_abs ext.number2_abs ext.number3_abs ext.omega_abs
ext.or_abs ext.or_closed ext.order_isomorphism_abs
ext.ordermap_closed ext.ordertype_closed ext.ordinal_abs
ext.pair_abs ext.pair_in_M_iff ext.powerset_abs ext.pred_closed
ext.pred_set_abs ext.quasilist_abs ext.quasinat_abs
ext.radd_closed ext.rall_abs ext.range_abs ext.range_closed
ext.relation_abs ext.restrict_closed ext.restriction_abs
ext.rex_abs ext.rmult_closed ext.rtrancl_abs ext.rtrancl_closed
ext.rvimage_closed ext.separation_closed ext.setdiff_abs
ext.singleton_abs ext.singleton_in_M_iff ext.snd_closed
ext.strong_replacement_closed ext.subset_abs ext.succ_in_M_iff
ext.successor_abs ext.successor_ordinal_abs ext.sum_abs
ext.sum_closed ext.surj_rel_closed ext.surjection_abs ext.tl_abs
ext.trancl_abs ext.trancl_closed ext.transitive_rel_abs
ext.transitive_set_abs ext.typed_function_abs ext.union_abs
ext.upair_abs ext.upair_in_M_iff ext.vimage_abs ext.vimage_closed
ext.well_ord_abs ext.nth_closed ext.Aleph_rel_closed
ext.csucc_rel_closed ext.Card_rel_Aleph_rel

― ‹The following was motivated by the fact that
@{thm [source] ext.apply_closed} did not simplify appropriately.›
declare mg_sharp_simps[simp del, simplified setclass_iff, simp]

lemmas mg_sharp_intros = ext.nat_into_M ext.Aleph_rel_closed
ext.Card_rel_Aleph_rel

declare mg_sharp_intros[rule del, simplified setclass_iff, intro]

― ‹Kunen IV.2.31›
lemma forces_below_filter:
assumes "M[G], map(val(G),env)  φ" "p  G"
"arity(φ)  length(env)" "φ  formula" "env  list(M)"
shows "qG. q  p  q  φ env"
proof -
note assms
moreover from this
obtain r where "r  φ env" "rG"
using generic truth_lemma[of φ env]
by blast
moreover from this and pG
obtain q where "q  p" "q  r" "q  G" by auto
ultimately
show ?thesis
using strengthening_lemma[of r φ _ env] by blast
qed

subsection‹Preservation by ccc forcing notions›

lemma ccc_fun_closed_lemma_aux:
assumes "f_dotM" "pM" "aM" "bM"
shows "{q   . q  p  (M, [q, , leq, 𝟭, f_dot, av, bv]  forces(0`1 is 2 ))}  M"
using separation_forces[where env="[f_dot, av, bv]" and φ="0`1 is 2",simplified]
assms G_subset_M[THEN subsetD] generic
separation_in lam_replacement_constant lam_replacement_identity
lam_replacement_product
separation_conj arity_fun_apply_fm union_abs1
by simp_all

lemma ccc_fun_closed_lemma_aux2:
assumes "BM" "f_dotM" "pM" "aM"
shows "(##M)(λbB. {q   . q  p  (M, [q, , leq, 𝟭, f_dot, av, bv]  forces(0`1 is 2 ))})"
proof -
have "separation(##M, λz. M, [snd(z), , leq, 𝟭, f_dot, τ, fst(z)v]  forces(0`1 is 2 ))"
if "τM" for τ
proof -
let ?f_fm="snd_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),fst_fm,2,0)"
note assms
moreover
have "arity(forces(0`1 is 2 ))  7"
using arity_fun_apply_fm union_abs1 arity_forces[of "0`1 is 2 "]
by simp
moreover
have "?f_fm  formula" "arity(?f_fm)  7" "?g_fm  formula" "arity(?g_fm)  8"
using ord_simp_union
unfolding hcomp_fm_def
ultimately
show ?thesis
using separation_sat_after_function assms that sats_fst_fm
snd_abs sats_snd_fm sats_check_fm check_abs fst_abs
unfolding hcomp_fm_def
by simp
qed
with assms
show ?thesis
using lam_replacement_imp_lam_closed separation_conj separation_in
lam_replacement_product lam_replacement_constant transitivity[of _ B]
lam_replacement_snd lam_replacement_Collect' ccc_fun_closed_lemma_aux
by simp
qed

lemma ccc_fun_closed_lemma:
assumes "AM" "BM" "f_dotM" "pM"
shows "(λaA. {bB. q. q  p  (q  0`1 is 2 [f_dot, av, bv])})  M"
proof -
have "separation(##M, λz. M, [snd(z), , leq, 𝟭, f_dot, fst(fst(z))v, snd(fst(z))v]  forces(0`1 is 2 ))"
proof -
let ?f_fm="snd_fm(1,0)"
let ?g="λz . fst(fst(fst(z)))v"
let ?g_fm="hcomp_fm(check_fm(6),hcomp_fm(fst_fm,fst_fm),2,0)"
let ?h_fm="hcomp_fm(check_fm(7),hcomp_fm(snd_fm,fst_fm),3,0)"
note assms
moreover
have "arity(forces(0`1 is 2 ))  7"
using arity_fun_apply_fm union_abs1 arity_forces[of "0`1 is 2 "]
by simp
moreover
have "?f_fm  formula" "arity(?f_fm)  6" "?g_fm  formula" "arity(?g_fm)  7"
"?h_fm  formula" "arity(?h_fm)  8"
using ord_simp_union
unfolding hcomp_fm_def
ultimately
show ?thesis
using separation_sat_after_function3 assms sats_check_fm check_abs
fst_abs snd_abs
unfolding hcomp_fm_def
by simp
qed
moreover
have 1:"separation(##M, λz. M, [snd(z), , leq, 𝟭, f_dot, τ, fst(z)v]  forces(0`1 is 2 ))"
if "τM" for τ
proof -
let ?f_fm="snd_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),fst_fm,2,0)"
note assms
moreover
have "arity(forces(0`1 is 2 ))  7"
using arity_forces[of "0`1 is 2 "] arity_fun_apply_fm union_abs1
by simp
moreover
have "?f_fm  formula" "arity(?f_fm)  7" "?g_fm  formula" "arity(?g_fm)  8"
using ord_simp_union
unfolding hcomp_fm_def
ultimately
show ?thesis
using separation_sat_after_function that fst_abs snd_abs sats_check_fm check_abs
unfolding hcomp_fm_def
by simp
qed
moreover note assms
ultimately
show ?thesis
using lam_replacement_imp_lam_closed lam_replacement_Collect' transitivity[of _ A]
lam_replacement_constant lam_replacement_identity lam_replacement_snd
lam_replacement_product separation_conj separation_in separation_bex separation_iff'
by simp
qed

― ‹Kunen IV.3.5›
lemma ccc_fun_approximation_lemma:
notes le_trans[trans]
assumes "ccc⇗M⇖(,leq)" "AM" "BM" "fM[G]" "f : A  B"
shows
"FM. F : A  Pow⇗M⇖(B)  (aA. f`a  F`a  |F`a|⇗M ω)"
proof -
from fM[G]
obtain f_dot where "f = val(G,f_dot)" "f_dotM" using GenExtD by force
with assms
obtain p where "p  0:12 [f_dot, Av, Bv]" "pG" "pM"
using G_subset_M truth_lemma[of "0:12" "[f_dot, Av, Bv]"]
by (auto simp add:ord_simp_union arity_typed_function_fm
― ‹NOTE: type-checking is not performed here by the Simplifier›
typed_function_type)
define F where "FλaA. {bB. q. q  p  (q  0`1 is 2 [f_dot, av, bv])}"
from assms f_dot_ pM
have "F  M"
unfolding F_def using ccc_fun_closed_lemma by simp
moreover from calculation
have "f`a  F`a" if "a  A" for a
proof -
note f: A  B a  A
moreover from this
have "f ` a  B" by simp
moreover
note fM[G] AM
moreover from calculation
have "M[G], [f, a, f`a]  0`1 is 2"
by (auto dest:transitivity)
moreover
note BM f = val(G,f_dot)
moreover from calculation
have "aM" "val(G, f_dot)`aM"
by (auto dest:transitivity)
moreover
note f_dotM pG
ultimately
obtain q where "q  p" "q  0`1 is 2 [f_dot, av, (f`a)v]" "qG"
using forces_below_filter[of "0`1 is 2" "[f_dot, av, (f`a)v]" p]
by (auto simp add: ord_simp_union arity_fun_apply_fm
fun_apply_type)
with f`a  B
have "f`a  {bB . q. q  p  q  0`1 is 2 [f_dot, av, bv]}"
by blast
with aA
show ?thesis unfolding F_def by simp
qed
moreover
have "|F`a|⇗M ω  F`aM" if "a  A" for a
proof -
let ?Q="λb. {q. q  p  (q  0`1 is 2 [f_dot, av, bv])}"
from F  M aA AM
have "F`a  M" "aM"
using transitivity[OF _ AM] by simp_all
moreover
have 2:"x. xF`a  xM"
using transitivity[OF _ F`aM] by simp
moreover
have 3:"x. xF`a  (##M)(?Q(x))"
using ccc_fun_closed_lemma_aux[OF f_dotM pM aM 2] transitivity[of _ "F`a"]
by simp
moreover
have 4:"lam_replacement(##M,λb. {q   . q  p  (M, [q, , leq, 𝟭, f_dot, av, bv]  forces(0`1 is 2 ))})"
using ccc_fun_closed_lemma_aux2[OF _ f_dotM pM aM]
lam_replacement_iff_lam_closed[THEN iffD2]
ccc_fun_closed_lemma_aux[OF  f_dotM pM aM]
by simp
ultimately
interpret M_Pi_assumptions_choice "##M" "F`a" ?Q
using Pi_replacement1[OF _ 3] lam_replacement_Sigfun[OF 4]
lam_replacement_imp_strong_replacement
ccc_fun_closed_lemma_aux[OF f_dotM pM aM]
lam_replacement_hcomp2[OF lam_replacement_constant 4 _ _
lam_replacement_minimum,unfolded lam_replacement_def]
by unfold_locales simp_all
from F`a  M
interpret M_Pi_assumptions2 "##M" "F`a" ?Q "λ_ . "
using lam_replacement_imp_strong_replacement[OF
lam_replacement_Sigfun[OF lam_replacement_constant]]
Pi_replacement1 transitivity[of _ "F`a"]
by unfold_locales simp_all
from p  0:12 [f_dot, Av, Bv] aA
have "y. y  ?Q(b)" if "b  F`a" for b
using that unfolding F_def by auto
then
obtain q where "q  Pi⇗M⇖(F`a,?Q)" "qM" using AC_Pi_rel by auto
moreover
note F`a  M
moreover from calculation
have "q : F`a →⇗M"
using Pi_rel_weaken_type def_function_space_rel by auto
moreover from calculation
have "q : F`a  range(q)" "q : F`a  " "q : F`a →⇗Mrange(q)"
using mem_function_space_rel_abs range_of_fun by simp_all
moreover
have "q`b  q`c" if "b  F`a" "c  F`a" "b  c"
― ‹For the next step, if the premise termb  c is first,
the proof breaks down badly›
for b c
proof -
from b  F`a c  F`a q  Pi⇗M⇖(F`a,?Q) qM
have "q`b  0`1 is 2 [f_dot, av, bv]"
"q`c  0`1 is 2 [f_dot, av, cv]"
using mem_Pi_rel_abs[of q] apply_type[of _ _  ?Q]
by simp_all
with b  c q : F`a   aA b_ c_
AM f_dotM F`aM
show ?thesis
using forces_neq_apply_imp_incompatible
transitivity[of _ A] transitivity[of _ "F`a"]
by auto
qed
moreover from calculation
have "antichain(,leq,range(q))"
using Pi_range_eq[of _  _ "λ_ . "]
unfolding antichain_def compat_in_def by auto
moreover from this and qM
have "antichain⇗M⇖(,leq,range(q))"
by (simp add:absolut del:P_in_M)
moreover from calculation
have "q`b  q`c" if "b  c" "b  F`a" "c  F`a" for b c
using that Incompatible_imp_not_eq apply_type
mem_function_space_rel_abs by simp
ultimately
have "q  inj⇗M⇖(F`a,range(q))"
using def_inj_rel by auto
with F`a  M qM
have "|F`a|⇗M |range(q)|⇗M⇖"
using def_lepoll_rel
by (rule_tac lepoll_rel_imp_cardinal_rel_le) auto
also from ‹antichain⇗M⇖(,leq,range(q)) ‹ccc⇗M⇖(,leq) qM
have "|range(q)|⇗M ω"
using def_ccc_rel by simp
finally
show ?thesis using F`aM by auto
qed
moreover from this
have "F`aM" if "aA" for a
using that by simp
moreover from this BM
have "F : A  Pow⇗M⇖(B)"
using Pow_rel_char
unfolding F_def by (rule_tac lam_type) auto
ultimately
show ?thesis by auto
qed

end ― ‹G\_generic1\_lemmas bundle›

end ― ‹localeG_generic3_AC

end