1.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,2438 +0,0 @@
1.4 -(* Title: HOL/Cardinals/Cardinal_Order_Relation_Base.thy
1.5 - Author: Andrei Popescu, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -Cardinal-order relations (base).
1.9 -*)
1.10 -
1.11 -header {* Cardinal-Order Relations (Base) *}
1.12 -
1.13 -theory Cardinal_Order_Relation_Base
1.14 -imports Constructions_on_Wellorders_Base
1.15 -begin
1.16 -
1.17 -
1.18 -text{* In this section, we define cardinal-order relations to be minim well-orders
1.19 -on their field. Then we define the cardinal of a set to be {\em some} cardinal-order
1.20 -relation on that set, which will be unique up to order isomorphism. Then we study
1.21 -the connection between cardinals and:
1.22 -\begin{itemize}
1.23 -\item standard set-theoretic constructions: products,
1.24 -sums, unions, lists, powersets, set-of finite sets operator;
1.25 -\item finiteness and infiniteness (in particular, with the numeric cardinal operator
1.26 -for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
1.27 -\end{itemize}
1.28 -%
1.29 -On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also
1.30 -define (again, up to order isomorphism) the successor of a cardinal, and show that
1.31 -any cardinal admits a successor.
1.32 -
1.33 -Main results of this section are the existence of cardinal relations and the
1.34 -facts that, in the presence of infiniteness,
1.35 -most of the standard set-theoretic constructions (except for the powerset)
1.36 -{\em do not increase cardinality}. In particular, e.g., the set of words/lists over
1.37 -any infinite set has the same cardinality (hence, is in bijection) with that set.
1.38 -*}
1.39 -
1.40 -
1.41 -subsection {* Cardinal orders *}
1.42 -
1.43 -
1.44 -text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.45 -order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
1.46 -strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
1.47 -
1.48 -definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.49 -where
1.50 -"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.51 -
1.52 -
1.53 -abbreviation "Card_order r \<equiv> card_order_on (Field r) r"
1.54 -abbreviation "card_order r \<equiv> card_order_on UNIV r"
1.55 -
1.56 -
1.57 -lemma card_order_on_well_order_on:
1.58 -assumes "card_order_on A r"
1.59 -shows "well_order_on A r"
1.60 -using assms unfolding card_order_on_def by simp
1.61 -
1.62 -
1.63 -lemma card_order_on_Card_order:
1.64 -"card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
1.65 -unfolding card_order_on_def using rel.well_order_on_Field by blast
1.66 -
1.67 -
1.68 -text{* The existence of a cardinal relation on any given set (which will mean
1.69 -that any set has a cardinal) follows from two facts:
1.70 -\begin{itemize}
1.71 -\item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
1.72 -which states that on any given set there exists a well-order;
1.73 -\item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
1.74 -such well-order, i.e., a cardinal order.
1.75 -\end{itemize}
1.76 -*}
1.77 -
1.78 -
1.79 -theorem card_order_on: "\<exists>r. card_order_on A r"
1.80 -proof-
1.81 - obtain R where R_def: "R = {r. well_order_on A r}" by blast
1.82 - have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
1.83 - using well_order_on[of A] R_def rel.well_order_on_Well_order by blast
1.84 - hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
1.85 - using exists_minim_Well_order[of R] by auto
1.86 - thus ?thesis using R_def unfolding card_order_on_def by auto
1.87 -qed
1.88 -
1.89 -
1.90 -lemma card_order_on_ordIso:
1.91 -assumes CO: "card_order_on A r" and CO': "card_order_on A r'"
1.92 -shows "r =o r'"
1.93 -using assms unfolding card_order_on_def
1.94 -using ordIso_iff_ordLeq by blast
1.95 -
1.96 -
1.97 -lemma Card_order_ordIso:
1.98 -assumes CO: "Card_order r" and ISO: "r' =o r"
1.99 -shows "Card_order r'"
1.100 -using ISO unfolding ordIso_def
1.101 -proof(unfold card_order_on_def, auto)
1.102 - fix p' assume "well_order_on (Field r') p'"
1.103 - hence 0: "Well_order p' \<and> Field p' = Field r'"
1.104 - using rel.well_order_on_Well_order by blast
1.105 - obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
1.106 - using ISO unfolding ordIso_def by auto
1.107 - hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
1.108 - by (auto simp add: iso_iff embed_inj_on)
1.109 - let ?p = "dir_image p' f"
1.110 - have 4: "p' =o ?p \<and> Well_order ?p"
1.111 - using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image)
1.112 - moreover have "Field ?p = Field r"
1.113 - using 0 3 by (auto simp add: dir_image_Field2 order_on_defs)
1.114 - ultimately have "well_order_on (Field r) ?p" by auto
1.115 - hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto
1.116 - thus "r' \<le>o p'"
1.117 - using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast
1.118 -qed
1.119 -
1.120 -
1.121 -lemma Card_order_ordIso2:
1.122 -assumes CO: "Card_order r" and ISO: "r =o r'"
1.123 -shows "Card_order r'"
1.124 -using assms Card_order_ordIso ordIso_symmetric by blast
1.125 -
1.126 -
1.127 -subsection {* Cardinal of a set *}
1.128 -
1.129 -
1.130 -text{* We define the cardinal of set to be {\em some} cardinal order on that set.
1.131 -We shall prove that this notion is unique up to order isomorphism, meaning
1.132 -that order isomorphism shall be the true identity of cardinals. *}
1.133 -
1.134 -
1.135 -definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
1.136 -where "card_of A = (SOME r. card_order_on A r)"
1.137 -
1.138 -
1.139 -lemma card_of_card_order_on: "card_order_on A |A|"
1.140 -unfolding card_of_def by (auto simp add: card_order_on someI_ex)
1.141 -
1.142 -
1.143 -lemma card_of_well_order_on: "well_order_on A |A|"
1.144 -using card_of_card_order_on card_order_on_def by blast
1.145 -
1.146 -
1.147 -lemma Field_card_of: "Field |A| = A"
1.148 -using card_of_card_order_on[of A] unfolding card_order_on_def
1.149 -using rel.well_order_on_Field by blast
1.150 -
1.151 -
1.152 -lemma card_of_Card_order: "Card_order |A|"
1.153 -by (simp only: card_of_card_order_on Field_card_of)
1.154 -
1.155 -
1.156 -corollary ordIso_card_of_imp_Card_order:
1.157 -"r =o |A| \<Longrightarrow> Card_order r"
1.158 -using card_of_Card_order Card_order_ordIso by blast
1.159 -
1.160 -
1.161 -lemma card_of_Well_order: "Well_order |A|"
1.162 -using card_of_Card_order unfolding card_order_on_def by auto
1.163 -
1.164 -
1.165 -lemma card_of_refl: "|A| =o |A|"
1.166 -using card_of_Well_order ordIso_reflexive by blast
1.167 -
1.168 -
1.169 -lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r"
1.170 -using card_of_card_order_on unfolding card_order_on_def by blast
1.171 -
1.172 -
1.173 -lemma card_of_ordIso:
1.174 -"(\<exists>f. bij_betw f A B) = ( |A| =o |B| )"
1.175 -proof(auto)
1.176 - fix f assume *: "bij_betw f A B"
1.177 - then obtain r where "well_order_on B r \<and> |A| =o r"
1.178 - using Well_order_iso_copy card_of_well_order_on by blast
1.179 - hence "|B| \<le>o |A|" using card_of_least
1.180 - ordLeq_ordIso_trans ordIso_symmetric by blast
1.181 - moreover
1.182 - {let ?g = "inv_into A f"
1.183 - have "bij_betw ?g B A" using * bij_betw_inv_into by blast
1.184 - then obtain r where "well_order_on A r \<and> |B| =o r"
1.185 - using Well_order_iso_copy card_of_well_order_on by blast
1.186 - hence "|A| \<le>o |B|" using card_of_least
1.187 - ordLeq_ordIso_trans ordIso_symmetric by blast
1.188 - }
1.189 - ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast
1.190 -next
1.191 - assume "|A| =o |B|"
1.192 - then obtain f where "iso ( |A| ) ( |B| ) f"
1.193 - unfolding ordIso_def by auto
1.194 - hence "bij_betw f A B" unfolding iso_def Field_card_of by simp
1.195 - thus "\<exists>f. bij_betw f A B" by auto
1.196 -qed
1.197 -
1.198 -
1.199 -lemma card_of_ordLeq:
1.200 -"(\<exists>f. inj_on f A \<and> f ` A \<le> B) = ( |A| \<le>o |B| )"
1.201 -proof(auto)
1.202 - fix f assume *: "inj_on f A" and **: "f ` A \<le> B"
1.203 - {assume "|B| <o |A|"
1.204 - hence "|B| \<le>o |A|" using ordLeq_iff_ordLess_or_ordIso by blast
1.205 - then obtain g where "embed ( |B| ) ( |A| ) g"
1.206 - unfolding ordLeq_def by auto
1.207 - hence 1: "inj_on g B \<and> g ` B \<le> A" using embed_inj_on[of "|B|" "|A|" "g"]
1.208 - card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
1.209 - embed_Field[of "|B|" "|A|" g] by auto
1.210 - obtain h where "bij_betw h A B"
1.211 - using * ** 1 Cantor_Bernstein[of f] by fastforce
1.212 - hence "|A| =o |B|" using card_of_ordIso by blast
1.213 - hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
1.214 - }
1.215 - thus "|A| \<le>o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"]
1.216 - by (auto simp: card_of_Well_order)
1.217 -next
1.218 - assume *: "|A| \<le>o |B|"
1.219 - obtain f where "embed ( |A| ) ( |B| ) f"
1.220 - using * unfolding ordLeq_def by auto
1.221 - hence "inj_on f A \<and> f ` A \<le> B" using embed_inj_on[of "|A|" "|B|" f]
1.222 - card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"]
1.223 - embed_Field[of "|A|" "|B|" f] by auto
1.224 - thus "\<exists>f. inj_on f A \<and> f ` A \<le> B" by auto
1.225 -qed
1.226 -
1.227 -
1.228 -lemma card_of_ordLeq2:
1.229 -"A \<noteq> {} \<Longrightarrow> (\<exists>g. g ` B = A) = ( |A| \<le>o |B| )"
1.230 -using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto
1.231 -
1.232 -
1.233 -lemma card_of_ordLess:
1.234 -"(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = ( |B| <o |A| )"
1.235 -proof-
1.236 - have "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = (\<not> |A| \<le>o |B| )"
1.237 - using card_of_ordLeq by blast
1.238 - also have "\<dots> = ( |B| <o |A| )"
1.239 - using card_of_Well_order[of A] card_of_Well_order[of B]
1.240 - not_ordLeq_iff_ordLess by blast
1.241 - finally show ?thesis .
1.242 -qed
1.243 -
1.244 -
1.245 -lemma card_of_ordLess2:
1.246 -"B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f ` A = B)) = ( |A| <o |B| )"
1.247 -using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto
1.248 -
1.249 -
1.250 -lemma card_of_ordIsoI:
1.251 -assumes "bij_betw f A B"
1.252 -shows "|A| =o |B|"
1.253 -using assms unfolding card_of_ordIso[symmetric] by auto
1.254 -
1.255 -
1.256 -lemma card_of_ordLeqI:
1.257 -assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B"
1.258 -shows "|A| \<le>o |B|"
1.259 -using assms unfolding card_of_ordLeq[symmetric] by auto
1.260 -
1.261 -
1.262 -lemma card_of_unique:
1.263 -"card_order_on A r \<Longrightarrow> r =o |A|"
1.264 -by (simp only: card_order_on_ordIso card_of_card_order_on)
1.265 -
1.266 -
1.267 -lemma card_of_mono1:
1.268 -"A \<le> B \<Longrightarrow> |A| \<le>o |B|"
1.269 -using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce
1.270 -
1.271 -
1.272 -lemma card_of_mono2:
1.273 -assumes "r \<le>o r'"
1.274 -shows "|Field r| \<le>o |Field r'|"
1.275 -proof-
1.276 - obtain f where
1.277 - 1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
1.278 - using assms unfolding ordLeq_def
1.279 - by (auto simp add: rel.well_order_on_Well_order)
1.280 - hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
1.281 - by (auto simp add: embed_inj_on embed_Field)
1.282 - thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
1.283 -qed
1.284 -
1.285 -
1.286 -lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|"
1.287 -by (simp add: ordIso_iff_ordLeq card_of_mono2)
1.288 -
1.289 -
1.290 -lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
1.291 -using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast
1.292 -
1.293 -
1.294 -lemma card_of_Field_ordIso:
1.295 -assumes "Card_order r"
1.296 -shows "|Field r| =o r"
1.297 -proof-
1.298 - have "card_order_on (Field r) r"
1.299 - using assms card_order_on_Card_order by blast
1.300 - moreover have "card_order_on (Field r) |Field r|"
1.301 - using card_of_card_order_on by blast
1.302 - ultimately show ?thesis using card_order_on_ordIso by blast
1.303 -qed
1.304 -
1.305 -
1.306 -lemma Card_order_iff_ordIso_card_of:
1.307 -"Card_order r = (r =o |Field r| )"
1.308 -using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast
1.309 -
1.310 -
1.311 -lemma Card_order_iff_ordLeq_card_of:
1.312 -"Card_order r = (r \<le>o |Field r| )"
1.313 -proof-
1.314 - have "Card_order r = (r =o |Field r| )"
1.315 - unfolding Card_order_iff_ordIso_card_of by simp
1.316 - also have "... = (r \<le>o |Field r| \<and> |Field r| \<le>o r)"
1.317 - unfolding ordIso_iff_ordLeq by simp
1.318 - also have "... = (r \<le>o |Field r| )"
1.319 - using card_of_Field_ordLess
1.320 - by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp)
1.321 - finally show ?thesis .
1.322 -qed
1.323 -
1.324 -
1.325 -lemma Card_order_iff_Restr_underS:
1.326 -assumes "Well_order r"
1.327 -shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )"
1.328 -using assms unfolding Card_order_iff_ordLeq_card_of
1.329 -using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
1.330 -
1.331 -
1.332 -lemma card_of_underS:
1.333 -assumes r: "Card_order r" and a: "a : Field r"
1.334 -shows "|rel.underS r a| <o r"
1.335 -proof-
1.336 - let ?A = "rel.underS r a" let ?r' = "Restr r ?A"
1.337 - have 1: "Well_order r"
1.338 - using r unfolding card_order_on_def by simp
1.339 - have "Well_order ?r'" using 1 Well_order_Restr by auto
1.340 - moreover have "card_order_on (Field ?r') |Field ?r'|"
1.341 - using card_of_card_order_on .
1.342 - ultimately have "|Field ?r'| \<le>o ?r'"
1.343 - unfolding card_order_on_def by simp
1.344 - moreover have "Field ?r' = ?A"
1.345 - using 1 wo_rel.underS_ofilter Field_Restr_ofilter
1.346 - unfolding wo_rel_def by fastforce
1.347 - ultimately have "|?A| \<le>o ?r'" by simp
1.348 - also have "?r' <o |Field r|"
1.349 - using 1 a r Card_order_iff_Restr_underS by blast
1.350 - also have "|Field r| =o r"
1.351 - using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto
1.352 - finally show ?thesis .
1.353 -qed
1.354 -
1.355 -
1.356 -lemma ordLess_Field:
1.357 -assumes "r <o r'"
1.358 -shows "|Field r| <o r'"
1.359 -proof-
1.360 - have "well_order_on (Field r) r" using assms unfolding ordLess_def
1.361 - by (auto simp add: rel.well_order_on_Well_order)
1.362 - hence "|Field r| \<le>o r" using card_of_least by blast
1.363 - thus ?thesis using assms ordLeq_ordLess_trans by blast
1.364 -qed
1.365 -
1.366 -
1.367 -lemma internalize_card_of_ordLeq:
1.368 -"( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)"
1.369 -proof
1.370 - assume "|A| \<le>o r"
1.371 - then obtain p where 1: "Field p \<le> Field r \<and> |A| =o p \<and> p \<le>o r"
1.372 - using internalize_ordLeq[of "|A|" r] by blast
1.373 - hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast
1.374 - hence "|Field p| =o p" using card_of_Field_ordIso by blast
1.375 - hence "|A| =o |Field p| \<and> |Field p| \<le>o r"
1.376 - using 1 ordIso_equivalence ordIso_ordLeq_trans by blast
1.377 - thus "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" using 1 by blast
1.378 -next
1.379 - assume "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r"
1.380 - thus "|A| \<le>o r" using ordIso_ordLeq_trans by blast
1.381 -qed
1.382 -
1.383 -
1.384 -lemma internalize_card_of_ordLeq2:
1.385 -"( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )"
1.386 -using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
1.387 -
1.388 -
1.389 -
1.390 -subsection {* Cardinals versus set operations on arbitrary sets *}
1.391 -
1.392 -
1.393 -text{* Here we embark in a long journey of simple results showing
1.394 -that the standard set-theoretic operations are well-behaved w.r.t. the notion of
1.395 -cardinal -- essentially, this means that they preserve the ``cardinal identity"
1.396 -@{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
1.397 -*}
1.398 -
1.399 -
1.400 -lemma card_of_empty: "|{}| \<le>o |A|"
1.401 -using card_of_ordLeq inj_on_id by blast
1.402 -
1.403 -
1.404 -lemma card_of_empty1:
1.405 -assumes "Well_order r \<or> Card_order r"
1.406 -shows "|{}| \<le>o r"
1.407 -proof-
1.408 - have "Well_order r" using assms unfolding card_order_on_def by auto
1.409 - hence "|Field r| <=o r"
1.410 - using assms card_of_Field_ordLess by blast
1.411 - moreover have "|{}| \<le>o |Field r|" by (simp add: card_of_empty)
1.412 - ultimately show ?thesis using ordLeq_transitive by blast
1.413 -qed
1.414 -
1.415 -
1.416 -corollary Card_order_empty:
1.417 -"Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1)
1.418 -
1.419 -
1.420 -lemma card_of_empty2:
1.421 -assumes LEQ: "|A| =o |{}|"
1.422 -shows "A = {}"
1.423 -using assms card_of_ordIso[of A] bij_betw_empty2 by blast
1.424 -
1.425 -
1.426 -lemma card_of_empty3:
1.427 -assumes LEQ: "|A| \<le>o |{}|"
1.428 -shows "A = {}"
1.429 -using assms
1.430 -by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2
1.431 - ordLeq_Well_order_simp)
1.432 -
1.433 -
1.434 -lemma card_of_empty_ordIso:
1.435 -"|{}::'a set| =o |{}::'b set|"
1.436 -using card_of_ordIso unfolding bij_betw_def inj_on_def by blast
1.437 -
1.438 -
1.439 -lemma card_of_image:
1.440 -"|f ` A| <=o |A|"
1.441 -proof(cases "A = {}", simp add: card_of_empty)
1.442 - assume "A ~= {}"
1.443 - hence "f ` A ~= {}" by auto
1.444 - thus "|f ` A| \<le>o |A|"
1.445 - using card_of_ordLeq2[of "f ` A" A] by auto
1.446 -qed
1.447 -
1.448 -
1.449 -lemma surj_imp_ordLeq:
1.450 -assumes "B <= f ` A"
1.451 -shows "|B| <=o |A|"
1.452 -proof-
1.453 - have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
1.454 - thus ?thesis using card_of_image ordLeq_transitive by blast
1.455 -qed
1.456 -
1.457 -
1.458 -lemma card_of_ordLeqI2:
1.459 -assumes "B \<subseteq> f ` A"
1.460 -shows "|B| \<le>o |A|"
1.461 -using assms by (metis surj_imp_ordLeq)
1.462 -
1.463 -
1.464 -lemma card_of_singl_ordLeq:
1.465 -assumes "A \<noteq> {}"
1.466 -shows "|{b}| \<le>o |A|"
1.467 -proof-
1.468 - obtain a where *: "a \<in> A" using assms by auto
1.469 - let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
1.470 - have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
1.471 - using * unfolding inj_on_def by auto
1.472 - thus ?thesis using card_of_ordLeq by blast
1.473 -qed
1.474 -
1.475 -
1.476 -corollary Card_order_singl_ordLeq:
1.477 -"\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r"
1.478 -using card_of_singl_ordLeq[of "Field r" b]
1.479 - card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
1.480 -
1.481 -
1.482 -lemma card_of_Pow: "|A| <o |Pow A|"
1.483 -using card_of_ordLess2[of "Pow A" A] Cantors_paradox[of A]
1.484 - Pow_not_empty[of A] by auto
1.485 -
1.486 -
1.487 -lemma infinite_Pow:
1.488 -assumes "infinite A"
1.489 -shows "infinite (Pow A)"
1.490 -proof-
1.491 - have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
1.492 - thus ?thesis by (metis assms finite_Pow_iff)
1.493 -qed
1.494 -
1.495 -
1.496 -corollary Card_order_Pow:
1.497 -"Card_order r \<Longrightarrow> r <o |Pow(Field r)|"
1.498 -using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
1.499 -
1.500 -
1.501 -corollary card_of_set_type: "|UNIV::'a set| <o |UNIV::'a set set|"
1.502 -using card_of_Pow[of "UNIV::'a set"] by simp
1.503 -
1.504 -
1.505 -lemma card_of_Plus1: "|A| \<le>o |A <+> B|"
1.506 -proof-
1.507 - have "Inl ` A \<le> A <+> B" by auto
1.508 - thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast
1.509 -qed
1.510 -
1.511 -
1.512 -corollary Card_order_Plus1:
1.513 -"Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|"
1.514 -using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
1.515 -
1.516 -
1.517 -lemma card_of_Plus2: "|B| \<le>o |A <+> B|"
1.518 -proof-
1.519 - have "Inr ` B \<le> A <+> B" by auto
1.520 - thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast
1.521 -qed
1.522 -
1.523 -
1.524 -corollary Card_order_Plus2:
1.525 -"Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|"
1.526 -using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
1.527 -
1.528 -
1.529 -lemma card_of_Plus_empty1: "|A| =o |A <+> {}|"
1.530 -proof-
1.531 - have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto
1.532 - thus ?thesis using card_of_ordIso by auto
1.533 -qed
1.534 -
1.535 -
1.536 -lemma card_of_Plus_empty2: "|A| =o |{} <+> A|"
1.537 -proof-
1.538 - have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto
1.539 - thus ?thesis using card_of_ordIso by auto
1.540 -qed
1.541 -
1.542 -
1.543 -lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|"
1.544 -proof-
1.545 - let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a
1.546 - | Inr b \<Rightarrow> Inl b"
1.547 - have "bij_betw ?f (A <+> B) (B <+> A)"
1.548 - unfolding bij_betw_def inj_on_def by force
1.549 - thus ?thesis using card_of_ordIso by blast
1.550 -qed
1.551 -
1.552 -
1.553 -lemma card_of_Plus_assoc:
1.554 -fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
1.555 -shows "|(A <+> B) <+> C| =o |A <+> B <+> C|"
1.556 -proof -
1.557 - def f \<equiv> "\<lambda>(k::('a + 'b) + 'c).
1.558 - case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a
1.559 - |Inr b \<Rightarrow> Inr (Inl b))
1.560 - |Inr c \<Rightarrow> Inr (Inr c)"
1.561 - have "A <+> B <+> C \<subseteq> f ` ((A <+> B) <+> C)"
1.562 - proof
1.563 - fix x assume x: "x \<in> A <+> B <+> C"
1.564 - show "x \<in> f ` ((A <+> B) <+> C)"
1.565 - proof(cases x)
1.566 - case (Inl a)
1.567 - hence "a \<in> A" "x = f (Inl (Inl a))"
1.568 - using x unfolding f_def by auto
1.569 - thus ?thesis by auto
1.570 - next
1.571 - case (Inr bc) note 1 = Inr show ?thesis
1.572 - proof(cases bc)
1.573 - case (Inl b)
1.574 - hence "b \<in> B" "x = f (Inl (Inr b))"
1.575 - using x 1 unfolding f_def by auto
1.576 - thus ?thesis by auto
1.577 - next
1.578 - case (Inr c)
1.579 - hence "c \<in> C" "x = f (Inr c)"
1.580 - using x 1 unfolding f_def by auto
1.581 - thus ?thesis by auto
1.582 - qed
1.583 - qed
1.584 - qed
1.585 - hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
1.586 - unfolding bij_betw_def inj_on_def f_def by force
1.587 - thus ?thesis using card_of_ordIso by blast
1.588 -qed
1.589 -
1.590 -
1.591 -lemma card_of_Plus_mono1:
1.592 -assumes "|A| \<le>o |B|"
1.593 -shows "|A <+> C| \<le>o |B <+> C|"
1.594 -proof-
1.595 - obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
1.596 - using assms card_of_ordLeq[of A] by fastforce
1.597 - obtain g where g_def:
1.598 - "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast
1.599 - have "inj_on g (A <+> C) \<and> g ` (A <+> C) \<le> (B <+> C)"
1.600 - proof-
1.601 - {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and
1.602 - "g d1 = g d2"
1.603 - hence "d1 = d2" using 1 unfolding inj_on_def
1.604 - by(case_tac d1, case_tac d2, auto simp add: g_def)
1.605 - }
1.606 - moreover
1.607 - {fix d assume "d \<in> A <+> C"
1.608 - hence "g d \<in> B <+> C" using 1
1.609 - by(case_tac d, auto simp add: g_def)
1.610 - }
1.611 - ultimately show ?thesis unfolding inj_on_def by auto
1.612 - qed
1.613 - thus ?thesis using card_of_ordLeq by metis
1.614 -qed
1.615 -
1.616 -
1.617 -corollary ordLeq_Plus_mono1:
1.618 -assumes "r \<le>o r'"
1.619 -shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|"
1.620 -using assms card_of_mono2 card_of_Plus_mono1 by blast
1.621 -
1.622 -
1.623 -lemma card_of_Plus_mono2:
1.624 -assumes "|A| \<le>o |B|"
1.625 -shows "|C <+> A| \<le>o |C <+> B|"
1.626 -using assms card_of_Plus_mono1[of A B C]
1.627 - card_of_Plus_commute[of C A] card_of_Plus_commute[of B C]
1.628 - ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"]
1.629 -by blast
1.630 -
1.631 -
1.632 -corollary ordLeq_Plus_mono2:
1.633 -assumes "r \<le>o r'"
1.634 -shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|"
1.635 -using assms card_of_mono2 card_of_Plus_mono2 by blast
1.636 -
1.637 -
1.638 -lemma card_of_Plus_mono:
1.639 -assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
1.640 -shows "|A <+> C| \<le>o |B <+> D|"
1.641 -using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B]
1.642 - ordLeq_transitive[of "|A <+> C|"] by blast
1.643 -
1.644 -
1.645 -corollary ordLeq_Plus_mono:
1.646 -assumes "r \<le>o r'" and "p \<le>o p'"
1.647 -shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|"
1.648 -using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast
1.649 -
1.650 -
1.651 -lemma card_of_Plus_cong1:
1.652 -assumes "|A| =o |B|"
1.653 -shows "|A <+> C| =o |B <+> C|"
1.654 -using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1)
1.655 -
1.656 -
1.657 -corollary ordIso_Plus_cong1:
1.658 -assumes "r =o r'"
1.659 -shows "|(Field r) <+> C| =o |(Field r') <+> C|"
1.660 -using assms card_of_cong card_of_Plus_cong1 by blast
1.661 -
1.662 -
1.663 -lemma card_of_Plus_cong2:
1.664 -assumes "|A| =o |B|"
1.665 -shows "|C <+> A| =o |C <+> B|"
1.666 -using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2)
1.667 -
1.668 -
1.669 -corollary ordIso_Plus_cong2:
1.670 -assumes "r =o r'"
1.671 -shows "|A <+> (Field r)| =o |A <+> (Field r')|"
1.672 -using assms card_of_cong card_of_Plus_cong2 by blast
1.673 -
1.674 -
1.675 -lemma card_of_Plus_cong:
1.676 -assumes "|A| =o |B|" and "|C| =o |D|"
1.677 -shows "|A <+> C| =o |B <+> D|"
1.678 -using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono)
1.679 -
1.680 -
1.681 -corollary ordIso_Plus_cong:
1.682 -assumes "r =o r'" and "p =o p'"
1.683 -shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|"
1.684 -using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast
1.685 -
1.686 -
1.687 -lemma card_of_Un1:
1.688 -shows "|A| \<le>o |A \<union> B| "
1.689 -using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce
1.690 -
1.691 -
1.692 -lemma card_of_diff:
1.693 -shows "|A - B| \<le>o |A|"
1.694 -using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce
1.695 -
1.696 -
1.697 -lemma card_of_Un_Plus_ordLeq:
1.698 -"|A \<union> B| \<le>o |A <+> B|"
1.699 -proof-
1.700 - let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c"
1.701 - have "inj_on ?f (A \<union> B) \<and> ?f ` (A \<union> B) \<le> A <+> B"
1.702 - unfolding inj_on_def by auto
1.703 - thus ?thesis using card_of_ordLeq by blast
1.704 -qed
1.705 -
1.706 -
1.707 -lemma card_of_Times1:
1.708 -assumes "A \<noteq> {}"
1.709 -shows "|B| \<le>o |B \<times> A|"
1.710 -proof(cases "B = {}", simp add: card_of_empty)
1.711 - assume *: "B \<noteq> {}"
1.712 - have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
1.713 - thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
1.714 - card_of_ordLeq[of B "B \<times> A"] * by blast
1.715 -qed
1.716 -
1.717 -
1.718 -corollary Card_order_Times1:
1.719 -"\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|"
1.720 -using card_of_Times1[of B] card_of_Field_ordIso
1.721 - ordIso_ordLeq_trans ordIso_symmetric by blast
1.722 -
1.723 -
1.724 -lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|"
1.725 -proof-
1.726 - let ?f = "\<lambda>(a::'a,b::'b). (b,a)"
1.727 - have "bij_betw ?f (A \<times> B) (B \<times> A)"
1.728 - unfolding bij_betw_def inj_on_def by auto
1.729 - thus ?thesis using card_of_ordIso by blast
1.730 -qed
1.731 -
1.732 -
1.733 -lemma card_of_Times2:
1.734 -assumes "A \<noteq> {}" shows "|B| \<le>o |A \<times> B|"
1.735 -using assms card_of_Times1[of A B] card_of_Times_commute[of B A]
1.736 - ordLeq_ordIso_trans by blast
1.737 -
1.738 -
1.739 -corollary Card_order_Times2:
1.740 -"\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|"
1.741 -using card_of_Times2[of A] card_of_Field_ordIso
1.742 - ordIso_ordLeq_trans ordIso_symmetric by blast
1.743 -
1.744 -
1.745 -lemma card_of_Times3: "|A| \<le>o |A \<times> A|"
1.746 -using card_of_Times1[of A]
1.747 -by(cases "A = {}", simp add: card_of_empty, blast)
1.748 -
1.749 -
1.750 -lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|"
1.751 -proof-
1.752 - let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True)
1.753 - |Inr a \<Rightarrow> (a,False)"
1.754 - have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))"
1.755 - proof-
1.756 - {fix c1 and c2 assume "?f c1 = ?f c2"
1.757 - hence "c1 = c2"
1.758 - by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
1.759 - }
1.760 - moreover
1.761 - {fix c assume "c \<in> A <+> A"
1.762 - hence "?f c \<in> A \<times> (UNIV::bool set)"
1.763 - by(case_tac c, auto)
1.764 - }
1.765 - moreover
1.766 - {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
1.767 - have "(a,bl) \<in> ?f ` ( A <+> A)"
1.768 - proof(cases bl)
1.769 - assume bl hence "?f(Inl a) = (a,bl)" by auto
1.770 - thus ?thesis using * by force
1.771 - next
1.772 - assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto
1.773 - thus ?thesis using * by force
1.774 - qed
1.775 - }
1.776 - ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto
1.777 - qed
1.778 - thus ?thesis using card_of_ordIso by blast
1.779 -qed
1.780 -
1.781 -
1.782 -lemma card_of_Times_mono1:
1.783 -assumes "|A| \<le>o |B|"
1.784 -shows "|A \<times> C| \<le>o |B \<times> C|"
1.785 -proof-
1.786 - obtain f where 1: "inj_on f A \<and> f ` A \<le> B"
1.787 - using assms card_of_ordLeq[of A] by fastforce
1.788 - obtain g where g_def:
1.789 - "g = (\<lambda>(a,c::'c). (f a,c))" by blast
1.790 - have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)"
1.791 - using 1 unfolding inj_on_def using g_def by auto
1.792 - thus ?thesis using card_of_ordLeq by metis
1.793 -qed
1.794 -
1.795 -
1.796 -corollary ordLeq_Times_mono1:
1.797 -assumes "r \<le>o r'"
1.798 -shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|"
1.799 -using assms card_of_mono2 card_of_Times_mono1 by blast
1.800 -
1.801 -
1.802 -lemma card_of_Times_mono2:
1.803 -assumes "|A| \<le>o |B|"
1.804 -shows "|C \<times> A| \<le>o |C \<times> B|"
1.805 -using assms card_of_Times_mono1[of A B C]
1.806 - card_of_Times_commute[of C A] card_of_Times_commute[of B C]
1.807 - ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"]
1.808 -by blast
1.809 -
1.810 -
1.811 -corollary ordLeq_Times_mono2:
1.812 -assumes "r \<le>o r'"
1.813 -shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|"
1.814 -using assms card_of_mono2 card_of_Times_mono2 by blast
1.815 -
1.816 -
1.817 -lemma card_of_Times_cong1:
1.818 -assumes "|A| =o |B|"
1.819 -shows "|A \<times> C| =o |B \<times> C|"
1.820 -using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1)
1.821 -
1.822 -
1.823 -lemma card_of_Times_cong2:
1.824 -assumes "|A| =o |B|"
1.825 -shows "|C \<times> A| =o |C \<times> B|"
1.826 -using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2)
1.827 -
1.828 -
1.829 -corollary ordIso_Times_cong2:
1.830 -assumes "r =o r'"
1.831 -shows "|A \<times> (Field r)| =o |A \<times> (Field r')|"
1.832 -using assms card_of_cong card_of_Times_cong2 by blast
1.833 -
1.834 -
1.835 -lemma card_of_Sigma_mono1:
1.836 -assumes "\<forall>i \<in> I. |A i| \<le>o |B i|"
1.837 -shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|"
1.838 -proof-
1.839 - have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
1.840 - using assms by (auto simp add: card_of_ordLeq)
1.841 - with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
1.842 - 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.843 - obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
1.844 - have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
1.845 - using 1 unfolding inj_on_def using g_def by force
1.846 - thus ?thesis using card_of_ordLeq by metis
1.847 -qed
1.848 -
1.849 -
1.850 -corollary card_of_Sigma_Times:
1.851 -"\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
1.852 -using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
1.853 -
1.854 -
1.855 -lemma card_of_UNION_Sigma:
1.856 -"|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
1.857 -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis
1.858 -
1.859 -
1.860 -lemma card_of_bool:
1.861 -assumes "a1 \<noteq> a2"
1.862 -shows "|UNIV::bool set| =o |{a1,a2}|"
1.863 -proof-
1.864 - let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2"
1.865 - have "bij_betw ?f UNIV {a1,a2}"
1.866 - proof-
1.867 - {fix bl1 and bl2 assume "?f bl1 = ?f bl2"
1.868 - hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
1.869 - }
1.870 - moreover
1.871 - {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
1.872 - }
1.873 - moreover
1.874 - {fix a assume *: "a \<in> {a1,a2}"
1.875 - have "a \<in> ?f ` UNIV"
1.876 - proof(cases "a = a1")
1.877 - assume "a = a1"
1.878 - hence "?f True = a" by auto thus ?thesis by blast
1.879 - next
1.880 - assume "a \<noteq> a1" hence "a = a2" using * by auto
1.881 - hence "?f False = a" by auto thus ?thesis by blast
1.882 - qed
1.883 - }
1.884 - ultimately show ?thesis unfolding bij_betw_def inj_on_def
1.885 - by (metis image_subsetI order_eq_iff subsetI)
1.886 - qed
1.887 - thus ?thesis using card_of_ordIso by blast
1.888 -qed
1.889 -
1.890 -
1.891 -lemma card_of_Plus_Times_aux:
1.892 -assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
1.893 - LEQ: "|A| \<le>o |B|"
1.894 -shows "|A <+> B| \<le>o |A \<times> B|"
1.895 -proof-
1.896 - have 1: "|UNIV::bool set| \<le>o |A|"
1.897 - using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
1.898 - ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis
1.899 - (* *)
1.900 - have "|A <+> B| \<le>o |B <+> B|"
1.901 - using LEQ card_of_Plus_mono1 by blast
1.902 - moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|"
1.903 - using card_of_Plus_Times_bool by blast
1.904 - moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|"
1.905 - using 1 by (simp add: card_of_Times_mono2)
1.906 - moreover have " |B \<times> A| =o |A \<times> B|"
1.907 - using card_of_Times_commute by blast
1.908 - ultimately show "|A <+> B| \<le>o |A \<times> B|"
1.909 - using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"]
1.910 - ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"]
1.911 - ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"]
1.912 - by blast
1.913 -qed
1.914 -
1.915 -
1.916 -lemma card_of_Plus_Times:
1.917 -assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and
1.918 - B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B"
1.919 -shows "|A <+> B| \<le>o |A \<times> B|"
1.920 -proof-
1.921 - {assume "|A| \<le>o |B|"
1.922 - hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux)
1.923 - }
1.924 - moreover
1.925 - {assume "|B| \<le>o |A|"
1.926 - hence "|B <+> A| \<le>o |B \<times> A|"
1.927 - using assms by (auto simp add: card_of_Plus_Times_aux)
1.928 - hence ?thesis
1.929 - using card_of_Plus_commute card_of_Times_commute
1.930 - ordIso_ordLeq_trans ordLeq_ordIso_trans by metis
1.931 - }
1.932 - ultimately show ?thesis
1.933 - using card_of_Well_order[of A] card_of_Well_order[of B]
1.934 - ordLeq_total[of "|A|"] by metis
1.935 -qed
1.936 -
1.937 -
1.938 -lemma card_of_ordLeq_finite:
1.939 -assumes "|A| \<le>o |B|" and "finite B"
1.940 -shows "finite A"
1.941 -using assms unfolding ordLeq_def
1.942 -using embed_inj_on[of "|A|" "|B|"] embed_Field[of "|A|" "|B|"]
1.943 - Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce
1.944 -
1.945 -
1.946 -lemma card_of_ordLeq_infinite:
1.947 -assumes "|A| \<le>o |B|" and "infinite A"
1.948 -shows "infinite B"
1.949 -using assms card_of_ordLeq_finite by auto
1.950 -
1.951 -
1.952 -lemma card_of_ordIso_finite:
1.953 -assumes "|A| =o |B|"
1.954 -shows "finite A = finite B"
1.955 -using assms unfolding ordIso_def iso_def[abs_def]
1.956 -by (auto simp: bij_betw_finite Field_card_of)
1.957 -
1.958 -
1.959 -lemma card_of_ordIso_finite_Field:
1.960 -assumes "Card_order r" and "r =o |A|"
1.961 -shows "finite(Field r) = finite A"
1.962 -using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
1.963 -
1.964 -
1.965 -subsection {* Cardinals versus set operations involving infinite sets *}
1.966 -
1.967 -
1.968 -text{* Here we show that, for infinite sets, most set-theoretic constructions
1.969 -do not increase the cardinality. The cornerstone for this is
1.970 -theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
1.971 -does not increase cardinality -- the proof of this fact adapts a standard
1.972 -set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
1.973 -at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
1.974 -
1.975 -
1.976 -lemma infinite_iff_card_of_nat:
1.977 -"infinite A = ( |UNIV::nat set| \<le>o |A| )"
1.978 -by (auto simp add: infinite_iff_countable_subset card_of_ordLeq)
1.979 -
1.980 -
1.981 -lemma finite_iff_cardOf_nat:
1.982 -"finite A = ( |A| <o |UNIV :: nat set| )"
1.983 -using infinite_iff_card_of_nat[of A]
1.984 -not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
1.985 -by (fastforce simp: card_of_Well_order)
1.986 -
1.987 -lemma finite_ordLess_infinite2:
1.988 -assumes "finite A" and "infinite B"
1.989 -shows "|A| <o |B|"
1.990 -using assms
1.991 -finite_ordLess_infinite[of "|A|" "|B|"]
1.992 -card_of_Well_order[of A] card_of_Well_order[of B]
1.993 -Field_card_of[of A] Field_card_of[of B] by auto
1.994 -
1.995 -
1.996 -text{* The next two results correspond to the ZF fact that all infinite cardinals are
1.997 -limit ordinals: *}
1.998 -
1.999 -lemma Card_order_infinite_not_under:
1.1000 -assumes CARD: "Card_order r" and INF: "infinite (Field r)"
1.1001 -shows "\<not> (\<exists>a. Field r = rel.under r a)"
1.1002 -proof(auto)
1.1003 - have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
1.1004 - using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
1.1005 - fix a assume *: "Field r = rel.under r a"
1.1006 - show False
1.1007 - proof(cases "a \<in> Field r")
1.1008 - assume Case1: "a \<notin> Field r"
1.1009 - hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto
1.1010 - thus False using INF * by auto
1.1011 - next
1.1012 - let ?r' = "Restr r (rel.underS r a)"
1.1013 - assume Case2: "a \<in> Field r"
1.1014 - hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a"
1.1015 - using 0 rel.Refl_under_underS rel.underS_notIn by fastforce
1.1016 - have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r"
1.1017 - using 0 wo_rel.underS_ofilter * 1 Case2 by auto
1.1018 - hence "?r' <o r" using 0 using ofilter_ordLess by blast
1.1019 - moreover
1.1020 - have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
1.1021 - using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
1.1022 - ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto
1.1023 - moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
1.1024 - ultimately have "|rel.underS r a| <o |rel.under r a|"
1.1025 - using ordIso_symmetric ordLess_ordIso_trans by blast
1.1026 - moreover
1.1027 - {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)"
1.1028 - using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
1.1029 - hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast
1.1030 - }
1.1031 - ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
1.1032 - qed
1.1033 -qed
1.1034 -
1.1035 -
1.1036 -lemma infinite_Card_order_limit:
1.1037 -assumes r: "Card_order r" and "infinite (Field r)"
1.1038 -and a: "a : Field r"
1.1039 -shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
1.1040 -proof-
1.1041 - have "Field r \<noteq> rel.under r a"
1.1042 - using assms Card_order_infinite_not_under by blast
1.1043 - moreover have "rel.under r a \<le> Field r"
1.1044 - using rel.under_Field .
1.1045 - ultimately have "rel.under r a < Field r" by blast
1.1046 - then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
1.1047 - unfolding rel.under_def by blast
1.1048 - moreover have ba: "b \<noteq> a"
1.1049 - using 1 r unfolding card_order_on_def well_order_on_def
1.1050 - linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
1.1051 - ultimately have "(a,b) : r"
1.1052 - using a r unfolding card_order_on_def well_order_on_def linear_order_on_def
1.1053 - total_on_def by blast
1.1054 - thus ?thesis using 1 ba by auto
1.1055 -qed
1.1056 -
1.1057 -
1.1058 -theorem Card_order_Times_same_infinite:
1.1059 -assumes CO: "Card_order r" and INF: "infinite(Field r)"
1.1060 -shows "|Field r \<times> Field r| \<le>o r"
1.1061 -proof-
1.1062 - obtain phi where phi_def:
1.1063 - "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and>
1.1064 - \<not> |Field r \<times> Field r| \<le>o r )" by blast
1.1065 - have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
1.1066 - unfolding phi_def card_order_on_def by auto
1.1067 - have Ft: "\<not>(\<exists>r. phi r)"
1.1068 - proof
1.1069 - assume "\<exists>r. phi r"
1.1070 - hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}"
1.1071 - using temp1 by auto
1.1072 - then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and
1.1073 - 3: "Card_order r \<and> Well_order r"
1.1074 - using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast
1.1075 - let ?A = "Field r" let ?r' = "bsqr r"
1.1076 - have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r"
1.1077 - using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast
1.1078 - have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|"
1.1079 - using card_of_Card_order card_of_Well_order by blast
1.1080 - (* *)
1.1081 - have "r <o |?A \<times> ?A|"
1.1082 - using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast
1.1083 - moreover have "|?A \<times> ?A| \<le>o ?r'"
1.1084 - using card_of_least[of "?A \<times> ?A"] 4 by auto
1.1085 - ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto
1.1086 - then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)"
1.1087 - unfolding ordLess_def embedS_def[abs_def]
1.1088 - by (auto simp add: Field_bsqr)
1.1089 - let ?B = "f ` ?A"
1.1090 - have "|?A| =o |?B|"
1.1091 - using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast
1.1092 - hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast
1.1093 - (* *)
1.1094 - have "wo_rel.ofilter ?r' ?B"
1.1095 - using 6 embed_Field_ofilter 3 4 by blast
1.1096 - hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'"
1.1097 - using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
1.1098 - hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
1.1099 - using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
1.1100 - have "\<not> (\<exists>a. Field r = rel.under r a)"
1.1101 - using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
1.1102 - then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
1.1103 - using temp2 3 bsqr_ofilter[of r ?B] by blast
1.1104 - hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast
1.1105 - hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast
1.1106 - let ?r1 = "Restr r A1"
1.1107 - have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast
1.1108 - moreover
1.1109 - {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast
1.1110 - hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast
1.1111 - }
1.1112 - ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
1.1113 - (* *)
1.1114 - have "infinite (Field r)" using 1 unfolding phi_def by simp
1.1115 - hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
1.1116 - hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast
1.1117 - moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
1.1118 - using card_of_Card_order[of A1] card_of_Well_order[of A1]
1.1119 - by (simp add: Field_card_of)
1.1120 - moreover have "\<not> r \<le>o | A1 |"
1.1121 - using temp4 11 3 using not_ordLeq_iff_ordLess by blast
1.1122 - ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
1.1123 - by (simp add: card_of_card_order_on)
1.1124 - hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
1.1125 - using 2 unfolding phi_def by blast
1.1126 - hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto
1.1127 - hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast
1.1128 - thus False using 11 not_ordLess_ordLeq by auto
1.1129 - qed
1.1130 - thus ?thesis using assms unfolding phi_def by blast
1.1131 -qed
1.1132 -
1.1133 -
1.1134 -corollary card_of_Times_same_infinite:
1.1135 -assumes "infinite A"
1.1136 -shows "|A \<times> A| =o |A|"
1.1137 -proof-
1.1138 - let ?r = "|A|"
1.1139 - have "Field ?r = A \<and> Card_order ?r"
1.1140 - using Field_card_of card_of_Card_order[of A] by fastforce
1.1141 - hence "|A \<times> A| \<le>o |A|"
1.1142 - using Card_order_Times_same_infinite[of ?r] assms by auto
1.1143 - thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast
1.1144 -qed
1.1145 -
1.1146 -
1.1147 -lemma card_of_Times_infinite:
1.1148 -assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
1.1149 -shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
1.1150 -proof-
1.1151 - have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
1.1152 - using assms by (simp add: card_of_Times1 card_of_Times2)
1.1153 - moreover
1.1154 - {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|"
1.1155 - using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast
1.1156 - moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast
1.1157 - ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|"
1.1158 - using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto
1.1159 - }
1.1160 - ultimately show ?thesis by (simp add: ordIso_iff_ordLeq)
1.1161 -qed
1.1162 -
1.1163 -
1.1164 -corollary card_of_Times_infinite_simps:
1.1165 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
1.1166 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
1.1167 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
1.1168 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
1.1169 -by (auto simp add: card_of_Times_infinite ordIso_symmetric)
1.1170 -
1.1171 -
1.1172 -corollary Card_order_Times_infinite:
1.1173 -assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
1.1174 - NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
1.1175 -shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
1.1176 -proof-
1.1177 - have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|"
1.1178 - using assms by (simp add: card_of_Times_infinite card_of_mono2)
1.1179 - thus ?thesis
1.1180 - using assms card_of_Field_ordIso[of r]
1.1181 - ordIso_transitive[of "|Field r \<times> Field p|"]
1.1182 - ordIso_transitive[of _ "|Field r|"] by blast
1.1183 -qed
1.1184 -
1.1185 -
1.1186 -lemma card_of_Sigma_ordLeq_infinite:
1.1187 -assumes INF: "infinite B" and
1.1188 - LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1.1189 -shows "|SIGMA i : I. A i| \<le>o |B|"
1.1190 -proof(cases "I = {}", simp add: card_of_empty)
1.1191 - assume *: "I \<noteq> {}"
1.1192 - have "|SIGMA i : I. A i| \<le>o |I \<times> B|"
1.1193 - using LEQ card_of_Sigma_Times by blast
1.1194 - moreover have "|I \<times> B| =o |B|"
1.1195 - using INF * LEQ_I by (auto simp add: card_of_Times_infinite)
1.1196 - ultimately show ?thesis using ordLeq_ordIso_trans by blast
1.1197 -qed
1.1198 -
1.1199 -
1.1200 -lemma card_of_Sigma_ordLeq_infinite_Field:
1.1201 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
1.1202 - LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1.1203 -shows "|SIGMA i : I. A i| \<le>o r"
1.1204 -proof-
1.1205 - let ?B = "Field r"
1.1206 - have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1.1207 - ordIso_symmetric by blast
1.1208 - hence "|I| \<le>o |?B|" "\<forall>i \<in> I. |A i| \<le>o |?B|"
1.1209 - using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1.1210 - hence "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ
1.1211 - card_of_Sigma_ordLeq_infinite by blast
1.1212 - thus ?thesis using 1 ordLeq_ordIso_trans by blast
1.1213 -qed
1.1214 -
1.1215 -
1.1216 -lemma card_of_Times_ordLeq_infinite_Field:
1.1217 -"\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
1.1218 - \<Longrightarrow> |A <*> B| \<le>o r"
1.1219 -by(simp add: card_of_Sigma_ordLeq_infinite_Field)
1.1220 -
1.1221 -
1.1222 -lemma card_of_UNION_ordLeq_infinite:
1.1223 -assumes INF: "infinite B" and
1.1224 - LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
1.1225 -shows "|\<Union> i \<in> I. A i| \<le>o |B|"
1.1226 -proof(cases "I = {}", simp add: card_of_empty)
1.1227 - assume *: "I \<noteq> {}"
1.1228 - have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
1.1229 - using card_of_UNION_Sigma by blast
1.1230 - moreover have "|SIGMA i : I. A i| \<le>o |B|"
1.1231 - using assms card_of_Sigma_ordLeq_infinite by blast
1.1232 - ultimately show ?thesis using ordLeq_transitive by blast
1.1233 -qed
1.1234 -
1.1235 -
1.1236 -corollary card_of_UNION_ordLeq_infinite_Field:
1.1237 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
1.1238 - LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
1.1239 -shows "|\<Union> i \<in> I. A i| \<le>o r"
1.1240 -proof-
1.1241 - let ?B = "Field r"
1.1242 - have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
1.1243 - ordIso_symmetric by blast
1.1244 - hence "|I| \<le>o |?B|" "\<forall>i \<in> I. |A i| \<le>o |?B|"
1.1245 - using LEQ_I LEQ ordLeq_ordIso_trans by blast+
1.1246 - hence "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
1.1247 - card_of_UNION_ordLeq_infinite by blast
1.1248 - thus ?thesis using 1 ordLeq_ordIso_trans by blast
1.1249 -qed
1.1250 -
1.1251 -
1.1252 -lemma card_of_Plus_infinite1:
1.1253 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
1.1254 -shows "|A <+> B| =o |A|"
1.1255 -proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
1.1256 - let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b" let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
1.1257 - assume *: "B \<noteq> {}"
1.1258 - then obtain b1 where 1: "b1 \<in> B" by blast
1.1259 - show ?thesis
1.1260 - proof(cases "B = {b1}")
1.1261 - assume Case1: "B = {b1}"
1.1262 - have 2: "bij_betw ?Inl A ((?Inl ` A))"
1.1263 - unfolding bij_betw_def inj_on_def by auto
1.1264 - hence 3: "infinite (?Inl ` A)"
1.1265 - using INF bij_betw_finite[of ?Inl A] by blast
1.1266 - let ?A' = "?Inl ` A \<union> {?Inr b1}"
1.1267 - obtain g where "bij_betw g (?Inl ` A) ?A'"
1.1268 - using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto
1.1269 - moreover have "?A' = A <+> B" using Case1 by blast
1.1270 - ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp
1.1271 - hence "bij_betw (g o ?Inl) A (A <+> B)"
1.1272 - using 2 by (auto simp add: bij_betw_trans)
1.1273 - thus ?thesis using card_of_ordIso ordIso_symmetric by blast
1.1274 - next
1.1275 - assume Case2: "B \<noteq> {b1}"
1.1276 - with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce
1.1277 - obtain f where "inj_on f B \<and> f ` B \<le> A"
1.1278 - using LEQ card_of_ordLeq[of B] by fastforce
1.1279 - with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A"
1.1280 - unfolding inj_on_def by auto
1.1281 - with 3 have "|A <+> B| \<le>o |A \<times> B|"
1.1282 - by (auto simp add: card_of_Plus_Times)
1.1283 - moreover have "|A \<times> B| =o |A|"
1.1284 - using assms * by (simp add: card_of_Times_infinite_simps)
1.1285 - ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
1.1286 - thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
1.1287 - qed
1.1288 -qed
1.1289 -
1.1290 -
1.1291 -lemma card_of_Plus_infinite2:
1.1292 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
1.1293 -shows "|B <+> A| =o |A|"
1.1294 -using assms card_of_Plus_commute card_of_Plus_infinite1
1.1295 -ordIso_equivalence by blast
1.1296 -
1.1297 -
1.1298 -lemma card_of_Plus_infinite:
1.1299 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
1.1300 -shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
1.1301 -using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
1.1302 -
1.1303 -
1.1304 -corollary Card_order_Plus_infinite:
1.1305 -assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
1.1306 - LEQ: "p \<le>o r"
1.1307 -shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
1.1308 -proof-
1.1309 - have "| Field r <+> Field p | =o | Field r | \<and>
1.1310 - | Field p <+> Field r | =o | Field r |"
1.1311 - using assms by (simp add: card_of_Plus_infinite card_of_mono2)
1.1312 - thus ?thesis
1.1313 - using assms card_of_Field_ordIso[of r]
1.1314 - ordIso_transitive[of "|Field r <+> Field p|"]
1.1315 - ordIso_transitive[of _ "|Field r|"] by blast
1.1316 -qed
1.1317 -
1.1318 -
1.1319 -lemma card_of_Un_infinite:
1.1320 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
1.1321 -shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
1.1322 -proof-
1.1323 - have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
1.1324 - moreover have "|A <+> B| =o |A|"
1.1325 - using assms by (metis card_of_Plus_infinite)
1.1326 - ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
1.1327 - hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast
1.1328 - thus ?thesis using Un_commute[of B A] by auto
1.1329 -qed
1.1330 -
1.1331 -
1.1332 -lemma card_of_Un_diff_infinite:
1.1333 -assumes INF: "infinite A" and LESS: "|B| <o |A|"
1.1334 -shows "|A - B| =o |A|"
1.1335 -proof-
1.1336 - obtain C where C_def: "C = A - B" by blast
1.1337 - have "|A \<union> B| =o |A|"
1.1338 - using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast
1.1339 - moreover have "C \<union> B = A \<union> B" unfolding C_def by auto
1.1340 - ultimately have 1: "|C \<union> B| =o |A|" by auto
1.1341 - (* *)
1.1342 - {assume *: "|C| \<le>o |B|"
1.1343 - moreover
1.1344 - {assume **: "finite B"
1.1345 - hence "finite C"
1.1346 - using card_of_ordLeq_finite * by blast
1.1347 - hence False using ** INF card_of_ordIso_finite 1 by blast
1.1348 - }
1.1349 - hence "infinite B" by auto
1.1350 - ultimately have False
1.1351 - using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
1.1352 - }
1.1353 - hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast
1.1354 - {assume *: "finite C"
1.1355 - hence "finite B" using card_of_ordLeq_finite 2 by blast
1.1356 - hence False using * INF card_of_ordIso_finite 1 by blast
1.1357 - }
1.1358 - hence "infinite C" by auto
1.1359 - hence "|C| =o |A|"
1.1360 - using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
1.1361 - thus ?thesis unfolding C_def .
1.1362 -qed
1.1363 -
1.1364 -
1.1365 -lemma card_of_Plus_ordLess_infinite:
1.1366 -assumes INF: "infinite C" and
1.1367 - LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
1.1368 -shows "|A <+> B| <o |C|"
1.1369 -proof(cases "A = {} \<or> B = {}")
1.1370 - assume Case1: "A = {} \<or> B = {}"
1.1371 - hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|"
1.1372 - using card_of_Plus_empty1 card_of_Plus_empty2 by blast
1.1373 - hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|"
1.1374 - using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast
1.1375 - thus ?thesis using LESS1 LESS2
1.1376 - ordIso_ordLess_trans[of "|A <+> B|" "|A|"]
1.1377 - ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast
1.1378 -next
1.1379 - assume Case2: "\<not>(A = {} \<or> B = {})"
1.1380 - {assume *: "|C| \<le>o |A <+> B|"
1.1381 - hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast
1.1382 - hence 1: "infinite A \<or> infinite B" using finite_Plus by blast
1.1383 - {assume Case21: "|A| \<le>o |B|"
1.1384 - hence "infinite B" using 1 card_of_ordLeq_finite by blast
1.1385 - hence "|A <+> B| =o |B|" using Case2 Case21
1.1386 - by (auto simp add: card_of_Plus_infinite)
1.1387 - hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1.1388 - }
1.1389 - moreover
1.1390 - {assume Case22: "|B| \<le>o |A|"
1.1391 - hence "infinite A" using 1 card_of_ordLeq_finite by blast
1.1392 - hence "|A <+> B| =o |A|" using Case2 Case22
1.1393 - by (auto simp add: card_of_Plus_infinite)
1.1394 - hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
1.1395 - }
1.1396 - ultimately have False using ordLeq_total card_of_Well_order[of A]
1.1397 - card_of_Well_order[of B] by blast
1.1398 - }
1.1399 - thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"]
1.1400 - card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto
1.1401 -qed
1.1402 -
1.1403 -
1.1404 -lemma card_of_Plus_ordLess_infinite_Field:
1.1405 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
1.1406 - LESS1: "|A| <o r" and LESS2: "|B| <o r"
1.1407 -shows "|A <+> B| <o r"
1.1408 -proof-
1.1409 - let ?C = "Field r"
1.1410 - have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso
1.1411 - ordIso_symmetric by blast
1.1412 - hence "|A| <o |?C|" "|B| <o |?C|"
1.1413 - using LESS1 LESS2 ordLess_ordIso_trans by blast+
1.1414 - hence "|A <+> B| <o |?C|" using INF
1.1415 - card_of_Plus_ordLess_infinite by blast
1.1416 - thus ?thesis using 1 ordLess_ordIso_trans by blast
1.1417 -qed
1.1418 -
1.1419 -
1.1420 -lemma infinite_card_of_insert:
1.1421 -assumes "infinite A"
1.1422 -shows "|insert a A| =o |A|"
1.1423 -proof-
1.1424 - have iA: "insert a A = A \<union> {a}" by simp
1.1425 - show ?thesis
1.1426 - using infinite_imp_bij_betw2[OF assms] unfolding iA
1.1427 - by (metis bij_betw_inv card_of_ordIso)
1.1428 -qed
1.1429 -
1.1430 -
1.1431 -subsection {* Cardinals versus lists *}
1.1432 -
1.1433 -
1.1434 -text{* The next is an auxiliary operator, which shall be used for inductive
1.1435 -proofs of facts concerning the cardinality of @{text "List"} : *}
1.1436 -
1.1437 -definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set"
1.1438 -where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}"
1.1439 -
1.1440 -
1.1441 -lemma lists_def2: "lists A = {l. set l \<le> A}"
1.1442 -using in_listsI by blast
1.1443 -
1.1444 -
1.1445 -lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
1.1446 -unfolding lists_def2 nlists_def by blast
1.1447 -
1.1448 -
1.1449 -lemma card_of_lists: "|A| \<le>o |lists A|"
1.1450 -proof-
1.1451 - let ?h = "\<lambda> a. [a]"
1.1452 - have "inj_on ?h A \<and> ?h ` A \<le> lists A"
1.1453 - unfolding inj_on_def lists_def2 by auto
1.1454 - thus ?thesis by (metis card_of_ordLeq)
1.1455 -qed
1.1456 -
1.1457 -
1.1458 -lemma nlists_0: "nlists A 0 = {[]}"
1.1459 -unfolding nlists_def by auto
1.1460 -
1.1461 -
1.1462 -lemma nlists_not_empty:
1.1463 -assumes "A \<noteq> {}"
1.1464 -shows "nlists A n \<noteq> {}"
1.1465 -proof(induct n, simp add: nlists_0)
1.1466 - fix n assume "nlists A n \<noteq> {}"
1.1467 - then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto
1.1468 - hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto
1.1469 - thus "nlists A (Suc n) \<noteq> {}" by auto
1.1470 -qed
1.1471 -
1.1472 -
1.1473 -lemma Nil_in_lists: "[] \<in> lists A"
1.1474 -unfolding lists_def2 by auto
1.1475 -
1.1476 -
1.1477 -lemma lists_not_empty: "lists A \<noteq> {}"
1.1478 -using Nil_in_lists by blast
1.1479 -
1.1480 -
1.1481 -lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
1.1482 -proof-
1.1483 - let ?B = "A \<times> (nlists A n)" let ?h = "\<lambda>(a,l). a # l"
1.1484 - have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)"
1.1485 - unfolding inj_on_def nlists_def by auto
1.1486 - moreover have "nlists A (Suc n) \<le> ?h ` ?B"
1.1487 - proof(auto)
1.1488 - fix l assume "l \<in> nlists A (Suc n)"
1.1489 - hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto
1.1490 - then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv)
1.1491 - hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto
1.1492 - thus "l \<in> ?h ` ?B" using 2 unfolding nlists_def by auto
1.1493 - qed
1.1494 - ultimately have "bij_betw ?h ?B (nlists A (Suc n))"
1.1495 - unfolding bij_betw_def by auto
1.1496 - thus ?thesis using card_of_ordIso ordIso_symmetric by blast
1.1497 -qed
1.1498 -
1.1499 -
1.1500 -lemma card_of_nlists_infinite:
1.1501 -assumes "infinite A"
1.1502 -shows "|nlists A n| \<le>o |A|"
1.1503 -proof(induct n)
1.1504 - have "A \<noteq> {}" using assms by auto
1.1505 - thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq)
1.1506 -next
1.1507 - fix n assume IH: "|nlists A n| \<le>o |A|"
1.1508 - have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
1.1509 - using card_of_nlists_Succ by blast
1.1510 - moreover
1.1511 - {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast
1.1512 - hence "|A \<times> (nlists A n)| =o |A|"
1.1513 - using assms IH by (auto simp add: card_of_Times_infinite)
1.1514 - }
1.1515 - ultimately show "|nlists A (Suc n)| \<le>o |A|"
1.1516 - using ordIso_transitive ordIso_iff_ordLeq by blast
1.1517 -qed
1.1518 -
1.1519 -
1.1520 -lemma card_of_lists_infinite:
1.1521 -assumes "infinite A"
1.1522 -shows "|lists A| =o |A|"
1.1523 -proof-
1.1524 - have "|lists A| \<le>o |A|"
1.1525 - using assms
1.1526 - by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite
1.1527 - infinite_iff_card_of_nat card_of_nlists_infinite)
1.1528 - thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
1.1529 -qed
1.1530 -
1.1531 -
1.1532 -lemma Card_order_lists_infinite:
1.1533 -assumes "Card_order r" and "infinite(Field r)"
1.1534 -shows "|lists(Field r)| =o r"
1.1535 -using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
1.1536 -
1.1537 -
1.1538 -
1.1539 -subsection {* The cardinal $\omega$ and the finite cardinals *}
1.1540 -
1.1541 -
1.1542 -text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.1543 -order relation on
1.1544 -@{text "nat"}, that we abbreviate by @{text "natLeq"}. The finite cardinals
1.1545 -shall be the restrictions of these relations to the numbers smaller than
1.1546 -fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
1.1547 -
1.1548 -abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.1549 -abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.1550 -
1.1551 -abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
1.1552 -where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
1.1553 -
1.1554 -lemma infinite_cartesian_product:
1.1555 -assumes "infinite A" "infinite B"
1.1556 -shows "infinite (A \<times> B)"
1.1557 -proof
1.1558 - assume "finite (A \<times> B)"
1.1559 - from assms(1) have "A \<noteq> {}" by auto
1.1560 - with `finite (A \<times> B)` have "finite B" using finite_cartesian_productD2 by auto
1.1561 - with assms(2) show False by simp
1.1562 -qed
1.1563 -
1.1564 -
1.1565 -
1.1566 -subsubsection {* First as well-orders *}
1.1567 -
1.1568 -
1.1569 -lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
1.1570 -by(unfold Field_def, auto)
1.1571 -
1.1572 -
1.1573 -lemma natLeq_Refl: "Refl natLeq"
1.1574 -unfolding refl_on_def Field_def by auto
1.1575 -
1.1576 -
1.1577 -lemma natLeq_trans: "trans natLeq"
1.1578 -unfolding trans_def by auto
1.1579 -
1.1580 -
1.1581 -lemma natLeq_Preorder: "Preorder natLeq"
1.1582 -unfolding preorder_on_def
1.1583 -by (auto simp add: natLeq_Refl natLeq_trans)
1.1584 -
1.1585 -
1.1586 -lemma natLeq_antisym: "antisym natLeq"
1.1587 -unfolding antisym_def by auto
1.1588 -
1.1589 -
1.1590 -lemma natLeq_Partial_order: "Partial_order natLeq"
1.1591 -unfolding partial_order_on_def
1.1592 -by (auto simp add: natLeq_Preorder natLeq_antisym)
1.1593 -
1.1594 -
1.1595 -lemma natLeq_Total: "Total natLeq"
1.1596 -unfolding total_on_def by auto
1.1597 -
1.1598 -
1.1599 -lemma natLeq_Linear_order: "Linear_order natLeq"
1.1600 -unfolding linear_order_on_def
1.1601 -by (auto simp add: natLeq_Partial_order natLeq_Total)
1.1602 -
1.1603 -
1.1604 -lemma natLeq_natLess_Id: "natLess = natLeq - Id"
1.1605 -by auto
1.1606 -
1.1607 -
1.1608 -lemma natLeq_Well_order: "Well_order natLeq"
1.1609 -unfolding well_order_on_def
1.1610 -using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
1.1611 -
1.1612 -
1.1613 -corollary natLeq_well_order_on: "well_order_on UNIV natLeq"
1.1614 -using natLeq_Well_order Field_natLeq by auto
1.1615 -
1.1616 -
1.1617 -lemma natLeq_wo_rel: "wo_rel natLeq"
1.1618 -unfolding wo_rel_def using natLeq_Well_order .
1.1619 -
1.1620 -
1.1621 -lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
1.1622 -using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
1.1623 -
1.1624 -
1.1625 -lemma closed_nat_set_iff:
1.1626 -assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
1.1627 -shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
1.1628 -proof-
1.1629 - {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
1.1630 - moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
1.1631 - ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
1.1632 - using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
1.1633 - have "A = {0 ..< n}"
1.1634 - proof(auto simp add: 1)
1.1635 - fix m assume *: "m \<in> A"
1.1636 - {assume "n \<le> m" with assms * have "n \<in> A" by blast
1.1637 - hence False using 1 by auto
1.1638 - }
1.1639 - thus "m < n" by fastforce
1.1640 - qed
1.1641 - hence "\<exists>n. A = {0 ..< n}" by blast
1.1642 - }
1.1643 - thus ?thesis by blast
1.1644 -qed
1.1645 -
1.1646 -
1.1647 -lemma Field_natLeq_on: "Field (natLeq_on n) = {0 ..< n}"
1.1648 -unfolding Field_def by auto
1.1649 -
1.1650 -
1.1651 -lemma natLeq_underS_less: "rel.underS natLeq n = {0 ..< n}"
1.1652 -unfolding rel.underS_def by auto
1.1653 -
1.1654 -
1.1655 -lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n"
1.1656 -by auto
1.1657 -
1.1658 -
1.1659 -lemma Restr_natLeq2:
1.1660 -"Restr natLeq (rel.underS natLeq n) = natLeq_on n"
1.1661 -by (auto simp add: Restr_natLeq natLeq_underS_less)
1.1662 -
1.1663 -
1.1664 -lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
1.1665 -using Restr_natLeq[of n] natLeq_Well_order
1.1666 - Well_order_Restr[of natLeq "{0..<n}"] by auto
1.1667 -
1.1668 -
1.1669 -corollary natLeq_on_well_order_on: "well_order_on {0 ..< n} (natLeq_on n)"
1.1670 -using natLeq_on_Well_order Field_natLeq_on by auto
1.1671 -
1.1672 -
1.1673 -lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)"
1.1674 -unfolding wo_rel_def using natLeq_on_Well_order .
1.1675 -
1.1676 -
1.1677 -lemma natLeq_on_ofilter_less_eq:
1.1678 -"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
1.1679 -by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
1.1680 - simp add: Field_natLeq_on, unfold rel.under_def, auto)
1.1681 -
1.1682 -
1.1683 -lemma natLeq_on_ofilter_iff:
1.1684 -"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
1.1685 -proof(rule iffI)
1.1686 - assume *: "wo_rel.ofilter (natLeq_on m) A"
1.1687 - hence 1: "A \<le> {0..<m}"
1.1688 - by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
1.1689 - hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
1.1690 - using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
1.1691 - hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
1.1692 - thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
1.1693 -next
1.1694 - assume "(\<exists>n\<le>m. A = {0 ..< n})"
1.1695 - thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
1.1696 -qed
1.1697 -
1.1698 -
1.1699 -
1.1700 -subsubsection {* Then as cardinals *}
1.1701 -
1.1702 -
1.1703 -lemma natLeq_Card_order: "Card_order natLeq"
1.1704 -proof(auto simp add: natLeq_Well_order
1.1705 - Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq)
1.1706 - fix n have "finite(Field (natLeq_on n))"
1.1707 - unfolding Field_natLeq_on by auto
1.1708 - moreover have "infinite(UNIV::nat set)" by auto
1.1709 - ultimately show "natLeq_on n <o |UNIV::nat set|"
1.1710 - using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
1.1711 - Field_card_of[of "UNIV::nat set"]
1.1712 - card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto
1.1713 -qed
1.1714 -
1.1715 -
1.1716 -corollary card_of_Field_natLeq:
1.1717 -"|Field natLeq| =o natLeq"
1.1718 -using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq]
1.1719 - ordIso_symmetric[of natLeq] by blast
1.1720 -
1.1721 -
1.1722 -corollary card_of_nat:
1.1723 -"|UNIV::nat set| =o natLeq"
1.1724 -using Field_natLeq card_of_Field_natLeq by auto
1.1725 -
1.1726 -
1.1727 -corollary infinite_iff_natLeq_ordLeq:
1.1728 -"infinite A = ( natLeq \<le>o |A| )"
1.1729 -using infinite_iff_card_of_nat[of A] card_of_nat
1.1730 - ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
1.1731 -
1.1732 -
1.1733 -corollary finite_iff_ordLess_natLeq:
1.1734 -"finite A = ( |A| <o natLeq)"
1.1735 -using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
1.1736 - card_of_Well_order natLeq_Well_order by blast
1.1737 -
1.1738 -
1.1739 -lemma ordIso_natLeq_on_imp_finite:
1.1740 -"|A| =o natLeq_on n \<Longrightarrow> finite A"
1.1741 -unfolding ordIso_def iso_def[abs_def]
1.1742 -by (auto simp: Field_natLeq_on bij_betw_finite Field_card_of)
1.1743 -
1.1744 -
1.1745 -lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
1.1746 -proof(unfold card_order_on_def,
1.1747 - auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
1.1748 - fix r assume "well_order_on {0..<n} r"
1.1749 - thus "natLeq_on n \<le>o r"
1.1750 - using finite_atLeastLessThan natLeq_on_well_order_on
1.1751 - finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
1.1752 -qed
1.1753 -
1.1754 -
1.1755 -corollary card_of_Field_natLeq_on:
1.1756 -"|Field (natLeq_on n)| =o natLeq_on n"
1.1757 -using Field_natLeq_on natLeq_on_Card_order
1.1758 - Card_order_iff_ordIso_card_of[of "natLeq_on n"]
1.1759 - ordIso_symmetric[of "natLeq_on n"] by blast
1.1760 -
1.1761 -
1.1762 -corollary card_of_less:
1.1763 -"|{0 ..< n}| =o natLeq_on n"
1.1764 -using Field_natLeq_on card_of_Field_natLeq_on by auto
1.1765 -
1.1766 -
1.1767 -lemma natLeq_on_ordLeq_less_eq:
1.1768 -"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
1.1769 -proof
1.1770 - assume "natLeq_on m \<le>o natLeq_on n"
1.1771 - then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
1.1772 - unfolding ordLeq_def using
1.1773 - embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
1.1774 - embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
1.1775 - thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
1.1776 -next
1.1777 - assume "m \<le> n"
1.1778 - hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
1.1779 - hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
1.1780 - thus "natLeq_on m \<le>o natLeq_on n"
1.1781 - using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
1.1782 -qed
1.1783 -
1.1784 -
1.1785 -lemma natLeq_on_ordLeq_less:
1.1786 -"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
1.1787 -using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
1.1788 -natLeq_on_Well_order natLeq_on_ordLeq_less_eq by auto
1.1789 -
1.1790 -
1.1791 -
1.1792 -subsubsection {* "Backwards compatibility" with the numeric cardinal operator for finite sets *}
1.1793 -
1.1794 -
1.1795 -lemma finite_card_of_iff_card2:
1.1796 -assumes FIN: "finite A" and FIN': "finite B"
1.1797 -shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
1.1798 -using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
1.1799 -
1.1800 -
1.1801 -lemma finite_imp_card_of_natLeq_on:
1.1802 -assumes "finite A"
1.1803 -shows "|A| =o natLeq_on (card A)"
1.1804 -proof-
1.1805 - obtain h where "bij_betw h A {0 ..< card A}"
1.1806 - using assms ex_bij_betw_finite_nat by blast
1.1807 - thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
1.1808 -qed
1.1809 -
1.1810 -
1.1811 -lemma finite_iff_card_of_natLeq_on:
1.1812 -"finite A = (\<exists>n. |A| =o natLeq_on n)"
1.1813 -using finite_imp_card_of_natLeq_on[of A]
1.1814 -by(auto simp add: ordIso_natLeq_on_imp_finite)
1.1815 -
1.1816 -
1.1817 -
1.1818 -subsection {* The successor of a cardinal *}
1.1819 -
1.1820 -
1.1821 -text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.1822 -being a successor cardinal of @{text "r"}. Although the definition does
1.1823 -not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
1.1824 -
1.1825 -
1.1826 -definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1.1827 -where
1.1828 -"isCardSuc r r' \<equiv>
1.1829 - Card_order r' \<and> r <o r' \<and>
1.1830 - (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
1.1831 -
1.1832 -
1.1833 -text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},
1.1834 -by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
1.1835 -Again, the picked item shall be proved unique up to order-isomorphism. *}
1.1836 -
1.1837 -
1.1838 -definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
1.1839 -where
1.1840 -"cardSuc r \<equiv> SOME r'. isCardSuc r r'"
1.1841 -
1.1842 -
1.1843 -lemma exists_minim_Card_order:
1.1844 -"\<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.1845 -unfolding card_order_on_def using exists_minim_Well_order by blast
1.1846 -
1.1847 -
1.1848 -lemma exists_isCardSuc:
1.1849 -assumes "Card_order r"
1.1850 -shows "\<exists>r'. isCardSuc r r'"
1.1851 -proof-
1.1852 - let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}"
1.1853 - have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms
1.1854 - by (simp add: card_of_Card_order Card_order_Pow)
1.1855 - then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')"
1.1856 - using exists_minim_Card_order[of ?R] by blast
1.1857 - thus ?thesis unfolding isCardSuc_def by auto
1.1858 -qed
1.1859 -
1.1860 -
1.1861 -lemma cardSuc_isCardSuc:
1.1862 -assumes "Card_order r"
1.1863 -shows "isCardSuc r (cardSuc r)"
1.1864 -unfolding cardSuc_def using assms
1.1865 -by (simp add: exists_isCardSuc someI_ex)
1.1866 -
1.1867 -
1.1868 -lemma cardSuc_Card_order:
1.1869 -"Card_order r \<Longrightarrow> Card_order(cardSuc r)"
1.1870 -using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1871 -
1.1872 -
1.1873 -lemma cardSuc_greater:
1.1874 -"Card_order r \<Longrightarrow> r <o cardSuc r"
1.1875 -using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1876 -
1.1877 -
1.1878 -lemma cardSuc_ordLeq:
1.1879 -"Card_order r \<Longrightarrow> r \<le>o cardSuc r"
1.1880 -using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1.1881 -
1.1882 -
1.1883 -text{* The minimality property of @{text "cardSuc"} originally present in its definition
1.1884 -is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
1.1885 -
1.1886 -lemma cardSuc_least_aux:
1.1887 -"\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
1.1888 -using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.1889 -
1.1890 -
1.1891 -text{* But from this we can infer general minimality: *}
1.1892 -
1.1893 -lemma cardSuc_least:
1.1894 -assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
1.1895 -shows "cardSuc r \<le>o r'"
1.1896 -proof-
1.1897 - let ?p = "cardSuc r"
1.1898 - have 0: "Well_order ?p \<and> Well_order r'"
1.1899 - using assms cardSuc_Card_order unfolding card_order_on_def by blast
1.1900 - {assume "r' <o ?p"
1.1901 - then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p"
1.1902 - using internalize_ordLess[of r' ?p] by blast
1.1903 - (* *)
1.1904 - have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast
1.1905 - moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast
1.1906 - ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast
1.1907 - hence False using 2 not_ordLess_ordLeq by blast
1.1908 - }
1.1909 - thus ?thesis using 0 ordLess_or_ordLeq by blast
1.1910 -qed
1.1911 -
1.1912 -
1.1913 -lemma cardSuc_ordLess_ordLeq:
1.1914 -assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1915 -shows "(r <o r') = (cardSuc r \<le>o r')"
1.1916 -proof(auto simp add: assms cardSuc_least)
1.1917 - assume "cardSuc r \<le>o r'"
1.1918 - thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast
1.1919 -qed
1.1920 -
1.1921 -
1.1922 -lemma cardSuc_ordLeq_ordLess:
1.1923 -assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1924 -shows "(r' <o cardSuc r) = (r' \<le>o r)"
1.1925 -proof-
1.1926 - have "Well_order r \<and> Well_order r'"
1.1927 - using assms unfolding card_order_on_def by auto
1.1928 - moreover have "Well_order(cardSuc r)"
1.1929 - using assms cardSuc_Card_order card_order_on_def by blast
1.1930 - ultimately show ?thesis
1.1931 - using assms cardSuc_ordLess_ordLeq[of r r']
1.1932 - not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast
1.1933 -qed
1.1934 -
1.1935 -
1.1936 -lemma cardSuc_mono_ordLeq:
1.1937 -assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1938 -shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')"
1.1939 -using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast
1.1940 -
1.1941 -
1.1942 -lemma cardSuc_invar_ordIso:
1.1943 -assumes CARD: "Card_order r" and CARD': "Card_order r'"
1.1944 -shows "(cardSuc r =o cardSuc r') = (r =o r')"
1.1945 -proof-
1.1946 - have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')"
1.1947 - using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order)
1.1948 - thus ?thesis
1.1949 - using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq
1.1950 - using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast
1.1951 -qed
1.1952 -
1.1953 -
1.1954 -lemma cardSuc_natLeq_on_Suc:
1.1955 -"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
1.1956 -proof-
1.1957 - obtain r r' p where r_def: "r = natLeq_on n" and
1.1958 - r'_def: "r' = cardSuc(natLeq_on n)" and
1.1959 - p_def: "p = natLeq_on(Suc n)" by blast
1.1960 - (* Preliminary facts: *)
1.1961 - have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
1.1962 - using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
1.1963 - hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
1.1964 - unfolding card_order_on_def by force
1.1965 - have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
1.1966 - unfolding r_def p_def Field_natLeq_on by simp
1.1967 - hence FIN: "finite (Field r)" by force
1.1968 - have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
1.1969 - hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
1.1970 - hence LESS: "|Field r| <o |Field r'|"
1.1971 - using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
1.1972 - (* Main proof: *)
1.1973 - have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
1.1974 - using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
1.1975 - moreover have "p \<le>o r'"
1.1976 - proof-
1.1977 - {assume "r' <o p"
1.1978 - then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
1.1979 - let ?q = "Restr p (f ` Field r')"
1.1980 - have 1: "embed r' p f" using 0 unfolding embedS_def by force
1.1981 - hence 2: "f ` Field r' < {0..<(Suc n)}"
1.1982 - using WELL FIELD 0 by (auto simp add: embedS_iff)
1.1983 - have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
1.1984 - then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
1.1985 - unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
1.1986 - hence 4: "m \<le> n" using 2 by force
1.1987 - (* *)
1.1988 - have "bij_betw f (Field r') (f ` (Field r'))"
1.1989 - using 1 WELL embed_inj_on unfolding bij_betw_def by force
1.1990 - moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
1.1991 - ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
1.1992 - using bij_betw_same_card bij_betw_finite by metis
1.1993 - hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
1.1994 - hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
1.1995 - hence False using LESS not_ordLess_ordLeq by auto
1.1996 - }
1.1997 - thus ?thesis using WELL CARD by (fastforce simp: not_ordLess_iff_ordLeq)
1.1998 - qed
1.1999 - ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
1.2000 -qed
1.2001 -
1.2002 -
1.2003 -lemma card_of_cardSuc_finite:
1.2004 -"finite(Field(cardSuc |A| )) = finite A"
1.2005 -proof
1.2006 - assume *: "finite (Field (cardSuc |A| ))"
1.2007 - have 0: "|Field(cardSuc |A| )| =o cardSuc |A|"
1.2008 - using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
1.2009 - hence "|A| \<le>o |Field(cardSuc |A| )|"
1.2010 - using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric
1.2011 - ordLeq_ordIso_trans by blast
1.2012 - thus "finite A" using * card_of_ordLeq_finite by blast
1.2013 -next
1.2014 - assume "finite A"
1.2015 - then obtain n where "|A| =o natLeq_on n" using finite_iff_card_of_natLeq_on by blast
1.2016 - hence "cardSuc |A| =o cardSuc(natLeq_on n)"
1.2017 - using card_of_Card_order cardSuc_invar_ordIso natLeq_on_Card_order by blast
1.2018 - hence "cardSuc |A| =o natLeq_on(Suc n)"
1.2019 - using cardSuc_natLeq_on_Suc ordIso_transitive by blast
1.2020 - hence "cardSuc |A| =o |{0..<(Suc n)}|" using card_of_less ordIso_equivalence by blast
1.2021 - moreover have "|Field (cardSuc |A| ) | =o cardSuc |A|"
1.2022 - using card_of_Field_ordIso cardSuc_Card_order card_of_Card_order by blast
1.2023 - ultimately have "|Field (cardSuc |A| ) | =o |{0..<(Suc n)}|"
1.2024 - using ordIso_equivalence by blast
1.2025 - thus "finite (Field (cardSuc |A| ))"
1.2026 - using card_of_ordIso_finite finite_atLeastLessThan by blast
1.2027 -qed
1.2028 -
1.2029 -
1.2030 -lemma cardSuc_finite:
1.2031 -assumes "Card_order r"
1.2032 -shows "finite (Field (cardSuc r)) = finite (Field r)"
1.2033 -proof-
1.2034 - let ?A = "Field r"
1.2035 - have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso)
1.2036 - hence "cardSuc |?A| =o cardSuc r" using assms
1.2037 - by (simp add: card_of_Card_order cardSuc_invar_ordIso)
1.2038 - moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|"
1.2039 - by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order)
1.2040 - moreover
1.2041 - {have "|Field (cardSuc r) | =o cardSuc r"
1.2042 - using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order)
1.2043 - hence "cardSuc r =o |Field (cardSuc r) |"
1.2044 - using ordIso_symmetric by blast
1.2045 - }
1.2046 - ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |"
1.2047 - using ordIso_transitive by blast
1.2048 - hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))"
1.2049 - using card_of_ordIso_finite by blast
1.2050 - thus ?thesis by (simp only: card_of_cardSuc_finite)
1.2051 -qed
1.2052 -
1.2053 -
1.2054 -lemma card_of_Plus_ordLeq_infinite_Field:
1.2055 -assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1.2056 -and c: "Card_order r"
1.2057 -shows "|A <+> B| \<le>o r"
1.2058 -proof-
1.2059 - let ?r' = "cardSuc r"
1.2060 - have "Card_order ?r' \<and> infinite (Field ?r')" using assms
1.2061 - by (simp add: cardSuc_Card_order cardSuc_finite)
1.2062 - moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
1.2063 - by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1.2064 - ultimately have "|A <+> B| <o ?r'"
1.2065 - using card_of_Plus_ordLess_infinite_Field by blast
1.2066 - thus ?thesis using c r
1.2067 - by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
1.2068 -qed
1.2069 -
1.2070 -
1.2071 -lemma card_of_Un_ordLeq_infinite_Field:
1.2072 -assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
1.2073 -and "Card_order r"
1.2074 -shows "|A Un B| \<le>o r"
1.2075 -using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
1.2076 -ordLeq_transitive by blast
1.2077 -
1.2078 -
1.2079 -
1.2080 -subsection {* Regular cardinals *}
1.2081 -
1.2082 -
1.2083 -definition cofinal where
1.2084 -"cofinal A r \<equiv>
1.2085 - ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
1.2086 -
1.2087 -
1.2088 -definition regular where
1.2089 -"regular r \<equiv>
1.2090 - ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1.2091 -
1.2092 -
1.2093 -definition relChain where
1.2094 -"relChain r As \<equiv>
1.2095 - ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1.2096 -
1.2097 -lemma regular_UNION:
1.2098 -assumes r: "Card_order r" "regular r"
1.2099 -and As: "relChain r As"
1.2100 -and Bsub: "B \<le> (UN i : Field r. As i)"
1.2101 -and cardB: "|B| <o r"
1.2102 -shows "EX i : Field r. B \<le> As i"
1.2103 -proof-
1.2104 - let ?phi = "%b j. j : Field r \<and> b : As j"
1.2105 - have "ALL b : B. EX j. ?phi b j" using Bsub by blast
1.2106 - then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)"
1.2107 - using bchoice[of B ?phi] by blast
1.2108 - let ?K = "f ` B"
1.2109 - {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i"
1.2110 - have 2: "cofinal ?K r"
1.2111 - unfolding cofinal_def proof auto
1.2112 - fix i assume i: "i : Field r"
1.2113 - with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast
1.2114 - hence "i \<noteq> f b \<and> ~ (f b,i) : r"
1.2115 - using As f unfolding relChain_def by auto
1.2116 - hence "i \<noteq> f b \<and> (i, f b) : r" using r
1.2117 - unfolding card_order_on_def well_order_on_def linear_order_on_def
1.2118 - total_on_def using i f b by auto
1.2119 - with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
1.2120 - qed
1.2121 - moreover have "?K \<le> Field r" using f by blast
1.2122 - ultimately have "|?K| =o r" using 2 r unfolding regular_def by blast
1.2123 - moreover
1.2124 - {
1.2125 - have "|?K| <=o |B|" using card_of_image .
1.2126 - hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast
1.2127 - }
1.2128 - ultimately have False using not_ordLess_ordIso by blast
1.2129 - }
1.2130 - thus ?thesis by blast
1.2131 -qed
1.2132 -
1.2133 -
1.2134 -lemma infinite_cardSuc_regular:
1.2135 -assumes r_inf: "infinite (Field r)" and r_card: "Card_order r"
1.2136 -shows "regular (cardSuc r)"
1.2137 -proof-
1.2138 - let ?r' = "cardSuc r"
1.2139 - have r': "Card_order ?r'"
1.2140 - "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"
1.2141 - using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
1.2142 - show ?thesis
1.2143 - unfolding regular_def proof auto
1.2144 - fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
1.2145 - hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
1.2146 - also have 22: "|Field ?r'| =o ?r'"
1.2147 - using r' by (simp add: card_of_Field_ordIso[of ?r'])
1.2148 - finally have "|K| \<le>o ?r'" .
1.2149 - moreover
1.2150 - {let ?L = "UN j : K. rel.underS ?r' j"
1.2151 - let ?J = "Field r"
1.2152 - have rJ: "r =o |?J|"
1.2153 - using r_card card_of_Field_ordIso ordIso_symmetric by blast
1.2154 - assume "|K| <o ?r'"
1.2155 - hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
1.2156 - hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
1.2157 - moreover
1.2158 - {have "ALL j : K. |rel.underS ?r' j| <o ?r'"
1.2159 - using r' 1 by (auto simp: card_of_underS)
1.2160 - hence "ALL j : K. |rel.underS ?r' j| \<le>o r"
1.2161 - using r' card_of_Card_order by blast
1.2162 - hence "ALL j : K. |rel.underS ?r' j| \<le>o |?J|"
1.2163 - using rJ ordLeq_ordIso_trans by blast
1.2164 - }
1.2165 - ultimately have "|?L| \<le>o |?J|"
1.2166 - using r_inf card_of_UNION_ordLeq_infinite by blast
1.2167 - hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast
1.2168 - hence "|?L| <o ?r'" using r' card_of_Card_order by blast
1.2169 - moreover
1.2170 - {
1.2171 - have "Field ?r' \<le> ?L"
1.2172 - using 2 unfolding rel.underS_def cofinal_def by auto
1.2173 - hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
1.2174 - hence "?r' \<le>o |?L|"
1.2175 - using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
1.2176 - }
1.2177 - ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast
1.2178 - hence False using ordLess_irreflexive by blast
1.2179 - }
1.2180 - ultimately show "|K| =o ?r'"
1.2181 - unfolding ordLeq_iff_ordLess_or_ordIso by blast
1.2182 - qed
1.2183 -qed
1.2184 -
1.2185 -lemma cardSuc_UNION:
1.2186 -assumes r: "Card_order r" and "infinite (Field r)"
1.2187 -and As: "relChain (cardSuc r) As"
1.2188 -and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
1.2189 -and cardB: "|B| <=o r"
1.2190 -shows "EX i : Field (cardSuc r). B \<le> As i"
1.2191 -proof-
1.2192 - let ?r' = "cardSuc r"
1.2193 - have "Card_order ?r' \<and> |B| <o ?r'"
1.2194 - using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
1.2195 - card_of_Card_order by blast
1.2196 - moreover have "regular ?r'"
1.2197 - using assms by(simp add: infinite_cardSuc_regular)
1.2198 - ultimately show ?thesis
1.2199 - using As Bsub cardB regular_UNION by blast
1.2200 -qed
1.2201 -
1.2202 -
1.2203 -subsection {* Others *}
1.2204 -
1.2205 -lemma card_of_infinite_diff_finite:
1.2206 -assumes "infinite A" and "finite B"
1.2207 -shows "|A - B| =o |A|"
1.2208 -by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
1.2209 -
1.2210 -(* function space *)
1.2211 -definition Func where
1.2212 -"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
1.2213 -
1.2214 -lemma Func_empty:
1.2215 -"Func {} B = {\<lambda>x. undefined}"
1.2216 -unfolding Func_def by auto
1.2217 -
1.2218 -lemma Func_elim:
1.2219 -assumes "g \<in> Func A B" and "a \<in> A"
1.2220 -shows "\<exists> b. b \<in> B \<and> g a = b"
1.2221 -using assms unfolding Func_def by (cases "g a = undefined") auto
1.2222 -
1.2223 -definition curr where
1.2224 -"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
1.2225 -
1.2226 -lemma curr_in:
1.2227 -assumes f: "f \<in> Func (A <*> B) C"
1.2228 -shows "curr A f \<in> Func A (Func B C)"
1.2229 -using assms unfolding curr_def Func_def by auto
1.2230 -
1.2231 -lemma curr_inj:
1.2232 -assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
1.2233 -shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
1.2234 -proof safe
1.2235 - assume c: "curr A f1 = curr A f2"
1.2236 - show "f1 = f2"
1.2237 - proof (rule ext, clarify)
1.2238 - fix a b show "f1 (a, b) = f2 (a, b)"
1.2239 - proof (cases "(a,b) \<in> A <*> B")
1.2240 - case False
1.2241 - thus ?thesis using assms unfolding Func_def by auto
1.2242 - next
1.2243 - case True hence a: "a \<in> A" and b: "b \<in> B" by auto
1.2244 - thus ?thesis
1.2245 - using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
1.2246 - qed
1.2247 - qed
1.2248 -qed
1.2249 -
1.2250 -lemma curr_surj:
1.2251 -assumes "g \<in> Func A (Func B C)"
1.2252 -shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
1.2253 -proof
1.2254 - let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
1.2255 - show "curr A ?f = g"
1.2256 - proof (rule ext)
1.2257 - fix a show "curr A ?f a = g a"
1.2258 - proof (cases "a \<in> A")
1.2259 - case False
1.2260 - hence "g a = undefined" using assms unfolding Func_def by auto
1.2261 - thus ?thesis unfolding curr_def using False by simp
1.2262 - next
1.2263 - case True
1.2264 - obtain g1 where "g1 \<in> Func B C" and "g a = g1"
1.2265 - using assms using Func_elim[OF assms True] by blast
1.2266 - thus ?thesis using True unfolding Func_def curr_def by auto
1.2267 - qed
1.2268 - qed
1.2269 - show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
1.2270 -qed
1.2271 -
1.2272 -lemma bij_betw_curr:
1.2273 -"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
1.2274 -unfolding bij_betw_def inj_on_def image_def
1.2275 -using curr_in curr_inj curr_surj by blast
1.2276 -
1.2277 -lemma card_of_Func_Times:
1.2278 -"|Func (A <*> B) C| =o |Func A (Func B C)|"
1.2279 -unfolding card_of_ordIso[symmetric]
1.2280 -using bij_betw_curr by blast
1.2281 -
1.2282 -definition Func_map where
1.2283 -"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
1.2284 -
1.2285 -lemma Func_map:
1.2286 -assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
1.2287 -shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
1.2288 -using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
1.2289 -
1.2290 -lemma Func_non_emp:
1.2291 -assumes "B \<noteq> {}"
1.2292 -shows "Func A B \<noteq> {}"
1.2293 -proof-
1.2294 - obtain b where b: "b \<in> B" using assms by auto
1.2295 - hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
1.2296 - thus ?thesis by blast
1.2297 -qed
1.2298 -
1.2299 -lemma Func_is_emp:
1.2300 -"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
1.2301 -proof
1.2302 - assume L: ?L
1.2303 - moreover {assume "A = {}" hence False using L Func_empty by auto}
1.2304 - moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
1.2305 - ultimately show ?R by blast
1.2306 -next
1.2307 - assume R: ?R
1.2308 - moreover
1.2309 - {fix f assume "f \<in> Func A B"
1.2310 - moreover obtain a where "a \<in> A" using R by blast
1.2311 - ultimately obtain b where "b \<in> B" unfolding Func_def by(cases "f a = undefined", force+)
1.2312 - with R have False by auto
1.2313 - }
1.2314 - thus ?L by blast
1.2315 -qed
1.2316 -
1.2317 -lemma Func_map_surj:
1.2318 -assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
1.2319 -and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
1.2320 -shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
1.2321 -proof(cases "B2 = {}")
1.2322 - case True
1.2323 - thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
1.2324 -next
1.2325 - case False note B2 = False
1.2326 - show ?thesis
1.2327 - proof safe
1.2328 - fix h assume h: "h \<in> Func B2 B1"
1.2329 - def j1 \<equiv> "inv_into A1 f1"
1.2330 - have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
1.2331 - then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
1.2332 - {fix b2 assume b2: "b2 \<in> B2"
1.2333 - hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
1.2334 - moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
1.2335 - ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
1.2336 - } note kk = this
1.2337 - obtain b22 where b22: "b22 \<in> B2" using B2 by auto
1.2338 - def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
1.2339 - have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
1.2340 - have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
1.2341 - using kk unfolding j2_def by auto
1.2342 - def g \<equiv> "Func_map A2 j1 j2 h"
1.2343 - have "Func_map B2 f1 f2 g = h"
1.2344 - proof (rule ext)
1.2345 - fix b2 show "Func_map B2 f1 f2 g b2 = h b2"
1.2346 - proof(cases "b2 \<in> B2")
1.2347 - case True
1.2348 - show ?thesis
1.2349 - proof (cases "h b2 = undefined")
1.2350 - case True
1.2351 - hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto
1.2352 - show ?thesis using A2 f_inv_into_f[OF b1]
1.2353 - unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto
1.2354 - qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
1.2355 - auto intro: f_inv_into_f)
1.2356 - qed(insert h, unfold Func_def Func_map_def, auto)
1.2357 - qed
1.2358 - moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
1.2359 - using inv_into_into j2A2 B1 A2 inv_into_into
1.2360 - unfolding j1_def image_def by fast+
1.2361 - ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
1.2362 - unfolding Func_map_def[abs_def] unfolding image_def by auto
1.2363 - qed(insert B1 Func_map[OF _ _ A2(2)], auto)
1.2364 -qed
1.2365 -
1.2366 -lemma card_of_Pow_Func:
1.2367 -"|Pow A| =o |Func A (UNIV::bool set)|"
1.2368 -proof-
1.2369 - def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False)
1.2370 - else undefined"
1.2371 - have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
1.2372 - unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
1.2373 - fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
1.2374 - thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)
1.2375 - next
1.2376 - show "F ` Pow A = Func A UNIV"
1.2377 - proof safe
1.2378 - fix f assume f: "f \<in> Func A (UNIV::bool set)"
1.2379 - show "f \<in> F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
1.2380 - let ?A1 = "{a \<in> A. f a = True}"
1.2381 - show "f = F ?A1" unfolding F_def apply(rule ext)
1.2382 - using f unfolding Func_def mem_Collect_eq by auto
1.2383 - qed auto
1.2384 - qed(unfold Func_def mem_Collect_eq F_def, auto)
1.2385 - qed
1.2386 - thus ?thesis unfolding card_of_ordIso[symmetric] by blast
1.2387 -qed
1.2388 -
1.2389 -lemma card_of_Func_mono:
1.2390 -fixes A1 A2 :: "'a set" and B :: "'b set"
1.2391 -assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}"
1.2392 -shows "|Func A1 B| \<le>o |Func A2 B|"
1.2393 -proof-
1.2394 - obtain bb where bb: "bb \<in> B" using B by auto
1.2395 - def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b) a. if a \<in> A2 then (if a \<in> A1 then f1 a else bb)
1.2396 - else undefined"
1.2397 - show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI)
1.2398 - show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe
1.2399 - fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g"
1.2400 - show "f = g"
1.2401 - proof(rule ext)
1.2402 - fix a show "f a = g a"
1.2403 - proof(cases "a \<in> A1")
1.2404 - case True
1.2405 - thus ?thesis using eq A12 unfolding F_def fun_eq_iff
1.2406 - by (elim allE[of _ a]) auto
1.2407 - qed(insert f g, unfold Func_def, fastforce)
1.2408 - qed
1.2409 - qed
1.2410 - qed(insert bb, unfold Func_def F_def, force)
1.2411 -qed
1.2412 -
1.2413 -lemma ordLeq_Func:
1.2414 -assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
1.2415 -shows "|A| \<le>o |Func A B|"
1.2416 -unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
1.2417 - let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined"
1.2418 - show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto
1.2419 - show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto
1.2420 -qed
1.2421 -
1.2422 -lemma infinite_Func:
1.2423 -assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
1.2424 -shows "infinite (Func A B)"
1.2425 -using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
1.2426 -
1.2427 -lemma card_of_Func_UNIV:
1.2428 -"|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|"
1.2429 -apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
1.2430 - let ?F = "\<lambda> f (a::'a). ((f a)::'b)"
1.2431 - show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"
1.2432 - unfolding bij_betw_def inj_on_def proof safe
1.2433 - fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
1.2434 - hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
1.2435 - then obtain f where f: "\<forall> a. h a = f a" by metis
1.2436 - hence "range f \<subseteq> B" using h unfolding Func_def by auto
1.2437 - thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
1.2438 - qed(unfold Func_def fun_eq_iff, auto)
1.2439 -qed
1.2440 -
1.2441 -end