Theory HOL.BNF_Cardinal_Order_Relation
section ‹Cardinal-Order Relations as Needed by Bounded Natural Functors›
theory BNF_Cardinal_Order_Relation
imports Zorn BNF_Wellorder_Constructions
begin
text‹In this section, we define cardinal-order relations to be minim well-orders
on their field. Then we define the cardinal of a set to be {\em some} cardinal-order
relation on that set, which will be unique up to order isomorphism. Then we study
the connection between cardinals and:
\begin{itemize}
\item standard set-theoretic constructions: products,
sums, unions, lists, powersets, set-of finite sets operator;
\item finiteness and infiniteness (in particular, with the numeric cardinal operator
for finite sets, ‹card›, from the theory ‹Finite_Sets.thy›).
\end{itemize}
%
On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also
define (again, up to order isomorphism) the successor of a cardinal, and show that
any cardinal admits a successor.
Main results of this section are the existence of cardinal relations and the
facts that, in the presence of infiniteness,
most of the standard set-theoretic constructions (except for the powerset)
{\em do not increase cardinality}. In particular, e.g., the set of words/lists over
any infinite set has the same cardinality (hence, is in bijection) with that set.
›
subsection ‹Cardinal orders›
text‹A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
order-embedding relation, ‹≤o› (which is the same as being {\em minimal} w.r.t. the
strict order-embedding relation, ‹<o›), among all the well-orders on its field.›
definition card_order_on :: "'a set ⇒ 'a rel ⇒ bool"
where
"card_order_on A r ≡ well_order_on A r ∧ (∀r'. well_order_on A r' ⟶ r ≤o r')"
abbreviation "Card_order r ≡ card_order_on (Field r) r"
abbreviation "card_order r ≡ card_order_on UNIV r"
lemma card_order_on_well_order_on:
assumes "card_order_on A r"
shows "well_order_on A r"
using assms unfolding card_order_on_def by simp
lemma card_order_on_Card_order:
"card_order_on A r ⟹ A = Field r ∧ Card_order r"
unfolding card_order_on_def using well_order_on_Field by blast
text‹The existence of a cardinal relation on any given set (which will mean
that any set has a cardinal) follows from two facts:
\begin{itemize}
\item Zermelo's theorem (proved in ‹Zorn.thy› as theorem ‹well_order_on›),
which states that on any given set there exists a well-order;
\item The well-founded-ness of ‹<o›, ensuring that then there exists a minimal
such well-order, i.e., a cardinal order.
\end{itemize}
›
theorem card_order_on: "∃r. card_order_on A r"
proof -
define R where "R ≡ {r. well_order_on A r}"
have "R ≠ {} ∧ (∀r ∈ R. Well_order r)"
using well_order_on[of A] R_def well_order_on_Well_order by blast
with exists_minim_Well_order[of R] show ?thesis
by (auto simp: R_def card_order_on_def)
qed
lemma card_order_on_ordIso:
assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
shows "r =o r'"
using assms unfolding card_order_on_def
using ordIso_iff_ordLeq by blast
lemma Card_order_ordIso:
assumes CO: "Card_order r" and ISO: "r' =o r"
shows "Card_order r'"
using ISO unfolding ordIso_def
proof(unfold card_order_on_def, auto)
fix p' assume "well_order_on (Field r') p'"
hence 0: "Well_order p' ∧ Field p' = Field r'"
using well_order_on_Well_order by blast
obtain f where 1: "iso r' r f" and 2: "Well_order r ∧ Well_order r'"
using ISO unfolding ordIso_def by auto
hence 3: "inj_on f (Field r') ∧ f ` (Field r') = Field r"
by (auto simp add: iso_iff embed_inj_on)
let ?p = "dir_image p' f"
have 4: "p' =o ?p ∧ Well_order ?p"
using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
moreover have "Field ?p = Field r"
using 0 3 by (auto simp add: dir_image_Field)
ultimately have "well_order_on (Field r) ?p" by auto
hence "r ≤o ?p" using CO unfolding card_order_on_def by auto
thus "r' ≤o p'"
using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
qed
lemma Card_order_ordIso2:
assumes CO: "Card_order r" and ISO: "r =o r'"
shows "Card_order r'"
using assms Card_order_ordIso ordIso_symmetric by blast
subsection ‹Cardinal of a set›
text‹We define the cardinal of set to be {\em some} cardinal order on that set.
We shall prove that this notion is unique up to order isomorphism, meaning
that order isomorphism shall be the true identity of cardinals.›
definition card_of :: "'a set ⇒ 'a rel" ("|_|" )
where "card_of A = (SOME r. card_order_on A r)"
lemma card_of_card_order_on: "card_order_on A |A|"
unfolding card_of_def by (auto simp add: card_order_on someI_ex)
lemma card_of_well_order_on: "well_order_on A |A|"
using card_of_card_order_on card_order_on_def by blast
lemma Field_card_of: "Field |A| = A"
using card_of_card_order_on[of A] unfolding card_order_on_def
using well_order_on_Field by blast
lemma card_of_Card_order: "Card_order |A|"
by (simp only: card_of_card_order_on Field_card_of)
corollary ordIso_card_of_imp_Card_order:
"r =o |A| ⟹ Card_order r"
using card_of_Card_order Card_order_ordIso by blast
lemma card_of_Well_order: "Well_order |A|"
using card_of_Card_order unfolding card_order_on_def by auto
lemma card_of_refl: "|A| =o |A|"
using card_of_Well_order ordIso_reflexive by blast
lemma card_of_least: "well_order_on A r ⟹ |A| ≤o r"
using card_of_card_order_on unfolding card_order_on_def by blast
lemma card_of_ordIso:
"(∃f. bij_betw f A B) = ( |A| =o |B| )"
proof(auto)
fix f assume *: "bij_betw f A B"
then obtain r where "well_order_on B r ∧ |A| =o r"
using Well_order_iso_copy card_of_well_order_on by blast
hence "|B| ≤o |A|" using card_of_least
ordLeq_ordIso_trans ordIso_symmetric by blast
moreover
{let ?g = "inv_into A f"
have "bij_betw ?g B A" using * bij_betw_inv_into by blast
then obtain r where "well_order_on A r ∧ |B| =o r"
using Well_order_iso_copy card_of_well_order_on by blast
hence "|A| ≤o |B|"
using card_of_least ordLeq_ordIso_trans ordIso_symmetric by blast
}
ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
next
assume "|A| =o |B|"
then obtain f where "iso ( |A| ) ( |B| ) f"
unfolding ordIso_def by auto
hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
thus "∃f. bij_betw f A B" by auto
qed
lemma card_of_ordLeq:
"(∃f. inj_on f A ∧ f ` A ≤ B) = ( |A| ≤o |B| )"
proof(auto)
fix f assume *: "inj_on f A" and **: "f ` A ≤ B"
{assume "|B| <o |A|"
hence "|B| ≤o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
then obtain g where "embed ( |B| ) ( |A| ) g"
unfolding ordLeq_def by auto
hence 1: "inj_on g B ∧ g ` B ≤ A" using embed_inj_on[of "|B|" "|A|" "g"]
card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
embed_Field[of "|B|" "|A|" g] by auto
obtain h where "bij_betw h A B"
using * ** 1 Schroeder_Bernstein[of f] by fastforce
hence "|A| ≤o |B|" using card_of_ordIso ordIso_iff_ordLeq by auto
}
thus "|A| ≤o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
by (auto simp: card_of_Well_order)
next
assume *: "|A| ≤o |B|"
obtain f where "embed |A| |B| f"
using * unfolding ordLeq_def by auto
hence "inj_on f A ∧ f ` A ≤ B"
using embed_inj_on[of "|A|" "|B|"] card_of_Well_order embed_Field[of "|A|" "|B|"]
by (auto simp: Field_card_of)
thus "∃f. inj_on f A ∧ f ` A ≤ B" by auto
qed
lemma card_of_ordLeq2:
"A ≠ {} ⟹ (∃g. g ` B = A) = ( |A| ≤o |B| )"
using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
lemma card_of_ordLess:
"(¬(∃f. inj_on f A ∧ f ` A ≤ B)) = ( |B| <o |A| )"
proof -
have "(¬(∃f. inj_on f A ∧ f ` A ≤ B)) = (¬ |A| ≤o |B| )"
using card_of_ordLeq by blast
also have "… = ( |B| <o |A| )"
using not_ordLeq_iff_ordLess by (auto intro: card_of_Well_order)
finally show ?thesis .
qed
lemma card_of_ordLess2:
"B ≠ {} ⟹ (¬(∃f. f ` A = B)) = ( |A| <o |B| )"
using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
lemma card_of_ordIsoI:
assumes "bij_betw f A B"
shows "|A| =o |B|"
using assms unfolding card_of_ordIso[symmetric] by auto
lemma card_of_ordLeqI:
assumes "inj_on f A" and "⋀ a. a ∈ A ⟹ f a ∈ B"
shows "|A| ≤o |B|"
using assms unfolding card_of_ordLeq[symmetric] by auto
lemma card_of_unique:
"card_order_on A r ⟹ r =o |A|"
by (simp only: card_order_on_ordIso card_of_card_order_on)
lemma card_of_mono1:
"A ≤ B ⟹ |A| ≤o |B|"
using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
lemma card_of_mono2:
assumes "r ≤o r'"
shows "|Field r| ≤o |Field r'|"
proof -
obtain f where
1: "well_order_on (Field r) r ∧ well_order_on (Field r) r ∧ embed r r' f"
using assms unfolding ordLeq_def
by (auto simp add: well_order_on_Well_order)
hence "inj_on f (Field r) ∧ f ` (Field r) ≤ Field r'"
by (auto simp add: embed_inj_on embed_Field)
thus "|Field r| ≤o |Field r'|" using card_of_ordLeq by blast
qed
lemma card_of_cong: "r =o r' ⟹ |Field r| =o |Field r'|"
by (simp add: ordIso_iff_ordLeq card_of_mono2)
lemma card_of_Field_ordIso:
assumes "Card_order r"
shows "|Field r| =o r"
proof -
have "card_order_on (Field r) r"
using assms card_order_on_Card_order by blast
moreover have "card_order_on (Field r) |Field r|"
using card_of_card_order_on by blast
ultimately show ?thesis using card_order_on_ordIso by blast
qed
lemma Card_order_iff_ordIso_card_of:
"Card_order r = (r =o |Field r| )"
using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
lemma Card_order_iff_ordLeq_card_of:
"Card_order r = (r ≤o |Field r| )"
proof -
have "Card_order r = (r =o |Field r| )"
unfolding Card_order_iff_ordIso_card_of by simp
also have "… = (r ≤o |Field r| ∧ |Field r| ≤o r)"
unfolding ordIso_iff_ordLeq by simp
also have "… = (r ≤o |Field r| )"
using card_of_least
by (auto simp: card_of_least ordLeq_Well_order_simp)
finally show ?thesis .
qed
lemma Card_order_iff_Restr_underS:
assumes "Well_order r"
shows "Card_order r = (∀a ∈ Field r. Restr r (underS r a) <o |Field r| )"
using assms ordLeq_iff_ordLess_Restr card_of_Well_order
unfolding Card_order_iff_ordLeq_card_of by blast
lemma card_of_underS:
assumes r: "Card_order r" and a: "a ∈ Field r"
shows "|underS r a| <o r"
proof -
let ?A = "underS r a" let ?r' = "Restr r ?A"
have 1: "Well_order r"
using r unfolding card_order_on_def by simp
have "Well_order ?r'" using 1 Well_order_Restr by auto
with card_of_card_order_on have "|Field ?r'| ≤o ?r'"
unfolding card_order_on_def by auto
moreover have "Field ?r' = ?A"
using 1 wo_rel.underS_ofilter Field_Restr_ofilter
unfolding wo_rel_def by fastforce
ultimately have "|?A| ≤o ?r'" by simp
also have "?r' <o |Field r|"
using 1 a r Card_order_iff_Restr_underS by blast
also have "|Field r| =o r"
using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
finally show ?thesis .
qed
lemma ordLess_Field:
assumes "r <o r'"
shows "|Field r| <o r'"
proof -
have "well_order_on (Field r) r" using assms unfolding ordLess_def
by (auto simp add: well_order_on_Well_order)
hence "|Field r| ≤o r" using card_of_least by blast
thus ?thesis using assms ordLeq_ordLess_trans by blast
qed
lemma internalize_card_of_ordLeq:
"( |A| ≤o r) = (∃B ≤ Field r. |A| =o |B| ∧ |B| ≤o r)"
proof
assume "|A| ≤o r"
then obtain p where 1: "Field p ≤ Field r ∧ |A| =o p ∧ p ≤o r"
using internalize_ordLeq[of "|A|" r] by blast
hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
hence "|Field p| =o p" using card_of_Field_ordIso by blast
hence "|A| =o |Field p| ∧ |Field p| ≤o r"
using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
thus "∃B ≤ Field r. |A| =o |B| ∧ |B| ≤o r" using 1 by blast
next
assume "∃B ≤ Field r. |A| =o |B| ∧ |B| ≤o r"
thus "|A| ≤o r" using ordIso_ordLeq_trans by blast
qed
lemma internalize_card_of_ordLeq2:
"( |A| ≤o |C| ) = (∃B ≤ C. |A| =o |B| ∧ |B| ≤o |C| )"
using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
subsection ‹Cardinals versus set operations on arbitrary sets›
text‹Here we embark in a long journey of simple results showing
that the standard set-theoretic operations are well-behaved w.r.t. the notion of
cardinal -- essentially, this means that they preserve the ``cardinal identity"
‹=o› and are monotonic w.r.t. ‹≤o›.
›
lemma card_of_empty: "|{}| ≤o |A|"
using card_of_ordLeq inj_on_id by blast
lemma card_of_empty1:
assumes "Well_order r ∨ Card_order r"
shows "|{}| ≤o r"
proof -
have "Well_order r" using assms unfolding card_order_on_def by auto
hence "|Field r| ≤o r"
using assms card_of_least by blast
moreover have "|{}| ≤o |Field r|" by (simp add: card_of_empty)
ultimately show ?thesis using ordLeq_transitive by blast
qed
corollary Card_order_empty:
"Card_order r ⟹ |{}| ≤o r" by (simp add: card_of_empty1)
lemma card_of_empty2:
assumes "|A| =o |{}|"
shows "A = {}"
using assms card_of_ordIso[of A] bij_betw_empty2 by blast
lemma card_of_empty3:
assumes "|A| ≤o |{}|"
shows "A = {}"
using assms
by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
ordLeq_Well_order_simp)
lemma card_of_empty_ordIso:
"|{}::'a set| =o |{}::'b set|"
using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
lemma card_of_image:
"|f ` A| ≤o |A|"
proof(cases "A = {}")
case False
hence "f ` A ≠ {}" by auto
thus ?thesis
using card_of_ordLeq2[of "f ` A" A] by auto
qed (simp add: card_of_empty)
lemma surj_imp_ordLeq:
assumes "B ⊆ f ` A"
shows "|B| ≤o |A|"
proof -
have "|B| ≤o |f ` A|" using assms card_of_mono1 by auto
thus ?thesis using card_of_image ordLeq_transitive by blast
qed
lemma card_of_singl_ordLeq:
assumes "A ≠ {}"
shows "|{b}| ≤o |A|"
proof -
obtain a where *: "a ∈ A" using assms by auto
let ?h = "λ b'::'b. if b' = b then a else undefined"
have "inj_on ?h {b} ∧ ?h ` {b} ≤ A"
using * unfolding inj_on_def by auto
thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
qed
corollary Card_order_singl_ordLeq:
"⟦Card_order r; Field r ≠ {}⟧ ⟹ |{b}| ≤o r"
using card_of_singl_ordLeq[of "Field r" b]
card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
lemma card_of_Pow: "|A| <o |Pow A|"
using card_of_ordLess2[of "Pow A" A] Cantors_theorem[of A]
Pow_not_empty[of A] by auto
corollary Card_order_Pow:
"Card_order r ⟹ r <o |Pow(Field r)|"
using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
lemma card_of_Plus1: "|A| ≤o |A <+> B|" and card_of_Plus2: "|B| ≤o |A <+> B|"
using card_of_ordLeq by force+
corollary Card_order_Plus1:
"Card_order r ⟹ r ≤o |(Field r) <+> B|"
using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
corollary Card_order_Plus2:
"Card_order r ⟹ r ≤o |A <+> (Field r)|"
using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
proof -
have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by auto
qed
lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
proof -
have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by auto
qed
lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
proof -
let ?f = "λc. case c of Inl a ⇒ Inr a | Inr b ⇒ Inl b"
have "bij_betw ?f (A <+> B) (B <+> A)"
unfolding bij_betw_def inj_on_def by force
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_assoc:
fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
proof -
define f :: "('a + 'b) + 'c ⇒ 'a + 'b + 'c"
where [abs_def]: "f k =
(case k of
Inl ab ⇒
(case ab of
Inl a ⇒ Inl a
| Inr b ⇒ Inr (Inl b))
| Inr c ⇒ Inr (Inr c))"
for k
have "A <+> B <+> C ⊆ f ` ((A <+> B) <+> C)"
proof
fix x assume x: "x ∈ A <+> B <+> C"
show "x ∈ f ` ((A <+> B) <+> C)"
proof(cases x)
case (Inl a)
hence "a ∈ A" "x = f (Inl (Inl a))"
using x unfolding f_def by auto
thus ?thesis by auto
next
case (Inr bc) with x show ?thesis
by (cases bc) (force simp: f_def)+
qed
qed
hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
unfolding bij_betw_def inj_on_def f_def by fastforce
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_mono1:
assumes "|A| ≤o |B|"
shows "|A <+> C| ≤o |B <+> C|"
proof -
obtain f where f: "inj_on f A ∧ f ` A ≤ B"
using assms card_of_ordLeq[of A] by fastforce
define g where "g ≡ λd. case d of Inl a ⇒ Inl(f a) | Inr (c::'c) ⇒ Inr c"
have "inj_on g (A <+> C) ∧ g ` (A <+> C) ≤ (B <+> C)"
using f unfolding inj_on_def g_def by force
thus ?thesis using card_of_ordLeq by blast
qed
corollary ordLeq_Plus_mono1:
assumes "r ≤o r'"
shows "|(Field r) <+> C| ≤o |(Field r') <+> C|"
using assms card_of_mono2 card_of_Plus_mono1 by blast
lemma card_of_Plus_mono2:
assumes "|A| ≤o |B|"
shows "|C <+> A| ≤o |C <+> B|"
using card_of_Plus_mono1[OF assms]
by (blast intro: card_of_Plus_commute ordIso_ordLeq_trans ordLeq_ordIso_trans)
corollary ordLeq_Plus_mono2:
assumes "r ≤o r'"
shows "|A <+> (Field r)| ≤o |A <+> (Field r')|"
using assms card_of_mono2 card_of_Plus_mono2 by blast
lemma card_of_Plus_mono:
assumes "|A| ≤o |B|" and "|C| ≤o |D|"
shows "|A <+> C| ≤o |B <+> D|"
using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
ordLeq_transitive by blast
corollary ordLeq_Plus_mono:
assumes "r ≤o r'" and "p ≤o p'"
shows "|(Field r) <+> (Field p)| ≤o |(Field r') <+> (Field p')|"
using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
lemma card_of_Plus_cong1:
assumes "|A| =o |B|"
shows "|A <+> C| =o |B <+> C|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
corollary ordIso_Plus_cong1:
assumes "r =o r'"
shows "|(Field r) <+> C| =o |(Field r') <+> C|"
using assms card_of_cong card_of_Plus_cong1 by blast
lemma card_of_Plus_cong2:
assumes "|A| =o |B|"
shows "|C <+> A| =o |C <+> B|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
corollary ordIso_Plus_cong2:
assumes "r =o r'"
shows "|A <+> (Field r)| =o |A <+> (Field r')|"
using assms card_of_cong card_of_Plus_cong2 by blast
lemma card_of_Plus_cong:
assumes "|A| =o |B|" and "|C| =o |D|"
shows "|A <+> C| =o |B <+> D|"
using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
corollary ordIso_Plus_cong:
assumes "r =o r'" and "p =o p'"
shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
lemma card_of_Un_Plus_ordLeq:
"|A ∪ B| ≤o |A <+> B|"
proof -
let ?f = "λ c. if c ∈ A then Inl c else Inr c"
have "inj_on ?f (A ∪ B) ∧ ?f ` (A ∪ B) ≤ A <+> B"
unfolding inj_on_def by auto
thus ?thesis using card_of_ordLeq by blast
qed
lemma card_of_Times1:
assumes "A ≠ {}"
shows "|B| ≤o |B × A|"
proof(cases "B = {}")
case False
have "fst `(B × A) = B" using assms by auto
thus ?thesis using inj_on_iff_surj[of B "B × A"]
card_of_ordLeq False by blast
qed (simp add: card_of_empty)
lemma card_of_Times_commute: "|A × B| =o |B × A|"
proof -
have "bij_betw (λ(a,b). (b,a)) (A × B) (B × A)"
unfolding bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Times2:
assumes "A ≠ {}" shows "|B| ≤o |A × B|"
using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
ordLeq_ordIso_trans by blast
corollary Card_order_Times1:
"⟦Card_order r; B ≠ {}⟧ ⟹ r ≤o |(Field r) × B|"
using card_of_Times1[of B] card_of_Field_ordIso
ordIso_ordLeq_trans ordIso_symmetric by blast
corollary Card_order_Times2:
"⟦Card_order r; A ≠ {}⟧ ⟹ r ≤o |A × (Field r)|"
using card_of_Times2[of A] card_of_Field_ordIso
ordIso_ordLeq_trans ordIso_symmetric by blast
lemma card_of_Times3: "|A| ≤o |A × A|"
using card_of_Times1[of A]
by(cases "A = {}", simp add: card_of_empty)
lemma card_of_Plus_Times_bool: "|A <+> A| =o |A × (UNIV::bool set)|"
proof -
let ?f = "λc::'a + 'a. case c of Inl a ⇒ (a,True)
|Inr a ⇒ (a,False)"
have "bij_betw ?f (A <+> A) (A × (UNIV::bool set))"
proof -
have "⋀c1 c2. ?f c1 = ?f c2 ⟹ c1 = c2"
by (force split: sum.split_asm)
moreover
have "⋀c. c ∈ A <+> A ⟹ ?f c ∈ A × (UNIV::bool set)"
by (force split: sum.split_asm)
moreover
{fix a bl assume "(a,bl) ∈ A × (UNIV::bool set)"
hence "(a,bl) ∈ ?f ` ( A <+> A)"
by (cases bl) (force split: sum.split_asm)+
}
ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
qed
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Times_mono1:
assumes "|A| ≤o |B|"
shows "|A × C| ≤o |B × C|"
proof -
obtain f where f: "inj_on f A ∧ f ` A ≤ B"
using assms card_of_ordLeq[of A] by fastforce
define g where "g ≡ (λ(a,c::'c). (f a,c))"
have "inj_on g (A × C) ∧ g ` (A × C) ≤ (B × C)"
using f unfolding inj_on_def using g_def by auto
thus ?thesis using card_of_ordLeq by blast
qed
corollary ordLeq_Times_mono1:
assumes "r ≤o r'"
shows "|(Field r) × C| ≤o |(Field r') × C|"
using assms card_of_mono2 card_of_Times_mono1 by blast
lemma card_of_Times_mono2:
assumes "|A| ≤o |B|"
shows "|C × A| ≤o |C × B|"
using assms card_of_Times_mono1[of A B C]
by (blast intro: card_of_Times_commute ordIso_ordLeq_trans ordLeq_ordIso_trans)
corollary ordLeq_Times_mono2:
assumes "r ≤o r'"
shows "|A × (Field r)| ≤o |A × (Field r')|"
using assms card_of_mono2 card_of_Times_mono2 by blast
lemma card_of_Sigma_mono1:
assumes "∀i ∈ I. |A i| ≤o |B i|"
shows "|SIGMA i : I. A i| ≤o |SIGMA i : I. B i|"
proof -
have "∀i. i ∈ I ⟶ (∃f. inj_on f (A i) ∧ f ` (A i) ≤ B i)"
using assms by (auto simp add: card_of_ordLeq)
with choice[of "λ i f. i ∈ I ⟶ inj_on f (A i) ∧ f ` (A i) ≤ B i"]
obtain F where F: "∀i ∈ I. inj_on (F i) (A i) ∧ (F i) ` (A i) ≤ B i"
by atomize_elim (auto intro: bchoice)
define g where "g ≡ (λ(i,a::'b). (i,F i a))"
have "inj_on g (Sigma I A) ∧ g ` (Sigma I A) ≤ (Sigma I B)"
using F unfolding inj_on_def using g_def by force
thus ?thesis using card_of_ordLeq by blast
qed
lemma card_of_UNION_Sigma:
"|⋃i ∈ I. A i| ≤o |SIGMA i : I. A i|"
using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
lemma card_of_bool:
assumes "a1 ≠ a2"
shows "|UNIV::bool set| =o |{a1,a2}|"
proof -
let ?f = "λ bl. if bl then a1 else a2"
have "bij_betw ?f UNIV {a1,a2}"
proof -
have "⋀bl1 bl2. ?f bl1 = ?f bl2 ⟹ bl1 = bl2"
using assms by (force split: if_split_asm)
moreover
have "⋀bl. ?f bl ∈ {a1,a2}"
using assms by (force split: if_split_asm)
ultimately show ?thesis unfolding bij_betw_def inj_on_def by force
qed
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Plus_Times_aux:
assumes A2: "a1 ≠ a2 ∧ {a1,a2} ≤ A" and
LEQ: "|A| ≤o |B|"
shows "|A <+> B| ≤o |A × B|"
proof -
have 1: "|UNIV::bool set| ≤o |A|"
using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
by (blast intro: ordIso_ordLeq_trans)
have "|A <+> B| ≤o |B <+> B|"
using LEQ card_of_Plus_mono1 by blast
moreover have "|B <+> B| =o |B × (UNIV::bool set)|"
using card_of_Plus_Times_bool by blast
moreover have "|B × (UNIV::bool set)| ≤o |B × A|"
using 1 by (simp add: card_of_Times_mono2)
moreover have " |B × A| =o |A × B|"
using card_of_Times_commute by blast
ultimately show "|A <+> B| ≤o |A × B|"
by (blast intro: ordLeq_transitive dest: ordLeq_ordIso_trans)
qed
lemma card_of_Plus_Times:
assumes A2: "a1 ≠ a2 ∧ {a1,a2} ≤ A" and B2: "b1 ≠ b2 ∧ {b1,b2} ≤ B"
shows "|A <+> B| ≤o |A × B|"
proof -
{assume "|A| ≤o |B|"
hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
}
moreover
{assume "|B| ≤o |A|"
hence "|B <+> A| ≤o |B × A|"
using assms by (auto simp add: card_of_Plus_Times_aux)
hence ?thesis
using card_of_Plus_commute card_of_Times_commute
ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
}
ultimately show ?thesis
using card_of_Well_order[of A] card_of_Well_order[of B]
ordLeq_total[of "|A|"] by blast
qed
lemma card_of_Times_Plus_distrib:
"|A × (B <+> C)| =o |A × B <+> A × C|" (is "|?RHS| =o |?LHS|")
proof -
let ?f = "λ(a, bc). case bc of Inl b ⇒ Inl (a, b) | Inr c ⇒ Inr (a, c)"
have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_ordLeq_finite:
assumes "|A| ≤o |B|" and "finite B"
shows "finite A"
using assms unfolding ordLeq_def
using embed_inj_on[of "|A|" "|B|"] embed_Field[of "|A|" "|B|"]
Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
lemma card_of_ordLeq_infinite:
assumes "|A| ≤o |B|" and "¬ finite A"
shows "¬ finite B"
using assms card_of_ordLeq_finite by auto
lemma card_of_ordIso_finite:
assumes "|A| =o |B|"
shows "finite A = finite B"
using assms unfolding ordIso_def iso_def[abs_def]
by (auto simp: bij_betw_finite Field_card_of)
lemma card_of_ordIso_finite_Field:
assumes "Card_order r" and "r =o |A|"
shows "finite(Field r) = finite A"
using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
subsection ‹Cardinals versus set operations involving infinite sets›
text‹Here we show that, for infinite sets, most set-theoretic constructions
do not increase the cardinality. The cornerstone for this is
theorem ‹Card_order_Times_same_infinite›, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
at page 47 in \<^cite>‹"card-book"›. Then everything else follows fairly easily.›
lemma infinite_iff_card_of_nat:
"¬ finite A ⟷ ( |UNIV::nat set| ≤o |A| )"
unfolding infinite_iff_countable_subset card_of_ordLeq ..
text‹The next two results correspond to the ZF fact that all infinite cardinals are
limit ordinals:›
lemma Card_order_infinite_not_under:
assumes CARD: "Card_order r" and INF: "¬finite (Field r)"
shows "¬ (∃a. Field r = under r a)"
proof(auto)
have 0: "Well_order r ∧ wo_rel r ∧ Refl r"
using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
fix a assume *: "Field r = under r a"
show False
proof(cases "a ∈ Field r")
assume Case1: "a ∉ Field r"
hence "under r a = {}" unfolding Field_def under_def by auto
thus False using INF * by auto
next
let ?r' = "Restr r (underS r a)"
assume Case2: "a ∈ Field r"
hence 1: "under r a = underS r a ∪ {a} ∧ a ∉ underS r a"
using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
have 2: "wo_rel.ofilter r (underS r a) ∧ underS r a < Field r"
using 0 wo_rel.underS_ofilter * 1 Case2 by fast
hence "?r' <o r" using 0 using ofilter_ordLess by blast
moreover
have "Field ?r' = underS r a ∧ Well_order ?r'"
using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
ultimately have "|underS r a| <o |under r a|"
using ordIso_symmetric ordLess_ordIso_trans by blast
moreover
{have "∃f. bij_betw f (under r a) (underS r a)"
using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
}
ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
qed
qed
lemma infinite_Card_order_limit:
assumes r: "Card_order r" and "¬finite (Field r)"
and a: "a ∈ Field r"
shows "∃b ∈ Field r. a ≠ b ∧ (a,b) ∈ r"
proof -
have "Field r ≠ under r a"
using assms Card_order_infinite_not_under by blast
moreover have "under r a ≤ Field r"
using under_Field .
ultimately obtain b where b: "b ∈ Field r ∧ ¬ (b,a) ∈ r"
unfolding under_def by blast
moreover have ba: "b ≠ a"
using b r unfolding card_order_on_def well_order_on_def
linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
ultimately have "(a,b) ∈ r"
using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
total_on_def by blast
thus ?thesis using b ba by auto
qed
theorem Card_order_Times_same_infinite:
assumes CO: "Card_order r" and INF: "¬finite(Field r)"
shows "|Field r × Field r| ≤o r"
proof -
define phi where
"phi ≡ λr::'a rel. Card_order r ∧ ¬finite(Field r) ∧ ¬ |Field r × Field r| ≤o r"
have temp1: "∀r. phi r ⟶ Well_order r"
unfolding phi_def card_order_on_def by auto
have Ft: "¬(∃r. phi r)"
proof
assume "∃r. phi r"
hence "{r. phi r} ≠ {} ∧ {r. phi r} ≤ {r. Well_order r}"
using temp1 by auto
then obtain r where 1: "phi r" and 2: "∀r'. phi r' ⟶ r ≤o r'" and
3: "Card_order r ∧ Well_order r"
using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
let ?A = "Field r" let ?r' = "bsqr r"
have 4: "Well_order ?r' ∧ Field ?r' = ?A × ?A ∧ |?A| =o r"
using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
have 5: "Card_order |?A × ?A| ∧ Well_order |?A × ?A|"
using card_of_Card_order card_of_Well_order by blast
have "r <o |?A × ?A|"
using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
moreover have "|?A × ?A| ≤o ?r'"
using card_of_least[of "?A × ?A"] 4 by auto
ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
then obtain f where 6: "embed r ?r' f" and 7: "¬ bij_betw f ?A (?A × ?A)"
unfolding ordLess_def embedS_def[abs_def]
by (auto simp add: Field_bsqr)
let ?B = "f ` ?A"
have "|?A| =o |?B|"
using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
have "wo_rel.ofilter ?r' ?B"
using 6 embed_Field_ofilter 3 4 by blast
hence "wo_rel.ofilter ?r' ?B ∧ ?B ≠ ?A × ?A ∧ ?B ≠ Field ?r'"
using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
hence temp2: "wo_rel.ofilter ?r' ?B ∧ ?B < ?A × ?A"
using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
have "¬ (∃a. Field r = under r a)"
using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
then obtain A1 where temp3: "wo_rel.ofilter r A1 ∧ A1 < ?A" and 9: "?B ≤ A1 × A1"
using temp2 3 bsqr_ofilter[of r ?B] by blast
hence "|?B| ≤o |A1 × A1|" using card_of_mono1 by blast
hence 10: "r ≤o |A1 × A1|" using 8 ordIso_ordLeq_trans by blast
let ?r1 = "Restr r A1"
have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
moreover
{have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
hence "|A1| ≤o ?r1" using 3 Well_order_Restr card_of_least by blast
}
ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
have "¬ finite (Field r)" using 1 unfolding phi_def by simp
hence "¬ finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
hence "¬ finite A1" using 9 finite_cartesian_product finite_subset by blast
moreover have temp4: "Field |A1| = A1 ∧ Well_order |A1| ∧ Card_order |A1|"
using card_of_Card_order[of A1] card_of_Well_order[of A1]
by (simp add: Field_card_of)
moreover have "¬ r ≤o | A1 |"
using temp4 11 3 using not_ordLeq_iff_ordLess by blast
ultimately have "¬ finite(Field |A1| ) ∧ Card_order |A1| ∧ ¬ r ≤o | A1 |"
by (simp add: card_of_card_order_on)
hence "|Field |A1| × Field |A1| | ≤o |A1|"
using 2 unfolding phi_def by blast
hence "|A1 × A1 | ≤o |A1|" using temp4 by auto
hence "r ≤o |A1|" using 10 ordLeq_transitive by blast
thus False using 11 not_ordLess_ordLeq by auto
qed
thus ?thesis using assms unfolding phi_def by blast
qed
corollary card_of_Times_same_infinite:
assumes "¬finite A"
shows "|A × A| =o |A|"
proof -
let ?r = "|A|"
have "Field ?r = A ∧ Card_order ?r"
using Field_card_of card_of_Card_order[of A] by fastforce
hence "|A × A| ≤o |A|"
using Card_order_Times_same_infinite[of ?r] assms by auto
thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
qed
lemma card_of_Times_infinite:
assumes INF: "¬finite A" and NE: "B ≠ {}" and LEQ: "|B| ≤o |A|"
shows "|A × B| =o |A| ∧ |B × A| =o |A|"
proof -
have "|A| ≤o |A × B| ∧ |A| ≤o |B × A|"
using assms by (simp add: card_of_Times1 card_of_Times2)
moreover
{have "|A × B| ≤o |A × A| ∧ |B × A| ≤o |A × A|"
using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
moreover have "|A × A| =o |A|" using INF card_of_Times_same_infinite by blast
ultimately have "|A × B| ≤o |A| ∧ |B × A| ≤o |A|"
using ordLeq_ordIso_trans[of "|A × B|"] ordLeq_ordIso_trans[of "|B × A|"] by auto
}
ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
qed
corollary Card_order_Times_infinite:
assumes INF: "¬finite(Field r)" and CARD: "Card_order r" and
NE: "Field p ≠ {}" and LEQ: "p ≤o r"
shows "| (Field r) × (Field p) | =o r ∧ | (Field p) × (Field r) | =o r"
proof -
have "|Field r × Field p| =o |Field r| ∧ |Field p × Field r| =o |Field r|"
using assms by (simp add: card_of_Times_infinite card_of_mono2)
thus ?thesis
using assms card_of_Field_ordIso by (blast intro: ordIso_transitive)
qed
lemma card_of_Sigma_ordLeq_infinite:
assumes INF: "¬finite B" and
LEQ_I: "|I| ≤o |B|" and LEQ: "∀i ∈ I. |A i| ≤o |B|"
shows "|SIGMA i : I. A i| ≤o |B|"
proof(cases "I = {}")
case False
have "|SIGMA i : I. A i| ≤o |I × B|"
using card_of_Sigma_mono1[OF LEQ] by blast
moreover have "|I × B| =o |B|"
using INF False LEQ_I by (auto simp add: card_of_Times_infinite)
ultimately show ?thesis using ordLeq_ordIso_trans by blast
qed (simp add: card_of_empty)
lemma card_of_Sigma_ordLeq_infinite_Field:
assumes INF: "¬finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| ≤o r" and LEQ: "∀i ∈ I. |A i| ≤o r"
shows "|SIGMA i : I. A i| ≤o r"
proof -
let ?B = "Field r"
have 1: "r =o |?B| ∧ |?B| =o r"
using r card_of_Field_ordIso ordIso_symmetric by blast
hence "|I| ≤o |?B|" "∀i ∈ I. |A i| ≤o |?B|"
using LEQ_I LEQ ordLeq_ordIso_trans by blast+
hence "|SIGMA i : I. A i| ≤o |?B|" using INF LEQ
card_of_Sigma_ordLeq_infinite by blast
thus ?thesis using 1 ordLeq_ordIso_trans by blast
qed
lemma card_of_Times_ordLeq_infinite_Field:
"⟦¬finite (Field r); |A| ≤o r; |B| ≤o r; Card_order r⟧ ⟹ |A × B| ≤o r"
by(simp add: card_of_Sigma_ordLeq_infinite_Field)
lemma card_of_Times_infinite_simps:
"⟦¬finite A; B ≠ {}; |B| ≤o |A|⟧ ⟹ |A × B| =o |A|"
"⟦¬finite A; B ≠ {}; |B| ≤o |A|⟧ ⟹ |A| =o |A × B|"
"⟦¬finite A; B ≠ {}; |B| ≤o |A|⟧ ⟹ |B × A| =o |A|"
"⟦¬finite A; B ≠ {}; |B| ≤o |A|⟧ ⟹ |A| =o |B × A|"
by (auto simp add: card_of_Times_infinite ordIso_symmetric)
lemma card_of_UNION_ordLeq_infinite:
assumes INF: "¬finite B" and LEQ_I: "|I| ≤o |B|" and LEQ: "∀i ∈ I. |A i| ≤o |B|"
shows "|⋃i ∈ I. A i| ≤o |B|"
proof(cases "I = {}")
case False
have "|⋃i ∈ I. A i| ≤o |SIGMA i : I. A i|"
using card_of_UNION_Sigma by blast
moreover have "|SIGMA i : I. A i| ≤o |B|"
using assms card_of_Sigma_ordLeq_infinite by blast
ultimately show ?thesis using ordLeq_transitive by blast
qed (simp add: card_of_empty)
corollary card_of_UNION_ordLeq_infinite_Field:
assumes INF: "¬finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| ≤o r" and LEQ: "∀i ∈ I. |A i| ≤o r"
shows "|⋃i ∈ I. A i| ≤o r"
proof -
let ?B = "Field r"
have 1: "r =o |?B| ∧ |?B| =o r"
using r card_of_Field_ordIso ordIso_symmetric by blast
hence "|I| ≤o |?B|" "∀i ∈ I. |A i| ≤o |?B|"
using LEQ_I LEQ ordLeq_ordIso_trans by blast+
hence "|⋃i ∈ I. A i| ≤o |?B|" using INF LEQ
card_of_UNION_ordLeq_infinite by blast
thus ?thesis using 1 ordLeq_ordIso_trans by blast
qed
lemma card_of_Plus_infinite1:
assumes INF: "¬finite A" and LEQ: "|B| ≤o |A|"
shows "|A <+> B| =o |A|"
proof(cases "B = {}")
case True
then show ?thesis
by (simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
next
case False
let ?Inl = "Inl::'a ⇒ 'a + 'b" let ?Inr = "Inr::'b ⇒ 'a + 'b"
assume *: "B ≠ {}"
then obtain b1 where 1: "b1 ∈ B" by blast
show ?thesis
proof(cases "B = {b1}")
case True
have 2: "bij_betw ?Inl A ((?Inl ` A))"
unfolding bij_betw_def inj_on_def by auto
hence 3: "¬finite (?Inl ` A)"
using INF bij_betw_finite[of ?Inl A] by blast
let ?A' = "?Inl ` A ∪ {?Inr b1}"
obtain g where "bij_betw g (?Inl ` A) ?A'"
using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
moreover have "?A' = A <+> B" using True by blast
ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
hence "bij_betw (g ∘ ?Inl) A (A <+> B)"
using 2 by (auto simp add: bij_betw_trans)
thus ?thesis using card_of_ordIso ordIso_symmetric by blast
next
case False
with * 1 obtain b2 where 3: "b1 ≠ b2 ∧ {b1,b2} ≤ B" by fastforce
obtain f where "inj_on f B ∧ f ` B ≤ A"
using LEQ card_of_ordLeq[of B] by fastforce
with 3 have "f b1 ≠ f b2 ∧ {f b1, f b2} ≤ A"
unfolding inj_on_def by auto
with 3 have "|A <+> B| ≤o |A × B|"
by (auto simp add: card_of_Plus_Times)
moreover have "|A × B| =o |A|"
using assms * by (simp add: card_of_Times_infinite_simps)
ultimately have "|A <+> B| ≤o |A|" using ordLeq_ordIso_trans by blast
thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
qed
qed
lemma card_of_Plus_infinite2:
assumes INF: "¬finite A" and LEQ: "|B| ≤o |A|"
shows "|B <+> A| =o |A|"
using assms card_of_Plus_commute card_of_Plus_infinite1
ordIso_equivalence by blast
lemma card_of_Plus_infinite:
assumes INF: "¬finite A" and LEQ: "|B| ≤o |A|"
shows "|A <+> B| =o |A| ∧ |B <+> A| =o |A|"
using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
corollary Card_order_Plus_infinite:
assumes INF: "¬finite(Field r)" and CARD: "Card_order r" and
LEQ: "p ≤o r"
shows "| (Field r) <+> (Field p) | =o r ∧ | (Field p) <+> (Field r) | =o r"
proof -
have "| Field r <+> Field p | =o | Field r | ∧
| Field p <+> Field r | =o | Field r |"
using assms by (simp add: card_of_Plus_infinite card_of_mono2)
thus ?thesis
using assms card_of_Field_ordIso by (blast intro: ordIso_transitive)
qed
subsection ‹The cardinal $\omega$ and the finite cardinals›
text‹The cardinal $\omega$, of natural numbers, shall be the standard non-strict
order relation on
‹nat›, that we abbreviate by ‹natLeq›. The finite cardinals
shall be the restrictions of these relations to the numbers smaller than
fixed numbers ‹n›, that we abbreviate by ‹natLeq_on n›.›
definition "(natLeq::(nat * nat) set) ≡ {(x,y). x ≤ y}"
definition "(natLess::(nat * nat) set) ≡ {(x,y). x < y}"
abbreviation natLeq_on :: "nat ⇒ (nat * nat) set"
where "natLeq_on n ≡ {(x,y). x < n ∧ y < n ∧ x ≤ y}"
lemma infinite_cartesian_product:
assumes "¬finite A" "¬finite B"
shows "¬finite (A × B)"
using assms finite_cartesian_productD2 by auto
subsubsection ‹First as well-orders›
lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
by(unfold Field_def natLeq_def, auto)
lemma natLeq_Refl: "Refl natLeq"
unfolding refl_on_def Field_def natLeq_def by auto
lemma natLeq_trans: "trans natLeq"
unfolding trans_def natLeq_def by auto
lemma natLeq_Preorder: "Preorder natLeq"
unfolding preorder_on_def
by (auto simp add: natLeq_Refl natLeq_trans)
lemma natLeq_antisym: "antisym natLeq"
unfolding antisym_def natLeq_def by auto
lemma natLeq_Partial_order: "Partial_order natLeq"
unfolding partial_order_on_def
by (auto simp add: natLeq_Preorder natLeq_antisym)
lemma natLeq_Total: "Total natLeq"
unfolding total_on_def natLeq_def by auto
lemma natLeq_Linear_order: "Linear_order natLeq"
unfolding linear_order_on_def
by (auto simp add: natLeq_Partial_order natLeq_Total)
lemma natLeq_natLess_Id: "natLess = natLeq - Id"
unfolding natLeq_def natLess_def by auto
lemma natLeq_Well_order: "Well_order natLeq"
unfolding well_order_on_def
using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
unfolding Field_def by auto
lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
unfolding underS_def natLeq_def by auto
lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
unfolding natLeq_def by force
lemma Restr_natLeq2:
"Restr natLeq (underS natLeq n) = natLeq_on n"
by (auto simp add: Restr_natLeq natLeq_underS_less)
lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
using Restr_natLeq[of n] natLeq_Well_order
Well_order_Restr[of natLeq "{x. x < n}"] by auto
corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
using natLeq_on_Well_order Field_natLeq_on by auto
lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
unfolding wo_rel_def using natLeq_on_Well_order .
subsubsection ‹Then as cardinals›
lemma natLeq_Card_order: "Card_order natLeq"
proof -
have "natLeq_on n <o |UNIV::nat set|" for n
proof -
have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
moreover have "¬finite(UNIV::nat set)" by auto
ultimately show ?thesis
using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order
by (force simp add: Field_card_of)
qed
then show ?thesis
apply (simp add: natLeq_Well_order Card_order_iff_Restr_underS Restr_natLeq2)
apply (force simp add: Field_natLeq)
done
qed
corollary card_of_Field_natLeq:
"|Field natLeq| =o natLeq"
using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
ordIso_symmetric[of natLeq] by blast
corollary card_of_nat:
"|UNIV::nat set| =o natLeq"
using Field_natLeq card_of_Field_natLeq by auto
corollary infinite_iff_natLeq_ordLeq:
"¬finite A = ( natLeq ≤o |A| )"
using infinite_iff_card_of_nat[of A] card_of_nat
ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
corollary finite_iff_ordLess_natLeq:
"finite A = ( |A| <o natLeq)"
using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
card_of_Well_order natLeq_Well_order by blast
subsection ‹The successor of a cardinal›
text‹First we define ‹isCardSuc r r'›, the notion of ‹r'›
being a successor cardinal of ‹r›. Although the definition does
not require ‹r› to be a cardinal, only this case will be meaningful.›
definition isCardSuc :: "'a rel ⇒ 'a set rel ⇒ bool"
where
"isCardSuc r r' ≡
Card_order r' ∧ r <o r' ∧
(∀(r''::'a set rel). Card_order r'' ∧ r <o r'' ⟶ r' ≤o r'')"
text‹Now we introduce the cardinal-successor operator ‹cardSuc›,
by picking {\em some} cardinal-order relation fulfilling ‹isCardSuc›.
Again, the picked item shall be proved unique up to order-isomorphism.›
definition cardSuc :: "'a rel ⇒ 'a set rel"
where "cardSuc r ≡ SOME r'. isCardSuc r r'"
lemma exists_minim_Card_order:
"⟦R ≠ {}; ∀r ∈ R. Card_order r⟧ ⟹ ∃r ∈ R. ∀r' ∈ R. r ≤o r'"
unfolding card_order_on_def using exists_minim_Well_order by blast
lemma exists_isCardSuc:
assumes "Card_order r"
shows "∃r'. isCardSuc r r'"
proof -
let ?R = "{(r'::'a set rel). Card_order r' ∧ r <o r'}"
have "|Pow(Field r)| ∈ ?R ∧ (∀r ∈ ?R. Card_order r)" using assms
by (simp add: card_of_Card_order Card_order_Pow)
then obtain r where "r ∈ ?R ∧ (∀r' ∈ ?R. r ≤o r')"
using exists_minim_Card_order[of ?R] by blast
thus ?thesis unfolding isCardSuc_def by auto
qed
lemma cardSuc_isCardSuc:
assumes "Card_order r"
shows "isCardSuc r (cardSuc r)"
unfolding cardSuc_def using assms
by (simp add: exists_isCardSuc someI_ex)
lemma cardSuc_Card_order:
"Card_order r ⟹ Card_order(cardSuc r)"
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
lemma cardSuc_greater:
"Card_order r ⟹ r <o cardSuc r"
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
lemma cardSuc_ordLeq:
"Card_order r ⟹ r ≤o cardSuc r"
using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
text‹The minimality property of ‹cardSuc› originally present in its definition
is local to the type ‹'a set rel›, i.e., that of ‹cardSuc r›:›
lemma cardSuc_least_aux:
"⟦Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'⟧ ⟹ cardSuc r ≤o r'"
using cardSuc_isCardSuc unfolding isCardSuc_def by blast
text‹But from this we can infer general minimality:›
lemma cardSuc_least:
assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
shows "cardSuc r ≤o r'"
proof -
let ?p = "cardSuc r"
have 0: "Well_order ?p ∧ Well_order r'"
using assms cardSuc_Card_order unfolding card_order_on_def by blast
{ assume "r' <o ?p"
then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' ∧ r'' <o ?p"
using internalize_ordLess[of r' ?p] by blast
have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
ultimately have "?p ≤o r''" using cardSuc_least_aux CARD by blast
hence False using 2 not_ordLess_ordLeq by blast
}
thus ?thesis using 0 ordLess_or_ordLeq by blast
qed
lemma cardSuc_ordLess_ordLeq:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(r <o r') = (cardSuc r ≤o r')"
proof
show "cardSuc r ≤o r' ⟹ r <o r'"
using assms cardSuc_greater ordLess_ordLeq_trans by blast
qed (auto simp add: assms cardSuc_least)
lemma cardSuc_ordLeq_ordLess:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(r' <o cardSuc r) = (r' ≤o r)"
proof -
have "Well_order r ∧ Well_order r'"
using assms unfolding card_order_on_def by auto
moreover have "Well_order(cardSuc r)"
using assms cardSuc_Card_order card_order_on_def by blast
ultimately show ?thesis
using assms cardSuc_ordLess_ordLeq by (blast dest: not_ordLeq_iff_ordLess)
qed
lemma cardSuc_mono_ordLeq:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(cardSuc r ≤o cardSuc r') = (r ≤o r')"
using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
lemma cardSuc_invar_ordIso:
assumes CARD: "Card_order r" and CARD': "Card_order r'"
shows "(cardSuc r =o cardSuc r') = (r =o r')"
proof -
have 0: "Well_order r ∧ Well_order r' ∧ Well_order(cardSuc r) ∧ Well_order(cardSuc r')"
using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
thus ?thesis
using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
qed
lemma card_of_cardSuc_finite:
"finite(Field(cardSuc |A| )) = finite A"
proof
assume *: "finite (Field (cardSuc |A| ))"
have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
hence "|A| ≤o |Field(cardSuc |A| )|"
using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
ordLeq_ordIso_trans by blast
thus "finite A" using * card_of_ordLeq_finite by blast
next
assume "finite A"
then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
moreover
have "cardSuc |A| ≤o |Pow A|"
by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
ultimately show "finite (Field (cardSuc |A| ))"
by (blast intro: card_of_ordLeq_finite card_of_mono2)
qed
lemma cardSuc_finite:
assumes "Card_order r"
shows "finite (Field (cardSuc r)) = finite (Field r)"
proof -
let ?A = "Field r"
have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
hence "cardSuc |?A| =o cardSuc r" using assms
by (simp add: card_of_Card_order cardSuc_invar_ordIso)
moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
moreover
{ have "|Field (cardSuc r) | =o cardSuc r"
using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
hence "cardSuc r =o |Field (cardSuc r) |"
using ordIso_symmetric by blast
}
ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
using ordIso_transitive by blast
hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
using card_of_ordIso_finite by blast
thus ?thesis by (simp only: card_of_cardSuc_finite)
qed
lemma Field_cardSuc_not_empty:
assumes "Card_order r"
shows "Field (cardSuc r) ≠ {}"
proof
assume "Field(cardSuc r) = {}"
then have "|Field(cardSuc r)| ≤o r" using assms Card_order_empty[of r] by auto
then have "cardSuc r ≤o r" using assms card_of_Field_ordIso
cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
then show False using cardSuc_greater not_ordLess_ordLeq assms by blast
qed
typedef 'a suc = "Field (cardSuc |UNIV :: 'a set| )"
using Field_cardSuc_not_empty card_of_Card_order by blast
definition card_suc :: "'a rel ⇒ 'a suc rel" where
"card_suc ≡ λ_. map_prod Abs_suc Abs_suc ` cardSuc |UNIV :: 'a set|"
lemma Field_card_suc: "Field (card_suc r) = UNIV"
proof -
let ?r = "cardSuc |UNIV|"
let ?ar = "λx. Abs_suc (Rep_suc x)"
have 1: "⋀P. (∀x∈Field ?r. P x) = (∀x. P (Rep_suc x))" using Rep_suc_induct Rep_suc by blast
have 2: "⋀P. (∃x∈Field ?r. P x) = (∃x. P (Rep_suc x))" using Rep_suc_cases Rep_suc by blast
have 3: "⋀A a b. (a, b) ∈ A ⟹ (Abs_suc a, Abs_suc b) ∈ map_prod Abs_suc Abs_suc ` A" unfolding map_prod_def by auto
have "∀x∈Field ?r. (∃b∈Field ?r. (x, b) ∈ ?r) ∨ (∃a∈Field ?r. (a, x) ∈ ?r)"
unfolding Field_def Range.simps Domain.simps Un_iff by blast
then have "∀x. (∃b. (Rep_suc x, Rep_suc b) ∈ ?r) ∨ (∃a. (Rep_suc a, Rep_suc x) ∈ ?r)" unfolding 1 2 .
then have "∀x. (∃b. (?ar x, ?ar b) ∈ map_prod Abs_suc Abs_suc ` ?r) ∨ (∃a. (?ar a, ?ar x) ∈ map_prod Abs_suc Abs_suc ` ?r)" using 3 by fast
then have "∀x. (∃b. (x, b) ∈ card_suc r) ∨ (∃a. (a, x) ∈ card_suc r)" unfolding card_suc_def Rep_suc_inverse .
then show ?thesis unfolding Field_def Domain.simps Range.simps set_eq_iff Un_iff eqTrueI[OF UNIV_I] ex_simps simp_thms .
qed
lemma card_suc_alt: "card_suc r = dir_image (cardSuc |UNIV :: 'a set| ) Abs_suc"
unfolding card_suc_def dir_image_def by auto
lemma cardSuc_Well_order: "Card_order r ⟹ Well_order(cardSuc r)"
using cardSuc_Card_order unfolding card_order_on_def by blast
lemma cardSuc_ordIso_card_suc:
assumes "card_order r"
shows "cardSuc r =o card_suc (r :: 'a rel)"
proof -
have "cardSuc (r :: 'a rel) =o cardSuc |UNIV :: 'a set|"
using cardSuc_invar_ordIso[THEN iffD2, OF _ card_of_Card_order card_of_unique[OF assms]] assms
by (simp add: card_order_on_Card_order)
also have "cardSuc |UNIV :: 'a set| =o card_suc (r :: 'a rel)"
unfolding card_suc_alt
by (rule dir_image_ordIso) (simp_all add: inj_on_def Abs_suc_inject cardSuc_Well_order card_of_Card_order)
finally show ?thesis .
qed
lemma Card_order_card_suc: "card_order r ⟹ Card_order (card_suc r)"
using cardSuc_Card_order[THEN Card_order_ordIso2[OF _ cardSuc_ordIso_card_suc]] card_order_on_Card_order by blast
lemma card_order_card_suc: "card_order r ⟹ card_order (card_suc r)"
using Card_order_card_suc arg_cong2[OF Field_card_suc refl, of "card_order_on"] by blast
lemma card_suc_greater: "card_order r ⟹ r <o card_suc r"
using ordLess_ordIso_trans[OF cardSuc_greater cardSuc_ordIso_card_suc] card_order_on_Card_order by blast
lemma card_of_Plus_ordLess_infinite:
assumes INF: "¬finite C" and LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A <+> B| <o |C|"
proof(cases "A = {} ∨ B = {}")
case True
hence "|A| =o |A <+> B| ∨ |B| =o |A <+> B|"
using card_of_Plus_empty1 card_of_Plus_empty2 by blast
hence "|A <+> B| =o |A| ∨ |A <+> B| =o |B|"
using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
thus ?thesis using LESS1 LESS2
ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
next
case False
have False if "|C| ≤o |A <+> B|"
proof -
have §: "¬finite A ∨ ¬finite B"
using that INF card_of_ordLeq_finite finite_Plus by blast
consider "|A| ≤o |B|" | "|B| ≤o |A|"
using ordLeq_total [OF card_of_Well_order card_of_Well_order] by blast
then show False
proof cases
case 1
hence "¬finite B" using § card_of_ordLeq_finite by blast
hence "|A <+> B| =o |B|" using False 1
by (auto simp add: card_of_Plus_infinite)
thus False using LESS2 not_ordLess_ordLeq that ordLeq_ordIso_trans by blast
next
case 2
hence "¬finite A" using § card_of_ordLeq_finite by blast
hence "|A <+> B| =o |A|" using False 2
by (auto simp add: card_of_Plus_infinite)
thus False using LESS1 not_ordLess_ordLeq that ordLeq_ordIso_trans by blast
qed
qed
thus ?thesis
using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
qed
lemma card_of_Plus_ordLess_infinite_Field:
assumes INF: "¬finite (Field r)" and r: "Card_order r" and
LESS1: "|A| <o r" and LESS2: "|B| <o r"
shows "|A <+> B| <o r"
proof -
let ?C = "Field r"
have 1: "r =o |?C| ∧ |?C| =o r"
using r card_of_Field_ordIso ordIso_symmetric by blast
hence "|A| <o |?C|" "|B| <o |?C|"
using LESS1 LESS2 ordLess_ordIso_trans by blast+
hence "|A <+> B| <o |?C|" using INF
card_of_Plus_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
lemma card_of_Plus_ordLeq_infinite_Field:
assumes r: "¬finite (Field r)" and A: "|A| ≤o r" and B: "|B| ≤o r"
and c: "Card_order r"
shows "|A <+> B| ≤o r"
proof -
let ?r' = "cardSuc r"
have "Card_order ?r' ∧ ¬finite (Field ?r')" using assms
by (simp add: cardSuc_Card_order cardSuc_finite)
moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
ultimately have "|A <+> B| <o ?r'"
using card_of_Plus_ordLess_infinite_Field by blast
thus ?thesis using c r
by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
qed
lemma card_of_Un_ordLeq_infinite_Field:
assumes C: "¬finite (Field r)" and A: "|A| ≤o r" and B: "|B| ≤o r"
and "Card_order r"
shows "|A Un B| ≤o r"
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
ordLeq_transitive by fast
lemma card_of_Un_ordLess_infinite:
assumes INF: "¬finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A ∪ B| <o |C|"
using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
ordLeq_ordLess_trans by blast
lemma card_of_Un_ordLess_infinite_Field:
assumes INF: "¬finite (Field r)" and r: "Card_order r" and
LESS1: "|A| <o r" and LESS2: "|B| <o r"
shows "|A Un B| <o r"
proof -
let ?C = "Field r"
have 1: "r =o |?C| ∧ |?C| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|A| <o |?C|" "|B| <o |?C|"
using LESS1 LESS2 ordLess_ordIso_trans by blast+
hence "|A Un B| <o |?C|" using INF
card_of_Un_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
subsection ‹Regular cardinals›
definition cofinal where
"cofinal A r ≡ ∀a ∈ Field r. ∃b ∈ A. a ≠ b ∧ (a,b) ∈ r"
definition regularCard where
"regularCard r ≡ ∀K. K ≤ Field r ∧ cofinal K r ⟶ |K| =o r"
definition relChain where
"relChain r As ≡ ∀i j. (i,j) ∈ r ⟶ As i ≤ As j"
lemma regularCard_UNION:
assumes r: "Card_order r" "regularCard r"
and As: "relChain r As"
and Bsub: "B ≤ (⋃i ∈ Field r. As i)"
and cardB: "|B| <o r"
shows "∃i ∈ Field r. B ≤ As i"
proof -
let ?phi = "λb j. j ∈ Field r ∧ b ∈ As j"
have "∀b∈B. ∃j. ?phi b j" using Bsub by blast
then obtain f where f: "⋀b. b ∈ B ⟹ ?phi b (f b)"
using bchoice[of B ?phi] by blast
let ?K = "f ` B"
{assume 1: "⋀i. i ∈ Field r ⟹ ¬ B ≤ As i"
have 2: "cofinal ?K r"
unfolding cofinal_def
proof (intro strip)
fix i assume i: "i ∈ Field r"
with 1 obtain b where b: "b ∈ B ∧ b ∉ As i" by blast
hence "i ≠ f b ∧ ¬ (f b,i) ∈ r"
using As f unfolding relChain_def by auto
hence "i ≠ f b ∧ (i, f b) ∈ r" using r
unfolding card_order_on_def well_order_on_def linear_order_on_def
total_on_def using i f b by auto
with b show "∃b ∈ f`B. i ≠ b ∧ (i,b) ∈ r" by blast
qed
moreover have "?K ≤ Field r" using f by blast
ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast
moreover
have "|?K| <o r" using cardB ordLeq_ordLess_trans card_of_image by blast
ultimately have False using not_ordLess_ordIso by blast
}
thus ?thesis by blast
qed
lemma infinite_cardSuc_regularCard:
assumes r_inf: "¬finite (Field r)" and r_card: "Card_order r"
shows "regularCard (cardSuc r)"
proof -
let ?r' = "cardSuc r"
have r': "Card_order ?r'" "⋀p. Card_order p ⟶ (p ≤o r) = (p <o ?r')"
using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
show ?thesis
unfolding regularCard_def proof auto
fix K assume 1: "K ≤ Field ?r'" and 2: "cofinal K ?r'"
hence "|K| ≤o |Field ?r'|" by (simp only: card_of_mono1)
also have 22: "|Field ?r'| =o ?r'"
using r' by (simp add: card_of_Field_ordIso[of ?r'])
finally have "|K| ≤o ?r'" .
moreover
{ let ?L = "⋃ j ∈ K. underS ?r' j"
let ?J = "Field r"
have rJ: "r =o |?J|"
using r_card card_of_Field_ordIso ordIso_symmetric by blast
assume "|K| <o ?r'"
hence "|K| ≤o r" using r' card_of_Card_order[of K] by blast
hence "|K| ≤o |?J|" using rJ ordLeq_ordIso_trans by blast
moreover
{have "∀j∈K. |underS ?r' j| <o ?r'"
using r' 1 by (auto simp: card_of_underS)
hence "∀j∈K. |underS ?r' j| ≤o r"
using r' card_of_Card_order by blast
hence "∀j∈K. |underS ?r' j| ≤o |?J|"
using rJ ordLeq_ordIso_trans by blast
}
ultimately have "|?L| ≤o |?J|"
using r_inf card_of_UNION_ordLeq_infinite by blast
hence "|?L| ≤o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
hence "|?L| <o ?r'" using r' card_of_Card_order by blast
moreover
{
have "Field ?r' ≤ ?L"
using 2 unfolding underS_def cofinal_def by auto
hence "|Field ?r'| ≤o |?L|" by (simp add: card_of_mono1)
hence "?r' ≤o |?L|"
using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
}
ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast
hence False using ordLess_irreflexive by blast
}
ultimately show "|K| =o ?r'"
unfolding ordLeq_iff_ordLess_or_ordIso by blast
qed
qed
lemma cardSuc_UNION:
assumes r: "Card_order r" and "¬finite (Field r)"
and As: "relChain (cardSuc r) As"
and Bsub: "B ≤ (⋃ i ∈ Field (cardSuc r). As i)"
and cardB: "|B| ≤o r"
shows "∃i ∈ Field (cardSuc r). B ≤ As i"
proof -
let ?r' = "cardSuc r"
have "Card_order ?r' ∧ |B| <o ?r'"
using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
card_of_Card_order by blast
moreover have "regularCard ?r'"
using assms by(simp add: infinite_cardSuc_regularCard)
ultimately show ?thesis
using As Bsub cardB regularCard_UNION by blast
qed
subsection ‹Others›
lemma card_of_Func_Times:
"|Func (A × B) C| =o |Func A (Func B C)|"
unfolding card_of_ordIso[symmetric]
using bij_betw_curr by blast
lemma card_of_Pow_Func:
"|Pow A| =o |Func A (UNIV::bool set)|"
proof -
define F where [abs_def]: "F A' a ≡
(if a ∈ A then (if a ∈ A' then True else False) else undefined)" for A' a
have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
fix A1 A2 assume "A1 ∈ Pow A" "A2 ∈ Pow A" "F A1 = F A2"
thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: if_split_asm)
next
show "F ` Pow A = Func A UNIV"
proof safe
fix f assume f: "f ∈ Func A (UNIV::bool set)"
show "f ∈ F ` Pow A"
unfolding image_iff
proof
show "f = F {a ∈ A. f a = True}"
using f unfolding Func_def F_def by force
qed auto
qed(unfold Func_def F_def, auto)
qed
thus ?thesis unfolding card_of_ordIso[symmetric] by blast
qed
lemma card_of_Func_UNIV:
"|Func (UNIV::'a set) (B::'b set)| =o |{f::'a ⇒ 'b. range f ⊆ B}|"
proof -
let ?F = "λ f (a::'a). ((f a)::'b)"
have "bij_betw ?F {f. range f ⊆ B} (Func UNIV B)"
unfolding bij_betw_def inj_on_def
proof safe
fix h :: "'a ⇒ 'b" assume h: "h ∈ Func UNIV B"
then obtain f where f: "∀ a. h a = f a" by blast
hence "range f ⊆ B" using h unfolding Func_def by auto
thus "h ∈ (λf a. f a) ` {f. range f ⊆ B}" using f by auto
qed(unfold Func_def fun_eq_iff, auto)
then show ?thesis
by (blast intro: ordIso_symmetric card_of_ordIsoI)
qed
lemma Func_Times_Range:
"|Func A (B × C)| =o |Func A B × Func A C|" (is "|?LHS| =o |?RHS|")
proof -
let ?F = "λfg. (λx. if x ∈ A then fst (fg x) else undefined,
λx. if x ∈ A then snd (fg x) else undefined)"
let ?G = "λ(f, g) x. if x ∈ A then (f x, g x) else undefined"
have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
proof (intro conjI impI ballI equalityI subsetI)
fix f g assume *: "f ∈ Func A (B × C)" "g ∈ Func A (B × C)" "?F f = ?F g"
show "f = g"
proof
fix x from * have "fst (f x) = fst (g x) ∧ snd (f x) = snd (g x)"
by (cases "x ∈ A") (auto simp: Func_def fun_eq_iff split: if_splits)
then show "f x = g x" by (subst (1 2) surjective_pairing) simp
qed
next
fix fg assume "fg ∈ Func A B × Func A C"
thus "fg ∈ ?F ` Func A (B × C)"
by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
qed (auto simp: Func_def fun_eq_iff)
thus ?thesis using card_of_ordIso by blast
qed
subsection ‹Regular vs. stable cardinals›
definition stable :: "'a rel ⇒ bool"
where
"stable r ≡ ∀(A::'a set) (F :: 'a ⇒ 'a set).
|A| <o r ∧ (∀a ∈ A. |F a| <o r)
⟶ |SIGMA a : A. F a| <o r"
lemma regularCard_stable:
assumes cr: "Card_order r" and ir: "¬finite (Field r)" and reg: "regularCard r"
shows "stable r"
unfolding stable_def proof safe
fix A :: "'a set" and F :: "'a ⇒ 'a set" assume A: "|A| <o r" and F: "∀a∈A. |F a| <o r"
{assume "r ≤o |Sigma A F|"
hence "|Field r| ≤o |Sigma A F|" using card_of_Field_ordIso[OF cr] ordIso_ordLeq_trans by blast
moreover have Fi: "Field r ≠ {}" using ir by auto
ultimately have "∃f. f ` Sigma A F = Field r" using card_of_ordLeq2[OF Fi] by blast
then obtain f where f: "f ` Sigma A F = Field r" by blast
have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto
{fix a assume a: "a ∈ A"
define L where "L = {(a,u) | u. u ∈ F a}"
have fL: "f ` L ⊆ Field r" using f a unfolding L_def by auto
have "bij_betw snd {(a, u) |u. u ∈ F a} (F a)"
unfolding bij_betw_def inj_on_def by (auto simp: image_def)
then have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric] by blast
hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
hence "¬ cofinal (f ` L) r" using reg fL unfolding regularCard_def
by (force simp add: dest: not_ordLess_ordIso)
then obtain k where k: "k ∈ Field r" and "∀ l ∈ L. ¬ (f l ≠ k ∧ (k, f l) ∈ r)"
unfolding cofinal_def image_def by auto
hence "∃ k ∈ Field r. ∀ l ∈ L. (f l, k) ∈ r"
using wo_rel.in_notinI[OF r _ _ ‹k ∈ Field r›] fL unfolding image_subset_iff by fast
hence "∃ k ∈ Field r. ∀ u ∈ F a. (f (a,u), k) ∈ r" unfolding L_def by auto
}
then have x: "⋀a. a∈A ⟹ ∃k. k ∈ Field r ∧ (∀u∈F a. (f (a, u), k) ∈ r)" by blast
obtain gg where "⋀a. a∈A ⟹ gg a = (SOME k. k ∈ Field r ∧ (∀u∈F a. (f (a, u), k) ∈ r))" by simp
then have gg: "∀a∈A. ∀u∈F a. (f (a, u), gg a) ∈ r" using someI_ex[OF x] by auto
obtain j0 where j0: "j0 ∈ Field r" using Fi by auto
define g where [abs_def]: "g a = (if F a ≠ {} then gg a else j0)" for a
have g: "∀ a ∈ A. ∀ u ∈ F a. (f (a,u),g a) ∈ r" using gg unfolding g_def by auto
hence 1: "Field r ⊆ (⋃a ∈ A. under r (g a))"
using f[symmetric] unfolding under_def image_def by auto
have gA: "g ` A ⊆ Field r" using gg j0 unfolding Field_def g_def by auto
moreover have "cofinal (g ` A) r" unfolding cofinal_def
proof safe
fix i assume "i ∈ Field r"
then obtain j where ij: "(i,j) ∈ r" "i ≠ j" using cr ir infinite_Card_order_limit by fast
hence "j ∈ Field r" using card_order_on_def cr well_order_on_domain by fast
then obtain a where a: "a ∈ A" and j: "(j, g a) ∈ r"
using 1 unfolding under_def by auto
hence "(i, g a) ∈ r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
moreover have "i ≠ g a"
using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
partial_order_on_def antisym_def by auto
ultimately show "∃j∈g ` A. i ≠ j ∧ (i, j) ∈ r" using a by auto
qed
ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
moreover have "|g ` A| ≤o |A|" using card_of_image by blast
ultimately have False using A using not_ordLess_ordIso ordLeq_ordLess_trans by blast
}
thus "|Sigma A F| <o r"
using cr not_ordLess_iff_ordLeq using card_of_Well_order card_order_on_well_order_on by blast
qed
lemma stable_regularCard:
assumes cr: "Card_order r" and ir: "¬finite (Field r)" and st: "stable r"
shows "regularCard r"
unfolding regularCard_def proof safe
fix K assume K: "K ⊆ Field r" and cof: "cofinal K r"
have "|K| ≤o r" using K card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans by blast
moreover
{assume Kr: "|K| <o r"
have x: "⋀a. a ∈ Field r ⟹ ∃b. b ∈ K ∧ a ≠ b ∧ (a, b) ∈ r" using cof unfolding cofinal_def by blast
then obtain f where "⋀a. a ∈ Field r ⟹ f a = (SOME b. b ∈ K ∧ a ≠ b ∧ (a, b) ∈ r)" by simp
then have "∀a∈Field r. f a ∈ K ∧ a ≠ f a ∧ (a, f a) ∈ r" using someI_ex[OF x] by simp
hence "Field r ⊆ (⋃a ∈ K. underS r a)" unfolding underS_def by auto
hence "r ≤o |⋃a ∈ K. underS r a|"
using cr Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive by blast
also have "|⋃a ∈ K. underS r a| ≤o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
also
{have "∀ a ∈ K. |underS r a| <o r" using K card_of_underS[OF cr] subsetD by auto
hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
}
finally have "r <o r" .
hence False using ordLess_irreflexive by blast
}
ultimately show "|K| =o r" using ordLeq_iff_ordLess_or_ordIso by blast
qed
lemma internalize_card_of_ordLess:
"( |A| <o r) = (∃B < Field r. |A| =o |B| ∧ |B| <o r)"
proof
assume "|A| <o r"
then obtain p where 1: "Field p < Field r ∧ |A| =o p ∧ p <o r"
using internalize_ordLess[of "|A|" r] by blast
hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
hence "|Field p| =o p" using card_of_Field_ordIso by blast
hence "|A| =o |Field p| ∧ |Field p| <o r"
using 1 ordIso_equivalence ordIso_ordLess_trans by blast
thus "∃B < Field r. |A| =o |B| ∧ |B| <o r" using 1 by blast
next
assume "∃B < Field r. |A| =o |B| ∧ |B| <o r"
thus "|A| <o r" using ordIso_ordLess_trans by blast
qed
lemma card_of_Sigma_cong1:
assumes "∀i ∈ I. |A i| =o |B i|"
shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
lemma card_of_Sigma_cong2:
assumes "bij_betw f (I::'i set) (J::'j set)"
shows "|SIGMA i : I. (A::'j ⇒ 'a set) (f i)| =o |SIGMA j : J. A j|"
proof -
let ?LEFT = "SIGMA i : I. A (f i)"
let ?RIGHT = "SIGMA j : J. A j"
define u where "u ≡ λ(i::'i,a::'a). (f i,a)"
have "bij_betw u ?LEFT ?RIGHT"
using assms unfolding u_def bij_betw_def inj_on_def by auto
thus ?thesis using card_of_ordIso by blast
qed
lemma card_of_Sigma_cong:
assumes BIJ: "bij_betw f I J" and ISO: "∀j ∈ J. |A j| =o |B j|"
shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
proof -
have "∀i ∈ I. |A(f i)| =o |B(f i)|"
using ISO BIJ unfolding bij_betw_def by blast
hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1)
moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
using BIJ card_of_Sigma_cong2 by blast
ultimately show ?thesis using ordIso_transitive by blast
qed
lemma stable_elim:
assumes ST: "stable r" and A_LESS: "|A| <o r" and
F_LESS: "⋀ a. a ∈ A ⟹ |F a| <o r"
shows "|SIGMA a : A. F a| <o r"
proof -
obtain A' where 1: "A' < Field r ∧ |A'| <o r" and 2: " |A| =o |A'|"
using internalize_card_of_ordLess[of A r] A_LESS by blast
then obtain G where 3: "bij_betw G A' A"
using card_of_ordIso ordIso_symmetric by blast
{fix a assume "a ∈ A"
hence "∃B'. B' ≤ Field r ∧ |F a| =o |B'| ∧ |B'| <o r"
using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
}
then obtain F' where
temp: "∀a ∈ A. F' a ≤ Field r ∧ |F a| =o |F' a| ∧ |F' a| <o r"
using bchoice[of A "λ a B'. B' ≤ Field r ∧ |F a| =o |B'| ∧ |B'| <o r"] by blast
hence 4: "∀a ∈ A. F' a ≤ Field r ∧ |F' a| <o r" by auto
have 5: "∀a ∈ A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
have "∀a' ∈ A'. F'(G a') ≤ Field r ∧ |F'(G a')| <o r"
using 3 4 bij_betw_ball[of G A' A] by auto
hence "|SIGMA a' : A'. F'(G a')| <o r"
using ST 1 unfolding stable_def by auto
moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
qed
lemma stable_natLeq: "stable natLeq"
proof(unfold stable_def, safe)
fix A :: "'a set" and F :: "'a ⇒ 'a set"
assume "|A| <o natLeq" and "∀a∈A. |F a| <o natLeq"
hence "finite A ∧ (∀a ∈ A. finite(F a))"
by (auto simp add: finite_iff_ordLess_natLeq)
hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F])
thus "|Sigma A F | <o natLeq"
by (auto simp add: finite_iff_ordLess_natLeq)
qed
corollary regularCard_natLeq: "regularCard natLeq"
using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
lemma stable_ordIso1:
assumes ST: "stable r" and ISO: "r' =o r"
shows "stable r'"
proof(unfold stable_def, auto)
fix A::"'b set" and F::"'b ⇒ 'b set"
assume "|A| <o r'" and "∀a ∈ A. |F a| <o r'"
hence "( |A| <o r) ∧ (∀a ∈ A. |F a| <o r)"
using ISO ordLess_ordIso_trans by blast
hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
thus "|SIGMA a : A. F a| <o r'"
using ISO ordIso_symmetric ordLess_ordIso_trans by blast
qed
lemma stable_UNION:
assumes "stable r" and "|A| <o r" and "⋀ a. a ∈ A ⟹ |F a| <o r"
shows "|⋃a ∈ A. F a| <o r"
using assms card_of_UNION_Sigma stable_elim ordLeq_ordLess_trans by blast
corollary card_of_UNION_ordLess_infinite:
assumes "stable |B|" and "|I| <o |B|" and "∀i ∈ I. |A i| <o |B|"
shows "|⋃i ∈ I. A i| <o |B|"
using assms stable_UNION by blast
corollary card_of_UNION_ordLess_infinite_Field:
assumes ST: "stable r" and r: "Card_order r" and
LEQ_I: "|I| <o r" and LEQ: "∀i ∈ I. |A i| <o r"
shows "|⋃i ∈ I. A i| <o r"
proof -
let ?B = "Field r"
have 1: "r =o |?B| ∧ |?B| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|I| <o |?B|" "∀i ∈ I. |A i| <o |?B|"
using LEQ_I LEQ ordLess_ordIso_trans by blast+
moreover have "stable |?B|" using stable_ordIso1 ST 1 by blast
ultimately have "|⋃i ∈ I. A i| <o |?B|" using LEQ
card_of_UNION_ordLess_infinite by blast
thus ?thesis using 1 ordLess_ordIso_trans by blast
qed
end