src/HOL/BNF_Cardinal_Order_Relation.thy
 author traytel Thu Feb 20 13:53:26 2014 +0100 (2014-02-20) changeset 55603 48596c45bf7f parent 55206 f7358e55018f child 55811 aa1acc25126b permissions -rw-r--r--
less flex-flex pairs (thanks to Lars' statistics)
     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 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 <= f  A"

   398 shows "|B| <=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_ordLeqI2:

   405 assumes "B \<subseteq> f  A"

   406 shows "|B| \<le>o |A|"

   407 using assms by (metis surj_imp_ordLeq)

   408

   409 lemma card_of_singl_ordLeq:

   410 assumes "A \<noteq> {}"

   411 shows "|{b}| \<le>o |A|"

   412 proof-

   413   obtain a where *: "a \<in> A" using assms by auto

   414   let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"

   415   have "inj_on ?h {b} \<and> ?h  {b} \<le> A"

   416   using * unfolding inj_on_def by auto

   417   thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)

   418 qed

   419

   420 corollary Card_order_singl_ordLeq:

   421 "\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r"

   422 using card_of_singl_ordLeq[of "Field r" b]

   423       card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast

   424

   425 lemma card_of_Pow: "|A| <o |Pow A|"

   426 using card_of_ordLess2[of "Pow A" A]  Cantors_paradox[of A]

   427       Pow_not_empty[of A] by auto

   428

   429 corollary Card_order_Pow:

   430 "Card_order r \<Longrightarrow> r <o |Pow(Field r)|"

   431 using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast

   432

   433 lemma card_of_Plus1: "|A| \<le>o |A <+> B|"

   434 proof-

   435   have "Inl  A \<le> A <+> B" by auto

   436   thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast

   437 qed

   438

   439 corollary Card_order_Plus1:

   440 "Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|"

   441 using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast

   442

   443 lemma card_of_Plus2: "|B| \<le>o |A <+> B|"

   444 proof-

   445   have "Inr  B \<le> A <+> B" by auto

   446   thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast

   447 qed

   448

   449 corollary Card_order_Plus2:

   450 "Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|"

   451 using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast

   452

   453 lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"

   454 proof-

   455   have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto

   456   thus ?thesis using card_of_ordIso by auto

   457 qed

   458

   459 lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"

   460 proof-

   461   have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto

   462   thus ?thesis using card_of_ordIso by auto

   463 qed

   464

   465 lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"

   466 proof-

   467   let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a

   468                                    | Inr b \<Rightarrow> Inl b"

   469   have "bij_betw ?f (A <+> B) (B <+> A)"

   470   unfolding bij_betw_def inj_on_def by force

   471   thus ?thesis using card_of_ordIso by blast

   472 qed

   473

   474 lemma card_of_Plus_assoc:

   475 fixes A :: "'a set" and B :: "'b set" and C :: "'c set"

   476 shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"

   477 proof -

   478   def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).

   479   case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a

   480                                  |Inr b \<Rightarrow> Inr (Inl b))

   481            |Inr c \<Rightarrow> Inr (Inr c)"

   482   have "A <+> B <+> C \<subseteq> f  ((A <+> B) <+> C)"

   483   proof

   484     fix x assume x: "x \<in> A <+> B <+> C"

   485     show "x \<in> f  ((A <+> B) <+> C)"

   486     proof(cases x)

   487       case (Inl a)

   488       hence "a \<in> A" "x = f (Inl (Inl a))"

   489       using x unfolding f_def by auto

   490       thus ?thesis by auto

   491     next

   492       case (Inr bc) note 1 = Inr show ?thesis

   493       proof(cases bc)

   494         case (Inl b)

   495         hence "b \<in> B" "x = f (Inl (Inr b))"

   496         using x 1 unfolding f_def by auto

   497         thus ?thesis by auto

   498       next

   499         case (Inr c)

   500         hence "c \<in> C" "x = f (Inr c)"

   501         using x 1 unfolding f_def by auto

   502         thus ?thesis by auto

   503       qed

   504     qed

   505   qed

   506   hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"

   507   unfolding bij_betw_def inj_on_def f_def by fastforce

   508   thus ?thesis using card_of_ordIso by blast

   509 qed

   510

   511 lemma card_of_Plus_mono1:

   512 assumes "|A| \<le>o |B|"

   513 shows "|A <+> C| \<le>o |B <+> C|"

   514 proof-

   515   obtain f where 1: "inj_on f A \<and> f  A \<le> B"

   516   using assms card_of_ordLeq[of A] by fastforce

   517   obtain g where g_def:

   518   "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast

   519   have "inj_on g (A <+> C) \<and> g  (A <+> C) \<le> (B <+> C)"

   520   proof-

   521     {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and

   522                           "g d1 = g d2"

   523      hence "d1 = d2" using 1 unfolding inj_on_def g_def by force

   524     }

   525     moreover

   526     {fix d assume "d \<in> A <+> C"

   527      hence "g d \<in> B <+> C"  using 1

   528      by(case_tac d, auto simp add: g_def)

   529     }

   530     ultimately show ?thesis unfolding inj_on_def by auto

   531   qed

   532   thus ?thesis using card_of_ordLeq by metis

   533 qed

   534

   535 corollary ordLeq_Plus_mono1:

   536 assumes "r \<le>o r'"

   537 shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|"

   538 using assms card_of_mono2 card_of_Plus_mono1 by blast

   539

   540 lemma card_of_Plus_mono2:

   541 assumes "|A| \<le>o |B|"

   542 shows "|C <+> A| \<le>o |C <+> B|"

   543 using assms card_of_Plus_mono1[of A B C]

   544       card_of_Plus_commute[of C A]  card_of_Plus_commute[of B C]

   545       ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]

   546 by blast

   547

   548 corollary ordLeq_Plus_mono2:

   549 assumes "r \<le>o r'"

   550 shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|"

   551 using assms card_of_mono2 card_of_Plus_mono2 by blast

   552

   553 lemma card_of_Plus_mono:

   554 assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"

   555 shows "|A <+> C| \<le>o |B <+> D|"

   556 using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]

   557       ordLeq_transitive[of "|A <+> C|"] by blast

   558

   559 corollary ordLeq_Plus_mono:

   560 assumes "r \<le>o r'" and "p \<le>o p'"

   561 shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|"

   562 using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast

   563

   564 lemma card_of_Plus_cong1:

   565 assumes "|A| =o |B|"

   566 shows "|A <+> C| =o |B <+> C|"

   567 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)

   568

   569 corollary ordIso_Plus_cong1:

   570 assumes "r =o r'"

   571 shows "|(Field r) <+> C| =o |(Field r') <+> C|"

   572 using assms card_of_cong card_of_Plus_cong1 by blast

   573

   574 lemma card_of_Plus_cong2:

   575 assumes "|A| =o |B|"

   576 shows "|C <+> A| =o |C <+> B|"

   577 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)

   578

   579 corollary ordIso_Plus_cong2:

   580 assumes "r =o r'"

   581 shows "|A <+> (Field r)| =o |A <+> (Field r')|"

   582 using assms card_of_cong card_of_Plus_cong2 by blast

   583

   584 lemma card_of_Plus_cong:

   585 assumes "|A| =o |B|" and "|C| =o |D|"

   586 shows "|A <+> C| =o |B <+> D|"

   587 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)

   588

   589 corollary ordIso_Plus_cong:

   590 assumes "r =o r'" and "p =o p'"

   591 shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"

   592 using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast

   593

   594 lemma card_of_Un_Plus_ordLeq:

   595 "|A \<union> B| \<le>o |A <+> B|"

   596 proof-

   597    let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"

   598    have "inj_on ?f (A \<union> B) \<and> ?f  (A \<union> B) \<le> A <+> B"

   599    unfolding inj_on_def by auto

   600    thus ?thesis using card_of_ordLeq by blast

   601 qed

   602

   603 lemma card_of_Times1:

   604 assumes "A \<noteq> {}"

   605 shows "|B| \<le>o |B \<times> A|"

   606 proof(cases "B = {}", simp add: card_of_empty)

   607   assume *: "B \<noteq> {}"

   608   have "fst (B \<times> A) = B" unfolding image_def using assms by auto

   609   thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]

   610                      card_of_ordLeq[of B "B \<times> A"] * by blast

   611 qed

   612

   613 lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|"

   614 proof-

   615   let ?f = "\<lambda>(a::'a,b::'b). (b,a)"

   616   have "bij_betw ?f (A \<times> B) (B \<times> A)"

   617   unfolding bij_betw_def inj_on_def by auto

   618   thus ?thesis using card_of_ordIso by blast

   619 qed

   620

   621 lemma card_of_Times2:

   622 assumes "A \<noteq> {}"   shows "|B| \<le>o |A \<times> B|"

   623 using assms card_of_Times1[of A B] card_of_Times_commute[of B A]

   624       ordLeq_ordIso_trans by blast

   625

   626 corollary Card_order_Times1:

   627 "\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|"

   628 using card_of_Times1[of B] card_of_Field_ordIso

   629       ordIso_ordLeq_trans ordIso_symmetric by blast

   630

   631 corollary Card_order_Times2:

   632 "\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|"

   633 using card_of_Times2[of A] card_of_Field_ordIso

   634       ordIso_ordLeq_trans ordIso_symmetric by blast

   635

   636 lemma card_of_Times3: "|A| \<le>o |A \<times> A|"

   637 using card_of_Times1[of A]

   638 by(cases "A = {}", simp add: card_of_empty, blast)

   639

   640 lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|"

   641 proof-

   642   let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True)

   643                                   |Inr a \<Rightarrow> (a,False)"

   644   have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))"

   645   proof-

   646     {fix  c1 and c2 assume "?f c1 = ?f c2"

   647      hence "c1 = c2"

   648      by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)

   649     }

   650     moreover

   651     {fix c assume "c \<in> A <+> A"

   652      hence "?f c \<in> A \<times> (UNIV::bool set)"

   653      by(case_tac c, auto)

   654     }

   655     moreover

   656     {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"

   657      have "(a,bl) \<in> ?f  ( A <+> A)"

   658      proof(cases bl)

   659        assume bl hence "?f(Inl a) = (a,bl)" by auto

   660        thus ?thesis using * by force

   661      next

   662        assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto

   663        thus ?thesis using * by force

   664      qed

   665     }

   666     ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto

   667   qed

   668   thus ?thesis using card_of_ordIso by blast

   669 qed

   670

   671 lemma card_of_Times_mono1:

   672 assumes "|A| \<le>o |B|"

   673 shows "|A \<times> C| \<le>o |B \<times> C|"

   674 proof-

   675   obtain f where 1: "inj_on f A \<and> f  A \<le> B"

   676   using assms card_of_ordLeq[of A] by fastforce

   677   obtain g where g_def:

   678   "g = (\<lambda>(a,c::'c). (f a,c))" by blast

   679   have "inj_on g (A \<times> C) \<and> g  (A \<times> C) \<le> (B \<times> C)"

   680   using 1 unfolding inj_on_def using g_def by auto

   681   thus ?thesis using card_of_ordLeq by metis

   682 qed

   683

   684 corollary ordLeq_Times_mono1:

   685 assumes "r \<le>o r'"

   686 shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|"

   687 using assms card_of_mono2 card_of_Times_mono1 by blast

   688

   689 lemma card_of_Times_mono2:

   690 assumes "|A| \<le>o |B|"

   691 shows "|C \<times> A| \<le>o |C \<times> B|"

   692 using assms card_of_Times_mono1[of A B C]

   693       card_of_Times_commute[of C A]  card_of_Times_commute[of B C]

   694       ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"]

   695 by blast

   696

   697 corollary ordLeq_Times_mono2:

   698 assumes "r \<le>o r'"

   699 shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|"

   700 using assms card_of_mono2 card_of_Times_mono2 by blast

   701

   702 lemma card_of_Sigma_mono1:

   703 assumes "\<forall>i \<in> I. |A i| \<le>o |B i|"

   704 shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|"

   705 proof-

   706   have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f  (A i) \<le> B i)"

   707   using assms by (auto simp add: card_of_ordLeq)

   708   with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f  (A i) \<le> B i"]

   709   obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i)  (A i) \<le> B i" by metis

   710   obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast

   711   have "inj_on g (Sigma I A) \<and> g  (Sigma I A) \<le> (Sigma I B)"

   712   using 1 unfolding inj_on_def using g_def by force

   713   thus ?thesis using card_of_ordLeq by metis

   714 qed

   715

   716 corollary card_of_Sigma_Times:

   717 "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"

   718 using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .

   719

   720 lemma card_of_UNION_Sigma:

   721 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"

   722 using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis

   723

   724 lemma card_of_bool:

   725 assumes "a1 \<noteq> a2"

   726 shows "|UNIV::bool set| =o |{a1,a2}|"

   727 proof-

   728   let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"

   729   have "bij_betw ?f UNIV {a1,a2}"

   730   proof-

   731     {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"

   732      hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)

   733     }

   734     moreover

   735     {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)

   736     }

   737     moreover

   738     {fix a assume *: "a \<in> {a1,a2}"

   739      have "a \<in> ?f  UNIV"

   740      proof(cases "a = a1")

   741        assume "a = a1"

   742        hence "?f True = a" by auto  thus ?thesis by blast

   743      next

   744        assume "a \<noteq> a1" hence "a = a2" using * by auto

   745        hence "?f False = a" by auto  thus ?thesis by blast

   746      qed

   747     }

   748     ultimately show ?thesis unfolding bij_betw_def inj_on_def

   749     by (metis (no_types) image_subsetI order_eq_iff subsetI)

   750   qed

   751   thus ?thesis using card_of_ordIso by blast

   752 qed

   753

   754 lemma card_of_Plus_Times_aux:

   755 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and

   756         LEQ: "|A| \<le>o |B|"

   757 shows "|A <+> B| \<le>o |A \<times> B|"

   758 proof-

   759   have 1: "|UNIV::bool set| \<le>o |A|"

   760   using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]

   761         ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis

   762   (*  *)

   763   have "|A <+> B| \<le>o |B <+> B|"

   764   using LEQ card_of_Plus_mono1 by blast

   765   moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"

   766   using card_of_Plus_Times_bool by blast

   767   moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"

   768   using 1 by (simp add: card_of_Times_mono2)

   769   moreover have " |B \<times> A| =o |A \<times> B|"

   770   using card_of_Times_commute by blast

   771   ultimately show "|A <+> B| \<le>o |A \<times> B|"

   772   using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]

   773         ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]

   774         ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]

   775   by blast

   776 qed

   777

   778 lemma card_of_Plus_Times:

   779 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and

   780         B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"

   781 shows "|A <+> B| \<le>o |A \<times> B|"

   782 proof-

   783   {assume "|A| \<le>o |B|"

   784    hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)

   785   }

   786   moreover

   787   {assume "|B| \<le>o |A|"

   788    hence "|B <+> A| \<le>o |B \<times> A|"

   789    using assms by (auto simp add: card_of_Plus_Times_aux)

   790    hence ?thesis

   791    using card_of_Plus_commute card_of_Times_commute

   792          ordIso_ordLeq_trans ordLeq_ordIso_trans by metis

   793   }

   794   ultimately show ?thesis

   795   using card_of_Well_order[of A] card_of_Well_order[of B]

   796         ordLeq_total[of "|A|"] by metis

   797 qed

   798

   799 lemma card_of_ordLeq_finite:

   800 assumes "|A| \<le>o |B|" and "finite B"

   801 shows "finite A"

   802 using assms unfolding ordLeq_def

   803 using embed_inj_on[of "|A|" "|B|"]  embed_Field[of "|A|" "|B|"]

   804       Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce

   805

   806 lemma card_of_ordLeq_infinite:

   807 assumes "|A| \<le>o |B|" and "\<not> finite A"

   808 shows "\<not> finite B"

   809 using assms card_of_ordLeq_finite by auto

   810

   811 lemma card_of_ordIso_finite:

   812 assumes "|A| =o |B|"

   813 shows "finite A = finite B"

   814 using assms unfolding ordIso_def iso_def[abs_def]

   815 by (auto simp: bij_betw_finite Field_card_of)

   816

   817 lemma card_of_ordIso_finite_Field:

   818 assumes "Card_order r" and "r =o |A|"

   819 shows "finite(Field r) = finite A"

   820 using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast

   821

   822

   823 subsection {* Cardinals versus set operations involving infinite sets *}

   824

   825 text{* Here we show that, for infinite sets, most set-theoretic constructions

   826 do not increase the cardinality.  The cornerstone for this is

   827 theorem @{text "Card_order_Times_same_infinite"}, which states that self-product

   828 does not increase cardinality -- the proof of this fact adapts a standard

   829 set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11

   830 at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}

   831

   832 lemma infinite_iff_card_of_nat:

   833 "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"

   834 unfolding infinite_iff_countable_subset card_of_ordLeq ..

   835

   836 text{* The next two results correspond to the ZF fact that all infinite cardinals are

   837 limit ordinals: *}

   838

   839 lemma Card_order_infinite_not_under:

   840 assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"

   841 shows "\<not> (\<exists>a. Field r = under r a)"

   842 proof(auto)

   843   have 0: "Well_order r \<and> wo_rel r \<and> Refl r"

   844   using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto

   845   fix a assume *: "Field r = under r a"

   846   show False

   847   proof(cases "a \<in> Field r")

   848     assume Case1: "a \<notin> Field r"

   849     hence "under r a = {}" unfolding Field_def under_def by auto

   850     thus False using INF *  by auto

   851   next

   852     let ?r' = "Restr r (underS r a)"

   853     assume Case2: "a \<in> Field r"

   854     hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"

   855     using 0 Refl_under_underS underS_notIn by metis

   856     have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"

   857     using 0 wo_rel.underS_ofilter * 1 Case2 by fast

   858     hence "?r' <o r" using 0 using ofilter_ordLess by blast

   859     moreover

   860     have "Field ?r' = underS r a \<and> Well_order ?r'"

   861     using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast

   862     ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto

   863     moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto

   864     ultimately have "|underS r a| <o |under r a|"

   865     using ordIso_symmetric ordLess_ordIso_trans by blast

   866     moreover

   867     {have "\<exists>f. bij_betw f (under r a) (underS r a)"

   868      using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto

   869      hence "|under r a| =o |underS r a|" using card_of_ordIso by blast

   870     }

   871     ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast

   872   qed

   873 qed

   874

   875 lemma infinite_Card_order_limit:

   876 assumes r: "Card_order r" and "\<not>finite (Field r)"

   877 and a: "a : Field r"

   878 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"

   879 proof-

   880   have "Field r \<noteq> under r a"

   881   using assms Card_order_infinite_not_under by blast

   882   moreover have "under r a \<le> Field r"

   883   using under_Field .

   884   ultimately have "under r a < Field r" by blast

   885   then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"

   886   unfolding under_def by blast

   887   moreover have ba: "b \<noteq> a"

   888   using 1 r unfolding card_order_on_def well_order_on_def

   889   linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto

   890   ultimately have "(a,b) : r"

   891   using a r unfolding card_order_on_def well_order_on_def linear_order_on_def

   892   total_on_def by blast

   893   thus ?thesis using 1 ba by auto

   894 qed

   895

   896 theorem Card_order_Times_same_infinite:

   897 assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"

   898 shows "|Field r \<times> Field r| \<le>o r"

   899 proof-

   900   obtain phi where phi_def:

   901   "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>

   902                       \<not> |Field r \<times> Field r| \<le>o r )" by blast

   903   have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"

   904   unfolding phi_def card_order_on_def by auto

   905   have Ft: "\<not>(\<exists>r. phi r)"

   906   proof

   907     assume "\<exists>r. phi r"

   908     hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"

   909     using temp1 by auto

   910     then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and

   911                    3: "Card_order r \<and> Well_order r"

   912     using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast

   913     let ?A = "Field r"  let ?r' = "bsqr r"

   914     have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"

   915     using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast

   916     have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"

   917     using card_of_Card_order card_of_Well_order by blast

   918     (*  *)

   919     have "r <o |?A \<times> ?A|"

   920     using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast

   921     moreover have "|?A \<times> ?A| \<le>o ?r'"

   922     using card_of_least[of "?A \<times> ?A"] 4 by auto

   923     ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto

   924     then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"

   925     unfolding ordLess_def embedS_def[abs_def]

   926     by (auto simp add: Field_bsqr)

   927     let ?B = "f  ?A"

   928     have "|?A| =o |?B|"

   929     using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast

   930     hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast

   931     (*  *)

   932     have "wo_rel.ofilter ?r' ?B"

   933     using 6 embed_Field_ofilter 3 4 by blast

   934     hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"

   935     using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto

   936     hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"

   937     using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast

   938     have "\<not> (\<exists>a. Field r = under r a)"

   939     using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto

   940     then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"

   941     using temp2 3 bsqr_ofilter[of r ?B] by blast

   942     hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast

   943     hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast

   944     let ?r1 = "Restr r A1"

   945     have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast

   946     moreover

   947     {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast

   948      hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast

   949     }

   950     ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast

   951     (*  *)

   952     have "\<not> finite (Field r)" using 1 unfolding phi_def by simp

   953     hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast

   954     hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis

   955     moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"

   956     using card_of_Card_order[of A1] card_of_Well_order[of A1]

   957     by (simp add: Field_card_of)

   958     moreover have "\<not> r \<le>o | A1 |"

   959     using temp4 11 3 using not_ordLeq_iff_ordLess by blast

   960     ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"

   961     by (simp add: card_of_card_order_on)

   962     hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"

   963     using 2 unfolding phi_def by blast

   964     hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto

   965     hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast

   966     thus False using 11 not_ordLess_ordLeq by auto

   967   qed

   968   thus ?thesis using assms unfolding phi_def by blast

   969 qed

   970

   971 corollary card_of_Times_same_infinite:

   972 assumes "\<not>finite A"

   973 shows "|A \<times> A| =o |A|"

   974 proof-

   975   let ?r = "|A|"

   976   have "Field ?r = A \<and> Card_order ?r"

   977   using Field_card_of card_of_Card_order[of A] by fastforce

   978   hence "|A \<times> A| \<le>o |A|"

   979   using Card_order_Times_same_infinite[of ?r] assms by auto

   980   thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast

   981 qed

   982

   983 lemma card_of_Times_infinite:

   984 assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"

   985 shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"

   986 proof-

   987   have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"

   988   using assms by (simp add: card_of_Times1 card_of_Times2)

   989   moreover

   990   {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"

   991    using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast

   992    moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast

   993    ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"

   994    using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto

   995   }

   996   ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)

   997 qed

   998

   999 corollary Card_order_Times_infinite:

  1000 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and

  1001         NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"

  1002 shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"

  1003 proof-

  1004   have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"

  1005   using assms by (simp add: card_of_Times_infinite card_of_mono2)

  1006   thus ?thesis

  1007   using assms card_of_Field_ordIso[of r]

  1008         ordIso_transitive[of "|Field r \<times> Field p|"]

  1009         ordIso_transitive[of _ "|Field r|"] by blast

  1010 qed

  1011

  1012 lemma card_of_Sigma_ordLeq_infinite:

  1013 assumes INF: "\<not>finite B" and

  1014         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"

  1015 shows "|SIGMA i : I. A i| \<le>o |B|"

  1016 proof(cases "I = {}", simp add: card_of_empty)

  1017   assume *: "I \<noteq> {}"

  1018   have "|SIGMA i : I. A i| \<le>o |I \<times> B|"

  1019   using LEQ card_of_Sigma_Times by blast

  1020   moreover have "|I \<times> B| =o |B|"

  1021   using INF * LEQ_I by (auto simp add: card_of_Times_infinite)

  1022   ultimately show ?thesis using ordLeq_ordIso_trans by blast

  1023 qed

  1024

  1025 lemma card_of_Sigma_ordLeq_infinite_Field:

  1026 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and

  1027         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"

  1028 shows "|SIGMA i : I. A i| \<le>o r"

  1029 proof-

  1030   let ?B  = "Field r"

  1031   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso

  1032   ordIso_symmetric by blast

  1033   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"

  1034   using LEQ_I LEQ ordLeq_ordIso_trans by blast+

  1035   hence  "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ

  1036   card_of_Sigma_ordLeq_infinite by blast

  1037   thus ?thesis using 1 ordLeq_ordIso_trans by blast

  1038 qed

  1039

  1040 lemma card_of_Times_ordLeq_infinite_Field:

  1041 "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>

  1042  \<Longrightarrow> |A <*> B| \<le>o r"

  1043 by(simp add: card_of_Sigma_ordLeq_infinite_Field)

  1044

  1045 lemma card_of_Times_infinite_simps:

  1046 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"

  1047 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"

  1048 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"

  1049 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"

  1050 by (auto simp add: card_of_Times_infinite ordIso_symmetric)

  1051

  1052 lemma card_of_UNION_ordLeq_infinite:

  1053 assumes INF: "\<not>finite B" and

  1054         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"

  1055 shows "|\<Union> i \<in> I. A i| \<le>o |B|"

  1056 proof(cases "I = {}", simp add: card_of_empty)

  1057   assume *: "I \<noteq> {}"

  1058   have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"

  1059   using card_of_UNION_Sigma by blast

  1060   moreover have "|SIGMA i : I. A i| \<le>o |B|"

  1061   using assms card_of_Sigma_ordLeq_infinite by blast

  1062   ultimately show ?thesis using ordLeq_transitive by blast

  1063 qed

  1064

  1065 corollary card_of_UNION_ordLeq_infinite_Field:

  1066 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and

  1067         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"

  1068 shows "|\<Union> i \<in> I. A i| \<le>o r"

  1069 proof-

  1070   let ?B  = "Field r"

  1071   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso

  1072   ordIso_symmetric by blast

  1073   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"

  1074   using LEQ_I LEQ ordLeq_ordIso_trans by blast+

  1075   hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ

  1076   card_of_UNION_ordLeq_infinite by blast

  1077   thus ?thesis using 1 ordLeq_ordIso_trans by blast

  1078 qed

  1079

  1080 lemma card_of_Plus_infinite1:

  1081 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"

  1082 shows "|A <+> B| =o |A|"

  1083 proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)

  1084   let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"

  1085   assume *: "B \<noteq> {}"

  1086   then obtain b1 where 1: "b1 \<in> B" by blast

  1087   show ?thesis

  1088   proof(cases "B = {b1}")

  1089     assume Case1: "B = {b1}"

  1090     have 2: "bij_betw ?Inl A ((?Inl  A))"

  1091     unfolding bij_betw_def inj_on_def by auto

  1092     hence 3: "\<not>finite (?Inl  A)"

  1093     using INF bij_betw_finite[of ?Inl A] by blast

  1094     let ?A' = "?Inl  A \<union> {?Inr b1}"

  1095     obtain g where "bij_betw g (?Inl  A) ?A'"

  1096     using 3 infinite_imp_bij_betw2[of "?Inl  A"] by auto

  1097     moreover have "?A' = A <+> B" using Case1 by blast

  1098     ultimately have "bij_betw g (?Inl  A) (A <+> B)" by simp

  1099     hence "bij_betw (g o ?Inl) A (A <+> B)"

  1100     using 2 by (auto simp add: bij_betw_trans)

  1101     thus ?thesis using card_of_ordIso ordIso_symmetric by blast

  1102   next

  1103     assume Case2: "B \<noteq> {b1}"

  1104     with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce

  1105     obtain f where "inj_on f B \<and> f  B \<le> A"

  1106     using LEQ card_of_ordLeq[of B] by fastforce

  1107     with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"

  1108     unfolding inj_on_def by auto

  1109     with 3 have "|A <+> B| \<le>o |A \<times> B|"

  1110     by (auto simp add: card_of_Plus_Times)

  1111     moreover have "|A \<times> B| =o |A|"

  1112     using assms * by (simp add: card_of_Times_infinite_simps)

  1113     ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis

  1114     thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast

  1115   qed

  1116 qed

  1117

  1118 lemma card_of_Plus_infinite2:

  1119 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"

  1120 shows "|B <+> A| =o |A|"

  1121 using assms card_of_Plus_commute card_of_Plus_infinite1

  1122 ordIso_equivalence by blast

  1123

  1124 lemma card_of_Plus_infinite:

  1125 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"

  1126 shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"

  1127 using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)

  1128

  1129 corollary Card_order_Plus_infinite:

  1130 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and

  1131         LEQ: "p \<le>o r"

  1132 shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"

  1133 proof-

  1134   have "| Field r <+> Field p | =o | Field r | \<and>

  1135         | Field p <+> Field r | =o | Field r |"

  1136   using assms by (simp add: card_of_Plus_infinite card_of_mono2)

  1137   thus ?thesis

  1138   using assms card_of_Field_ordIso[of r]

  1139         ordIso_transitive[of "|Field r <+> Field p|"]

  1140         ordIso_transitive[of _ "|Field r|"] by blast

  1141 qed

  1142

  1143

  1144 subsection {* The cardinal $\omega$ and the finite cardinals *}

  1145

  1146 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict

  1147 order relation on

  1148 @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals

  1149 shall be the restrictions of these relations to the numbers smaller than

  1150 fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}

  1151

  1152 abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"

  1153 abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"

  1154

  1155 abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"

  1156 where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"

  1157

  1158 lemma infinite_cartesian_product:

  1159 assumes "\<not>finite A" "\<not>finite B"

  1160 shows "\<not>finite (A \<times> B)"

  1161 proof

  1162   assume "finite (A \<times> B)"

  1163   from assms(1) have "A \<noteq> {}" by auto

  1164   with finite (A \<times> B) have "finite B" using finite_cartesian_productD2 by auto

  1165   with assms(2) show False by simp

  1166 qed

  1167

  1168

  1169 subsubsection {* First as well-orders *}

  1170

  1171 lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"

  1172 by(unfold Field_def, auto)

  1173

  1174 lemma natLeq_Refl: "Refl natLeq"

  1175 unfolding refl_on_def Field_def by auto

  1176

  1177 lemma natLeq_trans: "trans natLeq"

  1178 unfolding trans_def by auto

  1179

  1180 lemma natLeq_Preorder: "Preorder natLeq"

  1181 unfolding preorder_on_def

  1182 by (auto simp add: natLeq_Refl natLeq_trans)

  1183

  1184 lemma natLeq_antisym: "antisym natLeq"

  1185 unfolding antisym_def by auto

  1186

  1187 lemma natLeq_Partial_order: "Partial_order natLeq"

  1188 unfolding partial_order_on_def

  1189 by (auto simp add: natLeq_Preorder natLeq_antisym)

  1190

  1191 lemma natLeq_Total: "Total natLeq"

  1192 unfolding total_on_def by auto

  1193

  1194 lemma natLeq_Linear_order: "Linear_order natLeq"

  1195 unfolding linear_order_on_def

  1196 by (auto simp add: natLeq_Partial_order natLeq_Total)

  1197

  1198 lemma natLeq_natLess_Id: "natLess = natLeq - Id"

  1199 by auto

  1200

  1201 lemma natLeq_Well_order: "Well_order natLeq"

  1202 unfolding well_order_on_def

  1203 using natLeq_Linear_order wf_less natLeq_natLess_Id by auto

  1204

  1205 lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"

  1206 unfolding Field_def by auto

  1207

  1208 lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"

  1209 unfolding underS_def by auto

  1210

  1211 lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"

  1212 by force

  1213

  1214 lemma Restr_natLeq2:

  1215 "Restr natLeq (underS natLeq n) = natLeq_on n"

  1216 by (auto simp add: Restr_natLeq natLeq_underS_less)

  1217

  1218 lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"

  1219 using Restr_natLeq[of n] natLeq_Well_order

  1220       Well_order_Restr[of natLeq "{x. x < n}"] by auto

  1221

  1222 corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"

  1223 using natLeq_on_Well_order Field_natLeq_on by auto

  1224

  1225 lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"

  1226 unfolding wo_rel_def using natLeq_on_Well_order .

  1227

  1228

  1229 subsubsection {* Then as cardinals *}

  1230

  1231 lemma natLeq_Card_order: "Card_order natLeq"

  1232 proof(auto simp add: natLeq_Well_order

  1233       Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)

  1234   fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)

  1235   moreover have "\<not>finite(UNIV::nat set)" by auto

  1236   ultimately show "natLeq_on n <o |UNIV::nat set|"

  1237   using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]

  1238         Field_card_of[of "UNIV::nat set"]

  1239         card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto

  1240 qed

  1241

  1242 corollary card_of_Field_natLeq:

  1243 "|Field natLeq| =o natLeq"

  1244 using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]

  1245       ordIso_symmetric[of natLeq] by blast

  1246

  1247 corollary card_of_nat:

  1248 "|UNIV::nat set| =o natLeq"

  1249 using Field_natLeq card_of_Field_natLeq by auto

  1250

  1251 corollary infinite_iff_natLeq_ordLeq:

  1252 "\<not>finite A = ( natLeq \<le>o |A| )"

  1253 using infinite_iff_card_of_nat[of A] card_of_nat

  1254       ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast

  1255

  1256 corollary finite_iff_ordLess_natLeq:

  1257 "finite A = ( |A| <o natLeq)"

  1258 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess

  1259       card_of_Well_order natLeq_Well_order by metis

  1260

  1261

  1262 subsection {* The successor of a cardinal *}

  1263

  1264 text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}

  1265 being a successor cardinal of @{text "r"}. Although the definition does

  1266 not require @{text "r"} to be a cardinal, only this case will be meaningful. *}

  1267

  1268 definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"

  1269 where

  1270 "isCardSuc r r' \<equiv>

  1271  Card_order r' \<and> r <o r' \<and>

  1272  (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"

  1273

  1274 text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},

  1275 by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.

  1276 Again, the picked item shall be proved unique up to order-isomorphism. *}

  1277

  1278 definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"

  1279 where

  1280 "cardSuc r \<equiv> SOME r'. isCardSuc r r'"

  1281

  1282 lemma exists_minim_Card_order:

  1283 "\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"

  1284 unfolding card_order_on_def using exists_minim_Well_order by blast

  1285

  1286 lemma exists_isCardSuc:

  1287 assumes "Card_order r"

  1288 shows "\<exists>r'. isCardSuc r r'"

  1289 proof-

  1290   let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"

  1291   have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms

  1292   by (simp add: card_of_Card_order Card_order_Pow)

  1293   then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"

  1294   using exists_minim_Card_order[of ?R] by blast

  1295   thus ?thesis unfolding isCardSuc_def by auto

  1296 qed

  1297

  1298 lemma cardSuc_isCardSuc:

  1299 assumes "Card_order r"

  1300 shows "isCardSuc r (cardSuc r)"

  1301 unfolding cardSuc_def using assms

  1302 by (simp add: exists_isCardSuc someI_ex)

  1303

  1304 lemma cardSuc_Card_order:

  1305 "Card_order r \<Longrightarrow> Card_order(cardSuc r)"

  1306 using cardSuc_isCardSuc unfolding isCardSuc_def by blast

  1307

  1308 lemma cardSuc_greater:

  1309 "Card_order r \<Longrightarrow> r <o cardSuc r"

  1310 using cardSuc_isCardSuc unfolding isCardSuc_def by blast

  1311

  1312 lemma cardSuc_ordLeq:

  1313 "Card_order r \<Longrightarrow> r \<le>o cardSuc r"

  1314 using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast

  1315

  1316 text{* The minimality property of @{text "cardSuc"} originally present in its definition

  1317 is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}

  1318

  1319 lemma cardSuc_least_aux:

  1320 "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"

  1321 using cardSuc_isCardSuc unfolding isCardSuc_def by blast

  1322

  1323 text{* But from this we can infer general minimality: *}

  1324

  1325 lemma cardSuc_least:

  1326 assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"

  1327 shows "cardSuc r \<le>o r'"

  1328 proof-

  1329   let ?p = "cardSuc r"

  1330   have 0: "Well_order ?p \<and> Well_order r'"

  1331   using assms cardSuc_Card_order unfolding card_order_on_def by blast

  1332   {assume "r' <o ?p"

  1333    then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"

  1334    using internalize_ordLess[of r' ?p] by blast

  1335    (*  *)

  1336    have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast

  1337    moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast

  1338    ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast

  1339    hence False using 2 not_ordLess_ordLeq by blast

  1340   }

  1341   thus ?thesis using 0 ordLess_or_ordLeq by blast

  1342 qed

  1343

  1344 lemma cardSuc_ordLess_ordLeq:

  1345 assumes CARD: "Card_order r" and CARD': "Card_order r'"

  1346 shows "(r <o r') = (cardSuc r \<le>o r')"

  1347 proof(auto simp add: assms cardSuc_least)

  1348   assume "cardSuc r \<le>o r'"

  1349   thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast

  1350 qed

  1351

  1352 lemma cardSuc_ordLeq_ordLess:

  1353 assumes CARD: "Card_order r" and CARD': "Card_order r'"

  1354 shows "(r' <o cardSuc r) = (r' \<le>o r)"

  1355 proof-

  1356   have "Well_order r \<and> Well_order r'"

  1357   using assms unfolding card_order_on_def by auto

  1358   moreover have "Well_order(cardSuc r)"

  1359   using assms cardSuc_Card_order card_order_on_def by blast

  1360   ultimately show ?thesis

  1361   using assms cardSuc_ordLess_ordLeq[of r r']

  1362   not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast

  1363 qed

  1364

  1365 lemma cardSuc_mono_ordLeq:

  1366 assumes CARD: "Card_order r" and CARD': "Card_order r'"

  1367 shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"

  1368 using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast

  1369

  1370 lemma cardSuc_invar_ordIso:

  1371 assumes CARD: "Card_order r" and CARD': "Card_order r'"

  1372 shows "(cardSuc r =o cardSuc r') = (r =o r')"

  1373 proof-

  1374   have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"

  1375   using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)

  1376   thus ?thesis

  1377   using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq

  1378   using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast

  1379 qed

  1380

  1381 lemma card_of_cardSuc_finite:

  1382 "finite(Field(cardSuc |A| )) = finite A"

  1383 proof

  1384   assume *: "finite (Field (cardSuc |A| ))"

  1385   have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"

  1386   using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast

  1387   hence "|A| \<le>o |Field(cardSuc |A| )|"

  1388   using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric

  1389   ordLeq_ordIso_trans by blast

  1390   thus "finite A" using * card_of_ordLeq_finite by blast

  1391 next

  1392   assume "finite A"

  1393   then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp

  1394   then show "finite (Field (cardSuc |A| ))"

  1395   proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])

  1396     show "cardSuc |A| \<le>o |Pow A|"

  1397       by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)

  1398   qed

  1399 qed

  1400

  1401 lemma cardSuc_finite:

  1402 assumes "Card_order r"

  1403 shows "finite (Field (cardSuc r)) = finite (Field r)"

  1404 proof-

  1405   let ?A = "Field r"

  1406   have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)

  1407   hence "cardSuc |?A| =o cardSuc r" using assms

  1408   by (simp add: card_of_Card_order cardSuc_invar_ordIso)

  1409   moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"

  1410   by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)

  1411   moreover

  1412   {have "|Field (cardSuc r) | =o cardSuc r"

  1413    using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)

  1414    hence "cardSuc r =o |Field (cardSuc r) |"

  1415    using ordIso_symmetric by blast

  1416   }

  1417   ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"

  1418   using ordIso_transitive by blast

  1419   hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"

  1420   using card_of_ordIso_finite by blast

  1421   thus ?thesis by (simp only: card_of_cardSuc_finite)

  1422 qed

  1423

  1424 lemma card_of_Plus_ordLess_infinite:

  1425 assumes INF: "\<not>finite C" and

  1426         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"

  1427 shows "|A <+> B| <o |C|"

  1428 proof(cases "A = {} \<or> B = {}")

  1429   assume Case1: "A = {} \<or> B = {}"

  1430   hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"

  1431   using card_of_Plus_empty1 card_of_Plus_empty2 by blast

  1432   hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"

  1433   using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast

  1434   thus ?thesis using LESS1 LESS2

  1435        ordIso_ordLess_trans[of "|A <+> B|" "|A|"]

  1436        ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast

  1437 next

  1438   assume Case2: "\<not>(A = {} \<or> B = {})"

  1439   {assume *: "|C| \<le>o |A <+> B|"

  1440    hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast

  1441    hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast

  1442    {assume Case21: "|A| \<le>o |B|"

  1443     hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast

  1444     hence "|A <+> B| =o |B|" using Case2 Case21

  1445     by (auto simp add: card_of_Plus_infinite)

  1446     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast

  1447    }

  1448    moreover

  1449    {assume Case22: "|B| \<le>o |A|"

  1450     hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast

  1451     hence "|A <+> B| =o |A|" using Case2 Case22

  1452     by (auto simp add: card_of_Plus_infinite)

  1453     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast

  1454    }

  1455    ultimately have False using ordLeq_total card_of_Well_order[of A]

  1456    card_of_Well_order[of B] by blast

  1457   }

  1458   thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]

  1459   card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto

  1460 qed

  1461

  1462 lemma card_of_Plus_ordLess_infinite_Field:

  1463 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and

  1464         LESS1: "|A| <o r" and LESS2: "|B| <o r"

  1465 shows "|A <+> B| <o r"

  1466 proof-

  1467   let ?C  = "Field r"

  1468   have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso

  1469   ordIso_symmetric by blast

  1470   hence "|A| <o |?C|"  "|B| <o |?C|"

  1471   using LESS1 LESS2 ordLess_ordIso_trans by blast+

  1472   hence  "|A <+> B| <o |?C|" using INF

  1473   card_of_Plus_ordLess_infinite by blast

  1474   thus ?thesis using 1 ordLess_ordIso_trans by blast

  1475 qed

  1476

  1477 lemma card_of_Plus_ordLeq_infinite_Field:

  1478 assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"

  1479 and c: "Card_order r"

  1480 shows "|A <+> B| \<le>o r"

  1481 proof-

  1482   let ?r' = "cardSuc r"

  1483   have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms

  1484   by (simp add: cardSuc_Card_order cardSuc_finite)

  1485   moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c

  1486   by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)

  1487   ultimately have "|A <+> B| <o ?r'"

  1488   using card_of_Plus_ordLess_infinite_Field by blast

  1489   thus ?thesis using c r

  1490   by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)

  1491 qed

  1492

  1493 lemma card_of_Un_ordLeq_infinite_Field:

  1494 assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"

  1495 and "Card_order r"

  1496 shows "|A Un B| \<le>o r"

  1497 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq

  1498 ordLeq_transitive by fast

  1499

  1500

  1501 subsection {* Regular cardinals *}

  1502

  1503 definition cofinal where

  1504 "cofinal A r \<equiv>

  1505  ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"

  1506

  1507 definition regularCard where

  1508 "regularCard r \<equiv>

  1509  ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"

  1510

  1511 definition relChain where

  1512 "relChain r As \<equiv>

  1513  ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"

  1514

  1515 lemma regularCard_UNION:

  1516 assumes r: "Card_order r"   "regularCard r"

  1517 and As: "relChain r As"

  1518 and Bsub: "B \<le> (UN i : Field r. As i)"

  1519 and cardB: "|B| <o r"

  1520 shows "EX i : Field r. B \<le> As i"

  1521 proof-

  1522   let ?phi = "%b j. j : Field r \<and> b : As j"

  1523   have "ALL b : B. EX j. ?phi b j" using Bsub by blast

  1524   then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"

  1525   using bchoice[of B ?phi] by blast

  1526   let ?K = "f  B"

  1527   {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"

  1528    have 2: "cofinal ?K r"

  1529    unfolding cofinal_def proof auto

  1530      fix i assume i: "i : Field r"

  1531      with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast

  1532      hence "i \<noteq> f b \<and> ~ (f b,i) : r"

  1533      using As f unfolding relChain_def by auto

  1534      hence "i \<noteq> f b \<and> (i, f b) : r" using r

  1535      unfolding card_order_on_def well_order_on_def linear_order_on_def

  1536      total_on_def using i f b by auto

  1537      with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast

  1538    qed

  1539    moreover have "?K \<le> Field r" using f by blast

  1540    ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast

  1541    moreover

  1542    {

  1543     have "|?K| <=o |B|" using card_of_image .

  1544     hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast

  1545    }

  1546    ultimately have False using not_ordLess_ordIso by blast

  1547   }

  1548   thus ?thesis by blast

  1549 qed

  1550

  1551 lemma infinite_cardSuc_regularCard:

  1552 assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"

  1553 shows "regularCard (cardSuc r)"

  1554 proof-

  1555   let ?r' = "cardSuc r"

  1556   have r': "Card_order ?r'"

  1557   "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"

  1558   using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)

  1559   show ?thesis

  1560   unfolding regularCard_def proof auto

  1561     fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"

  1562     hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)

  1563     also have 22: "|Field ?r'| =o ?r'"

  1564     using r' by (simp add: card_of_Field_ordIso[of ?r'])

  1565     finally have "|K| \<le>o ?r'" .

  1566     moreover

  1567     {let ?L = "UN j : K. underS ?r' j"

  1568      let ?J = "Field r"

  1569      have rJ: "r =o |?J|"

  1570      using r_card card_of_Field_ordIso ordIso_symmetric by blast

  1571      assume "|K| <o ?r'"

  1572      hence "|K| <=o r" using r' card_of_Card_order[of K] by blast

  1573      hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast

  1574      moreover

  1575      {have "ALL j : K. |underS ?r' j| <o ?r'"

  1576       using r' 1 by (auto simp: card_of_underS)

  1577       hence "ALL j : K. |underS ?r' j| \<le>o r"

  1578       using r' card_of_Card_order by blast

  1579       hence "ALL j : K. |underS ?r' j| \<le>o |?J|"

  1580       using rJ ordLeq_ordIso_trans by blast

  1581      }

  1582      ultimately have "|?L| \<le>o |?J|"

  1583      using r_inf card_of_UNION_ordLeq_infinite by blast

  1584      hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast

  1585      hence "|?L| <o ?r'" using r' card_of_Card_order by blast

  1586      moreover

  1587      {

  1588       have "Field ?r' \<le> ?L"

  1589       using 2 unfolding underS_def cofinal_def by auto

  1590       hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)

  1591       hence "?r' \<le>o |?L|"

  1592       using 22 ordIso_ordLeq_trans ordIso_symmetric by blast

  1593      }

  1594      ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast

  1595      hence False using ordLess_irreflexive by blast

  1596     }

  1597     ultimately show "|K| =o ?r'"

  1598     unfolding ordLeq_iff_ordLess_or_ordIso by blast

  1599   qed

  1600 qed

  1601

  1602 lemma cardSuc_UNION:

  1603 assumes r: "Card_order r" and "\<not>finite (Field r)"

  1604 and As: "relChain (cardSuc r) As"

  1605 and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"

  1606 and cardB: "|B| <=o r"

  1607 shows "EX i : Field (cardSuc r). B \<le> As i"

  1608 proof-

  1609   let ?r' = "cardSuc r"

  1610   have "Card_order ?r' \<and> |B| <o ?r'"

  1611   using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order

  1612   card_of_Card_order by blast

  1613   moreover have "regularCard ?r'"

  1614   using assms by(simp add: infinite_cardSuc_regularCard)

  1615   ultimately show ?thesis

  1616   using As Bsub cardB regularCard_UNION by blast

  1617 qed

  1618

  1619

  1620 subsection {* Others *}

  1621

  1622 lemma card_of_Func_Times:

  1623 "|Func (A <*> B) C| =o |Func A (Func B C)|"

  1624 unfolding card_of_ordIso[symmetric]

  1625 using bij_betw_curr by blast

  1626

  1627 lemma card_of_Pow_Func:

  1628 "|Pow A| =o |Func A (UNIV::bool set)|"

  1629 proof-

  1630   def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False)

  1631                             else undefined"

  1632   have "bij_betw F (Pow A) (Func A (UNIV::bool set))"

  1633   unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)

  1634     fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"

  1635     thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)

  1636   next

  1637     show "F  Pow A = Func A UNIV"

  1638     proof safe

  1639       fix f assume f: "f \<in> Func A (UNIV::bool set)"

  1640       show "f \<in> F  Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)

  1641         let ?A1 = "{a \<in> A. f a = True}"

  1642         show "f = F ?A1" unfolding F_def apply(rule ext)

  1643         using f unfolding Func_def mem_Collect_eq by auto

  1644       qed auto

  1645     qed(unfold Func_def mem_Collect_eq F_def, auto)

  1646   qed

  1647   thus ?thesis unfolding card_of_ordIso[symmetric] by blast

  1648 qed

  1649

  1650 lemma card_of_Func_UNIV:

  1651 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|"

  1652 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)

  1653   let ?F = "\<lambda> f (a::'a). ((f a)::'b)"

  1654   show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"

  1655   unfolding bij_betw_def inj_on_def proof safe

  1656     fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"

  1657     hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto

  1658     then obtain f where f: "\<forall> a. h a = f a" by metis

  1659     hence "range f \<subseteq> B" using h unfolding Func_def by auto

  1660     thus "h \<in> (\<lambda>f a. f a)  {f. range f \<subseteq> B}" using f unfolding image_def by auto

  1661   qed(unfold Func_def fun_eq_iff, auto)

  1662 qed

  1663

  1664 end
`