Theory Cardinal_Relative
section‹Relative, Choice-less Cardinal Numbers›
theory Cardinal_Relative
imports
ZF_Miscellanea
Discipline_Cardinal
Lambda_Replacement
begin
hide_const (open) L
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)"
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
locale M_cardinals= M_ordertype + M_trancl + M_Perm + M_replacement_extra +
assumes
rvimage_separation: "M(f) ⟹ M(r) ⟹
separation(M, λz. ∃x y. z = ⟨x, y⟩ ∧ ⟨f ` x, f ` y⟩ ∈ r)"
and
radd_separation: "M(R) ⟹ M(S) ⟹
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))"
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))"
begin
lemma radd_closed [intro,simp]: "M(a) ⟹ M(b) ⟹ M(c) ⟹ M(d) ⟹ M(radd(a,b,c,d))"
using radd_separation by (auto simp add: radd_def)
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
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
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)"
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
by(rule_tac nat_induct[OF that],simp_all add:banach_functor_closed)
with assms
show ?thesis
using family_union_closed'[OF banach_repl_iter M_nat] lfp_banach_functor
by simp
qed
lemma banach_decomposition_rel :
"[| 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]
unfolding banach_functor_def by simp_all
lemma schroeder_bernstein_closed :
"[| 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])
apply (simp add: inj_is_fun)
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
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 [simp]: "⟦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 [simp]: "⟦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
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 id_closed : "M(A) ⟹ M(id(A))"
using lam_replacement_identity lam_replacement_iff_lam_closed
unfolding id_def by simp
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)
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 def_eqpoll_rel using schroeder_bernstein_closed
by auto
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)
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\_rel: contributions by Krzysztof Grabczewski›
lemma lesspoll_rel_not_refl : "M(i) ⟹ ~ (i ≺⇗M⇖ i)"
by (simp add: lesspoll_rel_def eqpoll_rel_refl)
lemma lesspoll_rel_irrefl : "i ≺⇗M⇖ i ==> M(i) ⟹ P"
by (simp add: lesspoll_rel_def eqpoll_rel_refl)
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
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
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)"
by (auto simp add: def_surj_rel)
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)"
by (simp add: def_inj_rel) blast
qed
qed
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
lemma cardinal_rel_cong : "X ≈⇗M⇖ Y ⟹ M(X) ⟹ M(Y) ⟹ |X|⇗M⇖ = |Y|⇗M⇖"
apply (simp add: def_eqpoll_rel cardinal_rel_def)
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››
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
using Least_0[of "λi. M(i) ∧ i ≈⇗M⇖ A"] Card_rel_0
by fastforce
next
case True
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)
qed (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
by (simp add: lt_Ord)
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⇖" .
thus ?thesis by (simp add:types)
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)
thus ?thesis by (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 (auto simp add: lt_def)
apply (blast intro: Ord_trans)
done
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)
apply (rule if_type [THEN lam_type])
apply (blast dest: apply_funtype)
apply (blast elim!: mem_irrefl dest: apply_funtype)
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 (simp add: eqpoll_rel_iff)
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
by (simp add: def_lepoll_rel inj_def)
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)
apply (simp add: eqpoll_rel_refl)
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 (simp add: def_lepoll_rel def_eqpoll_rel)
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+)
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"
by (simp add: lt_def lt_not_lepoll_rel)
hence False using i
by (simp add: eqpoll_rel_iff)
}
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)"
by (simp add: eqpoll_rel_iff cons_lepoll_rel_cong)
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)
apply (simp add: cons_eqpoll_rel_cong mem_not_refl)
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 (typecheck add: bij_is_inj inj_is_fun)
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 (typecheck add: bij_is_inj inj_is_fun)
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 (typecheck add: bij_is_inj inj_is_fun)
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 (simp add: def_eqpoll_rel)
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 (simp add: def_lepoll_rel)
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
apply (simp add: Inl_def Inr_def)
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]])
(auto simp add: types)
lemma disj_Un_eqpoll_rel_sum : "M(A) ⟹ M(B) ⟹ A ∩ B = 0 ⟹ A ∪ B ≈⇗M⇖ A + B"
apply (simp add: def_eqpoll_rel)
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
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"
by (force dest:nat_into_M simp add:def_eqpoll_rel)
qed
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
by (auto simp add: Finite_rel_def)
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
end
end