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.6 +    Copyright   2012
     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.1046 +by(simp add: card_of_Sigma_ordLeq_infinite_Field)
  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.1235 +proof(auto simp add: natLeq_Well_order
  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