Quelle  Cardinal_Order_Relation.thy   Sprache: Isabelle

(*  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_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"
    by (metis (mono_tags, lifting) assms inj_onI mem_Collect_eq)
  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_ordLess2:
  "( |A| B < C. |A| =o |B| \ |B|
  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 "\r\R. Card_order r"
  shows "Card_order (omax R)"
  by (simp add: assms omax_in)

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|
  using card_of_Pow[of "UNIV::'a set"] by simp

lemma card_of_Un1[simp]: "|A| \o |A \ B| "
  by fastforce

lemma card_of_diff[simp]: "|A - B| \o |A|"
  by fastforce

lemma subset_ordLeq_strict:
  assumes "A \ B" and "|A|
  shows "A < B"
  using assms ordLess_irreflexive by blast

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

lemma card_of_empty4:
  "|{}::'b set| {})"
  by (metis card_of_empty card_of_ordLess2 image_is_empty not_ordLess_ordLeq)

lemma card_of_empty5:
  "|A| 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|"
  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: 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|"
  by (meson assms card_of_Pow_mono ordIso_iff_ordLeq)

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_of_Un2[simp]:
  shows "|A| \o |B \ A|"
  by fastforce

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

lemma card_of_Un_Plus_ordIso:
  assumes "A Int B = {}"
  shows "|A \ B| =o |A <+> B|"
  by (meson Un_Plus_bij_betw assms card_of_ordIso)

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

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: 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: 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)"] by metis

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: 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 "|\i\I. A i| =o |Sigma I A|"
proof-
  let ?L = "\i\I. 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: 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: 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: card_of_ordIso card_of_Times_infinite)
qed

corollary Times_infinite_bij_betw_types:
  assumes "\finite(UNIV::'a set)" and "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: card_of_ordIso)
qed

corollary Plus_infinite_bij_betw_types:
  assumes "\finite(UNIV::'a set)" and "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|"
  by (simp add: INF LEQ card_of_Un_ordLeq_infinite_Field ordIso_iff_ordLeq)

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|
  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: 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|
  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|  and LESS2: "|B|
  shows "|A \ B|
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:  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: 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: 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|  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_Times_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|
  by (meson card_of_Well_order infinite_iff_card_of_nat not_ordLeq_iff_ordLess)

lemma finite_ordLess_infinite2[simp]:
  assumes "finite A" and "\finite B"
  shows "|A|
  by (meson assms card_of_Well_order card_of_ordLeq_finite not_ordLeq_iff_ordLess)

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|
  shows "|{a} Un A|
  by (metis assms card_of_Un_ordLess_infinite finite.emptyI finite_insert finite_ordLess_infinite2)

lemma card_of_Un_singl_ordLess_infinite:
  assumes "\finite B"
  shows "|A| |{a} Un A|
  using assms card_of_Un_singl_ordLess_infinite1[of B A]
  using card_of_Un2 ordLeq_ordLess_trans by blast


subsection ‹Cardinals versus lists›

text‹The 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_UNION_nlists: "lists A = (\n. nlists A n)"
  unfolding lists_eq_set 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_eq_set 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 (induction n)
  case (Suc 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
  then show ?case  by auto
qed (simp add: nlists_0)

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 clarify
    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(induction n)
  case 0
  have "A \ {}" using assms by auto
  then show ?case
    by (simp add: nlists_0)
next
  case (Suc n)
  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 Suc assms by auto
  ultimately show ?case
    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"
proof -
  { fix a assume "a \ A"
  hence "set [a] \ A \ a \ set [a]" by auto
  hence "\l. set l \ A \ a \ set l" by blast }
  then show ?thesis by force
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 by force

lemma map_lists_surjective:
  assumes "f ` A = B"
  shows "(map f) ` (lists A) = lists B"
  by (metis assms lists_image)

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: 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: 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|"
  by (meson assms card_of_lists_mono ordIso_iff_ordLeq)

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 lists_infinite_bij_betw by fastforce


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"
proof -
  have "\C. \C \ f ` A; finite C\ \ C \ (`) f ` {X. X \ A \ finite X}"
    by (simp add: finite_subset_image image_iff)
  then show ?thesis
    using assms by (force simp add: Fpow_def)
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: 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: 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|"
  by (meson assms card_of_Fpow_mono ordIso_iff_ordLeq)

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_eq_set 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 (auto simp: Field_def natLess_def)

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}"
proof -
  have "\t Field natLeq"
    by (simp add: Field_natLeq)
  moreover have "\xt. (t, x) \ natLeq \ t < n"
    by (simp add: natLeq_def)
  ultimately show ?thesis
    by (auto simp: natLeq_wo_rel wo_rel.ofilter_def under_def)
qed

lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
  by (metis (no_types) atLeastLessThanSuc_atLeastAtMost natLeq_ofilter_less)

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
    then have "A = {0 ..< n}"
    proof(auto simp: 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: 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: 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}"
  by (auto simp: natLeq_on_wo_rel wo_rel.ofilter_def Field_natLeq_on 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..
    by (auto simp: 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 "(\n\m. A = {0 ..< n})"
  thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp: natLeq_on_ofilter_less_eq)
qed

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

lemma natLeq_on_ofilter_less:
  assumes "n < m" shows "ofilter (natLeq_on m) {0 .. n}"
proof -
  have "Suc n \ m"
    using assms by simp
  then show ?thesis
    using natLeq_on_ofilter_iff by auto
qed

lemma natLeq_on_ordLess_natLeq: "natLeq_on n
proof -
  have "well_order natLeq"
    using Field_natLeq natLeq_Well_order by auto
  moreover have "\n. well_order_on {na. na < n} (natLeq_on n)"
    using Field_natLeq_on natLeq_on_Well_order by presburger
  ultimately show ?thesis
    by (simp add: Field_natLeq Field_natLeq_on finite_ordLess_infinite)
qed

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: natLeq_on_Well_order ordIso_reflexive)
  assume "natLeq_on m =o natLeq_on n"
  then obtain f where "bij_betw f {x. x
    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"
  by (meson finite_iff_ordLess_natLeq not_ordLess_ordIso)

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 -
  { fix r assume "well_order_on {x. x < n} r"
    hence "natLeq_on n \o r"
      using finite_atLeastLessThan natLeq_on_well_order_on
        finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
  }
  then show ?thesis
    unfolding card_order_on_def using Field_natLeq_on natLeq_on_Well_order by presburger
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.. id ` {0.. {0.. unfolding inj_on_def by auto
  hence "|{0..o |{0.. 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)
  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: card_of_ordLeq_finite)
qed


subsubsection \<open>"Backward compatibility" with the numeric cardinal operator for finite sets\<close>

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: 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|
proof-
  have "( |A| 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 \<open>The successor of a cardinal\<close>

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_mono_ordLess[simp]:
  assumes CARD: "Card_order r" and CARD': "Card_order r'"
  shows "(cardSuc 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.. 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  using CARD unfolding r_def r'_def using cardSuc_greater by blast
  hence "|Field r|  using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
  hence LESS: "|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'
      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: 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..
        unfolding p_def by (auto simp: 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 "\finite C" and "|A| \o |C|" and "|B| \o |C|"
  shows "|A <+> B| \o |C|"
  by (simp add: assms)

lemma card_of_Un_ordLeq_infinite[simp]:
  assumes "\finite C" and "|A| \o |C|" and "|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 \<open>Others\<close>

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|"
  by (metis Int_absorb2 assms image_vimage_eq order_refl surj_imp_ordLeq)

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

(* 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. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> 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"
        by (smt (verit) Func_def eq f g mem_Collect_eq option.inject)
    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. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
     (\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> 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 \<in> A2 then (if a \<in> 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"
          by (smt (verit) A12 F_def Func_def eq f g mem_Collect_eq subsetD)
      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'. Func_option A' B)| \o |Pow A \ Func_option A B|"
    by (simp add: assms card_of_Func_option_mono card_of_Sigma_mono1)
  finally show ?thesis .
qed

lemma Bpow_ordLeq_Func_Field:
  assumes rc: "Card_order r" and r: "Field r \ {}" and A: "\finite A"
  shows "|Bpow r A| \o |Func (Field r) A|"
proof-
  let ?F = "\ f. {x | x a. f a = x \ a \ Field r}"
  {fix X assume "X \ Bpow r A - {{}}"
    hence XA: "X \ A" and "|X| \o r"
      and X: "X \ {}" unfolding Bpow_def by auto
    hence "|X| \o |Field r|" by (metis Field_card_of card_of_mono2)
    then obtain F where 1: "X = F ` (Field r)"
      using card_of_ordLeq2[OF X] by metis
    define f where [abs_def]: "f i = (if i \ Field r then F i else undefined)" for i
    have "\ f \ Func (Field r) A. X = ?F f"
      apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
  }
  hence "Bpow r A - {{}} \ ?F ` (Func (Field r) A)" by auto
  hence "|Bpow r A - {{}}| \o |Func (Field r) A|"
    by (rule surj_imp_ordLeq)
  moreover
  {have 2: "\finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
    have "|Bpow r A| =o |Bpow r A - {{}}|"
      by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
  }
  ultimately show ?thesis by (metis ordIso_ordLeq_trans)
qed

lemma empty_in_Func[simp]:
  "B \ {} \ (\x. undefined) \ Func {} B"
  by simp

lemma Func_mono[simp]:
  assumes "B1 \ B2"
  shows "Func A B1 \ Func A B2"
  using assms unfolding Func_def by force

lemma Pfunc_mono[simp]:
  assumes "A1 \ A2" and "B1 \ B2"
  shows "Pfunc A B1 \ Pfunc A B2"
  using assms unfolding Pfunc_def
  by (force split: option.split_asm option.split)

lemma card_of_Func_UNIV_UNIV:
  "|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \ 'b) set|"
  using card_of_Func_UNIV[of "UNIV::'b set"] by auto

lemma ordLeq_Func:
  assumes "{b1,b2} \ B" "b1 \ b2"
  shows "|A| \o |Func A B|"
  unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
  let ?F = "\x a. if a \ A then (if a = x then b1 else b2) else undefined"
  show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto
  show "?F ` A \ Func A B" using assms unfolding Func_def by auto
qed

lemma infinite_Func:
  assumes A: "\finite A" and B: "{b1,b2} \ B" "b1 \ b2"
  shows "\finite (Func A B)"
  using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)


subsection \<open>Infinite cardinals are limit ordinals\<close>

lemma card_order_infinite_isLimOrd:
  assumes c: "Card_order r" and i: "\finite (Field r)"
  shows "isLimOrd r"
proof-
  have 0: "wo_rel r" and 00: "Well_order r"
    using c unfolding card_order_on_def wo_rel_def by auto
  hence rr: "Refl r" by (metis wo_rel.REFL)
  show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] 
  proof safe
    fix j assume "j \ Field r" and "\i\Field r. (i, j) \ r"
    then show False
      by (metis Card_order_trans c i infinite_Card_order_limit)
  qed
qed

lemma insert_Chain:
  assumes "Refl r" "C \ Chains r" and "i \ Field r" and "\j. j \ C \ (j,i) \ r \ (i,j) \ r"
  shows "insert i C \ Chains r"
  using assms unfolding Chains_def by (auto dest: refl_onD)

lemma Collect_insert: "{R j |j. j \ insert j1 J} = insert (R j1) {R j |j. j \ J}"
  by auto

lemma Field_init_seg_of[simp]:
  "Field init_seg_of = UNIV"
  unfolding Field_def init_seg_of_def by auto

lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
  unfolding refl_on_def Field_def by auto

lemma regularCard_all_ex:
  assumes r: "Card_order r"   "regularCard r"
    and As: "\ i j b. b \ B \ (i,j) \ r \ P i b \ P j b"
    and Bsub: "\ b \ B. \ i \ Field r. P i b"
    and cardB: "|B|
  shows "\ i \ Field r. \ b \ B. P i b"
proof-
  let ?As = "\i. {b \ B. P i b}"
  have "\i \ Field r. B \ ?As i"
    apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
  thus ?thesis by auto
qed

lemma relChain_stabilize:
  assumes rc: "relChain r As" and AsB: "(\i \ Field r. As i) \ B" and Br: "|B|
    and ir: "\finite (Field r)" and cr: "Card_order r"
  shows "\ i \ Field r. As (succ r i) = As i"
proof(rule ccontr, auto)
  have 0: "wo_rel r" and 00: "Well_order r"
    unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
  have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
  have AsBs: "(\i \ Field r. As (succ r i)) \ B"
    using AsB L by (simp add: "0" Sup_le_iff wo_rel.isLimOrd_succ)
  assume As_s: "\i\Field r. As (succ r i) \ As i"
  have 1: "\i j. (i,j) \ r \ i \ j \ As i \ As j"
  proof safe
    fix i j assume 1: "(i, j) \ r" "i \ j" and Asij: "As i = As j"
    hence rij: "(succ r i, j) \ r" by (metis "0" wo_rel.succ_smallest)
    hence "As (succ r i) \ As j" using rc unfolding relChain_def by auto
    moreover
    { have "(i,succ r i) \ r"
        by (meson "0" "1"(1) FieldI1 L wo_rel.isLimOrd_aboveS wo_rel.succ_in)
      hence "As i \ As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
    }
    ultimately show False unfolding Asij by auto
  qed (insert rc, unfold relChain_def, auto)
  hence "\ i \ Field r. \ a. a \ As (succ r i) - As i"
    using wo_rel.succ_in[OF 0] AsB
    by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
        wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
  then obtain f where f: "\ i \ Field r. f i \ As (succ r i) - As i" by metis
  have "inj_on f (Field r)" unfolding inj_on_def 
  proof safe
    fix i j assume ij: "i \ Field r" "j \ Field r" and fij: "f i = f j"
    show "i = j"
    proof(cases rule: wo_rel.cases_Total3[OF 0], safe)
      assume "(i, j) \ r" and ijd: "i \ j"
      hence rij: "(succ r i, j) \ r" by (metis "0" wo_rel.succ_smallest)
      hence "As (succ r i) \ As j" using rc unfolding relChain_def by auto
      thus "i = j" using ij ijd fij f by auto
    next
      assume "(j, i) \ r" and ijd: "i \ j"
      hence rij: "(succ r j, i) \ r" by (metis "0" wo_rel.succ_smallest)
      hence "As (succ r j) \ As i" using rc unfolding relChain_def by auto
      thus "j = i" using ij ijd fij f by fastforce
    qed(insert ij, auto)
  qed
  moreover have "f ` (Field r) \ B" using f AsBs by auto
  moreover have "|B|  using Br cr by (metis card_of_unique ordLess_ordIso_trans)
  ultimately show False unfolding card_of_ordLess[symmetric] by auto
qed


subsection \<open>Regular vs. stable cardinals\<close>

lemma stable_cardSuc:
  assumes CARD: "Card_order r" and INF: "\finite (Field r)"
  shows "stable(cardSuc r)"
  using infinite_cardSuc_regularCard regularCard_stable
  by (metis CARD INF cardSuc_Card_order cardSuc_finite)

lemma stable_ordIso:
  assumes "r =o r'"
  shows "stable r = stable r'"
  by (metis assms ordIso_symmetric stable_ordIso1)

lemma stable_nat: "stable |UNIV::nat set|"
  using stable_natLeq card_of_nat stable_ordIso by auto

text\<open>Below, the type of "A" is not important -- we just had to choose an appropriate
   type to make "A" possible. What is important is that arbitrarily large
   infinite sets of stable cardinality exist.\<close>

lemma infinite_stable_exists:
  assumes CARD: "\r \ R. Card_order (r::'a rel)"
  shows "\(A :: (nat + 'a set)set).
          \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
proof-
  have "\(A :: (nat + 'a set)set).
          \<not>finite A \<and> stable |A| \<and> |UNIV::'a set|
  proof(cases "finite (UNIV::'a set)")
    case True
    let ?B = "UNIV::nat set"
    have "\finite(?B <+> {})" using finite_Plus_iff by blast
    moreover
    have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast
    hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast
    moreover
    have "\finite(Field |?B| ) \ finite(Field |UNIV::'a set| )" using True by simp
    hence "|UNIV::'a set|  by (simp add: finite_ordLess_infinite)
    hence "|UNIV::'a set| {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast
    ultimately show ?thesis by blast
  next
    case False
    hence *: "\finite(Field |UNIV::'a set| )" by simp
    let ?B = "Field(cardSuc |UNIV::'a set| )"
    have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast
    have 1: "\finite ?B" using False card_of_cardSuc_finite by blast
    hence 2: "\finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast
    have "|?B| =o cardSuc |UNIV::'a set|"
      using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
    moreover have "stable(cardSuc |UNIV::'a set| )"
      using stable_cardSuc * card_of_Card_order by blast
    ultimately have "stable |?B|" using stable_ordIso by blast
    hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast
    have "|UNIV::'a set|
      using card_of_Card_order cardSuc_greater by blast
    moreover have "|?B| =o cardSuc |UNIV::'a set|"
      using card_of_Card_order cardSuc_Card_order  card_of_Field_ordIso by blast
    ultimately have "|UNIV::'a set|
      using ordIso_symmetric ordLess_ordIso_trans by blast
    hence "|UNIV::'a set| ?B|" using 0 ordLess_ordIso_trans by blast
    thus ?thesis using 2 3 by blast
  qed
  thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
qed

corollary infinite_regularCard_exists:
  assumes CARD: "\r \ R. Card_order (r::'a rel)"
  shows "\(A :: (nat + 'a set)set).
          \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
  using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)

end