Theory Absolute_Versions

section‹From $M$ to $\calV$›

theory Absolute_Versions
  imports
    CH
    ZF.Cardinal_AC
begin

hide_const (open) Order.pred

subsection‹Locales of a class term‹M› hold in term‹𝒱››

interpretation V: M_trivial 𝒱
  using Union_ax_absolute upair_ax_absolute
  by unfold_locales auto

lemmas bad_simps = V.nonempty V.Forall_in_M_iff V.Inl_in_M_iff V.Inr_in_M_iff
  V.succ_in_M_iff V.singleton_in_M_iff V.Equal_in_M_iff V.Member_in_M_iff V.Nand_in_M_iff
  V.Cons_in_M_iff V.pair_in_M_iff V.upair_in_M_iff

lemmas bad_M_trivial_simps[simp del] = V.Forall_in_M_iff V.Equal_in_M_iff
  V.nonempty

lemmas bad_M_trivial_rules[rule del] =  V.pair_in_MI V.singleton_in_MI V.pair_in_MD V.nat_into_M
  V.depth_closed V.length_closed V.nat_case_closed V.separation_closed
  V.Un_closed V.strong_replacement_closed V.nonempty

interpretation V:M_basic 𝒱
  using power_ax_absolute separation_absolute replacement_absolute
  by unfold_locales auto

interpretation V:M_eclose 𝒱
  by unfold_locales (auto intro:separation_absolute replacement_absolute
      simp:iterates_replacement_def wfrec_replacement_def)

lemmas bad_M_basic_rules[simp del, rule del] =
  V.cartprod_closed V.finite_funspace_closed V.converse_closed
  V.list_case'_closed V.pred_closed

interpretation V:M_cardinal_arith 𝒱
  by unfold_locales (auto intro:separation_absolute replacement_absolute
      simp add:iterates_replacement_def wfrec_replacement_def lam_replacement_def)

lemmas bad_M_cardinals_rules[simp del, rule del] =
  V.iterates_closed V.M_nat V.trancl_closed V.rvimage_closed

interpretation V:M_cardinal_arith_jump 𝒱
  by unfold_locales (auto intro:separation_absolute replacement_absolute
      simp:wfrec_replacement_def)

lemma choice_ax_Universe: "choice_ax(𝒱)"
proof -
  {
    fix x
    obtain f where "f ∈ surj(|x|,x)"
      using cardinal_eqpoll unfolding eqpoll_def bij_def by fast
    moreover
    have "Ord(|x|)" by simp
    ultimately
    have "∃a. Ord(a) ∧ (∃f. f ∈ surj(a,x))"
      by fast
  }
  then
  show ?thesis  unfolding choice_ax_def rall_def rex_def
    by simp
qed

interpretation V:M_master 𝒱
  using choice_ax_Universe
  by unfold_locales (auto intro:separation_absolute replacement_absolute
      simp:lam_replacement_def transrec_replacement_def wfrec_replacement_def
      is_wfrec_def M_is_recfun_def)

named_theorems V_simps

― ‹To work systematically, ASCII versions of "\_absolute" theorems as
    those below are preferable.›
lemma eqpoll_rel_absolute[V_simps]: "x ≈⇗𝒱⇖ y ⟷ x ≈ y"
  unfolding eqpoll_def using V.def_eqpoll_rel by auto

lemma cardinal_rel_absolute[V_simps]: "|x|⇗𝒱⇖ = |x|"
  unfolding cardinal_def cardinal_rel_def by (simp add:V_simps)

lemma Card_rel_absolute[V_simps]:"Card⇗𝒱⇖(a) ⟷ Card(a)"
  unfolding Card_rel_def Card_def by (simp only:V_simps)

lemma csucc_rel_absolute[V_simps]:"(a+)⇗𝒱⇖ = a+"
  unfolding csucc_rel_def csucc_def by (simp add:V_simps)

lemma function_space_rel_absolute[V_simps]:"x →⇗𝒱⇖ y = x → y"
  using V.function_space_rel_char by (simp add:V_simps)

lemma cexp_rel_absolute[V_simps]:"x⇗↑y,𝒱⇖ = x⇗↑y⇖"
  unfolding cexp_rel_def cexp_def by (simp only:V_simps)

lemma HAleph_rel_absolute[V_simps]:"HAleph_rel(𝒱,a,b) = HAleph(a,b)"
  unfolding HAleph_rel_def HAleph_def by (auto simp add:V_simps)

lemma Aleph_rel_absolute[V_simps]: "Ord(x) ⟹ ℵ⇘x⇙⇗𝒱⇖ = ℵ⇘x⇙"
proof -
  assume "Ord(x)"
  have "ℵ⇘x⇙⇗𝒱⇖ = transrec(x, λa b. HAleph_rel(𝒱,a,b))"
    unfolding Aleph_rel_def by simp
  also
  have "… = transrec(x, HAleph)"
    by (simp only:V_simps)
  also from ‹Ord(x)›
  have "… = ℵ⇘x⇙"
    using Aleph'_eq_Aleph unfolding Aleph'_def by simp
  finally
  show ?thesis .
qed

text‹Example of absolute lemmas obtained from the relative versions.
    Note the ∗‹only› declarations›
lemma Ord_cardinal_idem': "Ord(A) ⟹ ||A|| = |A|"
  using V.Ord_cardinal_rel_idem by (simp only:V_simps)

lemma Aleph_succ': "Ord(α) ⟹ ℵ⇘succ(α)⇙ = ℵ⇘α⇙+"
  using V.Aleph_rel_succ by (simp only:V_simps)

text‹These two results are new, first obtained in relative form
    (not ported).›
lemma csucc_cardinal:
  assumes "Ord(κ)" shows "|κ|+ = κ+"
  using assms V.csucc_rel_cardinal_rel by (simp only:V_simps)

lemma csucc_le_mono:
  assumes "κ ≤ ν"  shows "κ+ ≤ ν+"
  using assms V.csucc_rel_le_mono by (simp only:V_simps)

text‹Example of transferring results from a transitive model to term‹𝒱››
lemma (in M_Perm) eqpoll_rel_transfer_absolute:
  assumes "M(A)" "M(B)" "A ≈⇗M⇖ B"
  shows "A ≈ B"
proof -
  interpret M_N_Perm M 𝒱
    by (unfold_locales, simp only:V_simps)
  from assms
  show ?thesis using eqpoll_rel_transfer
    by (simp only:V_simps)
qed

text‹The “relationalized” $\CH$ with respect to term‹𝒱› corresponds
    to the real $\CH$.›
lemma is_ContHyp_iff_CH: "is_ContHyp(𝒱) ⟷ ContHyp"
  using V.is_ContHyp_iff
  by (auto simp add:ContHyp_rel_def ContHyp_def V_simps)

end