# 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

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"

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```