# Theory Cardinal_Relative

```section‹Relative, Choice-less Cardinal Numbers›

theory Cardinal_Relative
imports
Lambda_Replacement
Univ_Relative
begin

txt‹The following command avoids that a commonly used one-letter variable be
captured by the definition of the constructible universe \<^term>‹L›.›
hide_const (open) L

txt‹We also return to the old notation for \<^term>‹sum› to preserve the old
Constructibility code.›
notation sum (infixr ‹+› 65)

definition
Finite_rel   :: "[i⇒o,i]=>o"  where
"Finite_rel(M,A) ≡ ∃om[M]. ∃n[M]. omega(M,om) ∧ n∈om ∧ eqpoll_rel(M,A,n)"

definition
banach_functor :: "[i,i,i,i,i] ⇒ i" where
"banach_functor(X,Y,f,g,W) ≡ X - g``(Y - f``W)"

lemma banach_functor_subset: "banach_functor(X,Y,f,g,W) ⊆ X"
unfolding banach_functor_def by auto

definition
is_banach_functor :: "[i⇒o,i,i,i,i,i,i]⇒o"  where
"is_banach_functor(M,X,Y,f,g,W,b) ≡
∃fW[M]. ∃YfW[M]. ∃gYfW[M]. image(M,f,W,fW) ∧ setdiff(M,Y,fW,YfW) ∧
image(M,g,YfW,gYfW) ∧ setdiff(M,X,gYfW,b)"

lemma (in M_basic) banach_functor_abs :
assumes "M(X)" "M(Y)" "M(f)" "M(g)"
shows "relation1(M,is_banach_functor(M,X,Y,f,g),banach_functor(X,Y,f,g))"
unfolding relation1_def is_banach_functor_def banach_functor_def
using assms
by simp

lemma (in M_basic) banach_functor_closed:
assumes "M(X)" "M(Y)" "M(f)" "M(g)"
shows "∀W[M]. M(banach_functor(X,Y,f,g,W))"
unfolding banach_functor_def using assms image_closed
by simp

context M_trancl
begin

lemma iterates_banach_functor_closed:
assumes "n∈ω" "M(X)" "M(Y)" "M(f)" "M(g)"
shows "M(banach_functor(X,Y,f,g)^n(0))"
using assms banach_functor_closed
by (induct) simp_all

lemma banach_repl_iter':
assumes
"⋀A. M(A) ⟹ separation(M, λb. ∃x∈A. x ∈ ω ∧ b = banach_functor(X, Y, f, g)^x (0))"
"M(X)" "M(Y)" "M(f)" "M(g)"
shows
"strong_replacement(M, λx y. x∈nat ∧ y = banach_functor(X, Y, f, g)^x (0))"
unfolding strong_replacement_def
proof clarsimp
fix A
let ?Z="{b ∈ Pow⇗M⇖(X) . (∃x∈A. x ∈ ω ∧ b = banach_functor(X, Y, f, g)^x (0))}"
assume "M(A)"
moreover
note assms
moreover from calculation
have "M(?Z)" by simp
moreover from assms(2-)
have "b ∈ ?Z ⟷ (∃x∈A. x ∈ ω ∧ b = banach_functor(X, Y, f, g)^x (0))" for b
by (auto, rename_tac x, induct_tac x, (auto simp:def_Pow_rel)[1],
rule_tac def_Pow_rel[THEN iffD2, OF iterates_banach_functor_closed[of _ X Y f g]])
ultimately
show "∃Z[M]. ∀b[M]. b ∈ Z ⟷ (∃x∈A. x ∈ ω ∧ b = banach_functor(X, Y, f, g)^x (0))"
by (intro rexI[of _ ?Z]) simp
qed

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

context M_Perm
begin

lemma mem_Pow_rel: "M(r) ⟹ a ∈ Pow_rel(M,r) ⟹ a ∈ Pow(r) ∧ M(a)"
using Pow_rel_char by simp

lemma mem_bij_abs: "⟦M(f);M(A);M(B)⟧ ⟹  f ∈ bij⇗M⇖(A,B) ⟷ f∈bij(A,B)"
using bij_rel_char by simp

lemma mem_inj_abs: "⟦M(f);M(A);M(B)⟧ ⟹  f ∈ inj⇗M⇖(A,B) ⟷ f∈inj(A,B)"
using inj_rel_char by simp

lemma mem_surj_abs: "⟦M(f);M(A);M(B)⟧ ⟹  f ∈ surj⇗M⇖(A,B) ⟷ f∈surj(A,B)"
using surj_rel_char by simp

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

locale M_cardinals = M_ordertype + M_trancl + M_Perm + M_replacement +
assumes
separation(M, λz.
(∃x y. z = ⟨Inl(x), Inr(y)⟩) ∨
(∃x' x. z = ⟨Inl(x'), Inl(x)⟩ ∧ ⟨x', x⟩ ∈ R) ∨
(∃y' y. z = ⟨Inr(y'), Inr(y)⟩ ∧ ⟨y', y⟩ ∈ S))"
and
rmult_separation: "M(b) ⟹ M(d) ⟹ separation(M,
λz. ∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ b ∨ x' = x ∧ ⟨y', y⟩ ∈ d))"

begin

lemma rvimage_separation: "M(f) ⟹ M(r) ⟹
separation(M, λz. ∃x y. z = ⟨x, y⟩ ∧ ⟨f ` x, f ` y⟩ ∈ r)"
using separation_Pair separation_in lam_replacement_product
lam_replacement_fst lam_replacement_snd lam_replacement_constant
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
by simp

lemma rmult_closed[intro,simp]: "M(a) ⟹ M(b) ⟹ M(c) ⟹ M(d) ⟹ M(rmult(a,b,c,d))"
using rmult_separation by (auto simp add: rmult_def)

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

lemma (in M_cardinals) is_cardinal_iff_Least:
assumes "M(A)" "M(κ)"
shows "is_cardinal(M,A,κ) ⟷ κ = (μ i. M(i) ∧ i ≈⇗M⇖ A)"
using is_cardinal_iff assms
unfolding cardinal_rel_def by simp

subsection‹The Schroeder-Bernstein Theorem›
text‹See Davey and Priestly, page 106›

context M_cardinals
begin

subsection‹Banach's Decomposition Theorem›

lemma bnd_mono_banach_functor: "bnd_mono(X, banach_functor(X,Y,f,g))"
unfolding bnd_mono_def banach_functor_def
by blast

lemma inj_Inter:
assumes "g ∈ inj(Y,X)" "A≠0" "∀a∈A. a ⊆ Y"
shows "g``(⋂A) = (⋂a∈A. g``a)"
proof (intro equalityI subsetI)
fix x
from assms
obtain a where "a∈A" by blast
moreover
assume "x ∈ (⋂a∈A. g `` a)"
ultimately
have x_in_im: "x ∈ g``y" if "y∈A" for y
using that by auto
have exists: "∃z ∈ y. x = g`z" if "y∈A" for y
proof -
note that
moreover from this and x_in_im
have "x ∈ g``y" by simp
moreover from calculation
have "x ∈ g``y" by simp
moreover
note assms
ultimately
show ?thesis
using image_fun[OF inj_is_fun] by auto
qed
with ‹a∈A›
obtain z where "z ∈ a" "x = g`z" by auto
moreover
have "z ∈ y" if "y∈A" for y
proof -
from that and exists
obtain w where "w ∈ y" "x = g`w" by auto
moreover from this ‹x = g`z› assms that ‹a∈A› ‹z∈a›
have "z = w" unfolding inj_def by blast
ultimately
show ?thesis by simp
qed
moreover
note assms
moreover from calculation
have "z ∈ ⋂A" by auto
moreover from calculation
have "z ∈ Y" by blast
ultimately
show "x ∈ g `` (⋂A)"
using inj_is_fun[THEN funcI, of g] by fast
qed auto

lemma contin_banach_functor:
assumes "g ∈ inj(Y,X)"
shows "contin(banach_functor(X,Y,f,g))"
unfolding contin_def
proof (intro allI impI)
fix A
assume "directed(A)"
then
have "A ≠ 0"
unfolding directed_def ..
have "banach_functor(X, Y, f, g, ⋃A) = X - g``(Y - f``(⋃A))"
unfolding banach_functor_def ..
also
have " … = X - g``(Y - (⋃a∈A. f``a))"
by auto
also from ‹A≠0›
have " … = X - g``(⋂a∈A. Y-f``a)"
by auto
also from ‹A≠0› and assms
have " … = X - (⋂a∈A. g``(Y-f``a))"
using inj_Inter[of g Y X "{Y-f``a. a∈A}" ] by fastforce
also from ‹A≠0›
have " … = (⋃a∈A. X - g``(Y-f``a))" by simp
also
have " … = (⋃a∈A. banach_functor(X, Y, f, g, a))"
unfolding banach_functor_def ..
finally
show "banach_functor(X,Y,f,g,⋃A) = (⋃a∈A. banach_functor(X,Y,f,g,a))" .
qed

lemma lfp_banach_functor:
assumes "g∈inj(Y,X)"
shows "lfp(X, banach_functor(X,Y,f,g)) =
(⋃n∈nat. banach_functor(X,Y,f,g)^n (0))"
using assms lfp_eq_Union bnd_mono_banach_functor contin_banach_functor
by simp

lemma lfp_banach_functor_closed:
assumes "M(g)" "M(X)" "M(Y)" "M(f)" "g∈inj(Y,X)"
and banach_repl_iter: "M(X) ⟹ M(Y) ⟹ M(f) ⟹ M(g) ⟹
strong_replacement(M, λx y. x∈nat ∧ y = banach_functor(X, Y, f, g)^x (0))"
shows "M(lfp(X, banach_functor(X,Y,f,g)))"
proof -
from assms
have "M(banach_functor(X,Y,f,g)^n (0))" if "n∈nat" for n
with assms
show ?thesis
using family_union_closed'[OF banach_repl_iter M_nat] lfp_banach_functor
by simp
qed

lemma banach_decomposition_rel:
assumes
banach_repl_iter: "M(f) ⟹ M(g) ⟹ M(X) ⟹ M(Y) ⟹
strong_replacement(M, λx y. x∈nat ∧ y = banach_functor(X, Y, f, g)^x (0))"
shows
"[| M(f); M(g); M(X); M(Y); f ∈ X->Y;  g ∈ inj(Y,X) |] ==>
∃XA[M]. ∃XB[M]. ∃YA[M]. ∃YB[M].
(XA ∩ XB = 0) & (XA ∪ XB = X) &
(YA ∩ YB = 0) & (YA ∪ YB = Y) &
f``XA=YA & g``YB=XB"
apply (intro rexI conjI)
apply (rule_tac [6] Banach_last_equation)
apply (rule_tac [5] refl)
apply (assumption |
rule inj_is_fun Diff_disjoint Diff_partition fun_is_rel
image_subset lfp_subset)+
using lfp_banach_functor_closed[of g X Y f] assms
unfolding banach_functor_def by simp_all

lemma schroeder_bernstein_closed:
assumes
banach_repl_iter: "M(X) ⟹ M(Y) ⟹ M(f) ⟹ M(g) ⟹
strong_replacement(M, λx y. x∈nat ∧ y = banach_functor(X, Y, f, g)^x (0))"
shows
"[| M(f); M(g); M(X); M(Y); f ∈ inj(X,Y);  g ∈ inj(Y,X) |] ==> ∃h[M]. h ∈ bij(X,Y)"
apply (insert banach_decomposition_rel [of f g X Y, OF banach_repl_iter])
apply (auto)
apply (rule_tac x="restrict(f,XA) ∪ converse(restrict(g,YB))" in rexI)
apply (auto intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
done

text‹The previous lemmas finish our original, direct relativization
of the material involving the iterative proof (as appearing in \<^theory>‹ZF.Cardinal›)
of the Schröder-Bernstein theorem. Next, we formalize
Zermelo's proof that replaces the recursive construction by a fixed point
represented as an intersection \<^cite>‹‹Exr. x4.27› in "moschovakis1994notes"›. This allows
to avoid at least one replacement assumption.›

lemma dedekind_zermelo:
assumes
"A' ⊆ B" "B ⊆ A" "A ≈⇗M⇖ A'"
and types: "M(A')" "M(B)" "M(A)"
shows
"A ≈⇗M⇖ B"
proof -
from ‹A ≈⇗M⇖ A'› and types
obtain f where "f ∈ bij⇗M⇖(A,A')"
unfolding eqpoll_rel_def by blast
let ?Q="B - f``A"
from ‹f ∈ _› ‹A' ⊆ B› types
have "f``X ⊆ B" for X
using mem_bij_rel[THEN bij_is_fun, THEN Image_sub_codomain, of f A A'] by auto
moreover
note ‹B ⊆ A›
moreover from calculation
have "f``X ⊆ A" for X by auto
moreover
define 𝒯 where "𝒯  ≡ { X ∈ Pow⇗M⇖(A) . ?Q ∪ f `` X ⊆ X}"
moreover from calculation
have "A ∈ 𝒯" using def_Pow_rel by (auto simp:types)
ultimately
have "𝒯 ≠ 0" unfolding 𝒯_def by auto
let ?T="⋂𝒯"
have "?T ⊆ A"
proof
fix x
assume "x ∈ ?T"
with ‹𝒯 ≠ 0›
obtain X where "x ∈ X" "X ∈ 𝒯"
by blast
moreover from this
have "X ∈ Pow⇗M⇖(A)"
unfolding 𝒯_def by simp
moreover from calculation and ‹M(A)›
have "M(x)" using Pow_rel_char by (auto dest:transM)
ultimately
show "x ∈ A" using Pow_rel_char by (auto simp:types)
qed
moreover from ‹𝒯 ≠ 0›
have "?Q ∪ f``?T ⊆ ?T"
using image_mono unfolding 𝒯_def by blast
moreover from ‹f ∈ _›
have "M(𝒯)"
using zermelo_separation unfolding 𝒯_def by (auto simp:types dest:transM)
moreover from this
have "M(?T)" by simp
moreover
note ‹𝒯 ≠ 0›
ultimately
have "?T ∈ 𝒯"
unfolding 𝒯_def using def_Pow_rel
by (auto simp:types)
have "?T ⊆ ?Q ∪ f``?T"
proof (intro subsetI, rule ccontr)
fix x
from ‹_ ∪ f ``?T ⊆ ?T›
have "f `` (?T - {x}) ⊆ ?T" "f `` (?T - {x}) ⊆ f`` ?T" by auto
assume "x ∈ ?T" "x ∉ ?Q ∪ f``?T"
then
have "?T - {x} ∈ 𝒯"
proof -
note ‹f `` (?T - {x}) ⊆ ?T›
moreover from this and ‹x ∉ _ ∪ f``?T›
have "x ∉ f `` ?T" by simp
ultimately
have "f `` (?T - {x}) ⊆ ?T - {x}" by auto
moreover from ‹x ∉ ?Q ∪ _› ‹?Q ∪ _ ⊆ ?T›
have "?Q ⊆ ?T - {x}" by auto
moreover
note ‹?T ∈ _› ‹x ∈ ?T› ‹M(?T)› ‹?T ⊆ _›
ultimately
show ?thesis
using def_Pow_rel[of "?T - {x}" A] transM[of _ ?T]
unfolding 𝒯_def
by (auto simp:types)
qed
moreover
note ‹f `` (?T - {x}) ⊆ f`` ?T›
ultimately
have "?T ⊆ ?T - {x}" by auto
with ‹x ∈ ?T›
show False by auto
qed
with ‹?Q ∪ f``?T ⊆ ?T›
have "?T = ?Q ∪ f``?T" by auto
from ‹⋀X. f``X ⊆ B›
have "(?Q ∪ f``?T) ∪ (f``A - f``?T) ⊆ B" by auto
with ‹?T = _›
have "?T ∪ (f``A - f``?T) ⊆ B" by simp
with ‹𝒯 ≠ 0› ‹?T = _›
have "B = ?T ∪ (f``A - f``?T)"
proof (intro equalityI, intro subsetI)
fix x
assume "x ∈ B"
with ‹𝒯 ≠ 0› ‹?T = _›
show "x ∈ ?T ∪ (f``A - f``?T)"
by (subst ‹?T = _›, clarify)
qed
moreover from ‹?T ⊆ A›
have "A = ?T ∪ (A - ?T)" by auto
moreover from ‹M(?T)› ‹f ∈ _›
have "M(id(?T) ∪ restrict(f,A-?T))"
using bij_rel_closed[THEN [2] transM] id_closed by (auto simp:types)
moreover from ‹?T = _› ‹f ∈ _›
have "f``A - f``?T = f``(A - ?T)"
using bij_rel_char bij_is_inj[THEN inj_range_Diff, of f A]
by (auto simp:types)
from ‹f ∈ _› types
have "id(?T) ∪ restrict(f, A-?T) ∈ bij(?T ∪ (A - ?T),?T ∪ (f``A - f``?T))"
using id_bij mem_bij_rel[of _ A A', THEN bij_is_inj]
by (rule_tac bij_disjoint_Un; clarsimp)
(subst ‹f``A - f``?T =_ ›, auto intro:restrict_bij, subst ‹?T = _›, auto)
moreover
note types
ultimately
show ?thesis
using bij_rel_char unfolding eqpoll_rel_def by fastforce
qed

lemma schroeder_bernstein_closed':
assumes "f ∈ inj⇗M⇖(A,C)" " g ∈ inj⇗M⇖(C,A)"
and types:"M(A)" "M(C)"
shows "A ≈⇗M⇖ C"
proof -
from assms
have "f ∈ inj(A,C)" " g ∈ inj(C,A)" "M(f)" "M(g)"
using inj_rel_char by auto
moreover from this
have "g ∈ bij(C,range(g))" "g O f ∈ bij(A,range(g O f))"
using inj_bij_range comp_inj by auto blast
moreover from calculation
have "range(g O f) ⊆ range(g)" "range(g) ⊆ A"
using inj_is_fun[THEN range_fun_subset_codomain] by auto
moreover from calculation
obtain h where "h ∈ bij⇗M⇖(A, range(g))"
using dedekind_zermelo[of "range(g O f)" "range(g)" A]
bij_rel_char def_eqpoll_rel
by (auto simp:types)
ultimately
show ?thesis
using bij_rel_char def_eqpoll_rel comp_bij[of h A "range(g)" "converse(g)" C]
bij_converse_bij[of g C "range(g)"] by (auto simp:types)
qed

text‹Relative equipollence is an equivalence relation›

declare mem_bij_abs[simp] mem_inj_abs[simp]

lemma bij_imp_eqpoll_rel:
assumes "f ∈ bij(A,B)" "M(f)" "M(A)" "M(B)"
shows "A ≈⇗M⇖ B"
using assms by (auto simp add:def_eqpoll_rel)

lemma eqpoll_rel_refl: "M(A) ⟹ A ≈⇗M⇖ A"
using bij_imp_eqpoll_rel[OF id_bij, OF id_closed] .

lemma eqpoll_rel_sym: "X ≈⇗M⇖ Y ⟹ M(X) ⟹ M(Y) ⟹  Y ≈⇗M⇖ X"
unfolding def_eqpoll_rel using converse_closed
by (auto intro: bij_converse_bij)

lemma eqpoll_rel_trans [trans]:
"[|X ≈⇗M⇖ Y;  Y ≈⇗M⇖ Z;  M(X); M(Y) ; M(Z) |] ==> X ≈⇗M⇖ Z"
unfolding def_eqpoll_rel by (auto intro: comp_bij)

text‹Relative le-pollence is a preorder›

lemma subset_imp_lepoll_rel: "X ⊆ Y ⟹ M(X) ⟹ M(Y) ⟹ X ≲⇗M⇖ Y"
unfolding def_lepoll_rel using id_subset_inj id_closed
by simp blast

lemmas lepoll_rel_refl = subset_refl [THEN subset_imp_lepoll_rel, simp]

lemmas le_imp_lepoll_rel = le_imp_subset [THEN subset_imp_lepoll_rel]

lemma eqpoll_rel_imp_lepoll_rel: "X ≈⇗M⇖ Y ==> M(X) ⟹ M(Y) ⟹ X ≲⇗M⇖ Y"
unfolding def_eqpoll_rel bij_def def_lepoll_rel using bij_is_inj
by (auto)

lemma lepoll_rel_trans [trans]:
assumes
"X ≲⇗M⇖ Y" "Y ≲⇗M⇖ Z" "M(X)" "M(Y)" "M(Z)"
shows
"X ≲⇗M⇖ Z"
using assms def_lepoll_rel
by (auto intro: comp_inj)

lemma eq_lepoll_rel_trans [trans]:
assumes
"X ≈⇗M⇖ Y"  "Y ≲⇗M⇖ Z" "M(X)" "M(Y)" "M(Z)"
shows
"X ≲⇗M⇖ Z"
using assms
by (blast intro: eqpoll_rel_imp_lepoll_rel lepoll_rel_trans)

lemma lepoll_rel_eq_trans [trans]:
assumes "X ≲⇗M⇖ Y"  "Y ≈⇗M⇖ Z" "M(X)" "M(Y)" "M(Z)"
shows "X ≲⇗M⇖ Z"
using assms
eqpoll_rel_imp_lepoll_rel[of Y Z] lepoll_rel_trans[of X Y Z]
by simp

lemma eqpoll_relI: "⟦ X ≲⇗M⇖ Y; Y ≲⇗M⇖ X; M(X) ; M(Y) ⟧ ⟹ X ≈⇗M⇖ Y"
unfolding def_lepoll_rel using schroeder_bernstein_closed'
by (auto simp del:mem_inj_abs)

lemma eqpoll_relE:
"[| X ≈⇗M⇖ Y; [| X ≲⇗M⇖ Y; Y ≲⇗M⇖ X |] ==> P ;  M(X) ; M(Y) |] ==> P"
by (blast intro: eqpoll_rel_imp_lepoll_rel eqpoll_rel_sym)

lemma eqpoll_rel_iff: "M(X) ⟹ M(Y) ⟹ X ≈⇗M⇖ Y ⟷ X ≲⇗M⇖ Y & Y ≲⇗M⇖ X"
by (blast intro: eqpoll_relI elim: eqpoll_relE)

lemma lepoll_rel_0_is_0: "A ≲⇗M⇖ 0 ⟹ M(A) ⟹ A = 0"
using def_lepoll_rel
by (cases "A=0") (auto simp add: inj_def)

― ‹\<^term>‹M(Y) ⟹ 0 ≲⇗M⇖ Y››
lemmas empty_lepoll_relI = empty_subsetI [THEN subset_imp_lepoll_rel, OF nonempty]

lemma lepoll_rel_0_iff: "M(A) ⟹ A ≲⇗M⇖ 0 ⟷ A=0"
by (blast intro: lepoll_rel_0_is_0 lepoll_rel_refl)

lemma Un_lepoll_rel_Un:
"[| A ≲⇗M⇖ B; C ≲⇗M⇖ D; B ∩ D = 0; M(A); M(B); M(C); M(D) |] ==> A ∪ C ≲⇗M⇖ B ∪ D"
using def_lepoll_rel using inj_disjoint_Un[of _ A B _ C D] if_then_replacement
apply (auto)
apply (rule, assumption)
apply (auto intro!:lam_closed elim:transM)+
done

lemma eqpoll_rel_0_is_0: "A ≈⇗M⇖ 0 ⟹ M(A) ⟹ A = 0"
using eqpoll_rel_imp_lepoll_rel lepoll_rel_0_is_0 nonempty
by blast

lemma eqpoll_rel_0_iff: "M(A) ⟹ A ≈⇗M⇖ 0 ⟷ A=0"
by (blast intro: eqpoll_rel_0_is_0 eqpoll_rel_refl)

lemma eqpoll_rel_disjoint_Un:
"[| A ≈⇗M⇖ B;  C ≈⇗M⇖ D;  A ∩ C = 0;  B ∩ D = 0; M(A); M(B); M(C) ; M(D) |]
==> A ∪ C ≈⇗M⇖ B ∪ D"
by (auto intro: bij_disjoint_Un simp add:def_eqpoll_rel)

subsection‹lesspoll: contributions by Krzysztof Grabczewski›

lemma lesspoll_rel_not_refl: "M(i) ⟹ ~ (i ≺⇗M⇖ i)"

lemma lesspoll_rel_irrefl: "i ≺⇗M⇖ i ==> M(i) ⟹ P"

lemma lesspoll_rel_imp_lepoll_rel: "⟦A ≺⇗M⇖ B; M(A); M(B)⟧⟹ A ≲⇗M⇖ B"
by (unfold lesspoll_rel_def, blast)

lemma rvimage_closed [intro,simp]:
assumes
"M(A)" "M(f)" "M(r)"
shows
"M(rvimage(A,f,r))"
unfolding rvimage_def using assms rvimage_separation by auto

lemma lepoll_rel_well_ord: "[| A ≲⇗M⇖ B; well_ord(B,r); M(A); M(B); M(r) |] ==> ∃s[M]. well_ord(A,s)"
unfolding def_lepoll_rel by (auto intro:well_ord_rvimage)

lemma lepoll_rel_iff_leqpoll_rel: "⟦M(A); M(B)⟧ ⟹ A ≲⇗M⇖ B ⟷ A ≺⇗M⇖ B | A ≈⇗M⇖ B"
apply (unfold lesspoll_rel_def)
apply (blast intro: eqpoll_relI elim: eqpoll_relE)
done

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

context M_cardinals
begin

lemma inj_rel_is_fun_M: "f ∈ inj⇗M⇖(A,B) ⟹ M(f) ⟹ M(A) ⟹ M(B) ⟹ f ∈ A →⇗M⇖ B"
using inj_is_fun function_space_rel_char by simp

― ‹In porting the following theorem, I tried to follow the Discipline
strictly, though finally only an approach maximizing the use of
absoluteness results (@{thm [source] function_space_rel_char inj_rel_char}) was
the one paying dividends.›
lemma inj_rel_not_surj_rel_succ:
notes mem_inj_abs[simp del]
assumes fi: "f ∈ inj⇗M⇖(A, succ(m))" and fns: "f ∉ surj⇗M⇖(A, succ(m))"
and types: "M(f)" "M(A)" "M(m)"
shows "∃f[M]. f ∈ inj⇗M⇖(A,m)"
proof -
from fi [THEN inj_rel_is_fun_M] fns types
obtain y where y: "y ∈ succ(m)" "⋀x. x∈A ⟹ f ` x ≠ y" "M(y)"
show ?thesis
proof
from types and ‹M(y)›
show "M(λz∈A. if f ` z = m then y else f ` z)"
using transM[OF _ ‹M(A)›] lam_if_then_apply_replacement2 lam_replacement_iff_lam_closed
by (auto)
with types y fi
have "(λz∈A. if f`z = m then y else f`z) ∈ A→⇗M⇖ m"
using function_space_rel_char inj_rel_char inj_is_fun[of f A "succ(m)"]
by (auto intro!: if_type [THEN lam_type] dest: apply_funtype)
with types y fi
show "(λz∈A. if f`z = m then y else f`z) ∈ inj⇗M⇖(A, m)"
qed
qed

― ‹Variations on transitivity›

lemma lesspoll_rel_trans [trans]:
"[| X ≺⇗M⇖ Y; Y ≺⇗M⇖ Z; M(X); M(Y) ; M(Z) |] ==> X ≺⇗M⇖ Z"
apply (unfold lesspoll_rel_def)
apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
done

lemma lesspoll_rel_trans1 [trans]:
"[| X ≲⇗M⇖ Y; Y ≺⇗M⇖ Z; M(X); M(Y) ; M(Z) |] ==> X ≺⇗M⇖ Z"
apply (unfold lesspoll_rel_def)
apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
done

lemma lesspoll_rel_trans2 [trans]:
"[|  X ≺⇗M⇖ Y; Y ≲⇗M⇖ Z; M(X); M(Y) ; M(Z)|] ==> X ≺⇗M⇖ Z"
apply (unfold lesspoll_rel_def)
apply (blast elim: eqpoll_relE intro: eqpoll_relI lepoll_rel_trans)
done

lemma eq_lesspoll_rel_trans [trans]:
"[| X ≈⇗M⇖ Y; Y ≺⇗M⇖ Z; M(X); M(Y) ; M(Z) |] ==> X ≺⇗M⇖ Z"
by (blast intro: eqpoll_rel_imp_lepoll_rel lesspoll_rel_trans1)

lemma lesspoll_rel_eq_trans [trans]:
"[| X ≺⇗M⇖ Y; Y ≈⇗M⇖ Z; M(X); M(Y) ; M(Z) |] ==> X ≺⇗M⇖ Z"
by (blast intro: eqpoll_rel_imp_lepoll_rel lesspoll_rel_trans2)

lemma is_cardinal_cong:
assumes "X ≈⇗M⇖ Y" "M(X)" "M(Y)"
shows "∃κ[M]. is_cardinal(M,X,κ) ∧ is_cardinal(M,Y,κ)"
proof -
from assms
have "(μ i. M(i) ∧ i ≈⇗M⇖ X) = (μ i. M(i) ∧ i ≈⇗M⇖ Y)"
by (intro Least_cong) (auto intro: comp_bij bij_converse_bij simp add:def_eqpoll_rel)
moreover from assms
have "M(μ i. M(i) ∧ i ≈⇗M⇖ X)"
using Least_closed' by fastforce
moreover
note assms
ultimately
show ?thesis
using is_cardinal_iff_Least
by auto
qed

― ‹ported from Cardinal›
lemma cardinal_rel_cong: "X ≈⇗M⇖ Y ⟹ M(X) ⟹ M(Y) ⟹ |X|⇗M⇖ = |Y|⇗M⇖"
apply (rule Least_cong)
apply (auto intro: comp_bij bij_converse_bij)
done

lemma well_ord_is_cardinal_eqpoll_rel:
assumes "well_ord(A,r)" shows "is_cardinal(M,A,κ) ⟹ M(A) ⟹ M(κ) ⟹ M(r) ⟹ κ ≈⇗M⇖ A"
proof (subst is_cardinal_iff_Least[THEN iffD1, of A κ])
assume "M(A)" "M(κ)" "M(r)" "is_cardinal(M,A,κ)"
moreover from assms and calculation
obtain f i where "M(f)" "Ord(i)" "M(i)" "f ∈ bij(A,i)"
using ordertype_exists[of A r] ord_iso_is_bij by auto
moreover
have "M(μ i. M(i) ∧ i ≈⇗M⇖ A)"
using Least_closed' by fastforce
ultimately
show "(μ i. M(i) ∧ i ≈⇗M⇖ A) ≈⇗M⇖ A"
using assms[THEN well_ord_imp_relativized]
LeastI[of "λi. M(i) ∧ i ≈⇗M⇖ A" i] Ord_ordertype[OF assms]
bij_converse_bij[THEN bij_imp_eqpoll_rel, of f] by simp
qed

lemmas Ord_is_cardinal_eqpoll_rel = well_ord_Memrel[THEN well_ord_is_cardinal_eqpoll_rel]

section‹Porting from \<^theory>‹ZF.Cardinal››

txt‹The following results were ported more or less directly from \<^theory>‹ZF.Cardinal››

― ‹This result relies on various closure properties and
thus cannot be translated directly›
lemma well_ord_cardinal_rel_eqpoll_rel:
assumes r: "well_ord(A,r)" and "M(A)" "M(r)" shows "|A|⇗M⇖ ≈⇗M⇖ A"
using assms well_ord_is_cardinal_eqpoll_rel is_cardinal_iff
by blast

lemmas Ord_cardinal_rel_eqpoll_rel = well_ord_Memrel[THEN well_ord_cardinal_rel_eqpoll_rel]

lemma Ord_cardinal_rel_idem: "Ord(A) ⟹ M(A) ⟹ ||A|⇗M⇖|⇗M⇖ = |A|⇗M⇖"
by (rule_tac Ord_cardinal_rel_eqpoll_rel [THEN cardinal_rel_cong]) auto

lemma well_ord_cardinal_rel_eqE:
assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X|⇗M⇖ = |Y|⇗M⇖"
and types: "M(X)" "M(r)" "M(Y)" "M(s)"
shows "X ≈⇗M⇖ Y"
proof -
from types
have "X ≈⇗M⇖ |X|⇗M⇖" by (blast intro: well_ord_cardinal_rel_eqpoll_rel [OF woX] eqpoll_rel_sym)
also
have "... = |Y|⇗M⇖" by (rule eq)
also from types
have "... ≈⇗M⇖ Y" by (rule_tac well_ord_cardinal_rel_eqpoll_rel [OF woY])
finally show ?thesis  by (simp add:types)
qed

lemma well_ord_cardinal_rel_eqpoll_rel_iff:
"[| well_ord(X,r);  well_ord(Y,s); M(X); M(r); M(Y); M(s) |] ==> |X|⇗M⇖ = |Y|⇗M⇖ ⟷ X ≈⇗M⇖ Y"
by (blast intro: cardinal_rel_cong well_ord_cardinal_rel_eqE)

lemma Ord_cardinal_rel_le: "Ord(i) ⟹ M(i) ==> |i|⇗M⇖ ≤ i"
unfolding cardinal_rel_def
using eqpoll_rel_refl Least_le by simp

lemma Card_rel_cardinal_rel_eq: "Card⇗M⇖(K) ==> M(K) ⟹ |K|⇗M⇖ = K"
apply (unfold Card_rel_def)
apply (erule sym)
done

lemma Card_relI: "[| Ord(i);  !!j. j<i ⟹ M(j) ==> ~(j ≈⇗M⇖ i); M(i) |] ==> Card⇗M⇖(i)"
apply (unfold Card_rel_def cardinal_rel_def)
apply (subst Least_equality)
apply (blast intro: eqpoll_rel_refl)+
done

lemma Card_rel_is_Ord: "Card⇗M⇖(i) ==> M(i) ⟹ Ord(i)"
apply (unfold Card_rel_def cardinal_rel_def)
apply (erule ssubst)
apply (rule Ord_Least)
done

lemma Card_rel_cardinal_rel_le: "Card⇗M⇖(K) ==> M(K) ⟹ K ≤ |K|⇗M⇖"
apply (simp (no_asm_simp) add: Card_rel_is_Ord Card_rel_cardinal_rel_eq)
done

lemma Ord_cardinal_rel [simp,intro!]: "M(A) ⟹ Ord(|A|⇗M⇖)"
apply (unfold cardinal_rel_def)
apply (rule Ord_Least)
done

lemma Card_rel_iff_initial: assumes types:"M(K)"
shows "Card⇗M⇖(K) ⟷ Ord(K) & (∀j[M]. j<K ⟶ ~ (j ≈⇗M⇖ K))"
proof -
{ fix j
assume K: "Card⇗M⇖(K)" "M(j) ∧ j ≈⇗M⇖ K"
assume "j < K"
also have "... = (μ i. M(i) ∧ i ≈⇗M⇖ K)" using K
by (simp add: Card_rel_def cardinal_rel_def types)
finally have "j < (μ i. M(i) ∧ i ≈⇗M⇖ K)" .
then have "False" using K
by (best intro: less_LeastE[of "λj. M(j) ∧ j ≈⇗M⇖ K"])
}
with types
show ?thesis
by (blast intro: Card_relI Card_rel_is_Ord)
qed

lemma lt_Card_rel_imp_lesspoll_rel: "[| Card⇗M⇖(a); i<a; M(a); M(i) |] ==> i ≺⇗M⇖ a"
apply (unfold lesspoll_rel_def)
apply (frule Card_rel_iff_initial [THEN iffD1], assumption)
apply (blast intro!: leI [THEN le_imp_lepoll_rel])
done

lemma Card_rel_0: "Card⇗M⇖(0)"
apply (rule Ord_0 [THEN Card_relI])
apply (auto elim!: ltE)
done

lemma Card_rel_Un: "[| Card⇗M⇖(K);  Card⇗M⇖(L); M(K); M(L) |] ==> Card⇗M⇖(K ∪ L)"
apply (rule Ord_linear_le [of K L])
apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_rel_is_Ord le_imp_subset
subset_Un_iff2 [THEN iffD1])
done

lemma Card_rel_cardinal_rel [iff]: assumes types:"M(A)" shows "Card⇗M⇖(|A|⇗M⇖)"
using assms
proof (unfold cardinal_rel_def)
show "Card⇗M⇖(μ i. M(i) ∧ i ≈⇗M⇖ A)"
proof (cases "∃i[M]. Ord (i) ∧ i ≈⇗M⇖ A")
case False thus ?thesis           ― ‹degenerate case›
using Least_0[of "λi. M(i) ∧ i ≈⇗M⇖ A"] Card_rel_0
by fastforce
next
case True                         ― ‹real case: \<^term>‹A› is isomorphic to some ordinal›
then obtain i where i: "Ord(i)" "i ≈⇗M⇖ A" "M(i)" by blast
show ?thesis
proof (rule Card_relI [OF Ord_Least], rule notI)
fix j
assume j: "j < (μ i. M(i) ∧ i ≈⇗M⇖ A)" and "M(j)"
assume "j ≈⇗M⇖ (μ i. M(i) ∧ i ≈⇗M⇖ A)"
also have "... ≈⇗M⇖ A" using i LeastI[of "λi. M(i) ∧ i ≈⇗M⇖ A"] by (auto)
finally have "j ≈⇗M⇖ A"
using Least_closed'[of "λi. M(i) ∧ i ≈⇗M⇖ A"] by (simp add: ‹M(j)› types)
thus False
using ‹M(j)› by (blast intro:less_LeastE [OF _ j])
qed (auto intro:Least_closed)
qed
qed

lemma cardinal_rel_eq_lemma:
assumes i:"|i|⇗M⇖ ≤ j" and j: "j ≤ i" and types: "M(i)" "M(j)"
shows "|j|⇗M⇖ = |i|⇗M⇖"
proof (rule eqpoll_relI [THEN cardinal_rel_cong])
show "j ≲⇗M⇖ i" by (rule le_imp_lepoll_rel [OF j]) (simp_all add:types)
next
have Oi: "Ord(i)" using j by (rule le_Ord2)
with types
have "i ≈⇗M⇖ |i|⇗M⇖"
by (blast intro: Ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym)
also from types
have "... ≲⇗M⇖ j"
by (blast intro: le_imp_lepoll_rel i)
finally show "i ≲⇗M⇖ j" by (simp_all add:types)

lemma cardinal_rel_mono:
assumes ij: "i ≤ j" and types:"M(i)" "M(j)" shows "|i|⇗M⇖ ≤ |j|⇗M⇖"
using Ord_cardinal_rel [OF ‹M(i)›] Ord_cardinal_rel [OF ‹M(j)›]
proof (cases rule: Ord_linear_le)
case le then show ?thesis .
next
case ge
have i: "Ord(i)" using ij
have ci: "|i|⇗M⇖ ≤ j"
by (blast intro: Ord_cardinal_rel_le ij le_trans i types)
have "|i|⇗M⇖ = ||i|⇗M⇖|⇗M⇖"
by (auto simp add: Ord_cardinal_rel_idem i types)
also have "... = |j|⇗M⇖"
by (rule cardinal_rel_eq_lemma [OF ge ci]) (simp_all add:types)
finally have "|i|⇗M⇖ = |j|⇗M⇖" .
qed

lemma cardinal_rel_lt_imp_lt: "[| |i|⇗M⇖ < |j|⇗M⇖;  Ord(i);  Ord(j); M(i); M(j) |] ==> i < j"
apply (rule Ord_linear2 [of i j], assumption+)
apply (erule lt_trans2 [THEN lt_irrefl])
apply (erule cardinal_rel_mono, assumption+)
done

lemma Card_rel_lt_imp_lt: "[| |i|⇗M⇖ < K;  Ord(i);  Card⇗M⇖(K); M(i); M(K)|] ==> i < K"
by (simp (no_asm_simp) add: cardinal_rel_lt_imp_lt Card_rel_is_Ord Card_rel_cardinal_rel_eq)

lemma Card_rel_lt_iff: "[| Ord(i);  Card⇗M⇖(K); M(i); M(K) |] ==> (|i|⇗M⇖ < K) ⟷ (i < K)"
by (blast intro: Card_rel_lt_imp_lt Ord_cardinal_rel_le [THEN lt_trans1])

lemma Card_rel_le_iff: "[| Ord(i);  Card⇗M⇖(K); M(i); M(K) |] ==> (K ≤ |i|⇗M⇖) ⟷ (K ≤ i)"
by (simp add: Card_rel_lt_iff Card_rel_is_Ord not_lt_iff_le [THEN iff_sym])

lemma well_ord_lepoll_rel_imp_cardinal_rel_le:
assumes wB: "well_ord(B,r)" and AB: "A ≲⇗M⇖ B"
and
types: "M(B)" "M(r)" "M(A)"
shows "|A|⇗M⇖ ≤ |B|⇗M⇖"
using Ord_cardinal_rel [OF ‹M(A)›] Ord_cardinal_rel [OF ‹M(B)›]
proof (cases rule: Ord_linear_le)
case le thus ?thesis .
next
case ge
from lepoll_rel_well_ord [OF AB wB]
obtain s where s: "well_ord(A, s)" "M(s)" by (blast intro:types)
have "B ≈⇗M⇖ |B|⇗M⇖" by (blast intro: wB eqpoll_rel_sym well_ord_cardinal_rel_eqpoll_rel types)
also have "... ≲⇗M⇖ |A|⇗M⇖" by (rule le_imp_lepoll_rel [OF ge]) (simp_all add:types)
also have "... ≈⇗M⇖ A" by (rule well_ord_cardinal_rel_eqpoll_rel [OF s(1) _ s(2)]) (simp_all add:types)
finally have "B ≲⇗M⇖ A" by (simp_all add:types)
hence "A ≈⇗M⇖ B" by (blast intro: eqpoll_relI AB types)
hence "|A|⇗M⇖ = |B|⇗M⇖" by (rule cardinal_rel_cong) (simp_all add:types)
qed

lemma lepoll_rel_cardinal_rel_le: "[| A ≲⇗M⇖ i; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ ≤ i"
using Memrel_closed
apply (rule_tac le_trans)
apply (erule well_ord_Memrel [THEN well_ord_lepoll_rel_imp_cardinal_rel_le], assumption+)
apply (erule Ord_cardinal_rel_le, assumption)
done

lemma lepoll_rel_Ord_imp_eqpoll_rel: "[| A ≲⇗M⇖ i; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ ≈⇗M⇖ A"
by (blast intro: lepoll_rel_cardinal_rel_le well_ord_Memrel well_ord_cardinal_rel_eqpoll_rel dest!: lepoll_rel_well_ord)

lemma lesspoll_rel_imp_eqpoll_rel: "[| A ≺⇗M⇖ i; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ ≈⇗M⇖ A"
using lepoll_rel_Ord_imp_eqpoll_rel[OF lesspoll_rel_imp_lepoll_rel] .

lemma lesspoll_cardinal_lt_rel:
shows "[| A ≺⇗M⇖ i; Ord(i); M(i); M(A) |] ==> |A|⇗M⇖ < i"
proof -
assume assms:"A ≺⇗M⇖ i" ‹Ord(i)› ‹M(i)› ‹M(A)›
then
have A:"Ord(|A|⇗M⇖)" "|A|⇗M⇖ ≈⇗M⇖ A" "M(|A|⇗M⇖)"
using Ord_cardinal_rel lesspoll_rel_imp_eqpoll_rel
by simp_all
with assms
have "|A|⇗M⇖ ≺⇗M⇖ i"
using eq_lesspoll_rel_trans by auto
consider "|A|⇗M⇖∈i" | "|A|⇗M⇖=i" | "i∈|A|⇗M⇖"
using Ord_linear[OF ‹Ord(i)› ‹Ord(|A|⇗M⇖)›] by auto
then
have "|A|⇗M⇖ < i"
proof(cases)
case 1
then show ?thesis using ltI ‹Ord(i)› by simp
next
case 2
with ‹|A|⇗M⇖ ≺⇗M⇖ i› ‹M(i)›
show ?thesis using lesspoll_rel_irrefl by simp
next
case 3
with ‹Ord(|A|⇗M⇖)›
have "i<|A|⇗M⇖" using ltI by simp
with ‹M(A)› A ‹M(i)›
have "i ≺⇗M⇖ |A|⇗M⇖"
using lt_Card_rel_imp_lesspoll_rel Card_rel_cardinal_rel by simp
with ‹M(|A|⇗M⇖)› ‹M(i)›
show ?thesis
using lesspoll_rel_irrefl lesspoll_rel_trans[OF ‹|A|⇗M⇖ ≺⇗M⇖ i› ‹i ≺⇗M⇖ _ ›]
by simp
qed
then show ?thesis by simp
qed

lemma cardinal_rel_subset_Ord: "[|A<=i; Ord(i); M(A); M(i)|] ==> |A|⇗M⇖ ⊆ i"
apply (drule subset_imp_lepoll_rel [THEN lepoll_rel_cardinal_rel_le])
apply (blast intro: Ord_trans)
done

― ‹The next lemma is the first with several porting issues›
lemma cons_lepoll_rel_consD:
"[| cons(u,A) ≲⇗M⇖ cons(v,B);  u∉A;  v∉B; M(u); M(A); M(v); M(B) |] ==> A ≲⇗M⇖ B"
apply (simp add: def_lepoll_rel, unfold inj_def, safe)
apply (rule_tac x = "λx∈A. if f`x=v then f`u else f`x" in rexI)
apply (rule CollectI)
― ‹Proving it's in the function space \<^term>‹A→B››
apply (rule if_type [THEN lam_type])
apply (blast dest: apply_funtype)
apply (blast elim!: mem_irrefl dest: apply_funtype)
― ‹Proving it's injective›
apply (auto simp add:transM[of _ A])
using lam_replacement_iff_lam_closed  lam_if_then_apply_replacement
by simp

lemma cons_eqpoll_rel_consD: "[| cons(u,A) ≈⇗M⇖ cons(v,B);  u∉A;  v∉B; M(u); M(A); M(v); M(B) |] ==> A ≈⇗M⇖ B"
apply (blast intro: cons_lepoll_rel_consD)
done

lemma succ_lepoll_rel_succD: "succ(m) ≲⇗M⇖ succ(n) ⟹ M(m) ⟹ M(n) ==> m ≲⇗M⇖ n"
apply (unfold succ_def)
apply (erule cons_lepoll_rel_consD)
apply (rule mem_not_refl)+
apply assumption+
done

lemma nat_lepoll_rel_imp_le:
"m ∈ nat ==> n ∈ nat ⟹ m ≲⇗M⇖ n ⟹ M(m) ⟹ M(n) ⟹ m ≤ n"
proof (induct m arbitrary: n rule: nat_induct)
case 0 thus ?case by (blast intro!: nat_0_le)
next
case (succ m)
show ?case  using ‹n ∈ nat›
proof (cases rule: natE)
case 0 thus ?thesis using succ
next
case (succ n') thus ?thesis using succ.hyps ‹ succ(m) ≲⇗M⇖ n›
by (blast dest!: succ_lepoll_rel_succD)
qed
qed

lemma nat_eqpoll_rel_iff: "[| m ∈ nat; n ∈ nat; M(m); M(n) |] ==> m ≈⇗M⇖ n ⟷ m = n"
apply (rule iffI)
apply (blast intro: nat_lepoll_rel_imp_le le_anti_sym elim!: eqpoll_relE)
done

lemma nat_into_Card_rel:
assumes n: "n ∈ nat" and types: "M(n)" shows "Card⇗M⇖(n)"
using types
apply (subst Card_rel_def)
proof (unfold cardinal_rel_def, rule sym)
have "Ord(n)" using n  by auto
moreover
{ fix i
assume "i < n" "M(i)" "i ≈⇗M⇖ n"
hence False using n
by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_rel_iff] types)
}
ultimately show "(μ i. M(i) ∧ i ≈⇗M⇖ n) = n" by (auto intro!: Least_equality types eqpoll_rel_refl)
qed

lemmas cardinal_rel_0 = nat_0I [THEN nat_into_Card_rel, THEN Card_rel_cardinal_rel_eq, simplified, iff]
lemmas cardinal_rel_1 = nat_1I [THEN nat_into_Card_rel, THEN Card_rel_cardinal_rel_eq, simplified, iff]

lemma succ_lepoll_rel_natE: "[| succ(n) ≲⇗M⇖ n;  n ∈ nat |] ==> P"
by (rule nat_lepoll_rel_imp_le [THEN lt_irrefl], auto)

lemma nat_lepoll_rel_imp_ex_eqpoll_rel_n:
"[| n ∈ nat;  nat ≲⇗M⇖ X ; M(n); M(X)|] ==> ∃Y[M]. Y ⊆ X & n ≈⇗M⇖ Y"
apply (fast del: subsetI subsetCE
intro!: subset_SIs
dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
elim!: restrict_bij
inj_is_fun [THEN fun_is_rel, THEN image_subset])
done

lemma lepoll_rel_succ: "M(i) ⟹ i ≲⇗M⇖ succ(i)"
by (blast intro: subset_imp_lepoll_rel)

lemma lepoll_rel_imp_lesspoll_rel_succ:
assumes A: "A ≲⇗M⇖ m" and m: "m ∈ nat"
and types: "M(A)" "M(m)"
shows "A ≺⇗M⇖ succ(m)"
proof -
{ assume "A ≈⇗M⇖ succ(m)"
hence "succ(m) ≈⇗M⇖ A" by (rule eqpoll_rel_sym) (auto simp add:types)
also have "... ≲⇗M⇖ m" by (rule A)
finally have "succ(m) ≲⇗M⇖ m" by (auto simp add:types)
hence False by (rule succ_lepoll_rel_natE) (rule m) }
moreover have "A ≲⇗M⇖ succ(m)" by (blast intro: lepoll_rel_trans A lepoll_rel_succ types)
ultimately show ?thesis by (auto simp add: types lesspoll_rel_def)
qed

lemma lesspoll_rel_succ_imp_lepoll_rel:
"[| A ≺⇗M⇖ succ(m); m ∈ nat; M(A); M(m) |] ==> A ≲⇗M⇖ m"
proof -
{
assume "m ∈ nat" "M(A)" "M(m)" "A ≲⇗M⇖ succ(m)"
"∀f∈inj⇗M⇖(A, succ(m)). f ∉ surj⇗M⇖(A, succ(m))"
moreover from this
obtain f where "M(f)" "f∈inj⇗M⇖(A,succ(m))"
using def_lepoll_rel by auto
moreover from calculation
have "f ∉ surj⇗M⇖(A, succ(m))" by simp
ultimately
have "∃f[M]. f ∈ inj⇗M⇖(A, m)"
using inj_rel_not_surj_rel_succ by auto
}
from this
show "⟦ A ≺⇗M⇖ succ(m); m ∈ nat; M(A); M(m) ⟧ ⟹ A ≲⇗M⇖ m"
unfolding lepoll_rel_def eqpoll_rel_def bij_rel_def lesspoll_rel_def
by (simp del:mem_inj_abs)
qed

lemma lesspoll_rel_succ_iff: "m ∈ nat ⟹ M(A) ==> A ≺⇗M⇖ succ(m) ⟷ A ≲⇗M⇖ m"
by (blast intro!: lepoll_rel_imp_lesspoll_rel_succ lesspoll_rel_succ_imp_lepoll_rel)

lemma lepoll_rel_succ_disj: "[| A ≲⇗M⇖ succ(m);  m ∈ nat; M(A) ; M(m)|] ==> A ≲⇗M⇖ m | A ≈⇗M⇖ succ(m)"
apply (rule disjCI)
apply (rule lesspoll_rel_succ_imp_lepoll_rel)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: lesspoll_rel_def, assumption+)
done

lemma lesspoll_rel_cardinal_rel_lt: "[| A ≺⇗M⇖ i; Ord(i); M(A); M(i) |] ==> |A|⇗M⇖ < i"
apply (unfold lesspoll_rel_def, clarify)
apply (frule lepoll_rel_cardinal_rel_le, assumption+) ― ‹because of types›
apply (blast intro: well_ord_Memrel well_ord_cardinal_rel_eqpoll_rel [THEN eqpoll_rel_sym]
dest: lepoll_rel_well_ord  elim!: leE)
done

lemma lt_not_lepoll_rel:
assumes n: "n<i" "n ∈ nat"
and types:"M(n)" "M(i)" shows "~ i ≲⇗M⇖ n"
proof -
{ assume i: "i ≲⇗M⇖ n"
have "succ(n) ≲⇗M⇖ i" using n
by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll_rel] types)
also have "... ≲⇗M⇖ n" by (rule i)
finally have "succ(n) ≲⇗M⇖ n" by (simp add:types)
hence False  by (rule succ_lepoll_rel_natE) (rule n) }
thus ?thesis by auto
qed

text‹A slightly weaker version of ‹nat_eqpoll_rel_iff››
lemma Ord_nat_eqpoll_rel_iff:
assumes i: "Ord(i)" and n: "n ∈ nat"
and types: "M(i)" "M(n)"
shows "i ≈⇗M⇖ n ⟷ i=n"
using i nat_into_Ord [OF n]
proof (cases rule: Ord_linear_lt)
case lt
hence  "i ∈ nat" by (rule lt_nat_in_nat) (rule n)
thus ?thesis by (simp add: nat_eqpoll_rel_iff n types)
next
case eq
thus ?thesis by (simp add: eqpoll_rel_refl types)
next
case gt
hence  "~ i ≲⇗M⇖ n" using n  by (rule lt_not_lepoll_rel) (simp_all add: types)
hence  "~ i ≈⇗M⇖ n" using n  by (blast intro: eqpoll_rel_imp_lepoll_rel types)
moreover have "i ≠ n" using ‹n<i› by auto
ultimately show ?thesis by blast
qed

lemma Card_rel_nat: "Card⇗M⇖(nat)"
proof -
{ fix i
assume i: "i < nat" "i ≈⇗M⇖ nat" "M(i)"
hence "~ nat ≲⇗M⇖ i"
hence False using i
}
hence "(μ i. M(i) ∧ i ≈⇗M⇖ nat) = nat" by (blast intro: Least_equality eqpoll_rel_refl)
thus ?thesis
by (auto simp add: Card_rel_def cardinal_rel_def)
qed

lemma nat_le_cardinal_rel: "nat ≤ i ⟹ M(i) ==> nat ≤ |i|⇗M⇖"
apply (rule Card_rel_nat [THEN Card_rel_cardinal_rel_eq, THEN subst], simp_all)
apply (erule cardinal_rel_mono, simp_all)
done

lemma n_lesspoll_rel_nat: "n ∈ nat ==> n ≺⇗M⇖ nat"
by (blast intro: Card_rel_nat ltI lt_Card_rel_imp_lesspoll_rel)

lemma cons_lepoll_rel_cong:
"[| A ≲⇗M⇖ B;  b ∉ B; M(A); M(B); M(b); M(a) |] ==> cons(a,A) ≲⇗M⇖ cons(b,B)"
apply (subst (asm) def_lepoll_rel, simp_all, subst def_lepoll_rel, simp_all, safe)
apply (rule_tac x = "λy∈cons (a,A) . if y=a then b else f`y" in rexI)
apply (rule_tac d = "%z. if z ∈ B then converse (f) `z else a" in lam_injective)
apply (safe elim!: consE')
apply simp_all
apply (blast intro: inj_is_fun [THEN apply_type])+
apply (auto intro:lam_closed lam_if_then_replacement simp add:transM[of _ A])
done

lemma cons_eqpoll_rel_cong:
"[| A ≈⇗M⇖ B;  a ∉ A;  b ∉ B;  M(A); M(B); M(a) ; M(b) |] ==> cons(a,A) ≈⇗M⇖ cons(b,B)"

lemma cons_lepoll_rel_cons_iff:
"[| a ∉ A;  b ∉ B; M(a); M(A); M(b); M(B) |] ==> cons(a,A) ≲⇗M⇖ cons(b,B)  ⟷  A ≲⇗M⇖ B"
by (blast intro: cons_lepoll_rel_cong cons_lepoll_rel_consD)

lemma cons_eqpoll_rel_cons_iff:
"[| a ∉ A;  b ∉ B; M(a); M(A); M(b); M(B) |] ==> cons(a,A) ≈⇗M⇖ cons(b,B)  ⟷  A ≈⇗M⇖ B"
by (blast intro: cons_eqpoll_rel_cong cons_eqpoll_rel_consD)

lemma singleton_eqpoll_rel_1: "M(a) ⟹ {a} ≈⇗M⇖ 1"
apply (unfold succ_def)
apply (blast intro!: eqpoll_rel_refl [THEN cons_eqpoll_rel_cong])
done

lemma cardinal_rel_singleton: "M(a) ⟹ |{a}|⇗M⇖ = 1"
apply (rule singleton_eqpoll_rel_1 [THEN cardinal_rel_cong, THEN trans])
apply (simp (no_asm) add: nat_into_Card_rel [THEN Card_rel_cardinal_rel_eq])
apply auto
done

lemma not_0_is_lepoll_rel_1: "A ≠ 0 ==> M(A) ⟹ 1 ≲⇗M⇖ A"
apply (erule not_emptyE)
apply (rule_tac a = "cons (x, A-{x}) " in subst)
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y ≲⇗M⇖ cons (x, A-{x})" in subst)
apply auto
proof -
fix x
assume "M(A)"
then
show "x ∈ A ⟹ {0} ≲⇗M⇖ cons(x, A - {x})"
by (auto intro: cons_lepoll_rel_cong transM[OF _ ‹M(A)›] subset_imp_lepoll_rel)
qed

lemma succ_eqpoll_rel_cong: "A ≈⇗M⇖ B ⟹ M(A) ⟹ M(B) ==> succ(A) ≈⇗M⇖ succ(B)"
apply (unfold succ_def)
done

text‹The next result was not straightforward to port, and even a
different statement was needed.›

lemma sum_bij_rel:
"[| f ∈ bij⇗M⇖(A,C); g ∈ bij⇗M⇖(B,D); M(f); M(A); M(C); M(g); M(B); M(D)|]
==> (λz∈A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) ∈ bij⇗M⇖(A+B, C+D)"
proof -
assume asm:"f ∈ bij⇗M⇖(A,C)" "g ∈ bij⇗M⇖(B,D)" "M(f)" "M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
then
have "M(λz∈A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›]
by (auto intro:case_replacement4[THEN lam_closed])
with asm
show ?thesis
apply simp
apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
in lam_bijective)
apply (auto simp add: left_inverse_bij right_inverse_bij)
done
qed

lemma sum_bij_rel':
assumes "f ∈ bij⇗M⇖(A,C)" "g ∈ bij⇗M⇖(B,D)" "M(f)"
"M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
shows
"(λz∈A+B. case(λx. Inl(f`x), λy. Inr(g`y), z)) ∈ bij(A+B, C+D)"
"M(λz∈A+B. case(λx. Inl(f`x), λy. Inr(g`y), z))"
proof -
from assms
show "M(λz∈A+B. case(λx. Inl(f`x), λy. Inr(g`y), z))"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›]
by (auto intro:case_replacement4[THEN lam_closed])
with assms
show "(λz∈A+B. case(λx. Inl(f`x), λy. Inr(g`y), z)) ∈ bij(A+B, C+D)"
apply simp
apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))"
in lam_bijective)
apply (auto simp add: left_inverse_bij right_inverse_bij)
done
qed

lemma sum_eqpoll_rel_cong:
assumes "A ≈⇗M⇖ C" "B ≈⇗M⇖ D" "M(A)" "M(C)" "M(B)" "M(D)"
shows "A+B ≈⇗M⇖ C+D"
using assms
proof (simp add: def_eqpoll_rel, safe, rename_tac g)
fix f g
assume  "M(f)" "f ∈ bij(A, C)" "M(g)" "g ∈ bij(B, D)"
with assms
obtain h where "h∈bij(A+B, C+D)" "M(h)"
using sum_bij_rel'[of f A C g B D] by simp
then
show "∃f[M]. f ∈ bij(A + B, C + D)"
by auto
qed

lemma prod_bij_rel':
assumes "f ∈ bij⇗M⇖(A,C)" "g ∈ bij⇗M⇖(B,D)" "M(f)"
"M(A)" "M(C)" "M(g)" "M(B)" "M(D)"
shows
"(λ<x,y>∈A*B. <f`x, g`y>) ∈ bij(A*B, C*D)"
"M(λ<x,y>∈A*B. <f`x, g`y>)"
proof -
from assms
show "M((λ<x,y>∈A*B. <f`x, g`y>))"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›]
transM[OF _ cartprod_closed, of _ A B]
by (auto intro:prod_fun_replacement[THEN lam_closed, of f g "A×B"])
with assms
show "(λ<x,y>∈A*B. <f`x, g`y>) ∈ bij(A*B, C*D)"
apply simp
apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>"
in lam_bijective)
apply (auto simp add: left_inverse_bij right_inverse_bij)
done
qed

lemma prod_eqpoll_rel_cong:
assumes "A ≈⇗M⇖ C" "B ≈⇗M⇖ D" "M(A)" "M(C)" "M(B)" "M(D)"
shows "A×B ≈⇗M⇖ C×D"
using assms
proof (simp add: def_eqpoll_rel, safe, rename_tac g)
fix f g
assume  "M(f)" "f ∈ bij(A, C)" "M(g)" "g ∈ bij(B, D)"
with assms
obtain h where "h∈bij(A×B, C×D)" "M(h)"
using prod_bij_rel'[of f A C g B D] by simp
then
show "∃f[M]. f ∈ bij(A × B, C × D)"
by auto
qed

lemma inj_rel_disjoint_eqpoll_rel:
"[| f ∈ inj⇗M⇖(A,B);  A ∩ B = 0;M(f); M(A);M(B) |] ==> A ∪ (B - range(f)) ≈⇗M⇖ B"
apply (rule rexI)
apply (rule_tac c = "%x. if x ∈ A then f`x else x"
and d = "%y. if y ∈ range (f) then converse (f) `y else y"
in lam_bijective)
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
apply (safe elim!: UnE')
apply (simp_all add: inj_is_fun [THEN apply_rangeI])
apply (blast intro: inj_converse_fun [THEN apply_type])
proof -
assume "f ∈ inj(A, B)" "A ∩ B = 0" "M(f)" "M(A)" "M(B)"
then
show "M(λx∈A ∪ (B - range(f)). if x ∈ A then f ` x else x)"
using  transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›]
lam_replacement_iff_lam_closed lam_if_then_replacement2
by auto
qed

lemma Diff_sing_lepoll_rel:
"[| a ∈ A;  A ≲⇗M⇖ succ(n); M(a); M(A); M(n) |] ==> A - {a} ≲⇗M⇖ n"
apply (unfold succ_def)
apply (rule cons_lepoll_rel_consD)
apply (rule_tac [3] mem_not_refl)
apply (erule cons_Diff [THEN ssubst], simp_all)
done

lemma lepoll_rel_Diff_sing:
assumes A: "succ(n) ≲⇗M⇖ A"
and types: "M(n)" "M(A)" "M(a)"
shows "n ≲⇗M⇖ A - {a}"
proof -
have "cons(n,n) ≲⇗M⇖ A" using A
by (unfold succ_def)
also from types
have "... ≲⇗M⇖ cons(a, A-{a})"
by (blast intro: subset_imp_lepoll_rel)
finally have "cons(n,n) ≲⇗M⇖ cons(a, A-{a})" by (simp_all add:types)
with types
show ?thesis
by (blast intro: cons_lepoll_rel_consD mem_irrefl)
qed

lemma Diff_sing_eqpoll_rel: "[| a ∈ A; A ≈⇗M⇖ succ(n); M(a); M(A); M(n) |] ==> A - {a} ≈⇗M⇖ n"
by (blast intro!: eqpoll_relI
elim!: eqpoll_relE
intro: Diff_sing_lepoll_rel lepoll_rel_Diff_sing)

lemma lepoll_rel_1_is_sing: "[| A ≲⇗M⇖ 1; a ∈ A ;M(a); M(A) |] ==> A = {a}"
apply (frule Diff_sing_lepoll_rel, assumption+, simp)
apply (drule lepoll_rel_0_is_0, simp)
apply (blast elim: equalityE)
done

lemma Un_lepoll_rel_sum: "M(A) ⟹ M(B) ⟹ A ∪ B ≲⇗M⇖ A+B"
apply (rule_tac x = "λx∈A ∪ B. if x∈A then Inl (x) else Inr (x)" in rexI)
apply (rule_tac d = "%z. snd (z)" in lam_injective)
apply force
proof -
assume "M(A)" "M(B)"
then
show "M(λx∈A ∪ B. if x ∈ A then Inl(x) else Inr(x))"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›] if_then_Inj_replacement
by (rule_tac lam_closed) auto
qed

lemma well_ord_Un_M:
assumes "well_ord(X,R)" "well_ord(Y,S)"
and types: "M(X)" "M(R)" "M(Y)" "M(S)"
shows "∃T[M]. well_ord(X ∪ Y, T)"
using assms
by (erule_tac well_ord_radd [THEN [3] Un_lepoll_rel_sum [THEN lepoll_rel_well_ord]])

lemma disj_Un_eqpoll_rel_sum: "M(A) ⟹ M(B) ⟹ A ∩ B = 0 ⟹ A ∪ B ≈⇗M⇖ A + B"
apply (rule_tac x = "λa∈A ∪ B. if a ∈ A then Inl (a) else Inr (a)" in rexI)
apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
apply auto
proof -
assume "M(A)" "M(B)"
then
show "M(λx∈A ∪ B. if x ∈ A then Inl(x) else Inr(x))"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›] if_then_Inj_replacement
by (rule_tac lam_closed) auto
qed

lemma eqpoll_rel_imp_Finite_rel_iff: "A ≈⇗M⇖ B ==> M(A) ⟹ M(B) ⟹ Finite_rel(M,A) ⟷ Finite_rel(M,B)"
apply (unfold Finite_rel_def)
apply (blast intro: eqpoll_rel_trans eqpoll_rel_sym)
done

― ‹It seems reasonable to have the absoluteness of \<^term>‹Finite› here,
and deduce the rest of the results from this.

Perhaps modularize that proof to have absoluteness of injections and
bijections of finite sets (cf. @{thm [source] lesspoll_rel_succ_imp_lepoll_rel}.›

lemma Finite_abs[simp]:
assumes "M(A)"
shows "Finite_rel(M,A) ⟷ Finite(A)"
unfolding Finite_rel_def Finite_def
proof (simp, intro iffI)
assume "∃n∈nat. A ≈⇗M⇖ n"
then
obtain n where "A ≈⇗M⇖ n" "n∈nat" by blast
with assms
show "∃n∈nat. A ≈ n"
unfolding eqpoll_def using nat_into_M by (auto simp add:def_eqpoll_rel)
next
fix n
assume "∃n∈nat. A ≈ n"
then
obtain n where "A ≈ n" "n∈nat" by blast
moreover from this
obtain f where "f ∈ bij(A,n)" unfolding eqpoll_def by auto
moreover
note assms
moreover from calculation
have "converse(f) ∈ n→A"  using bij_is_fun by simp
moreover from calculation
have "M(converse(f))" using transM[of _ "n→A"] by simp
moreover from calculation
have "M(f)" using bij_is_fun
fun_is_rel[of "f" A "λ_. n", THEN converse_converse]
converse_closed[of "converse(f)"] by simp
ultimately
show "∃n∈nat. A ≈⇗M⇖ n"
qed

― ‹From the next result, the relative versions of
@{thm [source] Finite_Fin_lemma} and @{thm [source] Fin_lemma} should follow›

lemma lepoll_rel_nat_imp_Finite_rel:
assumes A: "A ≲⇗M⇖ n" and n: "n ∈ nat"
and types: "M(A)" "M(n)"
shows "Finite_rel(M,A)"
proof -
have "A ≲⇗M⇖ n ⟹ Finite_rel(M,A)" using n
proof (induct n)
case 0
hence "A = 0" by (rule lepoll_rel_0_is_0, simp_all add:types)
thus ?case by simp
next
case (succ n)
hence "A ≲⇗M⇖ n ∨ A ≈⇗M⇖ succ(n)" by (blast dest: lepoll_rel_succ_disj intro:types)
thus ?case using succ by (auto simp add: Finite_rel_def types)
qed
thus ?thesis using A .
qed

lemma lesspoll_rel_nat_is_Finite_rel:
"A ≺⇗M⇖ nat ⟹ M(A) ⟹ Finite_rel(M,A)"
apply (unfold Finite_rel_def)
apply (auto dest: ltD lesspoll_rel_cardinal_rel_lt
lesspoll_rel_imp_eqpoll_rel [THEN eqpoll_rel_sym])
done

lemma lepoll_rel_Finite_rel:
assumes Y: "Y ≲⇗M⇖ X" and X: "Finite_rel(M,X)"
and types:"M(Y)" "M(X)"
shows "Finite_rel(M,Y)"
proof -
obtain n where n: "n ∈ nat" "X ≈⇗M⇖ n" "M(n)" using X
have "Y ≲⇗M⇖ X"         by (rule Y)
also have "... ≈⇗M⇖ n"  by (rule n)
finally have "Y ≲⇗M⇖ n" by (simp_all add:types ‹M(n)›)
thus ?thesis using n
by (simp add: lepoll_rel_nat_imp_Finite_rel types ‹M(n)› del:Finite_abs)
qed

lemma succ_lepoll_rel_imp_not_empty: "succ(x) ≲⇗M⇖ y ==> M(x) ⟹ M(y) ⟹ y ≠ 0"
by (fast dest!: lepoll_rel_0_is_0)

lemma eqpoll_rel_succ_imp_not_empty: "x ≈⇗M⇖ succ(n) ==> M(x) ⟹ M(n) ⟹ x ≠ 0"
by (fast elim!: eqpoll_rel_sym [THEN eqpoll_rel_0_is_0, THEN succ_neq_0])

lemma Finite_subset_closed:
assumes "Finite(B)" "B⊆A" "M(A)"
shows "M(B)"
proof -
from ‹Finite(B)› ‹B⊆A›
show ?thesis
proof(induct,simp)
case (cons x D)
with assms
have "M(D)" "x∈A"
unfolding cons_def by auto
then
show ?case using transM[OF _ ‹M(A)›] by simp
qed
qed

lemma Finite_Pow_abs:
assumes "Finite(A)" " M(A)"
shows "Pow(A) = Pow_rel(M,A)"
using Finite_subset_closed[OF subset_Finite] assms Pow_rel_char
by auto

lemma Finite_Pow_rel:
assumes "Finite(A)" "M(A)"
shows "Finite(Pow_rel(M,A))"
using Finite_Pow Finite_Pow_abs[symmetric] assms by simp

lemma Pow_rel_0 [simp]: "Pow_rel(M,0) = {0}"
using Finite_Pow_abs[of 0] by simp

lemma eqpoll_rel_imp_Finite: "A ≈⇗M⇖ B ⟹ Finite(A) ⟹ M(A) ⟹ M(B) ⟹ Finite(B)"
proof -
assume "A ≈⇗M⇖ B" "Finite(A)" "M(A)" "M(B)"
then obtain f n g where "f∈bij(A,B)" "n∈nat" "g∈bij(A,n)"
unfolding Finite_def eqpoll_def eqpoll_rel_def
using bij_rel_char
by auto
then
have "g O converse(f) ∈ bij(B,n)"
using bij_converse_bij comp_bij by simp
with ‹n∈_›
show"Finite(B)"
unfolding Finite_def eqpoll_def by auto
qed

lemma eqpoll_rel_imp_Finite_iff: "A ≈⇗M⇖ B ⟹ M(A) ⟹ M(B) ⟹ Finite(A) ⟷ Finite(B)"
using eqpoll_rel_imp_Finite eqpoll_rel_sym by force

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

end```