1(* Title: HOL/BNF_Cardinal_Order_Relation.thy 2 Author: Andrei Popescu, TU Muenchen 3 Copyright 2012 4 5Cardinal-order relations as needed by bounded natural functors. 6*) 7 8section \<open>Cardinal-Order Relations as Needed by Bounded Natural Functors\<close> 9 10theory BNF_Cardinal_Order_Relation 11imports Zorn BNF_Wellorder_Constructions 12begin 13 14text\<open>In this section, we define cardinal-order relations to be minim well-orders 15on their field. Then we define the cardinal of a set to be {\em some} cardinal-order 16relation on that set, which will be unique up to order isomorphism. Then we study 17the connection between cardinals and: 18\begin{itemize} 19\item standard set-theoretic constructions: products, 20sums, unions, lists, powersets, set-of finite sets operator; 21\item finiteness and infiniteness (in particular, with the numeric cardinal operator 22for finite sets, \<open>card\<close>, from the theory \<open>Finite_Sets.thy\<close>). 23\end{itemize} 24% 25On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also 26define (again, up to order isomorphism) the successor of a cardinal, and show that 27any cardinal admits a successor. 28 29Main results of this section are the existence of cardinal relations and the 30facts that, in the presence of infiniteness, 31most 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 33any infinite set has the same cardinality (hence, is in bijection) with that set. 34\<close> 35 36 37subsection \<open>Cardinal orders\<close> 38 39text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the 40order-embedding relation, \<open>\<le>o\<close> (which is the same as being {\em minimal} w.r.t. the 41strict order-embedding relation, \<open><o\<close>), among all the well-orders on its field.\<close> 42 43definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" 44where 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 47abbreviation "Card_order r \<equiv> card_order_on (Field r) r" 48abbreviation "card_order r \<equiv> card_order_on UNIV r" 49 50lemma card_order_on_well_order_on: 51assumes "card_order_on A r" 52shows "well_order_on A r" 53using assms unfolding card_order_on_def by simp 54 55lemma card_order_on_Card_order: 56"card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r" 57unfolding card_order_on_def using well_order_on_Field by blast 58 59text\<open>The existence of a cardinal relation on any given set (which will mean 60that 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>), 63which 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 65such well-order, i.e., a cardinal order. 66\end{itemize} 67\<close> 68 69theorem card_order_on: "\<exists>r. card_order_on A r" 70proof- 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 77qed 78 79lemma card_order_on_ordIso: 80assumes CO: "card_order_on A r" and CO': "card_order_on A r'" 81shows "r =o r'" 82using assms unfolding card_order_on_def 83using ordIso_iff_ordLeq by blast 84 85lemma Card_order_ordIso: 86assumes CO: "Card_order r" and ISO: "r' =o r" 87shows "Card_order r'" 88using ISO unfolding ordIso_def 89proof(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 106qed 107 108lemma Card_order_ordIso2: 109assumes CO: "Card_order r" and ISO: "r =o r'" 110shows "Card_order r'" 111using assms Card_order_ordIso ordIso_symmetric by blast 112 113 114subsection \<open>Cardinal of a set\<close> 115 116text\<open>We define the cardinal of set to be {\em some} cardinal order on that set. 117We shall prove that this notion is unique up to order isomorphism, meaning 118that order isomorphism shall be the true identity of cardinals.\<close> 119 120definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" ) 121where "card_of A = (SOME r. card_order_on A r)" 122 123lemma card_of_card_order_on: "card_order_on A |A|" 124unfolding card_of_def by (auto simp add: card_order_on someI_ex) 125 126lemma card_of_well_order_on: "well_order_on A |A|" 127using card_of_card_order_on card_order_on_def by blast 128 129lemma Field_card_of: "Field |A| = A" 130using card_of_card_order_on[of A] unfolding card_order_on_def 131using well_order_on_Field by blast 132 133lemma card_of_Card_order: "Card_order |A|" 134by (simp only: card_of_card_order_on Field_card_of) 135 136corollary ordIso_card_of_imp_Card_order: 137"r =o |A| \<Longrightarrow> Card_order r" 138using card_of_Card_order Card_order_ordIso by blast 139 140lemma card_of_Well_order: "Well_order |A|" 141using card_of_Card_order unfolding card_order_on_def by auto 142 143lemma card_of_refl: "|A| =o |A|" 144using card_of_Well_order ordIso_reflexive by blast 145 146lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r" 147using card_of_card_order_on unfolding card_order_on_def by blast 148 149lemma card_of_ordIso: 150"(\<exists>f. bij_betw f A B) = ( |A| =o |B| )" 151proof(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 166next 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 172qed 173 174lemma card_of_ordLeq: 175"(\<exists>f. inj_on f A \<and> f ` A \<le> B) = ( |A| \<le>o |B| )" 176proof(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) 192next 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 200qed 201 202lemma card_of_ordLeq2: 203"A \<noteq> {} \<Longrightarrow> (\<exists>g. g ` B = A) = ( |A| \<le>o |B| )" 204using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto 205 206lemma card_of_ordLess: 207"(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = ( |B| <o |A| )" 208proof- 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 . 215qed 216 217lemma card_of_ordLess2: 218"B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f ` A = B)) = ( |A| <o |B| )" 219using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto 220 221lemma card_of_ordIsoI: 222assumes "bij_betw f A B" 223shows "|A| =o |B|" 224using assms unfolding card_of_ordIso[symmetric] by auto 225 226lemma card_of_ordLeqI: 227assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B" 228shows "|A| \<le>o |B|" 229using assms unfolding card_of_ordLeq[symmetric] by auto 230 231lemma card_of_unique: 232"card_order_on A r \<Longrightarrow> r =o |A|" 233by (simp only: card_order_on_ordIso card_of_card_order_on) 234 235lemma card_of_mono1: 236"A \<le> B \<Longrightarrow> |A| \<le>o |B|" 237using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce 238 239lemma card_of_mono2: 240assumes "r \<le>o r'" 241shows "|Field r| \<le>o |Field r'|" 242proof- 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 250qed 251 252lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|" 253by (simp add: ordIso_iff_ordLeq card_of_mono2) 254 255lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r" 256using card_of_least card_of_well_order_on well_order_on_Well_order by blast 257 258lemma card_of_Field_ordIso: 259assumes "Card_order r" 260shows "|Field r| =o r" 261proof- 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 267qed 268 269lemma Card_order_iff_ordIso_card_of: 270"Card_order r = (r =o |Field r| )" 271using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast 272 273lemma Card_order_iff_ordLeq_card_of: 274"Card_order r = (r \<le>o |Field r| )" 275proof- 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 . 284qed 285 286lemma Card_order_iff_Restr_underS: 287assumes "Well_order r" 288shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )" 289using assms unfolding Card_order_iff_ordLeq_card_of 290using ordLeq_iff_ordLess_Restr card_of_Well_order by blast 291 292lemma card_of_underS: 293assumes r: "Card_order r" and a: "a \<in> Field r" 294shows "|underS r a| <o r" 295proof- 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 . 313qed 314 315lemma ordLess_Field: 316assumes "r <o r'" 317shows "|Field r| <o r'" 318proof- 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 323qed 324 325lemma internalize_card_of_ordLeq: 326"( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)" 327proof 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 336next 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 339qed 340 341lemma internalize_card_of_ordLeq2: 342"( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )" 343using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto 344 345 346subsection \<open>Cardinals versus set operations on arbitrary sets\<close> 347 348text\<open>Here we embark in a long journey of simple results showing 349that the standard set-theoretic operations are well-behaved w.r.t. the notion of 350cardinal -- 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> 353 354lemma card_of_empty: "|{}| \<le>o |A|" 355using card_of_ordLeq inj_on_id by blast 356 357lemma card_of_empty1: 358assumes "Well_order r \<or> Card_order r" 359shows "|{}| \<le>o r" 360proof- 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 366qed 367 368corollary Card_order_empty: 369"Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1) 370 371lemma card_of_empty2: 372assumes LEQ: "|A| =o |{}|" 373shows "A = {}" 374using assms card_of_ordIso[of A] bij_betw_empty2 by blast 375 376lemma card_of_empty3: 377assumes LEQ: "|A| \<le>o |{}|" 378shows "A = {}" 379using assms 380by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2 381 ordLeq_Well_order_simp) 382 383lemma card_of_empty_ordIso: 384"|{}::'a set| =o |{}::'b set|" 385using card_of_ordIso unfolding bij_betw_def inj_on_def by blast 386 387lemma card_of_image: 388"|f ` A| <=o |A|" 389proof(cases "A = {}", simp add: card_of_empty) 390 assume "A \<noteq> {}" 391 hence "f ` A \<noteq> {}" by auto 392 thus "|f ` A| \<le>o |A|" 393 using card_of_ordLeq2[of "f ` A" A] by auto 394qed 395 396lemma surj_imp_ordLeq: 397assumes "B \<subseteq> f ` A" 398shows "|B| \<le>o |A|" 399proof- 400 have "|B| <=o |f ` A|" using assms card_of_mono1 by auto 401 thus ?thesis using card_of_image ordLeq_transitive by blast 402qed 403 404lemma card_of_singl_ordLeq: 405assumes "A \<noteq> {}" 406shows "|{b}| \<le>o |A|" 407proof- 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) 413qed 414 415corollary Card_order_singl_ordLeq: 416"\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r" 417using card_of_singl_ordLeq[of "Field r" b] 418 card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast 419 420lemma card_of_Pow: "|A| <o |Pow A|" 421using card_of_ordLess2[of "Pow A" A] Cantors_paradox[of A] 422 Pow_not_empty[of A] by auto 423 424corollary Card_order_Pow: 425"Card_order r \<Longrightarrow> r <o |Pow(Field r)|" 426using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast 427 428lemma card_of_Plus1: "|A| \<le>o |A <+> B|" 429proof- 430 have "Inl ` A \<le> A <+> B" by auto 431 thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast 432qed 433 434corollary Card_order_Plus1: 435"Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|" 436using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast 437 438lemma card_of_Plus2: "|B| \<le>o |A <+> B|" 439proof- 440 have "Inr ` B \<le> A <+> B" by auto 441 thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast 442qed 443 444corollary Card_order_Plus2: 445"Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|" 446using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast 447 448lemma card_of_Plus_empty1: "|A| =o |A <+> {}|" 449proof- 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 452qed 453 454lemma card_of_Plus_empty2: "|A| =o |{} <+> A|" 455proof- 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 458qed 459 460lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|" 461proof- 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 467qed 468 469lemma card_of_Plus_assoc: 470fixes A :: "'a set" and B :: "'b set" and C :: "'c set" 471shows "|(A <+> B) <+> C| =o |A <+> B <+> C|" 472proof - 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 509qed 510 511lemma card_of_Plus_mono1: 512assumes "|A| \<le>o |B|" 513shows "|A <+> C| \<le>o |B <+> C|" 514proof- 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 533qed 534 535corollary ordLeq_Plus_mono1: 536assumes "r \<le>o r'" 537shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|" 538using assms card_of_mono2 card_of_Plus_mono1 by blast 539 540lemma card_of_Plus_mono2: 541assumes "|A| \<le>o |B|" 542shows "|C <+> A| \<le>o |C <+> B|" 543using 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|"] 546by blast 547 548corollary ordLeq_Plus_mono2: 549assumes "r \<le>o r'" 550shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|" 551using assms card_of_mono2 card_of_Plus_mono2 by blast 552 553lemma card_of_Plus_mono: 554assumes "|A| \<le>o |B|" and "|C| \<le>o |D|" 555shows "|A <+> C| \<le>o |B <+> D|" 556using 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 559corollary ordLeq_Plus_mono: 560assumes "r \<le>o r'" and "p \<le>o p'" 561shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|" 562using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast 563 564lemma card_of_Plus_cong1: 565assumes "|A| =o |B|" 566shows "|A <+> C| =o |B <+> C|" 567using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1) 568 569corollary ordIso_Plus_cong1: 570assumes "r =o r'" 571shows "|(Field r) <+> C| =o |(Field r') <+> C|" 572using assms card_of_cong card_of_Plus_cong1 by blast 573 574lemma card_of_Plus_cong2: 575assumes "|A| =o |B|" 576shows "|C <+> A| =o |C <+> B|" 577using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2) 578 579corollary ordIso_Plus_cong2: 580assumes "r =o r'" 581shows "|A <+> (Field r)| =o |A <+> (Field r')|" 582using assms card_of_cong card_of_Plus_cong2 by blast 583 584lemma card_of_Plus_cong: 585assumes "|A| =o |B|" and "|C| =o |D|" 586shows "|A <+> C| =o |B <+> D|" 587using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono) 588 589corollary ordIso_Plus_cong: 590assumes "r =o r'" and "p =o p'" 591shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|" 592using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast 593 594lemma card_of_Un_Plus_ordLeq: 595"|A \<union> B| \<le>o |A <+> B|" 596proof- 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 601qed 602 603lemma card_of_Times1: 604assumes "A \<noteq> {}" 605shows "|B| \<le>o |B \<times> A|" 606proof(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 611qed 612 613lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|" 614proof- 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 619qed 620 621lemma card_of_Times2: 622assumes "A \<noteq> {}" shows "|B| \<le>o |A \<times> B|" 623using assms card_of_Times1[of A B] card_of_Times_commute[of B A] 624 ordLeq_ordIso_trans by blast 625 626corollary Card_order_Times1: 627"\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|" 628using card_of_Times1[of B] card_of_Field_ordIso 629 ordIso_ordLeq_trans ordIso_symmetric by blast 630 631corollary Card_order_Times2: 632"\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|" 633using card_of_Times2[of A] card_of_Field_ordIso 634 ordIso_ordLeq_trans ordIso_symmetric by blast 635 636lemma card_of_Times3: "|A| \<le>o |A \<times> A|" 637using card_of_Times1[of A] 638by(cases "A = {}", simp add: card_of_empty, blast) 639 640lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|" 641proof- 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 669qed 670 671lemma card_of_Times_mono1: 672assumes "|A| \<le>o |B|" 673shows "|A \<times> C| \<le>o |B \<times> C|" 674proof- 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 682qed 683 684corollary ordLeq_Times_mono1: 685assumes "r \<le>o r'" 686shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|" 687using assms card_of_mono2 card_of_Times_mono1 by blast 688 689lemma card_of_Times_mono2: 690assumes "|A| \<le>o |B|" 691shows "|C \<times> A| \<le>o |C \<times> B|" 692using 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|"] 695by blast 696 697corollary ordLeq_Times_mono2: 698assumes "r \<le>o r'" 699shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|" 700using assms card_of_mono2 card_of_Times_mono2 by blast 701 702lemma card_of_Sigma_mono1: 703assumes "\<forall>i \<in> I. |A i| \<le>o |B i|" 704shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|" 705proof- 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 715qed 716 717lemma card_of_UNION_Sigma: 718"|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|" 719using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast 720 721lemma card_of_bool: 722assumes "a1 \<noteq> a2" 723shows "|UNIV::bool set| =o |{a1,a2}|" 724proof- 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 748qed 749 750lemma card_of_Plus_Times_aux: 751assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and 752 LEQ: "|A| \<le>o |B|" 753shows "|A <+> B| \<le>o |A \<times> B|" 754proof- 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 772qed 773 774lemma card_of_Plus_Times: 775assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and 776 B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" 777shows "|A <+> B| \<le>o |A \<times> B|" 778proof- 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 793qed 794 795lemma card_of_Times_Plus_distrib: 796 "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|") 797proof - 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 801qed 802 803lemma card_of_ordLeq_finite: 804assumes "|A| \<le>o |B|" and "finite B" 805shows "finite A" 806using assms unfolding ordLeq_def 807using 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 809 810lemma card_of_ordLeq_infinite: 811assumes "|A| \<le>o |B|" and "\<not> finite A" 812shows "\<not> finite B" 813using assms card_of_ordLeq_finite by auto 814 815lemma card_of_ordIso_finite: 816assumes "|A| =o |B|" 817shows "finite A = finite B" 818using assms unfolding ordIso_def iso_def[abs_def] 819by (auto simp: bij_betw_finite Field_card_of) 820 821lemma card_of_ordIso_finite_Field: 822assumes "Card_order r" and "r =o |A|" 823shows "finite(Field r) = finite A" 824using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast 825 826 827subsection \<open>Cardinals versus set operations involving infinite sets\<close> 828 829text\<open>Here we show that, for infinite sets, most set-theoretic constructions 830do not increase the cardinality. The cornerstone for this is 831theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product 832does not increase cardinality -- the proof of this fact adapts a standard 833set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11 834at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close> 835 836lemma infinite_iff_card_of_nat: 837"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )" 838unfolding infinite_iff_countable_subset card_of_ordLeq .. 839 840text\<open>The next two results correspond to the ZF fact that all infinite cardinals are 841limit ordinals:\<close> 842 843lemma Card_order_infinite_not_under: 844assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)" 845shows "\<not> (\<exists>a. Field r = under r a)" 846proof(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 877qed 878 879lemma infinite_Card_order_limit: 880assumes r: "Card_order r" and "\<not>finite (Field r)" 881and a: "a \<in> Field r" 882shows "\<exists>b \<in> Field r. a \<noteq> b \<and> (a,b) \<in> r" 883proof- 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 \<in> Field r \<and> \<not> (b,a) \<in> 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) \<in> 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 898qed 899 900theorem Card_order_Times_same_infinite: 901assumes CO: "Card_order r" and INF: "\<not>finite(Field r)" 902shows "|Field r \<times> Field r| \<le>o r" 903proof- 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 973qed 974 975corollary card_of_Times_same_infinite: 976assumes "\<not>finite A" 977shows "|A \<times> A| =o |A|" 978proof- 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 985qed 986 987lemma card_of_Times_infinite: 988assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|" 989shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|" 990proof- 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) 1001qed 1002 1003corollary Card_order_Times_infinite: 1004assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and 1005 NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r" 1006shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r" 1007proof- 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 1014qed 1015 1016lemma card_of_Sigma_ordLeq_infinite: 1017assumes INF: "\<not>finite B" and 1018 LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|" 1019shows "|SIGMA i : I. A i| \<le>o |B|" 1020proof(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 1027qed 1028 1029lemma card_of_Sigma_ordLeq_infinite_Field: 1030assumes 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" 1032shows "|SIGMA i : I. A i| \<le>o r" 1033proof- 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 1042qed 1043 1044lemma 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" 1047by(simp add: card_of_Sigma_ordLeq_infinite_Field) 1048 1049lemma 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|" 1054by (auto simp add: card_of_Times_infinite ordIso_symmetric) 1055 1056lemma card_of_UNION_ordLeq_infinite: 1057assumes INF: "\<not>finite B" and 1058 LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|" 1059shows "|\<Union>i \<in> I. A i| \<le>o |B|" 1060proof(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 1067qed 1068 1069corollary card_of_UNION_ordLeq_infinite_Field: 1070assumes 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" 1072shows "|\<Union>i \<in> I. A i| \<le>o r" 1073proof- 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 1082qed 1083 1084lemma card_of_Plus_infinite1: 1085assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|" 1086shows "|A <+> B| =o |A|" 1087proof(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 \<circ> ?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 1120qed 1121 1122lemma card_of_Plus_infinite2: 1123assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|" 1124shows "|B <+> A| =o |A|" 1125using assms card_of_Plus_commute card_of_Plus_infinite1 1126ordIso_equivalence by blast 1127 1128lemma card_of_Plus_infinite: 1129assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|" 1130shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|" 1131using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2) 1132 1133corollary Card_order_Plus_infinite: 1134assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and 1135 LEQ: "p \<le>o r" 1136shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r" 1137proof- 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 1145qed 1146 1147 1148subsection \<open>The cardinal $\omega$ and the finite cardinals\<close> 1149 1150text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict 1151order relation on 1152\<open>nat\<close>, that we abbreviate by \<open>natLeq\<close>. The finite cardinals 1153shall be the restrictions of these relations to the numbers smaller than 1154fixed numbers \<open>n\<close>, that we abbreviate by \<open>natLeq_on n\<close>.\<close> 1155 1156definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}" 1157definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}" 1158 1159abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set" 1160where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}" 1161 1162lemma infinite_cartesian_product: 1163assumes "\<not>finite A" "\<not>finite B" 1164shows "\<not>finite (A \<times> B)" 1165proof 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 1170qed 1171 1172 1173subsubsection \<open>First as well-orders\<close> 1174 1175lemma Field_natLeq: "Field natLeq = (UNIV::nat set)" 1176by(unfold Field_def natLeq_def, auto) 1177 1178lemma natLeq_Refl: "Refl natLeq" 1179unfolding refl_on_def Field_def natLeq_def by auto 1180 1181lemma natLeq_trans: "trans natLeq" 1182unfolding trans_def natLeq_def by auto 1183 1184lemma natLeq_Preorder: "Preorder natLeq" 1185unfolding preorder_on_def 1186by (auto simp add: natLeq_Refl natLeq_trans) 1187 1188lemma natLeq_antisym: "antisym natLeq" 1189unfolding antisym_def natLeq_def by auto 1190 1191lemma natLeq_Partial_order: "Partial_order natLeq" 1192unfolding partial_order_on_def 1193by (auto simp add: natLeq_Preorder natLeq_antisym) 1194 1195lemma natLeq_Total: "Total natLeq" 1196unfolding total_on_def natLeq_def by auto 1197 1198lemma natLeq_Linear_order: "Linear_order natLeq" 1199unfolding linear_order_on_def 1200by (auto simp add: natLeq_Partial_order natLeq_Total) 1201 1202lemma natLeq_natLess_Id: "natLess = natLeq - Id" 1203unfolding natLeq_def natLess_def by auto 1204 1205lemma natLeq_Well_order: "Well_order natLeq" 1206unfolding well_order_on_def 1207using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto 1208 1209lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}" 1210unfolding Field_def by auto 1211 1212lemma natLeq_underS_less: "underS natLeq n = {x. x < n}" 1213unfolding underS_def natLeq_def by auto 1214 1215lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n" 1216unfolding natLeq_def by force 1217 1218lemma Restr_natLeq2: 1219"Restr natLeq (underS natLeq n) = natLeq_on n" 1220by (auto simp add: Restr_natLeq natLeq_underS_less) 1221 1222lemma natLeq_on_Well_order: "Well_order(natLeq_on n)" 1223using Restr_natLeq[of n] natLeq_Well_order 1224 Well_order_Restr[of natLeq "{x. x < n}"] by auto 1225 1226corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)" 1227using natLeq_on_Well_order Field_natLeq_on by auto 1228 1229lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)" 1230unfolding wo_rel_def using natLeq_on_Well_order . 1231 1232 1233subsubsection \<open>Then as cardinals\<close> 1234 1235lemma natLeq_Card_order: "Card_order natLeq" 1236proof(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 1244qed 1245 1246corollary card_of_Field_natLeq: 1247"|Field natLeq| =o natLeq" 1248using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq] 1249 ordIso_symmetric[of natLeq] by blast 1250 1251corollary card_of_nat: 1252"|UNIV::nat set| =o natLeq" 1253using Field_natLeq card_of_Field_natLeq by auto 1254 1255corollary infinite_iff_natLeq_ordLeq: 1256"\<not>finite A = ( natLeq \<le>o |A| )" 1257using infinite_iff_card_of_nat[of A] card_of_nat 1258 ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast 1259 1260corollary finite_iff_ordLess_natLeq: 1261"finite A = ( |A| <o natLeq)" 1262using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess 1263 card_of_Well_order natLeq_Well_order by blast 1264 1265 1266subsection \<open>The successor of a cardinal\<close> 1267 1268text\<open>First we define \<open>isCardSuc r r'\<close>, the notion of \<open>r'\<close> 1269being a successor cardinal of \<open>r\<close>. Although the definition does 1270not require \<open>r\<close> to be a cardinal, only this case will be meaningful.\<close> 1271 1272definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool" 1273where 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'')" 1277 1278text\<open>Now we introduce the cardinal-successor operator \<open>cardSuc\<close>, 1279by picking {\em some} cardinal-order relation fulfilling \<open>isCardSuc\<close>. 1280Again, the picked item shall be proved unique up to order-isomorphism.\<close> 1281 1282definition cardSuc :: "'a rel \<Rightarrow> 'a set rel" 1283where 1284"cardSuc r \<equiv> SOME r'. isCardSuc r r'" 1285 1286lemma 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'" 1288unfolding card_order_on_def using exists_minim_Well_order by blast 1289 1290lemma exists_isCardSuc: 1291assumes "Card_order r" 1292shows "\<exists>r'. isCardSuc r r'" 1293proof- 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 1300qed 1301 1302lemma cardSuc_isCardSuc: 1303assumes "Card_order r" 1304shows "isCardSuc r (cardSuc r)" 1305unfolding cardSuc_def using assms 1306by (simp add: exists_isCardSuc someI_ex) 1307 1308lemma cardSuc_Card_order: 1309"Card_order r \<Longrightarrow> Card_order(cardSuc r)" 1310using cardSuc_isCardSuc unfolding isCardSuc_def by blast 1311 1312lemma cardSuc_greater: 1313"Card_order r \<Longrightarrow> r <o cardSuc r" 1314using cardSuc_isCardSuc unfolding isCardSuc_def by blast 1315 1316lemma cardSuc_ordLeq: 1317"Card_order r \<Longrightarrow> r \<le>o cardSuc r" 1318using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast 1319 1320text\<open>The minimality property of \<open>cardSuc\<close> originally present in its definition 1321is local to the type \<open>'a set rel\<close>, i.e., that of \<open>cardSuc r\<close>:\<close> 1322 1323lemma 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'" 1325using cardSuc_isCardSuc unfolding isCardSuc_def by blast 1326 1327text\<open>But from this we can infer general minimality:\<close> 1328 1329lemma cardSuc_least: 1330assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'" 1331shows "cardSuc r \<le>o r'" 1332proof- 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 1346qed 1347 1348lemma cardSuc_ordLess_ordLeq: 1349assumes CARD: "Card_order r" and CARD': "Card_order r'" 1350shows "(r <o r') = (cardSuc r \<le>o r')" 1351proof(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 1354qed 1355 1356lemma cardSuc_ordLeq_ordLess: 1357assumes CARD: "Card_order r" and CARD': "Card_order r'" 1358shows "(r' <o cardSuc r) = (r' \<le>o r)" 1359proof- 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 1367qed 1368 1369lemma cardSuc_mono_ordLeq: 1370assumes CARD: "Card_order r" and CARD': "Card_order r'" 1371shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')" 1372using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast 1373 1374lemma cardSuc_invar_ordIso: 1375assumes CARD: "Card_order r" and CARD': "Card_order r'" 1376shows "(cardSuc r =o cardSuc r') = (r =o r')" 1377proof- 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 1383qed 1384 1385lemma card_of_cardSuc_finite: 1386"finite(Field(cardSuc |A| )) = finite A" 1387proof 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 1395next 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 1403qed 1404 1405lemma cardSuc_finite: 1406assumes "Card_order r" 1407shows "finite (Field (cardSuc r)) = finite (Field r)" 1408proof- 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) 1426qed 1427 1428lemma card_of_Plus_ordLess_infinite: 1429assumes INF: "\<not>finite C" and 1430 LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|" 1431shows "|A <+> B| <o |C|" 1432proof(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 1441next 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 1464qed 1465 1466lemma card_of_Plus_ordLess_infinite_Field: 1467assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and 1468 LESS1: "|A| <o r" and LESS2: "|B| <o r" 1469shows "|A <+> B| <o r" 1470proof- 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 1479qed 1480 1481lemma card_of_Plus_ordLeq_infinite_Field: 1482assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" 1483and c: "Card_order r" 1484shows "|A <+> B| \<le>o r" 1485proof- 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) 1495qed 1496 1497lemma card_of_Un_ordLeq_infinite_Field: 1498assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" 1499and "Card_order r" 1500shows "|A Un B| \<le>o r" 1501using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq 1502ordLeq_transitive by fast 1503 1504 1505subsection \<open>Regular cardinals\<close> 1506 1507definition cofinal where 1508"cofinal A r \<equiv> 1509 \<forall>a \<in> Field r. \<exists>b \<in> A. a \<noteq> b \<and> (a,b) \<in> r" 1510 1511definition regularCard where 1512"regularCard r \<equiv> 1513 \<forall>K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r" 1514 1515definition relChain where 1516"relChain r As \<equiv> 1517 \<forall>i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j" 1518 1519lemma regularCard_UNION: 1520assumes r: "Card_order r" "regularCard r" 1521and As: "relChain r As" 1522and Bsub: "B \<le> (UN i : Field r. As i)" 1523and cardB: "|B| <o r" 1524shows "\<exists>i \<in> Field r. B \<le> As i" 1525proof- 1526 let ?phi = "\<lambda>b j. j \<in> Field r \<and> b \<in> As j" 1527 have "\<forall>b\<in>B. \<exists>j. ?phi b j" using Bsub by blast 1528 then obtain f where f: "\<And>b. b \<in> B \<Longrightarrow> ?phi b (f b)" 1529 using bchoice[of B ?phi] by blast 1530 let ?K = "f ` B" 1531 {assume 1: "\<And>i. i \<in> Field r \<Longrightarrow> \<not> B \<le> As i" 1532 have 2: "cofinal ?K r" 1533 unfolding cofinal_def proof auto 1534 fix i assume i: "i \<in> Field r" 1535 with 1 obtain b where b: "b \<in> B \<and> b \<notin> As i" by blast 1536 hence "i \<noteq> f b \<and> \<not> (f b,i) \<in> r" 1537 using As f unfolding relChain_def by auto 1538 hence "i \<noteq> f b \<and> (i, f b) \<in> 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 1553qed 1554 1555lemma infinite_cardSuc_regularCard: 1556assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r" 1557shows "regularCard (cardSuc r)" 1558proof- 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 "\<forall>j\<in>K. |underS ?r' j| <o ?r'" 1580 using r' 1 by (auto simp: card_of_underS) 1581 hence "\<forall>j\<in>K. |underS ?r' j| \<le>o r" 1582 using r' card_of_Card_order by blast 1583 hence "\<forall>j\<in>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 1604qed 1605 1606lemma cardSuc_UNION: 1607assumes r: "Card_order r" and "\<not>finite (Field r)" 1608and As: "relChain (cardSuc r) As" 1609and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)" 1610and cardB: "|B| <=o r" 1611shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i" 1612proof- 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 1621qed 1622 1623 1624subsection \<open>Others\<close> 1625 1626lemma card_of_Func_Times: 1627"|Func (A \<times> B) C| =o |Func A (Func B C)|" 1628unfolding card_of_ordIso[symmetric] 1629using bij_betw_curr by blast 1630 1631lemma card_of_Pow_Func: 1632"|Pow A| =o |Func A (UNIV::bool set)|" 1633proof- 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 1653qed 1654 1655lemma card_of_Func_UNIV: 1656"|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|" 1657apply(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) 1667qed 1668 1669lemma Func_Times_Range: 1670 "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|") 1671proof - 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 1690qed 1691 1692end 1693