Theory Cardinal_Order_Relation

(*  Title:      HOL/Cardinals/Cardinal_Order_Relation.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Cardinal-order relations.
*)

section Cardinal-Order Relations

theory Cardinal_Order_Relation
imports Wellorder_Constructions
begin

declare
  card_order_on_well_order_on[simp]
  card_of_card_order_on[simp]
  card_of_well_order_on[simp]
  Field_card_of[simp]
  card_of_Card_order[simp]
  card_of_Well_order[simp]
  card_of_least[simp]
  card_of_unique[simp]
  card_of_mono1[simp]
  card_of_mono2[simp]
  card_of_cong[simp]
  card_of_Field_ordLess[simp]
  card_of_Field_ordIso[simp]
  card_of_underS[simp]
  ordLess_Field[simp]
  card_of_empty[simp]
  card_of_empty1[simp]
  card_of_image[simp]
  card_of_singl_ordLeq[simp]
  Card_order_singl_ordLeq[simp]
  card_of_Pow[simp]
  Card_order_Pow[simp]
  card_of_Plus1[simp]
  Card_order_Plus1[simp]
  card_of_Plus2[simp]
  Card_order_Plus2[simp]
  card_of_Plus_mono1[simp]
  card_of_Plus_mono2[simp]
  card_of_Plus_mono[simp]
  card_of_Plus_cong2[simp]
  card_of_Plus_cong[simp]
  card_of_Un_Plus_ordLeq[simp]
  card_of_Times1[simp]
  card_of_Times2[simp]
  card_of_Times3[simp]
  card_of_Times_mono1[simp]
  card_of_Times_mono2[simp]
  card_of_ordIso_finite[simp]
  card_of_Times_same_infinite[simp]
  card_of_Times_infinite_simps[simp]
  card_of_Plus_infinite1[simp]
  card_of_Plus_infinite2[simp]
  card_of_Plus_ordLess_infinite[simp]
  card_of_Plus_ordLess_infinite_Field[simp]
  infinite_cartesian_product[simp]
  cardSuc_Card_order[simp]
  cardSuc_greater[simp]
  cardSuc_ordLeq[simp]
  cardSuc_ordLeq_ordLess[simp]
  cardSuc_mono_ordLeq[simp]
  cardSuc_invar_ordIso[simp]
  card_of_cardSuc_finite[simp]
  cardSuc_finite[simp]
  card_of_Plus_ordLeq_infinite_Field[simp]
  curr_in[intro, simp]


subsection Cardinal of a set

lemma card_of_inj_rel: assumes INJ: "x y y'. (x,y)  R; (x,y')  R  y = y'"
shows "|{y. x. (x,y)  R}| <=o |{x. y. (x,y)  R}|"
proof-
  let ?Y = "{y. x. (x,y)  R}"  let ?X = "{x. y. (x,y)  R}"
  let ?f = "λy. SOME x. (x,y)  R"
  have "?f ` ?Y <= ?X" by (auto dest: someI)
  moreover have "inj_on ?f ?Y"
  unfolding inj_on_def proof(auto)
    fix y1 x1 y2 x2
    assume *: "(x1, y1)  R" "(x2, y2)  R" and **: "?f y1 = ?f y2"
    hence "(?f y1,y1)  R" using someI[of "λx. (x,y1)  R"] by auto
    moreover have "(?f y2,y2)  R" using * someI[of "λx. (x,y2)  R"] by auto
    ultimately show "y1 = y2" using ** INJ by auto
  qed
  ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast
qed

lemma card_of_unique2: "card_order_on B r; bij_betw f A B  r =o |A|"
using card_of_ordIso card_of_unique ordIso_equivalence by blast

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 internalize_card_of_ordLess2:
"( |A| <o |C| ) = (B < C. |A| =o |B|  |B| <o |C| )"
using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto

lemma Card_order_omax:
assumes "finite R" and "R  {}" and "rR. Card_order r"
shows "Card_order (omax R)"
proof-
  have "rR. Well_order r"
  using assms unfolding card_order_on_def by simp
  thus ?thesis using assms apply - apply(drule omax_in) by auto
qed

lemma Card_order_omax2:
assumes "finite I" and "I  {}"
shows "Card_order (omax {|A i| | i. i  I})"
proof-
  let ?R = "{|A i| | i. i  I}"
  have "finite ?R" and "?R  {}" using assms by auto
  moreover have "r?R. Card_order r"
  using card_of_Card_order by auto
  ultimately show ?thesis by(rule Card_order_omax)
qed


subsection Cardinals versus set operations on arbitrary sets

lemma card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|"
using card_of_Pow[of "UNIV::'a set"] by simp

lemma card_of_Un1[simp]:
shows "|A| ≤o |A  B| "
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce

lemma card_of_diff[simp]:
shows "|A - B| ≤o |A|"
using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce

lemma subset_ordLeq_strict:
assumes "A  B" and "|A| <o |B|"
shows "A < B"
proof-
  {assume "¬(A < B)"
   hence "A = B" using assms(1) by blast
   hence False using assms(2) not_ordLess_ordIso card_of_refl by blast
  }
  thus ?thesis by blast
qed

corollary subset_ordLeq_diff:
assumes "A  B" and "|A| <o |B|"
shows "B - A  {}"
using assms subset_ordLeq_strict by blast

lemma card_of_empty4:
"|{}::'b set| <o |A::'a set| = (A  {})"
proof(intro iffI notI)
  assume *: "|{}::'b set| <o |A|" and "A = {}"
  hence "|A| =o |{}::'b set|"
  using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
  hence "|{}::'b set| =o |A|" using ordIso_symmetric by blast
  with * show False using not_ordLess_ordIso[of "|{}::'b set|" "|A|"] by blast
next
  assume "A  {}"
  hence "(¬ (f. inj_on f A  f ` A  {}))"
  unfolding inj_on_def by blast
  thus "| {} | <o | A |"
  using card_of_ordLess by blast
qed

lemma card_of_empty5:
"|A| <o |B|  B  {}"
using card_of_empty not_ordLess_ordLeq by blast

lemma Well_order_card_of_empty:
"Well_order r  |{}| ≤o r" by simp

lemma card_of_UNIV[simp]:
"|A :: 'a set| ≤o |UNIV :: 'a set|"
using card_of_mono1[of A] by simp

lemma card_of_UNIV2[simp]:
"Card_order r  (r :: 'a rel) ≤o |UNIV :: 'a set|"
using card_of_UNIV[of "Field r"] card_of_Field_ordIso
      ordIso_symmetric ordIso_ordLeq_trans by blast

lemma card_of_Pow_mono[simp]:
assumes "|A| ≤o |B|"
shows "|Pow A| ≤o |Pow B|"
proof-
  obtain f where "inj_on f A  f ` A  B"
  using assms card_of_ordLeq[of A B] by auto
  hence "inj_on (image f) (Pow A)  (image f) ` (Pow A)  (Pow B)"
  by (auto simp add: inj_on_image_Pow image_Pow_mono)
  thus ?thesis using card_of_ordLeq[of "Pow A"] by metis
qed

lemma ordIso_Pow_mono[simp]:
assumes "r ≤o r'"
shows "|Pow(Field r)| ≤o |Pow(Field r')|"
using assms card_of_mono2 card_of_Pow_mono by blast

lemma card_of_Pow_cong[simp]:
assumes "|A| =o |B|"
shows "|Pow A| =o |Pow B|"
proof-
  obtain f where "bij_betw f A B"
  using assms card_of_ordIso[of A B] by auto
  hence "bij_betw (image f) (Pow A) (Pow B)"
  by (auto simp add: bij_betw_image_Pow)
  thus ?thesis using card_of_ordIso[of "Pow A"] by auto
qed

lemma ordIso_Pow_cong[simp]:
assumes "r =o r'"
shows "|Pow(Field r)| =o |Pow(Field r')|"
using assms card_of_cong card_of_Pow_cong by blast

corollary Card_order_Plus_empty1:
"Card_order r  r =o |(Field r) <+> {}|"
using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast

corollary Card_order_Plus_empty2:
"Card_order r  r =o |{} <+> (Field r)|"
using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast

lemma Card_order_Un1:
shows "Card_order r  |Field r| ≤o |(Field r)  B| "
using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto

lemma card_of_Un2[simp]:
shows "|A| ≤o |B  A|"
using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce

lemma Card_order_Un2:
shows "Card_order r  |Field r| ≤o |A  (Field r)| "
using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto

lemma Un_Plus_bij_betw:
assumes "A Int B = {}"
shows "f. bij_betw f (A  B) (A <+> B)"
proof-
  let ?f = "λ c. if c  A then Inl c else Inr c"
  have "bij_betw ?f (A  B) (A <+> B)"
  using assms by(unfold bij_betw_def inj_on_def, auto)
  thus ?thesis by blast
qed

lemma card_of_Un_Plus_ordIso:
assumes "A Int B = {}"
shows "|A  B| =o |A <+> B|"
using assms card_of_ordIso[of "A  B"] Un_Plus_bij_betw[of A B] by auto

lemma card_of_Un_Plus_ordIso1:
"|A  B| =o |A <+> (B - A)|"
using card_of_Un_Plus_ordIso[of A "B - A"] by auto

lemma card_of_Un_Plus_ordIso2:
"|A  B| =o |(A - B) <+> B|"
using card_of_Un_Plus_ordIso[of "A - B" B] by auto

lemma card_of_Times_singl1: "|A| =o |A × {b}|"
proof-
  have "bij_betw fst (A × {b}) A" unfolding bij_betw_def inj_on_def by force
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
qed

corollary Card_order_Times_singl1:
"Card_order r  r =o |(Field r) × {b}|"
using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast

lemma card_of_Times_singl2: "|A| =o |{b} × A|"
proof-
  have "bij_betw snd ({b} × A) A" unfolding bij_betw_def inj_on_def by force
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
qed

corollary Card_order_Times_singl2:
"Card_order r  r =o |{a} × (Field r)|"
using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast

lemma card_of_Times_assoc: "|(A × B) × C| =o |A × B × C|"
proof -
  let ?f = "λ((a,b),c). (a,(b,c))"
  have "A × B × C  ?f ` ((A × B) × C)"
  proof
    fix x assume "x  A × B × C"
    then obtain a b c where *: "a  A" "b  B" "c  C" "x = (a, b, c)" by blast
    let ?x = "((a, b), c)"
    from * have "?x  (A × B) × C" "x = ?f ?x" by auto
    thus "x  ?f ` ((A × B) × C)" by blast
  qed
  hence "bij_betw ?f ((A × B) × C) (A × B × C)"
  unfolding bij_betw_def inj_on_def by auto
  thus ?thesis using card_of_ordIso by blast
qed

corollary Card_order_Times3:
"Card_order r  |Field r| ≤o |(Field r) × (Field r)|"
  by (rule card_of_Times3)

lemma card_of_Times_cong1[simp]:
assumes "|A| =o |B|"
shows "|A × C| =o |B × C|"
using assms by (simp add: ordIso_iff_ordLeq)

lemma card_of_Times_cong2[simp]:
assumes "|A| =o |B|"
shows "|C × A| =o |C × B|"
using assms by (simp add: ordIso_iff_ordLeq)

lemma card_of_Times_mono[simp]:
assumes "|A| ≤o |B|" and "|C| ≤o |D|"
shows "|A × C| ≤o |B × D|"
using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
      ordLeq_transitive[of "|A × C|"] by blast

corollary ordLeq_Times_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_Times_mono by blast

corollary ordIso_Times_cong1[simp]:
assumes "r =o r'"
shows "|(Field r) × C| =o |(Field r') × C|"
using assms card_of_cong card_of_Times_cong1 by blast

corollary ordIso_Times_cong2:
assumes "r =o r'"
shows "|A × (Field r)| =o |A × (Field r')|"
using assms card_of_cong card_of_Times_cong2 by blast

lemma card_of_Times_cong[simp]:
assumes "|A| =o |B|" and "|C| =o |D|"
shows "|A × C| =o |B × D|"
using assms
by (auto simp add: ordIso_iff_ordLeq)

corollary ordIso_Times_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_Times_cong by blast

lemma card_of_Sigma_mono2:
assumes "inj_on f (I::'i set)" and "f ` I  (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"
  obtain u where u_def: "u = (λ(i::'i,a::'a). (f i,a))" by blast
  have "inj_on u ?LEFT  u `?LEFT  ?RIGHT"
  using assms unfolding u_def inj_on_def by auto
  thus ?thesis using card_of_ordLeq by blast
qed

lemma card_of_Sigma_mono:
assumes INJ: "inj_on f I" and IM: "f ` I  J" and
        LEQ: "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 IM LEQ by blast
  hence "|SIGMA i : I. A (f i)| ≤o |SIGMA i : I. B (f i)|"
  using card_of_Sigma_mono1[of I] by metis
  moreover have "|SIGMA i : I. B (f i)| ≤o |SIGMA j : J. B j|"
  using INJ IM card_of_Sigma_mono2 by blast
  ultimately show ?thesis using ordLeq_transitive by blast
qed

lemma ordLeq_Sigma_mono1:
assumes "i  I. p i ≤o r i"
shows "|SIGMA i : I. Field(p i)| ≤o |SIGMA i : I. Field(r i)|"
using assms by (auto simp add: card_of_Sigma_mono1)

lemma ordLeq_Sigma_mono:
assumes "inj_on f I" and "f ` I  J" and
        "j  J. p j ≤o r j"
shows "|SIGMA i : I. Field(p(f i))| ≤o |SIGMA j : J. Field(r j)|"
using assms card_of_mono2 card_of_Sigma_mono
      [of f I J "λ i. Field(p i)" "λ j. Field(r j)"] by metis

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"
  obtain u where u_def: "u = (λ(i::'i,a::'a). (f i,a))" by blast
  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 ordIso_Sigma_cong1:
assumes "i  I. p i =o r i"
shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
using assms by (auto simp add: card_of_Sigma_cong1)

lemma ordLeq_Sigma_cong:
assumes "bij_betw f I J" and
        "j  J. p j =o r j"
shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
using assms card_of_cong card_of_Sigma_cong
      [of f I J "λ j. Field(p j)" "λ j. Field(r j)"] by blast

lemma card_of_UNION_Sigma2:
assumes
"!! i j. {i,j} <= I; i ~= j  A i Int A j = {}"
shows
"|iI. A i| =o |Sigma I A|"
proof-
  let ?L = "iI. A i"  let ?R = "Sigma I A"
  have "|?L| <=o |?R|" using card_of_UNION_Sigma .
  moreover have "|?R| <=o |?L|"
  proof-
    have "inj_on snd ?R"
    unfolding inj_on_def using assms by auto
    moreover have "snd ` ?R <= ?L" by auto
    ultimately show ?thesis using card_of_ordLeq by blast
  qed
  ultimately show ?thesis by(simp add: ordIso_iff_ordLeq)
qed

corollary Plus_into_Times:
assumes A2: "a1  a2  {a1,a2}  A" and
        B2: "b1  b2  {b1,b2}  B"
shows "f. inj_on f (A <+> B)  f ` (A <+> B)  A × B"
using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq)

corollary Plus_into_Times_types:
assumes A2: "(a1::'a)  a2" and  B2: "(b1::'b)  b2"
shows "(f::'a + 'b  'a * 'b). inj f"
using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
by auto

corollary Times_same_infinite_bij_betw:
assumes "¬finite A"
shows "f. bij_betw f (A × A) A"
using assms by (auto simp add: card_of_ordIso)

corollary Times_same_infinite_bij_betw_types:
assumes INF: "¬finite(UNIV::'a set)"
shows "(f::('a * 'a) => 'a). bij f"
using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
by auto

corollary Times_infinite_bij_betw:
assumes INF: "¬finite A" and NE: "B  {}" and INJ: "inj_on g B  g ` B  A"
shows "(f. bij_betw f (A × B) A)  (h. bij_betw h (B × A) A)"
proof-
  have "|B| ≤o |A|" using INJ card_of_ordLeq by blast
  thus ?thesis using INF NE
  by (auto simp add: card_of_ordIso card_of_Times_infinite)
qed

corollary Times_infinite_bij_betw_types:
assumes INF: "¬finite(UNIV::'a set)" and
        BIJ: "inj(g::'b  'a)"
shows "((f::('b * 'a) => 'a). bij f)  ((h::('a * 'b) => 'a). bij h)"
using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
by auto

lemma card_of_Times_ordLeq_infinite:
"¬finite C; |A| ≤o |C|; |B| ≤o |C|
  |A × B| ≤o |C|"
by(simp add: card_of_Sigma_ordLeq_infinite)

corollary Plus_infinite_bij_betw:
assumes INF: "¬finite A" and INJ: "inj_on g B  g ` B  A"
shows "(f. bij_betw f (A <+> B) A)  (h. bij_betw h (B <+> A) A)"
proof-
  have "|B| ≤o |A|" using INJ card_of_ordLeq by blast
  thus ?thesis using INF
  by (auto simp add: card_of_ordIso)
qed

corollary Plus_infinite_bij_betw_types:
assumes INF: "¬finite(UNIV::'a set)" and
        BIJ: "inj(g::'b  'a)"
shows "((f::('b + 'a) => 'a). bij f)  ((h::('a + 'b) => 'a). bij h)"
using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
by auto

lemma card_of_Un_infinite:
assumes INF: "¬finite A" and LEQ: "|B| ≤o |A|"
shows "|A  B| =o |A|  |B  A| =o |A|"
proof-
  have "|A  B| ≤o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
  moreover have "|A <+> B| =o |A|"
  using assms by (metis card_of_Plus_infinite)
  ultimately have "|A  B| ≤o |A|" using ordLeq_ordIso_trans by blast
  hence "|A  B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
  thus ?thesis using Un_commute[of B A] by auto
qed

lemma card_of_Un_infinite_simps[simp]:
"¬finite A; |B| ≤o |A|   |A  B| =o |A|"
"¬finite A; |B| ≤o |A|   |B  A| =o |A|"
using card_of_Un_infinite by auto

lemma card_of_Un_diff_infinite:
assumes INF: "¬finite A" and LESS: "|B| <o |A|"
shows "|A - B| =o |A|"
proof-
  obtain C where C_def: "C = A - B" by blast
  have "|A  B| =o |A|"
  using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
  moreover have "C  B = A  B" unfolding C_def by auto
  ultimately have 1: "|C  B| =o |A|" by auto
  (*  *)
  {assume *: "|C| ≤o |B|"
   moreover
   {assume **: "finite B"
    hence "finite C"
    using card_of_ordLeq_finite * by blast
    hence False using ** INF card_of_ordIso_finite 1 by blast
   }
   hence "¬finite B" by auto
   ultimately have False
   using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
  }
  hence 2: "|B| ≤o |C|" using card_of_Well_order ordLeq_total by blast
  {assume *: "finite C"
    hence "finite B" using card_of_ordLeq_finite 2 by blast
    hence False using * INF card_of_ordIso_finite 1 by blast
  }
  hence "¬finite C" by auto
  hence "|C| =o |A|"
  using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
  thus ?thesis unfolding C_def .
qed

corollary Card_order_Un_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 (auto simp add: card_of_Un_infinite)
  thus ?thesis
  using assms card_of_Field_ordIso[of r]
        ordIso_transitive[of "|Field r  Field p|"]
        ordIso_transitive[of _ "|Field r|"] by blast
qed

corollary subset_ordLeq_diff_infinite:
assumes INF: "¬finite B" and SUB: "A  B" and LESS: "|A| <o |B|"
shows "¬finite (B - A)"
using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast

lemma card_of_Times_ordLess_infinite[simp]:
assumes INF: "¬finite C" and
        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A × B| <o |C|"
proof(cases "A = {}  B = {}")
  assume Case1: "A = {}  B = {}"
  hence "A × B = {}" by blast
  moreover have "C  {}" using
  LESS1 card_of_empty5 by blast
  ultimately show ?thesis by(auto simp add:  card_of_empty4)
next
  assume Case2: "¬(A = {}  B = {})"
  {assume *: "|C| ≤o |A × B|"
   hence "¬finite (A × B)" using INF card_of_ordLeq_finite by blast
   hence 1: "¬finite A  ¬finite B" using finite_cartesian_product by blast
   {assume Case21: "|A| ≤o |B|"
    hence "¬finite B" using 1 card_of_ordLeq_finite by blast
    hence "|A × B| =o |B|" using Case2 Case21
    by (auto simp add: card_of_Times_infinite)
    hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   }
   moreover
   {assume Case22: "|B| ≤o |A|"
    hence "¬finite A" using 1 card_of_ordLeq_finite by blast
    hence "|A × B| =o |A|" using Case2 Case22
    by (auto simp add: card_of_Times_infinite)
    hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   }
   ultimately have False using ordLeq_total card_of_Well_order[of A]
   card_of_Well_order[of B] by blast
  }
  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_Times_ordLess_infinite_Field[simp]:
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_Times_ordLess_infinite by blast
  thus ?thesis using 1 ordLess_ordIso_trans by blast
qed

lemma card_of_Un_ordLess_infinite[simp]:
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[simp]:
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

lemma ordLeq_finite_Field:
assumes "r ≤o s" and "finite (Field s)"
shows "finite (Field r)"
by (metis assms card_of_mono2 card_of_ordLeq_infinite)

lemma ordIso_finite_Field:
assumes "r =o s"
shows "finite (Field r)  finite (Field s)"
by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field)


subsection Cardinals versus set operations involving infinite sets

lemma finite_iff_cardOf_nat:
"finite A = ( |A| <o |UNIV :: nat set| )"
using infinite_iff_card_of_nat[of A]
not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
by fastforce

lemma finite_ordLess_infinite2[simp]:
assumes "finite A" and "¬finite B"
shows "|A| <o |B|"
using assms
finite_ordLess_infinite[of "|A|" "|B|"]
card_of_Well_order[of A] card_of_Well_order[of B]
Field_card_of[of A] Field_card_of[of B] by auto

lemma infinite_card_of_insert:
assumes "¬finite A"
shows "|insert a A| =o |A|"
proof-
  have iA: "insert a A = A  {a}" by simp
  show ?thesis
  using infinite_imp_bij_betw2[OF assms] unfolding iA
  by (metis bij_betw_inv card_of_ordIso)
qed

lemma card_of_Un_singl_ordLess_infinite1:
assumes "¬finite B" and "|A| <o |B|"
shows "|{a} Un A| <o |B|"
proof-
  have "|{a}| <o |B|" using assms by auto
  thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
qed

lemma card_of_Un_singl_ordLess_infinite:
assumes "¬finite B"
shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
using assms card_of_Un_singl_ordLess_infinite1[of B A]
proof(auto)
  assume "|insert a A| <o |B|"
  moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
  ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
qed


subsection Cardinals versus lists

textThe next is an auxiliary operator, which shall be used for inductive
proofs of facts concerning the cardinality of List› :

definition nlists :: "'a set  nat  'a list set"
where "nlists A n  {l. set l  A  length l = n}"

lemma lists_def2: "lists A = {l. set l  A}"
using in_listsI by blast

lemma lists_UNION_nlists: "lists A = (n. nlists A n)"
unfolding lists_def2 nlists_def by blast

lemma card_of_lists: "|A| ≤o |lists A|"
proof-
  let ?h = "λ a. [a]"
  have "inj_on ?h A  ?h ` A  lists A"
  unfolding inj_on_def lists_def2 by auto
  thus ?thesis by (metis card_of_ordLeq)
qed

lemma nlists_0: "nlists A 0 = {[]}"
unfolding nlists_def by auto

lemma nlists_not_empty:
assumes "A  {}"
shows "nlists A n  {}"
proof(induct n, simp add: nlists_0)
  fix n assume "nlists A n  {}"
  then obtain a and l where "a  A  l  nlists A n" using assms by auto
  hence "a # l  nlists A (Suc n)" unfolding nlists_def by auto
  thus "nlists A (Suc n)  {}" by auto
qed

lemma Nil_in_lists: "[]  lists A"
unfolding lists_def2 by auto

lemma lists_not_empty: "lists A  {}"
using Nil_in_lists by blast

lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A × (nlists A n)|"
proof-
  let ?B = "A × (nlists A n)"   let ?h = "λ(a,l). a # l"
  have "inj_on ?h ?B  ?h ` ?B  nlists A (Suc n)"
  unfolding inj_on_def nlists_def by auto
  moreover have "nlists A (Suc n)  ?h ` ?B"
  proof(auto)
    fix l assume "l  nlists A (Suc n)"
    hence 1: "length l = Suc n  set l  A" unfolding nlists_def by auto
    then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
    hence "a  A  set l'  A  length l' = n" using 1 by auto
    thus "l  ?h ` ?B"  using 2 unfolding nlists_def by auto
  qed
  ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
  unfolding bij_betw_def by auto
  thus ?thesis using card_of_ordIso ordIso_symmetric by blast
qed

lemma card_of_nlists_infinite:
assumes "¬finite A"
shows "|nlists A n| ≤o |A|"
proof(induct n)
  have "A  {}" using assms by auto
  thus "|nlists A 0| ≤o |A|" by (simp add: nlists_0)
next
  fix n assume IH: "|nlists A n| ≤o |A|"
  have "|nlists A (Suc n)| =o |A × (nlists A n)|"
  using card_of_nlists_Succ by blast
  moreover
  {have "nlists A n  {}" using assms nlists_not_empty[of A] by blast
   hence "|A × (nlists A n)| =o |A|"
   using assms IH by (auto simp add: card_of_Times_infinite)
  }
  ultimately show "|nlists A (Suc n)| ≤o |A|"
  using ordIso_transitive ordIso_iff_ordLeq by blast
qed

lemma Card_order_lists: "Card_order r  r ≤o |lists(Field r) |"
using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast

lemma Union_set_lists: "(set ` (lists A)) = A"
  unfolding lists_def2
proof(auto)
  fix a assume "a  A"
  hence "set [a]  A  a  set [a]" by auto
  thus "l. set l  A  a  set l" by blast
qed

lemma inj_on_map_lists:
assumes "inj_on f A"
shows "inj_on (map f) (lists A)"
using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto

lemma map_lists_mono:
assumes "f ` A  B"
shows "(map f) ` (lists A)  lists B"
using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :)  *)

lemma map_lists_surjective:
assumes "f ` A = B"
shows "(map f) ` (lists A) = lists B"
using assms unfolding lists_def2
proof (auto, blast)
  fix l' assume *: "set l'  f ` A"
  have "set l'  f ` A  l'  map f ` {l. set l  A}"
  proof(induct l', auto)
    fix l a
    assume "a  A" and "set l  A" and
           IH: "f ` (set l)  f ` A"
    hence "set (a # l)  A" by auto
    hence "map f (a # l)  map f ` {l. set l  A}" by blast
    thus "f a # map f l  map f ` {l. set l  A}" by auto
  qed
  thus "l'  map f ` {l. set l  A}" using * by auto
qed

lemma bij_betw_map_lists:
assumes "bij_betw f A B"
shows "bij_betw (map f) (lists A) (lists B)"
using assms unfolding bij_betw_def
by(auto simp add: inj_on_map_lists map_lists_surjective)

lemma card_of_lists_mono[simp]:
assumes "|A| ≤o |B|"
shows "|lists A| ≤o |lists B|"
proof-
  obtain f where "inj_on f A  f ` A  B"
  using assms card_of_ordLeq[of A B] by auto
  hence "inj_on (map f) (lists A)  (map f) ` (lists A)  (lists B)"
  by (auto simp add: inj_on_map_lists map_lists_mono)
  thus ?thesis using card_of_ordLeq[of "lists A"] by metis
qed

lemma ordIso_lists_mono:
assumes "r ≤o r'"
shows "|lists(Field r)| ≤o |lists(Field r')|"
using assms card_of_mono2 card_of_lists_mono by blast

lemma card_of_lists_cong[simp]:
assumes "|A| =o |B|"
shows "|lists A| =o |lists B|"
proof-
  obtain f where "bij_betw f A B"
  using assms card_of_ordIso[of A B] by auto
  hence "bij_betw (map f) (lists A) (lists B)"
  by (auto simp add: bij_betw_map_lists)
  thus ?thesis using card_of_ordIso[of "lists A"] by auto
qed

lemma card_of_lists_infinite[simp]:
assumes "¬finite A"
shows "|lists A| =o |A|"
proof-
  have "|lists A| ≤o |A|" unfolding lists_UNION_nlists
  by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
    (metis infinite_iff_card_of_nat assms)
  thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
qed

lemma Card_order_lists_infinite:
assumes "Card_order r" and "¬finite(Field r)"
shows "|lists(Field r)| =o r"
using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast

lemma ordIso_lists_cong:
assumes "r =o r'"
shows "|lists(Field r)| =o |lists(Field r')|"
using assms card_of_cong card_of_lists_cong by blast

corollary lists_infinite_bij_betw:
assumes "¬finite A"
shows "f. bij_betw f (lists A) A"
using assms card_of_lists_infinite card_of_ordIso by blast

corollary lists_infinite_bij_betw_types:
assumes "¬finite(UNIV :: 'a set)"
shows "(f::'a list  'a). bij f"
using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
using lists_UNIV by auto


subsection Cardinals versus the finite powerset operator

lemma card_of_Fpow[simp]: "|A| ≤o |Fpow A|"
proof-
  let ?h = "λ a. {a}"
  have "inj_on ?h A  ?h ` A  Fpow A"
  unfolding inj_on_def Fpow_def by auto
  thus ?thesis using card_of_ordLeq by metis
qed

lemma Card_order_Fpow: "Card_order r  r ≤o |Fpow(Field r) |"
using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast

lemma image_Fpow_surjective:
assumes "f ` A = B"
shows "(image f) ` (Fpow A) = Fpow B"
using assms proof(unfold Fpow_def, auto)
  fix Y assume *: "Y  f ` A" and **: "finite Y"
  hence "b  Y. a. a  A  f a = b" by auto
  with bchoice[of Y "λb a. a  A  f a = b"]
  obtain g where 1: "b  Y. g b  A  f(g b) = b" by blast
  obtain X where X_def: "X = g ` Y" by blast
  have "f ` X = Y  X  A  finite X"
  by(unfold X_def, force simp add: ** 1)
  thus "Y  (image f) ` {X. X  A  finite X}" by auto
qed

lemma bij_betw_image_Fpow:
assumes "bij_betw f A B"
shows "bij_betw (image f) (Fpow A) (Fpow B)"
using assms unfolding bij_betw_def
by (auto simp add: inj_on_image_Fpow image_Fpow_surjective)

lemma card_of_Fpow_mono[simp]:
assumes "|A| ≤o |B|"
shows "|Fpow A| ≤o |Fpow B|"
proof-
  obtain f where "inj_on f A  f ` A  B"
  using assms card_of_ordLeq[of A B] by auto
  hence "inj_on (image f) (Fpow A)  (image f) ` (Fpow A)  (Fpow B)"
  by (auto simp add: inj_on_image_Fpow image_Fpow_mono)
  thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto
qed

lemma ordIso_Fpow_mono:
assumes "r ≤o r'"
shows "|Fpow(Field r)| ≤o |Fpow(Field r')|"
using assms card_of_mono2 card_of_Fpow_mono by blast

lemma card_of_Fpow_cong[simp]:
assumes "|A| =o |B|"
shows "|Fpow A| =o |Fpow B|"
proof-
  obtain f where "bij_betw f A B"
  using assms card_of_ordIso[of A B] by auto
  hence "bij_betw (image f) (Fpow A) (Fpow B)"
  by (auto simp add: bij_betw_image_Fpow)
  thus ?thesis using card_of_ordIso[of "Fpow A"] by auto
qed

lemma ordIso_Fpow_cong:
assumes "r =o r'"
shows "|Fpow(Field r)| =o |Fpow(Field r')|"
using assms card_of_cong card_of_Fpow_cong by blast

lemma card_of_Fpow_lists: "|Fpow A| ≤o |lists A|"
proof-
  have "set ` (lists A) = Fpow A"
  unfolding lists_def2 Fpow_def using finite_list finite_set by blast
  thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast
qed

lemma card_of_Fpow_infinite[simp]:
assumes "¬finite A"
shows "|Fpow A| =o |A|"
using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
      ordLeq_ordIso_trans ordIso_iff_ordLeq by blast

corollary Fpow_infinite_bij_betw:
assumes "¬finite A"
shows "f. bij_betw f (Fpow A) A"
using assms card_of_Fpow_infinite card_of_ordIso by blast


subsection The cardinal $\omega$ and the finite cardinals

subsubsection First as well-orders

lemma Field_natLess: "Field natLess = (UNIV::nat set)"
by(unfold Field_def natLess_def, auto)

lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
using natLeq_Well_order Field_natLeq by auto

lemma natLeq_wo_rel: "wo_rel natLeq"
unfolding wo_rel_def using natLeq_Well_order .

lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
   simp add: Field_natLeq, unfold under_def natLeq_def, auto)

lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
   simp add: Field_natLeq, unfold under_def natLeq_def, auto)

lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto

lemma closed_nat_set_iff:
assumes "(m::nat) n. n  A  m  n  m  A"
shows "A = UNIV  (n. A = {0 ..< n})"
proof-
  {assume "A  UNIV" hence "n. n  A" by blast
   moreover obtain n where n_def: "n = (LEAST n. n  A)" by blast
   ultimately have 1: "n  A  (m. m < n  m  A)"
   using LeastI_ex[of "λ n. n  A"] n_def Least_le[of "λ n. n  A"] by fastforce
   have "A = {0 ..< n}"
   proof(auto simp add: 1)
     fix m assume *: "m  A"
     {assume "n  m" with assms * have "n  A" by blast
      hence False using 1 by auto
     }
     thus "m < n" by fastforce
   qed
   hence "n. A = {0 ..< n}" by blast
  }
  thus ?thesis by blast
qed

lemma natLeq_ofilter_iff:
"ofilter natLeq A = (A = UNIV  (n. A = {0 ..< n}))"
proof(rule iffI)
  assume "ofilter natLeq A"
  hence "m n. n  A  m  n  m  A" using natLeq_wo_rel
  by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
  thus "A = UNIV  (n. A = {0 ..< n})" using closed_nat_set_iff by blast
next
  assume "A = UNIV  (n. A = {0 ..< n})"
  thus "ofilter natLeq A"
  by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter)
qed

lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
unfolding under_def natLeq_def by auto

lemma natLeq_on_ofilter_less_eq:
"n  m  wo_rel.ofilter (natLeq_on m) {0 ..< n}"
apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
apply (simp add: Field_natLeq_on)
by (auto simp add: under_def)

lemma natLeq_on_ofilter_iff:
"wo_rel.ofilter (natLeq_on m) A = (n  m. A = {0 ..< n})"
proof(rule iffI)
  assume *: "wo_rel.ofilter (natLeq_on m) A"
  hence 1: "A  {0..<m}"
  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
  hence "n1 n2. n2  A  n1  n2  n1  A"
  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
  hence "A = UNIV  (n. A = {0 ..< n})" using closed_nat_set_iff by blast
  thus "n  m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
next
  assume "(nm. A = {0 ..< n})"
  thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
qed

corollary natLeq_on_ofilter:
"ofilter(natLeq_on n) {0 ..< n}"
by (auto simp add: natLeq_on_ofilter_less_eq)

lemma natLeq_on_ofilter_less:
"n < m  ofilter (natLeq_on m) {0 .. n}"
by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
   simp add: Field_natLeq_on, unfold under_def, auto)

lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
using Field_natLeq Field_natLeq_on[of n]
      finite_ordLess_infinite[of "natLeq_on n" natLeq]
      natLeq_Well_order natLeq_on_Well_order[of n] by auto

lemma natLeq_on_injective:
"natLeq_on m = natLeq_on n  m = n"
using Field_natLeq_on[of m] Field_natLeq_on[of n]
      atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast

lemma natLeq_on_injective_ordIso:
"(natLeq_on m =o natLeq_on n) = (m = n)"
proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
  assume "natLeq_on m =o natLeq_on n"
  then obtain f where "bij_betw f {x. x<m} {x. x<n}"
  using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
  thus "m = n" using atLeastLessThan_injective2[of f m n]
    unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
qed


subsubsection Then as cardinals

lemma ordIso_natLeq_infinite1:
"|A| =o natLeq  ¬finite A"
using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast

lemma ordIso_natLeq_infinite2:
"natLeq =o |A|  ¬finite A"
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast

lemma ordIso_natLeq_on_imp_finite:
"|A| =o natLeq_on n  finite A"
unfolding ordIso_def iso_def[abs_def]
by (auto simp: Field_natLeq_on bij_betw_finite)

lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
proof(unfold card_order_on_def,
      auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
  fix r assume "well_order_on {x. x < n} r"
  thus "natLeq_on n ≤o r"
  using finite_atLeastLessThan natLeq_on_well_order_on
        finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
qed

corollary card_of_Field_natLeq_on:
"|Field (natLeq_on n)| =o natLeq_on n"
using Field_natLeq_on natLeq_on_Card_order
      Card_order_iff_ordIso_card_of[of "natLeq_on n"]
      ordIso_symmetric[of "natLeq_on n"] by blast

corollary card_of_less:
"|{0 ..< n}| =o natLeq_on n"
using Field_natLeq_on card_of_Field_natLeq_on
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto

lemma natLeq_on_ordLeq_less_eq:
"((natLeq_on m) ≤o (natLeq_on n)) = (m  n)"
proof
  assume "natLeq_on m ≤o natLeq_on n"
  then obtain f where "inj_on f {x. x < m}  f ` {x. x < m}  {x. x < n}"
  unfolding ordLeq_def using
    embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
     embed_Field Field_natLeq_on by blast
  thus "m  n" using atLeastLessThan_less_eq2
    unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
next
  assume "m  n"
  hence "inj_on id {0..<m}  id ` {0..<m}  {0..<n}" unfolding inj_on_def by auto
  hence "|{0..<m}| ≤o |{0..<n}|" using card_of_ordLeq by blast
  thus "natLeq_on m ≤o natLeq_on n"
  using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
qed

lemma natLeq_on_ordLeq_less:
"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
   natLeq_on_ordLeq_less_eq[of n m] by linarith

lemma ordLeq_natLeq_on_imp_finite:
assumes "|A| ≤o natLeq_on n"
shows "finite A"
proof-
  have "|A| ≤o |{0 ..< n}|"
  using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
  thus ?thesis by (auto simp add: card_of_ordLeq_finite)
qed


subsubsection "Backward compatibility" with the numeric cardinal operator for finite sets

lemma finite_card_of_iff_card2:
assumes FIN: "finite A" and FIN': "finite B"
shows "( |A| ≤o |B| ) = (card A  card B)"
using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast

lemma finite_imp_card_of_natLeq_on:
assumes "finite A"
shows "|A| =o natLeq_on (card A)"
proof-
  obtain h where "bij_betw h A {0 ..< card A}"
  using assms ex_bij_betw_finite_nat by blast
  thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
qed

lemma finite_iff_card_of_natLeq_on:
"finite A = (n. |A| =o natLeq_on n)"
using finite_imp_card_of_natLeq_on[of A]
by(auto simp add: ordIso_natLeq_on_imp_finite)

lemma finite_card_of_iff_card:
assumes FIN: "finite A" and FIN': "finite B"
shows "( |A| =o |B| ) = (card A = card B)"
using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast

lemma finite_card_of_iff_card3:
assumes FIN: "finite A" and FIN': "finite B"
shows "( |A| <o |B| ) = (card A < card B)"
proof-
  have "( |A| <o |B| ) = (~ ( |B| ≤o |A| ))" by simp
  also have "... = (~ (card B  card A))"
  using assms by(simp add: finite_card_of_iff_card2)
  also have "... = (card A < card B)" by auto
  finally show ?thesis .
qed

lemma card_Field_natLeq_on:
"card(Field(natLeq_on n)) = n"
using Field_natLeq_on card_atLeastLessThan by auto


subsection The successor of a cardinal

lemma embed_implies_ordIso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
shows "r' =o Restr r (f ` (Field r'))"
using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast

lemma cardSuc_Well_order[simp]:
"Card_order r  Well_order(cardSuc r)"
using cardSuc_Card_order unfolding card_order_on_def by blast

lemma Field_cardSuc_not_empty:
assumes "Card_order r"
shows "Field (cardSuc r)  {}"
proof
  assume "Field(cardSuc r) = {}"
  hence "|Field(cardSuc r)| ≤o r" using assms Card_order_empty[of r] by auto
  hence "cardSuc r ≤o r" using assms card_of_Field_ordIso
  cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
  thus False using cardSuc_greater not_ordLess_ordLeq assms by blast
qed

lemma cardSuc_mono_ordLess[simp]:
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 auto
  thus ?thesis
  using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
  using cardSuc_mono_ordLeq[of r' r] assms by blast
qed

lemma cardSuc_natLeq_on_Suc:
"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
proof-
  obtain r r' p where r_def: "r = natLeq_on n" and
                      r'_def: "r' = cardSuc(natLeq_on n)"  and
                      p_def: "p = natLeq_on(Suc n)" by blast
  (* Preliminary facts:  *)
  have CARD: "Card_order r  Card_order r'  Card_order p" unfolding r_def r'_def p_def
  using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
  hence WELL: "Well_order r  Well_order r'   Well_order p"
  unfolding card_order_on_def by force
  have FIELD: "Field r = {0..<n}  Field p = {0..<(Suc n)}"
  unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
  hence FIN: "finite (Field r)" by force
  have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
  hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
  hence LESS: "|Field r| <o |Field r'|"
  using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
  (* Main proof: *)
  have "r' ≤o p" using CARD unfolding r_def r'_def p_def
  using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
  moreover have "p ≤o r'"
  proof-
    {assume "r' <o p"
     then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
     let ?q = "Restr p (f ` Field r')"
     have 1: "embed r' p f" using 0 unfolding embedS_def by force
     hence 2: "f ` Field r' < {0..<(Suc n)}"
     using WELL FIELD 0 by (auto simp add: embedS_iff)
     have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
     then obtain m where "m  Suc n" and 3: "f ` (Field r') = {0..<m}"
     unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
     hence 4: "m  n" using 2 by force
     (*  *)
     have "bij_betw f (Field r') (f ` (Field r'))"
     using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
     moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
     ultimately have 5: "finite (Field r')  card(Field r') = card (f ` (Field r'))"
     using bij_betw_same_card bij_betw_finite by metis
     hence "card(Field r')  card(Field r)" using 3 4 FIELD by force
     hence "|Field r'| ≤o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
     hence False using LESS not_ordLess_ordLeq by auto
    }
    thus ?thesis using WELL CARD by fastforce
  qed
  ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
qed

lemma card_of_Plus_ordLeq_infinite[simp]:
assumes C: "¬finite C" and A: "|A| ≤o |C|" and B: "|B| ≤o |C|"
shows "|A <+> B| ≤o |C|"
proof-
  let ?r = "cardSuc |C|"
  have "Card_order ?r  ¬finite (Field ?r)" using assms by simp
  moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
  ultimately have "|A <+> B| <o ?r"
  using card_of_Plus_ordLess_infinite_Field by blast
  thus ?thesis using C by simp
qed

lemma card_of_Un_ordLeq_infinite[simp]:
assumes C: "¬finite C" and A: "|A| ≤o |C|" and B: "|B| ≤o |C|"
shows "|A Un B| ≤o |C|"
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
ordLeq_transitive by metis


subsection Others

lemma under_mono[simp]:
assumes "Well_order r" and "(i,j)  r"
shows "under r i  under r j"
using assms unfolding under_def order_on_defs
trans_def by blast

lemma underS_under:
assumes "i  Field r"
shows "underS r i = under r i - {i}"
using assms unfolding underS_def under_def by auto

lemma relChain_under:
assumes "Well_order r"
shows "relChain r (λ i. under r i)"
using assms unfolding relChain_def by auto

lemma card_of_infinite_diff_finite:
assumes "¬finite A" and "finite B"
shows "|A - B| =o |A|"
by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)

lemma infinite_card_of_diff_singl:
assumes "¬finite A"
shows "|A - {a}| =o |A|"
by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)

lemma card_of_vimage:
assumes "B  range f"
shows "|B| ≤o |f -` B|"
apply(rule surj_imp_ordLeq[of _ f])
using assms by (metis Int_absorb2 image_vimage_eq order_refl)

lemma surj_card_of_vimage:
assumes "surj f"
shows "|B| ≤o |f -` B|"
by (metis assms card_of_vimage subset_UNIV)

lemma infinite_Pow:
assumes "¬ finite A"
shows "¬ finite (Pow A)"
proof-
  have "|A| ≤o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
  thus ?thesis by (metis assms finite_Pow_iff)
qed

(* bounded powerset *)
definition Bpow where
"Bpow r A  {X . X  A  |X| ≤o r}"

lemma Bpow_empty[simp]:
assumes "Card_order r"
shows "Bpow r {} = {{}}"
using assms unfolding Bpow_def by auto

lemma singl_in_Bpow:
assumes rc: "Card_order r"
and r: "Field r  {}" and a: "a  A"
shows "{a}  Bpow r A"
proof-
  have "|{a}| ≤o r" using r rc by auto
  thus ?thesis unfolding Bpow_def using a by auto
qed

lemma ordLeq_card_Bpow:
assumes rc: "Card_order r" and r: "Field r  {}"
shows "|A| ≤o |Bpow r A|"
proof-
  have "inj_on (λ a. {a}) A" unfolding inj_on_def by auto
  moreover have "(λ a. {a}) ` A  Bpow r A"
  using singl_in_Bpow[OF assms] by auto
  ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast
qed

lemma infinite_Bpow:
assumes rc: "Card_order r" and r: "Field r  {}"
and A: "¬finite A"
shows "¬finite (Bpow r A)"
using ordLeq_card_Bpow[OF rc r]
by (metis A card_of_ordLeq_infinite)

definition Func_option where
 "Func_option A B 
  {f. ( a. f a  None  a  A)  ( a  A. case f a of Some b  b  B |None  True)}"

lemma card_of_Func_option_Func:
"|Func_option A B| =o |Func A B|"
proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI)
  let ?F = "λ f a. if a  A then Some (f a) else None"
  show "bij_betw ?F (Func A B) (Func_option A B)"
  unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI)
    fix f g assume f: "f  Func A B" and g: "g  Func A B" and eq: "?F f = ?F g"
    show "f = g"
    proof(rule ext)
      fix a
      show "f a = g a"
      proof(cases "a  A")
        case True
        have "Some (f a) = ?F f a" using True by auto
        also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE)
        also have "... = Some (g a)" using True by auto
        finally have "Some (f a) = Some (g a)" .
        thus ?thesis by simp
      qed(insert f g, unfold Func_def, auto)
    qed
  next
    show "?F ` Func A B = Func_option A B"
    proof safe
      fix f assume f: "f  Func_option A B"
      define g where [abs_def]: "g a = (case f a of Some b  b | None  undefined)" for a
      have "g  Func A B"
      using f unfolding g_def Func_def Func_option_def by force+
      moreover have "f = ?F g"
      proof(rule ext)
        fix a show "f a = ?F g a"
        using f unfolding Func_option_def g_def by (cases "a  A") force+
      qed
      ultimately show "f  ?F ` (Func A B)" by blast
    qed(unfold Func_def Func_option_def, auto)
  qed
qed

(* partial-function space: *)
definition Pfunc where
"Pfunc A B 
 {f. (a. f a  None  a  A) 
     (a. case f a of None  True | Some b  b  B)}"

lemma Func_Pfunc:
"Func_option A B  Pfunc A B"
unfolding Func_option_def Pfunc_def by auto

lemma Pfunc_Func_option:
"Pfunc A B = (A'  Pow A. Func_option A' B)"
proof safe
  fix f assume f: "f  Pfunc A B"
  show "f  (A'Pow A. Func_option A' B)"
  proof (intro UN_I)
    let ?A' = "{a. f a  None}"
    show "?A'  Pow A" using f unfolding Pow_def Pfunc_def by auto
    show "f  Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto
  qed
next
  fix f A' assume "f  Func_option A' B" and "A'  A"
  thus "f  Pfunc A B" unfolding Func_option_def Pfunc_def by auto
qed

lemma card_of_Func_mono:
fixes A1 A2 :: "'a set" and B :: "'b set"
assumes A12: "A1  A2" and B: "B  {}"
shows "|Func A1 B| ≤o |Func A2 B|"
proof-
  obtain bb where bb: "bb  B" using B by auto
  define F where [abs_def]: "F f1 a =
    (if a  A2 then (if a  A1 then f1 a else bb) else undefined)" for f1 :: "'a  'b" and a
  show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI)
    show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe
      fix f g assume f: "f  Func A1 B" and g: "g  Func A1 B" and eq: "F f = F g"
      show "f = g"
      proof(rule ext)
        fix a show "f a = g a"
        proof(cases "a  A1")
          case True
          thus ?thesis using eq A12 unfolding F_def fun_eq_iff
          by (elim allE[of _ a]) auto
        qed(insert f g, unfold Func_def, fastforce)
      qed
    qed
  qed(insert bb, unfold Func_def F_def, force)
qed

lemma card_of_Func_option_mono:
fixes A1 A2 :: "'a set" and B :: "'b set"
assumes A12: "A1  A2" and B: "B  {}"
shows "|Func_option A1 B| ≤o |Func_option A2 B|"
by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func
  ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric)

lemma card_of_Pfunc_Pow_Func_option:
assumes "B  {}"
shows "|Pfunc A B| ≤o |Pow A × Func_option A B|"
proof-
  have "|Pfunc A B| =o |A'  Pow A. Func_option A' B|" (is "_ =o ?K")
    unfolding Pfunc_Func_option by(rule card_of_refl)
  also have "?K ≤o |Sigma (Pow A) (λ A'. Func_option A' B)|" using card_of_UNION_Sigma .
  also have "|Sigma (Pow A) (λ A'.