src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 55056 b5c94200d081 parent 55055 3f0dfce0e27a child 55059 ef2e0fb783c6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 18:24:55 2014 +0100
1.3 @@ -0,0 +1,1664 @@
1.4 +(*  Title:      HOL/BNF_Cardinal_Order_Relation.thy
1.5 +    Author:     Andrei Popescu, TU Muenchen
1.7 +
1.8 +Cardinal-order relations (BNF).
1.9 +*)
1.10 +
1.11 +header {* Cardinal-Order Relations (BNF) *}
1.12 +
1.13 +theory BNF_Cardinal_Order_Relation
1.14 +imports BNF_Constructions_on_Wellorders
1.15 +begin
1.16 +
1.17 +text{* In this section, we define cardinal-order relations to be minim well-orders
1.18 +on their field.  Then we define the cardinal of a set to be {\em some} cardinal-order
1.19 +relation on that set, which will be unique up to order isomorphism.  Then we study
1.20 +the connection between cardinals and:
1.21 +\begin{itemize}
1.22 +\item standard set-theoretic constructions: products,
1.23 +sums, unions, lists, powersets, set-of finite sets operator;
1.24 +\item finiteness and infiniteness (in particular, with the numeric cardinal operator
1.25 +for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
1.26 +\end{itemize}
1.27 +%
1.28 +On the way, we define the canonical $\omega$ cardinal and finite cardinals.  We also
1.29 +define (again, up to order isomorphism) the successor of a cardinal, and show that
1.30 +any cardinal admits a successor.
1.31 +
1.32 +Main results of this section are the existence of cardinal relations and the
1.33 +facts that, in the presence of infiniteness,
1.34 +most of the standard set-theoretic constructions (except for the powerset)
1.35 +{\em do not increase cardinality}.  In particular, e.g., the set of words/lists over
1.36 +any infinite set has the same cardinality (hence, is in bijection) with that set.
1.37 +*}
1.38 +
1.39 +
1.40 +subsection {* Cardinal orders *}
1.41 +
1.42 +text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.43 +order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
1.44 +strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.  *}
1.45 +
1.46 +definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.47 +where
1.48 +"card_order_on A r \<equiv> well_order_on A r \<and> (\<forall>r'. well_order_on A r' \<longrightarrow> r \<le>o r')"
1.49 +
1.50 +abbreviation "Card_order r \<equiv> card_order_on (Field r) r"
1.51 +abbreviation "card_order r \<equiv> card_order_on UNIV r"
1.52 +
1.53 +lemma card_order_on_well_order_on:
1.54 +assumes "card_order_on A r"
1.55 +shows "well_order_on A r"
1.56 +using assms unfolding card_order_on_def by simp
1.57 +
1.58 +lemma card_order_on_Card_order:
1.59 +"card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
1.60 +unfolding card_order_on_def using well_order_on_Field by blast
1.61 +
1.62 +text{* The existence of a cardinal relation on any given set (which will mean
1.63 +that any set has a cardinal) follows from two facts:
1.64 +\begin{itemize}
1.65 +\item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
1.66 +which states that on any given set there exists a well-order;
1.67 +\item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
1.68 +such well-order, i.e., a cardinal order.
1.69 +\end{itemize}
1.70 +*}
1.71 +
1.72 +theorem card_order_on: "\<exists>r. card_order_on A r"
1.73 +proof-
1.74 +  obtain R where R_def: "R = {r. well_order_on A r}" by blast
1.75 +  have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
1.76 +  using well_order_on[of A] R_def well_order_on_Well_order by blast
1.77 +  hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
1.78 +  using  exists_minim_Well_order[of R] by auto
1.79 +  thus ?thesis using R_def unfolding card_order_on_def by auto
1.80 +qed
1.81 +
1.82 +lemma card_order_on_ordIso:
1.83 +assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
1.84 +shows "r =o r'"
1.85 +using assms unfolding card_order_on_def
1.86 +using ordIso_iff_ordLeq by blast
1.87 +
1.88 +lemma Card_order_ordIso:
1.89 +assumes CO: "Card_order r" and ISO: "r' =o r"
1.90 +shows "Card_order r'"
1.91 +using ISO unfolding ordIso_def
1.92 +proof(unfold card_order_on_def, auto)
1.93 +  fix p' assume "well_order_on (Field r') p'"
1.94 +  hence 0: "Well_order p' \<and> Field p' = Field r'"
1.95 +  using well_order_on_Well_order by blast
1.96 +  obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
1.97 +  using ISO unfolding ordIso_def by auto
1.98 +  hence 3: "inj_on f (Field r') \<and> f  (Field r') = Field r"
1.99 +  by (auto simp add: iso_iff embed_inj_on)
1.100 +  let ?p = "dir_image p' f"
1.101 +  have 4: "p' =o ?p \<and> Well_order ?p"
1.102 +  using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
1.103 +  moreover have "Field ?p =  Field r"
1.104 +  using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
1.105 +  ultimately have "well_order_on (Field r) ?p" by auto
1.106 +  hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
1.107 +  thus "r' \<le>o p'"
1.108 +  using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
1.109 +qed
1.110 +
1.111 +lemma Card_order_ordIso2:
1.112 +assumes CO: "Card_order r" and ISO: "r =o r'"
1.113 +shows "Card_order r'"
1.114 +using assms Card_order_ordIso ordIso_symmetric by blast
1.115 +
1.116 +
1.117 +subsection {* Cardinal of a set *}
1.118 +
1.119 +text{* We define the cardinal of set to be {\em some} cardinal order on that set.
1.120 +We shall prove that this notion is unique up to order isomorphism, meaning
1.121 +that order isomorphism shall be the true identity of cardinals.  *}
1.122 +
1.123 +definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
1.124 +where "card_of A = (SOME r. card_order_on A r)"
1.125 +
1.126 +lemma card_of_card_order_on: "card_order_on A |A|"
1.127 +unfolding card_of_def by (auto simp add: card_order_on someI_ex)
1.128 +
1.129 +lemma card_of_well_order_on: "well_order_on A |A|"
1.130 +using card_of_card_order_on card_order_on_def by blast
1.131 +
1.132 +lemma Field_card_of: "Field |A| = A"
1.133 +using card_of_card_order_on[of A] unfolding card_order_on_def
1.134 +using well_order_on_Field by blast
1.135 +
1.136 +lemma card_of_Card_order: "Card_order |A|"
1.137 +by (simp only: card_of_card_order_on Field_card_of)
1.138 +
1.139 +corollary ordIso_card_of_imp_Card_order:
1.140 +"r =o |A| \<Longrightarrow> Card_order r"
1.141 +using card_of_Card_order Card_order_ordIso by blast
1.142 +
1.143 +lemma card_of_Well_order: "Well_order |A|"
1.144 +using card_of_Card_order unfolding card_order_on_def by auto
1.145 +
1.146 +lemma card_of_refl: "|A| =o |A|"
1.147 +using card_of_Well_order ordIso_reflexive by blast
1.148 +
1.149 +lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r"
1.150 +using card_of_card_order_on unfolding card_order_on_def by blast
1.151 +
1.152 +lemma card_of_ordIso:
1.153 +"(\<exists>f. bij_betw f A B) = ( |A| =o |B| )"
1.154 +proof(auto)
1.155 +  fix f assume *: "bij_betw f A B"
1.156 +  then obtain r where "well_order_on B r \<and> |A| =o r"
1.157 +  using Well_order_iso_copy card_of_well_order_on by blast
1.158 +  hence "|B| \<le>o |A|" using card_of_least
1.159 +  ordLeq_ordIso_trans ordIso_symmetric by blast
1.160 +  moreover
1.161 +  {let ?g = "inv_into A f"
1.162 +   have "bij_betw ?g B A" using * bij_betw_inv_into by blast
1.163 +   then obtain r where "well_order_on A r \<and> |B| =o r"
1.164 +   using Well_order_iso_copy card_of_well_order_on by blast
1.165 +   hence "|A| \<le>o |B|" using card_of_least
1.166 +   ordLeq_ordIso_trans ordIso_symmetric by blast
1.167 +  }
1.168 +  ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
1.169 +next
1.170 +  assume "|A| =o |B|"
1.171 +  then obtain f where "iso ( |A| ) ( |B| ) f"
1.172 +  unfolding ordIso_def by auto
1.173 +  hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
1.174 +  thus "\<exists>f. bij_betw f A B" by auto
1.175 +qed
1.176 +
1.177 +lemma card_of_ordLeq:
1.178 +"(\<exists>f. inj_on f A \<and> f  A \<le> B) = ( |A| \<le>o |B| )"
1.179 +proof(auto)
1.180 +  fix f assume *: "inj_on f A" and **: "f  A \<le> B"
1.181 +  {assume "|B| <o |A|"
1.182 +   hence "|B| \<le>o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
1.183 +   then obtain g where "embed ( |B| ) ( |A| ) g"
1.184 +   unfolding ordLeq_def by auto
1.185 +   hence 1: "inj_on g B \<and> g  B \<le> A" using embed_inj_on[of "|B|" "|A|" "g"]
1.186 +   card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
1.187 +   embed_Field[of "|B|" "|A|" g] by auto
1.188 +   obtain h where "bij_betw h A B"
1.189 +   using * ** 1 Cantor_Bernstein[of f] by fastforce
1.190 +   hence "|A| =o |B|" using card_of_ordIso by blast
1.191 +   hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
1.192 +  }
1.193 +  thus "|A| \<le>o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
1.194 +  by (auto simp: card_of_Well_order)
1.195 +next
1.196 +  assume *: "|A| \<le>o |B|"
1.197 +  obtain f where "embed ( |A| ) ( |B| ) f"
1.198 +  using * unfolding ordLeq_def by auto
1.199 +  hence "inj_on f A \<and> f  A \<le> B" using embed_inj_on[of "|A|" "|B|" f]
1.200 +  card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"]
1.201 +  embed_Field[of "|A|" "|B|" f] by auto
1.202 +  thus "\<exists>f. inj_on f A \<and> f  A \<le> B" by auto
1.203 +qed
1.204 +
1.205 +lemma card_of_ordLeq2:
1.206 +"A \<noteq> {} \<Longrightarrow> (\<exists>g. g  B = A) = ( |A| \<le>o |B| )"
1.207 +using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
1.208 +
1.209 +lemma card_of_ordLess:
1.210 +"(\<not>(\<exists>f. inj_on f A \<and> f  A \<le> B)) = ( |B| <o |A| )"
1.211 +proof-
1.212 +  have "(\<not>(\<exists>f. inj_on f A \<and> f  A \<le> B)) = (\<not> |A| \<le>o |B| )"
1.213 +  using card_of_ordLeq by blast
1.214 +  also have "\<dots> = ( |B| <o |A| )"
1.215 +  using card_of_Well_order[of A] card_of_Well_order[of B]
1.216 +        not_ordLeq_iff_ordLess by blast
1.217 +  finally show ?thesis .
1.218 +qed
1.219 +
1.220 +lemma card_of_ordLess2:
1.221 +"B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f  A = B)) = ( |A| <o |B| )"
1.222 +using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
1.223 +
1.224 +lemma card_of_ordIsoI:
1.225 +assumes "bij_betw f A B"
1.226 +shows "|A| =o |B|"
1.227 +using assms unfolding card_of_ordIso[symmetric] by auto
1.228 +
1.229 +lemma card_of_ordLeqI:
1.230 +assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B"
1.231 +shows "|A| \<le>o |B|"
1.232 +using assms unfolding card_of_ordLeq[symmetric] by auto
1.233 +
1.234 +lemma card_of_unique:
1.235 +"card_order_on A r \<Longrightarrow> r =o |A|"
1.236 +by (simp only: card_order_on_ordIso card_of_card_order_on)
1.237 +
1.238 +lemma card_of_mono1:
1.239 +"A \<le> B \<Longrightarrow> |A| \<le>o |B|"
1.240 +using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
1.241 +
1.242 +lemma card_of_mono2:
1.243 +assumes "r \<le>o r'"
1.244 +shows "|Field r| \<le>o |Field r'|"
1.245 +proof-
1.246 +  obtain f where
1.247 +  1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
1.248 +  using assms unfolding ordLeq_def
1.249 +  by (auto simp add: well_order_on_Well_order)
1.250 +  hence "inj_on f (Field r) \<and> f  (Field r) \<le> Field r'"
1.251 +  by (auto simp add: embed_inj_on embed_Field)
1.252 +  thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
1.253 +qed
1.254 +
1.255 +lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|"
1.256 +by (simp add: ordIso_iff_ordLeq card_of_mono2)
1.257 +
1.258 +lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
1.259 +using card_of_least card_of_well_order_on well_order_on_Well_order by blast
1.260 +
1.261 +lemma card_of_Field_ordIso:
1.262 +assumes "Card_order r"
1.263 +shows "|Field r| =o r"
1.264 +proof-
1.265 +  have "card_order_on (Field r) r"
1.266 +  using assms card_order_on_Card_order by blast
1.267 +  moreover have "card_order_on (Field r) |Field r|"
1.268 +  using card_of_card_order_on by blast
1.269 +  ultimately show ?thesis using card_order_on_ordIso by blast
1.270 +qed
1.271 +
1.272 +lemma Card_order_iff_ordIso_card_of:
1.273 +"Card_order r = (r =o |Field r| )"
1.274 +using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
1.275 +
1.276 +lemma Card_order_iff_ordLeq_card_of:
1.277 +"Card_order r = (r \<le>o |Field r| )"
1.278 +proof-
1.279 +  have "Card_order r = (r =o |Field r| )"
1.280 +  unfolding Card_order_iff_ordIso_card_of by simp
1.281 +  also have "... = (r \<le>o |Field r| \<and> |Field r| \<le>o r)"
1.282 +  unfolding ordIso_iff_ordLeq by simp
1.283 +  also have "... = (r \<le>o |Field r| )"
1.284 +  using card_of_Field_ordLess
1.285 +  by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp)
1.286 +  finally show ?thesis .
1.287 +qed
1.288 +
1.289 +lemma Card_order_iff_Restr_underS:
1.290 +assumes "Well_order r"
1.291 +shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )"
1.292 +using assms unfolding Card_order_iff_ordLeq_card_of
1.293 +using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
1.294 +
1.295 +lemma card_of_underS:
1.296 +assumes r: "Card_order r" and a: "a : Field r"
1.297 +shows "|underS r a| <o r"
1.298 +proof-
1.299 +  let ?A = "underS r a"  let ?r' = "Restr r ?A"
1.300 +  have 1: "Well_order r"
1.301 +  using r unfolding card_order_on_def by simp
1.302 +  have "Well_order ?r'" using 1 Well_order_Restr by auto
1.303 +  moreover have "card_order_on (Field ?r') |Field ?r'|"
1.304 +  using card_of_card_order_on .
1.305 +  ultimately have "|Field ?r'| \<le>o ?r'"
1.306 +  unfolding card_order_on_def by simp
1.307 +  moreover have "Field ?r' = ?A"
1.308 +  using 1 wo_rel.underS_ofilter Field_Restr_ofilter
1.309 +  unfolding wo_rel_def by fastforce
1.310 +  ultimately have "|?A| \<le>o ?r'" by simp
1.311 +  also have "?r' <o |Field r|"
1.312 +  using 1 a r Card_order_iff_Restr_underS by blast
1.313 +  also have "|Field r| =o r"
1.314 +  using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
1.315 +  finally show ?thesis .
1.316 +qed
1.317 +
1.318 +lemma ordLess_Field:
1.319 +assumes "r <o r'"
1.320 +shows "|Field r| <o r'"
1.321 +proof-
1.322 +  have "well_order_on (Field r) r" using assms unfolding ordLess_def
1.323 +  by (auto simp add: well_order_on_Well_order)
1.324 +  hence "|Field r| \<le>o r" using card_of_least by blast
1.325 +  thus ?thesis using assms ordLeq_ordLess_trans by blast
1.326 +qed
1.327 +
1.328 +lemma internalize_card_of_ordLeq:
1.329 +"( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)"
1.330 +proof
1.331 +  assume "|A| \<le>o r"
1.332 +  then obtain p where 1: "Field p \<le> Field r \<and> |A| =o p \<and> p \<le>o r"
1.333 +  using internalize_ordLeq[of "|A|" r] by blast
1.334 +  hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
1.335 +  hence "|Field p| =o p" using card_of_Field_ordIso by blast
1.336 +  hence "|A| =o |Field p| \<and> |Field p| \<le>o r"
1.337 +  using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
1.338 +  thus "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" using 1 by blast
1.339 +next
1.340 +  assume "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r"
1.341 +  thus "|A| \<le>o r" using ordIso_ordLeq_trans by blast
1.342 +qed
1.343 +
1.344 +lemma internalize_card_of_ordLeq2:
1.345 +"( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )"
1.346 +using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
1.347 +
1.348 +
1.349 +subsection {* Cardinals versus set operations on arbitrary sets *}
1.350 +
1.351 +text{* Here we embark in a long journey of simple results showing
1.352 +that the standard set-theoretic operations are well-behaved w.r.t. the notion of
1.353 +cardinal -- essentially, this means that they preserve the cardinal identity"
1.354 +@{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
1.355 +*}
1.356 +
1.357 +lemma card_of_empty: "|{}| \<le>o |A|"
1.358 +using card_of_ordLeq inj_on_id by blast
1.359 +
1.360 +lemma card_of_empty1:
1.361 +assumes "Well_order r \<or> Card_order r"
1.362 +shows "|{}| \<le>o r"
1.363 +proof-
1.364 +  have "Well_order r" using assms unfolding card_order_on_def by auto
1.365 +  hence "|Field r| <=o r"
1.366 +  using assms card_of_Field_ordLess by blast
1.367 +  moreover have "|{}| \<le>o |Field r|" by (simp add: card_of_empty)
1.368 +  ultimately show ?thesis using ordLeq_transitive by blast
1.369 +qed
1.370 +
1.371 +corollary Card_order_empty:
1.372 +"Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1)
1.373 +
1.374 +lemma card_of_empty2:
1.375 +assumes LEQ: "|A| =o |{}|"
1.376 +shows "A = {}"
1.377 +using assms card_of_ordIso[of A] bij_betw_empty2 by blast
1.378 +
1.379 +lemma card_of_empty3:
1.380 +assumes LEQ: "|A| \<le>o |{}|"
1.381 +shows "A = {}"
1.382 +using assms
1.383 +by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
1.384 +              ordLeq_Well_order_simp)
1.385 +
1.386 +lemma card_of_empty_ordIso:
1.387 +"|{}::'a set| =o |{}::'b set|"
1.388 +using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
1.389 +
1.390 +lemma card_of_image:
1.391 +"|f  A| <=o |A|"
1.392 +proof(cases "A = {}", simp add: card_of_empty)
1.393 +  assume "A ~= {}"
1.394 +  hence "f  A ~= {}" by auto
1.395 +  thus "|f  A| \<le>o |A|"
1.396 +  using card_of_ordLeq2[of "f  A" A] by auto
1.397 +qed
1.398 +
1.399 +lemma surj_imp_ordLeq:
1.400 +assumes "B <= f  A"
1.401 +shows "|B| <=o |A|"
1.402 +proof-
1.403 +  have "|B| <=o |f  A|" using assms card_of_mono1 by auto
1.404 +  thus ?thesis using card_of_image ordLeq_transitive by blast
1.405 +qed
1.406 +
1.407 +lemma card_of_ordLeqI2:
1.408 +assumes "B \<subseteq> f  A"
1.409 +shows "|B| \<le>o |A|"
1.410 +using assms by (metis surj_imp_ordLeq)
1.411 +
1.412 +lemma card_of_singl_ordLeq:
1.413 +assumes "A \<noteq> {}"
1.414 +shows "|{b}| \<le>o |A|"
1.415 +proof-
1.416 +  obtain a where *: "a \<in> A" using assms by auto
1.417 +  let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
1.418 +  have "inj_on ?h {b} \<and> ?h  {b} \<le> A"
1.419 +  using * unfolding inj_on_def by auto
1.420 +  thus ?thesis using card_of_ordLeq by fast
1.421 +qed
1.422 +
1.423 +corollary Card_order_singl_ordLeq:
1.424 +"\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r"
1.425 +using card_of_singl_ordLeq[of "Field r" b]
1.426 +      card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
1.427 +
1.428 +lemma card_of_Pow: "|A| <o |Pow A|"
1.429 +using card_of_ordLess2[of "Pow A" A]  Cantors_paradox[of A]
1.430 +      Pow_not_empty[of A] by auto
1.431 +
1.432 +corollary Card_order_Pow:
1.433 +"Card_order r \<Longrightarrow> r <o |Pow(Field r)|"
1.434 +using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
1.435 +
1.436 +lemma card_of_Plus1: "|A| \<le>o |A <+> B|"
1.437 +proof-
1.438 +  have "Inl  A \<le> A <+> B" by auto
1.439 +  thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast
1.440 +qed
1.441 +
1.442 +corollary Card_order_Plus1:
1.443 +"Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|"
1.444 +using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
1.445 +
1.446 +lemma card_of_Plus2: "|B| \<le>o |A <+> B|"
1.447 +proof-
1.448 +  have "Inr  B \<le> A <+> B" by auto
1.449 +  thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast
1.450 +qed
1.451 +
1.452 +corollary Card_order_Plus2:
1.453 +"Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|"
1.454 +using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
1.455 +
1.456 +lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
1.457 +proof-
1.458 +  have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
1.459 +  thus ?thesis using card_of_ordIso by auto
1.460 +qed
1.461 +
1.462 +lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
1.463 +proof-
1.464 +  have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
1.465 +  thus ?thesis using card_of_ordIso by auto
1.466 +qed
1.467 +
1.468 +lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
1.469 +proof-
1.470 +  let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a
1.471 +                                   | Inr b \<Rightarrow> Inl b"
1.472 +  have "bij_betw ?f (A <+> B) (B <+> A)"
1.473 +  unfolding bij_betw_def inj_on_def by force
1.474 +  thus ?thesis using card_of_ordIso by blast
1.475 +qed
1.476 +
1.477 +lemma card_of_Plus_assoc:
1.478 +fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
1.479 +shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
1.480 +proof -
1.481 +  def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).
1.482 +  case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a
1.483 +                                 |Inr b \<Rightarrow> Inr (Inl b))
1.484 +           |Inr c \<Rightarrow> Inr (Inr c)"
1.485 +  have "A <+> B <+> C \<subseteq> f  ((A <+> B) <+> C)"
1.486 +  proof
1.487 +    fix x assume x: "x \<in> A <+> B <+> C"
1.488 +    show "x \<in> f  ((A <+> B) <+> C)"
1.489 +    proof(cases x)
1.490 +      case (Inl a)
1.491 +      hence "a \<in> A" "x = f (Inl (Inl a))"
1.492 +      using x unfolding f_def by auto
1.493 +      thus ?thesis by auto
1.494 +    next
1.495 +      case (Inr bc) note 1 = Inr show ?thesis
1.496 +      proof(cases bc)
1.497 +        case (Inl b)
1.498 +        hence "b \<in> B" "x = f (Inl (Inr b))"
1.499 +        using x 1 unfolding f_def by auto
1.500 +        thus ?thesis by auto
1.501 +      next
1.502 +        case (Inr c)
1.503 +        hence "c \<in> C" "x = f (Inr c)"
1.504 +        using x 1 unfolding f_def by auto
1.505 +        thus ?thesis by auto
1.506 +      qed
1.507 +    qed
1.508 +  qed
1.509 +  hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
1.510 +  unfolding bij_betw_def inj_on_def f_def by fastforce
1.511 +  thus ?thesis using card_of_ordIso by blast
1.512 +qed
1.513 +
1.514 +lemma card_of_Plus_mono1:
1.515 +assumes "|A| \<le>o |B|"
1.516 +shows "|A <+> C| \<le>o |B <+> C|"
1.517 +proof-
1.518 +  obtain f where 1: "inj_on f A \<and> f  A \<le> B"
1.519 +  using assms card_of_ordLeq[of A] by fastforce
1.520 +  obtain g where g_def:
1.521 +  "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast
1.522 +  have "inj_on g (A <+> C) \<and> g  (A <+> C) \<le> (B <+> C)"
1.523 +  proof-
1.524 +    {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and
1.525 +                          "g d1 = g d2"
1.526 +     hence "d1 = d2" using 1 unfolding inj_on_def g_def by force
1.527 +    }
1.528 +    moreover
1.529 +    {fix d assume "d \<in> A <+> C"
1.530 +     hence "g d \<in> B <+> C"  using 1
1.531 +     by(case_tac d, auto simp add: g_def)
1.532 +    }
1.533 +    ultimately show ?thesis unfolding inj_on_def by auto
1.534 +  qed
1.535 +  thus ?thesis using card_of_ordLeq by metis
1.536 +qed
1.537 +
1.538 +corollary ordLeq_Plus_mono1:
1.539 +assumes "r \<le>o r'"
1.540 +shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|"
1.541 +using assms card_of_mono2 card_of_Plus_mono1 by blast
1.542 +
1.543 +lemma card_of_Plus_mono2:
1.544 +assumes "|A| \<le>o |B|"
1.545 +shows "|C <+> A| \<le>o |C <+> B|"
1.546 +using assms card_of_Plus_mono1[of A B C]
1.547 +      card_of_Plus_commute[of C A]  card_of_Plus_commute[of B C]
1.548 +      ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]
1.549 +by blast
1.550 +
1.551 +corollary ordLeq_Plus_mono2:
1.552 +assumes "r \<le>o r'"
1.553 +shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|"
1.554 +using assms card_of_mono2 card_of_Plus_mono2 by blast
1.555 +
1.556 +lemma card_of_Plus_mono:
1.557 +assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
1.558 +shows "|A <+> C| \<le>o |B <+> D|"
1.559 +using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
1.560 +      ordLeq_transitive[of "|A <+> C|"] by blast
1.561 +
1.562 +corollary ordLeq_Plus_mono:
1.563 +assumes "r \<le>o r'" and "p \<le>o p'"
1.564 +shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|"
1.565 +using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
1.566 +
1.567 +lemma card_of_Plus_cong1:
1.568 +assumes "|A| =o |B|"
1.569 +shows "|A <+> C| =o |B <+> C|"
1.570 +using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
1.571 +
1.572 +corollary ordIso_Plus_cong1:
1.573 +assumes "r =o r'"
1.574 +shows "|(Field r) <+> C| =o |(Field r') <+> C|"
1.575 +using assms card_of_cong card_of_Plus_cong1 by blast
1.576 +
1.577 +lemma card_of_Plus_cong2:
1.578 +assumes "|A| =o |B|"
1.579 +shows "|C <+> A| =o |C <+> B|"
1.580 +using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
1.581 +
1.582 +corollary ordIso_Plus_cong2:
1.583 +assumes "r =o r'"
1.584 +shows "|A <+> (Field r)| =o |A <+> (Field r')|"
1.585 +using assms card_of_cong card_of_Plus_cong2 by blast
1.586 +
1.587 +lemma card_of_Plus_cong:
1.588 +assumes "|A| =o |B|" and "|C| =o |D|"
1.589 +shows "|A <+> C| =o |B <+> D|"
1.590 +using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
1.591 +
1.592 +corollary ordIso_Plus_cong:
1.593 +assumes "r =o r'" and "p =o p'"
1.594 +shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
1.595 +using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
1.596 +
1.597 +lemma card_of_Un_Plus_ordLeq:
1.598 +"|A \<union> B| \<le>o |A <+> B|"
1.599 +proof-
1.600 +   let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
1.601 +   have "inj_on ?f (A \<union> B) \<and> ?f  (A \<union> B) \<le> A <+> B"
1.602 +   unfolding inj_on_def by auto
1.603 +   thus ?thesis using card_of_ordLeq by blast
1.604 +qed
1.605 +
1.606 +lemma card_of_Times1:
1.607 +assumes "A \<noteq> {}"
1.608 +shows "|B| \<le>o |B \<times> A|"
1.609 +proof(cases "B = {}", simp add: card_of_empty)
1.610 +  assume *: "B \<noteq> {}"
1.611 +  have "fst (B \<times> A) = B" unfolding image_def using assms by auto
1.612 +  thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
1.613 +                     card_of_ordLeq[of B "B \<times> A"] * by blast
1.614 +qed
1.615 +
1.616 +lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|"
1.617 +proof-
1.618 +  let ?f = "\<lambda>(a::'a,b::'b). (b,a)"
1.619 +  have "bij_betw ?f (A \<times> B) (B \<times> A)"
1.620 +  unfolding bij_betw_def inj_on_def by auto
1.621 +  thus ?thesis using card_of_ordIso by blast
1.622 +qed
1.623 +
1.624 +lemma card_of_Times2:
1.625 +assumes "A \<noteq> {}"   shows "|B| \<le>o |A \<times> B|"
1.626 +using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
1.627 +      ordLeq_ordIso_trans by blast
1.628 +
1.629 +corollary Card_order_Times1:
1.630 +"\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|"
1.631 +using card_of_Times1[of B] card_of_Field_ordIso
1.632 +      ordIso_ordLeq_trans ordIso_symmetric by blast
1.633 +
1.634 +corollary Card_order_Times2:
1.635 +"\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|"
1.636 +using card_of_Times2[of A] card_of_Field_ordIso
1.637 +      ordIso_ordLeq_trans ordIso_symmetric by blast
1.638 +
1.639 +lemma card_of_Times3: "|A| \<le>o |A \<times> A|"
1.640 +using card_of_Times1[of A]
1.641 +by(cases "A = {}", simp add: card_of_empty, blast)
1.642 +
1.643 +lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|"
1.644 +proof-
1.645 +  let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True)
1.646 +                                  |Inr a \<Rightarrow> (a,False)"
1.647 +  have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))"
1.648 +  proof-
1.649 +    {fix  c1 and c2 assume "?f c1 = ?f c2"
1.650 +     hence "c1 = c2"
1.651 +     by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
1.652 +    }
1.653 +    moreover
1.654 +    {fix c assume "c \<in> A <+> A"
1.655 +     hence "?f c \<in> A \<times> (UNIV::bool set)"
1.656 +     by(case_tac c, auto)
1.657 +    }
1.658 +    moreover
1.659 +    {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
1.660 +     have "(a,bl) \<in> ?f  ( A <+> A)"
1.661 +     proof(cases bl)
1.662 +       assume bl hence "?f(Inl a) = (a,bl)" by auto
1.663 +       thus ?thesis using * by force
1.664 +     next
1.665 +       assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto
1.666 +       thus ?thesis using * by force
1.667 +     qed
1.668 +    }
1.669 +    ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
1.670 +  qed
1.671 +  thus ?thesis using card_of_ordIso by blast
1.672 +qed
1.673 +
1.674 +lemma card_of_Times_mono1:
1.675 +assumes "|A| \<le>o |B|"
1.676 +shows "|A \<times> C| \<le>o |B \<times> C|"
1.677 +proof-
1.678 +  obtain f where 1: "inj_on f A \<and> f  A \<le> B"
1.679 +  using assms card_of_ordLeq[of A] by fastforce
1.680 +  obtain g where g_def:
1.681 +  "g = (\<lambda>(a,c::'c). (f a,c))" by blast
1.682 +  have "inj_on g (A \<times> C) \<and> g  (A \<times> C) \<le> (B \<times> C)"
1.683 +  using 1 unfolding inj_on_def using g_def by auto
1.684 +  thus ?thesis using card_of_ordLeq by metis
1.685 +qed
1.686 +
1.687 +corollary ordLeq_Times_mono1:
1.688 +assumes "r \<le>o r'"
1.689 +shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|"
1.690 +using assms card_of_mono2 card_of_Times_mono1 by blast
1.691 +
1.692 +lemma card_of_Times_mono2:
1.693 +assumes "|A| \<le>o |B|"
1.694 +shows "|C \<times> A| \<le>o |C \<times> B|"
1.695 +using assms card_of_Times_mono1[of A B C]
1.696 +      card_of_Times_commute[of C A]  card_of_Times_commute[of B C]
1.697 +      ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"]
1.698 +by blast
1.699 +
1.700 +corollary ordLeq_Times_mono2:
1.701 +assumes "r \<le>o r'"
1.702 +shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|"
1.703 +using assms card_of_mono2 card_of_Times_mono2 by blast
1.704 +
1.705 +lemma card_of_Sigma_mono1:
1.706 +assumes "\<forall>i \<in> I. |A i| \<le>o |B i|"
1.707 +shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|"
1.708 +proof-
1.709 +  have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f  (A i) \<le> B i)"
1.710 +  using assms by (auto simp add: card_of_ordLeq)
1.711 +  with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f  (A i) \<le> B i"]
1.712 +  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i)  (A i) \<le> B i" by metis
1.713 +  obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
1.714 +  have "inj_on g (Sigma I A) \<and> g  (Sigma I A) \<le> (Sigma I B)"
1.715 +  using 1 unfolding inj_on_def using g_def by force
1.716 +  thus ?thesis using card_of_ordLeq by metis
1.717 +qed
1.718 +
1.719 +corollary card_of_Sigma_Times:
1.720 +"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
1.721 +using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
1.722 +
1.723 +lemma card_of_UNION_Sigma:
1.724 +"|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
1.725 +using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis
1.726 +
1.727 +lemma card_of_bool:
1.728 +assumes "a1 \<noteq> a2"
1.729 +shows "|UNIV::bool set| =o |{a1,a2}|"
1.730 +proof-
1.731 +  let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"
1.732 +  have "bij_betw ?f UNIV {a1,a2}"
1.733 +  proof-
1.734 +    {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"
1.735 +     hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
1.736 +    }
1.737 +    moreover
1.738 +    {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
1.739 +    }
1.740 +    moreover
1.741 +    {fix a assume *: "a \<in> {a1,a2}"
1.742 +     have "a \<in> ?f  UNIV"
1.743 +     proof(cases "a = a1")
1.744 +       assume "a = a1"
1.745 +       hence "?f True = a" by auto  thus ?thesis by blast
1.746 +     next
1.747 +       assume "a \<noteq> a1" hence "a = a2" using * by auto
1.748 +       hence "?f False = a" by auto  thus ?thesis by blast
1.749 +     qed
1.750 +    }
1.751 +    ultimately show ?thesis unfolding bij_betw_def inj_on_def
1.752 +    by (metis image_subsetI order_eq_iff subsetI)
1.753 +  qed
1.754 +  thus ?thesis using card_of_ordIso by blast
1.755 +qed
1.756 +
1.757 +lemma card_of_Plus_Times_aux:
1.758 +assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
1.759 +        LEQ: "|A| \<le>o |B|"
1.760 +shows "|A <+> B| \<le>o |A \<times> B|"
1.761 +proof-
1.762 +  have 1: "|UNIV::bool set| \<le>o |A|"
1.763 +  using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
1.764 +        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis
1.765 +  (*  *)
1.766 +  have "|A <+> B| \<le>o |B <+> B|"
1.767 +  using LEQ card_of_Plus_mono1 by blast
1.768 +  moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"
1.769 +  using card_of_Plus_Times_bool by blast
1.770 +  moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"
1.771 +  using 1 by (simp add: card_of_Times_mono2)
1.772 +  moreover have " |B \<times> A| =o |A \<times> B|"
1.773 +  using card_of_Times_commute by blast
1.774 +  ultimately show "|A <+> B| \<le>o |A \<times> B|"
1.775 +  using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]
1.776 +        ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]
1.777 +        ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]
1.778 +  by blast
1.779 +qed
1.780 +
1.781 +lemma card_of_Plus_Times:
1.782 +assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
1.783 +        B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
1.784 +shows "|A <+> B| \<le>o |A \<times> B|"
1.785 +proof-
1.786 +  {assume "|A| \<le>o |B|"
1.787 +   hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
1.788 +  }
1.789 +  moreover
1.790 +  {assume "|B| \<le>o |A|"
1.791 +   hence "|B <+> A| \<le>o |B \<times> A|"
1.792 +   using assms by (auto simp add: card_of_Plus_Times_aux)
1.793 +   hence ?thesis
1.794 +   using card_of_Plus_commute card_of_Times_commute
1.795 +         ordIso_ordLeq_trans ordLeq_ordIso_trans by metis
1.796 +  }
1.797 +  ultimately show ?thesis
1.798 +  using card_of_Well_order[of A] card_of_Well_order[of B]
1.799 +        ordLeq_total[of "|A|"] by metis
1.800 +qed
1.801 +
1.802 +lemma card_of_ordLeq_finite:
1.803 +assumes "|A| \<le>o |B|" and "finite B"
1.804 +shows "finite A"
1.805 +using assms unfolding ordLeq_def
1.806 +using embed_inj_on[of "|A|" "|B|"]  embed_Field[of "|A|" "|B|"]
1.807 +      Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
1.808 +
1.809 +lemma card_of_ordLeq_infinite:
1.810 +assumes "|A| \<le>o |B|" and "\<not> finite A"
1.811 +shows "\<not> finite B"
1.812 +using assms card_of_ordLeq_finite by auto
1.813 +
1.814 +lemma card_of_ordIso_finite:
1.815 +assumes "|A| =o |B|"
1.816 +shows "finite A = finite B"
1.817 +using assms unfolding ordIso_def iso_def[abs_def]
1.818 +by (auto simp: bij_betw_finite Field_card_of)
1.819 +
1.820 +lemma card_of_ordIso_finite_Field:
1.821 +assumes "Card_order r" and "r =o |A|"
1.822 +shows "finite(Field r) = finite A"
1.823 +using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
1.824 +
1.825 +
1.826 +subsection {* Cardinals versus set operations involving infinite sets *}
1.827 +
1.828 +text{* Here we show that, for infinite sets, most set-theoretic constructions
1.829 +do not increase the cardinality.  The cornerstone for this is
1.830 +theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
1.831 +does not increase cardinality -- the proof of this fact adapts a standard
1.832 +set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
1.833 +at page 47 in \cite{card-book}. Then everything else follows fairly easily.  *}
1.834 +
1.835 +lemma infinite_iff_card_of_nat:
1.836 +"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
1.837 +unfolding infinite_iff_countable_subset card_of_ordLeq ..
1.838 +
1.839 +text{* The next two results correspond to the ZF fact that all infinite cardinals are
1.840 +limit ordinals: *}
1.841 +
1.842 +lemma Card_order_infinite_not_under:
1.843 +assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
1.844 +shows "\<not> (\<exists>a. Field r = under r a)"
1.845 +proof(auto)
1.846 +  have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
1.847 +  using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
1.848 +  fix a assume *: "Field r = under r a"
1.849 +  show False
1.850 +  proof(cases "a \<in> Field r")
1.851 +    assume Case1: "a \<notin> Field r"
1.852 +    hence "under r a = {}" unfolding Field_def under_def by auto
1.853 +    thus False using INF *  by auto
1.854 +  next
1.855 +    let ?r' = "Restr r (underS r a)"
1.856 +    assume Case2: "a \<in> Field r"
1.857 +    hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
1.858 +    using 0 Refl_under_underS underS_notIn by metis
1.859 +    have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
1.860 +    using 0 wo_rel.underS_ofilter * 1 Case2 by fast
1.861 +    hence "?r' <o r" using 0 using ofilter_ordLess by blast
1.862 +    moreover
1.863 +    have "Field ?r' = underS r a \<and> Well_order ?r'"
1.864 +    using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
1.865 +    ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
1.866 +    moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
1.867 +    ultimately have "|underS r a| <o |under r a|"
1.868 +    using ordIso_symmetric ordLess_ordIso_trans by blast
1.869 +    moreover
1.870 +    {have "\<exists>f. bij_betw f (under r a) (underS r a)"
1.871 +     using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
1.872 +     hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
1.873 +    }
1.874 +    ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
1.875 +  qed
1.876 +qed
1.877 +
1.878 +lemma infinite_Card_order_limit:
1.879 +assumes r: "Card_order r" and "\<not>finite (Field r)"
1.880 +and a: "a : Field r"
1.881 +shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
1.882 +proof-
1.883 +  have "Field r \<noteq> under r a"
1.884 +  using assms Card_order_infinite_not_under by blast
1.885 +  moreover have "under r a \<le> Field r"
1.886 +  using under_Field .
1.887 +  ultimately have "under r a < Field r" by blast
1.888 +  then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
1.889 +  unfolding under_def by blast
1.890 +  moreover have ba: "b \<noteq> a"
1.891 +  using 1 r unfolding card_order_on_def well_order_on_def
1.892 +  linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
1.893 +  ultimately have "(a,b) : r"
1.894 +  using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
1.895 +  total_on_def by blast
1.896 +  thus ?thesis using 1 ba by auto
1.897 +qed
1.898 +
1.899 +theorem Card_order_Times_same_infinite:
1.900 +assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
1.901 +shows "|Field r \<times> Field r| \<le>o r"
1.902 +proof-
1.903 +  obtain phi where phi_def:
1.904 +  "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
1.905 +                      \<not> |Field r \<times> Field r| \<le>o r )" by blast
1.906 +  have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
1.907 +  unfolding phi_def card_order_on_def by auto
1.908 +  have Ft: "\<not>(\<exists>r. phi r)"
1.909 +  proof
1.910 +    assume "\<exists>r. phi r"
1.911 +    hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"
1.912 +    using temp1 by auto
1.913 +    then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and
1.914 +                   3: "Card_order r \<and> Well_order r"
1.915 +    using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
1.916 +    let ?A = "Field r"  let ?r' = "bsqr r"
1.917 +    have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"
1.918 +    using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
1.919 +    have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"
1.920 +    using card_of_Card_order card_of_Well_order by blast
1.921 +    (*  *)
1.922 +    have "r <o |?A \<times> ?A|"
1.923 +    using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
1.924 +    moreover have "|?A \<times> ?A| \<le>o ?r'"
1.925 +    using card_of_least[of "?A \<times> ?A"] 4 by auto
1.926 +    ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
1.927 +    then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"
1.928 +    unfolding ordLess_def embedS_def[abs_def]
1.929 +    by (auto simp add: Field_bsqr)
1.930 +    let ?B = "f  ?A"
1.931 +    have "|?A| =o |?B|"
1.932 +    using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
1.933 +    hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
1.934 +    (*  *)
1.935 +    have "wo_rel.ofilter ?r' ?B"
1.936 +    using 6 embed_Field_ofilter 3 4 by blast
1.937 +    hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"
1.938 +    using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
1.939 +    hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
1.940 +    using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
1.941 +    have "\<not> (\<exists>a. Field r = under r a)"
1.942 +    using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
1.943 +    then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
1.944 +    using temp2 3 bsqr_ofilter[of r ?B] by blast
1.945 +    hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast
1.946 +    hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast
1.947 +    let ?r1 = "Restr r A1"
1.948 +    have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
1.949 +    moreover
1.950 +    {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
1.951 +     hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast
1.952 +    }
1.953 +    ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
1.954 +    (*  *)
1.955 +    have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
1.956 +    hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
1.957 +    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
1.958 +    moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
1.959 +    using card_of_Card_order[of A1] card_of_Well_order[of A1]
1.960 +    by (simp add: Field_card_of)
1.961 +    moreover have "\<not> r \<le>o | A1 |"
1.962 +    using temp4 11 3 using not_ordLeq_iff_ordLess by blast
1.963 +    ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
1.964 +    by (simp add: card_of_card_order_on)
1.965 +    hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
1.966 +    using 2 unfolding phi_def by blast
1.967 +    hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto
1.968 +    hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast
1.969 +    thus False using 11 not_ordLess_ordLeq by auto
1.970 +  qed
1.971 +  thus ?thesis using assms unfolding phi_def by blast
1.972 +qed
1.973 +
1.974 +corollary card_of_Times_same_infinite:
1.975 +assumes "\<not>finite A"
1.976 +shows "|A \<times> A| =o |A|"
1.977 +proof-
1.978 +  let ?r = "|A|"
1.979 +  have "Field ?r = A \<and> Card_order ?r"
1.980 +  using Field_card_of card_of_Card_order[of A] by fastforce
1.981 +  hence "|A \<times> A| \<le>o |A|"
1.982 +  using Card_order_Times_same_infinite[of ?r] assms by auto
1.983 +  thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
1.984 +qed
1.985 +
1.986 +lemma card_of_Times_infinite:
1.987 +assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
1.988 +shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
1.989 +proof-
1.990 +  have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
1.991 +  using assms by (simp add: card_of_Times1 card_of_Times2)
1.992 +  moreover
1.993 +  {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"
1.994 +   using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
1.995 +   moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast
1.996 +   ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"
1.997 +   using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto
1.998 +  }
1.999 +  ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
1.1000 +qed
1.1001 +
1.1002 +corollary Card_order_Times_infinite:
1.1003 +assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
1.1004 +        NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
1.1005 +shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
1.1006 +proof-
1.1007 +  have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"
1.1008 +  using assms by (simp add: card_of_Times_infinite card_of_mono2)
1.1009 +  thus ?thesis
1.1010 +  using assms card_of_Field_ordIso[of r]
1.1011 +        ordIso_transitive[of "|Field r \<times> Field p|"]
1.1012 +        ordIso_transitive[of _ "|Field r|"] by blast
1.1013 +qed
1.1014 +
1.1015 +lemma card_of_Sigma_ordLeq_infinite:
1.1016 +assumes INF: "\<not>finite B" and
1.1017 +        LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1.1018 +shows "|SIGMA i : I. A i| \<le>o |B|"
1.1019 +proof(cases "I = {}", simp add: card_of_empty)
1.1020 +  assume *: "I \<noteq> {}"
1.1021 +  have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
1.1022 +  using LEQ card_of_Sigma_Times by blast
1.1023 +  moreover have "|I \<times> B| =o |B|"
1.1024 +  using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
1.1025 +  ultimately show ?thesis using ordLeq_ordIso_trans by blast
1.1026 +qed
1.1027 +
1.1028 +lemma card_of_Sigma_ordLeq_infinite_Field:
1.1029 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1.1030 +        LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1.1031 +shows "|SIGMA i : I. A i| \<le>o r"
1.1032 +proof-
1.1033 +  let ?B  = "Field r"
1.1034 +  have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1.1035 +  ordIso_symmetric by blast
1.1036 +  hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
1.1037 +  using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1.1038 +  hence  "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ
1.1039 +  card_of_Sigma_ordLeq_infinite by blast
1.1040 +  thus ?thesis using 1 ordLeq_ordIso_trans by blast
1.1041 +qed
1.1042 +
1.1043 +lemma card_of_Times_ordLeq_infinite_Field:
1.1044 +"\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
1.1045 + \<Longrightarrow> |A <*> B| \<le>o r"
1.1047 +
1.1048 +lemma card_of_Times_infinite_simps:
1.1049 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
1.1050 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
1.1051 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
1.1052 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
1.1053 +by (auto simp add: card_of_Times_infinite ordIso_symmetric)
1.1054 +
1.1055 +lemma card_of_UNION_ordLeq_infinite:
1.1056 +assumes INF: "\<not>finite B" and
1.1057 +        LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1.1058 +shows "|\<Union> i \<in> I. A i| \<le>o |B|"
1.1059 +proof(cases "I = {}", simp add: card_of_empty)
1.1060 +  assume *: "I \<noteq> {}"
1.1061 +  have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
1.1062 +  using card_of_UNION_Sigma by blast
1.1063 +  moreover have "|SIGMA i : I. A i| \<le>o |B|"
1.1064 +  using assms card_of_Sigma_ordLeq_infinite by blast
1.1065 +  ultimately show ?thesis using ordLeq_transitive by blast
1.1066 +qed
1.1067 +
1.1068 +corollary card_of_UNION_ordLeq_infinite_Field:
1.1069 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1.1070 +        LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1.1071 +shows "|\<Union> i \<in> I. A i| \<le>o r"
1.1072 +proof-
1.1073 +  let ?B  = "Field r"
1.1074 +  have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1.1075 +  ordIso_symmetric by blast
1.1076 +  hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
1.1077 +  using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1.1078 +  hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
1.1079 +  card_of_UNION_ordLeq_infinite by blast
1.1080 +  thus ?thesis using 1 ordLeq_ordIso_trans by blast
1.1081 +qed
1.1082 +
1.1083 +lemma card_of_Plus_infinite1:
1.1084 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1.1085 +shows "|A <+> B| =o |A|"
1.1086 +proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
1.1087 +  let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
1.1088 +  assume *: "B \<noteq> {}"
1.1089 +  then obtain b1 where 1: "b1 \<in> B" by blast
1.1090 +  show ?thesis
1.1091 +  proof(cases "B = {b1}")
1.1092 +    assume Case1: "B = {b1}"
1.1093 +    have 2: "bij_betw ?Inl A ((?Inl  A))"
1.1094 +    unfolding bij_betw_def inj_on_def by auto
1.1095 +    hence 3: "\<not>finite (?Inl  A)"
1.1096 +    using INF bij_betw_finite[of ?Inl A] by blast
1.1097 +    let ?A' = "?Inl  A \<union> {?Inr b1}"
1.1098 +    obtain g where "bij_betw g (?Inl  A) ?A'"
1.1099 +    using 3 infinite_imp_bij_betw2[of "?Inl  A"] by auto
1.1100 +    moreover have "?A' = A <+> B" using Case1 by blast
1.1101 +    ultimately have "bij_betw g (?Inl  A) (A <+> B)" by simp
1.1102 +    hence "bij_betw (g o ?Inl) A (A <+> B)"
1.1103 +    using 2 by (auto simp add: bij_betw_trans)
1.1104 +    thus ?thesis using card_of_ordIso ordIso_symmetric by blast
1.1105 +  next
1.1106 +    assume Case2: "B \<noteq> {b1}"
1.1107 +    with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce
1.1108 +    obtain f where "inj_on f B \<and> f  B \<le> A"
1.1109 +    using LEQ card_of_ordLeq[of B] by fastforce
1.1110 +    with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"
1.1111 +    unfolding inj_on_def by auto
1.1112 +    with 3 have "|A <+> B| \<le>o |A \<times> B|"
1.1113 +    by (auto simp add: card_of_Plus_Times)
1.1114 +    moreover have "|A \<times> B| =o |A|"
1.1115 +    using assms * by (simp add: card_of_Times_infinite_simps)
1.1116 +    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
1.1117 +    thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
1.1118 +  qed
1.1119 +qed
1.1120 +
1.1121 +lemma card_of_Plus_infinite2:
1.1122 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1.1123 +shows "|B <+> A| =o |A|"
1.1124 +using assms card_of_Plus_commute card_of_Plus_infinite1
1.1125 +ordIso_equivalence by blast
1.1126 +
1.1127 +lemma card_of_Plus_infinite:
1.1128 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
1.1129 +shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
1.1130 +using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
1.1131 +
1.1132 +corollary Card_order_Plus_infinite:
1.1133 +assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
1.1134 +        LEQ: "p \<le>o r"
1.1135 +shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
1.1136 +proof-
1.1137 +  have "| Field r <+> Field p | =o | Field r | \<and>
1.1138 +        | Field p <+> Field r | =o | Field r |"
1.1139 +  using assms by (simp add: card_of_Plus_infinite card_of_mono2)
1.1140 +  thus ?thesis
1.1141 +  using assms card_of_Field_ordIso[of r]
1.1142 +        ordIso_transitive[of "|Field r <+> Field p|"]
1.1143 +        ordIso_transitive[of _ "|Field r|"] by blast
1.1144 +qed
1.1145 +
1.1146 +
1.1147 +subsection {* The cardinal $\omega$ and the finite cardinals  *}
1.1148 +
1.1149 +text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.1150 +order relation on
1.1151 +@{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
1.1152 +shall be the restrictions of these relations to the numbers smaller than
1.1153 +fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.  *}
1.1154 +
1.1155 +abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.1156 +abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.1157 +
1.1158 +abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
1.1159 +where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
1.1160 +
1.1161 +lemma infinite_cartesian_product:
1.1162 +assumes "\<not>finite A" "\<not>finite B"
1.1163 +shows "\<not>finite (A \<times> B)"
1.1164 +proof
1.1165 +  assume "finite (A \<times> B)"
1.1166 +  from assms(1) have "A \<noteq> {}" by auto
1.1167 +  with finite (A \<times> B) have "finite B" using finite_cartesian_productD2 by auto
1.1168 +  with assms(2) show False by simp
1.1169 +qed
1.1170 +
1.1171 +
1.1172 +subsubsection {* First as well-orders *}
1.1173 +
1.1174 +lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
1.1175 +by(unfold Field_def, auto)
1.1176 +
1.1177 +lemma natLeq_Refl: "Refl natLeq"
1.1178 +unfolding refl_on_def Field_def by auto
1.1179 +
1.1180 +lemma natLeq_trans: "trans natLeq"
1.1181 +unfolding trans_def by auto
1.1182 +
1.1183 +lemma natLeq_Preorder: "Preorder natLeq"
1.1184 +unfolding preorder_on_def
1.1185 +by (auto simp add: natLeq_Refl natLeq_trans)
1.1186 +
1.1187 +lemma natLeq_antisym: "antisym natLeq"
1.1188 +unfolding antisym_def by auto
1.1189 +
1.1190 +lemma natLeq_Partial_order: "Partial_order natLeq"
1.1191 +unfolding partial_order_on_def
1.1192 +by (auto simp add: natLeq_Preorder natLeq_antisym)
1.1193 +
1.1194 +lemma natLeq_Total: "Total natLeq"
1.1195 +unfolding total_on_def by auto
1.1196 +
1.1197 +lemma natLeq_Linear_order: "Linear_order natLeq"
1.1198 +unfolding linear_order_on_def
1.1199 +by (auto simp add: natLeq_Partial_order natLeq_Total)
1.1200 +
1.1201 +lemma natLeq_natLess_Id: "natLess = natLeq - Id"
1.1202 +by auto
1.1203 +
1.1204 +lemma natLeq_Well_order: "Well_order natLeq"
1.1205 +unfolding well_order_on_def
1.1206 +using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
1.1207 +
1.1208 +lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
1.1209 +unfolding Field_def by auto
1.1210 +
1.1211 +lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
1.1212 +unfolding underS_def by auto
1.1213 +
1.1214 +lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
1.1215 +by force
1.1216 +
1.1217 +lemma Restr_natLeq2:
1.1218 +"Restr natLeq (underS natLeq n) = natLeq_on n"
1.1219 +by (auto simp add: Restr_natLeq natLeq_underS_less)
1.1220 +
1.1221 +lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
1.1222 +using Restr_natLeq[of n] natLeq_Well_order
1.1223 +      Well_order_Restr[of natLeq "{x. x < n}"] by auto
1.1224 +
1.1225 +corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
1.1226 +using natLeq_on_Well_order Field_natLeq_on by auto
1.1227 +
1.1228 +lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
1.1229 +unfolding wo_rel_def using natLeq_on_Well_order .
1.1230 +
1.1231 +
1.1232 +subsubsection {* Then as cardinals *}
1.1233 +
1.1234 +lemma natLeq_Card_order: "Card_order natLeq"
1.1236 +      Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
1.1237 +  fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
1.1238 +  moreover have "\<not>finite(UNIV::nat set)" by auto
1.1239 +  ultimately show "natLeq_on n <o |UNIV::nat set|"
1.1240 +  using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
1.1241 +        Field_card_of[of "UNIV::nat set"]
1.1242 +        card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
1.1243 +qed
1.1244 +
1.1245 +corollary card_of_Field_natLeq:
1.1246 +"|Field natLeq| =o natLeq"
1.1247 +using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
1.1248 +      ordIso_symmetric[of natLeq] by blast
1.1249 +
1.1250 +corollary card_of_nat:
1.1251 +"|UNIV::nat set| =o natLeq"
1.1252 +using Field_natLeq card_of_Field_natLeq by auto
1.1253 +
1.1254 +corollary infinite_iff_natLeq_ordLeq:
1.1255 +"\<not>finite A = ( natLeq \<le>o |A| )"
1.1256 +using infinite_iff_card_of_nat[of A] card_of_nat
1.1257 +      ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
1.1258 +
1.1259 +corollary finite_iff_ordLess_natLeq:
1.1260 +"finite A = ( |A| <o natLeq)"
1.1261 +using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
1.1262 +      card_of_Well_order natLeq_Well_order by metis
1.1263 +
1.1264 +
1.1265 +subsection {* The successor of a cardinal *}
1.1266 +
1.1267 +text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.1268 +being a successor cardinal of @{text "r"}. Although the definition does
1.1269 +not require @{text "r"} to be a cardinal, only this case will be meaningful.  *}
1.1270 +
1.1271 +definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1.1272 +where
1.1273 +"isCardSuc r r' \<equiv>
1.1274 + Card_order r' \<and> r <o r' \<and>
1.1275 + (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
1.1276 +
1.1277 +text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},
1.1278 +by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
1.1279 +Again, the picked item shall be proved unique up to order-isomorphism. *}
1.1280 +
1.1281 +definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
1.1282 +where
1.1283 +"cardSuc r \<equiv> SOME r'. isCardSuc r r'"
1.1284 +
1.1285 +lemma exists_minim_Card_order:
1.1286 +"\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
1.1287 +unfolding card_order_on_def using exists_minim_Well_order by blast
1.1288 +
1.1289 +lemma exists_isCardSuc:
1.1290 +assumes "Card_order r"
1.1291 +shows "\<exists>r'. isCardSuc r r'"
1.1292 +proof-
1.1293 +  let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"
1.1294 +  have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms
1.1295 +  by (simp add: card_of_Card_order Card_order_Pow)
1.1296 +  then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"
1.1297 +  using exists_minim_Card_order[of ?R] by blast
1.1298 +  thus ?thesis unfolding isCardSuc_def by auto
1.1299 +qed
1.1300 +
1.1301 +lemma cardSuc_isCardSuc:
1.1302 +assumes "Card_order r"
1.1303 +shows "isCardSuc r (cardSuc r)"
1.1304 +unfolding cardSuc_def using assms
1.1305 +by (simp add: exists_isCardSuc someI_ex)
1.1306 +
1.1307 +lemma cardSuc_Card_order:
1.1308 +"Card_order r \<Longrightarrow> Card_order(cardSuc r)"
1.1309 +using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1310 +
1.1311 +lemma cardSuc_greater:
1.1312 +"Card_order r \<Longrightarrow> r <o cardSuc r"
1.1313 +using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1314 +
1.1315 +lemma cardSuc_ordLeq:
1.1316 +"Card_order r \<Longrightarrow> r \<le>o cardSuc r"
1.1317 +using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1.1318 +
1.1319 +text{* The minimality property of @{text "cardSuc"} originally present in its definition
1.1320 +is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:  *}
1.1321 +
1.1322 +lemma cardSuc_least_aux:
1.1323 +"\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
1.1324 +using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1325 +
1.1326 +text{* But from this we can infer general minimality: *}
1.1327 +
1.1328 +lemma cardSuc_least:
1.1329 +assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
1.1330 +shows "cardSuc r \<le>o r'"
1.1331 +proof-
1.1332 +  let ?p = "cardSuc r"
1.1333 +  have 0: "Well_order ?p \<and> Well_order r'"
1.1334 +  using assms cardSuc_Card_order unfolding card_order_on_def by blast
1.1335 +  {assume "r' <o ?p"
1.1336 +   then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"
1.1337 +   using internalize_ordLess[of r' ?p] by blast
1.1338 +   (*  *)
1.1339 +   have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
1.1340 +   moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
1.1341 +   ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast
1.1342 +   hence False using 2 not_ordLess_ordLeq by blast
1.1343 +  }
1.1344 +  thus ?thesis using 0 ordLess_or_ordLeq by blast
1.1345 +qed
1.1346 +
1.1347 +lemma cardSuc_ordLess_ordLeq:
1.1348 +assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1349 +shows "(r <o r') = (cardSuc r \<le>o r')"
1.1350 +proof(auto simp add: assms cardSuc_least)
1.1351 +  assume "cardSuc r \<le>o r'"
1.1352 +  thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast
1.1353 +qed
1.1354 +
1.1355 +lemma cardSuc_ordLeq_ordLess:
1.1356 +assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1357 +shows "(r' <o cardSuc r) = (r' \<le>o r)"
1.1358 +proof-
1.1359 +  have "Well_order r \<and> Well_order r'"
1.1360 +  using assms unfolding card_order_on_def by auto
1.1361 +  moreover have "Well_order(cardSuc r)"
1.1362 +  using assms cardSuc_Card_order card_order_on_def by blast
1.1363 +  ultimately show ?thesis
1.1364 +  using assms cardSuc_ordLess_ordLeq[of r r']
1.1365 +  not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
1.1366 +qed
1.1367 +
1.1368 +lemma cardSuc_mono_ordLeq:
1.1369 +assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1370 +shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"
1.1371 +using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
1.1372 +
1.1373 +lemma cardSuc_invar_ordIso:
1.1374 +assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1375 +shows "(cardSuc r =o cardSuc r') = (r =o r')"
1.1376 +proof-
1.1377 +  have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
1.1378 +  using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
1.1379 +  thus ?thesis
1.1380 +  using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
1.1381 +  using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
1.1382 +qed
1.1383 +
1.1384 +lemma card_of_cardSuc_finite:
1.1385 +"finite(Field(cardSuc |A| )) = finite A"
1.1386 +proof
1.1387 +  assume *: "finite (Field (cardSuc |A| ))"
1.1388 +  have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
1.1389 +  using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
1.1390 +  hence "|A| \<le>o |Field(cardSuc |A| )|"
1.1391 +  using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
1.1392 +  ordLeq_ordIso_trans by blast
1.1393 +  thus "finite A" using * card_of_ordLeq_finite by blast
1.1394 +next
1.1395 +  assume "finite A"
1.1396 +  then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
1.1397 +  then show "finite (Field (cardSuc |A| ))"
1.1398 +  proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
1.1399 +    show "cardSuc |A| \<le>o |Pow A|"
1.1400 +      by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)
1.1401 +  qed
1.1402 +qed
1.1403 +
1.1404 +lemma cardSuc_finite:
1.1405 +assumes "Card_order r"
1.1406 +shows "finite (Field (cardSuc r)) = finite (Field r)"
1.1407 +proof-
1.1408 +  let ?A = "Field r"
1.1409 +  have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
1.1410 +  hence "cardSuc |?A| =o cardSuc r" using assms
1.1411 +  by (simp add: card_of_Card_order cardSuc_invar_ordIso)
1.1412 +  moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
1.1413 +  by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
1.1414 +  moreover
1.1415 +  {have "|Field (cardSuc r) | =o cardSuc r"
1.1416 +   using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
1.1417 +   hence "cardSuc r =o |Field (cardSuc r) |"
1.1418 +   using ordIso_symmetric by blast
1.1419 +  }
1.1420 +  ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
1.1421 +  using ordIso_transitive by blast
1.1422 +  hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
1.1423 +  using card_of_ordIso_finite by blast
1.1424 +  thus ?thesis by (simp only: card_of_cardSuc_finite)
1.1425 +qed
1.1426 +
1.1427 +lemma card_of_Plus_ordLess_infinite:
1.1428 +assumes INF: "\<not>finite C" and
1.1429 +        LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
1.1430 +shows "|A <+> B| <o |C|"
1.1431 +proof(cases "A = {} \<or> B = {}")
1.1432 +  assume Case1: "A = {} \<or> B = {}"
1.1433 +  hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"
1.1434 +  using card_of_Plus_empty1 card_of_Plus_empty2 by blast
1.1435 +  hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"
1.1436 +  using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
1.1437 +  thus ?thesis using LESS1 LESS2
1.1438 +       ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
1.1439 +       ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
1.1440 +next
1.1441 +  assume Case2: "\<not>(A = {} \<or> B = {})"
1.1442 +  {assume *: "|C| \<le>o |A <+> B|"
1.1443 +   hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
1.1444 +   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
1.1445 +   {assume Case21: "|A| \<le>o |B|"
1.1446 +    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
1.1447 +    hence "|A <+> B| =o |B|" using Case2 Case21
1.1448 +    by (auto simp add: card_of_Plus_infinite)
1.1449 +    hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1.1450 +   }
1.1451 +   moreover
1.1452 +   {assume Case22: "|B| \<le>o |A|"
1.1453 +    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
1.1454 +    hence "|A <+> B| =o |A|" using Case2 Case22
1.1455 +    by (auto simp add: card_of_Plus_infinite)
1.1456 +    hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1.1457 +   }
1.1458 +   ultimately have False using ordLeq_total card_of_Well_order[of A]
1.1459 +   card_of_Well_order[of B] by blast
1.1460 +  }
1.1461 +  thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
1.1462 +  card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
1.1463 +qed
1.1464 +
1.1465 +lemma card_of_Plus_ordLess_infinite_Field:
1.1466 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
1.1467 +        LESS1: "|A| <o r" and LESS2: "|B| <o r"
1.1468 +shows "|A <+> B| <o r"
1.1469 +proof-
1.1470 +  let ?C  = "Field r"
1.1471 +  have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
1.1472 +  ordIso_symmetric by blast
1.1473 +  hence "|A| <o |?C|"  "|B| <o |?C|"
1.1474 +  using LESS1 LESS2 ordLess_ordIso_trans by blast+
1.1475 +  hence  "|A <+> B| <o |?C|" using INF
1.1476 +  card_of_Plus_ordLess_infinite by blast
1.1477 +  thus ?thesis using 1 ordLess_ordIso_trans by blast
1.1478 +qed
1.1479 +
1.1480 +lemma card_of_Plus_ordLeq_infinite_Field:
1.1481 +assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1.1482 +and c: "Card_order r"
1.1483 +shows "|A <+> B| \<le>o r"
1.1484 +proof-
1.1485 +  let ?r' = "cardSuc r"
1.1486 +  have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
1.1487 +  by (simp add: cardSuc_Card_order cardSuc_finite)
1.1488 +  moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
1.1489 +  by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1.1490 +  ultimately have "|A <+> B| <o ?r'"
1.1491 +  using card_of_Plus_ordLess_infinite_Field by blast
1.1492 +  thus ?thesis using c r
1.1493 +  by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1.1494 +qed
1.1495 +
1.1496 +lemma card_of_Un_ordLeq_infinite_Field:
1.1497 +assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1.1498 +and "Card_order r"
1.1499 +shows "|A Un B| \<le>o r"
1.1500 +using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
1.1501 +ordLeq_transitive by fast
1.1502 +
1.1503 +
1.1504 +subsection {* Regular cardinals *}
1.1505 +
1.1506 +definition cofinal where
1.1507 +"cofinal A r \<equiv>
1.1508 + ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
1.1509 +
1.1510 +definition regular where
1.1511 +"regular r \<equiv>
1.1512 + ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1.1513 +
1.1514 +definition relChain where
1.1515 +"relChain r As \<equiv>
1.1516 + ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1.1517 +
1.1518 +lemma regular_UNION:
1.1519 +assumes r: "Card_order r"   "regular r"
1.1520 +and As: "relChain r As"
1.1521 +and Bsub: "B \<le> (UN i : Field r. As i)"
1.1522 +and cardB: "|B| <o r"
1.1523 +shows "EX i : Field r. B \<le> As i"
1.1524 +proof-
1.1525 +  let ?phi = "%b j. j : Field r \<and> b : As j"
1.1526 +  have "ALL b : B. EX j. ?phi b j" using Bsub by blast
1.1527 +  then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"
1.1528 +  using bchoice[of B ?phi] by blast
1.1529 +  let ?K = "f  B"
1.1530 +  {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"
1.1531 +   have 2: "cofinal ?K r"
1.1532 +   unfolding cofinal_def proof auto
1.1533 +     fix i assume i: "i : Field r"
1.1534 +     with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast
1.1535 +     hence "i \<noteq> f b \<and> ~ (f b,i) : r"
1.1536 +     using As f unfolding relChain_def by auto
1.1537 +     hence "i \<noteq> f b \<and> (i, f b) : r" using r
1.1538 +     unfolding card_order_on_def well_order_on_def linear_order_on_def
1.1539 +     total_on_def using i f b by auto
1.1540 +     with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
1.1541 +   qed
1.1542 +   moreover have "?K \<le> Field r" using f by blast
1.1543 +   ultimately have "|?K| =o r" using 2 r unfolding regular_def by blast
1.1544 +   moreover
1.1545 +   {
1.1546 +    have "|?K| <=o |B|" using card_of_image .
1.1547 +    hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast
1.1548 +   }
1.1549 +   ultimately have False using not_ordLess_ordIso by blast
1.1550 +  }
1.1551 +  thus ?thesis by blast
1.1552 +qed
1.1553 +
1.1554 +lemma infinite_cardSuc_regular:
1.1555 +assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
1.1556 +shows "regular (cardSuc r)"
1.1557 +proof-
1.1558 +  let ?r' = "cardSuc r"
1.1559 +  have r': "Card_order ?r'"
1.1560 +  "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"
1.1561 +  using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
1.1562 +  show ?thesis
1.1563 +  unfolding regular_def proof auto
1.1564 +    fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
1.1565 +    hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
1.1566 +    also have 22: "|Field ?r'| =o ?r'"
1.1567 +    using r' by (simp add: card_of_Field_ordIso[of ?r'])
1.1568 +    finally have "|K| \<le>o ?r'" .
1.1569 +    moreover
1.1570 +    {let ?L = "UN j : K. underS ?r' j"
1.1571 +     let ?J = "Field r"
1.1572 +     have rJ: "r =o |?J|"
1.1573 +     using r_card card_of_Field_ordIso ordIso_symmetric by blast
1.1574 +     assume "|K| <o ?r'"
1.1575 +     hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
1.1576 +     hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
1.1577 +     moreover
1.1578 +     {have "ALL j : K. |underS ?r' j| <o ?r'"
1.1579 +      using r' 1 by (auto simp: card_of_underS)
1.1580 +      hence "ALL j : K. |underS ?r' j| \<le>o r"
1.1581 +      using r' card_of_Card_order by blast
1.1582 +      hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
1.1583 +      using rJ ordLeq_ordIso_trans by blast
1.1584 +     }
1.1585 +     ultimately have "|?L| \<le>o |?J|"
1.1586 +     using r_inf card_of_UNION_ordLeq_infinite by blast
1.1587 +     hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
1.1588 +     hence "|?L| <o ?r'" using r' card_of_Card_order by blast
1.1589 +     moreover
1.1590 +     {
1.1591 +      have "Field ?r' \<le> ?L"
1.1592 +      using 2 unfolding underS_def cofinal_def by auto
1.1593 +      hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
1.1594 +      hence "?r' \<le>o |?L|"
1.1595 +      using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
1.1596 +     }
1.1597 +     ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast
1.1598 +     hence False using ordLess_irreflexive by blast
1.1599 +    }
1.1600 +    ultimately show "|K| =o ?r'"
1.1601 +    unfolding ordLeq_iff_ordLess_or_ordIso by blast
1.1602 +  qed
1.1603 +qed
1.1604 +
1.1605 +lemma cardSuc_UNION:
1.1606 +assumes r: "Card_order r" and "\<not>finite (Field r)"
1.1607 +and As: "relChain (cardSuc r) As"
1.1608 +and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
1.1609 +and cardB: "|B| <=o r"
1.1610 +shows "EX i : Field (cardSuc r). B \<le> As i"
1.1611 +proof-
1.1612 +  let ?r' = "cardSuc r"
1.1613 +  have "Card_order ?r' \<and> |B| <o ?r'"
1.1614 +  using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
1.1615 +  card_of_Card_order by blast
1.1616 +  moreover have "regular ?r'"
1.1617 +  using assms by(simp add: infinite_cardSuc_regular)
1.1618 +  ultimately show ?thesis
1.1619 +  using As Bsub cardB regular_UNION by blast
1.1620 +qed
1.1621 +
1.1622 +
1.1623 +subsection {* Others *}
1.1624 +
1.1625 +lemma card_of_Func_Times:
1.1626 +"|Func (A <*> B) C| =o |Func A (Func B C)|"
1.1627 +unfolding card_of_ordIso[symmetric]
1.1628 +using bij_betw_curr by blast
1.1629 +
1.1630 +lemma card_of_Pow_Func:
1.1631 +"|Pow A| =o |Func A (UNIV::bool set)|"
1.1632 +proof-
1.1633 +  def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False)
1.1634 +                            else undefined"
1.1635 +  have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
1.1636 +  unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
1.1637 +    fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
1.1638 +    thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)
1.1639 +  next
1.1640 +    show "F  Pow A = Func A UNIV"
1.1641 +    proof safe
1.1642 +      fix f assume f: "f \<in> Func A (UNIV::bool set)"
1.1643 +      show "f \<in> F  Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
1.1644 +        let ?A1 = "{a \<in> A. f a = True}"
1.1645 +        show "f = F ?A1" unfolding F_def apply(rule ext)
1.1646 +        using f unfolding Func_def mem_Collect_eq by auto
1.1647 +      qed auto
1.1648 +    qed(unfold Func_def mem_Collect_eq F_def, auto)
1.1649 +  qed
1.1650 +  thus ?thesis unfolding card_of_ordIso[symmetric] by blast
1.1651 +qed
1.1652 +
1.1653 +lemma card_of_Func_UNIV:
1.1654 +"|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|"
1.1655 +apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
1.1656 +  let ?F = "\<lambda> f (a::'a). ((f a)::'b)"
1.1657 +  show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"
1.1658 +  unfolding bij_betw_def inj_on_def proof safe
1.1659 +    fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
1.1660 +    hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
1.1661 +    then obtain f where f: "\<forall> a. h a = f a" by metis
1.1662 +    hence "range f \<subseteq> B" using h unfolding Func_def by auto
1.1663 +    thus "h \<in> (\<lambda>f a. f a)  {f. range f \<subseteq> B}" using f unfolding image_def by auto
1.1664 +  qed(unfold Func_def fun_eq_iff, auto)
1.1665 +qed
1.1666 +
1.1667 +end
`