Theory Cardinal_Preservation
theory Cardinal_Preservation
imports
Cohen_Posets_Relative
Forcing_Main
ZF_Trans_Interpretations
begin
context forcing_notion
begin
definition
antichain :: "i⇒o" where
"antichain(A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A. p ≠ q ⟶ p ⊥ q)"
definition
ccc :: "o" where
"ccc ≡ ∀A. antichain(A) ⟶ |A| ≤ ω"
end
locale M_trivial_notion= M_trivial + forcing_notion
begin
abbreviation
antichain_r' :: "i ⇒ o" where
"antichain_r'(A) ≡ antichain_rel(M,P,leq,A)"
lemma antichain_abs' [absolut]:
"⟦ M(A); M(P); M(leq) ⟧ ⟹ antichain_r'(A) ⟷ antichain(A)"
unfolding antichain_rel_def antichain_def compat_def
by (simp add:absolut)
end
text‹The following interpretation makes the simplifications from the
locales ‹M_trans›, ‹M_trivial›, etc., available for ‹M[G]››
sublocale forcing_data ⊆ M_trivial_notion "##M" ..
context forcing_data
begin
lemma antichain_abs'' [absolut]: "A∈M ⟹ antichain_r'(A) ⟷ antichain(A)"
using P_in_M leq_in_M
unfolding antichain_rel_def antichain_def compat_def
by (auto simp add:absolut transitivity)
end
lemma (in forcing_notion) Incompatible_imp_not_eq : "⟦ p ⊥ q; p∈P; q∈P ⟧⟹ p ≠ q"
using refl_leq by blast
lemma (in forcing_data) inconsistent_imp_incompatible :
assumes "p ⊩ φ env" "q ⊩ Neg(φ) env" "p∈P" "q∈P"
"arity(φ) ≤ length(env)" "φ ∈ formula" "env ∈ list(M)"
shows "p ⊥ q"
proof
assume "compat(p,q)"
then
obtain d where "d ≼ p" "d ≼ q" "d ∈ P" 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 P_in_M
by (auto dest:transM; drule_tac bspec; auto dest:transM)
qed
notation (in forcing_data) check (‹_⇧v› [101] 100)
context G_generic begin
lemmas generic_simps= generic[THEN one_in_G, THEN valcheck, OF one_in_P]
generic[THEN one_in_G, THEN M_subset_MG, THEN subsetD]
check_in_M GenExtI P_in_M
lemmas generic_dests= M_genericD[OF generic] M_generic_compatD[OF generic]
bundle G_generic_lemmas = generic_simps[simp] generic_dests[dest]
end
sublocale G_generic ⊆ ext:M_ZF_trans "M[G]"
using Transset_MG generic pairing_in_MG Union_MG
extensionality_in_MG power_in_MG foundation_in_MG
strong_replacement_in_MG separation_in_MG infinity_in_MG
by unfold_locales simp_all
sublocale G_generic_AC ⊆ ext:M_ZFC_trans "M[G]"
using choice_ax choice_in_MG
by unfold_locales
lemma (in forcing_data) forces_neq_apply_imp_incompatible :
assumes
"p ⊩ ⋅0`1 is 2⋅ [f,a,b⇧v]"
"q ⊩ ⋅0`1 is 2⋅ [f,a,b'⇧v]"
"b ≠ b'"
and
types:"f∈M" "a∈M" "b∈M" "b'∈M" "p∈P" "q∈P"
shows
"p ⊥ q"
proof -
{
fix G
assume "M_generic(G)"
then
interpret G_generic _ _ _ _ _ G by unfold_locales
include G_generic_lemmas
assume "q∈G"
with assms ‹M_generic(G)›
have "M[G], map(val(P,G),[f,a,b'⇧v]) ⊨ ⋅0`1 is 2⋅"
using truth_lemma[of "⋅0`1 is 2⋅" G "[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(P,G),[f,a,b⇧v]) ⊨ ⋅¬⋅0`1 is 2⋅⋅"
using GenExtI by auto
}
with types
have "q ⊩ ⋅¬⋅0`1 is 2⋅⋅ [f,a,b⇧v]"
using definition_of_forcing[where φ="⋅¬⋅0`1 is 2⋅⋅" ] check_in_M
by (auto simp add:ord_simp_union arity_fun_apply_fm)
with ‹p ⊩ ⋅0`1 is 2⋅ [f,a,b⇧v]› and types
show "p ⊥ q"
using check_in_M inconsistent_imp_incompatible
by (simp add:ord_simp_union arity_fun_apply_fm fun_apply_type)
qed
context G_generic_AC begin
context
includes G_generic_lemmas
begin
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
bool_of_o_closed cadd_rel_0 cadd_rel_closed cardinal_rel_0_iff_0
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 formula_N_abs formula_N_closed formula_abs
formula_case_abs formula_case_closed formula_closed
formula_functor_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_depth_apply_abs is_eclose_n_abs is_funspace_abs
iterates_closed le_abs length_abs length_closed lepoll_rel_refl
limit_ordinal_abs linear_rel_abs list_N_abs list_N_closed list_abs
list_case'_closed list_case_abs list_closed list_functor_abs lt_abs
mem_bij_abs mem_eclose_abs mem_inj_abs mem_list_abs membership_abs
minimum_closed nat_case_abs nat_case_closed nonempty not_abs
not_closed nth_abs 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
mem_formula_abs fst_abs snd_abs nth_closed
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.cadd_rel_0 ext.cadd_rel_closed ext.cardinal_rel_0_iff_0
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.formula_N_abs
ext.formula_N_closed ext.formula_abs ext.formula_case_abs
ext.formula_case_closed ext.formula_closed ext.formula_functor_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_depth_apply_abs ext.is_eclose_n_abs ext.is_funspace_abs
ext.iterates_closed ext.le_abs ext.length_abs ext.length_closed
ext.lepoll_rel_refl ext.limit_ordinal_abs ext.linear_rel_abs
ext.list_N_abs ext.list_N_closed ext.list_abs
ext.list_case'_closed ext.list_case_abs ext.list_closed
ext.list_functor_abs ext.lt_abs ext.mem_bij_abs ext.mem_eclose_abs
ext.mem_inj_abs ext.mem_list_abs ext.membership_abs
ext.minimum_closed ext.nat_case_abs ext.nat_case_closed
ext.nonempty ext.not_abs ext.not_closed ext.nth_abs
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.mem_formula_abs ext.nth_closed
declare sharp_simps[simp del, simplified setclass_iff, simp]
declare mg_sharp_simps[simp del, simplified setclass_iff, simp]
lemma forces_below_filter :
assumes "M[G], map(val(P,G),env) ⊨ φ" "p ∈ G"
"arity(φ) ≤ length(env)" "φ ∈ formula" "env ∈ list(M)"
shows "∃q∈G. q ≼ p ∧ q ⊩ φ env"
proof -
note assms
moreover from this
obtain r where "r ⊩ φ env" "r∈G"
using generic truth_lemma[of φ _ env]
by blast
moreover from this and ‹p∈G›
obtain q where "q ≼ p" "q ≼ r" "q ∈ G" by auto
ultimately
show ?thesis
using strengthening_lemma[of r φ _ env] by blast
qed
abbreviation
fm_leq :: "[i,i,i] ⇒ i" (‹⋅_≼⇗_⇖_⋅›) where
"fm_leq(A,l,B) ≡ leq_fm(l,A,B)"
simple_rename "ren_F" src "[x_P, x_leq, x_o, x_f, y_c, x_bc, p, x, b]"
tgt "[x_bc, y_c,b,x, x_P, x_leq, x_o, x_f, p]"
simple_rename "ren_G" src "[x,x_P, x_leq, x_one, x_f,x_p,y,x_B]"
tgt "[x,y,x_P, x_leq, x_one, x_f,x_p,x_B]"
simple_rename "ren_F_aux" src "[q,x_P, x_leq, x_one, f_dot, x_a, x_bc,x_p,x_b]"
tgt "[x_bc, q, x_b, x_P, x_leq, x_one, f_dot,x_a,x_p]"
simple_rename "ren_G_aux" src "[ x_b, x_P, x_leq, x_one, f_dot,x_a,x_p,y]"
tgt "[ x_b, y, x_P, x_leq, x_one, f_dot,x_a,x_p]"
lemma ccc_fun_closed_lemma_aux :
assumes "f_dot∈M" "p∈M" "a∈M" "b∈M"
shows "{q ∈ P . q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))} ∈ M"
proof -
let ?app_fm="⋅0`1 is 2⋅"
let ?ψ="⋅⋅0 ≼⇗2⇖ 7⋅ ∧ forces(?app_fm) ⋅ "
let ?Q="λ q . q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v] ⊨ forces(?app_fm))"
have "?app_fm ∈ formula" "arity(?app_fm) = 3"
using arity_fun_apply_fm union_abs1
by simp_all
then
have "arity(forces(?app_fm)) ≤ 7"
using arity_forces[OF ‹?app_fm∈_›] by simp_all
then
have "arity(?ψ) ≤ 8" "?ψ∈formula"
using arity_leq_fm union_abs2 union_abs1 le_trans
by simp_all
with ‹a∈M› ‹b∈M›
have "a⇧v∈M" "b⇧v∈M"
by simp_all
note types=‹f_dot∈_› ‹p∈M› P_in_M leq_in_M one_in_M ‹a⇧v∈M› ‹b⇧v∈M›
then
have sats:"(M,[q, P, leq, one, f_dot,a⇧v, b⇧v,p] ⊨?ψ) ⟷ ?Q(q)" if "q∈P" for q
proof -
note types'= types transitivity[OF ‹q∈_› ‹P∈_›]
with types' ‹arity(forces(_))≤_›
have
"?Q(q) ⟷ q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v,p] ⊨ forces(?app_fm))"
using arity_sats_iff[of _ "[p]" _ "[_, _, _, _, _, _, _]"]
by simp
also from types'
have "... ⟷ (M, [q,P, leq, one, f_dot, a⇧v, b⇧v,p] ⊨ ?ψ)"
(is "_ ⟷ _, ?η ⊨ _")
unfolding leq_fm_def using transitivity[of _ P]
by auto
ultimately
show ?thesis by simp
qed
with types ‹?ψ∈_› ‹arity(?ψ) ≤ 8›
show "{q∈P. ?Q(q)}∈M"
using separation_in_M[where Q="?Q" and env="[P, leq, one, f_dot,a⇧v, b⇧v,p]"]
by simp
qed
lemma ccc_fun_closed_lemma_aux2 :
assumes "B∈M" "f_dot∈M" "p∈M" "a∈M"
shows "(##M)(λb∈B. {q ∈ P . q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))})"
proof -
let ?app_fm="⋅0`1 is 2⋅"
let ?Q="λ b q . q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v] ⊨ forces(?app_fm))"
from assms
have closed:"{q∈P . ?Q(b,q)} ∈ M" if "b∈B" for b
using ccc_fun_closed_lemma_aux transitivity[OF _ ‹B∈_›] that
by simp
let ?ψ="( ⋅⋅0 ≼⇗2⇖ 7⋅ ∧ forces(?app_fm) ⋅ )"
let ?G="(⋅∃⋅⋅2⇧v5 is 0⋅ ∧ ren(?ψ) ` 9 ` 9 ` ren_F_aux_fn ⋅⋅)"
have "?app_fm ∈ formula" "arity(?app_fm) = 3"
using arity_fun_apply_fm union_abs1
by simp_all
then
have "arity(forces(?app_fm)) ≤ 7"
using arity_forces[OF ‹?app_fm∈_›] by simp_all
then
have "arity(?ψ) ≤ 9"
using arity_leq_fm union_abs2 union_abs1 le_trans
by simp
then
have "ren(?ψ)`9`9`ren_F_aux_fn ∈ formula" "arity(ren(?ψ)`9`9`ren_F_aux_fn) ≤ 9"
using arity_ren ren_tc ren_F_aux_thm check_fm_type leq_fm_type ren_F_aux_fn_def pred_le
by simp_all
with ‹arity(forces(_))≤7›
have "arity(?G) ≤ 8" "?G∈formula"
using check_fm_type arity_check_fm pred_Un_distrib pred_le Un_le
by simp_all
have "pred(arity(?G)) ≤ 9" "pred(arity(?G))∈nat"
using pred_le[OF _ ‹arity(?G)≤8›] le_trans pred_type[OF _ ‹arity(?G)≤8›]
by simp_all
have "pred(arity(?G)) ≤ 8"
using le_trans pred_le ‹arity(?G)≤8›
by simp_all
note types=‹f_dot∈_› ‹p∈M› P_in_M leq_in_M one_in_M ‹a∈M› ‹B∈M›
from ‹a∈M›
have "a⇧v∈M" by simp
have sats:"(M, [q,b, P, leq, one, f_dot, a⇧v, p] ⊨ ?G) ⟷ ?Q(b,q)" if "b∈B" "q∈M" for b q
proof -
from that
have "b⇧v∈M" "b∈M"
using transitivity[OF _ ‹B∈_›] by simp_all
note types'=‹a⇧v∈M› types ‹b∈M› ‹b⇧v∈M› that
from types' ‹arity(forces(_))≤7›
have"?Q(b,q) ⟷
(q ≼ p ∧ (M, [q,P,leq,one,f_dot,a⇧v,b⇧v,p,b] ⊨ forces(?app_fm)))"
using arity_sats_iff[of _ "[p,b]" _ "[_, _, _, _, _,_, _]"] transitivity[of _ P]
by simp
also from types'
have "... ⟷ (M, [q,P, leq, one, f_dot, a⇧v, b⇧v,p,b] ⊨ ?ψ)"
(is "_ ⟷ _, ?η ⊨ _")
using sats_leq_fm[of 2 0 7] leq_abs
by simp
also from types' ‹arity(forces(_))≤_› ‹arity(?ψ)≤ 9› ren_F_aux_fn_def
have "... ⟷ M, [b⇧v,q,b, P, leq, one, f_dot,a⇧v,p] ⊨ ren(?ψ)`9`9`ren_F_aux_fn"
(is "_ ⟷ _, ?η' ⊨ ?ψ'")
using sats_iff_sats_ren[of ?ψ 9 9 ?η M ?η']ren_F_aux_thm(1)[where A=M] ren_F_aux_thm
by auto
also from assms types'
have "... ⟷ M, [q,b,P, leq, one, f_dot,a⇧v,p] ⊨ ?G" (is "_ ⟷ M,?η''⊨_")
using sats_check_fm[of 5 "[_]@?η''" 2 0] check_abs
by simp
ultimately
show ?thesis
by simp
qed
then
have sats':"(M,[q,b,P, leq, one, f_dot,a⇧v,p,y] ⊨?G) ⟷ ?Q(b,q)"
if "b∈B" "q∈M" "y∈M" for b q y
proof -
from that ‹?G∈_› ‹arity(?G)≤8› types
have "(M,[q,b, P, leq, one, f_dot,a⇧v,p,y] ⊨?G) ⟷ M,[q,b,P, leq, one, f_dot,a⇧v,p] ⊨?G"
using transitivity[of b B] transitivity[of q P]
arity_sats_iff[of ?G "[y]" M "[q,b, P, leq, one, f_dot,a⇧v,p]"]
by simp
then show ?thesis using sats[OF ‹b∈B› ‹q∈M›] that
by simp
qed
from types
have sats_col:"(M,[b,P, leq, one, f_dot,a⇧v,p,y] ⊨Collect_fm(1,?G,7)) ⟷
is_Collect(##M,P,?Q(b),y)" if "b∈B" "y∈M" for b y
using that sats'[OF ‹b∈B›] sats_Collect_fm[of M "?Q(b)"]
transitivity[OF ‹b∈B› ‹B∈M›]
by simp
from ‹pred(arity(?G))∈nat› ‹?G∈_›
have "Collect_fm(1,?G,7) ∈ formula" "arity(Collect_fm(1,?G,7)) ≤ 8"
using arity_Collect_fm pred_le union_abs1 Un_le[OF _ ‹pred(arity(?G))≤ 8 ›,of 8 ]
by (simp_all)
then
have "arity(ren(Collect_fm(1,?G,7))`8`8`ren_G_aux_fn) ≤ 8"
"ren(Collect_fm(1,?G,7))`8`8`ren_G_aux_fn ∈ formula" (is "?Γ∈_")
using ren_tc[of "Collect_fm(1,?G,7)"] ren_G_aux_thm(2) ren_G_aux_fn_def arity_ren
by simp_all
from ‹arity(Collect_fm(1,?G,7))≤_› ‹Collect_fm(1,?G,7)∈_› types
have "(M,[b,y,P, leq, one, f_dot,a⇧v,p] ⊨?Γ) ⟷
M,[b,P, leq, one, f_dot,a⇧v,p,y] ⊨ Collect_fm(1,?G,7)" if "b∈B" "y∈M" for b y
using sats_iff_sats_ren[of "Collect_fm(1,?G,7)" 8 8 _ M "[b,y,P, leq, one, f_dot,a⇧v,p]"]
ren_G_aux_thm(1)[where A=M] ren_G_aux_thm(2) transitivity[of b B] that ren_G_aux_fn_def
by simp
then
have "(M,[b,y,P, leq, one, f_dot,a⇧v,p] ⊨ren(Collect_fm(1,?G,7))`8`8`ren_G_aux_fn) ⟷
y = {q∈P . ?Q(b,q)}" if "b∈B" "y∈M" for y b
using that iff_trans[OF _ sats_col]
Collect_abs types
by auto
with assms types ‹?Γ∈_› ‹arity(?Γ)≤_›
show ?thesis
using closed Lambda_in_M[where env="[P, leq, one, f_dot,a⇧v,p]"
and φ="ren(Collect_fm(1,?G,7))`8`8`ren_G_aux_fn"]
by simp
qed
lemma ccc_fun_closed_lemma :
assumes "A∈M" "B∈M" "f_dot∈M" "p∈M"
shows "(λa∈A. {b∈B. ∃q∈P. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}) ∈ M"
proof -
let ?app_fm="⋅0`1 is 2⋅"
let ?ψ="(⋅∃⋅⋅0 ∈ 1⋅ ∧ ⋅ ⋅0 ≼⇗2⇖ 7⋅ ∧ forces(?app_fm) ⋅⋅⋅)"
let ?G="(⋅∃⋅⋅2⇧v5 is 0⋅ ∧ (⋅∃⋅⋅2⇧v6 is 0⋅ ∧ ren(?ψ) ` 9 ` 9 ` ren_F_fn⋅⋅)⋅⋅)"
let ?Q="λ x b . (∃q∈P. q ≼ p ∧ (M, [q, P, leq, one, f_dot, x⇧v, b⇧v] ⊨ forces(?app_fm)))"
have "?app_fm ∈ formula" "arity(?app_fm) = 3"
using arity_fun_apply_fm union_abs1
by simp_all
then
have "arity(forces(?app_fm)) ≤ 7"
using arity_forces[OF ‹?app_fm∈_›] by simp_all
then
have "arity(?ψ) ≤ 9"
using arity_leq_fm union_abs2 union_abs1 le_trans
by simp
then
have "ren(?ψ)`9`9`ren_F_fn ∈ formula" "pred(pred(arity(ren(?ψ)`9`9`ren_F_fn))) ≤ 7"
using arity_ren ren_tc ren_F_thm check_fm_type leq_fm_type ren_F_fn_def pred_le
by simp_all
with ‹arity(forces(_))≤7›
have "arity(?G) ≤ 7" "?G∈formula"
using check_fm_type arity_check_fm pred_Un_distrib Un_le
by simp_all
have "pred(arity(?G)) ≤ 8" "pred(arity(?G))∈nat"
using pred_le[OF _ ‹arity(?G)≤7›] le_trans pred_type[OF _ ‹arity(?G)≤7›]
by simp_all
note types=‹f_dot∈_› ‹p∈M› P_in_M leq_in_M one_in_M ‹A∈M› ‹B∈M›
{fix x
assume "x∈A"
with ‹A∈M›
have "x∈M" "x⇧v∈M"
using transitivity[of x A]
by simp_all
{
fix b
assume "b∈M"
then
have "b∈M"
using transitivity[OF _ ‹B∈_›] check_in_M by simp_all
note types'=‹x∈A› ‹x∈M› ‹x⇧v∈M› types ‹b∈M›
from types' ‹arity(forces(_))≤7›
have
"?Q(x,b) ⟷
(∃q∈P. q ≼ p ∧ (M, [q,P,leq,one,f_dot,x⇧v,b⇧v,p,x,b] ⊨ forces(?app_fm)))"
using arity_sats_iff[of _ "[p,x,b]" _ "[_, _, _, _, _, _, _]"] transitivity[of _ P]
by simp
also from types'
have "... ⟷ (M, [P, leq, one, f_dot, x⇧v, b⇧v,p,x,b] ⊨ ?ψ)"
(is "_ ⟷ _, ?η ⊨ _")
unfolding leq_fm_def using transitivity[of _ P]
by auto
also from types' ‹arity(forces(_))≤_› ‹arity(?ψ)≤ 9› ren_F_fn_def
have "... ⟷ M, [b⇧v, x⇧v, b, x, P, leq, one, f_dot, p] ⊨ ren(?ψ)`9`9`ren_F_fn"
(is "_ ⟷ _, ?η' ⊨ ?ψ'")
using sats_iff_sats_ren[of ?ψ 9 9 ?η M ?η']ren_F_thm(1)[where A=M] ren_F_thm
by auto
also from assms types'
have "... ⟷ M, [b,x,P, leq, one, f_dot,p] ⊨ ?G" (is "_ ⟷ M,?η''⊨_")
using sats_check_fm[of 5 "[_]@?η''"] sats_check_fm[of 6 "[_,_]@?η''"] check_abs
by simp
ultimately
have "?Q(x,b) ⟷ M,?η''⊨?G" by simp
}
then
have sats:"(M,[b, x, P, leq, one, f_dot,p] ⊨?G) ⟷ ?Q(x,b)" if "b∈M" for b
using that by simp
from types ‹x∈M› ‹arity(?G) ≤ 7› ‹?G∈_›
have sep:"{b∈B. ?Q(x,b)}∈M"
using sats Collect_in_M[where env="[x, P, leq, one, f_dot,p]"]
by simp
note sats sep
}
moreover from this
have sats:"(M,[b, x, P, leq, one, f_dot,p] ⊨?G) ⟷ ?Q(x,b)" if "b∈M" "x∈A" for b x
using that by simp
moreover from calculation
have closed:"{b∈B. ?Q(x,b)}∈M" if "x∈A" for x using that by simp
have sats':"(M,[b, x,P, leq, one, f_dot,p,y,B] ⊨?G) ⟷ ?Q(x,b)"
if "b∈M" "x∈A" "y∈M" for b x y
proof -
from that ‹?G∈_› ‹arity(?G)≤7› types
have "(M,[b, x,P, leq, one, f_dot,p,y,B] ⊨?G) ⟷ M,[b, x,P, leq, one, f_dot,p] ⊨?G"
using transitivity[of x A] arity_sats_iff[of ?G "[y,B]" M "[b, x,P, leq, one, f_dot,p]"]
by simp
then show ?thesis using sats that
by simp
qed
from types
have sats_col:"(M,[x,P, leq, one, f_dot,p,y,B] ⊨Collect_fm(7,?G,6)) ⟷
is_Collect(##M,B,λz.?Q(x,z),y)" if "x∈A" "y∈M" for x y
using that sats'[of _ x y] sats_Collect_fm[of M "λb.?Q(x,b)"] transitivity[of x A]
by simp
from ‹pred(arity(?G))∈nat› ‹?G∈_›
have "Collect_fm(7,?G,6) ∈ formula" "arity(Collect_fm(7,?G,6)) ≤ 8"
using union_abs2[OF ‹pred(arity(?G)) ≤ 8›] arity_Collect_fm union_abs2
by simp_all
then
have "arity(ren(Collect_fm(7,?G,6))`8`8`ren_G_fn) ≤ 8"
"ren(Collect_fm(7,?G,6))`8`8`ren_G_fn ∈ formula" (is "?Γ∈_")
using ren_tc[of "Collect_fm(7,?G,6)"] ren_G_thm(2) ren_G_fn_def arity_ren
by simp_all
from ‹arity(Collect_fm(7,?G,6))≤_› ‹Collect_fm(7,?G,6)∈_› types
have "(M,[x,y,P, leq, one, f_dot,p,B] ⊨?Γ) ⟷
M,[x,P, leq, one, f_dot,p,y,B] ⊨ Collect_fm(7,?G,6)" if "x∈A" "y∈M" for x y
using sats_iff_sats_ren[of "Collect_fm(7,?G,6)" 8 8 _ M "[x,y,P, leq, one, f_dot,p,B]"]
ren_G_thm(1)[where A=M] ren_G_thm(2) transitivity[of x A] that ren_G_fn_def
by simp
then
have "(M,[x,y,P, leq, one, f_dot,p,B] ⊨ren(Collect_fm(7,?G,6))`8`8`ren_G_fn) ⟷
y = {z∈B . ?Q(x,z)}" if "x∈A" "y∈M" for y x
using that iff_trans[OF _ sats_col]
Collect_abs types
by auto
with assms types ‹?Γ∈_› ‹arity(?Γ)≤_›
show ?thesis
using closed Lambda_in_M[where env="[P, leq, one, f_dot,p,B]" and φ="?Γ"]
by simp
qed
lemma ccc_fun_approximation_lemma :
notes le_trans[trans]
assumes "ccc⇗M⇖(P,leq)" "A∈M" "B∈M" "f∈M[G]" "f : A → B"
shows
"∃F∈M. F : A → Pow(B) ∧ (∀a∈A. f`a ∈ F`a ∧ |F`a|⇗M⇖ ≤ ω)"
proof -
from ‹f∈M[G]›
obtain f_dot where "f = val(P,G,f_dot)" "f_dot∈M" using GenExtD by force
with assms
obtain p where "p ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]" "p∈G" "p∈M"
using transitivity[OF M_genericD P_in_M]
generic truth_lemma[of "⋅0:1→2⋅" G "[f_dot, A⇧v, B⇧v]"]
by (auto simp add:ord_simp_union arity_typed_function_fm
typed_function_type)
define F where "F≡λa∈A. {b∈B. ∃q∈P. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}"
from assms ‹f_dot∈_› ‹p∈M›
have "F ∈ M"
unfolding F_def using ccc_fun_closed_lemma by simp
moreover
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 ‹f∈M[G]› ‹A∈M›
moreover from calculation
have "M[G], [f, a, f`a] ⊨ ⋅0`1 is 2⋅"
by (auto dest:transM)
moreover
note ‹B∈M› ‹f = val(P,G,f_dot)›
moreover from calculation
have "a∈M" "val(P,G, f_dot)`a∈M"
by (auto dest:transM)
moreover
note ‹f_dot∈M› ‹p∈G›
ultimately
obtain q where "q ≼ p" "q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, (f`a)⇧v]" "q∈G"
using forces_below_filter[of "⋅0`1 is 2⋅" "[f_dot, a⇧v, (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 ∈ {b∈B . ∃q∈P. q ≼ p ∧ q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v]}"
by blast
with ‹a∈A›
show ?thesis unfolding F_def by simp
qed
moreover
have "|F`a|⇗M⇖ ≤ ω" if "a ∈ A" for a
proof -
let ?Q="λb. {q∈P. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}"
from ‹F ∈ M› ‹a∈A› ‹A∈M›
have "F`a ∈ M" "a∈M"
using transitivity[OF _ ‹A∈M›] by simp_all
moreover
have 2:"⋀x. x∈F`a ⟹ x∈M"
using transitivity[OF _ ‹F`a∈M›] by simp
moreover
have 3:"⋀x. x∈F`a ⟹ (##M)(?Q(x))"
using ccc_fun_closed_lemma_aux[OF ‹f_dot∈M› ‹p∈M› ‹a∈M› 2] transitivity[of _ "F`a"]
by simp
moreover
have 4:"lam_replacement(##M,λb. {q ∈ P . q ≼ p ∧ (M, [q, P, leq, one, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))})"
using ccc_fun_closed_lemma_aux2[OF _ ‹f_dot∈M› ‹p∈M› ‹a∈M›]
lam_replacement_iff_lam_closed[THEN iffD2]
ccc_fun_closed_lemma_aux[OF ‹f_dot∈M› ‹p∈M› ‹a∈M›]
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_dot∈M› ‹p∈M› ‹a∈M›]
lam_replacement_product
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 "λ_ . P"
using P_in_M lam_replacement_imp_strong_replacement[OF
lam_replacement_Sigfun[OF lam_replacement_constant]]
Pi_replacement1 transM[of _ "F`a"]
by unfold_locales simp_all
from ‹p ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]› ‹a∈A›
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)" "q∈M" using AC_Pi_rel by auto
moreover
note ‹F`a ∈ M›
moreover from calculation
have "q : F`a →⇗M⇖ P"
using Pi_rel_weaken_type def_function_space_rel by auto
moreover from calculation
have "q : F`a → range(q)" "q : F`a → P" "q : F`a →⇗M⇖ range(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 b c
proof -
from ‹b ∈ F`a› ‹c ∈ F`a› ‹q ∈ Pi⇗M⇖(F`a,?Q)› ‹q∈M›
have "q`b ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v]"
"q`c ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, c⇧v]"
using mem_Pi_rel_abs[of q] apply_type[of _ _ ?Q]
by simp_all
with ‹b ≠ c› ‹q : F`a → P› ‹a∈A› ‹b∈_› ‹c∈_›
‹A∈M› ‹f_dot∈M› ‹F`a∈M›
show ?thesis
using forces_neq_apply_imp_incompatible
transitivity[of _ A] transitivity[of _ "F`a"]
by auto
qed
moreover from calculation
have "antichain(range(q))"
using Pi_range_eq[of _ _ "λ_ . P"]
unfolding antichain_def by auto
moreover from this and ‹q∈M›
have "antichain_r'(range(q))"
by (simp add:absolut)
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› ‹q∈M›
have "|F`a|⇗M⇖ ≤ |range(q)|⇗M⇖"
using def_lepoll_rel
by (rule_tac lepoll_rel_imp_cardinal_rel_le) auto
also from ‹antichain_r'(range(q))› ‹ccc⇗M⇖(P,leq)› ‹q∈M›
have "|range(q)|⇗M⇖ ≤ ω"
using def_ccc_rel by simp
finally
show ?thesis .
qed
moreover
have "F : A → Pow(B)"
unfolding F_def by (rule_tac lam_type) blast
ultimately
show ?thesis by auto
qed
end
end
end