SSL BNF_Cardinal_Order_Relation.thy

(*  Title:      HOL/BNF_Cardinal_Order_Relation.thy
  Author: Andrei Popescu, TU Muenchen
  Author: Jan van Brügge, TU Muenchen
  Copyright 2012, 2022
 
 Cardinal-order relations as needed by bounded natural functors.
*)

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, ‹🚫›), 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 ‹🚫›, 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" (‹(‹open_block notation=‹mixfix card_of›\›|_|)›)
  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|
    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|
proof -
  have "(¬(∃f. inj_on f A ∧ f ` A ≤ B)) = (¬ |A| ≤o |B| )"
    using card_of_ordLeq by blast
  also have "… = ( |B|
    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|
  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)
  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|
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'
    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
  shows "|Field 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|
  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
  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 🍋‹"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'  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|  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|
      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 × ?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  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  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|  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›,
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
proof (intro conjI)
  show "natLeq ⊆ Field natLeq × Field natLeq"
    unfolding natLeq_def Field_def by blast
next
  show "Refl natLeq"
    using natLeq_Refl .
next
  show "trans natLeq"
    using natLeq_trans .
qed

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  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|
  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 ∧
         (∀(r''::'a set rel). Card_order r'' ∧ 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
  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
  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 ] ==> 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
  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'
    then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' ∧ r''
      using internalize_ordLess[of r' ?p] by blast
        (*  *)
    have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
    moreover have "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')"
proof 
  show "cardSuc r ≤o r' ==> 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 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
  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|  and LESS2: "|B|
  shows "|A <+> B|
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|  and LESS2: "|B|
  shows "|A <+> B|
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|   "|B|
    using LESS1 LESS2 ordLess_ordIso_trans by blast+
  hence  "|A <+> B|  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|  and "|B|  using A B c
    by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
  ultimately have "|A <+> B|
    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|  and LESS2: "|B|
  shows "|A ∪ B|
  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|  and LESS2: "|B|
  shows "|A Un B|
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|   "|B|
    using LESS1 LESS2 ordLess_ordIso_trans by blast+
  hence  "|A Un B|  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|
  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|  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
    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|
      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|
          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|  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|  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|
    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| ∧ (∀a ∈ A. |F a|
               ⟶ |SIGMA a : A. F a|

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|  and F: "∀a∈A. |F a|
  {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|  using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
      hence "|f ` L|  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|
    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|
    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|  using K card_of_underS[OF cr] subsetD by auto
      hence "|SIGMA a: K. underS r a|  using st Kr unfolding stable_def by auto
    }
    finally have "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| ∃B < Field r. |A| =o |B| ∧ |B|
proof
  assume "|A|
  then obtain p where 1: "Field p < Field r ∧ |A| =o p ∧ p
    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|
    using 1 ordIso_equivalence ordIso_ordLess_trans by blast
  thus "∃B < Field r. |A| =o |B| ∧ |B|  using 1 by blast
next
  assume "∃B < Field r. |A| =o |B| ∧ |B|
  thus "|A|  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

(* Note that below the types of A and F are now unconstrained: *)
lemma stable_elim:
  assumes ST: "stable r" and A_LESS: "|A|  and
    F_LESS: "∧ a. a ∈ A ==> |F a|
  shows "|SIGMA a : A. F a|
proof -
  obtain A' where 1: "A' < Field r ∧ |A'|  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'|
      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|
    using bchoice[of A "λ a B'. B' ≤ Field r ∧ |F a| =o |B'| ∧ |B'| ] by blast
  hence 4: "∀a ∈ A. F' a ≤ Field r ∧ |F' a|  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')|
    using 3 4 bij_betw_ball[of G A' A] by auto
  hence "|SIGMA a' : A'. F'(G a')|
    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|  and "∀a∈A. |F a|
  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 |
    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|  and "∀a ∈ A. |F a|
  hence "( |A| ∧ (∀a ∈ A. |F a|
    using ISO ordLess_ordIso_trans by blast
  hence "|SIGMA a : A. F a|  using assms stable_elim by blast
  thus "|SIGMA a : A. F a|
    using ISO ordIso_symmetric ordLess_ordIso_trans by blast
qed

lemma stable_UNION:
  assumes "stable r" and "|A|  and "∧ a. a ∈ A ==> |F a|
  shows "|∪a ∈ A. F a|
  using assms card_of_UNION_Sigma stable_elim ordLeq_ordLess_trans by blast

corollary card_of_UNION_ordLess_infinite:
  assumes "stable |B|" and "|I|  and "∀i ∈ I. |A i|
  shows "|∪i ∈ I. A i|
  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|  and LEQ: "∀i ∈ I. |A i|
  shows "|∪i ∈ I. A i|
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|   "∀i ∈ I. |A i|
    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|  using LEQ
      card_of_UNION_ordLess_infinite by blast
  thus ?thesis using 1 ordLess_ordIso_trans by blast
qed

end