src/HOL/BNF_Cardinal_Order_Relation.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63980 f8e556c8ad6f child 67091 1393c2340eec permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
1 (*  Title:      HOL/BNF_Cardinal_Order_Relation.thy
2     Author:     Andrei Popescu, TU Muenchen
5 Cardinal-order relations as needed by bounded natural functors.
6 *)
8 section \<open>Cardinal-Order Relations as Needed by Bounded Natural Functors\<close>
10 theory BNF_Cardinal_Order_Relation
11 imports Zorn BNF_Wellorder_Constructions
12 begin
14 text\<open>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, \<open>card\<close>, from the theory \<open>Finite_Sets.thy\<close>).
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.
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 \<close>
37 subsection \<open>Cardinal orders\<close>
39 text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
40 order-embedding relation, \<open>\<le>o\<close> (which is the same as being {\em minimal} w.r.t. the
41 strict order-embedding relation, \<open><o\<close>), among all the well-orders on its field.\<close>
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')"
47 abbreviation "Card_order r \<equiv> card_order_on (Field r) r"
48 abbreviation "card_order r \<equiv> card_order_on UNIV r"
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
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
59 text\<open>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 \<open>Zorn.thy\<close> as theorem \<open>well_order_on\<close>),
63 which states that on any given set there exists a well-order;
64 \item The well-founded-ness of \<open><o\<close>, ensuring that then there exists a minimal
65 such well-order, i.e., a cardinal order.
66 \end{itemize}
67 \<close>
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
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
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_Field)
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
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
114 subsection \<open>Cardinal of a set\<close>
116 text\<open>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.\<close>
120 definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
121 where "card_of A = (SOME r. card_order_on A r)"
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)
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
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
133 lemma card_of_Card_order: "Card_order |A|"
134 by (simp only: card_of_card_order_on Field_card_of)
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
140 lemma card_of_Well_order: "Well_order |A|"
141 using card_of_Card_order unfolding card_order_on_def by auto
143 lemma card_of_refl: "|A| =o |A|"
144 using card_of_Well_order ordIso_reflexive by blast
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
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
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 Schroeder_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
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
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
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
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
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
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)
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
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
252 lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|"
253 by (simp add: ordIso_iff_ordLeq card_of_mono2)
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
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
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
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
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
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
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
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
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
346 subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
348 text\<open>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 \<open>=o\<close> and are monotonic w.r.t. \<open>\<le>o\<close>.
352 \<close>
354 lemma card_of_empty: "|{}| \<le>o |A|"
355 using card_of_ordLeq inj_on_id by blast
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
368 corollary Card_order_empty:
369 "Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1)
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
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)
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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   define f :: "('a + 'b) + 'c \<Rightarrow> 'a + 'b + 'c"
474     where [abs_def]: "f k =
475       (case k of
476         Inl ab \<Rightarrow>
477           (case ab of
478             Inl a \<Rightarrow> Inl a
479           | Inr b \<Rightarrow> Inr (Inl b))
480       | Inr c \<Rightarrow> Inr (Inr c))"
481     for k
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
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 blast
533 qed
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
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
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
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
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
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)
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
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)
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
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)
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
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
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" 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
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
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
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
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
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)
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
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 blast
682 qed
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
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
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
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"
710     by atomize_elim (auto intro: bchoice)
711   obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
712   have "inj_on g (Sigma I A) \<and> g  (Sigma I A) \<le> (Sigma I B)"
713   using 1 unfolding inj_on_def using g_def by force
714   thus ?thesis using card_of_ordLeq by blast
715 qed
717 lemma card_of_UNION_Sigma:
718 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
719 using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
721 lemma card_of_bool:
722 assumes "a1 \<noteq> a2"
723 shows "|UNIV::bool set| =o |{a1,a2}|"
724 proof-
725   let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"
726   have "bij_betw ?f UNIV {a1,a2}"
727   proof-
728     {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"
729      hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
730     }
731     moreover
732     {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
733     }
734     moreover
735     {fix a assume *: "a \<in> {a1,a2}"
736      have "a \<in> ?f  UNIV"
737      proof(cases "a = a1")
738        assume "a = a1"
739        hence "?f True = a" by auto  thus ?thesis by blast
740      next
741        assume "a \<noteq> a1" hence "a = a2" using * by auto
742        hence "?f False = a" by auto  thus ?thesis by blast
743      qed
744     }
745     ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast
746   qed
747   thus ?thesis using card_of_ordIso by blast
748 qed
750 lemma card_of_Plus_Times_aux:
751 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
752         LEQ: "|A| \<le>o |B|"
753 shows "|A <+> B| \<le>o |A \<times> B|"
754 proof-
755   have 1: "|UNIV::bool set| \<le>o |A|"
756   using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
757         ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast
758   (*  *)
759   have "|A <+> B| \<le>o |B <+> B|"
760   using LEQ card_of_Plus_mono1 by blast
761   moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"
762   using card_of_Plus_Times_bool by blast
763   moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"
764   using 1 by (simp add: card_of_Times_mono2)
765   moreover have " |B \<times> A| =o |A \<times> B|"
766   using card_of_Times_commute by blast
767   ultimately show "|A <+> B| \<le>o |A \<times> B|"
768   using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]
769         ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]
770         ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]
771   by blast
772 qed
774 lemma card_of_Plus_Times:
775 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
776         B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
777 shows "|A <+> B| \<le>o |A \<times> B|"
778 proof-
779   {assume "|A| \<le>o |B|"
780    hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
781   }
782   moreover
783   {assume "|B| \<le>o |A|"
784    hence "|B <+> A| \<le>o |B \<times> A|"
785    using assms by (auto simp add: card_of_Plus_Times_aux)
786    hence ?thesis
787    using card_of_Plus_commute card_of_Times_commute
788          ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
789   }
790   ultimately show ?thesis
791   using card_of_Well_order[of A] card_of_Well_order[of B]
792         ordLeq_total[of "|A|"] by blast
793 qed
795 lemma card_of_Times_Plus_distrib:
796   "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
797 proof -
798   let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
799   have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
800   thus ?thesis using card_of_ordIso by blast
801 qed
803 lemma card_of_ordLeq_finite:
804 assumes "|A| \<le>o |B|" and "finite B"
805 shows "finite A"
806 using assms unfolding ordLeq_def
807 using embed_inj_on[of "|A|" "|B|"]  embed_Field[of "|A|" "|B|"]
808       Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
810 lemma card_of_ordLeq_infinite:
811 assumes "|A| \<le>o |B|" and "\<not> finite A"
812 shows "\<not> finite B"
813 using assms card_of_ordLeq_finite by auto
815 lemma card_of_ordIso_finite:
816 assumes "|A| =o |B|"
817 shows "finite A = finite B"
818 using assms unfolding ordIso_def iso_def[abs_def]
819 by (auto simp: bij_betw_finite Field_card_of)
821 lemma card_of_ordIso_finite_Field:
822 assumes "Card_order r" and "r =o |A|"
823 shows "finite(Field r) = finite A"
824 using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
827 subsection \<open>Cardinals versus set operations involving infinite sets\<close>
829 text\<open>Here we show that, for infinite sets, most set-theoretic constructions
830 do not increase the cardinality.  The cornerstone for this is
831 theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
832 does not increase cardinality -- the proof of this fact adapts a standard
833 set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
834 at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
836 lemma infinite_iff_card_of_nat:
837 "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
838 unfolding infinite_iff_countable_subset card_of_ordLeq ..
840 text\<open>The next two results correspond to the ZF fact that all infinite cardinals are
841 limit ordinals:\<close>
843 lemma Card_order_infinite_not_under:
844 assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
845 shows "\<not> (\<exists>a. Field r = under r a)"
846 proof(auto)
847   have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
848   using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
849   fix a assume *: "Field r = under r a"
850   show False
851   proof(cases "a \<in> Field r")
852     assume Case1: "a \<notin> Field r"
853     hence "under r a = {}" unfolding Field_def under_def by auto
854     thus False using INF *  by auto
855   next
856     let ?r' = "Restr r (underS r a)"
857     assume Case2: "a \<in> Field r"
858     hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
859     using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
860     have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
861     using 0 wo_rel.underS_ofilter * 1 Case2 by fast
862     hence "?r' <o r" using 0 using ofilter_ordLess by blast
863     moreover
864     have "Field ?r' = underS r a \<and> Well_order ?r'"
865     using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
866     ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
867     moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
868     ultimately have "|underS r a| <o |under r a|"
869     using ordIso_symmetric ordLess_ordIso_trans by blast
870     moreover
871     {have "\<exists>f. bij_betw f (under r a) (underS r a)"
872      using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
873      hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
874     }
875     ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
876   qed
877 qed
879 lemma infinite_Card_order_limit:
880 assumes r: "Card_order r" and "\<not>finite (Field r)"
881 and a: "a : Field r"
882 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
883 proof-
884   have "Field r \<noteq> under r a"
885   using assms Card_order_infinite_not_under by blast
886   moreover have "under r a \<le> Field r"
887   using under_Field .
888   ultimately have "under r a < Field r" by blast
889   then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
890   unfolding under_def by blast
891   moreover have ba: "b \<noteq> a"
892   using 1 r unfolding card_order_on_def well_order_on_def
893   linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
894   ultimately have "(a,b) : r"
895   using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
896   total_on_def by blast
897   thus ?thesis using 1 ba by auto
898 qed
900 theorem Card_order_Times_same_infinite:
901 assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
902 shows "|Field r \<times> Field r| \<le>o r"
903 proof-
904   obtain phi where phi_def:
905   "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
906                       \<not> |Field r \<times> Field r| \<le>o r )" by blast
907   have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
908   unfolding phi_def card_order_on_def by auto
909   have Ft: "\<not>(\<exists>r. phi r)"
910   proof
911     assume "\<exists>r. phi r"
912     hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"
913     using temp1 by auto
914     then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and
915                    3: "Card_order r \<and> Well_order r"
916     using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
917     let ?A = "Field r"  let ?r' = "bsqr r"
918     have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"
919     using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
920     have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"
921     using card_of_Card_order card_of_Well_order by blast
922     (*  *)
923     have "r <o |?A \<times> ?A|"
924     using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
925     moreover have "|?A \<times> ?A| \<le>o ?r'"
926     using card_of_least[of "?A \<times> ?A"] 4 by auto
927     ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
928     then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"
929     unfolding ordLess_def embedS_def[abs_def]
930     by (auto simp add: Field_bsqr)
931     let ?B = "f  ?A"
932     have "|?A| =o |?B|"
933     using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
934     hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
935     (*  *)
936     have "wo_rel.ofilter ?r' ?B"
937     using 6 embed_Field_ofilter 3 4 by blast
938     hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"
939     using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
940     hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
941     using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
942     have "\<not> (\<exists>a. Field r = under r a)"
943     using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
944     then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
945     using temp2 3 bsqr_ofilter[of r ?B] by blast
946     hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast
947     hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast
948     let ?r1 = "Restr r A1"
949     have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
950     moreover
951     {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
952      hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast
953     }
954     ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
955     (*  *)
956     have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
957     hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
958     hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by blast
959     moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
960     using card_of_Card_order[of A1] card_of_Well_order[of A1]
961     by (simp add: Field_card_of)
962     moreover have "\<not> r \<le>o | A1 |"
963     using temp4 11 3 using not_ordLeq_iff_ordLess by blast
964     ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
965     by (simp add: card_of_card_order_on)
966     hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
967     using 2 unfolding phi_def by blast
968     hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto
969     hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast
970     thus False using 11 not_ordLess_ordLeq by auto
971   qed
972   thus ?thesis using assms unfolding phi_def by blast
973 qed
975 corollary card_of_Times_same_infinite:
976 assumes "\<not>finite A"
977 shows "|A \<times> A| =o |A|"
978 proof-
979   let ?r = "|A|"
980   have "Field ?r = A \<and> Card_order ?r"
981   using Field_card_of card_of_Card_order[of A] by fastforce
982   hence "|A \<times> A| \<le>o |A|"
983   using Card_order_Times_same_infinite[of ?r] assms by auto
984   thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
985 qed
987 lemma card_of_Times_infinite:
988 assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
989 shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
990 proof-
991   have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
992   using assms by (simp add: card_of_Times1 card_of_Times2)
993   moreover
994   {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"
995    using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
996    moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast
997    ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"
998    using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto
999   }
1000   ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
1001 qed
1003 corollary Card_order_Times_infinite:
1004 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
1005         NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
1006 shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
1007 proof-
1008   have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"
1009   using assms by (simp add: card_of_Times_infinite card_of_mono2)
1010   thus ?thesis
1011   using assms card_of_Field_ordIso[of r]
1012         ordIso_transitive[of "|Field r \<times> Field p|"]
1013         ordIso_transitive[of _ "|Field r|"] by blast
1014 qed
1016 lemma card_of_Sigma_ordLeq_infinite:
1017 assumes INF: "\<not>finite B" and
1018         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1019 shows "|SIGMA i : I. A i| \<le>o |B|"
1020 proof(cases "I = {}", simp add: card_of_empty)
1021   assume *: "I \<noteq> {}"
1022   have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
1023   using card_of_Sigma_mono1[OF LEQ] by blast
1024   moreover have "|I \<times> B| =o |B|"
1025   using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
1026   ultimately show ?thesis using ordLeq_ordIso_trans by blast
1027 qed
1029 lemma card_of_Sigma_ordLeq_infinite_Field:
1030 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1031         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1032 shows "|SIGMA i : I. A i| \<le>o r"
1033 proof-
1034   let ?B  = "Field r"
1035   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1036   ordIso_symmetric by blast
1037   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
1038   using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1039   hence  "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ
1040   card_of_Sigma_ordLeq_infinite by blast
1041   thus ?thesis using 1 ordLeq_ordIso_trans by blast
1042 qed
1044 lemma card_of_Times_ordLeq_infinite_Field:
1045 "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
1046  \<Longrightarrow> |A \<times> B| \<le>o r"
1047 by(simp add: card_of_Sigma_ordLeq_infinite_Field)
1049 lemma card_of_Times_infinite_simps:
1050 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
1051 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
1052 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
1053 "\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
1054 by (auto simp add: card_of_Times_infinite ordIso_symmetric)
1056 lemma card_of_UNION_ordLeq_infinite:
1057 assumes INF: "\<not>finite B" and
1058         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1059 shows "|\<Union>i \<in> I. A i| \<le>o |B|"
1060 proof(cases "I = {}", simp add: card_of_empty)
1061   assume *: "I \<noteq> {}"
1062   have "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
1063   using card_of_UNION_Sigma by blast
1064   moreover have "|SIGMA i : I. A i| \<le>o |B|"
1065   using assms card_of_Sigma_ordLeq_infinite by blast
1066   ultimately show ?thesis using ordLeq_transitive by blast
1067 qed
1069 corollary card_of_UNION_ordLeq_infinite_Field:
1070 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1071         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1072 shows "|\<Union>i \<in> I. A i| \<le>o r"
1073 proof-
1074   let ?B  = "Field r"
1075   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1076   ordIso_symmetric by blast
1077   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
1078   using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1079   hence  "|\<Union>i \<in> I. A i| \<le>o |?B|" using INF LEQ
1080   card_of_UNION_ordLeq_infinite by blast
1081   thus ?thesis using 1 ordLeq_ordIso_trans by blast
1082 qed
1084 lemma card_of_Plus_infinite1:
1085 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1086 shows "|A <+> B| =o |A|"
1087 proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
1088   let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
1089   assume *: "B \<noteq> {}"
1090   then obtain b1 where 1: "b1 \<in> B" by blast
1091   show ?thesis
1092   proof(cases "B = {b1}")
1093     assume Case1: "B = {b1}"
1094     have 2: "bij_betw ?Inl A ((?Inl  A))"
1095     unfolding bij_betw_def inj_on_def by auto
1096     hence 3: "\<not>finite (?Inl  A)"
1097     using INF bij_betw_finite[of ?Inl A] by blast
1098     let ?A' = "?Inl  A \<union> {?Inr b1}"
1099     obtain g where "bij_betw g (?Inl  A) ?A'"
1100     using 3 infinite_imp_bij_betw2[of "?Inl  A"] by auto
1101     moreover have "?A' = A <+> B" using Case1 by blast
1102     ultimately have "bij_betw g (?Inl  A) (A <+> B)" by simp
1103     hence "bij_betw (g o ?Inl) A (A <+> B)"
1104     using 2 by (auto simp add: bij_betw_trans)
1105     thus ?thesis using card_of_ordIso ordIso_symmetric by blast
1106   next
1107     assume Case2: "B \<noteq> {b1}"
1108     with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce
1109     obtain f where "inj_on f B \<and> f  B \<le> A"
1110     using LEQ card_of_ordLeq[of B] by fastforce
1111     with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"
1112     unfolding inj_on_def by auto
1113     with 3 have "|A <+> B| \<le>o |A \<times> B|"
1114     by (auto simp add: card_of_Plus_Times)
1115     moreover have "|A \<times> B| =o |A|"
1116     using assms * by (simp add: card_of_Times_infinite_simps)
1117     ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
1118     thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
1119   qed
1120 qed
1122 lemma card_of_Plus_infinite2:
1123 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1124 shows "|B <+> A| =o |A|"
1125 using assms card_of_Plus_commute card_of_Plus_infinite1
1126 ordIso_equivalence by blast
1128 lemma card_of_Plus_infinite:
1129 assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1130 shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
1131 using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
1133 corollary Card_order_Plus_infinite:
1134 assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
1135         LEQ: "p \<le>o r"
1136 shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
1137 proof-
1138   have "| Field r <+> Field p | =o | Field r | \<and>
1139         | Field p <+> Field r | =o | Field r |"
1140   using assms by (simp add: card_of_Plus_infinite card_of_mono2)
1141   thus ?thesis
1142   using assms card_of_Field_ordIso[of r]
1143         ordIso_transitive[of "|Field r <+> Field p|"]
1144         ordIso_transitive[of _ "|Field r|"] by blast
1145 qed
1148 subsection \<open>The cardinal $\omega$ and the finite cardinals\<close>
1150 text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1151 order relation on
1152 \<open>nat\<close>, that we abbreviate by \<open>natLeq\<close>.  The finite cardinals
1153 shall be the restrictions of these relations to the numbers smaller than
1154 fixed numbers \<open>n\<close>, that we abbreviate by \<open>natLeq_on n\<close>.\<close>
1156 definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1157 definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1159 abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
1160 where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
1162 lemma infinite_cartesian_product:
1163 assumes "\<not>finite A" "\<not>finite B"
1164 shows "\<not>finite (A \<times> B)"
1165 proof
1166   assume "finite (A \<times> B)"
1167   from assms(1) have "A \<noteq> {}" by auto
1168   with \<open>finite (A \<times> B)\<close> have "finite B" using finite_cartesian_productD2 by auto
1169   with assms(2) show False by simp
1170 qed
1173 subsubsection \<open>First as well-orders\<close>
1175 lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
1176 by(unfold Field_def natLeq_def, auto)
1178 lemma natLeq_Refl: "Refl natLeq"
1179 unfolding refl_on_def Field_def natLeq_def by auto
1181 lemma natLeq_trans: "trans natLeq"
1182 unfolding trans_def natLeq_def by auto
1184 lemma natLeq_Preorder: "Preorder natLeq"
1185 unfolding preorder_on_def
1186 by (auto simp add: natLeq_Refl natLeq_trans)
1188 lemma natLeq_antisym: "antisym natLeq"
1189 unfolding antisym_def natLeq_def by auto
1191 lemma natLeq_Partial_order: "Partial_order natLeq"
1192 unfolding partial_order_on_def
1193 by (auto simp add: natLeq_Preorder natLeq_antisym)
1195 lemma natLeq_Total: "Total natLeq"
1196 unfolding total_on_def natLeq_def by auto
1198 lemma natLeq_Linear_order: "Linear_order natLeq"
1199 unfolding linear_order_on_def
1200 by (auto simp add: natLeq_Partial_order natLeq_Total)
1202 lemma natLeq_natLess_Id: "natLess = natLeq - Id"
1203 unfolding natLeq_def natLess_def by auto
1205 lemma natLeq_Well_order: "Well_order natLeq"
1206 unfolding well_order_on_def
1207 using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
1209 lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
1210 unfolding Field_def by auto
1212 lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
1213 unfolding underS_def natLeq_def by auto
1215 lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
1216 unfolding natLeq_def by force
1218 lemma Restr_natLeq2:
1219 "Restr natLeq (underS natLeq n) = natLeq_on n"
1220 by (auto simp add: Restr_natLeq natLeq_underS_less)
1222 lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
1223 using Restr_natLeq[of n] natLeq_Well_order
1224       Well_order_Restr[of natLeq "{x. x < n}"] by auto
1226 corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
1227 using natLeq_on_Well_order Field_natLeq_on by auto
1229 lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
1230 unfolding wo_rel_def using natLeq_on_Well_order .
1233 subsubsection \<open>Then as cardinals\<close>
1235 lemma natLeq_Card_order: "Card_order natLeq"
1236 proof(auto simp add: natLeq_Well_order
1237       Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
1238   fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
1239   moreover have "\<not>finite(UNIV::nat set)" by auto
1240   ultimately show "natLeq_on n <o |UNIV::nat set|"
1241   using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
1242         Field_card_of[of "UNIV::nat set"]
1243         card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
1244 qed
1246 corollary card_of_Field_natLeq:
1247 "|Field natLeq| =o natLeq"
1248 using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
1249       ordIso_symmetric[of natLeq] by blast
1251 corollary card_of_nat:
1252 "|UNIV::nat set| =o natLeq"
1253 using Field_natLeq card_of_Field_natLeq by auto
1255 corollary infinite_iff_natLeq_ordLeq:
1256 "\<not>finite A = ( natLeq \<le>o |A| )"
1257 using infinite_iff_card_of_nat[of A] card_of_nat
1258       ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
1260 corollary finite_iff_ordLess_natLeq:
1261 "finite A = ( |A| <o natLeq)"
1262 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
1263       card_of_Well_order natLeq_Well_order by blast
1266 subsection \<open>The successor of a cardinal\<close>
1268 text\<open>First we define \<open>isCardSuc r r'\<close>, the notion of \<open>r'\<close>
1269 being a successor cardinal of \<open>r\<close>. Although the definition does
1270 not require \<open>r\<close> to be a cardinal, only this case will be meaningful.\<close>
1272 definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1273 where
1274 "isCardSuc r r' \<equiv>
1275  Card_order r' \<and> r <o r' \<and>
1276  (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
1278 text\<open>Now we introduce the cardinal-successor operator \<open>cardSuc\<close>,
1279 by picking {\em some} cardinal-order relation fulfilling \<open>isCardSuc\<close>.
1280 Again, the picked item shall be proved unique up to order-isomorphism.\<close>
1282 definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
1283 where
1284 "cardSuc r \<equiv> SOME r'. isCardSuc r r'"
1286 lemma exists_minim_Card_order:
1287 "\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
1288 unfolding card_order_on_def using exists_minim_Well_order by blast
1290 lemma exists_isCardSuc:
1291 assumes "Card_order r"
1292 shows "\<exists>r'. isCardSuc r r'"
1293 proof-
1294   let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"
1295   have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms
1296   by (simp add: card_of_Card_order Card_order_Pow)
1297   then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"
1298   using exists_minim_Card_order[of ?R] by blast
1299   thus ?thesis unfolding isCardSuc_def by auto
1300 qed
1302 lemma cardSuc_isCardSuc:
1303 assumes "Card_order r"
1304 shows "isCardSuc r (cardSuc r)"
1305 unfolding cardSuc_def using assms
1306 by (simp add: exists_isCardSuc someI_ex)
1308 lemma cardSuc_Card_order:
1309 "Card_order r \<Longrightarrow> Card_order(cardSuc r)"
1310 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1312 lemma cardSuc_greater:
1313 "Card_order r \<Longrightarrow> r <o cardSuc r"
1314 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1316 lemma cardSuc_ordLeq:
1317 "Card_order r \<Longrightarrow> r \<le>o cardSuc r"
1318 using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1320 text\<open>The minimality property of \<open>cardSuc\<close> originally present in its definition
1321 is local to the type \<open>'a set rel\<close>, i.e., that of \<open>cardSuc r\<close>:\<close>
1323 lemma cardSuc_least_aux:
1324 "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
1325 using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1327 text\<open>But from this we can infer general minimality:\<close>
1329 lemma cardSuc_least:
1330 assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
1331 shows "cardSuc r \<le>o r'"
1332 proof-
1333   let ?p = "cardSuc r"
1334   have 0: "Well_order ?p \<and> Well_order r'"
1335   using assms cardSuc_Card_order unfolding card_order_on_def by blast
1336   {assume "r' <o ?p"
1337    then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"
1338    using internalize_ordLess[of r' ?p] by blast
1339    (*  *)
1340    have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
1341    moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
1342    ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast
1343    hence False using 2 not_ordLess_ordLeq by blast
1344   }
1345   thus ?thesis using 0 ordLess_or_ordLeq by blast
1346 qed
1348 lemma cardSuc_ordLess_ordLeq:
1349 assumes CARD: "Card_order r" and CARD': "Card_order r'"
1350 shows "(r <o r') = (cardSuc r \<le>o r')"
1351 proof(auto simp add: assms cardSuc_least)
1352   assume "cardSuc r \<le>o r'"
1353   thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast
1354 qed
1356 lemma cardSuc_ordLeq_ordLess:
1357 assumes CARD: "Card_order r" and CARD': "Card_order r'"
1358 shows "(r' <o cardSuc r) = (r' \<le>o r)"
1359 proof-
1360   have "Well_order r \<and> Well_order r'"
1361   using assms unfolding card_order_on_def by auto
1362   moreover have "Well_order(cardSuc r)"
1363   using assms cardSuc_Card_order card_order_on_def by blast
1364   ultimately show ?thesis
1365   using assms cardSuc_ordLess_ordLeq[of r r']
1366   not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
1367 qed
1369 lemma cardSuc_mono_ordLeq:
1370 assumes CARD: "Card_order r" and CARD': "Card_order r'"
1371 shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"
1372 using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
1374 lemma cardSuc_invar_ordIso:
1375 assumes CARD: "Card_order r" and CARD': "Card_order r'"
1376 shows "(cardSuc r =o cardSuc r') = (r =o r')"
1377 proof-
1378   have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
1379   using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
1380   thus ?thesis
1381   using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
1382   using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
1383 qed
1385 lemma card_of_cardSuc_finite:
1386 "finite(Field(cardSuc |A| )) = finite A"
1387 proof
1388   assume *: "finite (Field (cardSuc |A| ))"
1389   have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
1390   using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
1391   hence "|A| \<le>o |Field(cardSuc |A| )|"
1392   using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
1393   ordLeq_ordIso_trans by blast
1394   thus "finite A" using * card_of_ordLeq_finite by blast
1395 next
1396   assume "finite A"
1397   then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
1398   then show "finite (Field (cardSuc |A| ))"
1399   proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
1400     show "cardSuc |A| \<le>o |Pow A|"
1401       by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
1402   qed
1403 qed
1405 lemma cardSuc_finite:
1406 assumes "Card_order r"
1407 shows "finite (Field (cardSuc r)) = finite (Field r)"
1408 proof-
1409   let ?A = "Field r"
1410   have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
1411   hence "cardSuc |?A| =o cardSuc r" using assms
1412   by (simp add: card_of_Card_order cardSuc_invar_ordIso)
1413   moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
1414   by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
1415   moreover
1416   {have "|Field (cardSuc r) | =o cardSuc r"
1417    using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
1418    hence "cardSuc r =o |Field (cardSuc r) |"
1419    using ordIso_symmetric by blast
1420   }
1421   ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
1422   using ordIso_transitive by blast
1423   hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
1424   using card_of_ordIso_finite by blast
1425   thus ?thesis by (simp only: card_of_cardSuc_finite)
1426 qed
1428 lemma card_of_Plus_ordLess_infinite:
1429 assumes INF: "\<not>finite C" and
1430         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
1431 shows "|A <+> B| <o |C|"
1432 proof(cases "A = {} \<or> B = {}")
1433   assume Case1: "A = {} \<or> B = {}"
1434   hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"
1435   using card_of_Plus_empty1 card_of_Plus_empty2 by blast
1436   hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"
1437   using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
1438   thus ?thesis using LESS1 LESS2
1439        ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
1440        ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
1441 next
1442   assume Case2: "\<not>(A = {} \<or> B = {})"
1443   {assume *: "|C| \<le>o |A <+> B|"
1444    hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
1445    hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
1446    {assume Case21: "|A| \<le>o |B|"
1447     hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
1448     hence "|A <+> B| =o |B|" using Case2 Case21
1449     by (auto simp add: card_of_Plus_infinite)
1450     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1451    }
1452    moreover
1453    {assume Case22: "|B| \<le>o |A|"
1454     hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
1455     hence "|A <+> B| =o |A|" using Case2 Case22
1456     by (auto simp add: card_of_Plus_infinite)
1457     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1458    }
1459    ultimately have False using ordLeq_total card_of_Well_order[of A]
1460    card_of_Well_order[of B] by blast
1461   }
1462   thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
1463   card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
1464 qed
1466 lemma card_of_Plus_ordLess_infinite_Field:
1467 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1468         LESS1: "|A| <o r" and LESS2: "|B| <o r"
1469 shows "|A <+> B| <o r"
1470 proof-
1471   let ?C  = "Field r"
1472   have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
1473   ordIso_symmetric by blast
1474   hence "|A| <o |?C|"  "|B| <o |?C|"
1475   using LESS1 LESS2 ordLess_ordIso_trans by blast+
1476   hence  "|A <+> B| <o |?C|" using INF
1477   card_of_Plus_ordLess_infinite by blast
1478   thus ?thesis using 1 ordLess_ordIso_trans by blast
1479 qed
1481 lemma card_of_Plus_ordLeq_infinite_Field:
1482 assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1483 and c: "Card_order r"
1484 shows "|A <+> B| \<le>o r"
1485 proof-
1486   let ?r' = "cardSuc r"
1487   have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
1488   by (simp add: cardSuc_Card_order cardSuc_finite)
1489   moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
1490   by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1491   ultimately have "|A <+> B| <o ?r'"
1492   using card_of_Plus_ordLess_infinite_Field by blast
1493   thus ?thesis using c r
1494   by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1495 qed
1497 lemma card_of_Un_ordLeq_infinite_Field:
1498 assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1499 and "Card_order r"
1500 shows "|A Un B| \<le>o r"
1501 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
1502 ordLeq_transitive by fast
1505 subsection \<open>Regular cardinals\<close>
1507 definition cofinal where
1508 "cofinal A r \<equiv>
1509  ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
1511 definition regularCard where
1512 "regularCard r \<equiv>
1513  ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1515 definition relChain where
1516 "relChain r As \<equiv>
1517  ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1519 lemma regularCard_UNION:
1520 assumes r: "Card_order r"   "regularCard r"
1521 and As: "relChain r As"
1522 and Bsub: "B \<le> (UN i : Field r. As i)"
1523 and cardB: "|B| <o r"
1524 shows "EX i : Field r. B \<le> As i"
1525 proof-
1526   let ?phi = "%b j. j : Field r \<and> b : As j"
1527   have "ALL b : B. EX j. ?phi b j" using Bsub by blast
1528   then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"
1529   using bchoice[of B ?phi] by blast
1530   let ?K = "f  B"
1531   {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"
1532    have 2: "cofinal ?K r"
1533    unfolding cofinal_def proof auto
1534      fix i assume i: "i : Field r"
1535      with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast
1536      hence "i \<noteq> f b \<and> ~ (f b,i) : r"
1537      using As f unfolding relChain_def by auto
1538      hence "i \<noteq> f b \<and> (i, f b) : r" using r
1539      unfolding card_order_on_def well_order_on_def linear_order_on_def
1540      total_on_def using i f b by auto
1541      with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
1542    qed
1543    moreover have "?K \<le> Field r" using f by blast
1544    ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast
1545    moreover
1546    {
1547     have "|?K| <=o |B|" using card_of_image .
1548     hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast
1549    }
1550    ultimately have False using not_ordLess_ordIso by blast
1551   }
1552   thus ?thesis by blast
1553 qed
1555 lemma infinite_cardSuc_regularCard:
1556 assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
1557 shows "regularCard (cardSuc r)"
1558 proof-
1559   let ?r' = "cardSuc r"
1560   have r': "Card_order ?r'"
1561   "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"
1562   using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
1563   show ?thesis
1564   unfolding regularCard_def proof auto
1565     fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
1566     hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
1567     also have 22: "|Field ?r'| =o ?r'"
1568     using r' by (simp add: card_of_Field_ordIso[of ?r'])
1569     finally have "|K| \<le>o ?r'" .
1570     moreover
1571     {let ?L = "UN j : K. underS ?r' j"
1572      let ?J = "Field r"
1573      have rJ: "r =o |?J|"
1574      using r_card card_of_Field_ordIso ordIso_symmetric by blast
1575      assume "|K| <o ?r'"
1576      hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
1577      hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
1578      moreover
1579      {have "ALL j : K. |underS ?r' j| <o ?r'"
1580       using r' 1 by (auto simp: card_of_underS)
1581       hence "ALL j : K. |underS ?r' j| \<le>o r"
1582       using r' card_of_Card_order by blast
1583       hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
1584       using rJ ordLeq_ordIso_trans by blast
1585      }
1586      ultimately have "|?L| \<le>o |?J|"
1587      using r_inf card_of_UNION_ordLeq_infinite by blast
1588      hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
1589      hence "|?L| <o ?r'" using r' card_of_Card_order by blast
1590      moreover
1591      {
1592       have "Field ?r' \<le> ?L"
1593       using 2 unfolding underS_def cofinal_def by auto
1594       hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
1595       hence "?r' \<le>o |?L|"
1596       using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
1597      }
1598      ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast
1599      hence False using ordLess_irreflexive by blast
1600     }
1601     ultimately show "|K| =o ?r'"
1602     unfolding ordLeq_iff_ordLess_or_ordIso by blast
1603   qed
1604 qed
1606 lemma cardSuc_UNION:
1607 assumes r: "Card_order r" and "\<not>finite (Field r)"
1608 and As: "relChain (cardSuc r) As"
1609 and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
1610 and cardB: "|B| <=o r"
1611 shows "EX i : Field (cardSuc r). B \<le> As i"
1612 proof-
1613   let ?r' = "cardSuc r"
1614   have "Card_order ?r' \<and> |B| <o ?r'"
1615   using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
1616   card_of_Card_order by blast
1617   moreover have "regularCard ?r'"
1618   using assms by(simp add: infinite_cardSuc_regularCard)
1619   ultimately show ?thesis
1620   using As Bsub cardB regularCard_UNION by blast
1621 qed
1624 subsection \<open>Others\<close>
1626 lemma card_of_Func_Times:
1627 "|Func (A \<times> B) C| =o |Func A (Func B C)|"
1628 unfolding card_of_ordIso[symmetric]
1629 using bij_betw_curr by blast
1631 lemma card_of_Pow_Func:
1632 "|Pow A| =o |Func A (UNIV::bool set)|"
1633 proof-
1634   define F where [abs_def]: "F A' a =
1635     (if a \<in> A then (if a \<in> A' then True else False) else undefined)" for A' a
1636   have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
1637   unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
1638     fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
1639     thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: if_split_asm)
1640   next
1641     show "F  Pow A = Func A UNIV"
1642     proof safe
1643       fix f assume f: "f \<in> Func A (UNIV::bool set)"
1644       show "f \<in> F  Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
1645         let ?A1 = "{a \<in> A. f a = True}"
1646         show "f = F ?A1"
1647           unfolding F_def apply(rule ext)
1648           using f unfolding Func_def mem_Collect_eq by auto
1649       qed auto
1650     qed(unfold Func_def mem_Collect_eq F_def, auto)
1651   qed
1652   thus ?thesis unfolding card_of_ordIso[symmetric] by blast
1653 qed
1655 lemma card_of_Func_UNIV:
1656 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|"
1657 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
1658   let ?F = "\<lambda> f (a::'a). ((f a)::'b)"
1659   show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"
1660   unfolding bij_betw_def inj_on_def proof safe
1661     fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
1662     hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
1663     then obtain f where f: "\<forall> a. h a = f a" by blast
1664     hence "range f \<subseteq> B" using h unfolding Func_def by auto
1665     thus "h \<in> (\<lambda>f a. f a)  {f. range f \<subseteq> B}" using f by auto
1666   qed(unfold Func_def fun_eq_iff, auto)
1667 qed
1669 lemma Func_Times_Range:
1670   "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
1671 proof -
1672   let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
1673                   \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
1674   let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
1675   have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
1676   proof (intro conjI impI ballI equalityI subsetI)
1677     fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
1678     show "f = g"
1679     proof
1680       fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
1681         by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
1682       then show "f x = g x" by (subst (1 2) surjective_pairing) simp
1683     qed
1684   next
1685     fix fg assume "fg \<in> Func A B \<times> Func A C"
1686     thus "fg \<in> ?F ` Func A (B \<times> C)"
1687       by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
1688   qed (auto simp: Func_def fun_eq_iff)
1689   thus ?thesis using card_of_ordIso by blast
1690 qed
1692 end