src/HOL/BNF_Cardinal_Order_Relation.thy
author traytel
Fri Mar 07 23:10:27 2014 +0100 (2014-03-07)
changeset 56011 39d5043ce8a3
parent 55936 f6591f8c629d
child 56075 c6d4425f1fdc
permissions -rw-r--r--
made natLe{q,ss} constants (yields smaller terms in composition)
     1 (*  Title:      HOL/BNF_Cardinal_Order_Relation.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 Cardinal-order relations as needed by bounded natural functors.
     6 *)
     7 
     8 header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
     9 
    10 theory BNF_Cardinal_Order_Relation
    11 imports Zorn BNF_Constructions_on_Wellorders
    12 begin
    13 
    14 text{* In this section, we define cardinal-order relations to be minim well-orders
    15 on their field.  Then we define the cardinal of a set to be {\em some} cardinal-order
    16 relation on that set, which will be unique up to order isomorphism.  Then we study
    17 the connection between cardinals and:
    18 \begin{itemize}
    19 \item standard set-theoretic constructions: products,
    20 sums, unions, lists, powersets, set-of finite sets operator;
    21 \item finiteness and infiniteness (in particular, with the numeric cardinal operator
    22 for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
    23 \end{itemize}
    24 %
    25 On the way, we define the canonical $\omega$ cardinal and finite cardinals.  We also
    26 define (again, up to order isomorphism) the successor of a cardinal, and show that
    27 any cardinal admits a successor.
    28 
    29 Main results of this section are the existence of cardinal relations and the
    30 facts that, in the presence of infiniteness,
    31 most of the standard set-theoretic constructions (except for the powerset)
    32 {\em do not increase cardinality}.  In particular, e.g., the set of words/lists over
    33 any infinite set has the same cardinality (hence, is in bijection) with that set.
    34 *}
    35 
    36 
    37 subsection {* Cardinal orders *}
    38 
    39 text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
    40 order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
    41 strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
    42 
    43 definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
    44 where
    45 "card_order_on A r \<equiv> well_order_on A r \<and> (\<forall>r'. well_order_on A r' \<longrightarrow> r \<le>o r')"
    46 
    47 abbreviation "Card_order r \<equiv> card_order_on (Field r) r"
    48 abbreviation "card_order r \<equiv> card_order_on UNIV r"
    49 
    50 lemma card_order_on_well_order_on:
    51 assumes "card_order_on A r"
    52 shows "well_order_on A r"
    53 using assms unfolding card_order_on_def by simp
    54 
    55 lemma card_order_on_Card_order:
    56 "card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
    57 unfolding card_order_on_def using well_order_on_Field by blast
    58 
    59 text{* The existence of a cardinal relation on any given set (which will mean
    60 that any set has a cardinal) follows from two facts:
    61 \begin{itemize}
    62 \item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
    63 which states that on any given set there exists a well-order;
    64 \item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
    65 such well-order, i.e., a cardinal order.
    66 \end{itemize}
    67 *}
    68 
    69 theorem card_order_on: "\<exists>r. card_order_on A r"
    70 proof-
    71   obtain R where R_def: "R = {r. well_order_on A r}" by blast
    72   have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
    73   using well_order_on[of A] R_def well_order_on_Well_order by blast
    74   hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
    75   using  exists_minim_Well_order[of R] by auto
    76   thus ?thesis using R_def unfolding card_order_on_def by auto
    77 qed
    78 
    79 lemma card_order_on_ordIso:
    80 assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
    81 shows "r =o r'"
    82 using assms unfolding card_order_on_def
    83 using ordIso_iff_ordLeq by blast
    84 
    85 lemma Card_order_ordIso:
    86 assumes CO: "Card_order r" and ISO: "r' =o r"
    87 shows "Card_order r'"
    88 using ISO unfolding ordIso_def
    89 proof(unfold card_order_on_def, auto)
    90   fix p' assume "well_order_on (Field r') p'"
    91   hence 0: "Well_order p' \<and> Field p' = Field r'"
    92   using well_order_on_Well_order by blast
    93   obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
    94   using ISO unfolding ordIso_def by auto
    95   hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
    96   by (auto simp add: iso_iff embed_inj_on)
    97   let ?p = "dir_image p' f"
    98   have 4: "p' =o ?p \<and> Well_order ?p"
    99   using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
   100   moreover have "Field ?p =  Field r"
   101   using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
   102   ultimately have "well_order_on (Field r) ?p" by auto
   103   hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
   104   thus "r' \<le>o p'"
   105   using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
   106 qed
   107 
   108 lemma Card_order_ordIso2:
   109 assumes CO: "Card_order r" and ISO: "r =o r'"
   110 shows "Card_order r'"
   111 using assms Card_order_ordIso ordIso_symmetric by blast
   112 
   113 
   114 subsection {* Cardinal of a set *}
   115 
   116 text{* We define the cardinal of set to be {\em some} cardinal order on that set.
   117 We shall prove that this notion is unique up to order isomorphism, meaning
   118 that order isomorphism shall be the true identity of cardinals. *}
   119 
   120 definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
   121 where "card_of A = (SOME r. card_order_on A r)"
   122 
   123 lemma card_of_card_order_on: "card_order_on A |A|"
   124 unfolding card_of_def by (auto simp add: card_order_on someI_ex)
   125 
   126 lemma card_of_well_order_on: "well_order_on A |A|"
   127 using card_of_card_order_on card_order_on_def by blast
   128 
   129 lemma Field_card_of: "Field |A| = A"
   130 using card_of_card_order_on[of A] unfolding card_order_on_def
   131 using well_order_on_Field by blast
   132 
   133 lemma card_of_Card_order: "Card_order |A|"
   134 by (simp only: card_of_card_order_on Field_card_of)
   135 
   136 corollary ordIso_card_of_imp_Card_order:
   137 "r =o |A| \<Longrightarrow> Card_order r"
   138 using card_of_Card_order Card_order_ordIso by blast
   139 
   140 lemma card_of_Well_order: "Well_order |A|"
   141 using card_of_Card_order unfolding card_order_on_def by auto
   142 
   143 lemma card_of_refl: "|A| =o |A|"
   144 using card_of_Well_order ordIso_reflexive by blast
   145 
   146 lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r"
   147 using card_of_card_order_on unfolding card_order_on_def by blast
   148 
   149 lemma card_of_ordIso:
   150 "(\<exists>f. bij_betw f A B) = ( |A| =o |B| )"
   151 proof(auto)
   152   fix f assume *: "bij_betw f A B"
   153   then obtain r where "well_order_on B r \<and> |A| =o r"
   154   using Well_order_iso_copy card_of_well_order_on by blast
   155   hence "|B| \<le>o |A|" using card_of_least
   156   ordLeq_ordIso_trans ordIso_symmetric by blast
   157   moreover
   158   {let ?g = "inv_into A f"
   159    have "bij_betw ?g B A" using * bij_betw_inv_into by blast
   160    then obtain r where "well_order_on A r \<and> |B| =o r"
   161    using Well_order_iso_copy card_of_well_order_on by blast
   162    hence "|A| \<le>o |B|" using card_of_least
   163    ordLeq_ordIso_trans ordIso_symmetric by blast
   164   }
   165   ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
   166 next
   167   assume "|A| =o |B|"
   168   then obtain f where "iso ( |A| ) ( |B| ) f"
   169   unfolding ordIso_def by auto
   170   hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
   171   thus "\<exists>f. bij_betw f A B" by auto
   172 qed
   173 
   174 lemma card_of_ordLeq:
   175 "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = ( |A| \<le>o |B| )"
   176 proof(auto)
   177   fix f assume *: "inj_on f A" and **: "f ` A \<le> B"
   178   {assume "|B| <o |A|"
   179    hence "|B| \<le>o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
   180    then obtain g where "embed ( |B| ) ( |A| ) g"
   181    unfolding ordLeq_def by auto
   182    hence 1: "inj_on g B \<and> g ` B \<le> A" using embed_inj_on[of "|B|" "|A|" "g"]
   183    card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
   184    embed_Field[of "|B|" "|A|" g] by auto
   185    obtain h where "bij_betw h A B"
   186    using * ** 1 Cantor_Bernstein[of f] by fastforce
   187    hence "|A| =o |B|" using card_of_ordIso by blast
   188    hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
   189   }
   190   thus "|A| \<le>o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
   191   by (auto simp: card_of_Well_order)
   192 next
   193   assume *: "|A| \<le>o |B|"
   194   obtain f where "embed ( |A| ) ( |B| ) f"
   195   using * unfolding ordLeq_def by auto
   196   hence "inj_on f A \<and> f ` A \<le> B" using embed_inj_on[of "|A|" "|B|" f]
   197   card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"]
   198   embed_Field[of "|A|" "|B|" f] by auto
   199   thus "\<exists>f. inj_on f A \<and> f ` A \<le> B" by auto
   200 qed
   201 
   202 lemma card_of_ordLeq2:
   203 "A \<noteq> {} \<Longrightarrow> (\<exists>g. g ` B = A) = ( |A| \<le>o |B| )"
   204 using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
   205 
   206 lemma card_of_ordLess:
   207 "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = ( |B| <o |A| )"
   208 proof-
   209   have "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = (\<not> |A| \<le>o |B| )"
   210   using card_of_ordLeq by blast
   211   also have "\<dots> = ( |B| <o |A| )"
   212   using card_of_Well_order[of A] card_of_Well_order[of B]
   213         not_ordLeq_iff_ordLess by blast
   214   finally show ?thesis .
   215 qed
   216 
   217 lemma card_of_ordLess2:
   218 "B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f ` A = B)) = ( |A| <o |B| )"
   219 using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
   220 
   221 lemma card_of_ordIsoI:
   222 assumes "bij_betw f A B"
   223 shows "|A| =o |B|"
   224 using assms unfolding card_of_ordIso[symmetric] by auto
   225 
   226 lemma card_of_ordLeqI:
   227 assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B"
   228 shows "|A| \<le>o |B|"
   229 using assms unfolding card_of_ordLeq[symmetric] by auto
   230 
   231 lemma card_of_unique:
   232 "card_order_on A r \<Longrightarrow> r =o |A|"
   233 by (simp only: card_order_on_ordIso card_of_card_order_on)
   234 
   235 lemma card_of_mono1:
   236 "A \<le> B \<Longrightarrow> |A| \<le>o |B|"
   237 using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
   238 
   239 lemma card_of_mono2:
   240 assumes "r \<le>o r'"
   241 shows "|Field r| \<le>o |Field r'|"
   242 proof-
   243   obtain f where
   244   1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
   245   using assms unfolding ordLeq_def
   246   by (auto simp add: well_order_on_Well_order)
   247   hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
   248   by (auto simp add: embed_inj_on embed_Field)
   249   thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
   250 qed
   251 
   252 lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|"
   253 by (simp add: ordIso_iff_ordLeq card_of_mono2)
   254 
   255 lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
   256 using card_of_least card_of_well_order_on well_order_on_Well_order by blast
   257 
   258 lemma card_of_Field_ordIso:
   259 assumes "Card_order r"
   260 shows "|Field r| =o r"
   261 proof-
   262   have "card_order_on (Field r) r"
   263   using assms card_order_on_Card_order by blast
   264   moreover have "card_order_on (Field r) |Field r|"
   265   using card_of_card_order_on by blast
   266   ultimately show ?thesis using card_order_on_ordIso by blast
   267 qed
   268 
   269 lemma Card_order_iff_ordIso_card_of:
   270 "Card_order r = (r =o |Field r| )"
   271 using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
   272 
   273 lemma Card_order_iff_ordLeq_card_of:
   274 "Card_order r = (r \<le>o |Field r| )"
   275 proof-
   276   have "Card_order r = (r =o |Field r| )"
   277   unfolding Card_order_iff_ordIso_card_of by simp
   278   also have "... = (r \<le>o |Field r| \<and> |Field r| \<le>o r)"
   279   unfolding ordIso_iff_ordLeq by simp
   280   also have "... = (r \<le>o |Field r| )"
   281   using card_of_Field_ordLess
   282   by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp)
   283   finally show ?thesis .
   284 qed
   285 
   286 lemma Card_order_iff_Restr_underS:
   287 assumes "Well_order r"
   288 shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )"
   289 using assms unfolding Card_order_iff_ordLeq_card_of
   290 using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
   291 
   292 lemma card_of_underS:
   293 assumes r: "Card_order r" and a: "a : Field r"
   294 shows "|underS r a| <o r"
   295 proof-
   296   let ?A = "underS r a"  let ?r' = "Restr r ?A"
   297   have 1: "Well_order r"
   298   using r unfolding card_order_on_def by simp
   299   have "Well_order ?r'" using 1 Well_order_Restr by auto
   300   moreover have "card_order_on (Field ?r') |Field ?r'|"
   301   using card_of_card_order_on .
   302   ultimately have "|Field ?r'| \<le>o ?r'"
   303   unfolding card_order_on_def by simp
   304   moreover have "Field ?r' = ?A"
   305   using 1 wo_rel.underS_ofilter Field_Restr_ofilter
   306   unfolding wo_rel_def by fastforce
   307   ultimately have "|?A| \<le>o ?r'" by simp
   308   also have "?r' <o |Field r|"
   309   using 1 a r Card_order_iff_Restr_underS by blast
   310   also have "|Field r| =o r"
   311   using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
   312   finally show ?thesis .
   313 qed
   314 
   315 lemma ordLess_Field:
   316 assumes "r <o r'"
   317 shows "|Field r| <o r'"
   318 proof-
   319   have "well_order_on (Field r) r" using assms unfolding ordLess_def
   320   by (auto simp add: well_order_on_Well_order)
   321   hence "|Field r| \<le>o r" using card_of_least by blast
   322   thus ?thesis using assms ordLeq_ordLess_trans by blast
   323 qed
   324 
   325 lemma internalize_card_of_ordLeq:
   326 "( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)"
   327 proof
   328   assume "|A| \<le>o r"
   329   then obtain p where 1: "Field p \<le> Field r \<and> |A| =o p \<and> p \<le>o r"
   330   using internalize_ordLeq[of "|A|" r] by blast
   331   hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
   332   hence "|Field p| =o p" using card_of_Field_ordIso by blast
   333   hence "|A| =o |Field p| \<and> |Field p| \<le>o r"
   334   using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
   335   thus "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" using 1 by blast
   336 next
   337   assume "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r"
   338   thus "|A| \<le>o r" using ordIso_ordLeq_trans by blast
   339 qed
   340 
   341 lemma internalize_card_of_ordLeq2:
   342 "( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )"
   343 using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
   344 
   345 
   346 subsection {* Cardinals versus set operations on arbitrary sets *}
   347 
   348 text{* Here we embark in a long journey of simple results showing
   349 that the standard set-theoretic operations are well-behaved w.r.t. the notion of
   350 cardinal -- essentially, this means that they preserve the ``cardinal identity"
   351 @{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
   352 *}
   353 
   354 lemma card_of_empty: "|{}| \<le>o |A|"
   355 using card_of_ordLeq inj_on_id by blast
   356 
   357 lemma card_of_empty1:
   358 assumes "Well_order r \<or> Card_order r"
   359 shows "|{}| \<le>o r"
   360 proof-
   361   have "Well_order r" using assms unfolding card_order_on_def by auto
   362   hence "|Field r| <=o r"
   363   using assms card_of_Field_ordLess by blast
   364   moreover have "|{}| \<le>o |Field r|" by (simp add: card_of_empty)
   365   ultimately show ?thesis using ordLeq_transitive by blast
   366 qed
   367 
   368 corollary Card_order_empty:
   369 "Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1)
   370 
   371 lemma card_of_empty2:
   372 assumes LEQ: "|A| =o |{}|"
   373 shows "A = {}"
   374 using assms card_of_ordIso[of A] bij_betw_empty2 by blast
   375 
   376 lemma card_of_empty3:
   377 assumes LEQ: "|A| \<le>o |{}|"
   378 shows "A = {}"
   379 using assms
   380 by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
   381               ordLeq_Well_order_simp)
   382 
   383 lemma card_of_empty_ordIso:
   384 "|{}::'a set| =o |{}::'b set|"
   385 using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
   386 
   387 lemma card_of_image:
   388 "|f ` A| <=o |A|"
   389 proof(cases "A = {}", simp add: card_of_empty)
   390   assume "A ~= {}"
   391   hence "f ` A ~= {}" by auto
   392   thus "|f ` A| \<le>o |A|"
   393   using card_of_ordLeq2[of "f ` A" A] by auto
   394 qed
   395 
   396 lemma surj_imp_ordLeq:
   397 assumes "B \<subseteq> f ` A"
   398 shows "|B| \<le>o |A|"
   399 proof-
   400   have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
   401   thus ?thesis using card_of_image ordLeq_transitive by blast
   402 qed
   403 
   404 lemma card_of_singl_ordLeq:
   405 assumes "A \<noteq> {}"
   406 shows "|{b}| \<le>o |A|"
   407 proof-
   408   obtain a where *: "a \<in> A" using assms by auto
   409   let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
   410   have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
   411   using * unfolding inj_on_def by auto
   412   thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
   413 qed
   414 
   415 corollary Card_order_singl_ordLeq:
   416 "\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r"
   417 using card_of_singl_ordLeq[of "Field r" b]
   418       card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
   419 
   420 lemma card_of_Pow: "|A| <o |Pow A|"
   421 using card_of_ordLess2[of "Pow A" A]  Cantors_paradox[of A]
   422       Pow_not_empty[of A] by auto
   423 
   424 corollary Card_order_Pow:
   425 "Card_order r \<Longrightarrow> r <o |Pow(Field r)|"
   426 using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
   427 
   428 lemma card_of_Plus1: "|A| \<le>o |A <+> B|"
   429 proof-
   430   have "Inl ` A \<le> A <+> B" by auto
   431   thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast
   432 qed
   433 
   434 corollary Card_order_Plus1:
   435 "Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|"
   436 using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
   437 
   438 lemma card_of_Plus2: "|B| \<le>o |A <+> B|"
   439 proof-
   440   have "Inr ` B \<le> A <+> B" by auto
   441   thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast
   442 qed
   443 
   444 corollary Card_order_Plus2:
   445 "Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|"
   446 using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
   447 
   448 lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
   449 proof-
   450   have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
   451   thus ?thesis using card_of_ordIso by auto
   452 qed
   453 
   454 lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
   455 proof-
   456   have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
   457   thus ?thesis using card_of_ordIso by auto
   458 qed
   459 
   460 lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
   461 proof-
   462   let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a
   463                                    | Inr b \<Rightarrow> Inl b"
   464   have "bij_betw ?f (A <+> B) (B <+> A)"
   465   unfolding bij_betw_def inj_on_def by force
   466   thus ?thesis using card_of_ordIso by blast
   467 qed
   468 
   469 lemma card_of_Plus_assoc:
   470 fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
   471 shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
   472 proof -
   473   def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).
   474   case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a
   475                                  |Inr b \<Rightarrow> Inr (Inl b))
   476            |Inr c \<Rightarrow> Inr (Inr c)"
   477   have "A <+> B <+> C \<subseteq> f ` ((A <+> B) <+> C)"
   478   proof
   479     fix x assume x: "x \<in> A <+> B <+> C"
   480     show "x \<in> f ` ((A <+> B) <+> C)"
   481     proof(cases x)
   482       case (Inl a)
   483       hence "a \<in> A" "x = f (Inl (Inl a))"
   484       using x unfolding f_def by auto
   485       thus ?thesis by auto
   486     next
   487       case (Inr bc) note 1 = Inr show ?thesis
   488       proof(cases bc)
   489         case (Inl b)
   490         hence "b \<in> B" "x = f (Inl (Inr b))"
   491         using x 1 unfolding f_def by auto
   492         thus ?thesis by auto
   493       next
   494         case (Inr c)
   495         hence "c \<in> C" "x = f (Inr c)"
   496         using x 1 unfolding f_def by auto
   497         thus ?thesis by auto
   498       qed
   499     qed
   500   qed
   501   hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
   502   unfolding bij_betw_def inj_on_def f_def by fastforce
   503   thus ?thesis using card_of_ordIso by blast
   504 qed
   505 
   506 lemma card_of_Plus_mono1:
   507 assumes "|A| \<le>o |B|"
   508 shows "|A <+> C| \<le>o |B <+> C|"
   509 proof-
   510   obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
   511   using assms card_of_ordLeq[of A] by fastforce
   512   obtain g where g_def:
   513   "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast
   514   have "inj_on g (A <+> C) \<and> g ` (A <+> C) \<le> (B <+> C)"
   515   proof-
   516     {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and
   517                           "g d1 = g d2"
   518      hence "d1 = d2" using 1 unfolding inj_on_def g_def by force
   519     }
   520     moreover
   521     {fix d assume "d \<in> A <+> C"
   522      hence "g d \<in> B <+> C"  using 1
   523      by(case_tac d, auto simp add: g_def)
   524     }
   525     ultimately show ?thesis unfolding inj_on_def by auto
   526   qed
   527   thus ?thesis using card_of_ordLeq by blast
   528 qed
   529 
   530 corollary ordLeq_Plus_mono1:
   531 assumes "r \<le>o r'"
   532 shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|"
   533 using assms card_of_mono2 card_of_Plus_mono1 by blast
   534 
   535 lemma card_of_Plus_mono2:
   536 assumes "|A| \<le>o |B|"
   537 shows "|C <+> A| \<le>o |C <+> B|"
   538 using assms card_of_Plus_mono1[of A B C]
   539       card_of_Plus_commute[of C A]  card_of_Plus_commute[of B C]
   540       ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]
   541 by blast
   542 
   543 corollary ordLeq_Plus_mono2:
   544 assumes "r \<le>o r'"
   545 shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|"
   546 using assms card_of_mono2 card_of_Plus_mono2 by blast
   547 
   548 lemma card_of_Plus_mono:
   549 assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
   550 shows "|A <+> C| \<le>o |B <+> D|"
   551 using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
   552       ordLeq_transitive[of "|A <+> C|"] by blast
   553 
   554 corollary ordLeq_Plus_mono:
   555 assumes "r \<le>o r'" and "p \<le>o p'"
   556 shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|"
   557 using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
   558 
   559 lemma card_of_Plus_cong1:
   560 assumes "|A| =o |B|"
   561 shows "|A <+> C| =o |B <+> C|"
   562 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
   563 
   564 corollary ordIso_Plus_cong1:
   565 assumes "r =o r'"
   566 shows "|(Field r) <+> C| =o |(Field r') <+> C|"
   567 using assms card_of_cong card_of_Plus_cong1 by blast
   568 
   569 lemma card_of_Plus_cong2:
   570 assumes "|A| =o |B|"
   571 shows "|C <+> A| =o |C <+> B|"
   572 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
   573 
   574 corollary ordIso_Plus_cong2:
   575 assumes "r =o r'"
   576 shows "|A <+> (Field r)| =o |A <+> (Field r')|"
   577 using assms card_of_cong card_of_Plus_cong2 by blast
   578 
   579 lemma card_of_Plus_cong:
   580 assumes "|A| =o |B|" and "|C| =o |D|"
   581 shows "|A <+> C| =o |B <+> D|"
   582 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
   583 
   584 corollary ordIso_Plus_cong:
   585 assumes "r =o r'" and "p =o p'"
   586 shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
   587 using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
   588 
   589 lemma card_of_Un_Plus_ordLeq:
   590 "|A \<union> B| \<le>o |A <+> B|"
   591 proof-
   592    let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
   593    have "inj_on ?f (A \<union> B) \<and> ?f ` (A \<union> B) \<le> A <+> B"
   594    unfolding inj_on_def by auto
   595    thus ?thesis using card_of_ordLeq by blast
   596 qed
   597 
   598 lemma card_of_Times1:
   599 assumes "A \<noteq> {}"
   600 shows "|B| \<le>o |B \<times> A|"
   601 proof(cases "B = {}", simp add: card_of_empty)
   602   assume *: "B \<noteq> {}"
   603   have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
   604   thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
   605                      card_of_ordLeq[of B "B \<times> A"] * by blast
   606 qed
   607 
   608 lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|"
   609 proof-
   610   let ?f = "\<lambda>(a::'a,b::'b). (b,a)"
   611   have "bij_betw ?f (A \<times> B) (B \<times> A)"
   612   unfolding bij_betw_def inj_on_def by auto
   613   thus ?thesis using card_of_ordIso by blast
   614 qed
   615 
   616 lemma card_of_Times2:
   617 assumes "A \<noteq> {}"   shows "|B| \<le>o |A \<times> B|"
   618 using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
   619       ordLeq_ordIso_trans by blast
   620 
   621 corollary Card_order_Times1:
   622 "\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|"
   623 using card_of_Times1[of B] card_of_Field_ordIso
   624       ordIso_ordLeq_trans ordIso_symmetric by blast
   625 
   626 corollary Card_order_Times2:
   627 "\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|"
   628 using card_of_Times2[of A] card_of_Field_ordIso
   629       ordIso_ordLeq_trans ordIso_symmetric by blast
   630 
   631 lemma card_of_Times3: "|A| \<le>o |A \<times> A|"
   632 using card_of_Times1[of A]
   633 by(cases "A = {}", simp add: card_of_empty, blast)
   634 
   635 lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|"
   636 proof-
   637   let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True)
   638                                   |Inr a \<Rightarrow> (a,False)"
   639   have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))"
   640   proof-
   641     {fix  c1 and c2 assume "?f c1 = ?f c2"
   642      hence "c1 = c2"
   643      by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
   644     }
   645     moreover
   646     {fix c assume "c \<in> A <+> A"
   647      hence "?f c \<in> A \<times> (UNIV::bool set)"
   648      by(case_tac c, auto)
   649     }
   650     moreover
   651     {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
   652      have "(a,bl) \<in> ?f ` ( A <+> A)"
   653      proof(cases bl)
   654        assume bl hence "?f(Inl a) = (a,bl)" by auto
   655        thus ?thesis using * by force
   656      next
   657        assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto
   658        thus ?thesis using * by force
   659      qed
   660     }
   661     ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
   662   qed
   663   thus ?thesis using card_of_ordIso by blast
   664 qed
   665 
   666 lemma card_of_Times_mono1:
   667 assumes "|A| \<le>o |B|"
   668 shows "|A \<times> C| \<le>o |B \<times> C|"
   669 proof-
   670   obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
   671   using assms card_of_ordLeq[of A] by fastforce
   672   obtain g where g_def:
   673   "g = (\<lambda>(a,c::'c). (f a,c))" by blast
   674   have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)"
   675   using 1 unfolding inj_on_def using g_def by auto
   676   thus ?thesis using card_of_ordLeq by blast
   677 qed
   678 
   679 corollary ordLeq_Times_mono1:
   680 assumes "r \<le>o r'"
   681 shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|"
   682 using assms card_of_mono2 card_of_Times_mono1 by blast
   683 
   684 lemma card_of_Times_mono2:
   685 assumes "|A| \<le>o |B|"
   686 shows "|C \<times> A| \<le>o |C \<times> B|"
   687 using assms card_of_Times_mono1[of A B C]
   688       card_of_Times_commute[of C A]  card_of_Times_commute[of B C]
   689       ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"]
   690 by blast
   691 
   692 corollary ordLeq_Times_mono2:
   693 assumes "r \<le>o r'"
   694 shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|"
   695 using assms card_of_mono2 card_of_Times_mono2 by blast
   696 
   697 lemma card_of_Sigma_mono1:
   698 assumes "\<forall>i \<in> I. |A i| \<le>o |B i|"
   699 shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|"
   700 proof-
   701   have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
   702   using assms by (auto simp add: card_of_ordLeq)
   703   with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
   704   obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i"
   705     by atomize_elim (auto intro: bchoice)
   706   obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
   707   have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
   708   using 1 unfolding inj_on_def using g_def by force
   709   thus ?thesis using card_of_ordLeq by blast
   710 qed
   711 
   712 corollary card_of_Sigma_Times:
   713 "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
   714 using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
   715 
   716 lemma card_of_UNION_Sigma:
   717 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
   718 using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
   719 
   720 lemma card_of_bool:
   721 assumes "a1 \<noteq> a2"
   722 shows "|UNIV::bool set| =o |{a1,a2}|"
   723 proof-
   724   let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"
   725   have "bij_betw ?f UNIV {a1,a2}"
   726   proof-
   727     {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"
   728      hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
   729     }
   730     moreover
   731     {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
   732     }
   733     moreover
   734     {fix a assume *: "a \<in> {a1,a2}"
   735      have "a \<in> ?f ` UNIV"
   736      proof(cases "a = a1")
   737        assume "a = a1"
   738        hence "?f True = a" by auto  thus ?thesis by blast
   739      next
   740        assume "a \<noteq> a1" hence "a = a2" using * by auto
   741        hence "?f False = a" by auto  thus ?thesis by blast
   742      qed
   743     }
   744     ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast
   745   qed
   746   thus ?thesis using card_of_ordIso by blast
   747 qed
   748 
   749 lemma card_of_Plus_Times_aux:
   750 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
   751         LEQ: "|A| \<le>o |B|"
   752 shows "|A <+> B| \<le>o |A \<times> B|"
   753 proof-
   754   have 1: "|UNIV::bool set| \<le>o |A|"
   755   using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
   756         ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast
   757   (*  *)
   758   have "|A <+> B| \<le>o |B <+> B|"
   759   using LEQ card_of_Plus_mono1 by blast
   760   moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"
   761   using card_of_Plus_Times_bool by blast
   762   moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"
   763   using 1 by (simp add: card_of_Times_mono2)
   764   moreover have " |B \<times> A| =o |A \<times> B|"
   765   using card_of_Times_commute by blast
   766   ultimately show "|A <+> B| \<le>o |A \<times> B|"
   767   using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]
   768         ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]
   769         ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]
   770   by blast
   771 qed
   772 
   773 lemma card_of_Plus_Times:
   774 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
   775         B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
   776 shows "|A <+> B| \<le>o |A \<times> B|"
   777 proof-
   778   {assume "|A| \<le>o |B|"
   779    hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
   780   }
   781   moreover
   782   {assume "|B| \<le>o |A|"
   783    hence "|B <+> A| \<le>o |B \<times> A|"
   784    using assms by (auto simp add: card_of_Plus_Times_aux)
   785    hence ?thesis
   786    using card_of_Plus_commute card_of_Times_commute
   787          ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
   788   }
   789   ultimately show ?thesis
   790   using card_of_Well_order[of A] card_of_Well_order[of B]
   791         ordLeq_total[of "|A|"] by blast
   792 qed
   793 
   794 lemma card_of_ordLeq_finite:
   795 assumes "|A| \<le>o |B|" and "finite B"
   796 shows "finite A"
   797 using assms unfolding ordLeq_def
   798 using embed_inj_on[of "|A|" "|B|"]  embed_Field[of "|A|" "|B|"]
   799       Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
   800 
   801 lemma card_of_ordLeq_infinite:
   802 assumes "|A| \<le>o |B|" and "\<not> finite A"
   803 shows "\<not> finite B"
   804 using assms card_of_ordLeq_finite by auto
   805 
   806 lemma card_of_ordIso_finite:
   807 assumes "|A| =o |B|"
   808 shows "finite A = finite B"
   809 using assms unfolding ordIso_def iso_def[abs_def]
   810 by (auto simp: bij_betw_finite Field_card_of)
   811 
   812 lemma card_of_ordIso_finite_Field:
   813 assumes "Card_order r" and "r =o |A|"
   814 shows "finite(Field r) = finite A"
   815 using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
   816 
   817 
   818 subsection {* Cardinals versus set operations involving infinite sets *}
   819 
   820 text{* Here we show that, for infinite sets, most set-theoretic constructions
   821 do not increase the cardinality.  The cornerstone for this is
   822 theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
   823 does not increase cardinality -- the proof of this fact adapts a standard
   824 set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
   825 at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
   826 
   827 lemma infinite_iff_card_of_nat:
   828 "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
   829 unfolding infinite_iff_countable_subset card_of_ordLeq ..
   830 
   831 text{* The next two results correspond to the ZF fact that all infinite cardinals are
   832 limit ordinals: *}
   833 
   834 lemma Card_order_infinite_not_under:
   835 assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
   836 shows "\<not> (\<exists>a. Field r = under r a)"
   837 proof(auto)
   838   have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
   839   using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
   840   fix a assume *: "Field r = under r a"
   841   show False
   842   proof(cases "a \<in> Field r")
   843     assume Case1: "a \<notin> Field r"
   844     hence "under r a = {}" unfolding Field_def under_def by auto
   845     thus False using INF *  by auto
   846   next
   847     let ?r' = "Restr r (underS r a)"
   848     assume Case2: "a \<in> Field r"
   849     hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
   850     using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
   851     have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
   852     using 0 wo_rel.underS_ofilter * 1 Case2 by fast
   853     hence "?r' <o r" using 0 using ofilter_ordLess by blast
   854     moreover
   855     have "Field ?r' = underS r a \<and> Well_order ?r'"
   856     using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
   857     ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
   858     moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
   859     ultimately have "|underS r a| <o |under r a|"
   860     using ordIso_symmetric ordLess_ordIso_trans by blast
   861     moreover
   862     {have "\<exists>f. bij_betw f (under r a) (underS r a)"
   863      using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
   864      hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
   865     }
   866     ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
   867   qed
   868 qed
   869 
   870 lemma infinite_Card_order_limit:
   871 assumes r: "Card_order r" and "\<not>finite (Field r)"
   872 and a: "a : Field r"
   873 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
   874 proof-
   875   have "Field r \<noteq> under r a"
   876   using assms Card_order_infinite_not_under by blast
   877   moreover have "under r a \<le> Field r"
   878   using under_Field .
   879   ultimately have "under r a < Field r" by blast
   880   then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
   881   unfolding under_def by blast
   882   moreover have ba: "b \<noteq> a"
   883   using 1 r unfolding card_order_on_def well_order_on_def
   884   linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
   885   ultimately have "(a,b) : r"
   886   using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
   887   total_on_def by blast
   888   thus ?thesis using 1 ba by auto
   889 qed
   890 
   891 theorem Card_order_Times_same_infinite:
   892 assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
   893 shows "|Field r \<times> Field r| \<le>o r"
   894 proof-
   895   obtain phi where phi_def:
   896   "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
   897                       \<not> |Field r \<times> Field r| \<le>o r )" by blast
   898   have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
   899   unfolding phi_def card_order_on_def by auto
   900   have Ft: "\<not>(\<exists>r. phi r)"
   901   proof
   902     assume "\<exists>r. phi r"
   903     hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"
   904     using temp1 by auto
   905     then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and
   906                    3: "Card_order r \<and> Well_order r"
   907     using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
   908     let ?A = "Field r"  let ?r' = "bsqr r"
   909     have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"
   910     using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
   911     have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"
   912     using card_of_Card_order card_of_Well_order by blast
   913     (*  *)
   914     have "r <o |?A \<times> ?A|"
   915     using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
   916     moreover have "|?A \<times> ?A| \<le>o ?r'"
   917     using card_of_least[of "?A \<times> ?A"] 4 by auto
   918     ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
   919     then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"
   920     unfolding ordLess_def embedS_def[abs_def]
   921     by (auto simp add: Field_bsqr)
   922     let ?B = "f ` ?A"
   923     have "|?A| =o |?B|"
   924     using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
   925     hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
   926     (*  *)
   927     have "wo_rel.ofilter ?r' ?B"
   928     using 6 embed_Field_ofilter 3 4 by blast
   929     hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"
   930     using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
   931     hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
   932     using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
   933     have "\<not> (\<exists>a. Field r = under r a)"
   934     using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
   935     then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
   936     using temp2 3 bsqr_ofilter[of r ?B] by blast
   937     hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast
   938     hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast
   939     let ?r1 = "Restr r A1"
   940     have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
   941     moreover
   942     {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
   943      hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast
   944     }
   945     ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
   946     (*  *)
   947     have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
   948     hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
   949     hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by blast
   950     moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
   951     using card_of_Card_order[of A1] card_of_Well_order[of A1]
   952     by (simp add: Field_card_of)
   953     moreover have "\<not> r \<le>o | A1 |"
   954     using temp4 11 3 using not_ordLeq_iff_ordLess by blast
   955     ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
   956     by (simp add: card_of_card_order_on)
   957     hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
   958     using 2 unfolding phi_def by blast
   959     hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto
   960     hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast
   961     thus False using 11 not_ordLess_ordLeq by auto
   962   qed
   963   thus ?thesis using assms unfolding phi_def by blast
   964 qed
   965 
   966 corollary card_of_Times_same_infinite:
   967 assumes "\<not>finite A"
   968 shows "|A \<times> A| =o |A|"
   969 proof-
   970   let ?r = "|A|"
   971   have "Field ?r = A \<and> Card_order ?r"
   972   using Field_card_of card_of_Card_order[of A] by fastforce
   973   hence "|A \<times> A| \<le>o |A|"
   974   using Card_order_Times_same_infinite[of ?r] assms by auto
   975   thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
   976 qed
   977 
   978 lemma card_of_Times_infinite:
   979 assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
   980 shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
   981 proof-
   982   have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
   983   using assms by (simp add: card_of_Times1 card_of_Times2)
   984   moreover
   985   {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"
   986    using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
   987    moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast
   988    ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"
   989    using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto
   990   }
   991   ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
   992 qed
   993 
   994 corollary Card_order_Times_infinite:
   995 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
   996         NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
   997 shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
   998 proof-
   999   have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"
  1000   using assms by (simp add: card_of_Times_infinite card_of_mono2)
  1001   thus ?thesis
  1002   using assms card_of_Field_ordIso[of r]
  1003         ordIso_transitive[of "|Field r \<times> Field p|"]
  1004         ordIso_transitive[of _ "|Field r|"] by blast
  1005 qed
  1006 
  1007 lemma card_of_Sigma_ordLeq_infinite:
  1008 assumes INF: "\<not>finite B" and
  1009         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
  1010 shows "|SIGMA i : I. A i| \<le>o |B|"
  1011 proof(cases "I = {}", simp add: card_of_empty)
  1012   assume *: "I \<noteq> {}"
  1013   have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
  1014   using LEQ card_of_Sigma_Times by blast
  1015   moreover have "|I \<times> B| =o |B|"
  1016   using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
  1017   ultimately show ?thesis using ordLeq_ordIso_trans by blast
  1018 qed
  1019 
  1020 lemma card_of_Sigma_ordLeq_infinite_Field:
  1021 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
  1022         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
  1023 shows "|SIGMA i : I. A i| \<le>o r"
  1024 proof-
  1025   let ?B  = "Field r"
  1026   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
  1027   ordIso_symmetric by blast
  1028   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
  1029   using LEQ_I LEQ ordLeq_ordIso_trans by blast+
  1030   hence  "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ
  1031   card_of_Sigma_ordLeq_infinite by blast
  1032   thus ?thesis using 1 ordLeq_ordIso_trans by blast
  1033 qed
  1034 
  1035 lemma card_of_Times_ordLeq_infinite_Field:
  1036 "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
  1037  \<Longrightarrow> |A <*> B| \<le>o r"
  1038 by(simp add: card_of_Sigma_ordLeq_infinite_Field)
  1039 
  1040 lemma card_of_Times_infinite_simps:
  1041 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
  1042 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
  1043 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
  1044 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
  1045 by (auto simp add: card_of_Times_infinite ordIso_symmetric)
  1046 
  1047 lemma card_of_UNION_ordLeq_infinite:
  1048 assumes INF: "\<not>finite B" and
  1049         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
  1050 shows "|\<Union> i \<in> I. A i| \<le>o |B|"
  1051 proof(cases "I = {}", simp add: card_of_empty)
  1052   assume *: "I \<noteq> {}"
  1053   have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
  1054   using card_of_UNION_Sigma by blast
  1055   moreover have "|SIGMA i : I. A i| \<le>o |B|"
  1056   using assms card_of_Sigma_ordLeq_infinite by blast
  1057   ultimately show ?thesis using ordLeq_transitive by blast
  1058 qed
  1059 
  1060 corollary card_of_UNION_ordLeq_infinite_Field:
  1061 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
  1062         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
  1063 shows "|\<Union> i \<in> I. A i| \<le>o r"
  1064 proof-
  1065   let ?B  = "Field r"
  1066   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
  1067   ordIso_symmetric by blast
  1068   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
  1069   using LEQ_I LEQ ordLeq_ordIso_trans by blast+
  1070   hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
  1071   card_of_UNION_ordLeq_infinite by blast
  1072   thus ?thesis using 1 ordLeq_ordIso_trans by blast
  1073 qed
  1074 
  1075 lemma card_of_Plus_infinite1:
  1076 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
  1077 shows "|A <+> B| =o |A|"
  1078 proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
  1079   let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
  1080   assume *: "B \<noteq> {}"
  1081   then obtain b1 where 1: "b1 \<in> B" by blast
  1082   show ?thesis
  1083   proof(cases "B = {b1}")
  1084     assume Case1: "B = {b1}"
  1085     have 2: "bij_betw ?Inl A ((?Inl ` A))"
  1086     unfolding bij_betw_def inj_on_def by auto
  1087     hence 3: "\<not>finite (?Inl ` A)"
  1088     using INF bij_betw_finite[of ?Inl A] by blast
  1089     let ?A' = "?Inl ` A \<union> {?Inr b1}"
  1090     obtain g where "bij_betw g (?Inl ` A) ?A'"
  1091     using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
  1092     moreover have "?A' = A <+> B" using Case1 by blast
  1093     ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
  1094     hence "bij_betw (g o ?Inl) A (A <+> B)"
  1095     using 2 by (auto simp add: bij_betw_trans)
  1096     thus ?thesis using card_of_ordIso ordIso_symmetric by blast
  1097   next
  1098     assume Case2: "B \<noteq> {b1}"
  1099     with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce
  1100     obtain f where "inj_on f B \<and> f ` B \<le> A"
  1101     using LEQ card_of_ordLeq[of B] by fastforce
  1102     with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"
  1103     unfolding inj_on_def by auto
  1104     with 3 have "|A <+> B| \<le>o |A \<times> B|"
  1105     by (auto simp add: card_of_Plus_Times)
  1106     moreover have "|A \<times> B| =o |A|"
  1107     using assms * by (simp add: card_of_Times_infinite_simps)
  1108     ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
  1109     thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
  1110   qed
  1111 qed
  1112 
  1113 lemma card_of_Plus_infinite2:
  1114 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
  1115 shows "|B <+> A| =o |A|"
  1116 using assms card_of_Plus_commute card_of_Plus_infinite1
  1117 ordIso_equivalence by blast
  1118 
  1119 lemma card_of_Plus_infinite:
  1120 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
  1121 shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
  1122 using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
  1123 
  1124 corollary Card_order_Plus_infinite:
  1125 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
  1126         LEQ: "p \<le>o r"
  1127 shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
  1128 proof-
  1129   have "| Field r <+> Field p | =o | Field r | \<and>
  1130         | Field p <+> Field r | =o | Field r |"
  1131   using assms by (simp add: card_of_Plus_infinite card_of_mono2)
  1132   thus ?thesis
  1133   using assms card_of_Field_ordIso[of r]
  1134         ordIso_transitive[of "|Field r <+> Field p|"]
  1135         ordIso_transitive[of _ "|Field r|"] by blast
  1136 qed
  1137 
  1138 
  1139 subsection {* The cardinal $\omega$ and the finite cardinals *}
  1140 
  1141 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
  1142 order relation on
  1143 @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
  1144 shall be the restrictions of these relations to the numbers smaller than
  1145 fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
  1146 
  1147 definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
  1148 definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
  1149 
  1150 abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
  1151 where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
  1152 
  1153 lemma infinite_cartesian_product:
  1154 assumes "\<not>finite A" "\<not>finite B"
  1155 shows "\<not>finite (A \<times> B)"
  1156 proof
  1157   assume "finite (A \<times> B)"
  1158   from assms(1) have "A \<noteq> {}" by auto
  1159   with `finite (A \<times> B)` have "finite B" using finite_cartesian_productD2 by auto
  1160   with assms(2) show False by simp
  1161 qed
  1162 
  1163 
  1164 subsubsection {* First as well-orders *}
  1165 
  1166 lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
  1167 by(unfold Field_def natLeq_def, auto)
  1168 
  1169 lemma natLeq_Refl: "Refl natLeq"
  1170 unfolding refl_on_def Field_def natLeq_def by auto
  1171 
  1172 lemma natLeq_trans: "trans natLeq"
  1173 unfolding trans_def natLeq_def by auto
  1174 
  1175 lemma natLeq_Preorder: "Preorder natLeq"
  1176 unfolding preorder_on_def
  1177 by (auto simp add: natLeq_Refl natLeq_trans)
  1178 
  1179 lemma natLeq_antisym: "antisym natLeq"
  1180 unfolding antisym_def natLeq_def by auto
  1181 
  1182 lemma natLeq_Partial_order: "Partial_order natLeq"
  1183 unfolding partial_order_on_def
  1184 by (auto simp add: natLeq_Preorder natLeq_antisym)
  1185 
  1186 lemma natLeq_Total: "Total natLeq"
  1187 unfolding total_on_def natLeq_def by auto
  1188 
  1189 lemma natLeq_Linear_order: "Linear_order natLeq"
  1190 unfolding linear_order_on_def
  1191 by (auto simp add: natLeq_Partial_order natLeq_Total)
  1192 
  1193 lemma natLeq_natLess_Id: "natLess = natLeq - Id"
  1194 unfolding natLeq_def natLess_def by auto
  1195 
  1196 lemma natLeq_Well_order: "Well_order natLeq"
  1197 unfolding well_order_on_def
  1198 using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
  1199 
  1200 lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
  1201 unfolding Field_def by auto
  1202 
  1203 lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
  1204 unfolding underS_def natLeq_def by auto
  1205 
  1206 lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
  1207 unfolding natLeq_def by force
  1208 
  1209 lemma Restr_natLeq2:
  1210 "Restr natLeq (underS natLeq n) = natLeq_on n"
  1211 by (auto simp add: Restr_natLeq natLeq_underS_less)
  1212 
  1213 lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
  1214 using Restr_natLeq[of n] natLeq_Well_order
  1215       Well_order_Restr[of natLeq "{x. x < n}"] by auto
  1216 
  1217 corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
  1218 using natLeq_on_Well_order Field_natLeq_on by auto
  1219 
  1220 lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
  1221 unfolding wo_rel_def using natLeq_on_Well_order .
  1222 
  1223 
  1224 subsubsection {* Then as cardinals *}
  1225 
  1226 lemma natLeq_Card_order: "Card_order natLeq"
  1227 proof(auto simp add: natLeq_Well_order
  1228       Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
  1229   fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
  1230   moreover have "\<not>finite(UNIV::nat set)" by auto
  1231   ultimately show "natLeq_on n <o |UNIV::nat set|"
  1232   using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
  1233         Field_card_of[of "UNIV::nat set"]
  1234         card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
  1235 qed
  1236 
  1237 corollary card_of_Field_natLeq:
  1238 "|Field natLeq| =o natLeq"
  1239 using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
  1240       ordIso_symmetric[of natLeq] by blast
  1241 
  1242 corollary card_of_nat:
  1243 "|UNIV::nat set| =o natLeq"
  1244 using Field_natLeq card_of_Field_natLeq by auto
  1245 
  1246 corollary infinite_iff_natLeq_ordLeq:
  1247 "\<not>finite A = ( natLeq \<le>o |A| )"
  1248 using infinite_iff_card_of_nat[of A] card_of_nat
  1249       ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
  1250 
  1251 corollary finite_iff_ordLess_natLeq:
  1252 "finite A = ( |A| <o natLeq)"
  1253 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
  1254       card_of_Well_order natLeq_Well_order by blast
  1255 
  1256 
  1257 subsection {* The successor of a cardinal *}
  1258 
  1259 text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
  1260 being a successor cardinal of @{text "r"}. Although the definition does
  1261 not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
  1262 
  1263 definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
  1264 where
  1265 "isCardSuc r r' \<equiv>
  1266  Card_order r' \<and> r <o r' \<and>
  1267  (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
  1268 
  1269 text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},
  1270 by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
  1271 Again, the picked item shall be proved unique up to order-isomorphism. *}
  1272 
  1273 definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
  1274 where
  1275 "cardSuc r \<equiv> SOME r'. isCardSuc r r'"
  1276 
  1277 lemma exists_minim_Card_order:
  1278 "\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
  1279 unfolding card_order_on_def using exists_minim_Well_order by blast
  1280 
  1281 lemma exists_isCardSuc:
  1282 assumes "Card_order r"
  1283 shows "\<exists>r'. isCardSuc r r'"
  1284 proof-
  1285   let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"
  1286   have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms
  1287   by (simp add: card_of_Card_order Card_order_Pow)
  1288   then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"
  1289   using exists_minim_Card_order[of ?R] by blast
  1290   thus ?thesis unfolding isCardSuc_def by auto
  1291 qed
  1292 
  1293 lemma cardSuc_isCardSuc:
  1294 assumes "Card_order r"
  1295 shows "isCardSuc r (cardSuc r)"
  1296 unfolding cardSuc_def using assms
  1297 by (simp add: exists_isCardSuc someI_ex)
  1298 
  1299 lemma cardSuc_Card_order:
  1300 "Card_order r \<Longrightarrow> Card_order(cardSuc r)"
  1301 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
  1302 
  1303 lemma cardSuc_greater:
  1304 "Card_order r \<Longrightarrow> r <o cardSuc r"
  1305 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
  1306 
  1307 lemma cardSuc_ordLeq:
  1308 "Card_order r \<Longrightarrow> r \<le>o cardSuc r"
  1309 using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
  1310 
  1311 text{* The minimality property of @{text "cardSuc"} originally present in its definition
  1312 is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
  1313 
  1314 lemma cardSuc_least_aux:
  1315 "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
  1316 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
  1317 
  1318 text{* But from this we can infer general minimality: *}
  1319 
  1320 lemma cardSuc_least:
  1321 assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
  1322 shows "cardSuc r \<le>o r'"
  1323 proof-
  1324   let ?p = "cardSuc r"
  1325   have 0: "Well_order ?p \<and> Well_order r'"
  1326   using assms cardSuc_Card_order unfolding card_order_on_def by blast
  1327   {assume "r' <o ?p"
  1328    then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"
  1329    using internalize_ordLess[of r' ?p] by blast
  1330    (*  *)
  1331    have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
  1332    moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
  1333    ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast
  1334    hence False using 2 not_ordLess_ordLeq by blast
  1335   }
  1336   thus ?thesis using 0 ordLess_or_ordLeq by blast
  1337 qed
  1338 
  1339 lemma cardSuc_ordLess_ordLeq:
  1340 assumes CARD: "Card_order r" and CARD': "Card_order r'"
  1341 shows "(r <o r') = (cardSuc r \<le>o r')"
  1342 proof(auto simp add: assms cardSuc_least)
  1343   assume "cardSuc r \<le>o r'"
  1344   thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast
  1345 qed
  1346 
  1347 lemma cardSuc_ordLeq_ordLess:
  1348 assumes CARD: "Card_order r" and CARD': "Card_order r'"
  1349 shows "(r' <o cardSuc r) = (r' \<le>o r)"
  1350 proof-
  1351   have "Well_order r \<and> Well_order r'"
  1352   using assms unfolding card_order_on_def by auto
  1353   moreover have "Well_order(cardSuc r)"
  1354   using assms cardSuc_Card_order card_order_on_def by blast
  1355   ultimately show ?thesis
  1356   using assms cardSuc_ordLess_ordLeq[of r r']
  1357   not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
  1358 qed
  1359 
  1360 lemma cardSuc_mono_ordLeq:
  1361 assumes CARD: "Card_order r" and CARD': "Card_order r'"
  1362 shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"
  1363 using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
  1364 
  1365 lemma cardSuc_invar_ordIso:
  1366 assumes CARD: "Card_order r" and CARD': "Card_order r'"
  1367 shows "(cardSuc r =o cardSuc r') = (r =o r')"
  1368 proof-
  1369   have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
  1370   using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
  1371   thus ?thesis
  1372   using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
  1373   using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
  1374 qed
  1375 
  1376 lemma card_of_cardSuc_finite:
  1377 "finite(Field(cardSuc |A| )) = finite A"
  1378 proof
  1379   assume *: "finite (Field (cardSuc |A| ))"
  1380   have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
  1381   using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
  1382   hence "|A| \<le>o |Field(cardSuc |A| )|"
  1383   using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
  1384   ordLeq_ordIso_trans by blast
  1385   thus "finite A" using * card_of_ordLeq_finite by blast
  1386 next
  1387   assume "finite A"
  1388   then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
  1389   then show "finite (Field (cardSuc |A| ))"
  1390   proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
  1391     show "cardSuc |A| \<le>o |Pow A|"
  1392       by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
  1393   qed
  1394 qed
  1395 
  1396 lemma cardSuc_finite:
  1397 assumes "Card_order r"
  1398 shows "finite (Field (cardSuc r)) = finite (Field r)"
  1399 proof-
  1400   let ?A = "Field r"
  1401   have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
  1402   hence "cardSuc |?A| =o cardSuc r" using assms
  1403   by (simp add: card_of_Card_order cardSuc_invar_ordIso)
  1404   moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
  1405   by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
  1406   moreover
  1407   {have "|Field (cardSuc r) | =o cardSuc r"
  1408    using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
  1409    hence "cardSuc r =o |Field (cardSuc r) |"
  1410    using ordIso_symmetric by blast
  1411   }
  1412   ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
  1413   using ordIso_transitive by blast
  1414   hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
  1415   using card_of_ordIso_finite by blast
  1416   thus ?thesis by (simp only: card_of_cardSuc_finite)
  1417 qed
  1418 
  1419 lemma card_of_Plus_ordLess_infinite:
  1420 assumes INF: "\<not>finite C" and
  1421         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
  1422 shows "|A <+> B| <o |C|"
  1423 proof(cases "A = {} \<or> B = {}")
  1424   assume Case1: "A = {} \<or> B = {}"
  1425   hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"
  1426   using card_of_Plus_empty1 card_of_Plus_empty2 by blast
  1427   hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"
  1428   using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
  1429   thus ?thesis using LESS1 LESS2
  1430        ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
  1431        ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
  1432 next
  1433   assume Case2: "\<not>(A = {} \<or> B = {})"
  1434   {assume *: "|C| \<le>o |A <+> B|"
  1435    hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
  1436    hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
  1437    {assume Case21: "|A| \<le>o |B|"
  1438     hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
  1439     hence "|A <+> B| =o |B|" using Case2 Case21
  1440     by (auto simp add: card_of_Plus_infinite)
  1441     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
  1442    }
  1443    moreover
  1444    {assume Case22: "|B| \<le>o |A|"
  1445     hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
  1446     hence "|A <+> B| =o |A|" using Case2 Case22
  1447     by (auto simp add: card_of_Plus_infinite)
  1448     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
  1449    }
  1450    ultimately have False using ordLeq_total card_of_Well_order[of A]
  1451    card_of_Well_order[of B] by blast
  1452   }
  1453   thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
  1454   card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
  1455 qed
  1456 
  1457 lemma card_of_Plus_ordLess_infinite_Field:
  1458 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
  1459         LESS1: "|A| <o r" and LESS2: "|B| <o r"
  1460 shows "|A <+> B| <o r"
  1461 proof-
  1462   let ?C  = "Field r"
  1463   have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
  1464   ordIso_symmetric by blast
  1465   hence "|A| <o |?C|"  "|B| <o |?C|"
  1466   using LESS1 LESS2 ordLess_ordIso_trans by blast+
  1467   hence  "|A <+> B| <o |?C|" using INF
  1468   card_of_Plus_ordLess_infinite by blast
  1469   thus ?thesis using 1 ordLess_ordIso_trans by blast
  1470 qed
  1471 
  1472 lemma card_of_Plus_ordLeq_infinite_Field:
  1473 assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
  1474 and c: "Card_order r"
  1475 shows "|A <+> B| \<le>o r"
  1476 proof-
  1477   let ?r' = "cardSuc r"
  1478   have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
  1479   by (simp add: cardSuc_Card_order cardSuc_finite)
  1480   moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
  1481   by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
  1482   ultimately have "|A <+> B| <o ?r'"
  1483   using card_of_Plus_ordLess_infinite_Field by blast
  1484   thus ?thesis using c r
  1485   by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
  1486 qed
  1487 
  1488 lemma card_of_Un_ordLeq_infinite_Field:
  1489 assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
  1490 and "Card_order r"
  1491 shows "|A Un B| \<le>o r"
  1492 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
  1493 ordLeq_transitive by fast
  1494 
  1495 
  1496 subsection {* Regular cardinals *}
  1497 
  1498 definition cofinal where
  1499 "cofinal A r \<equiv>
  1500  ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
  1501 
  1502 definition regularCard where
  1503 "regularCard r \<equiv>
  1504  ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
  1505 
  1506 definition relChain where
  1507 "relChain r As \<equiv>
  1508  ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
  1509 
  1510 lemma regularCard_UNION:
  1511 assumes r: "Card_order r"   "regularCard r"
  1512 and As: "relChain r As"
  1513 and Bsub: "B \<le> (UN i : Field r. As i)"
  1514 and cardB: "|B| <o r"
  1515 shows "EX i : Field r. B \<le> As i"
  1516 proof-
  1517   let ?phi = "%b j. j : Field r \<and> b : As j"
  1518   have "ALL b : B. EX j. ?phi b j" using Bsub by blast
  1519   then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"
  1520   using bchoice[of B ?phi] by blast
  1521   let ?K = "f ` B"
  1522   {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"
  1523    have 2: "cofinal ?K r"
  1524    unfolding cofinal_def proof auto
  1525      fix i assume i: "i : Field r"
  1526      with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast
  1527      hence "i \<noteq> f b \<and> ~ (f b,i) : r"
  1528      using As f unfolding relChain_def by auto
  1529      hence "i \<noteq> f b \<and> (i, f b) : r" using r
  1530      unfolding card_order_on_def well_order_on_def linear_order_on_def
  1531      total_on_def using i f b by auto
  1532      with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
  1533    qed
  1534    moreover have "?K \<le> Field r" using f by blast
  1535    ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast
  1536    moreover
  1537    {
  1538     have "|?K| <=o |B|" using card_of_image .
  1539     hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast
  1540    }
  1541    ultimately have False using not_ordLess_ordIso by blast
  1542   }
  1543   thus ?thesis by blast
  1544 qed
  1545 
  1546 lemma infinite_cardSuc_regularCard:
  1547 assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
  1548 shows "regularCard (cardSuc r)"
  1549 proof-
  1550   let ?r' = "cardSuc r"
  1551   have r': "Card_order ?r'"
  1552   "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"
  1553   using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
  1554   show ?thesis
  1555   unfolding regularCard_def proof auto
  1556     fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
  1557     hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
  1558     also have 22: "|Field ?r'| =o ?r'"
  1559     using r' by (simp add: card_of_Field_ordIso[of ?r'])
  1560     finally have "|K| \<le>o ?r'" .
  1561     moreover
  1562     {let ?L = "UN j : K. underS ?r' j"
  1563      let ?J = "Field r"
  1564      have rJ: "r =o |?J|"
  1565      using r_card card_of_Field_ordIso ordIso_symmetric by blast
  1566      assume "|K| <o ?r'"
  1567      hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
  1568      hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
  1569      moreover
  1570      {have "ALL j : K. |underS ?r' j| <o ?r'"
  1571       using r' 1 by (auto simp: card_of_underS)
  1572       hence "ALL j : K. |underS ?r' j| \<le>o r"
  1573       using r' card_of_Card_order by blast
  1574       hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
  1575       using rJ ordLeq_ordIso_trans by blast
  1576      }
  1577      ultimately have "|?L| \<le>o |?J|"
  1578      using r_inf card_of_UNION_ordLeq_infinite by blast
  1579      hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
  1580      hence "|?L| <o ?r'" using r' card_of_Card_order by blast
  1581      moreover
  1582      {
  1583       have "Field ?r' \<le> ?L"
  1584       using 2 unfolding underS_def cofinal_def by auto
  1585       hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
  1586       hence "?r' \<le>o |?L|"
  1587       using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
  1588      }
  1589      ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast
  1590      hence False using ordLess_irreflexive by blast
  1591     }
  1592     ultimately show "|K| =o ?r'"
  1593     unfolding ordLeq_iff_ordLess_or_ordIso by blast
  1594   qed
  1595 qed
  1596 
  1597 lemma cardSuc_UNION:
  1598 assumes r: "Card_order r" and "\<not>finite (Field r)"
  1599 and As: "relChain (cardSuc r) As"
  1600 and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
  1601 and cardB: "|B| <=o r"
  1602 shows "EX i : Field (cardSuc r). B \<le> As i"
  1603 proof-
  1604   let ?r' = "cardSuc r"
  1605   have "Card_order ?r' \<and> |B| <o ?r'"
  1606   using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
  1607   card_of_Card_order by blast
  1608   moreover have "regularCard ?r'"
  1609   using assms by(simp add: infinite_cardSuc_regularCard)
  1610   ultimately show ?thesis
  1611   using As Bsub cardB regularCard_UNION by blast
  1612 qed
  1613 
  1614 
  1615 subsection {* Others *}
  1616 
  1617 lemma card_of_Func_Times:
  1618 "|Func (A <*> B) C| =o |Func A (Func B C)|"
  1619 unfolding card_of_ordIso[symmetric]
  1620 using bij_betw_curr by blast
  1621 
  1622 lemma card_of_Pow_Func:
  1623 "|Pow A| =o |Func A (UNIV::bool set)|"
  1624 proof-
  1625   def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False)
  1626                             else undefined"
  1627   have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
  1628   unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
  1629     fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
  1630     thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)
  1631   next
  1632     show "F ` Pow A = Func A UNIV"
  1633     proof safe
  1634       fix f assume f: "f \<in> Func A (UNIV::bool set)"
  1635       show "f \<in> F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
  1636         let ?A1 = "{a \<in> A. f a = True}"
  1637         show "f = F ?A1" unfolding F_def apply(rule ext)
  1638         using f unfolding Func_def mem_Collect_eq by auto
  1639       qed auto
  1640     qed(unfold Func_def mem_Collect_eq F_def, auto)
  1641   qed
  1642   thus ?thesis unfolding card_of_ordIso[symmetric] by blast
  1643 qed
  1644 
  1645 lemma card_of_Func_UNIV:
  1646 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|"
  1647 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
  1648   let ?F = "\<lambda> f (a::'a). ((f a)::'b)"
  1649   show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"
  1650   unfolding bij_betw_def inj_on_def proof safe
  1651     fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
  1652     hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
  1653     then obtain f where f: "\<forall> a. h a = f a" by blast
  1654     hence "range f \<subseteq> B" using h unfolding Func_def by auto
  1655     thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
  1656   qed(unfold Func_def fun_eq_iff, auto)
  1657 qed
  1658 
  1659 end