# Theory Cardinal_AC_Relative

```section‹Relative, Cardinal Arithmetic Using AC›

theory Cardinal_AC_Relative
imports
CardinalArith_Relative

begin

locale M_AC =
fixes M
assumes
choice_ax: "choice_ax(M)"

locale M_cardinal_AC = M_cardinal_arith + M_AC +
assumes
lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
begin

lemma lam_replacement_minimum_vimage:
"M(f) ⟹ M(r) ⟹ lam_replacement(M, λx. minimum(r, f -`` {x}))"
using lam_replacement_minimum lam_replacement_vimage_sing_fun lam_replacement_constant
lam_replacement_identity lam_replacement_hcomp2[of _ _ minimum]
by simp

lemmas surj_imp_inj_replacement4 = lam_replacement_minimum_vimage[unfolded lam_replacement_def]

lemmas surj_imp_inj_replacement =
surj_imp_inj_replacement1 surj_imp_inj_replacement2 surj_imp_inj_replacement4
lam_replacement_vimage_sing_fun[THEN lam_replacement_imp_strong_replacement]

lemma well_ord_surj_imp_lepoll_rel:
assumes "well_ord(A,r)" "h ∈ surj(A,B)" and
types:"M(A)" "M(r)" "M(h)" "M(B)"
shows "B ≲⇗M⇖ A"
proof -
note eq=vimage_fun_sing[OF surj_is_fun[OF ‹h∈_›]]
from assms
have "(λb∈B. minimum(r, {a∈A. h`a=b})) ∈ inj(B,A)" (is "?f∈_")
using well_ord_surj_imp_inj_inverse assms(1,2) by simp
with assms
have "M(?f`b)" if "b∈B" for b
using apply_type[OF inj_is_fun[OF ‹?f∈_›]] that transM[OF _ ‹M(A)›] by simp
with assms
have "M(?f)"
using lam_closed surj_imp_inj_replacement4 eq by auto
with ‹?f∈_› assms
have "?f ∈ inj⇗M⇖(B,A)"
using mem_inj_abs by simp
with ‹M(?f)›
show ?thesis unfolding lepoll_rel_def by auto
qed

lemma surj_imp_well_ord_M:
assumes wos: "well_ord(A,r)" "h ∈ surj(A,B)"
and
types: "M(A)" "M(r)" "M(h)" "M(B)"
shows "∃s[M]. well_ord(B,s)"
using assms lepoll_rel_well_ord
well_ord_surj_imp_lepoll_rel by fast

lemma choice_ax_well_ord: "M(S) ⟹ ∃r[M]. well_ord(S,r)"
using choice_ax well_ord_Memrel[THEN surj_imp_well_ord_M]
unfolding choice_ax_def by auto

lemma Finite_cardinal_rel_Finite:
assumes "Finite(|i|⇗M⇖)" "M(i)"
shows "Finite(i)"
proof -
note assms
moreover from this
obtain r where "M(r)" "well_ord(i,r)"
using choice_ax_well_ord by auto
moreover from calculation
have "|i|⇗M⇖ ≈⇗M⇖ i"
using well_ord_cardinal_rel_eqpoll_rel
by auto
ultimately
show ?thesis
using eqpoll_rel_imp_Finite
by auto
qed

end ― ‹\<^locale>‹M_cardinal_AC››

locale M_Pi_assumptions_choice = M_Pi_assumptions + M_cardinal_AC +
assumes
B_replacement: "strong_replacement(M, λx y. y = B(x))"
and
― ‹The next one should be derivable from (some variant)
of B\_replacement. Proving both instances each time seems
inconvenient.›
minimum_replacement: "M(r) ⟹ strong_replacement(M, λx y. y = ⟨x, minimum(r, B(x))⟩)"
begin

lemma AC_M:
assumes "a ∈ A" "⋀x. x ∈ A ⟹ ∃y. y ∈ B(x)"
shows "∃z[M]. z ∈ Pi⇗M⇖(A, B)"
proof -
have "M(⋃x∈A. B(x))" using assms family_union_closed Pi_assumptions B_replacement by simp
then
obtain r where "well_ord(⋃x∈A. B(x),r)" "M(r)"
using choice_ax_well_ord by blast
let ?f="λx∈A. minimum(r,B(x))"
have "M(minimum(r, B(x)))" if "x∈A" for x
proof -
from ‹well_ord(_,r)› ‹x∈A›
have "well_ord(B(x),r)" using well_ord_subset UN_upper by simp
with assms ‹x∈A› ‹M(r)›
show ?thesis using Pi_assumptions by blast
qed
with assms and ‹M(r)›
have "M(?f)"
using Pi_assumptions minimum_replacement lam_closed
by simp
moreover from assms and calculation
have "?f ∈ Pi⇗M⇖(A,B)"
using lam_type[OF minimum_in, OF ‹well_ord(⋃x∈A. B(x),r)›, of A B]
Pi_rel_char by auto
ultimately
show ?thesis by blast
qed

lemma AC_Pi_rel: assumes "⋀x. x ∈ A ⟹ ∃y. y ∈ B(x)"
shows "∃z[M]. z ∈ Pi⇗M⇖(A, B)"
proof (cases "A=0")
interpret Pi0:M_Pi_assumptions_0
using Pi_assumptions by unfold_locales auto
case True
then
show ?thesis using assms by simp
next
case False
then
obtain a where "a ∈ A" by auto
― ‹It is noteworthy that without obtaining an element of
\<^term>‹A›, the final step won't work›
with assms
show ?thesis by (blast intro!: AC_M)
qed

end ― ‹\<^locale>‹M_Pi_assumptions_choice››

context M_cardinal_AC
begin

subsection‹Strengthened Forms of Existing Theorems on Cardinals›

lemma cardinal_rel_eqpoll_rel: "M(A) ⟹ |A|⇗M⇖ ≈⇗M⇖ A"
apply (rule choice_ax_well_ord [THEN rexE])
apply (auto intro:well_ord_cardinal_rel_eqpoll_rel)
done

lemmas cardinal_rel_idem = cardinal_rel_eqpoll_rel [THEN cardinal_rel_cong, simp]

lemma cardinal_rel_eqE: "|X|⇗M⇖ = |Y|⇗M⇖ ==> M(X) ⟹ M(Y) ⟹ X ≈⇗M⇖ Y"
apply (rule choice_ax_well_ord [THEN rexE], assumption)
apply (rule choice_ax_well_ord [THEN rexE, of Y], assumption)
apply (rule well_ord_cardinal_rel_eqE, assumption+)
done

lemma cardinal_rel_eqpoll_rel_iff: "M(X) ⟹ M(Y) ⟹ |X|⇗M⇖ = |Y|⇗M⇖ ⟷ X ≈⇗M⇖ Y"
by (blast intro: cardinal_rel_cong cardinal_rel_eqE)

lemma cardinal_rel_disjoint_Un:
"[| |A|⇗M⇖=|B|⇗M⇖;  |C|⇗M⇖=|D|⇗M⇖;  A ∩ C = 0;  B ∩ D = 0; M(A); M(B); M(C); M(D)|]
==> |A ∪ C|⇗M⇖ = |B ∪ D|⇗M⇖"

lemma lepoll_rel_imp_cardinal_rel_le: "A ≲⇗M⇖ B ==> M(A) ⟹ M(B) ⟹ |A|⇗M⇖ ≤ |B|⇗M⇖"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (erule well_ord_lepoll_rel_imp_cardinal_rel_le, assumption+)
done

lemma cadd_rel_assoc: "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊕⇗M⇖ j) ⊕⇗M⇖ k = i ⊕⇗M⇖ (j ⊕⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
done

lemma cmult_rel_assoc: "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊗⇗M⇖ j) ⊗⇗M⇖ k = i ⊗⇗M⇖ (j ⊗⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule well_ord_cmult_rel_assoc, assumption+)
done

lemma cadd_cmult_distrib: "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊕⇗M⇖ j) ⊗⇗M⇖ k = (i ⊗⇗M⇖ k) ⊕⇗M⇖ (j ⊗⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
done

lemma InfCard_rel_square_eq: "InfCard⇗M⇖(|A|⇗M⇖) ⟹ M(A) ⟹ A×A ≈⇗M⇖ A"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (erule well_ord_InfCard_rel_square_eq, assumption, simp_all)
done

subsection ‹The relationship between cardinality and le-pollence›

lemma Card_rel_le_imp_lepoll_rel:
assumes "|A|⇗M⇖ ≤ |B|⇗M⇖"
and types: "M(A)" "M(B)"
shows "A ≲⇗M⇖ B"
proof -
have "A ≈⇗M⇖ |A|⇗M⇖"
by (rule cardinal_rel_eqpoll_rel [THEN eqpoll_rel_sym], simp_all add:types)
also have "... ≲⇗M⇖ |B|⇗M⇖"
by (rule le_imp_subset [THEN subset_imp_lepoll_rel]) (rule assms, simp_all add:types)
also have "... ≈⇗M⇖ B"
finally show ?thesis by (simp_all add:types)
qed

lemma le_Card_rel_iff: "Card⇗M⇖(K) ==> M(K) ⟹ M(A) ⟹ |A|⇗M⇖ ≤ K ⟷ A ≲⇗M⇖ K"
apply (erule Card_rel_cardinal_rel_eq [THEN subst], assumption, rule iffI,
erule Card_rel_le_imp_lepoll_rel, assumption+)
apply (erule lepoll_rel_imp_cardinal_rel_le, assumption+)
done

lemma cardinal_rel_0_iff_0 [simp]: "M(A) ⟹ |A|⇗M⇖ = 0 ⟷ A = 0"
using cardinal_rel_0 eqpoll_rel_0_iff [THEN iffD1]
cardinal_rel_eqpoll_rel_iff [THEN iffD1, OF _ nonempty]
by auto

lemma cardinal_rel_lt_iff_lesspoll_rel:
assumes i: "Ord(i)" and
types: "M(i)" "M(A)"
shows "i < |A|⇗M⇖ ⟷ i ≺⇗M⇖ A"
proof
assume "i < |A|⇗M⇖"
hence  "i ≺⇗M⇖ |A|⇗M⇖"
by (blast intro: lt_Card_rel_imp_lesspoll_rel types)
also have "...  ≈⇗M⇖ A"
finally show "i ≺⇗M⇖ A" by (simp_all add:types)
next
assume "i ≺⇗M⇖ A"
also have "...  ≈⇗M⇖ |A|⇗M⇖"
by (blast intro: cardinal_rel_eqpoll_rel eqpoll_rel_sym types)
finally have "i ≺⇗M⇖ |A|⇗M⇖" by (simp_all add:types)
thus  "i < |A|⇗M⇖" using i types
by (force intro: cardinal_rel_lt_imp_lt lesspoll_rel_cardinal_rel_lt)
qed

lemma cardinal_rel_le_imp_lepoll_rel: " i ≤ |A|⇗M⇖ ==> M(i) ⟹ M(A) ⟹i ≲⇗M⇖ A"
by (blast intro: lt_Ord Card_rel_le_imp_lepoll_rel Ord_cardinal_rel_le le_trans)

subsection‹Other Applications of AC›

text‹We have an example of instantiating a locale involving higher
order variables inside a proof, by using the assumptions of the
first order, active locale.›

lemma surj_rel_implies_inj_rel:
assumes f: "f ∈ surj⇗M⇖(X,Y)" and
types: "M(f)" "M(X)" "M(Y)"
shows "∃g[M]. g ∈ inj⇗M⇖(Y,X)"
proof -
from types
interpret M_Pi_assumptions_choice _ Y "λy. f-``{y}"
by unfold_locales (auto intro:surj_imp_inj_replacement dest:transM)
from f AC_Pi_rel
obtain z where z: "z ∈ Pi⇗M⇖(Y, λy. f -`` {y})"
― ‹In this and the following ported result, it is not clear how
uniformly are "\_char" theorems to be used›
using surj_rel_char
by (auto simp add: surj_def types) (fast dest: apply_Pair)
show ?thesis
proof
show "z ∈ inj⇗M⇖(Y, X)" "M(z)"
using z surj_is_fun[of f X Y] f Pi_rel_char
by (auto dest: apply_type Pi_memberD
intro: apply_equality Pi_type f_imp_injective
qed
qed

text‹Kunen's Lemma 10.20›
lemma surj_rel_implies_cardinal_rel_le:
assumes f: "f ∈ surj⇗M⇖(X,Y)" and
types:"M(f)" "M(X)" "M(Y)"
shows "|Y|⇗M⇖ ≤ |X|⇗M⇖"
proof (rule lepoll_rel_imp_cardinal_rel_le)
from f [THEN surj_rel_implies_inj_rel]
obtain g where "g ∈ inj⇗M⇖(Y,X)"
by (blast intro:types)
then
show "Y ≲⇗M⇖ X"
using inj_rel_char
by (auto simp add: def_lepoll_rel types)

end ― ‹\<^locale>‹M_cardinal_AC››

text‹The set-theoretic universe.›

abbreviation
Universe :: "i⇒o" (‹𝒱›) where
"𝒱(x) ≡ True"

lemma separation_absolute: "separation(𝒱, P)"
unfolding separation_def
by (rule rallI, rule_tac x="{x∈_ . P(x)}" in rexI) auto

lemma univalent_absolute:
assumes "univalent(𝒱, A, P)" "P(x, b)" "x ∈ A"
shows "P(x, y) ⟹ y = b"
using assms
unfolding univalent_def by force

lemma replacement_absolute: "strong_replacement(𝒱, P)"
unfolding strong_replacement_def
proof (intro rallI impI)
fix A
assume "univalent(𝒱, A, P)"
then
show "∃Y[𝒱]. ∀b[𝒱]. b ∈ Y ⟷ (∃x[𝒱]. x ∈ A ∧ P(x, b))"
by (rule_tac x="{y. x∈A , P(x,y)}" in rexI)
(auto dest:univalent_absolute[of _ P])
qed

lemma Union_ax_absolute: "Union_ax(𝒱)"
unfolding Union_ax_def big_union_def
by (auto intro:rexI[of _ "⋃_"])

lemma upair_ax_absolute: "upair_ax(𝒱)"
unfolding upair_ax_def upair_def rall_def rex_def
by (auto)

lemma power_ax_absolute:"power_ax(𝒱)"
proof -
{
fix x
have "∀y[𝒱]. y ∈ Pow(x) ⟷ (∀z[𝒱]. z ∈ y ⟶ z ∈ x)"
by auto
}
then
show "power_ax(𝒱)"
unfolding power_ax_def powerset_def subset_def by blast
qed

locale M_cardinal_UN =  M_Pi_assumptions_choice _ K X for K X +
assumes
― ‹The next assumption is required by @{thm [source] Least_closed}›
X_witness_in_M: "w ∈ X(x) ⟹ M(x)"
and
lam_m_replacement:"M(f) ⟹ strong_replacement(M,
λx y. y = ⟨x, μ i. x ∈ X(i), f ` (μ i. x ∈ X(i)) ` x⟩)"
and
inj_replacement:
"M(x) ⟹ strong_replacement(M, λy z. y ∈ inj⇗M⇖(X(x), K) ∧ z = {⟨x, y⟩})"
"strong_replacement(M, λx y. y = inj⇗M⇖(X(x), K))"
"strong_replacement(M,
λx z. z = Sigfun(x, λi. inj⇗M⇖(X(i), K)))"
"M(r) ⟹ strong_replacement(M,
λx y. y = ⟨x, minimum(r, inj⇗M⇖(X(x), K))⟩)"

begin

lemma UN_closed: "M(⋃i∈K. X(i))"
using family_union_closed B_replacement Pi_assumptions by simp

text‹Kunen's Lemma 10.21›
lemma cardinal_rel_UN_le:
assumes K: "InfCard⇗M⇖(K)"
shows "(⋀i. i∈K ⟹ |X(i)|⇗M⇖ ≤ K) ⟹ |⋃i∈K. X(i)|⇗M⇖ ≤ K"
proof (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff Pi_assumptions)
have "M(f) ⟹ M(λx∈(⋃x∈K. X(x)). ⟨μ i. x ∈ X(i), f ` (μ i. x ∈ X(i)) ` x⟩)" for f
using lam_m_replacement X_witness_in_M Least_closed' Pi_assumptions UN_closed
by (rule_tac lam_closed) (auto dest:transM)
note types = this Pi_assumptions UN_closed
have [intro]: "Ord(K)" by (blast intro: InfCard_rel_is_Card_rel
Card_rel_is_Ord K types)
interpret pii:M_Pi_assumptions_choice _ K "λi. inj⇗M⇖(X(i), K)"
using inj_replacement Pi_assumptions transM[of _ K]
by unfold_locales (simp_all del:mem_inj_abs)
assume asm:"⋀i. i∈K ⟹ X(i) ≲⇗M⇖ K"
then
have "⋀i. i∈K ⟹ M(inj⇗M⇖(X(i), K))"
interpret V:M_N_Perm M "𝒱"
using separation_absolute replacement_absolute Union_ax_absolute
power_ax_absolute upair_ax_absolute
by unfold_locales auto
note bad_simps[simp del] = V.N.Forall_in_M_iff V.N.Equal_in_M_iff
V.N.nonempty
have abs:"inj_rel(𝒱,x,y) = inj(x,y)" for x y
using V.N.inj_rel_char by simp
from asm
have "⋀i. i∈K ⟹ ∃f[M]. f ∈ inj⇗M⇖(X(i), K)"
then
obtain f where "f ∈ (∏i∈K. inj⇗M⇖(X(i), K))" "M(f)"
using pii.AC_Pi_rel pii.Pi_rel_char by auto
with abs
have f:"f ∈ (∏i∈K. inj(X(i), K))"
using Pi_weaken_type[OF _ V.inj_rel_transfer, of f K X "λ_. K"]
Pi_assumptions by simp
{ fix z
assume z: "z ∈ (⋃i∈K. X(i))"
then obtain i where i: "i ∈ K" "Ord(i)" "z ∈ X(i)"
by (blast intro: Ord_in_Ord [of K])
hence "(μ i. z ∈ X(i)) ≤ i" by (fast intro: Least_le)
hence "(μ i. z ∈ X(i)) < K" by (best intro: lt_trans1 ltI i)
hence "(μ i. z ∈ X(i)) ∈ K" and "z ∈ X(μ i. z ∈ X(i))"
by (auto intro: LeastI ltD i)
} note mems = this
have "(⋃i∈K. X(i)) ≲⇗M⇖ K × K"
show "∃f[M]. f ∈ inj(⋃x∈K. X(x), K × K)"
apply (rule rexI)
apply (rule_tac c = "λz. ⟨μ i. z ∈ X(i), f ` (μ i. z ∈ X(i)) ` z⟩"
and d = "λ⟨i,j⟩. converse (f`i) ` j" in lam_injective)
apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
done
qed
also have "... ≈⇗M⇖ K"
by (simp add: K InfCard_rel_square_eq InfCard_rel_is_Card_rel
Card_rel_cardinal_rel_eq types)
finally have "(⋃i∈K. X(i)) ≲⇗M⇖ K" by (simp_all add:types)
then
show ?thesis
by (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff types)
qed

end ― ‹\<^locale>‹M_cardinal_UN››

end```