Theory Cardinal_Preservation

sectionPreservation 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 φ="⋅¬0`1 is 2" ]
    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
  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 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.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.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

subsectionPreservation 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
      by (simp_all add:arity)
    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
      by (simp_all add:arity)
    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
      by (simp_all add:arity)
    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