src/HOL/Cardinals/Cardinal_Order_Relation.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66453 cc19f7ca2ed6
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Cardinals/Cardinal_Order_Relation.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 Cardinal-order relations.
     6 *)
     7 
     8 section \<open>Cardinal-Order Relations\<close>
     9 
    10 theory Cardinal_Order_Relation
    11 imports HOL.BNF_Cardinal_Order_Relation Wellorder_Constructions
    12 begin
    13 
    14 declare
    15   card_order_on_well_order_on[simp]
    16   card_of_card_order_on[simp]
    17   card_of_well_order_on[simp]
    18   Field_card_of[simp]
    19   card_of_Card_order[simp]
    20   card_of_Well_order[simp]
    21   card_of_least[simp]
    22   card_of_unique[simp]
    23   card_of_mono1[simp]
    24   card_of_mono2[simp]
    25   card_of_cong[simp]
    26   card_of_Field_ordLess[simp]
    27   card_of_Field_ordIso[simp]
    28   card_of_underS[simp]
    29   ordLess_Field[simp]
    30   card_of_empty[simp]
    31   card_of_empty1[simp]
    32   card_of_image[simp]
    33   card_of_singl_ordLeq[simp]
    34   Card_order_singl_ordLeq[simp]
    35   card_of_Pow[simp]
    36   Card_order_Pow[simp]
    37   card_of_Plus1[simp]
    38   Card_order_Plus1[simp]
    39   card_of_Plus2[simp]
    40   Card_order_Plus2[simp]
    41   card_of_Plus_mono1[simp]
    42   card_of_Plus_mono2[simp]
    43   card_of_Plus_mono[simp]
    44   card_of_Plus_cong2[simp]
    45   card_of_Plus_cong[simp]
    46   card_of_Un_Plus_ordLeq[simp]
    47   card_of_Times1[simp]
    48   card_of_Times2[simp]
    49   card_of_Times3[simp]
    50   card_of_Times_mono1[simp]
    51   card_of_Times_mono2[simp]
    52   card_of_ordIso_finite[simp]
    53   card_of_Times_same_infinite[simp]
    54   card_of_Times_infinite_simps[simp]
    55   card_of_Plus_infinite1[simp]
    56   card_of_Plus_infinite2[simp]
    57   card_of_Plus_ordLess_infinite[simp]
    58   card_of_Plus_ordLess_infinite_Field[simp]
    59   infinite_cartesian_product[simp]
    60   cardSuc_Card_order[simp]
    61   cardSuc_greater[simp]
    62   cardSuc_ordLeq[simp]
    63   cardSuc_ordLeq_ordLess[simp]
    64   cardSuc_mono_ordLeq[simp]
    65   cardSuc_invar_ordIso[simp]
    66   card_of_cardSuc_finite[simp]
    67   cardSuc_finite[simp]
    68   card_of_Plus_ordLeq_infinite_Field[simp]
    69   curr_in[intro, simp]
    70 
    71 
    72 subsection \<open>Cardinal of a set\<close>
    73 
    74 lemma card_of_inj_rel: assumes INJ: "!! x y y'. \<lbrakk>(x,y) : R; (x,y') : R\<rbrakk> \<Longrightarrow> y = y'"
    75 shows "|{y. EX x. (x,y) : R}| <=o |{x. EX y. (x,y) : R}|"
    76 proof-
    77   let ?Y = "{y. EX x. (x,y) : R}"  let ?X = "{x. EX y. (x,y) : R}"
    78   let ?f = "% y. SOME x. (x,y) : R"
    79   have "?f ` ?Y <= ?X" by (auto dest: someI)
    80   moreover have "inj_on ?f ?Y"
    81   unfolding inj_on_def proof(auto)
    82     fix y1 x1 y2 x2
    83     assume *: "(x1, y1) \<in> R" "(x2, y2) \<in> R" and **: "?f y1 = ?f y2"
    84     hence "(?f y1,y1) : R" using someI[of "% x. (x,y1) : R"] by auto
    85     moreover have "(?f y2,y2) : R" using * someI[of "% x. (x,y2) : R"] by auto
    86     ultimately show "y1 = y2" using ** INJ by auto
    87   qed
    88   ultimately show "|?Y| <=o |?X|" using card_of_ordLeq by blast
    89 qed
    90 
    91 lemma card_of_unique2: "\<lbrakk>card_order_on B r; bij_betw f A B\<rbrakk> \<Longrightarrow> r =o |A|"
    92 using card_of_ordIso card_of_unique ordIso_equivalence by blast
    93 
    94 lemma internalize_card_of_ordLess:
    95 "( |A| <o r) = (\<exists>B < Field r. |A| =o |B| \<and> |B| <o r)"
    96 proof
    97   assume "|A| <o r"
    98   then obtain p where 1: "Field p < Field r \<and> |A| =o p \<and> p <o r"
    99   using internalize_ordLess[of "|A|" r] by blast
   100   hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
   101   hence "|Field p| =o p" using card_of_Field_ordIso by blast
   102   hence "|A| =o |Field p| \<and> |Field p| <o r"
   103   using 1 ordIso_equivalence ordIso_ordLess_trans by blast
   104   thus "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r" using 1 by blast
   105 next
   106   assume "\<exists>B < Field r. |A| =o |B| \<and> |B| <o r"
   107   thus "|A| <o r" using ordIso_ordLess_trans by blast
   108 qed
   109 
   110 lemma internalize_card_of_ordLess2:
   111 "( |A| <o |C| ) = (\<exists>B < C. |A| =o |B| \<and> |B| <o |C| )"
   112 using internalize_card_of_ordLess[of "A" "|C|"] Field_card_of[of C] by auto
   113 
   114 lemma Card_order_omax:
   115 assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Card_order r"
   116 shows "Card_order (omax R)"
   117 proof-
   118   have "\<forall>r\<in>R. Well_order r"
   119   using assms unfolding card_order_on_def by simp
   120   thus ?thesis using assms apply - apply(drule omax_in) by auto
   121 qed
   122 
   123 lemma Card_order_omax2:
   124 assumes "finite I" and "I \<noteq> {}"
   125 shows "Card_order (omax {|A i| | i. i \<in> I})"
   126 proof-
   127   let ?R = "{|A i| | i. i \<in> I}"
   128   have "finite ?R" and "?R \<noteq> {}" using assms by auto
   129   moreover have "\<forall>r\<in>?R. Card_order r"
   130   using card_of_Card_order by auto
   131   ultimately show ?thesis by(rule Card_order_omax)
   132 qed
   133 
   134 
   135 subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
   136 
   137 lemma card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|"
   138 using card_of_Pow[of "UNIV::'a set"] by simp
   139 
   140 lemma card_of_Un1[simp]:
   141 shows "|A| \<le>o |A \<union> B| "
   142 using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
   143 
   144 lemma card_of_diff[simp]:
   145 shows "|A - B| \<le>o |A|"
   146 using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce
   147 
   148 lemma subset_ordLeq_strict:
   149 assumes "A \<le> B" and "|A| <o |B|"
   150 shows "A < B"
   151 proof-
   152   {assume "\<not>(A < B)"
   153    hence "A = B" using assms(1) by blast
   154    hence False using assms(2) not_ordLess_ordIso card_of_refl by blast
   155   }
   156   thus ?thesis by blast
   157 qed
   158 
   159 corollary subset_ordLeq_diff:
   160 assumes "A \<le> B" and "|A| <o |B|"
   161 shows "B - A \<noteq> {}"
   162 using assms subset_ordLeq_strict by blast
   163 
   164 lemma card_of_empty4:
   165 "|{}::'b set| <o |A::'a set| = (A \<noteq> {})"
   166 proof(intro iffI notI)
   167   assume *: "|{}::'b set| <o |A|" and "A = {}"
   168   hence "|A| =o |{}::'b set|"
   169   using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
   170   hence "|{}::'b set| =o |A|" using ordIso_symmetric by blast
   171   with * show False using not_ordLess_ordIso[of "|{}::'b set|" "|A|"] by blast
   172 next
   173   assume "A \<noteq> {}"
   174   hence "(\<not> (\<exists>f. inj_on f A \<and> f ` A \<subseteq> {}))"
   175   unfolding inj_on_def by blast
   176   thus "| {} | <o | A |"
   177   using card_of_ordLess by blast
   178 qed
   179 
   180 lemma card_of_empty5:
   181 "|A| <o |B| \<Longrightarrow> B \<noteq> {}"
   182 using card_of_empty not_ordLess_ordLeq by blast
   183 
   184 lemma Well_order_card_of_empty:
   185 "Well_order r \<Longrightarrow> |{}| \<le>o r" by simp
   186 
   187 lemma card_of_UNIV[simp]:
   188 "|A :: 'a set| \<le>o |UNIV :: 'a set|"
   189 using card_of_mono1[of A] by simp
   190 
   191 lemma card_of_UNIV2[simp]:
   192 "Card_order r \<Longrightarrow> (r :: 'a rel) \<le>o |UNIV :: 'a set|"
   193 using card_of_UNIV[of "Field r"] card_of_Field_ordIso
   194       ordIso_symmetric ordIso_ordLeq_trans by blast
   195 
   196 lemma card_of_Pow_mono[simp]:
   197 assumes "|A| \<le>o |B|"
   198 shows "|Pow A| \<le>o |Pow B|"
   199 proof-
   200   obtain f where "inj_on f A \<and> f ` A \<le> B"
   201   using assms card_of_ordLeq[of A B] by auto
   202   hence "inj_on (image f) (Pow A) \<and> (image f) ` (Pow A) \<le> (Pow B)"
   203   by (auto simp add: inj_on_image_Pow image_Pow_mono)
   204   thus ?thesis using card_of_ordLeq[of "Pow A"] by metis
   205 qed
   206 
   207 lemma ordIso_Pow_mono[simp]:
   208 assumes "r \<le>o r'"
   209 shows "|Pow(Field r)| \<le>o |Pow(Field r')|"
   210 using assms card_of_mono2 card_of_Pow_mono by blast
   211 
   212 lemma card_of_Pow_cong[simp]:
   213 assumes "|A| =o |B|"
   214 shows "|Pow A| =o |Pow B|"
   215 proof-
   216   obtain f where "bij_betw f A B"
   217   using assms card_of_ordIso[of A B] by auto
   218   hence "bij_betw (image f) (Pow A) (Pow B)"
   219   by (auto simp add: bij_betw_image_Pow)
   220   thus ?thesis using card_of_ordIso[of "Pow A"] by auto
   221 qed
   222 
   223 lemma ordIso_Pow_cong[simp]:
   224 assumes "r =o r'"
   225 shows "|Pow(Field r)| =o |Pow(Field r')|"
   226 using assms card_of_cong card_of_Pow_cong by blast
   227 
   228 corollary Card_order_Plus_empty1:
   229 "Card_order r \<Longrightarrow> r =o |(Field r) <+> {}|"
   230 using card_of_Plus_empty1 card_of_Field_ordIso ordIso_equivalence by blast
   231 
   232 corollary Card_order_Plus_empty2:
   233 "Card_order r \<Longrightarrow> r =o |{} <+> (Field r)|"
   234 using card_of_Plus_empty2 card_of_Field_ordIso ordIso_equivalence by blast
   235 
   236 lemma Card_order_Un1:
   237 shows "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<union> B| "
   238 using card_of_Un1 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
   239 
   240 lemma card_of_Un2[simp]:
   241 shows "|A| \<le>o |B \<union> A|"
   242 using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
   243 
   244 lemma Card_order_Un2:
   245 shows "Card_order r \<Longrightarrow> |Field r| \<le>o |A \<union> (Field r)| "
   246 using card_of_Un2 card_of_Field_ordIso ordIso_symmetric ordIso_ordLeq_trans by auto
   247 
   248 lemma Un_Plus_bij_betw:
   249 assumes "A Int B = {}"
   250 shows "\<exists>f. bij_betw f (A \<union> B) (A <+> B)"
   251 proof-
   252   let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
   253   have "bij_betw ?f (A \<union> B) (A <+> B)"
   254   using assms by(unfold bij_betw_def inj_on_def, auto)
   255   thus ?thesis by blast
   256 qed
   257 
   258 lemma card_of_Un_Plus_ordIso:
   259 assumes "A Int B = {}"
   260 shows "|A \<union> B| =o |A <+> B|"
   261 using assms card_of_ordIso[of "A \<union> B"] Un_Plus_bij_betw[of A B] by auto
   262 
   263 lemma card_of_Un_Plus_ordIso1:
   264 "|A \<union> B| =o |A <+> (B - A)|"
   265 using card_of_Un_Plus_ordIso[of A "B - A"] by auto
   266 
   267 lemma card_of_Un_Plus_ordIso2:
   268 "|A \<union> B| =o |(A - B) <+> B|"
   269 using card_of_Un_Plus_ordIso[of "A - B" B] by auto
   270 
   271 lemma card_of_Times_singl1: "|A| =o |A \<times> {b}|"
   272 proof-
   273   have "bij_betw fst (A \<times> {b}) A" unfolding bij_betw_def inj_on_def by force
   274   thus ?thesis using card_of_ordIso ordIso_symmetric by blast
   275 qed
   276 
   277 corollary Card_order_Times_singl1:
   278 "Card_order r \<Longrightarrow> r =o |(Field r) \<times> {b}|"
   279 using card_of_Times_singl1[of _ b] card_of_Field_ordIso ordIso_equivalence by blast
   280 
   281 lemma card_of_Times_singl2: "|A| =o |{b} \<times> A|"
   282 proof-
   283   have "bij_betw snd ({b} \<times> A) A" unfolding bij_betw_def inj_on_def by force
   284   thus ?thesis using card_of_ordIso ordIso_symmetric by blast
   285 qed
   286 
   287 corollary Card_order_Times_singl2:
   288 "Card_order r \<Longrightarrow> r =o |{a} \<times> (Field r)|"
   289 using card_of_Times_singl2[of _ a] card_of_Field_ordIso ordIso_equivalence by blast
   290 
   291 lemma card_of_Times_assoc: "|(A \<times> B) \<times> C| =o |A \<times> B \<times> C|"
   292 proof -
   293   let ?f = "\<lambda>((a,b),c). (a,(b,c))"
   294   have "A \<times> B \<times> C \<subseteq> ?f ` ((A \<times> B) \<times> C)"
   295   proof
   296     fix x assume "x \<in> A \<times> B \<times> C"
   297     then obtain a b c where *: "a \<in> A" "b \<in> B" "c \<in> C" "x = (a, b, c)" by blast
   298     let ?x = "((a, b), c)"
   299     from * have "?x \<in> (A \<times> B) \<times> C" "x = ?f ?x" by auto
   300     thus "x \<in> ?f ` ((A \<times> B) \<times> C)" by blast
   301   qed
   302   hence "bij_betw ?f ((A \<times> B) \<times> C) (A \<times> B \<times> C)"
   303   unfolding bij_betw_def inj_on_def by auto
   304   thus ?thesis using card_of_ordIso by blast
   305 qed
   306 
   307 corollary Card_order_Times3:
   308 "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
   309   by (rule card_of_Times3)
   310 
   311 lemma card_of_Times_cong1[simp]:
   312 assumes "|A| =o |B|"
   313 shows "|A \<times> C| =o |B \<times> C|"
   314 using assms by (simp add: ordIso_iff_ordLeq)
   315 
   316 lemma card_of_Times_cong2[simp]:
   317 assumes "|A| =o |B|"
   318 shows "|C \<times> A| =o |C \<times> B|"
   319 using assms by (simp add: ordIso_iff_ordLeq)
   320 
   321 lemma card_of_Times_mono[simp]:
   322 assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
   323 shows "|A \<times> C| \<le>o |B \<times> D|"
   324 using assms card_of_Times_mono1[of A B C] card_of_Times_mono2[of C D B]
   325       ordLeq_transitive[of "|A \<times> C|"] by blast
   326 
   327 corollary ordLeq_Times_mono:
   328 assumes "r \<le>o r'" and "p \<le>o p'"
   329 shows "|(Field r) \<times> (Field p)| \<le>o |(Field r') \<times> (Field p')|"
   330 using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Times_mono by blast
   331 
   332 corollary ordIso_Times_cong1[simp]:
   333 assumes "r =o r'"
   334 shows "|(Field r) \<times> C| =o |(Field r') \<times> C|"
   335 using assms card_of_cong card_of_Times_cong1 by blast
   336 
   337 corollary ordIso_Times_cong2:
   338 assumes "r =o r'"
   339 shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
   340 using assms card_of_cong card_of_Times_cong2 by blast
   341 
   342 lemma card_of_Times_cong[simp]:
   343 assumes "|A| =o |B|" and "|C| =o |D|"
   344 shows "|A \<times> C| =o |B \<times> D|"
   345 using assms
   346 by (auto simp add: ordIso_iff_ordLeq)
   347 
   348 corollary ordIso_Times_cong:
   349 assumes "r =o r'" and "p =o p'"
   350 shows "|(Field r) \<times> (Field p)| =o |(Field r') \<times> (Field p')|"
   351 using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Times_cong by blast
   352 
   353 lemma card_of_Sigma_mono2:
   354 assumes "inj_on f (I::'i set)" and "f ` I \<le> (J::'j set)"
   355 shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| \<le>o |SIGMA j : J. A j|"
   356 proof-
   357   let ?LEFT = "SIGMA i : I. A (f i)"
   358   let ?RIGHT = "SIGMA j : J. A j"
   359   obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
   360   have "inj_on u ?LEFT \<and> u `?LEFT \<le> ?RIGHT"
   361   using assms unfolding u_def inj_on_def by auto
   362   thus ?thesis using card_of_ordLeq by blast
   363 qed
   364 
   365 lemma card_of_Sigma_mono:
   366 assumes INJ: "inj_on f I" and IM: "f ` I \<le> J" and
   367         LEQ: "\<forall>j \<in> J. |A j| \<le>o |B j|"
   368 shows "|SIGMA i : I. A (f i)| \<le>o |SIGMA j : J. B j|"
   369 proof-
   370   have "\<forall>i \<in> I. |A(f i)| \<le>o |B(f i)|"
   371   using IM LEQ by blast
   372   hence "|SIGMA i : I. A (f i)| \<le>o |SIGMA i : I. B (f i)|"
   373   using card_of_Sigma_mono1[of I] by metis
   374   moreover have "|SIGMA i : I. B (f i)| \<le>o |SIGMA j : J. B j|"
   375   using INJ IM card_of_Sigma_mono2 by blast
   376   ultimately show ?thesis using ordLeq_transitive by blast
   377 qed
   378 
   379 lemma ordLeq_Sigma_mono1:
   380 assumes "\<forall>i \<in> I. p i \<le>o r i"
   381 shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
   382 using assms by (auto simp add: card_of_Sigma_mono1)
   383 
   384 lemma ordLeq_Sigma_mono:
   385 assumes "inj_on f I" and "f ` I \<le> J" and
   386         "\<forall>j \<in> J. p j \<le>o r j"
   387 shows "|SIGMA i : I. Field(p(f i))| \<le>o |SIGMA j : J. Field(r j)|"
   388 using assms card_of_mono2 card_of_Sigma_mono
   389       [of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
   390 
   391 lemma card_of_Sigma_cong1:
   392 assumes "\<forall>i \<in> I. |A i| =o |B i|"
   393 shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
   394 using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
   395 
   396 lemma card_of_Sigma_cong2:
   397 assumes "bij_betw f (I::'i set) (J::'j set)"
   398 shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| =o |SIGMA j : J. A j|"
   399 proof-
   400   let ?LEFT = "SIGMA i : I. A (f i)"
   401   let ?RIGHT = "SIGMA j : J. A j"
   402   obtain u where u_def: "u = (\<lambda>(i::'i,a::'a). (f i,a))" by blast
   403   have "bij_betw u ?LEFT ?RIGHT"
   404   using assms unfolding u_def bij_betw_def inj_on_def by auto
   405   thus ?thesis using card_of_ordIso by blast
   406 qed
   407 
   408 lemma card_of_Sigma_cong:
   409 assumes BIJ: "bij_betw f I J" and
   410         ISO: "\<forall>j \<in> J. |A j| =o |B j|"
   411 shows "|SIGMA i : I. A (f i)| =o |SIGMA j : J. B j|"
   412 proof-
   413   have "\<forall>i \<in> I. |A(f i)| =o |B(f i)|"
   414   using ISO BIJ unfolding bij_betw_def by blast
   415   hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1)
   416   moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
   417   using BIJ card_of_Sigma_cong2 by blast
   418   ultimately show ?thesis using ordIso_transitive by blast
   419 qed
   420 
   421 lemma ordIso_Sigma_cong1:
   422 assumes "\<forall>i \<in> I. p i =o r i"
   423 shows "|SIGMA i : I. Field(p i)| =o |SIGMA i : I. Field(r i)|"
   424 using assms by (auto simp add: card_of_Sigma_cong1)
   425 
   426 lemma ordLeq_Sigma_cong:
   427 assumes "bij_betw f I J" and
   428         "\<forall>j \<in> J. p j =o r j"
   429 shows "|SIGMA i : I. Field(p(f i))| =o |SIGMA j : J. Field(r j)|"
   430 using assms card_of_cong card_of_Sigma_cong
   431       [of f I J "\<lambda> j. Field(p j)" "\<lambda> j. Field(r j)"] by blast
   432 
   433 lemma card_of_UNION_Sigma2:
   434 assumes
   435 "!! i j. \<lbrakk>{i,j} <= I; i ~= j\<rbrakk> \<Longrightarrow> A i Int A j = {}"
   436 shows
   437 "|\<Union>i\<in>I. A i| =o |Sigma I A|"
   438 proof-
   439   let ?L = "\<Union>i\<in>I. A i"  let ?R = "Sigma I A"
   440   have "|?L| <=o |?R|" using card_of_UNION_Sigma .
   441   moreover have "|?R| <=o |?L|"
   442   proof-
   443     have "inj_on snd ?R"
   444     unfolding inj_on_def using assms by auto
   445     moreover have "snd ` ?R <= ?L" by auto
   446     ultimately show ?thesis using card_of_ordLeq by blast
   447   qed
   448   ultimately show ?thesis by(simp add: ordIso_iff_ordLeq)
   449 qed
   450 
   451 corollary Plus_into_Times:
   452 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
   453         B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
   454 shows "\<exists>f. inj_on f (A <+> B) \<and> f ` (A <+> B) \<le> A \<times> B"
   455 using assms by (auto simp add: card_of_Plus_Times card_of_ordLeq)
   456 
   457 corollary Plus_into_Times_types:
   458 assumes A2: "(a1::'a) \<noteq> a2" and  B2: "(b1::'b) \<noteq> b2"
   459 shows "\<exists>(f::'a + 'b \<Rightarrow> 'a * 'b). inj f"
   460 using assms Plus_into_Times[of a1 a2 UNIV b1 b2 UNIV]
   461 by auto
   462 
   463 corollary Times_same_infinite_bij_betw:
   464 assumes "\<not>finite A"
   465 shows "\<exists>f. bij_betw f (A \<times> A) A"
   466 using assms by (auto simp add: card_of_ordIso)
   467 
   468 corollary Times_same_infinite_bij_betw_types:
   469 assumes INF: "\<not>finite(UNIV::'a set)"
   470 shows "\<exists>(f::('a * 'a) => 'a). bij f"
   471 using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
   472 by auto
   473 
   474 corollary Times_infinite_bij_betw:
   475 assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
   476 shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
   477 proof-
   478   have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
   479   thus ?thesis using INF NE
   480   by (auto simp add: card_of_ordIso card_of_Times_infinite)
   481 qed
   482 
   483 corollary Times_infinite_bij_betw_types:
   484 assumes INF: "\<not>finite(UNIV::'a set)" and
   485         BIJ: "inj(g::'b \<Rightarrow> 'a)"
   486 shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
   487 using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
   488 by auto
   489 
   490 lemma card_of_Times_ordLeq_infinite:
   491 "\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
   492  \<Longrightarrow> |A \<times> B| \<le>o |C|"
   493 by(simp add: card_of_Sigma_ordLeq_infinite)
   494 
   495 corollary Plus_infinite_bij_betw:
   496 assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
   497 shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
   498 proof-
   499   have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
   500   thus ?thesis using INF
   501   by (auto simp add: card_of_ordIso)
   502 qed
   503 
   504 corollary Plus_infinite_bij_betw_types:
   505 assumes INF: "\<not>finite(UNIV::'a set)" and
   506         BIJ: "inj(g::'b \<Rightarrow> 'a)"
   507 shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
   508 using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
   509 by auto
   510 
   511 lemma card_of_Un_infinite:
   512 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
   513 shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
   514 proof-
   515   have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
   516   moreover have "|A <+> B| =o |A|"
   517   using assms by (metis card_of_Plus_infinite)
   518   ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
   519   hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
   520   thus ?thesis using Un_commute[of B A] by auto
   521 qed
   522 
   523 lemma card_of_Un_infinite_simps[simp]:
   524 "\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
   525 "\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
   526 using card_of_Un_infinite by auto
   527 
   528 lemma card_of_Un_diff_infinite:
   529 assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
   530 shows "|A - B| =o |A|"
   531 proof-
   532   obtain C where C_def: "C = A - B" by blast
   533   have "|A \<union> B| =o |A|"
   534   using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
   535   moreover have "C \<union> B = A \<union> B" unfolding C_def by auto
   536   ultimately have 1: "|C \<union> B| =o |A|" by auto
   537   (*  *)
   538   {assume *: "|C| \<le>o |B|"
   539    moreover
   540    {assume **: "finite B"
   541     hence "finite C"
   542     using card_of_ordLeq_finite * by blast
   543     hence False using ** INF card_of_ordIso_finite 1 by blast
   544    }
   545    hence "\<not>finite B" by auto
   546    ultimately have False
   547    using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
   548   }
   549   hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast
   550   {assume *: "finite C"
   551     hence "finite B" using card_of_ordLeq_finite 2 by blast
   552     hence False using * INF card_of_ordIso_finite 1 by blast
   553   }
   554   hence "\<not>finite C" by auto
   555   hence "|C| =o |A|"
   556   using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
   557   thus ?thesis unfolding C_def .
   558 qed
   559 
   560 corollary Card_order_Un_infinite:
   561 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
   562         LEQ: "p \<le>o r"
   563 shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
   564 proof-
   565   have "| Field r \<union> Field p | =o | Field r | \<and>
   566         | Field p \<union> Field r | =o | Field r |"
   567   using assms by (auto simp add: card_of_Un_infinite)
   568   thus ?thesis
   569   using assms card_of_Field_ordIso[of r]
   570         ordIso_transitive[of "|Field r \<union> Field p|"]
   571         ordIso_transitive[of _ "|Field r|"] by blast
   572 qed
   573 
   574 corollary subset_ordLeq_diff_infinite:
   575 assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
   576 shows "\<not>finite (B - A)"
   577 using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
   578 
   579 lemma card_of_Times_ordLess_infinite[simp]:
   580 assumes INF: "\<not>finite C" and
   581         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
   582 shows "|A \<times> B| <o |C|"
   583 proof(cases "A = {} \<or> B = {}")
   584   assume Case1: "A = {} \<or> B = {}"
   585   hence "A \<times> B = {}" by blast
   586   moreover have "C \<noteq> {}" using
   587   LESS1 card_of_empty5 by blast
   588   ultimately show ?thesis by(auto simp add:  card_of_empty4)
   589 next
   590   assume Case2: "\<not>(A = {} \<or> B = {})"
   591   {assume *: "|C| \<le>o |A \<times> B|"
   592    hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
   593    hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
   594    {assume Case21: "|A| \<le>o |B|"
   595     hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
   596     hence "|A \<times> B| =o |B|" using Case2 Case21
   597     by (auto simp add: card_of_Times_infinite)
   598     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   599    }
   600    moreover
   601    {assume Case22: "|B| \<le>o |A|"
   602     hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
   603     hence "|A \<times> B| =o |A|" using Case2 Case22
   604     by (auto simp add: card_of_Times_infinite)
   605     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   606    }
   607    ultimately have False using ordLeq_total card_of_Well_order[of A]
   608    card_of_Well_order[of B] by blast
   609   }
   610   thus ?thesis using ordLess_or_ordLeq[of "|A \<times> B|" "|C|"]
   611   card_of_Well_order[of "A \<times> B"] card_of_Well_order[of "C"] by auto
   612 qed
   613 
   614 lemma card_of_Times_ordLess_infinite_Field[simp]:
   615 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   616         LESS1: "|A| <o r" and LESS2: "|B| <o r"
   617 shows "|A \<times> B| <o r"
   618 proof-
   619   let ?C  = "Field r"
   620   have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
   621   ordIso_symmetric by blast
   622   hence "|A| <o |?C|"  "|B| <o |?C|"
   623   using LESS1 LESS2 ordLess_ordIso_trans by blast+
   624   hence  "|A \<times> B| <o |?C|" using INF
   625   card_of_Times_ordLess_infinite by blast
   626   thus ?thesis using 1 ordLess_ordIso_trans by blast
   627 qed
   628 
   629 lemma card_of_Un_ordLess_infinite[simp]:
   630 assumes INF: "\<not>finite C" and
   631         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
   632 shows "|A \<union> B| <o |C|"
   633 using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
   634       ordLeq_ordLess_trans by blast
   635 
   636 lemma card_of_Un_ordLess_infinite_Field[simp]:
   637 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   638         LESS1: "|A| <o r" and LESS2: "|B| <o r"
   639 shows "|A Un B| <o r"
   640 proof-
   641   let ?C  = "Field r"
   642   have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
   643   ordIso_symmetric by blast
   644   hence "|A| <o |?C|"  "|B| <o |?C|"
   645   using LESS1 LESS2 ordLess_ordIso_trans by blast+
   646   hence  "|A Un B| <o |?C|" using INF
   647   card_of_Un_ordLess_infinite by blast
   648   thus ?thesis using 1 ordLess_ordIso_trans by blast
   649 qed
   650 
   651 lemma ordLeq_finite_Field:
   652 assumes "r \<le>o s" and "finite (Field s)"
   653 shows "finite (Field r)"
   654 by (metis assms card_of_mono2 card_of_ordLeq_infinite)
   655 
   656 lemma ordIso_finite_Field:
   657 assumes "r =o s"
   658 shows "finite (Field r) \<longleftrightarrow> finite (Field s)"
   659 by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field)
   660 
   661 
   662 subsection \<open>Cardinals versus set operations involving infinite sets\<close>
   663 
   664 lemma finite_iff_cardOf_nat:
   665 "finite A = ( |A| <o |UNIV :: nat set| )"
   666 using infinite_iff_card_of_nat[of A]
   667 not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
   668 by fastforce
   669 
   670 lemma finite_ordLess_infinite2[simp]:
   671 assumes "finite A" and "\<not>finite B"
   672 shows "|A| <o |B|"
   673 using assms
   674 finite_ordLess_infinite[of "|A|" "|B|"]
   675 card_of_Well_order[of A] card_of_Well_order[of B]
   676 Field_card_of[of A] Field_card_of[of B] by auto
   677 
   678 lemma infinite_card_of_insert:
   679 assumes "\<not>finite A"
   680 shows "|insert a A| =o |A|"
   681 proof-
   682   have iA: "insert a A = A \<union> {a}" by simp
   683   show ?thesis
   684   using infinite_imp_bij_betw2[OF assms] unfolding iA
   685   by (metis bij_betw_inv card_of_ordIso)
   686 qed
   687 
   688 lemma card_of_Un_singl_ordLess_infinite1:
   689 assumes "\<not>finite B" and "|A| <o |B|"
   690 shows "|{a} Un A| <o |B|"
   691 proof-
   692   have "|{a}| <o |B|" using assms by auto
   693   thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
   694 qed
   695 
   696 lemma card_of_Un_singl_ordLess_infinite:
   697 assumes "\<not>finite B"
   698 shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
   699 using assms card_of_Un_singl_ordLess_infinite1[of B A]
   700 proof(auto)
   701   assume "|insert a A| <o |B|"
   702   moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
   703   ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
   704 qed
   705 
   706 
   707 subsection \<open>Cardinals versus lists\<close>
   708 
   709 text\<open>The next is an auxiliary operator, which shall be used for inductive
   710 proofs of facts concerning the cardinality of \<open>List\<close> :\<close>
   711 
   712 definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set"
   713 where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
   714 
   715 lemma lists_def2: "lists A = {l. set l \<le> A}"
   716 using in_listsI by blast
   717 
   718 lemma lists_UNION_nlists: "lists A = (\<Union>n. nlists A n)"
   719 unfolding lists_def2 nlists_def by blast
   720 
   721 lemma card_of_lists: "|A| \<le>o |lists A|"
   722 proof-
   723   let ?h = "\<lambda> a. [a]"
   724   have "inj_on ?h A \<and> ?h ` A \<le> lists A"
   725   unfolding inj_on_def lists_def2 by auto
   726   thus ?thesis by (metis card_of_ordLeq)
   727 qed
   728 
   729 lemma nlists_0: "nlists A 0 = {[]}"
   730 unfolding nlists_def by auto
   731 
   732 lemma nlists_not_empty:
   733 assumes "A \<noteq> {}"
   734 shows "nlists A n \<noteq> {}"
   735 proof(induct n, simp add: nlists_0)
   736   fix n assume "nlists A n \<noteq> {}"
   737   then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto
   738   hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto
   739   thus "nlists A (Suc n) \<noteq> {}" by auto
   740 qed
   741 
   742 lemma Nil_in_lists: "[] \<in> lists A"
   743 unfolding lists_def2 by auto
   744 
   745 lemma lists_not_empty: "lists A \<noteq> {}"
   746 using Nil_in_lists by blast
   747 
   748 lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
   749 proof-
   750   let ?B = "A \<times> (nlists A n)"   let ?h = "\<lambda>(a,l). a # l"
   751   have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)"
   752   unfolding inj_on_def nlists_def by auto
   753   moreover have "nlists A (Suc n) \<le> ?h ` ?B"
   754   proof(auto)
   755     fix l assume "l \<in> nlists A (Suc n)"
   756     hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto
   757     then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
   758     hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto
   759     thus "l \<in> ?h ` ?B"  using 2 unfolding nlists_def by auto
   760   qed
   761   ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
   762   unfolding bij_betw_def by auto
   763   thus ?thesis using card_of_ordIso ordIso_symmetric by blast
   764 qed
   765 
   766 lemma card_of_nlists_infinite:
   767 assumes "\<not>finite A"
   768 shows "|nlists A n| \<le>o |A|"
   769 proof(induct n)
   770   have "A \<noteq> {}" using assms by auto
   771   thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
   772 next
   773   fix n assume IH: "|nlists A n| \<le>o |A|"
   774   have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
   775   using card_of_nlists_Succ by blast
   776   moreover
   777   {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
   778    hence "|A \<times> (nlists A n)| =o |A|"
   779    using assms IH by (auto simp add: card_of_Times_infinite)
   780   }
   781   ultimately show "|nlists A (Suc n)| \<le>o |A|"
   782   using ordIso_transitive ordIso_iff_ordLeq by blast
   783 qed
   784 
   785 lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
   786 using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
   787 
   788 lemma Union_set_lists: "\<Union>(set ` (lists A)) = A"
   789   unfolding lists_def2
   790 proof(auto)
   791   fix a assume "a \<in> A"
   792   hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
   793   thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
   794 qed
   795 
   796 lemma inj_on_map_lists:
   797 assumes "inj_on f A"
   798 shows "inj_on (map f) (lists A)"
   799 using assms Union_set_lists[of A] inj_on_mapI[of f "lists A"] by auto
   800 
   801 lemma map_lists_mono:
   802 assumes "f ` A \<le> B"
   803 shows "(map f) ` (lists A) \<le> lists B"
   804 using assms unfolding lists_def2 by (auto, blast) (* lethal combination of methods :)  *)
   805 
   806 lemma map_lists_surjective:
   807 assumes "f ` A = B"
   808 shows "(map f) ` (lists A) = lists B"
   809 using assms unfolding lists_def2
   810 proof (auto, blast)
   811   fix l' assume *: "set l' \<le> f ` A"
   812   have "set l' \<le> f ` A \<longrightarrow> l' \<in> map f ` {l. set l \<le> A}"
   813   proof(induct l', auto)
   814     fix l a
   815     assume "a \<in> A" and "set l \<le> A" and
   816            IH: "f ` (set l) \<le> f ` A"
   817     hence "set (a # l) \<le> A" by auto
   818     hence "map f (a # l) \<in> map f ` {l. set l \<le> A}" by blast
   819     thus "f a # map f l \<in> map f ` {l. set l \<le> A}" by auto
   820   qed
   821   thus "l' \<in> map f ` {l. set l \<le> A}" using * by auto
   822 qed
   823 
   824 lemma bij_betw_map_lists:
   825 assumes "bij_betw f A B"
   826 shows "bij_betw (map f) (lists A) (lists B)"
   827 using assms unfolding bij_betw_def
   828 by(auto simp add: inj_on_map_lists map_lists_surjective)
   829 
   830 lemma card_of_lists_mono[simp]:
   831 assumes "|A| \<le>o |B|"
   832 shows "|lists A| \<le>o |lists B|"
   833 proof-
   834   obtain f where "inj_on f A \<and> f ` A \<le> B"
   835   using assms card_of_ordLeq[of A B] by auto
   836   hence "inj_on (map f) (lists A) \<and> (map f) ` (lists A) \<le> (lists B)"
   837   by (auto simp add: inj_on_map_lists map_lists_mono)
   838   thus ?thesis using card_of_ordLeq[of "lists A"] by metis
   839 qed
   840 
   841 lemma ordIso_lists_mono:
   842 assumes "r \<le>o r'"
   843 shows "|lists(Field r)| \<le>o |lists(Field r')|"
   844 using assms card_of_mono2 card_of_lists_mono by blast
   845 
   846 lemma card_of_lists_cong[simp]:
   847 assumes "|A| =o |B|"
   848 shows "|lists A| =o |lists B|"
   849 proof-
   850   obtain f where "bij_betw f A B"
   851   using assms card_of_ordIso[of A B] by auto
   852   hence "bij_betw (map f) (lists A) (lists B)"
   853   by (auto simp add: bij_betw_map_lists)
   854   thus ?thesis using card_of_ordIso[of "lists A"] by auto
   855 qed
   856 
   857 lemma card_of_lists_infinite[simp]:
   858 assumes "\<not>finite A"
   859 shows "|lists A| =o |A|"
   860 proof-
   861   have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
   862   by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
   863     (metis infinite_iff_card_of_nat assms)
   864   thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
   865 qed
   866 
   867 lemma Card_order_lists_infinite:
   868 assumes "Card_order r" and "\<not>finite(Field r)"
   869 shows "|lists(Field r)| =o r"
   870 using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
   871 
   872 lemma ordIso_lists_cong:
   873 assumes "r =o r'"
   874 shows "|lists(Field r)| =o |lists(Field r')|"
   875 using assms card_of_cong card_of_lists_cong by blast
   876 
   877 corollary lists_infinite_bij_betw:
   878 assumes "\<not>finite A"
   879 shows "\<exists>f. bij_betw f (lists A) A"
   880 using assms card_of_lists_infinite card_of_ordIso by blast
   881 
   882 corollary lists_infinite_bij_betw_types:
   883 assumes "\<not>finite(UNIV :: 'a set)"
   884 shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
   885 using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
   886 using lists_UNIV by auto
   887 
   888 
   889 subsection \<open>Cardinals versus the set-of-finite-sets operator\<close>
   890 
   891 definition Fpow :: "'a set \<Rightarrow> 'a set set"
   892 where "Fpow A \<equiv> {X. X \<le> A \<and> finite X}"
   893 
   894 lemma Fpow_mono: "A \<le> B \<Longrightarrow> Fpow A \<le> Fpow B"
   895 unfolding Fpow_def by auto
   896 
   897 lemma empty_in_Fpow: "{} \<in> Fpow A"
   898 unfolding Fpow_def by auto
   899 
   900 lemma Fpow_not_empty: "Fpow A \<noteq> {}"
   901 using empty_in_Fpow by blast
   902 
   903 lemma Fpow_subset_Pow: "Fpow A \<le> Pow A"
   904 unfolding Fpow_def by auto
   905 
   906 lemma card_of_Fpow[simp]: "|A| \<le>o |Fpow A|"
   907 proof-
   908   let ?h = "\<lambda> a. {a}"
   909   have "inj_on ?h A \<and> ?h ` A \<le> Fpow A"
   910   unfolding inj_on_def Fpow_def by auto
   911   thus ?thesis using card_of_ordLeq by metis
   912 qed
   913 
   914 lemma Card_order_Fpow: "Card_order r \<Longrightarrow> r \<le>o |Fpow(Field r) |"
   915 using card_of_Fpow card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
   916 
   917 lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}"
   918 unfolding Fpow_def Pow_def by blast
   919 
   920 lemma inj_on_image_Fpow:
   921 assumes "inj_on f A"
   922 shows "inj_on (image f) (Fpow A)"
   923 using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
   924       inj_on_image_Pow by blast
   925 
   926 lemma image_Fpow_mono:
   927 assumes "f ` A \<le> B"
   928 shows "(image f) ` (Fpow A) \<le> Fpow B"
   929 using assms by(unfold Fpow_def, auto)
   930 
   931 lemma image_Fpow_surjective:
   932 assumes "f ` A = B"
   933 shows "(image f) ` (Fpow A) = Fpow B"
   934 using assms proof(unfold Fpow_def, auto)
   935   fix Y assume *: "Y \<le> f ` A" and **: "finite Y"
   936   hence "\<forall>b \<in> Y. \<exists>a. a \<in> A \<and> f a = b" by auto
   937   with bchoice[of Y "\<lambda>b a. a \<in> A \<and> f a = b"]
   938   obtain g where 1: "\<forall>b \<in> Y. g b \<in> A \<and> f(g b) = b" by blast
   939   obtain X where X_def: "X = g ` Y" by blast
   940   have "f ` X = Y \<and> X \<le> A \<and> finite X"
   941   by(unfold X_def, force simp add: ** 1)
   942   thus "Y \<in> (image f) ` {X. X \<le> A \<and> finite X}" by auto
   943 qed
   944 
   945 lemma bij_betw_image_Fpow:
   946 assumes "bij_betw f A B"
   947 shows "bij_betw (image f) (Fpow A) (Fpow B)"
   948 using assms unfolding bij_betw_def
   949 by (auto simp add: inj_on_image_Fpow image_Fpow_surjective)
   950 
   951 lemma card_of_Fpow_mono[simp]:
   952 assumes "|A| \<le>o |B|"
   953 shows "|Fpow A| \<le>o |Fpow B|"
   954 proof-
   955   obtain f where "inj_on f A \<and> f ` A \<le> B"
   956   using assms card_of_ordLeq[of A B] by auto
   957   hence "inj_on (image f) (Fpow A) \<and> (image f) ` (Fpow A) \<le> (Fpow B)"
   958   by (auto simp add: inj_on_image_Fpow image_Fpow_mono)
   959   thus ?thesis using card_of_ordLeq[of "Fpow A"] by auto
   960 qed
   961 
   962 lemma ordIso_Fpow_mono:
   963 assumes "r \<le>o r'"
   964 shows "|Fpow(Field r)| \<le>o |Fpow(Field r')|"
   965 using assms card_of_mono2 card_of_Fpow_mono by blast
   966 
   967 lemma card_of_Fpow_cong[simp]:
   968 assumes "|A| =o |B|"
   969 shows "|Fpow A| =o |Fpow B|"
   970 proof-
   971   obtain f where "bij_betw f A B"
   972   using assms card_of_ordIso[of A B] by auto
   973   hence "bij_betw (image f) (Fpow A) (Fpow B)"
   974   by (auto simp add: bij_betw_image_Fpow)
   975   thus ?thesis using card_of_ordIso[of "Fpow A"] by auto
   976 qed
   977 
   978 lemma ordIso_Fpow_cong:
   979 assumes "r =o r'"
   980 shows "|Fpow(Field r)| =o |Fpow(Field r')|"
   981 using assms card_of_cong card_of_Fpow_cong by blast
   982 
   983 lemma card_of_Fpow_lists: "|Fpow A| \<le>o |lists A|"
   984 proof-
   985   have "set ` (lists A) = Fpow A"
   986   unfolding lists_def2 Fpow_def using finite_list finite_set by blast
   987   thus ?thesis using card_of_ordLeq2[of "Fpow A"] Fpow_not_empty[of A] by blast
   988 qed
   989 
   990 lemma card_of_Fpow_infinite[simp]:
   991 assumes "\<not>finite A"
   992 shows "|Fpow A| =o |A|"
   993 using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
   994       ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
   995 
   996 corollary Fpow_infinite_bij_betw:
   997 assumes "\<not>finite A"
   998 shows "\<exists>f. bij_betw f (Fpow A) A"
   999 using assms card_of_Fpow_infinite card_of_ordIso by blast
  1000 
  1001 
  1002 subsection \<open>The cardinal $\omega$ and the finite cardinals\<close>
  1003 
  1004 subsubsection \<open>First as well-orders\<close>
  1005 
  1006 lemma Field_natLess: "Field natLess = (UNIV::nat set)"
  1007 by(unfold Field_def natLess_def, auto)
  1008 
  1009 lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
  1010 using natLeq_Well_order Field_natLeq by auto
  1011 
  1012 lemma natLeq_wo_rel: "wo_rel natLeq"
  1013 unfolding wo_rel_def using natLeq_Well_order .
  1014 
  1015 lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
  1016 by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
  1017    simp add: Field_natLeq, unfold under_def natLeq_def, auto)
  1018 
  1019 lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
  1020 by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
  1021    simp add: Field_natLeq, unfold under_def natLeq_def, auto)
  1022 
  1023 lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
  1024 using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
  1025 
  1026 lemma closed_nat_set_iff:
  1027 assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
  1028 shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
  1029 proof-
  1030   {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
  1031    moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
  1032    ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
  1033    using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
  1034    have "A = {0 ..< n}"
  1035    proof(auto simp add: 1)
  1036      fix m assume *: "m \<in> A"
  1037      {assume "n \<le> m" with assms * have "n \<in> A" by blast
  1038       hence False using 1 by auto
  1039      }
  1040      thus "m < n" by fastforce
  1041    qed
  1042    hence "\<exists>n. A = {0 ..< n}" by blast
  1043   }
  1044   thus ?thesis by blast
  1045 qed
  1046 
  1047 lemma natLeq_ofilter_iff:
  1048 "ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
  1049 proof(rule iffI)
  1050   assume "ofilter natLeq A"
  1051   hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" using natLeq_wo_rel
  1052   by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
  1053   thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
  1054 next
  1055   assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
  1056   thus "ofilter natLeq A"
  1057   by(auto simp add: natLeq_ofilter_less natLeq_UNIV_ofilter)
  1058 qed
  1059 
  1060 lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
  1061 unfolding under_def natLeq_def by auto
  1062 
  1063 lemma natLeq_on_ofilter_less_eq:
  1064 "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
  1065 apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
  1066 apply (simp add: Field_natLeq_on)
  1067 by (auto simp add: under_def)
  1068 
  1069 lemma natLeq_on_ofilter_iff:
  1070 "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
  1071 proof(rule iffI)
  1072   assume *: "wo_rel.ofilter (natLeq_on m) A"
  1073   hence 1: "A \<le> {0..<m}"
  1074   by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
  1075   hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
  1076   using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
  1077   hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
  1078   thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
  1079 next
  1080   assume "(\<exists>n\<le>m. A = {0 ..< n})"
  1081   thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
  1082 qed
  1083 
  1084 corollary natLeq_on_ofilter:
  1085 "ofilter(natLeq_on n) {0 ..< n}"
  1086 by (auto simp add: natLeq_on_ofilter_less_eq)
  1087 
  1088 lemma natLeq_on_ofilter_less:
  1089 "n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
  1090 by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
  1091    simp add: Field_natLeq_on, unfold under_def, auto)
  1092 
  1093 lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
  1094 using Field_natLeq Field_natLeq_on[of n]
  1095       finite_ordLess_infinite[of "natLeq_on n" natLeq]
  1096       natLeq_Well_order natLeq_on_Well_order[of n] by auto
  1097 
  1098 lemma natLeq_on_injective:
  1099 "natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
  1100 using Field_natLeq_on[of m] Field_natLeq_on[of n]
  1101       atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
  1102 
  1103 lemma natLeq_on_injective_ordIso:
  1104 "(natLeq_on m =o natLeq_on n) = (m = n)"
  1105 proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
  1106   assume "natLeq_on m =o natLeq_on n"
  1107   then obtain f where "bij_betw f {x. x<m} {x. x<n}"
  1108   using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
  1109   thus "m = n" using atLeastLessThan_injective2[of f m n]
  1110     unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
  1111 qed
  1112 
  1113 
  1114 subsubsection \<open>Then as cardinals\<close>
  1115 
  1116 lemma ordIso_natLeq_infinite1:
  1117 "|A| =o natLeq \<Longrightarrow> \<not>finite A"
  1118 using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
  1119 
  1120 lemma ordIso_natLeq_infinite2:
  1121 "natLeq =o |A| \<Longrightarrow> \<not>finite A"
  1122 using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
  1123 
  1124 lemma ordIso_natLeq_on_imp_finite:
  1125 "|A| =o natLeq_on n \<Longrightarrow> finite A"
  1126 unfolding ordIso_def iso_def[abs_def]
  1127 by (auto simp: Field_natLeq_on bij_betw_finite)
  1128 
  1129 lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
  1130 proof(unfold card_order_on_def,
  1131       auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
  1132   fix r assume "well_order_on {x. x < n} r"
  1133   thus "natLeq_on n \<le>o r"
  1134   using finite_atLeastLessThan natLeq_on_well_order_on
  1135         finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
  1136 qed
  1137 
  1138 corollary card_of_Field_natLeq_on:
  1139 "|Field (natLeq_on n)| =o natLeq_on n"
  1140 using Field_natLeq_on natLeq_on_Card_order
  1141       Card_order_iff_ordIso_card_of[of "natLeq_on n"]
  1142       ordIso_symmetric[of "natLeq_on n"] by blast
  1143 
  1144 corollary card_of_less:
  1145 "|{0 ..< n}| =o natLeq_on n"
  1146 using Field_natLeq_on card_of_Field_natLeq_on
  1147 unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
  1148 
  1149 lemma natLeq_on_ordLeq_less_eq:
  1150 "((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
  1151 proof
  1152   assume "natLeq_on m \<le>o natLeq_on n"
  1153   then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
  1154   unfolding ordLeq_def using
  1155     embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
  1156      embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
  1157   thus "m \<le> n" using atLeastLessThan_less_eq2
  1158     unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
  1159 next
  1160   assume "m \<le> n"
  1161   hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
  1162   hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
  1163   thus "natLeq_on m \<le>o natLeq_on n"
  1164   using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
  1165 qed
  1166 
  1167 lemma natLeq_on_ordLeq_less:
  1168 "((natLeq_on m) <o (natLeq_on n)) = (m < n)"
  1169 using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
  1170    natLeq_on_ordLeq_less_eq[of n m] by linarith
  1171 
  1172 lemma ordLeq_natLeq_on_imp_finite:
  1173 assumes "|A| \<le>o natLeq_on n"
  1174 shows "finite A"
  1175 proof-
  1176   have "|A| \<le>o |{0 ..< n}|"
  1177   using assms card_of_less ordIso_symmetric ordLeq_ordIso_trans by blast
  1178   thus ?thesis by (auto simp add: card_of_ordLeq_finite)
  1179 qed
  1180 
  1181 
  1182 subsubsection \<open>"Backward compatibility" with the numeric cardinal operator for finite sets\<close>
  1183 
  1184 lemma finite_card_of_iff_card2:
  1185 assumes FIN: "finite A" and FIN': "finite B"
  1186 shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
  1187 using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
  1188 
  1189 lemma finite_imp_card_of_natLeq_on:
  1190 assumes "finite A"
  1191 shows "|A| =o natLeq_on (card A)"
  1192 proof-
  1193   obtain h where "bij_betw h A {0 ..< card A}"
  1194   using assms ex_bij_betw_finite_nat by blast
  1195   thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
  1196 qed
  1197 
  1198 lemma finite_iff_card_of_natLeq_on:
  1199 "finite A = (\<exists>n. |A| =o natLeq_on n)"
  1200 using finite_imp_card_of_natLeq_on[of A]
  1201 by(auto simp add: ordIso_natLeq_on_imp_finite)
  1202 
  1203 lemma finite_card_of_iff_card:
  1204 assumes FIN: "finite A" and FIN': "finite B"
  1205 shows "( |A| =o |B| ) = (card A = card B)"
  1206 using assms card_of_ordIso[of A B] bij_betw_iff_card[of A B] by blast
  1207 
  1208 lemma finite_card_of_iff_card3:
  1209 assumes FIN: "finite A" and FIN': "finite B"
  1210 shows "( |A| <o |B| ) = (card A < card B)"
  1211 proof-
  1212   have "( |A| <o |B| ) = (~ ( |B| \<le>o |A| ))" by simp
  1213   also have "... = (~ (card B \<le> card A))"
  1214   using assms by(simp add: finite_card_of_iff_card2)
  1215   also have "... = (card A < card B)" by auto
  1216   finally show ?thesis .
  1217 qed
  1218 
  1219 lemma card_Field_natLeq_on:
  1220 "card(Field(natLeq_on n)) = n"
  1221 using Field_natLeq_on card_atLeastLessThan by auto
  1222 
  1223 
  1224 subsection \<open>The successor of a cardinal\<close>
  1225 
  1226 lemma embed_implies_ordIso_Restr:
  1227 assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r' r f"
  1228 shows "r' =o Restr r (f ` (Field r'))"
  1229 using assms embed_implies_iso_Restr Well_order_Restr unfolding ordIso_def by blast
  1230 
  1231 lemma cardSuc_Well_order[simp]:
  1232 "Card_order r \<Longrightarrow> Well_order(cardSuc r)"
  1233 using cardSuc_Card_order unfolding card_order_on_def by blast
  1234 
  1235 lemma Field_cardSuc_not_empty:
  1236 assumes "Card_order r"
  1237 shows "Field (cardSuc r) \<noteq> {}"
  1238 proof
  1239   assume "Field(cardSuc r) = {}"
  1240   hence "|Field(cardSuc r)| \<le>o r" using assms Card_order_empty[of r] by auto
  1241   hence "cardSuc r \<le>o r" using assms card_of_Field_ordIso
  1242   cardSuc_Card_order ordIso_symmetric ordIso_ordLeq_trans by blast
  1243   thus False using cardSuc_greater not_ordLess_ordLeq assms by blast
  1244 qed
  1245 
  1246 lemma cardSuc_mono_ordLess[simp]:
  1247 assumes CARD: "Card_order r" and CARD': "Card_order r'"
  1248 shows "(cardSuc r <o cardSuc r') = (r <o r')"
  1249 proof-
  1250   have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
  1251   using assms by auto
  1252   thus ?thesis
  1253   using not_ordLeq_iff_ordLess not_ordLeq_iff_ordLess[of r r']
  1254   using cardSuc_mono_ordLeq[of r' r] assms by blast
  1255 qed
  1256 
  1257 lemma cardSuc_natLeq_on_Suc:
  1258 "cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
  1259 proof-
  1260   obtain r r' p where r_def: "r = natLeq_on n" and
  1261                       r'_def: "r' = cardSuc(natLeq_on n)"  and
  1262                       p_def: "p = natLeq_on(Suc n)" by blast
  1263   (* Preliminary facts:  *)
  1264   have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
  1265   using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
  1266   hence WELL: "Well_order r \<and> Well_order r' \<and>  Well_order p"
  1267   unfolding card_order_on_def by force
  1268   have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
  1269   unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
  1270   hence FIN: "finite (Field r)" by force
  1271   have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
  1272   hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
  1273   hence LESS: "|Field r| <o |Field r'|"
  1274   using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
  1275   (* Main proof: *)
  1276   have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
  1277   using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
  1278   moreover have "p \<le>o r'"
  1279   proof-
  1280     {assume "r' <o p"
  1281      then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
  1282      let ?q = "Restr p (f ` Field r')"
  1283      have 1: "embed r' p f" using 0 unfolding embedS_def by force
  1284      hence 2: "f ` Field r' < {0..<(Suc n)}"
  1285      using WELL FIELD 0 by (auto simp add: embedS_iff)
  1286      have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
  1287      then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
  1288      unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
  1289      hence 4: "m \<le> n" using 2 by force
  1290      (*  *)
  1291      have "bij_betw f (Field r') (f ` (Field r'))"
  1292      using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
  1293      moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
  1294      ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
  1295      using bij_betw_same_card bij_betw_finite by metis
  1296      hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
  1297      hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
  1298      hence False using LESS not_ordLess_ordLeq by auto
  1299     }
  1300     thus ?thesis using WELL CARD by fastforce
  1301   qed
  1302   ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
  1303 qed
  1304 
  1305 lemma card_of_Plus_ordLeq_infinite[simp]:
  1306 assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
  1307 shows "|A <+> B| \<le>o |C|"
  1308 proof-
  1309   let ?r = "cardSuc |C|"
  1310   have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
  1311   moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
  1312   ultimately have "|A <+> B| <o ?r"
  1313   using card_of_Plus_ordLess_infinite_Field by blast
  1314   thus ?thesis using C by simp
  1315 qed
  1316 
  1317 lemma card_of_Un_ordLeq_infinite[simp]:
  1318 assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
  1319 shows "|A Un B| \<le>o |C|"
  1320 using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
  1321 ordLeq_transitive by metis
  1322 
  1323 
  1324 subsection \<open>Others\<close>
  1325 
  1326 lemma under_mono[simp]:
  1327 assumes "Well_order r" and "(i,j) \<in> r"
  1328 shows "under r i \<subseteq> under r j"
  1329 using assms unfolding under_def order_on_defs
  1330 trans_def by blast
  1331 
  1332 lemma underS_under:
  1333 assumes "i \<in> Field r"
  1334 shows "underS r i = under r i - {i}"
  1335 using assms unfolding underS_def under_def by auto
  1336 
  1337 lemma relChain_under:
  1338 assumes "Well_order r"
  1339 shows "relChain r (\<lambda> i. under r i)"
  1340 using assms unfolding relChain_def by auto
  1341 
  1342 lemma card_of_infinite_diff_finite:
  1343 assumes "\<not>finite A" and "finite B"
  1344 shows "|A - B| =o |A|"
  1345 by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
  1346 
  1347 lemma infinite_card_of_diff_singl:
  1348 assumes "\<not>finite A"
  1349 shows "|A - {a}| =o |A|"
  1350 by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
  1351 
  1352 lemma card_of_vimage:
  1353 assumes "B \<subseteq> range f"
  1354 shows "|B| \<le>o |f -` B|"
  1355 apply(rule surj_imp_ordLeq[of _ f])
  1356 using assms by (metis Int_absorb2 image_vimage_eq order_refl)
  1357 
  1358 lemma surj_card_of_vimage:
  1359 assumes "surj f"
  1360 shows "|B| \<le>o |f -` B|"
  1361 by (metis assms card_of_vimage subset_UNIV)
  1362 
  1363 lemma infinite_Pow:
  1364 assumes "\<not> finite A"
  1365 shows "\<not> finite (Pow A)"
  1366 proof-
  1367   have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
  1368   thus ?thesis by (metis assms finite_Pow_iff)
  1369 qed
  1370 
  1371 (* bounded powerset *)
  1372 definition Bpow where
  1373 "Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
  1374 
  1375 lemma Bpow_empty[simp]:
  1376 assumes "Card_order r"
  1377 shows "Bpow r {} = {{}}"
  1378 using assms unfolding Bpow_def by auto
  1379 
  1380 lemma singl_in_Bpow:
  1381 assumes rc: "Card_order r"
  1382 and r: "Field r \<noteq> {}" and a: "a \<in> A"
  1383 shows "{a} \<in> Bpow r A"
  1384 proof-
  1385   have "|{a}| \<le>o r" using r rc by auto
  1386   thus ?thesis unfolding Bpow_def using a by auto
  1387 qed
  1388 
  1389 lemma ordLeq_card_Bpow:
  1390 assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
  1391 shows "|A| \<le>o |Bpow r A|"
  1392 proof-
  1393   have "inj_on (\<lambda> a. {a}) A" unfolding inj_on_def by auto
  1394   moreover have "(\<lambda> a. {a}) ` A \<subseteq> Bpow r A"
  1395   using singl_in_Bpow[OF assms] by auto
  1396   ultimately show ?thesis unfolding card_of_ordLeq[symmetric] by blast
  1397 qed
  1398 
  1399 lemma infinite_Bpow:
  1400 assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
  1401 and A: "\<not>finite A"
  1402 shows "\<not>finite (Bpow r A)"
  1403 using ordLeq_card_Bpow[OF rc r]
  1404 by (metis A card_of_ordLeq_infinite)
  1405 
  1406 definition Func_option where
  1407  "Func_option A B \<equiv>
  1408   {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)}"
  1409 
  1410 lemma card_of_Func_option_Func:
  1411 "|Func_option A B| =o |Func A B|"
  1412 proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI)
  1413   let ?F = "\<lambda> f a. if a \<in> A then Some (f a) else None"
  1414   show "bij_betw ?F (Func A B) (Func_option A B)"
  1415   unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI)
  1416     fix f g assume f: "f \<in> Func A B" and g: "g \<in> Func A B" and eq: "?F f = ?F g"
  1417     show "f = g"
  1418     proof(rule ext)
  1419       fix a
  1420       show "f a = g a"
  1421       proof(cases "a \<in> A")
  1422         case True
  1423         have "Some (f a) = ?F f a" using True by auto
  1424         also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE)
  1425         also have "... = Some (g a)" using True by auto
  1426         finally have "Some (f a) = Some (g a)" .
  1427         thus ?thesis by simp
  1428       qed(insert f g, unfold Func_def, auto)
  1429     qed
  1430   next
  1431     show "?F ` Func A B = Func_option A B"
  1432     proof safe
  1433       fix f assume f: "f \<in> Func_option A B"
  1434       define g where [abs_def]: "g a = (case f a of Some b \<Rightarrow> b | None \<Rightarrow> undefined)" for a
  1435       have "g \<in> Func A B"
  1436       using f unfolding g_def Func_def Func_option_def by force+
  1437       moreover have "f = ?F g"
  1438       proof(rule ext)
  1439         fix a show "f a = ?F g a"
  1440         using f unfolding Func_option_def g_def by (cases "a \<in> A") force+
  1441       qed
  1442       ultimately show "f \<in> ?F ` (Func A B)" by blast
  1443     qed(unfold Func_def Func_option_def, auto)
  1444   qed
  1445 qed
  1446 
  1447 (* partial-function space: *)
  1448 definition Pfunc where
  1449 "Pfunc A B \<equiv>
  1450  {f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
  1451      (\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
  1452 
  1453 lemma Func_Pfunc:
  1454 "Func_option A B \<subseteq> Pfunc A B"
  1455 unfolding Func_option_def Pfunc_def by auto
  1456 
  1457 lemma Pfunc_Func_option:
  1458 "Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
  1459 proof safe
  1460   fix f assume f: "f \<in> Pfunc A B"
  1461   show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
  1462   proof (intro UN_I)
  1463     let ?A' = "{a. f a \<noteq> None}"
  1464     show "?A' \<in> Pow A" using f unfolding Pow_def Pfunc_def by auto
  1465     show "f \<in> Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto
  1466   qed
  1467 next
  1468   fix f A' assume "f \<in> Func_option A' B" and "A' \<subseteq> A"
  1469   thus "f \<in> Pfunc A B" unfolding Func_option_def Pfunc_def by auto
  1470 qed
  1471 
  1472 lemma card_of_Func_mono:
  1473 fixes A1 A2 :: "'a set" and B :: "'b set"
  1474 assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
  1475 shows "|Func A1 B| \<le>o |Func A2 B|"
  1476 proof-
  1477   obtain bb where bb: "bb \<in> B" using B by auto
  1478   define F where [abs_def]: "F f1 a =
  1479     (if a \<in> A2 then (if a \<in> A1 then f1 a else bb) else undefined)" for f1 :: "'a \<Rightarrow> 'b" and a
  1480   show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI)
  1481     show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe
  1482       fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g"
  1483       show "f = g"
  1484       proof(rule ext)
  1485         fix a show "f a = g a"
  1486         proof(cases "a \<in> A1")
  1487           case True
  1488           thus ?thesis using eq A12 unfolding F_def fun_eq_iff
  1489           by (elim allE[of _ a]) auto
  1490         qed(insert f g, unfold Func_def, fastforce)
  1491       qed
  1492     qed
  1493   qed(insert bb, unfold Func_def F_def, force)
  1494 qed
  1495 
  1496 lemma card_of_Func_option_mono:
  1497 fixes A1 A2 :: "'a set" and B :: "'b set"
  1498 assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
  1499 shows "|Func_option A1 B| \<le>o |Func_option A2 B|"
  1500 by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func
  1501   ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric)
  1502 
  1503 lemma card_of_Pfunc_Pow_Func_option:
  1504 assumes "B \<noteq> {}"
  1505 shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
  1506 proof-
  1507   have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
  1508     unfolding Pfunc_Func_option by(rule card_of_refl)
  1509   also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
  1510   also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
  1511     apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
  1512   finally show ?thesis .
  1513 qed
  1514 
  1515 lemma Bpow_ordLeq_Func_Field:
  1516 assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
  1517 shows "|Bpow r A| \<le>o |Func (Field r) A|"
  1518 proof-
  1519   let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
  1520   {fix X assume "X \<in> Bpow r A - {{}}"
  1521    hence XA: "X \<subseteq> A" and "|X| \<le>o r"
  1522    and X: "X \<noteq> {}" unfolding Bpow_def by auto
  1523    hence "|X| \<le>o |Field r|" by (metis Field_card_of card_of_mono2)
  1524    then obtain F where 1: "X = F ` (Field r)"
  1525    using card_of_ordLeq2[OF X] by metis
  1526    define f where [abs_def]: "f i = (if i \<in> Field r then F i else undefined)" for i
  1527    have "\<exists> f \<in> Func (Field r) A. X = ?F f"
  1528    apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto
  1529   }
  1530   hence "Bpow r A - {{}} \<subseteq> ?F ` (Func (Field r) A)" by auto
  1531   hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
  1532   by (rule surj_imp_ordLeq)
  1533   moreover
  1534   {have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
  1535    have "|Bpow r A| =o |Bpow r A - {{}}|"
  1536      by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
  1537   }
  1538   ultimately show ?thesis by (metis ordIso_ordLeq_trans)
  1539 qed
  1540 
  1541 lemma empty_in_Func[simp]:
  1542 "B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
  1543 unfolding Func_def by auto
  1544 
  1545 lemma Func_mono[simp]:
  1546 assumes "B1 \<subseteq> B2"
  1547 shows "Func A B1 \<subseteq> Func A B2"
  1548 using assms unfolding Func_def by force
  1549 
  1550 lemma Pfunc_mono[simp]:
  1551 assumes "A1 \<subseteq> A2" and "B1 \<subseteq> B2"
  1552 shows "Pfunc A B1 \<subseteq> Pfunc A B2"
  1553 using assms unfolding Pfunc_def
  1554 apply safe
  1555 apply (case_tac "x a", auto)
  1556 apply (metis in_mono option.simps(5))
  1557 done
  1558 
  1559 lemma card_of_Func_UNIV_UNIV:
  1560 "|Func (UNIV::'a set) (UNIV::'b set)| =o |UNIV::('a \<Rightarrow> 'b) set|"
  1561 using card_of_Func_UNIV[of "UNIV::'b set"] by auto
  1562 
  1563 lemma ordLeq_Func:
  1564 assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
  1565 shows "|A| \<le>o |Func A B|"
  1566 unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
  1567   let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined"
  1568   show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto
  1569   show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto
  1570 qed
  1571 
  1572 lemma infinite_Func:
  1573 assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
  1574 shows "\<not>finite (Func A B)"
  1575 using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
  1576 
  1577 
  1578 subsection \<open>Infinite cardinals are limit ordinals\<close>
  1579 
  1580 lemma card_order_infinite_isLimOrd:
  1581 assumes c: "Card_order r" and i: "\<not>finite (Field r)"
  1582 shows "isLimOrd r"
  1583 proof-
  1584   have 0: "wo_rel r" and 00: "Well_order r"
  1585   using c unfolding card_order_on_def wo_rel_def by auto
  1586   hence rr: "Refl r" by (metis wo_rel.REFL)
  1587   show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] proof safe
  1588     fix j assume j: "j \<in> Field r" and jm: "\<forall>i\<in>Field r. (i, j) \<in> r"
  1589     define p where "p = Restr r (Field r - {j})"
  1590     have fp: "Field p = Field r - {j}"
  1591     unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
  1592     have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
  1593       fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
  1594       hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding under_def Field_def by auto
  1595       moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm  unfolding fp by auto
  1596       ultimately have "x \<noteq> j" using j jm  by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
  1597       thus "x \<in> Field p" using x unfolding fp by auto
  1598     qed(unfold p_def Field_def, auto)
  1599     have "p <o r" using j ofilter_ordLess[OF 00 of] unfolding fp p_def[symmetric] by auto
  1600     hence 2: "|Field p| <o r" using c by (metis BNF_Cardinal_Order_Relation.ordLess_Field)
  1601     have "|Field p| =o |Field r|" unfolding fp using i by (metis infinite_card_of_diff_singl)
  1602     also have "|Field r| =o r"
  1603     using c by (metis card_of_unique ordIso_symmetric)
  1604     finally have "|Field p| =o r" .
  1605     with 2 show False by (metis not_ordLess_ordIso)
  1606   qed
  1607 qed
  1608 
  1609 lemma insert_Chain:
  1610 assumes "Refl r" "C \<in> Chains r" and "i \<in> Field r" and "\<And>j. j \<in> C \<Longrightarrow> (j,i) \<in> r \<or> (i,j) \<in> r"
  1611 shows "insert i C \<in> Chains r"
  1612 using assms unfolding Chains_def by (auto dest: refl_onD)
  1613 
  1614 lemma Collect_insert: "{R j |j. j \<in> insert j1 J} = insert (R j1) {R j |j. j \<in> J}"
  1615 by auto
  1616 
  1617 lemma Field_init_seg_of[simp]:
  1618 "Field init_seg_of = UNIV"
  1619 unfolding Field_def init_seg_of_def by auto
  1620 
  1621 lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
  1622 unfolding refl_on_def Field_def by auto
  1623 
  1624 lemma regularCard_all_ex:
  1625 assumes r: "Card_order r"   "regularCard r"
  1626 and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
  1627 and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
  1628 and cardB: "|B| <o r"
  1629 shows "\<exists> i \<in> Field r. \<forall> b \<in> B. P i b"
  1630 proof-
  1631   let ?As = "\<lambda>i. {b \<in> B. P i b}"
  1632   have "EX i : Field r. B \<le> ?As i"
  1633   apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
  1634   thus ?thesis by auto
  1635 qed
  1636 
  1637 lemma relChain_stabilize:
  1638 assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
  1639 and ir: "\<not>finite (Field r)" and cr: "Card_order r"
  1640 shows "\<exists> i \<in> Field r. As (succ r i) = As i"
  1641 proof(rule ccontr, auto)
  1642   have 0: "wo_rel r" and 00: "Well_order r"
  1643   unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
  1644   have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
  1645   have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
  1646   using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
  1647   assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
  1648   have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
  1649   proof safe
  1650     fix i j assume 1: "(i, j) \<in> r" "i \<noteq> j" and Asij: "As i = As j"
  1651     hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
  1652     hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
  1653     moreover
  1654     {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
  1655      using 1 unfolding aboveS_def by auto
  1656      hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
  1657     }
  1658     ultimately show False unfolding Asij by auto
  1659   qed (insert rc, unfold relChain_def, auto)
  1660   hence "\<forall> i \<in> Field r. \<exists> a. a \<in> As (succ r i) - As i"
  1661   using wo_rel.succ_in[OF 0] AsB
  1662   by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
  1663             wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
  1664   then obtain f where f: "\<forall> i \<in> Field r. f i \<in> As (succ r i) - As i" by metis
  1665   have "inj_on f (Field r)" unfolding inj_on_def proof safe
  1666     fix i j assume ij: "i \<in> Field r" "j \<in> Field r" and fij: "f i = f j"
  1667     show "i = j"
  1668     proof(cases rule: wo_rel.cases_Total3[OF 0], safe)
  1669       assume "(i, j) \<in> r" and ijd: "i \<noteq> j"
  1670       hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
  1671       hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
  1672       thus "i = j" using ij ijd fij f by auto
  1673     next
  1674       assume "(j, i) \<in> r" and ijd: "i \<noteq> j"
  1675       hence rij: "(succ r j, i) \<in> r" by (metis "0" wo_rel.succ_smallest)
  1676       hence "As (succ r j) \<subseteq> As i" using rc unfolding relChain_def by auto
  1677       thus "j = i" using ij ijd fij f by fastforce
  1678     qed(insert ij, auto)
  1679   qed
  1680   moreover have "f ` (Field r) \<subseteq> B" using f AsBs by auto
  1681   moreover have "|B| <o |Field r|" using Br cr by (metis card_of_unique ordLess_ordIso_trans)
  1682   ultimately show False unfolding card_of_ordLess[symmetric] by auto
  1683 qed
  1684 
  1685 
  1686 subsection \<open>Regular vs. stable cardinals\<close>
  1687 
  1688 definition stable :: "'a rel \<Rightarrow> bool"
  1689 where
  1690 "stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
  1691                |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
  1692                \<longrightarrow> |SIGMA a : A. F a| <o r"
  1693 
  1694 lemma regularCard_stable:
  1695 assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
  1696 shows "stable r"
  1697 unfolding stable_def proof safe
  1698   fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
  1699   {assume "r \<le>o |Sigma A F|"
  1700    hence "|Field r| \<le>o |Sigma A F|" using card_of_Field_ordIso[OF cr]
  1701    by (metis Field_card_of card_of_cong ordLeq_iff_ordLess_or_ordIso ordLeq_ordLess_trans)
  1702    moreover have Fi: "Field r \<noteq> {}" using ir by auto
  1703    ultimately obtain f where f: "f ` Sigma A F = Field r" using card_of_ordLeq2 by metis
  1704    have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto
  1705    {fix a assume a: "a \<in> A"
  1706     define L where "L = {(a,u) | u. u \<in> F a}"
  1707     have fL: "f ` L \<subseteq> Field r" using f a unfolding L_def by auto
  1708     have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric]
  1709     apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
  1710     hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
  1711     hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
  1712     hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso)
  1713     then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
  1714     unfolding cofinal_def image_def by auto
  1715     hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r" using r by (metis fL image_subset_iff wo_rel.in_notinI)
  1716     hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
  1717    }
  1718    then obtain gg where gg: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u), gg a) \<in> r" by metis
  1719    obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
  1720    define g where [abs_def]: "g a = (if F a \<noteq> {} then gg a else j0)" for a
  1721    have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
  1722    hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
  1723    using f[symmetric] unfolding under_def image_def by auto
  1724    have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
  1725    moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
  1726      fix i assume "i \<in> Field r"
  1727      then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
  1728      hence "j \<in> Field r" by (metis card_order_on_def cr well_order_on_domain)
  1729      then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
  1730      hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
  1731      moreover have "i \<noteq> g a"
  1732      using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
  1733      partial_order_on_def antisym_def by auto
  1734      ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
  1735    qed
  1736    ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
  1737    moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
  1738    ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
  1739   }
  1740   thus "|Sigma A F| <o r"
  1741   using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
  1742 qed
  1743 
  1744 lemma stable_regularCard:
  1745 assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
  1746 shows "regularCard r"
  1747 unfolding regularCard_def proof safe
  1748   fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
  1749   have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
  1750   moreover
  1751   {assume Kr: "|K| <o r"
  1752    then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
  1753    using cof unfolding cofinal_def by metis
  1754    hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
  1755    hence "r \<le>o |\<Union>a \<in> K. underS r a|" using cr
  1756    by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
  1757    also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
  1758    also
  1759    {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
  1760     hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
  1761    }
  1762    finally have "r <o r" .
  1763    hence False by (metis ordLess_irreflexive)
  1764   }
  1765   ultimately show "|K| =o r" by (metis ordLeq_iff_ordLess_or_ordIso)
  1766 qed
  1767 
  1768 (* Note that below the types of A and F are now unconstrained: *)
  1769 lemma stable_elim:
  1770 assumes ST: "stable r" and A_LESS: "|A| <o r" and
  1771         F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
  1772 shows "|SIGMA a : A. F a| <o r"
  1773 proof-
  1774   obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
  1775   using internalize_card_of_ordLess[of A r] A_LESS by blast
  1776   then obtain G where 3: "bij_betw G A' A"
  1777   using card_of_ordIso  ordIso_symmetric by blast
  1778   (*  *)
  1779   {fix a assume "a \<in> A"
  1780    hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
  1781    using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
  1782   }
  1783   then obtain F' where
  1784   temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
  1785   using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
  1786   hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
  1787   have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
  1788   (*  *)
  1789   have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
  1790   using 3 4 bij_betw_ball[of G A' A] by auto
  1791   hence "|SIGMA a' : A'. F'(G a')| <o r"
  1792   using ST 1 unfolding stable_def by auto
  1793   moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
  1794   using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
  1795   ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
  1796 qed
  1797 
  1798 lemma stable_natLeq: "stable natLeq"
  1799 proof(unfold stable_def, safe)
  1800   fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
  1801   assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
  1802   hence "finite A \<and> (\<forall>a \<in> A. finite(F a))"
  1803   by (auto simp add: finite_iff_ordLess_natLeq)
  1804   hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F])
  1805   thus "|Sigma A F | <o natLeq"
  1806   by (auto simp add: finite_iff_ordLess_natLeq)
  1807 qed
  1808 
  1809 corollary regularCard_natLeq: "regularCard natLeq"
  1810 using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
  1811 
  1812 lemma stable_cardSuc:
  1813 assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
  1814 shows "stable(cardSuc r)"
  1815 using infinite_cardSuc_regularCard regularCard_stable
  1816 by (metis CARD INF cardSuc_Card_order cardSuc_finite)
  1817 
  1818 lemma stable_UNION:
  1819 assumes ST: "stable r" and A_LESS: "|A| <o r" and
  1820         F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
  1821 shows "|\<Union>a \<in> A. F a| <o r"
  1822 proof-
  1823   have "|\<Union>a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
  1824   using card_of_UNION_Sigma by blast
  1825   thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
  1826 qed
  1827 
  1828 lemma stable_ordIso1:
  1829 assumes ST: "stable r" and ISO: "r' =o r"
  1830 shows "stable r'"
  1831 proof(unfold stable_def, auto)
  1832   fix A::"'b set" and F::"'b \<Rightarrow> 'b set"
  1833   assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
  1834   hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
  1835   using ISO ordLess_ordIso_trans by blast
  1836   hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
  1837   thus "|SIGMA a : A. F a| <o r'"
  1838   using ISO ordIso_symmetric ordLess_ordIso_trans by blast
  1839 qed
  1840 
  1841 lemma stable_ordIso2:
  1842 assumes ST: "stable r" and ISO: "r =o r'"
  1843 shows "stable r'"
  1844 using assms stable_ordIso1 ordIso_symmetric by blast
  1845 
  1846 lemma stable_ordIso:
  1847 assumes "r =o r'"
  1848 shows "stable r = stable r'"
  1849 using assms stable_ordIso1 stable_ordIso2 by blast
  1850 
  1851 lemma stable_nat: "stable |UNIV::nat set|"
  1852 using stable_natLeq card_of_nat stable_ordIso by auto
  1853 
  1854 text\<open>Below, the type of "A" is not important -- we just had to choose an appropriate
  1855    type to make "A" possible. What is important is that arbitrarily large
  1856    infinite sets of stable cardinality exist.\<close>
  1857 
  1858 lemma infinite_stable_exists:
  1859 assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
  1860 shows "\<exists>(A :: (nat + 'a set)set).
  1861           \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
  1862 proof-
  1863   have "\<exists>(A :: (nat + 'a set)set).
  1864           \<not>finite A \<and> stable |A| \<and> |UNIV::'a set| <o |A|"
  1865   proof(cases "finite (UNIV::'a set)")
  1866     assume Case1: "finite (UNIV::'a set)"
  1867     let ?B = "UNIV::nat set"
  1868     have "\<not>finite(?B <+> {})" using finite_Plus_iff by blast
  1869     moreover
  1870     have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast
  1871     hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast
  1872     moreover
  1873     have "\<not>finite(Field |?B| ) \<and> finite(Field |UNIV::'a set| )" using Case1 by simp
  1874     hence "|UNIV::'a set| <o |?B|" by (simp add: finite_ordLess_infinite)
  1875     hence "|UNIV::'a set| <o |?B <+> {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast
  1876     ultimately show ?thesis by blast
  1877   next
  1878     assume Case1: "\<not>finite (UNIV::'a set)"
  1879     hence *: "\<not>finite(Field |UNIV::'a set| )" by simp
  1880     let ?B = "Field(cardSuc |UNIV::'a set| )"
  1881     have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast
  1882     have 1: "\<not>finite ?B" using Case1 card_of_cardSuc_finite by blast
  1883     hence 2: "\<not>finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast
  1884     have "|?B| =o cardSuc |UNIV::'a set|"
  1885     using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
  1886     moreover have "stable(cardSuc |UNIV::'a set| )"
  1887     using stable_cardSuc * card_of_Card_order by blast
  1888     ultimately have "stable |?B|" using stable_ordIso by blast
  1889     hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast
  1890     have "|UNIV::'a set| <o cardSuc |UNIV::'a set|"
  1891     using card_of_Card_order cardSuc_greater by blast
  1892     moreover have "|?B| =o  cardSuc |UNIV::'a set|"
  1893     using card_of_Card_order cardSuc_Card_order  card_of_Field_ordIso by blast
  1894     ultimately have "|UNIV::'a set| <o |?B|"
  1895     using ordIso_symmetric ordLess_ordIso_trans by blast
  1896     hence "|UNIV::'a set| <o |{} <+> ?B|" using 0 ordLess_ordIso_trans by blast
  1897     thus ?thesis using 2 3 by blast
  1898   qed
  1899   thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
  1900 qed
  1901 
  1902 corollary infinite_regularCard_exists:
  1903 assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
  1904 shows "\<exists>(A :: (nat + 'a set)set).
  1905           \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
  1906 using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
  1907 
  1908 end