Theory Not_CH

theory Not_CH
  imports
    Cardinal_Preservation
begin

definition
  Add_subs :: "[i,i] ⇒ i" where
  "Add_subs(κ,α) ≡ Fn(ω,κ×α,2)"

locale M_master= M_cohen +
  assumes
  domain_separation: "M(x) ⟹ separation(M, λz. x ∈ domain(z))"
  and
  inj_dense_separation: "M(x) ⟹ M(w) ⟹
    separation(M, λz. ∃n∈ω.    ⟨⟨w, n⟩, 1⟩ ∈ z ∧ ⟨⟨x, n⟩, 0⟩ ∈ z)"
  and
  lam_apply_replacement: "M(A) ⟹ M(f) ⟹
      strong_replacement(M, λx y. y = ⟨x, λn∈A. f ` ⟨x, n⟩⟩)"
  and
  UN_lepoll_assumptions:
  "M(A) ⟹ M(b) ⟹ M(f) ⟹ M(A') ⟹ separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x∈if_range_F_else_F((`)(A), b, f, i)⟩)"

begin

lemma (in M_FiniteFun) Fn_nat_closed :
  assumes "M(A)" "M(B)" shows "M(Fn(ω,A,B))"
  using assms Fn_nat_eq_FiniteFun
  by simp

lemma Aleph_rel2_closed [intro,simp]: "M(ℵ⇘₂⇙⇗^M⇖)"
  using nat_into_M[of 2] nat_into_Ord by simp

end (* M_master *)

locale M_master_sub= M_master + N:M_master N for N +
  assumes
    M_imp_N: "M(x) ⟹ N(x)" and
    Ord_iff: "Ord(x) ⟹ M(x) ⟷ N(x)"

sublocale M_master_sub ⊆ M_N_Perm
  using M_imp_N by unfold_locales

context M_master_sub
begin

lemma cardinal_rel_le_cardinal_rel : "M(X) ⟹ |X|⇗^N⇖ ≤ |X|⇗^M⇖"
  using M_imp_N N.lepoll_rel_cardinal_rel_le[OF lepoll_rel_transfer Card_rel_is_Ord]
      cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym, THEN eqpoll_rel_imp_lepoll_rel]
  by simp

lemma Aleph_rel_sub_closed : "Ord(α) ⟹ M(α) ⟹ N(ℵ⇘_α⇙⇗^M⇖)"
  using Aleph_rel2_closed Ord_iff[THEN iffD1,
      OF Card_rel_Aleph_rel[THEN Card_rel_is_Ord]]
  by simp

lemma Card_rel_imp_Card_rel : "M(κ) ⟹ Card⇗^N⇖(κ) ⟹ Card⇗^M⇖(κ)"
  using N.Card_rel_is_Ord[of κ] M_imp_N Ord_cardinal_rel_le[of κ]
    cardinal_rel_le_cardinal_rel[of κ] le_anti_sym
  unfolding Card_rel_def by auto

lemma csucc_rel_le_csucc_rel :
  assumes "Ord(κ)" "M(κ)"
  shows "(κ⇧⁺)⇗^M⇖ ≤ (κ⇧⁺)⇗^N⇖"
proof -
  note assms
  moreover from this
  have "N(L) ∧ Card⇗^N⇖(L) ∧ κ < L ⟹ M(L) ∧ Card⇗^M⇖(L) ∧ κ < L"
    (is "?P(L) ⟹ ?Q(L)") for L
    using M_imp_N Ord_iff[THEN iffD2, of L] N.Card_rel_is_Ord lt_Ord
      Card_rel_imp_Card_rel by auto
  moreover from assms
  have "N((κ⇧⁺)⇗^N⇖)" "Card⇗^N⇖((κ⇧⁺)⇗^N⇖)" "κ < (κ⇧⁺)⇗^N⇖"
    using N.lt_csucc_rel[of κ] N.Card_rel_csucc_rel[of κ] M_imp_N by simp_all
  ultimately
  show ?thesis
    using M_imp_N Least_antitone[of _ ?P ?Q] unfolding csucc_rel_def by blast
qed

lemma Aleph_rel_le_Aleph_rel : "Ord(α) ⟹ M(α) ⟹ ℵ⇘_α⇙⇗^M⇖ ≤ ℵ⇘_α⇙⇗^N⇖"
proof (induct rule:trans_induct3)
  case 0
  then
  show ?case
    using Aleph_rel_zero N.Aleph_rel_zero by simp
next
  case (succ x)
  then
  have "ℵ⇘_x⇙⇗^M⇖ ≤ ℵ⇘_x⇙⇗^N⇖" "Ord(x)" "M(x)" by simp_all
  moreover from this
  have "(ℵ⇘_x⇙⇗^M⇖⇧⁺)⇗^M⇖ ≤ (ℵ⇘_x⇙⇗^N⇖⇧⁺)⇗^M⇖"
    using M_imp_N Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
    by (intro csucc_rel_le_mono) simp_all
  moreover from calculation
  have "(ℵ⇘_x⇙⇗^N⇖⇧⁺)⇗^M⇖ ≤ (ℵ⇘_x⇙⇗^N⇖⇧⁺)⇗^N⇖"
    using M_imp_N N.Card_rel_is_Ord Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
    by (intro csucc_rel_le_csucc_rel) auto
  ultimately
  show ?case
    using M_imp_N Aleph_rel_succ N.Aleph_rel_succ csucc_rel_le_csucc_rel
      le_trans by auto
next
  case (limit x)
  then
  show ?case
    using M_imp_N Aleph_rel_limit N.Aleph_rel_limit
     by simp (blast dest: transM intro!:le_implies_UN_le_UN)
qed

end (* M_master_sub *)

lemmas (in M_ZFC_trans) sep_instances =
 separation_toplevel1_body separation_toplevel2_body separation_toplevel3_body
 separation_toplevel4_body separation_toplevel5_body separation_toplevel6_body
 separation_toplevel7_body separation_toplevel8_body separation_toplevel9_body
 separation_toplevel10_body separation_toplevel11_body separation_Ord
 separation_toplevel12_body separation_insnd_ballPair
 separation_restrict_eq_dom_eq separation_restrict_eq_dom_eq_pair
 separation_ifrangeF_body separation_ifrangeF_body2 separation_ifrangeF_body3
 separation_ifrangeF_body4 separation_ifrangeF_body5 separation_ifrangeF_body6
 separation_ifrangeF_body7

(* FIXME: the second instance has been proved in Lambda Replacement, it shouldn't be here. *)
lemmas (in M_ZF_trans) repl_instances = lam_replacement_inj_rel
  lam_replacement_cardinal[unfolded lam_replacement_def] replacement_trans_apply_image
  replacement_abs_apply_pair

sublocale M_ZFC_trans ⊆ M_master "##M"
  by unfold_locales (simp_all add:repl_instances sep_instances del:setclass_iff)

context M_ctm_AC
begin

― ‹FIXME: using notation as if \<^term>‹Add_subs› were used›
lemma ccc_Add_subs_Aleph_2 : "ccc⇗^M⇖(Fn(ω,ℵ⇘₂⇙⇗^M⇖ × ω,2),Fnle(ω,ℵ⇘₂⇙⇗^M⇖ × ω,2))"
proof -
  interpret M_add_reals "##M" "ℵ⇘₂⇙⇗^M⇖ × ω"
    by unfold_locales blast
  show ?thesis
    using ccc_rel_Fn_nat by fast
qed

end (* M_ctm *)

sublocale G_generic_AC ⊆ M_master_sub "##M" "##(M[G])"
  using M_subset_MG[OF one_in_G] generic Ord_MG_iff
  by unfold_locales auto

lemma (in M_trans) mem_F_bound4 :
  fixes F A
  defines "F ≡ (`)"
  shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ domain(A))"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def)

lemma (in M_trans) mem_F_bound5 :
  fixes F A
  defines "F ≡ λ_ x. A`x "
  shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ domain(A))"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)

context G_generic_AC begin

context
  includes G_generic_lemmas
begin

lemma G_in_MG : "G ∈ M[G]"
  using G_in_Gen_Ext[ OF _ one_in_G, OF _ generic]
  by blast

lemma ccc_preserves_Aleph_succ :
  assumes "ccc⇗^M⇖(P,leq)" "Ord(z)" "z ∈ M"
  shows "Card⇗^M[G]⇖(ℵ⇘_succ(z)⇙⇗^M⇖)"
proof (rule ccontr)
  assume "¬ Card⇗^M[G]⇖(ℵ⇘_succ(z)⇙⇗^M⇖)"
  moreover
  note ‹z ∈ M›
  moreover from this and ‹Ord(z)›
  have "Ord(ℵ⇘_succ(z)⇙⇗^M⇖)"
    using Card_rel_Aleph_rel[of "succ(z)", THEN Card_rel_is_Ord]
    by fastforce
  ultimately
  obtain α f where "α < ℵ⇘_succ(z)⇙⇗^M⇖" "f ∈ surj⇗^M[G]⇖(α, ℵ⇘_succ(z)⇙⇗^M⇖)"
    using ext.lt_surj_rel_empty_imp_Card_rel M_subset_MG[OF one_in_G, OF generic]
      Aleph_rel_closed[of "succ(z)"] ‹Ord(z)› by simp blast
  moreover from this and ‹z∈M› ‹Ord(z)›
  have "α ∈ M" "f ∈ M[G]"
    using Aleph_rel_closed[of "succ(z)"] ext.trans_surj_rel_closed
    by (auto dest:transM ext.transM dest!:ltD)
  moreover
  note ‹ccc⇗^M⇖(P,leq)› ‹z∈M›
  ultimately
  obtain F where "F:α→Pow(ℵ⇘_succ(z)⇙⇗^M⇖)" "∀β∈α. f`β ∈ F`β" "∀β∈α. |F`β|⇗^M⇖ ≤ ω"
    "F ∈ M"
    using ccc_fun_approximation_lemma[of α "ℵ⇘_succ(z)⇙⇗^M⇖" f]
      ext.mem_surj_abs[of f α "ℵ⇘_succ(z)⇙⇗^M⇖"] ‹Ord(z)›
      Aleph_rel_closed[of "succ(z)"] surj_is_fun[of f α "ℵ⇘_succ(z)⇙⇗^M⇖"] by auto
  then
  have "β ∈ α ⟹ |F`β|⇗^M⇖ ≤ ℵ⇘₀⇙⇗^M⇖" for β
    using Aleph_rel_zero by simp
  interpret M_replacement_lepoll "##M" "(`)"
    using UN_lepoll_assumptions lam_replacement_apply lam_replacement_inj_rel
      mem_F_bound4 apply_0
    unfolding lepoll_assumptions_defs
  proof (unfold_locales, 
      rule_tac [3] lam_Least_assumption_general[where U=domain, OF _ mem_F_bound4], simp_all) 
    fix A i x
    assume "A ∈ M" "x ∈ M" "x ∈ A ` i"
    then
    show "i ∈ M"
      using apply_0[of i A] transM[of _ "domain(A)", simplified]
      by force
  qed
  from ‹α ∈ M› ‹F:α→Pow(ℵ⇘_succ(z)⇙⇗^M⇖)› ‹F∈M›
  interpret M_cardinal_UN_lepoll "##M" "λβ. F`β" α
    using Aleph_rel_closed[of 0] UN_lepoll_assumptions lepoll_assumptions
      lam_replacement_apply lam_replacement_inj_rel
  proof (unfold_locales, auto dest:transM simp del:if_range_F_else_F_def)
    show "w ∈ F ` x ⟹ x ∈ M" for w x
    proof -
      fix w x
      assume "w ∈ F`x"
      then
      have "x ∈ domain(F)"
        using apply_0 by auto
      with ‹F:α→Pow(ℵ⇘_succ(z)⇙⇗^M⇖)›
      have "x ∈ α"
        using domain_of_fun by simp
      with ‹α ∈ M›
      show "x ∈ M" by (auto dest:transM)
    qed
   show "w ∈ F ` x ⟹ x ∈ M" for w x ― ‹FIXME: why two times?›
    proof -
      fix w x
      assume "w ∈ F`x"
      then
      have "x ∈ domain(F)"
        using apply_0 by auto
      with ‹F:α→Pow(ℵ⇘_succ(z)⇙⇗^M⇖)›
      have "x ∈ α"
        using domain_of_fun by simp
      with ‹α ∈ M›
      show "x ∈ M" by (auto dest:transM)
    qed
  next
    fix f b
    assume "b∈M" "f∈M"
    with ‹F∈M›
    show "lam_replacement(##M, λx. μ i. x ∈ if_range_F_else_F((`)(F), b, f, i))"
      using UN_lepoll_assumptions mem_F_bound5
      by (rule_tac lam_Least_assumption_general[where U="domain", OF _ mem_F_bound5])
        simp_all
  qed
  from ‹α < ℵ⇘_succ(z)⇙⇗^M⇖› ‹α ∈ M› assms
  have "α ≲⇗^M⇖ ℵ⇘_z⇙⇗^M⇖"
    using
      Aleph_rel_zero
      cardinal_rel_lt_csucc_rel_iff[of "ℵ⇘_z⇙⇗^M⇖" α]
      le_Card_rel_iff[of "ℵ⇘_z⇙⇗^M⇖" α]
      Aleph_rel_succ[of z] Card_rel_lt_iff[of α "ℵ⇘_succ(z)⇙⇗^M⇖"]
      lt_Ord[of α "ℵ⇘_succ(z)⇙⇗^M⇖"]
      csucc_rel_closed[of "ℵ⇘_z⇙⇗^M⇖"] Card_rel_csucc_rel[of "ℵ⇘_z⇙⇗^M⇖"]
      Aleph_rel_closed[of z]
      Card_rel_Aleph_rel[THEN Card_rel_is_Ord, OF _ _ Aleph_rel_closed]
    by simp
  with ‹α < ℵ⇘_succ(z)⇙⇗^M⇖› ‹∀β∈α. |F`β|⇗^M⇖ ≤ ω› ‹α ∈ M› assms
  have "|⋃β∈α. F`β|⇗^M⇖ ≤ ℵ⇘_z⇙⇗^M⇖"
    using InfCard_rel_Aleph_rel[of z] Aleph_rel_zero
      subset_imp_lepoll_rel[THEN lepoll_rel_imp_cardinal_rel_le,
        of "⋃β∈α. F`β" "ℵ⇘_z⇙⇗^M⇖"]
      Aleph_rel_closed[of z] Aleph_rel_succ
      Aleph_rel_increasing[THEN leI, THEN [2] le_trans, of _ 0 z]
      Ord_0_lt_iff[THEN iffD1, of z]
    by (cases "0<z"; rule_tac leqpoll_rel_imp_cardinal_rel_UN_le) (auto, force)
  moreover
  note ‹z∈M› ‹Ord(z)›
  moreover from ‹∀β∈α. f`β ∈ F`β› ‹f ∈ surj⇗^M[G]⇖(α, ℵ⇘_succ(z)⇙⇗^M⇖)›
    ‹α ∈ M› ‹f ∈ M[G]› and this
  have "ℵ⇘_succ(z)⇙⇗^M⇖ ⊆ (⋃β∈α. F`β)"
    using Aleph_rel_closed[of "succ(z)"] ext.mem_surj_abs
    by (force simp add:surj_def)
  moreover from ‹F ∈ M› ‹α ∈ M›
  have "(⋃x∈α. F ` x) ∈ M"
    using j.B_replacement― ‹NOTE: it didn't require @{thm j.UN_closed} before!›
    by (intro Union_closed[simplified] RepFun_closed[simplified])
      (auto dest:transM)
  ultimately
  have "ℵ⇘_succ(z)⇙⇗^M⇖ ≤ ℵ⇘_z⇙⇗^M⇖"
    using subset_imp_le_cardinal_rel[of "ℵ⇘_succ(z)⇙⇗^M⇖" "⋃β∈α. F`β"]
      Aleph_rel_closed[of "succ(z)"] le_trans
    by auto
  with assms
  show "False"
    using Aleph_rel_increasing not_le_iff_lt[of "ℵ⇘_succ(z)⇙⇗^M⇖" "ℵ⇘_z⇙⇗^M⇖"]
      Card_rel_Aleph_rel[THEN Card_rel_is_Ord, OF _ _ Aleph_rel_closed]
    by auto
qed

end (* G_generic_lemmas *)

end (* G_generic *)

context M_ctm
begin

abbreviation
  Add :: "i" where
  "Add ≡ Fn(ω, ℵ⇘₂⇙⇗^M⇖ × ω, 2)"

end (* M_ctm *)

locale add_generic= G_generic_AC "Fn(ω, ℵ⇘₂⇙⇗^##M⇖ × ω, 2)" "Fnle(ω, ℵ⇘₂⇙⇗^##M⇖ × ω, 2)" 0

sublocale add_generic ⊆ cohen_data ω "ℵ⇘₂⇙⇗^M⇖ × ω" 2 by unfold_locales auto

context add_generic
begin

notation Leq (infixl "≼" 50)
notation Incompatible (infixl "⊥" 50)
notation GenExt_at_P ("_[_]" [71,1])

lemma Add_subs_preserves_Aleph_succ : "Ord(z) ⟹ z∈M ⟹ Card⇗^M[G]⇖(ℵ⇘_succ(z)⇙⇗^M⇖)"
  using ccc_preserves_Aleph_succ ccc_Add_subs_Aleph_2
  by auto

lemma Aleph_rel_nats_MG_eq_Aleph_rel_nats_M :
  includes G_generic_lemmas
  assumes "z ∈ ω"
  shows "ℵ⇘_z⇙⇗^M[G]⇖ = ℵ⇘_z⇙⇗^M⇖"
  using assms
proof (induct)
  case 0
  have "ℵ⇘₀⇙⇗^M[G]⇖ = ω"
    using ext.Aleph_rel_zero .
  also
  have "ω = ℵ⇘₀⇙⇗^M⇖"
    using Aleph_rel_zero by simp
  finally
  show ?case .
next
  case (succ z)
  then
  have "ℵ⇘_succ(z)⇙⇗^M⇖ ≤ ℵ⇘_succ(z)⇙⇗^M[G]⇖"
    using Aleph_rel_le_Aleph_rel nat_into_M by simp
  moreover from ‹z ∈ ω›
  have "ℵ⇘_z⇙⇗^M⇖ ∈ M[G]" "ℵ⇘_succ(z)⇙⇗^M⇖ ∈ M[G]"
    using Aleph_rel_closed nat_into_M by simp_all
  moreover from this and ‹ℵ⇘_z⇙⇗^M[G]⇖ = ℵ⇘_z⇙⇗^M⇖› ‹z ∈ ω›
  have "ℵ⇘_succ(z)⇙⇗^M[G]⇖ ≤ ℵ⇘_succ(z)⇙⇗^M⇖"
    using ext.Aleph_rel_succ nat_into_M
      Add_subs_preserves_Aleph_succ[THEN ext.csucc_rel_le, of z]
      Aleph_rel_increasing[of z "succ(z)"]
    by simp
  ultimately
  show ?case using le_anti_sym by blast
qed

abbreviation
  f_G :: "i" (‹f⇘_G⇙›) where
  "f⇘_G⇙ ≡ ⋃G"

abbreviation
  dom_dense :: "i⇒i" where
  "dom_dense(x) ≡ { p∈Add . x ∈ domain(p) }"

― ‹FIXME write general versions of this for \<^term>‹Fn(ω,I,J)›
    in a context with a generic filter for it›
lemma dense_dom_dense : "x ∈ ℵ⇘₂⇙⇗^M⇖ × ω ⟹ dense(dom_dense(x))"
proof
  fix p
  assume "x ∈ ℵ⇘₂⇙⇗^M⇖ × ω" "p ∈ Add"
  show "∃d∈dom_dense(x). d ≼ p"
  proof (cases "x ∈ domain(p)")
    case True
    with ‹x ∈ ℵ⇘₂⇙⇗^M⇖ × ω› ‹p ∈ Add›
    show ?thesis using refl_leq by auto
  next
    case False
    note ‹p ∈ Add›
    moreover from this and False and ‹x ∈ ℵ⇘₂⇙⇗^M⇖ × ω›
    have "cons(⟨x,0⟩, p) ∈ Add"
      using FiniteFun.consI[of x "ℵ⇘₂⇙⇗^M⇖ × ω" 0 2 p]
        Fn_nat_eq_FiniteFun by auto
    moreover from ‹p ∈ Add›
    have "x∈domain(cons(⟨x,0⟩, p))" by simp
    ultimately
    show ?thesis
      by (fastforce del:FnD)
  qed
qed

(*
NOTE Class model version?
lemma dom_dense_closed[intro,simp]: "x ∈ ℵ⇘₂⇙⇗^M⇖ × ω ⟹ M(dom_dense(x))" *)
lemma dom_dense_closed [intro,simp]: "x ∈ ℵ⇘₂⇙⇗^M⇖ × ω ⟹ dom_dense(x) ∈ M"
  using Fn_nat_closed Aleph_rel2_closed domain_separation[of x] nat_into_M
  by (rule_tac separation_closed[simplified], blast dest:transM) simp

lemma domain_f_G : assumes "x ∈ ℵ⇘₂⇙⇗^M⇖" "y ∈ ω"
  shows "⟨x, y⟩ ∈ domain(f⇘_G⇙)"
proof -
  from assms
  have "dense(dom_dense(⟨x, y⟩))" using dense_dom_dense by simp
  with assms
  obtain p where "p∈dom_dense(⟨x, y⟩)" "p∈G"
    using generic[THEN M_generic_denseD, of "dom_dense(⟨x, y⟩)"]
    by auto
  then
  show "⟨x, y⟩ ∈ domain(f⇘_G⇙)" by blast
qed

― ‹MOVE THIS to 🗏‹Cohen_Posets.thy››
lemma Fn_nat_subset_Pow : "Fn(ω,I,J) ⊆ Pow(I×J)"
  using subset_trans[OF FiniteFun.dom_subset Fin.dom_subset]
    Fn_nat_eq_FiniteFun by simp

lemma f_G_funtype :
  includes G_generic_lemmas
  shows "f⇘_G⇙ : ℵ⇘₂⇙⇗^M⇖ × ω → 2"
  using generic domain_f_G
  unfolding Pi_def
proof (auto)
  show "x ∈ B ⟹ B ∈ G ⟹ x ∈ (ℵ⇘₂⇙⇗^M⇖ × ω) × 2" for B x
    using Fn_nat_subset_Pow by blast
  show "function(f⇘_G⇙)"
    using Un_filter_is_function generic
    unfolding M_generic_def by fast
qed

abbreviation
  inj_dense :: "i⇒i⇒i" where
  "inj_dense(w,x) ≡
    { p∈Add . (∃n∈ω. <<w,n>,1> ∈ p ∧ <<x,n>,0> ∈ p) }"

― ‹FIXME write general versions of this for \<^term>‹Fn(ω,I,J)›
    in a context with a generic filter for it›
lemma dense_inj_dense :
  assumes "w ∈ ℵ⇘₂⇙⇗^M⇖" "x ∈ ℵ⇘₂⇙⇗^M⇖" "w ≠ x"
  shows "dense(inj_dense(w,x))"
proof
  fix p
  assume "p ∈ Add"
  then
  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 ∈ Add›
      have False
        using Fn_nat_eq_FiniteFun FiniteFun.dom_subset[of "ℵ⇘₂⇙⇗^M⇖ × ω" 2]
          Fin_into_Finite by auto
    }
    with that― ‹the shape of the goal puts assumptions in this variable›
    show ?thesis by auto
  qed
  moreover
  note ‹p ∈ Add› assms
  moreover from calculation
  have "cons(⟨⟨x,n⟩,0⟩, p) ∈ Add"
    using FiniteFun.consI[of "⟨x,n⟩" "ℵ⇘₂⇙⇗^M⇖ × ω" 0 2 p]
      Fn_nat_eq_FiniteFun by auto
  ultimately
  have "cons(⟨⟨w,n⟩,1⟩, cons(⟨⟨x,n⟩,0⟩, p) ) ∈ Add"
    using FiniteFun.consI[of "⟨w,n⟩" "ℵ⇘₂⇙⇗^M⇖ × ω" 1 2 "cons(⟨⟨x,n⟩,0⟩, p)"]
      Fn_nat_eq_FiniteFun by auto
  with ‹n ∈ ω›
  show "∃d∈inj_dense(w,x). d ≼ p"
    using ‹p ∈ Add› by (intro bexI) auto
qed

lemma inj_dense_closed [intro,simp]:
  "w ∈ ℵ⇘₂⇙⇗^M⇖ ⟹ x ∈ ℵ⇘₂⇙⇗^M⇖ ⟹ inj_dense(w,x) ∈ M"
  using Fn_nat_closed Aleph_rel2_closed domain_separation[of x] nat_into_M
    inj_dense_separation transM[OF _ Aleph_rel2_closed]
  by (rule_tac separation_closed[simplified]; simp_all)

lemma Aleph_rel2_new_reals :
  assumes "w ∈ ℵ⇘₂⇙⇗^M⇖" "x ∈ ℵ⇘₂⇙⇗^M⇖" "w ≠ x"
  shows "(λn∈ω. f⇘_G⇙ ` ⟨w, n⟩) ≠ (λn∈ω. f⇘_G⇙ ` ⟨x, n⟩)"
proof -
  from assms
  have "dense(inj_dense(w,x))" using dense_inj_dense by simp
  with assms
  obtain p where "p∈inj_dense(w,x)" "p∈G"
    using generic[THEN M_generic_denseD, of "inj_dense(w,x)"]
    by blast
  then
  obtain n where "n ∈ ω" "⟨⟨w, n⟩, 1⟩ ∈ p" "⟨⟨x, n⟩, 0⟩ ∈ p"
    by blast
  moreover from this and ‹p∈G›
  have "⟨⟨w, n⟩, 1⟩ ∈ f⇘_G⇙" "⟨⟨x, n⟩, 0⟩ ∈ f⇘_G⇙" by auto
  moreover from calculation
  have "f⇘_G⇙ ` ⟨w, n⟩ = 1" "f⇘_G⇙ ` ⟨x, n⟩ = 0"
    using f_G_funtype apply_equality
    by auto
  ultimately
  have "(λn∈ω. f⇘_G⇙ ` ⟨w, n⟩) ` n ≠ (λn∈ω. f⇘_G⇙ ` ⟨x, n⟩) ` n"
    by simp
  then
  show ?thesis by fastforce
qed

definition
  h_G :: "i" (‹h⇘_G⇙›) where
  "h⇘_G⇙ ≡ λα∈ℵ⇘₂⇙⇗^M⇖. λn∈ω. f⇘_G⇙`<α,n>"

lemma h_G_in_MG [simp]:
  includes G_generic_lemmas
  shows "h⇘_G⇙ ∈ M[G]"
  using Aleph_rel2_closed
    ext.lam_apply_replacement ext.apply_replacement2
    ext.Union_closed[simplified, OF G_in_MG]
    ― ‹The "simplified" here is because of
        the \<^term>‹setclass› ocurrences›
    ext.nat_in_M Aleph_rel2_closed ext.nat_into_M
  unfolding h_G_def
  by (rule_tac ext.lam_closed[simplified] | auto dest:transM)+

lemma h_G_inj_Aleph_rel2_reals : "h⇘_G⇙ ∈ inj⇗^M[G]⇖(ℵ⇘₂⇙⇗^M⇖, ω →⇗^M[G]⇖ 2)"
  using Aleph_rel_sub_closed
proof (intro ext.mem_inj_abs[THEN iffD2])
  show "h⇘_G⇙ ∈ inj(ℵ⇘₂⇙⇗^M⇖, ω →⇗^M[G]⇖ 2)"
    unfolding inj_def
  proof (intro ballI CollectI impI)
    show "h⇘_G⇙ ∈ ℵ⇘₂⇙⇗^M⇖ → ω →⇗^M[G]⇖ 2"
      using f_G_funtype G_in_MG ext.nat_into_M unfolding h_G_def
      apply (intro lam_type ext.mem_function_space_rel_abs[THEN iffD2], simp_all)
      apply (rule_tac ext.lam_closed[simplified], simp_all)
       apply (rule ext.apply_replacement2)
         apply (auto dest:ext.transM[OF _ Aleph_rel_sub_closed])
      done
    fix w x
    assume "w ∈ ℵ⇘₂⇙⇗^M⇖" "x ∈ ℵ⇘₂⇙⇗^M⇖" "h⇘_G⇙ ` w = h⇘_G⇙ ` x"
    then
    show "w = x"
      unfolding h_G_def using Aleph_rel2_new_reals by auto
  qed
qed simp_all

lemma Aleph2_extension_le_continuum_rel :
  includes G_generic_lemmas
  shows "ℵ⇘₂⇙⇗^M[G]⇖ ≤ 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖"
proof -
  have "ℵ⇘₂⇙⇗^M⇖ ∈ M[G]" "Ord(ℵ⇘₂⇙⇗^M⇖)"
    using Card_rel_Aleph_rel[THEN Card_rel_is_Ord, of 2]
      Aleph_rel2_closed
    by auto
  moreover from this
  have "ℵ⇘₂⇙⇗^M⇖ ≲⇗^M[G]⇖ ω →⇗^M[G]⇖ 2"
    using ext.def_lepoll_rel[of "ℵ⇘₂⇙⇗^M⇖" "ω →⇗^M[G]⇖ 2",
        OF _ ext.function_space_rel_closed]
      h_G_inj_Aleph_rel2_reals h_G_in_MG ext.nat_into_M ext.M_nat
    by auto
  moreover from calculation
  have "ℵ⇘₂⇙⇗^M⇖ ≲⇗^M[G]⇖ |ω →⇗^M[G]⇖ 2|⇗^M[G]⇖"
    using ext.lepoll_rel_imp_lepoll_rel_cardinal_rel by simp
  ultimately
  have "|ℵ⇘₂⇙⇗^M⇖|⇗^M[G]⇖ ≤ 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖"
    using ext.lepoll_rel_imp_cardinal_rel_le[of "ℵ⇘₂⇙⇗^M⇖" "ω →⇗^M[G]⇖ 2",
        OF _ _ ext.function_space_rel_closed] ext.nat_into_M ext.M_nat
      ext.Aleph_rel_zero Aleph_rel_nats_MG_eq_Aleph_rel_nats_M
    unfolding cexp_rel_def by simp
  then
  show "ℵ⇘₂⇙⇗^M[G]⇖ ≤ 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖"
    using Aleph_rel_nats_MG_eq_Aleph_rel_nats_M
      ext.Card_rel_Aleph_rel[of 2, THEN ext.Card_rel_cardinal_rel_eq]
      ext.Aleph_rel2_closed
    by simp
qed

lemma Aleph_rel_lt_continuum_rel : "ℵ⇘₁⇙⇗^M[G]⇖ < 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖"
  using Aleph2_extension_le_continuum_rel
    ext.Aleph_rel_increasing[of 1 2] le_trans by auto

corollary not_CH: "ℵ⇘₁⇙⇗^M[G]⇖ ≠ 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖"
  using Aleph_rel_lt_continuum_rel by auto

end (* add_generic *)

definition
  ContHyp :: "o" where
  "ContHyp ≡ ℵ⇘₁⇙ = 2⇗^{↑ℵ⇘₀⇙}⇖"

relativize functional "ContHyp" "ContHyp_rel"
notation ContHyp_rel (‹CH⇗_⇖›)
relationalize "ContHyp_rel" "is_ContHyp"

context M_master
begin

is_iff_rel for "ContHyp"
  using is_cexp_iff is_Aleph_iff[of 0] is_Aleph_iff[of 1] unfolding is_ContHyp_def ContHyp_rel_def
  by auto (rule_tac x=0 in rexI, auto)

end (* M_master *)

synthesize "is_ContHyp" from_definition assuming "nonempty"
arity_theorem for "is_ContHyp_fm"

notation is_ContHyp_fm (‹⋅CH⋅›)

theorem ctm_of_not_CH :
  assumes
    "M ≈ ω" "Transset(M)" "M ⊨ ZFC"
  shows
    "∃N.
      M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅} ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))"
proof -
  from ‹M ⊨ ZFC›
  interpret M_ZFC M
    using M_ZFC_iff_M_satT
    by simp
  from ‹Transset(M)›
  interpret M_ZF_trans M
    using M_ZF_iff_M_satT
    by unfold_locales
  from ‹M ≈ ω›
  obtain enum where "enum ∈ bij(ω,M)"
    using eqpoll_sym unfolding eqpoll_def by blast
  then
  interpret M_ctm_AC M enum by unfold_locales
  interpret forcing_data "Fn(ω,ℵ⇘₂⇙⇗^M⇖ × ω,2)" "Fnle(ω,ℵ⇘₂⇙⇗^M⇖ × ω,2)" 0 M enum
  proof -
    interpret cohen_data ω "ℵ⇘₂⇙⇗^M⇖ × ω" 2 by unfold_locales auto
    show "forcing_data(Fn(ω, ℵ⇘₂⇙⇗^M⇖ × ω, 2), Fnle(ω, ℵ⇘₂⇙⇗^M⇖ × ω, 2), 0, M, enum)"
      using nat_into_M[of 2] M_nat
        Fn_nat_closed[OF cartprod_closed, OF Aleph_rel_closed, of 2 ω 2]
        Fnle_nat_closed[OF cartprod_closed, OF Aleph_rel_closed, of 2 ω 2]
      by (unfold_locales, simp_all)
  qed
  obtain G where "M_generic(G)"
    using generic_filter_existence[OF one_in_P]
    by auto
  moreover from this
  interpret add_generic M enum G by unfold_locales
  have "¬ (ℵ⇘₁⇙⇗^M[G]⇖ = 2⇗^{↑ℵ⇘₀⇙⇗^M[G]⇖,M[G]}⇖)"
    using not_CH .
  then
  have "M[G], [] ⊨ ⋅¬⋅CH⋅⋅"
    using ext.is_ContHyp_iff
    by (simp add:ContHyp_rel_def)
  then
  have "M[G] ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅}"
    using M_ZFC_iff_M_satT[of "M[G]"] ext.M_ZFC_axioms by auto
  moreover
  have "Transset(M[G])" using Transset_MG .
  moreover
  have "M ⊆ M[G]" using M_subset_MG[OF one_in_G] generic by simp
  ultimately
  show ?thesis
    using Ord_MG_iff MG_eqpoll_nat
    by (rule_tac x="M[G]" in exI, simp)
qed

end