|
1 (* Title: HOL/Cardinals/Cardinal_Order_Relation_LFP.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Cardinal-order relations (LFP). |
|
6 *) |
|
7 |
|
8 header {* Cardinal-Order Relations (LFP) *} |
|
9 |
|
10 theory Cardinal_Order_Relation_LFP |
|
11 imports Constructions_on_Wellorders_LFP |
|
12 begin |
|
13 |
|
14 |
|
15 text{* In this section, we define cardinal-order relations to be minim well-orders |
|
16 on their field. Then we define the cardinal of a set to be {\em some} cardinal-order |
|
17 relation on that set, which will be unique up to order isomorphism. Then we study |
|
18 the connection between cardinals and: |
|
19 \begin{itemize} |
|
20 \item standard set-theoretic constructions: products, |
|
21 sums, unions, lists, powersets, set-of finite sets operator; |
|
22 \item finiteness and infiniteness (in particular, with the numeric cardinal operator |
|
23 for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}). |
|
24 \end{itemize} |
|
25 % |
|
26 On the way, we define the canonical $\omega$ cardinal and finite cardinals. We also |
|
27 define (again, up to order isomorphism) the successor of a cardinal, and show that |
|
28 any cardinal admits a successor. |
|
29 |
|
30 Main results of this section are the existence of cardinal relations and the |
|
31 facts that, in the presence of infiniteness, |
|
32 most of the standard set-theoretic constructions (except for the powerset) |
|
33 {\em do not increase cardinality}. In particular, e.g., the set of words/lists over |
|
34 any infinite set has the same cardinality (hence, is in bijection) with that set. |
|
35 *} |
|
36 |
|
37 |
|
38 subsection {* Cardinal orders *} |
|
39 |
|
40 |
|
41 text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the |
|
42 order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the |
|
43 strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *} |
|
44 |
|
45 definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
|
46 where |
|
47 "card_order_on A r \<equiv> well_order_on A r \<and> (\<forall>r'. well_order_on A r' \<longrightarrow> r \<le>o r')" |
|
48 |
|
49 |
|
50 abbreviation "Card_order r \<equiv> card_order_on (Field r) r" |
|
51 abbreviation "card_order r \<equiv> card_order_on UNIV r" |
|
52 |
|
53 |
|
54 lemma card_order_on_well_order_on: |
|
55 assumes "card_order_on A r" |
|
56 shows "well_order_on A r" |
|
57 using assms unfolding card_order_on_def by simp |
|
58 |
|
59 |
|
60 lemma card_order_on_Card_order: |
|
61 "card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r" |
|
62 unfolding card_order_on_def using rel.well_order_on_Field by blast |
|
63 |
|
64 |
|
65 text{* The existence of a cardinal relation on any given set (which will mean |
|
66 that any set has a cardinal) follows from two facts: |
|
67 \begin{itemize} |
|
68 \item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}), |
|
69 which states that on any given set there exists a well-order; |
|
70 \item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal |
|
71 such well-order, i.e., a cardinal order. |
|
72 \end{itemize} |
|
73 *} |
|
74 |
|
75 |
|
76 theorem card_order_on: "\<exists>r. card_order_on A r" |
|
77 proof- |
|
78 obtain R where R_def: "R = {r. well_order_on A r}" by blast |
|
79 have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)" |
|
80 using well_order_on[of A] R_def rel.well_order_on_Well_order by blast |
|
81 hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'" |
|
82 using exists_minim_Well_order[of R] by auto |
|
83 thus ?thesis using R_def unfolding card_order_on_def by auto |
|
84 qed |
|
85 |
|
86 |
|
87 lemma card_order_on_ordIso: |
|
88 assumes CO: "card_order_on A r" and CO': "card_order_on A r'" |
|
89 shows "r =o r'" |
|
90 using assms unfolding card_order_on_def |
|
91 using ordIso_iff_ordLeq by blast |
|
92 |
|
93 |
|
94 lemma Card_order_ordIso: |
|
95 assumes CO: "Card_order r" and ISO: "r' =o r" |
|
96 shows "Card_order r'" |
|
97 using ISO unfolding ordIso_def |
|
98 proof(unfold card_order_on_def, auto) |
|
99 fix p' assume "well_order_on (Field r') p'" |
|
100 hence 0: "Well_order p' \<and> Field p' = Field r'" |
|
101 using rel.well_order_on_Well_order by blast |
|
102 obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'" |
|
103 using ISO unfolding ordIso_def by auto |
|
104 hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r" |
|
105 by (auto simp add: iso_iff embed_inj_on) |
|
106 let ?p = "dir_image p' f" |
|
107 have 4: "p' =o ?p \<and> Well_order ?p" |
|
108 using 0 2 3 by (auto simp add: dir_image_ordIso Well_order_dir_image) |
|
109 moreover have "Field ?p = Field r" |
|
110 using 0 3 by (auto simp add: dir_image_Field2 order_on_defs) |
|
111 ultimately have "well_order_on (Field r) ?p" by auto |
|
112 hence "r \<le>o ?p" using CO unfolding card_order_on_def by auto |
|
113 thus "r' \<le>o p'" |
|
114 using ISO 4 ordLeq_ordIso_trans ordIso_ordLeq_trans ordIso_symmetric by blast |
|
115 qed |
|
116 |
|
117 |
|
118 lemma Card_order_ordIso2: |
|
119 assumes CO: "Card_order r" and ISO: "r =o r'" |
|
120 shows "Card_order r'" |
|
121 using assms Card_order_ordIso ordIso_symmetric by blast |
|
122 |
|
123 |
|
124 subsection {* Cardinal of a set *} |
|
125 |
|
126 |
|
127 text{* We define the cardinal of set to be {\em some} cardinal order on that set. |
|
128 We shall prove that this notion is unique up to order isomorphism, meaning |
|
129 that order isomorphism shall be the true identity of cardinals. *} |
|
130 |
|
131 |
|
132 definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" ) |
|
133 where "card_of A = (SOME r. card_order_on A r)" |
|
134 |
|
135 |
|
136 lemma card_of_card_order_on: "card_order_on A |A|" |
|
137 unfolding card_of_def by (auto simp add: card_order_on someI_ex) |
|
138 |
|
139 |
|
140 lemma card_of_well_order_on: "well_order_on A |A|" |
|
141 using card_of_card_order_on card_order_on_def by blast |
|
142 |
|
143 |
|
144 lemma Field_card_of: "Field |A| = A" |
|
145 using card_of_card_order_on[of A] unfolding card_order_on_def |
|
146 using rel.well_order_on_Field by blast |
|
147 |
|
148 |
|
149 lemma card_of_Card_order: "Card_order |A|" |
|
150 by (simp only: card_of_card_order_on Field_card_of) |
|
151 |
|
152 |
|
153 corollary ordIso_card_of_imp_Card_order: |
|
154 "r =o |A| \<Longrightarrow> Card_order r" |
|
155 using card_of_Card_order Card_order_ordIso by blast |
|
156 |
|
157 |
|
158 lemma card_of_Well_order: "Well_order |A|" |
|
159 using card_of_Card_order unfolding card_order_on_def by auto |
|
160 |
|
161 |
|
162 lemma card_of_refl: "|A| =o |A|" |
|
163 using card_of_Well_order ordIso_reflexive by blast |
|
164 |
|
165 |
|
166 lemma card_of_least: "well_order_on A r \<Longrightarrow> |A| \<le>o r" |
|
167 using card_of_card_order_on unfolding card_order_on_def by blast |
|
168 |
|
169 |
|
170 lemma card_of_ordIso: |
|
171 "(\<exists>f. bij_betw f A B) = ( |A| =o |B| )" |
|
172 proof(auto) |
|
173 fix f assume *: "bij_betw f A B" |
|
174 then obtain r where "well_order_on B r \<and> |A| =o r" |
|
175 using Well_order_iso_copy card_of_well_order_on by blast |
|
176 hence "|B| \<le>o |A|" using card_of_least |
|
177 ordLeq_ordIso_trans ordIso_symmetric by blast |
|
178 moreover |
|
179 {let ?g = "inv_into A f" |
|
180 have "bij_betw ?g B A" using * bij_betw_inv_into by blast |
|
181 then obtain r where "well_order_on A r \<and> |B| =o r" |
|
182 using Well_order_iso_copy card_of_well_order_on by blast |
|
183 hence "|A| \<le>o |B|" using card_of_least |
|
184 ordLeq_ordIso_trans ordIso_symmetric by blast |
|
185 } |
|
186 ultimately show "|A| =o |B|" using ordIso_iff_ordLeq by blast |
|
187 next |
|
188 assume "|A| =o |B|" |
|
189 then obtain f where "iso ( |A| ) ( |B| ) f" |
|
190 unfolding ordIso_def by auto |
|
191 hence "bij_betw f A B" unfolding iso_def Field_card_of by simp |
|
192 thus "\<exists>f. bij_betw f A B" by auto |
|
193 qed |
|
194 |
|
195 |
|
196 lemma card_of_ordLeq: |
|
197 "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = ( |A| \<le>o |B| )" |
|
198 proof(auto) |
|
199 fix f assume *: "inj_on f A" and **: "f ` A \<le> B" |
|
200 {assume "|B| <o |A|" |
|
201 hence "|B| \<le>o |A|" using ordLeq_iff_ordLess_or_ordIso by blast |
|
202 then obtain g where "embed ( |B| ) ( |A| ) g" |
|
203 unfolding ordLeq_def by auto |
|
204 hence 1: "inj_on g B \<and> g ` B \<le> A" using embed_inj_on[of "|B|" "|A|" "g"] |
|
205 card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"] |
|
206 embed_Field[of "|B|" "|A|" g] by auto |
|
207 obtain h where "bij_betw h A B" |
|
208 using * ** 1 Cantor_Bernstein[of f] by fastforce |
|
209 hence "|A| =o |B|" using card_of_ordIso by blast |
|
210 hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto |
|
211 } |
|
212 thus "|A| \<le>o |B|" using ordLess_or_ordLeq[of "|B|" "|A|"] |
|
213 by (auto simp: card_of_Well_order) |
|
214 next |
|
215 assume *: "|A| \<le>o |B|" |
|
216 obtain f where "embed ( |A| ) ( |B| ) f" |
|
217 using * unfolding ordLeq_def by auto |
|
218 hence "inj_on f A \<and> f ` A \<le> B" using embed_inj_on[of "|A|" "|B|" f] |
|
219 card_of_Well_order[of "A"] Field_card_of[of "A"] Field_card_of[of "B"] |
|
220 embed_Field[of "|A|" "|B|" f] by auto |
|
221 thus "\<exists>f. inj_on f A \<and> f ` A \<le> B" by auto |
|
222 qed |
|
223 |
|
224 |
|
225 lemma card_of_ordLeq2: |
|
226 "A \<noteq> {} \<Longrightarrow> (\<exists>g. g ` B = A) = ( |A| \<le>o |B| )" |
|
227 using card_of_ordLeq[of A B] inj_on_iff_surj[of A B] by auto |
|
228 |
|
229 |
|
230 lemma card_of_ordLess: |
|
231 "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = ( |B| <o |A| )" |
|
232 proof- |
|
233 have "(\<not>(\<exists>f. inj_on f A \<and> f ` A \<le> B)) = (\<not> |A| \<le>o |B| )" |
|
234 using card_of_ordLeq by blast |
|
235 also have "\<dots> = ( |B| <o |A| )" |
|
236 using card_of_Well_order[of A] card_of_Well_order[of B] |
|
237 not_ordLeq_iff_ordLess by blast |
|
238 finally show ?thesis . |
|
239 qed |
|
240 |
|
241 |
|
242 lemma card_of_ordLess2: |
|
243 "B \<noteq> {} \<Longrightarrow> (\<not>(\<exists>f. f ` A = B)) = ( |A| <o |B| )" |
|
244 using card_of_ordLess[of B A] inj_on_iff_surj[of B A] by auto |
|
245 |
|
246 |
|
247 lemma card_of_ordIsoI: |
|
248 assumes "bij_betw f A B" |
|
249 shows "|A| =o |B|" |
|
250 using assms unfolding card_of_ordIso[symmetric] by auto |
|
251 |
|
252 |
|
253 lemma card_of_ordLeqI: |
|
254 assumes "inj_on f A" and "\<And> a. a \<in> A \<Longrightarrow> f a \<in> B" |
|
255 shows "|A| \<le>o |B|" |
|
256 using assms unfolding card_of_ordLeq[symmetric] by auto |
|
257 |
|
258 |
|
259 lemma card_of_unique: |
|
260 "card_order_on A r \<Longrightarrow> r =o |A|" |
|
261 by (simp only: card_order_on_ordIso card_of_card_order_on) |
|
262 |
|
263 |
|
264 lemma card_of_mono1: |
|
265 "A \<le> B \<Longrightarrow> |A| \<le>o |B|" |
|
266 using inj_on_id[of A] card_of_ordLeq[of A B] by fastforce |
|
267 |
|
268 |
|
269 lemma card_of_mono2: |
|
270 assumes "r \<le>o r'" |
|
271 shows "|Field r| \<le>o |Field r'|" |
|
272 proof- |
|
273 obtain f where |
|
274 1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f" |
|
275 using assms unfolding ordLeq_def |
|
276 by (auto simp add: rel.well_order_on_Well_order) |
|
277 hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'" |
|
278 by (auto simp add: embed_inj_on embed_Field) |
|
279 thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast |
|
280 qed |
|
281 |
|
282 |
|
283 lemma card_of_cong: "r =o r' \<Longrightarrow> |Field r| =o |Field r'|" |
|
284 by (simp add: ordIso_iff_ordLeq card_of_mono2) |
|
285 |
|
286 |
|
287 lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r" |
|
288 using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast |
|
289 |
|
290 |
|
291 lemma card_of_Field_ordIso: |
|
292 assumes "Card_order r" |
|
293 shows "|Field r| =o r" |
|
294 proof- |
|
295 have "card_order_on (Field r) r" |
|
296 using assms card_order_on_Card_order by blast |
|
297 moreover have "card_order_on (Field r) |Field r|" |
|
298 using card_of_card_order_on by blast |
|
299 ultimately show ?thesis using card_order_on_ordIso by blast |
|
300 qed |
|
301 |
|
302 |
|
303 lemma Card_order_iff_ordIso_card_of: |
|
304 "Card_order r = (r =o |Field r| )" |
|
305 using ordIso_card_of_imp_Card_order card_of_Field_ordIso ordIso_symmetric by blast |
|
306 |
|
307 |
|
308 lemma Card_order_iff_ordLeq_card_of: |
|
309 "Card_order r = (r \<le>o |Field r| )" |
|
310 proof- |
|
311 have "Card_order r = (r =o |Field r| )" |
|
312 unfolding Card_order_iff_ordIso_card_of by simp |
|
313 also have "... = (r \<le>o |Field r| \<and> |Field r| \<le>o r)" |
|
314 unfolding ordIso_iff_ordLeq by simp |
|
315 also have "... = (r \<le>o |Field r| )" |
|
316 using card_of_Field_ordLess |
|
317 by (auto simp: card_of_Field_ordLess ordLeq_Well_order_simp) |
|
318 finally show ?thesis . |
|
319 qed |
|
320 |
|
321 |
|
322 lemma Card_order_iff_Restr_underS: |
|
323 assumes "Well_order r" |
|
324 shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )" |
|
325 using assms unfolding Card_order_iff_ordLeq_card_of |
|
326 using ordLeq_iff_ordLess_Restr card_of_Well_order by blast |
|
327 |
|
328 |
|
329 lemma card_of_underS: |
|
330 assumes r: "Card_order r" and a: "a : Field r" |
|
331 shows "|rel.underS r a| <o r" |
|
332 proof- |
|
333 let ?A = "rel.underS r a" let ?r' = "Restr r ?A" |
|
334 have 1: "Well_order r" |
|
335 using r unfolding card_order_on_def by simp |
|
336 have "Well_order ?r'" using 1 Well_order_Restr by auto |
|
337 moreover have "card_order_on (Field ?r') |Field ?r'|" |
|
338 using card_of_card_order_on . |
|
339 ultimately have "|Field ?r'| \<le>o ?r'" |
|
340 unfolding card_order_on_def by simp |
|
341 moreover have "Field ?r' = ?A" |
|
342 using 1 wo_rel.underS_ofilter Field_Restr_ofilter |
|
343 unfolding wo_rel_def by fastforce |
|
344 ultimately have "|?A| \<le>o ?r'" by simp |
|
345 also have "?r' <o |Field r|" |
|
346 using 1 a r Card_order_iff_Restr_underS by blast |
|
347 also have "|Field r| =o r" |
|
348 using r ordIso_symmetric unfolding Card_order_iff_ordIso_card_of by auto |
|
349 finally show ?thesis . |
|
350 qed |
|
351 |
|
352 |
|
353 lemma ordLess_Field: |
|
354 assumes "r <o r'" |
|
355 shows "|Field r| <o r'" |
|
356 proof- |
|
357 have "well_order_on (Field r) r" using assms unfolding ordLess_def |
|
358 by (auto simp add: rel.well_order_on_Well_order) |
|
359 hence "|Field r| \<le>o r" using card_of_least by blast |
|
360 thus ?thesis using assms ordLeq_ordLess_trans by blast |
|
361 qed |
|
362 |
|
363 |
|
364 lemma internalize_card_of_ordLeq: |
|
365 "( |A| \<le>o r) = (\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r)" |
|
366 proof |
|
367 assume "|A| \<le>o r" |
|
368 then obtain p where 1: "Field p \<le> Field r \<and> |A| =o p \<and> p \<le>o r" |
|
369 using internalize_ordLeq[of "|A|" r] by blast |
|
370 hence "Card_order p" using card_of_Card_order Card_order_ordIso2 by blast |
|
371 hence "|Field p| =o p" using card_of_Field_ordIso by blast |
|
372 hence "|A| =o |Field p| \<and> |Field p| \<le>o r" |
|
373 using 1 ordIso_equivalence ordIso_ordLeq_trans by blast |
|
374 thus "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" using 1 by blast |
|
375 next |
|
376 assume "\<exists>B \<le> Field r. |A| =o |B| \<and> |B| \<le>o r" |
|
377 thus "|A| \<le>o r" using ordIso_ordLeq_trans by blast |
|
378 qed |
|
379 |
|
380 |
|
381 lemma internalize_card_of_ordLeq2: |
|
382 "( |A| \<le>o |C| ) = (\<exists>B \<le> C. |A| =o |B| \<and> |B| \<le>o |C| )" |
|
383 using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto |
|
384 |
|
385 |
|
386 |
|
387 subsection {* Cardinals versus set operations on arbitrary sets *} |
|
388 |
|
389 |
|
390 text{* Here we embark in a long journey of simple results showing |
|
391 that the standard set-theoretic operations are well-behaved w.r.t. the notion of |
|
392 cardinal -- essentially, this means that they preserve the ``cardinal identity" |
|
393 @{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}. |
|
394 *} |
|
395 |
|
396 |
|
397 lemma card_of_empty: "|{}| \<le>o |A|" |
|
398 using card_of_ordLeq inj_on_id by blast |
|
399 |
|
400 |
|
401 lemma card_of_empty1: |
|
402 assumes "Well_order r \<or> Card_order r" |
|
403 shows "|{}| \<le>o r" |
|
404 proof- |
|
405 have "Well_order r" using assms unfolding card_order_on_def by auto |
|
406 hence "|Field r| <=o r" |
|
407 using assms card_of_Field_ordLess by blast |
|
408 moreover have "|{}| \<le>o |Field r|" by (simp add: card_of_empty) |
|
409 ultimately show ?thesis using ordLeq_transitive by blast |
|
410 qed |
|
411 |
|
412 |
|
413 corollary Card_order_empty: |
|
414 "Card_order r \<Longrightarrow> |{}| \<le>o r" by (simp add: card_of_empty1) |
|
415 |
|
416 |
|
417 lemma card_of_empty2: |
|
418 assumes LEQ: "|A| =o |{}|" |
|
419 shows "A = {}" |
|
420 using assms card_of_ordIso[of A] bij_betw_empty2 by blast |
|
421 |
|
422 |
|
423 lemma card_of_empty3: |
|
424 assumes LEQ: "|A| \<le>o |{}|" |
|
425 shows "A = {}" |
|
426 using assms |
|
427 by (simp add: ordIso_iff_ordLeq card_of_empty1 card_of_empty2 |
|
428 ordLeq_Well_order_simp) |
|
429 |
|
430 |
|
431 lemma card_of_empty_ordIso: |
|
432 "|{}::'a set| =o |{}::'b set|" |
|
433 using card_of_ordIso unfolding bij_betw_def inj_on_def by blast |
|
434 |
|
435 |
|
436 lemma card_of_image: |
|
437 "|f ` A| <=o |A|" |
|
438 proof(cases "A = {}", simp add: card_of_empty) |
|
439 assume "A ~= {}" |
|
440 hence "f ` A ~= {}" by auto |
|
441 thus "|f ` A| \<le>o |A|" |
|
442 using card_of_ordLeq2[of "f ` A" A] by auto |
|
443 qed |
|
444 |
|
445 |
|
446 lemma surj_imp_ordLeq: |
|
447 assumes "B <= f ` A" |
|
448 shows "|B| <=o |A|" |
|
449 proof- |
|
450 have "|B| <=o |f ` A|" using assms card_of_mono1 by auto |
|
451 thus ?thesis using card_of_image ordLeq_transitive by blast |
|
452 qed |
|
453 |
|
454 |
|
455 lemma card_of_ordLeqI2: |
|
456 assumes "B \<subseteq> f ` A" |
|
457 shows "|B| \<le>o |A|" |
|
458 using assms by (metis surj_imp_ordLeq) |
|
459 |
|
460 |
|
461 lemma card_of_singl_ordLeq: |
|
462 assumes "A \<noteq> {}" |
|
463 shows "|{b}| \<le>o |A|" |
|
464 proof- |
|
465 obtain a where *: "a \<in> A" using assms by auto |
|
466 let ?h = "\<lambda> b'::'b. if b' = b then a else undefined" |
|
467 have "inj_on ?h {b} \<and> ?h ` {b} \<le> A" |
|
468 using * unfolding inj_on_def by auto |
|
469 thus ?thesis using card_of_ordLeq by blast |
|
470 qed |
|
471 |
|
472 |
|
473 corollary Card_order_singl_ordLeq: |
|
474 "\<lbrakk>Card_order r; Field r \<noteq> {}\<rbrakk> \<Longrightarrow> |{b}| \<le>o r" |
|
475 using card_of_singl_ordLeq[of "Field r" b] |
|
476 card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast |
|
477 |
|
478 |
|
479 lemma card_of_Pow: "|A| <o |Pow A|" |
|
480 using card_of_ordLess2[of "Pow A" A] Cantors_paradox[of A] |
|
481 Pow_not_empty[of A] by auto |
|
482 |
|
483 |
|
484 lemma infinite_Pow: |
|
485 assumes "infinite A" |
|
486 shows "infinite (Pow A)" |
|
487 proof- |
|
488 have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq) |
|
489 thus ?thesis by (metis assms finite_Pow_iff) |
|
490 qed |
|
491 |
|
492 |
|
493 corollary Card_order_Pow: |
|
494 "Card_order r \<Longrightarrow> r <o |Pow(Field r)|" |
|
495 using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast |
|
496 |
|
497 |
|
498 corollary card_of_set_type: "|UNIV::'a set| <o |UNIV::'a set set|" |
|
499 using card_of_Pow[of "UNIV::'a set"] by simp |
|
500 |
|
501 |
|
502 lemma card_of_Plus1: "|A| \<le>o |A <+> B|" |
|
503 proof- |
|
504 have "Inl ` A \<le> A <+> B" by auto |
|
505 thus ?thesis using inj_Inl[of A] card_of_ordLeq by blast |
|
506 qed |
|
507 |
|
508 |
|
509 corollary Card_order_Plus1: |
|
510 "Card_order r \<Longrightarrow> r \<le>o |(Field r) <+> B|" |
|
511 using card_of_Plus1 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast |
|
512 |
|
513 |
|
514 lemma card_of_Plus2: "|B| \<le>o |A <+> B|" |
|
515 proof- |
|
516 have "Inr ` B \<le> A <+> B" by auto |
|
517 thus ?thesis using inj_Inr[of B] card_of_ordLeq by blast |
|
518 qed |
|
519 |
|
520 |
|
521 corollary Card_order_Plus2: |
|
522 "Card_order r \<Longrightarrow> r \<le>o |A <+> (Field r)|" |
|
523 using card_of_Plus2 card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast |
|
524 |
|
525 |
|
526 lemma card_of_Plus_empty1: "|A| =o |A <+> {}|" |
|
527 proof- |
|
528 have "bij_betw Inl A (A <+> {})" unfolding bij_betw_def inj_on_def by auto |
|
529 thus ?thesis using card_of_ordIso by auto |
|
530 qed |
|
531 |
|
532 |
|
533 lemma card_of_Plus_empty2: "|A| =o |{} <+> A|" |
|
534 proof- |
|
535 have "bij_betw Inr A ({} <+> A)" unfolding bij_betw_def inj_on_def by auto |
|
536 thus ?thesis using card_of_ordIso by auto |
|
537 qed |
|
538 |
|
539 |
|
540 lemma card_of_Plus_commute: "|A <+> B| =o |B <+> A|" |
|
541 proof- |
|
542 let ?f = "\<lambda>(c::'a + 'b). case c of Inl a \<Rightarrow> Inr a |
|
543 | Inr b \<Rightarrow> Inl b" |
|
544 have "bij_betw ?f (A <+> B) (B <+> A)" |
|
545 unfolding bij_betw_def inj_on_def by force |
|
546 thus ?thesis using card_of_ordIso by blast |
|
547 qed |
|
548 |
|
549 |
|
550 lemma card_of_Plus_assoc: |
|
551 fixes A :: "'a set" and B :: "'b set" and C :: "'c set" |
|
552 shows "|(A <+> B) <+> C| =o |A <+> B <+> C|" |
|
553 proof - |
|
554 def f \<equiv> "\<lambda>(k::('a + 'b) + 'c). |
|
555 case k of Inl ab \<Rightarrow> (case ab of Inl a \<Rightarrow> Inl a |
|
556 |Inr b \<Rightarrow> Inr (Inl b)) |
|
557 |Inr c \<Rightarrow> Inr (Inr c)" |
|
558 have "A <+> B <+> C \<subseteq> f ` ((A <+> B) <+> C)" |
|
559 proof |
|
560 fix x assume x: "x \<in> A <+> B <+> C" |
|
561 show "x \<in> f ` ((A <+> B) <+> C)" |
|
562 proof(cases x) |
|
563 case (Inl a) |
|
564 hence "a \<in> A" "x = f (Inl (Inl a))" |
|
565 using x unfolding f_def by auto |
|
566 thus ?thesis by auto |
|
567 next |
|
568 case (Inr bc) note 1 = Inr show ?thesis |
|
569 proof(cases bc) |
|
570 case (Inl b) |
|
571 hence "b \<in> B" "x = f (Inl (Inr b))" |
|
572 using x 1 unfolding f_def by auto |
|
573 thus ?thesis by auto |
|
574 next |
|
575 case (Inr c) |
|
576 hence "c \<in> C" "x = f (Inr c)" |
|
577 using x 1 unfolding f_def by auto |
|
578 thus ?thesis by auto |
|
579 qed |
|
580 qed |
|
581 qed |
|
582 hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)" |
|
583 unfolding bij_betw_def inj_on_def f_def by force |
|
584 thus ?thesis using card_of_ordIso by blast |
|
585 qed |
|
586 |
|
587 |
|
588 lemma card_of_Plus_mono1: |
|
589 assumes "|A| \<le>o |B|" |
|
590 shows "|A <+> C| \<le>o |B <+> C|" |
|
591 proof- |
|
592 obtain f where 1: "inj_on f A \<and> f ` A \<le> B" |
|
593 using assms card_of_ordLeq[of A] by fastforce |
|
594 obtain g where g_def: |
|
595 "g = (\<lambda>d. case d of Inl a \<Rightarrow> Inl(f a) | Inr (c::'c) \<Rightarrow> Inr c)" by blast |
|
596 have "inj_on g (A <+> C) \<and> g ` (A <+> C) \<le> (B <+> C)" |
|
597 proof- |
|
598 {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and |
|
599 "g d1 = g d2" |
|
600 hence "d1 = d2" using 1 unfolding inj_on_def |
|
601 by(case_tac d1, case_tac d2, auto simp add: g_def) |
|
602 } |
|
603 moreover |
|
604 {fix d assume "d \<in> A <+> C" |
|
605 hence "g d \<in> B <+> C" using 1 |
|
606 by(case_tac d, auto simp add: g_def) |
|
607 } |
|
608 ultimately show ?thesis unfolding inj_on_def by auto |
|
609 qed |
|
610 thus ?thesis using card_of_ordLeq by metis |
|
611 qed |
|
612 |
|
613 |
|
614 corollary ordLeq_Plus_mono1: |
|
615 assumes "r \<le>o r'" |
|
616 shows "|(Field r) <+> C| \<le>o |(Field r') <+> C|" |
|
617 using assms card_of_mono2 card_of_Plus_mono1 by blast |
|
618 |
|
619 |
|
620 lemma card_of_Plus_mono2: |
|
621 assumes "|A| \<le>o |B|" |
|
622 shows "|C <+> A| \<le>o |C <+> B|" |
|
623 using assms card_of_Plus_mono1[of A B C] |
|
624 card_of_Plus_commute[of C A] card_of_Plus_commute[of B C] |
|
625 ordIso_ordLeq_trans[of "|C <+> A|"] ordLeq_ordIso_trans[of "|C <+> A|"] |
|
626 by blast |
|
627 |
|
628 |
|
629 corollary ordLeq_Plus_mono2: |
|
630 assumes "r \<le>o r'" |
|
631 shows "|A <+> (Field r)| \<le>o |A <+> (Field r')|" |
|
632 using assms card_of_mono2 card_of_Plus_mono2 by blast |
|
633 |
|
634 |
|
635 lemma card_of_Plus_mono: |
|
636 assumes "|A| \<le>o |B|" and "|C| \<le>o |D|" |
|
637 shows "|A <+> C| \<le>o |B <+> D|" |
|
638 using assms card_of_Plus_mono1[of A B C] card_of_Plus_mono2[of C D B] |
|
639 ordLeq_transitive[of "|A <+> C|"] by blast |
|
640 |
|
641 |
|
642 corollary ordLeq_Plus_mono: |
|
643 assumes "r \<le>o r'" and "p \<le>o p'" |
|
644 shows "|(Field r) <+> (Field p)| \<le>o |(Field r') <+> (Field p')|" |
|
645 using assms card_of_mono2[of r r'] card_of_mono2[of p p'] card_of_Plus_mono by blast |
|
646 |
|
647 |
|
648 lemma card_of_Plus_cong1: |
|
649 assumes "|A| =o |B|" |
|
650 shows "|A <+> C| =o |B <+> C|" |
|
651 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono1) |
|
652 |
|
653 |
|
654 corollary ordIso_Plus_cong1: |
|
655 assumes "r =o r'" |
|
656 shows "|(Field r) <+> C| =o |(Field r') <+> C|" |
|
657 using assms card_of_cong card_of_Plus_cong1 by blast |
|
658 |
|
659 |
|
660 lemma card_of_Plus_cong2: |
|
661 assumes "|A| =o |B|" |
|
662 shows "|C <+> A| =o |C <+> B|" |
|
663 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono2) |
|
664 |
|
665 |
|
666 corollary ordIso_Plus_cong2: |
|
667 assumes "r =o r'" |
|
668 shows "|A <+> (Field r)| =o |A <+> (Field r')|" |
|
669 using assms card_of_cong card_of_Plus_cong2 by blast |
|
670 |
|
671 |
|
672 lemma card_of_Plus_cong: |
|
673 assumes "|A| =o |B|" and "|C| =o |D|" |
|
674 shows "|A <+> C| =o |B <+> D|" |
|
675 using assms by (simp add: ordIso_iff_ordLeq card_of_Plus_mono) |
|
676 |
|
677 |
|
678 corollary ordIso_Plus_cong: |
|
679 assumes "r =o r'" and "p =o p'" |
|
680 shows "|(Field r) <+> (Field p)| =o |(Field r') <+> (Field p')|" |
|
681 using assms card_of_cong[of r r'] card_of_cong[of p p'] card_of_Plus_cong by blast |
|
682 |
|
683 |
|
684 lemma card_of_Un1: |
|
685 shows "|A| \<le>o |A \<union> B| " |
|
686 using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce |
|
687 |
|
688 |
|
689 lemma card_of_diff: |
|
690 shows "|A - B| \<le>o |A|" |
|
691 using inj_on_id[of "A - B"] card_of_ordLeq[of "A - B" _] by fastforce |
|
692 |
|
693 |
|
694 lemma card_of_Un_Plus_ordLeq: |
|
695 "|A \<union> B| \<le>o |A <+> B|" |
|
696 proof- |
|
697 let ?f = "\<lambda> c. if c \<in> A then Inl c else Inr c" |
|
698 have "inj_on ?f (A \<union> B) \<and> ?f ` (A \<union> B) \<le> A <+> B" |
|
699 unfolding inj_on_def by auto |
|
700 thus ?thesis using card_of_ordLeq by blast |
|
701 qed |
|
702 |
|
703 |
|
704 lemma card_of_Times1: |
|
705 assumes "A \<noteq> {}" |
|
706 shows "|B| \<le>o |B \<times> A|" |
|
707 proof(cases "B = {}", simp add: card_of_empty) |
|
708 assume *: "B \<noteq> {}" |
|
709 have "fst `(B \<times> A) = B" unfolding image_def using assms by auto |
|
710 thus ?thesis using inj_on_iff_surj[of B "B \<times> A"] |
|
711 card_of_ordLeq[of B "B \<times> A"] * by blast |
|
712 qed |
|
713 |
|
714 |
|
715 corollary Card_order_Times1: |
|
716 "\<lbrakk>Card_order r; B \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |(Field r) \<times> B|" |
|
717 using card_of_Times1[of B] card_of_Field_ordIso |
|
718 ordIso_ordLeq_trans ordIso_symmetric by blast |
|
719 |
|
720 |
|
721 lemma card_of_Times_commute: "|A \<times> B| =o |B \<times> A|" |
|
722 proof- |
|
723 let ?f = "\<lambda>(a::'a,b::'b). (b,a)" |
|
724 have "bij_betw ?f (A \<times> B) (B \<times> A)" |
|
725 unfolding bij_betw_def inj_on_def by auto |
|
726 thus ?thesis using card_of_ordIso by blast |
|
727 qed |
|
728 |
|
729 |
|
730 lemma card_of_Times2: |
|
731 assumes "A \<noteq> {}" shows "|B| \<le>o |A \<times> B|" |
|
732 using assms card_of_Times1[of A B] card_of_Times_commute[of B A] |
|
733 ordLeq_ordIso_trans by blast |
|
734 |
|
735 |
|
736 corollary Card_order_Times2: |
|
737 "\<lbrakk>Card_order r; A \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o |A \<times> (Field r)|" |
|
738 using card_of_Times2[of A] card_of_Field_ordIso |
|
739 ordIso_ordLeq_trans ordIso_symmetric by blast |
|
740 |
|
741 |
|
742 lemma card_of_Times3: "|A| \<le>o |A \<times> A|" |
|
743 using card_of_Times1[of A] |
|
744 by(cases "A = {}", simp add: card_of_empty, blast) |
|
745 |
|
746 |
|
747 lemma card_of_Plus_Times_bool: "|A <+> A| =o |A \<times> (UNIV::bool set)|" |
|
748 proof- |
|
749 let ?f = "\<lambda>c::'a + 'a. case c of Inl a \<Rightarrow> (a,True) |
|
750 |Inr a \<Rightarrow> (a,False)" |
|
751 have "bij_betw ?f (A <+> A) (A \<times> (UNIV::bool set))" |
|
752 proof- |
|
753 {fix c1 and c2 assume "?f c1 = ?f c2" |
|
754 hence "c1 = c2" |
|
755 by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto) |
|
756 } |
|
757 moreover |
|
758 {fix c assume "c \<in> A <+> A" |
|
759 hence "?f c \<in> A \<times> (UNIV::bool set)" |
|
760 by(case_tac c, auto) |
|
761 } |
|
762 moreover |
|
763 {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)" |
|
764 have "(a,bl) \<in> ?f ` ( A <+> A)" |
|
765 proof(cases bl) |
|
766 assume bl hence "?f(Inl a) = (a,bl)" by auto |
|
767 thus ?thesis using * by force |
|
768 next |
|
769 assume "\<not> bl" hence "?f(Inr a) = (a,bl)" by auto |
|
770 thus ?thesis using * by force |
|
771 qed |
|
772 } |
|
773 ultimately show ?thesis unfolding bij_betw_def inj_on_def by auto |
|
774 qed |
|
775 thus ?thesis using card_of_ordIso by blast |
|
776 qed |
|
777 |
|
778 |
|
779 lemma card_of_Times_mono1: |
|
780 assumes "|A| \<le>o |B|" |
|
781 shows "|A \<times> C| \<le>o |B \<times> C|" |
|
782 proof- |
|
783 obtain f where 1: "inj_on f A \<and> f ` A \<le> B" |
|
784 using assms card_of_ordLeq[of A] by fastforce |
|
785 obtain g where g_def: |
|
786 "g = (\<lambda>(a,c::'c). (f a,c))" by blast |
|
787 have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)" |
|
788 using 1 unfolding inj_on_def using g_def by auto |
|
789 thus ?thesis using card_of_ordLeq by metis |
|
790 qed |
|
791 |
|
792 |
|
793 corollary ordLeq_Times_mono1: |
|
794 assumes "r \<le>o r'" |
|
795 shows "|(Field r) \<times> C| \<le>o |(Field r') \<times> C|" |
|
796 using assms card_of_mono2 card_of_Times_mono1 by blast |
|
797 |
|
798 |
|
799 lemma card_of_Times_mono2: |
|
800 assumes "|A| \<le>o |B|" |
|
801 shows "|C \<times> A| \<le>o |C \<times> B|" |
|
802 using assms card_of_Times_mono1[of A B C] |
|
803 card_of_Times_commute[of C A] card_of_Times_commute[of B C] |
|
804 ordIso_ordLeq_trans[of "|C \<times> A|"] ordLeq_ordIso_trans[of "|C \<times> A|"] |
|
805 by blast |
|
806 |
|
807 |
|
808 corollary ordLeq_Times_mono2: |
|
809 assumes "r \<le>o r'" |
|
810 shows "|A \<times> (Field r)| \<le>o |A \<times> (Field r')|" |
|
811 using assms card_of_mono2 card_of_Times_mono2 by blast |
|
812 |
|
813 |
|
814 lemma card_of_Times_cong1: |
|
815 assumes "|A| =o |B|" |
|
816 shows "|A \<times> C| =o |B \<times> C|" |
|
817 using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1) |
|
818 |
|
819 |
|
820 lemma card_of_Times_cong2: |
|
821 assumes "|A| =o |B|" |
|
822 shows "|C \<times> A| =o |C \<times> B|" |
|
823 using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2) |
|
824 |
|
825 |
|
826 corollary ordIso_Times_cong2: |
|
827 assumes "r =o r'" |
|
828 shows "|A \<times> (Field r)| =o |A \<times> (Field r')|" |
|
829 using assms card_of_cong card_of_Times_cong2 by blast |
|
830 |
|
831 |
|
832 lemma card_of_Sigma_mono1: |
|
833 assumes "\<forall>i \<in> I. |A i| \<le>o |B i|" |
|
834 shows "|SIGMA i : I. A i| \<le>o |SIGMA i : I. B i|" |
|
835 proof- |
|
836 have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)" |
|
837 using assms by (auto simp add: card_of_ordLeq) |
|
838 with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"] |
|
839 obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by metis |
|
840 obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast |
|
841 have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)" |
|
842 using 1 unfolding inj_on_def using g_def by force |
|
843 thus ?thesis using card_of_ordLeq by metis |
|
844 qed |
|
845 |
|
846 |
|
847 corollary card_of_Sigma_Times: |
|
848 "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|" |
|
849 using card_of_Sigma_mono1[of I A "\<lambda>i. B"] . |
|
850 |
|
851 |
|
852 lemma card_of_UNION_Sigma: |
|
853 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|" |
|
854 using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis |
|
855 |
|
856 |
|
857 lemma card_of_bool: |
|
858 assumes "a1 \<noteq> a2" |
|
859 shows "|UNIV::bool set| =o |{a1,a2}|" |
|
860 proof- |
|
861 let ?f = "\<lambda> bl. case bl of True \<Rightarrow> a1 | False \<Rightarrow> a2" |
|
862 have "bij_betw ?f UNIV {a1,a2}" |
|
863 proof- |
|
864 {fix bl1 and bl2 assume "?f bl1 = ?f bl2" |
|
865 hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto) |
|
866 } |
|
867 moreover |
|
868 {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto) |
|
869 } |
|
870 moreover |
|
871 {fix a assume *: "a \<in> {a1,a2}" |
|
872 have "a \<in> ?f ` UNIV" |
|
873 proof(cases "a = a1") |
|
874 assume "a = a1" |
|
875 hence "?f True = a" by auto thus ?thesis by blast |
|
876 next |
|
877 assume "a \<noteq> a1" hence "a = a2" using * by auto |
|
878 hence "?f False = a" by auto thus ?thesis by blast |
|
879 qed |
|
880 } |
|
881 ultimately show ?thesis unfolding bij_betw_def inj_on_def |
|
882 by (metis image_subsetI order_eq_iff subsetI) |
|
883 qed |
|
884 thus ?thesis using card_of_ordIso by blast |
|
885 qed |
|
886 |
|
887 |
|
888 lemma card_of_Plus_Times_aux: |
|
889 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and |
|
890 LEQ: "|A| \<le>o |B|" |
|
891 shows "|A <+> B| \<le>o |A \<times> B|" |
|
892 proof- |
|
893 have 1: "|UNIV::bool set| \<le>o |A|" |
|
894 using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2] |
|
895 ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis |
|
896 (* *) |
|
897 have "|A <+> B| \<le>o |B <+> B|" |
|
898 using LEQ card_of_Plus_mono1 by blast |
|
899 moreover have "|B <+> B| =o |B \<times> (UNIV::bool set)|" |
|
900 using card_of_Plus_Times_bool by blast |
|
901 moreover have "|B \<times> (UNIV::bool set)| \<le>o |B \<times> A|" |
|
902 using 1 by (simp add: card_of_Times_mono2) |
|
903 moreover have " |B \<times> A| =o |A \<times> B|" |
|
904 using card_of_Times_commute by blast |
|
905 ultimately show "|A <+> B| \<le>o |A \<times> B|" |
|
906 using ordLeq_ordIso_trans[of "|A <+> B|" "|B <+> B|" "|B \<times> (UNIV::bool set)|"] |
|
907 ordLeq_transitive[of "|A <+> B|" "|B \<times> (UNIV::bool set)|" "|B \<times> A|"] |
|
908 ordLeq_ordIso_trans[of "|A <+> B|" "|B \<times> A|" "|A \<times> B|"] |
|
909 by blast |
|
910 qed |
|
911 |
|
912 |
|
913 lemma card_of_Plus_Times: |
|
914 assumes A2: "a1 \<noteq> a2 \<and> {a1,a2} \<le> A" and |
|
915 B2: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" |
|
916 shows "|A <+> B| \<le>o |A \<times> B|" |
|
917 proof- |
|
918 {assume "|A| \<le>o |B|" |
|
919 hence ?thesis using assms by (auto simp add: card_of_Plus_Times_aux) |
|
920 } |
|
921 moreover |
|
922 {assume "|B| \<le>o |A|" |
|
923 hence "|B <+> A| \<le>o |B \<times> A|" |
|
924 using assms by (auto simp add: card_of_Plus_Times_aux) |
|
925 hence ?thesis |
|
926 using card_of_Plus_commute card_of_Times_commute |
|
927 ordIso_ordLeq_trans ordLeq_ordIso_trans by metis |
|
928 } |
|
929 ultimately show ?thesis |
|
930 using card_of_Well_order[of A] card_of_Well_order[of B] |
|
931 ordLeq_total[of "|A|"] by metis |
|
932 qed |
|
933 |
|
934 |
|
935 lemma card_of_ordLeq_finite: |
|
936 assumes "|A| \<le>o |B|" and "finite B" |
|
937 shows "finite A" |
|
938 using assms unfolding ordLeq_def |
|
939 using embed_inj_on[of "|A|" "|B|"] embed_Field[of "|A|" "|B|"] |
|
940 Field_card_of[of "A"] Field_card_of[of "B"] inj_on_finite[of _ "A" "B"] by fastforce |
|
941 |
|
942 |
|
943 lemma card_of_ordLeq_infinite: |
|
944 assumes "|A| \<le>o |B|" and "infinite A" |
|
945 shows "infinite B" |
|
946 using assms card_of_ordLeq_finite by auto |
|
947 |
|
948 |
|
949 lemma card_of_ordIso_finite: |
|
950 assumes "|A| =o |B|" |
|
951 shows "finite A = finite B" |
|
952 using assms unfolding ordIso_def iso_def[abs_def] |
|
953 by (auto simp: bij_betw_finite Field_card_of) |
|
954 |
|
955 |
|
956 lemma card_of_ordIso_finite_Field: |
|
957 assumes "Card_order r" and "r =o |A|" |
|
958 shows "finite(Field r) = finite A" |
|
959 using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast |
|
960 |
|
961 |
|
962 subsection {* Cardinals versus set operations involving infinite sets *} |
|
963 |
|
964 |
|
965 text{* Here we show that, for infinite sets, most set-theoretic constructions |
|
966 do not increase the cardinality. The cornerstone for this is |
|
967 theorem @{text "Card_order_Times_same_infinite"}, which states that self-product |
|
968 does not increase cardinality -- the proof of this fact adapts a standard |
|
969 set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11 |
|
970 at page 47 in \cite{card-book}. Then everything else follows fairly easily. *} |
|
971 |
|
972 |
|
973 lemma infinite_iff_card_of_nat: |
|
974 "infinite A = ( |UNIV::nat set| \<le>o |A| )" |
|
975 by (auto simp add: infinite_iff_countable_subset card_of_ordLeq) |
|
976 |
|
977 |
|
978 lemma finite_iff_cardOf_nat: |
|
979 "finite A = ( |A| <o |UNIV :: nat set| )" |
|
980 using infinite_iff_card_of_nat[of A] |
|
981 not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"] |
|
982 by (fastforce simp: card_of_Well_order) |
|
983 |
|
984 lemma finite_ordLess_infinite2: |
|
985 assumes "finite A" and "infinite B" |
|
986 shows "|A| <o |B|" |
|
987 using assms |
|
988 finite_ordLess_infinite[of "|A|" "|B|"] |
|
989 card_of_Well_order[of A] card_of_Well_order[of B] |
|
990 Field_card_of[of A] Field_card_of[of B] by auto |
|
991 |
|
992 |
|
993 text{* The next two results correspond to the ZF fact that all infinite cardinals are |
|
994 limit ordinals: *} |
|
995 |
|
996 lemma Card_order_infinite_not_under: |
|
997 assumes CARD: "Card_order r" and INF: "infinite (Field r)" |
|
998 shows "\<not> (\<exists>a. Field r = rel.under r a)" |
|
999 proof(auto) |
|
1000 have 0: "Well_order r \<and> wo_rel r \<and> Refl r" |
|
1001 using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto |
|
1002 fix a assume *: "Field r = rel.under r a" |
|
1003 show False |
|
1004 proof(cases "a \<in> Field r") |
|
1005 assume Case1: "a \<notin> Field r" |
|
1006 hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto |
|
1007 thus False using INF * by auto |
|
1008 next |
|
1009 let ?r' = "Restr r (rel.underS r a)" |
|
1010 assume Case2: "a \<in> Field r" |
|
1011 hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a" |
|
1012 using 0 rel.Refl_under_underS rel.underS_notIn by fastforce |
|
1013 have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r" |
|
1014 using 0 wo_rel.underS_ofilter * 1 Case2 by auto |
|
1015 hence "?r' <o r" using 0 using ofilter_ordLess by blast |
|
1016 moreover |
|
1017 have "Field ?r' = rel.underS r a \<and> Well_order ?r'" |
|
1018 using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast |
|
1019 ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto |
|
1020 moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto |
|
1021 ultimately have "|rel.underS r a| <o |rel.under r a|" |
|
1022 using ordIso_symmetric ordLess_ordIso_trans by blast |
|
1023 moreover |
|
1024 {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)" |
|
1025 using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto |
|
1026 hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast |
|
1027 } |
|
1028 ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast |
|
1029 qed |
|
1030 qed |
|
1031 |
|
1032 |
|
1033 lemma infinite_Card_order_limit: |
|
1034 assumes r: "Card_order r" and "infinite (Field r)" |
|
1035 and a: "a : Field r" |
|
1036 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r" |
|
1037 proof- |
|
1038 have "Field r \<noteq> rel.under r a" |
|
1039 using assms Card_order_infinite_not_under by blast |
|
1040 moreover have "rel.under r a \<le> Field r" |
|
1041 using rel.under_Field . |
|
1042 ultimately have "rel.under r a < Field r" by blast |
|
1043 then obtain b where 1: "b : Field r \<and> ~ (b,a) : r" |
|
1044 unfolding rel.under_def by blast |
|
1045 moreover have ba: "b \<noteq> a" |
|
1046 using 1 r unfolding card_order_on_def well_order_on_def |
|
1047 linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto |
|
1048 ultimately have "(a,b) : r" |
|
1049 using a r unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
1050 total_on_def by blast |
|
1051 thus ?thesis using 1 ba by auto |
|
1052 qed |
|
1053 |
|
1054 |
|
1055 theorem Card_order_Times_same_infinite: |
|
1056 assumes CO: "Card_order r" and INF: "infinite(Field r)" |
|
1057 shows "|Field r \<times> Field r| \<le>o r" |
|
1058 proof- |
|
1059 obtain phi where phi_def: |
|
1060 "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and> |
|
1061 \<not> |Field r \<times> Field r| \<le>o r )" by blast |
|
1062 have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r" |
|
1063 unfolding phi_def card_order_on_def by auto |
|
1064 have Ft: "\<not>(\<exists>r. phi r)" |
|
1065 proof |
|
1066 assume "\<exists>r. phi r" |
|
1067 hence "{r. phi r} \<noteq> {} \<and> {r. phi r} \<le> {r. Well_order r}" |
|
1068 using temp1 by auto |
|
1069 then obtain r where 1: "phi r" and 2: "\<forall>r'. phi r' \<longrightarrow> r \<le>o r'" and |
|
1070 3: "Card_order r \<and> Well_order r" |
|
1071 using exists_minim_Well_order[of "{r. phi r}"] temp1 phi_def by blast |
|
1072 let ?A = "Field r" let ?r' = "bsqr r" |
|
1073 have 4: "Well_order ?r' \<and> Field ?r' = ?A \<times> ?A \<and> |?A| =o r" |
|
1074 using 3 bsqr_Well_order Field_bsqr card_of_Field_ordIso by blast |
|
1075 have 5: "Card_order |?A \<times> ?A| \<and> Well_order |?A \<times> ?A|" |
|
1076 using card_of_Card_order card_of_Well_order by blast |
|
1077 (* *) |
|
1078 have "r <o |?A \<times> ?A|" |
|
1079 using 1 3 5 ordLess_or_ordLeq unfolding phi_def by blast |
|
1080 moreover have "|?A \<times> ?A| \<le>o ?r'" |
|
1081 using card_of_least[of "?A \<times> ?A"] 4 by auto |
|
1082 ultimately have "r <o ?r'" using ordLess_ordLeq_trans by auto |
|
1083 then obtain f where 6: "embed r ?r' f" and 7: "\<not> bij_betw f ?A (?A \<times> ?A)" |
|
1084 unfolding ordLess_def embedS_def[abs_def] |
|
1085 by (auto simp add: Field_bsqr) |
|
1086 let ?B = "f ` ?A" |
|
1087 have "|?A| =o |?B|" |
|
1088 using 3 6 embed_inj_on inj_on_imp_bij_betw card_of_ordIso by blast |
|
1089 hence 8: "r =o |?B|" using 4 ordIso_transitive ordIso_symmetric by blast |
|
1090 (* *) |
|
1091 have "wo_rel.ofilter ?r' ?B" |
|
1092 using 6 embed_Field_ofilter 3 4 by blast |
|
1093 hence "wo_rel.ofilter ?r' ?B \<and> ?B \<noteq> ?A \<times> ?A \<and> ?B \<noteq> Field ?r'" |
|
1094 using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto |
|
1095 hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A" |
|
1096 using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast |
|
1097 have "\<not> (\<exists>a. Field r = rel.under r a)" |
|
1098 using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto |
|
1099 then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1" |
|
1100 using temp2 3 bsqr_ofilter[of r ?B] by blast |
|
1101 hence "|?B| \<le>o |A1 \<times> A1|" using card_of_mono1 by blast |
|
1102 hence 10: "r \<le>o |A1 \<times> A1|" using 8 ordIso_ordLeq_trans by blast |
|
1103 let ?r1 = "Restr r A1" |
|
1104 have "?r1 <o r" using temp3 ofilter_ordLess 3 by blast |
|
1105 moreover |
|
1106 {have "well_order_on A1 ?r1" using 3 temp3 well_order_on_Restr by blast |
|
1107 hence "|A1| \<le>o ?r1" using 3 Well_order_Restr card_of_least by blast |
|
1108 } |
|
1109 ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast |
|
1110 (* *) |
|
1111 have "infinite (Field r)" using 1 unfolding phi_def by simp |
|
1112 hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast |
|
1113 hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast |
|
1114 moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|" |
|
1115 using card_of_Card_order[of A1] card_of_Well_order[of A1] |
|
1116 by (simp add: Field_card_of) |
|
1117 moreover have "\<not> r \<le>o | A1 |" |
|
1118 using temp4 11 3 using not_ordLeq_iff_ordLess by blast |
|
1119 ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |" |
|
1120 by (simp add: card_of_card_order_on) |
|
1121 hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|" |
|
1122 using 2 unfolding phi_def by blast |
|
1123 hence "|A1 \<times> A1 | \<le>o |A1|" using temp4 by auto |
|
1124 hence "r \<le>o |A1|" using 10 ordLeq_transitive by blast |
|
1125 thus False using 11 not_ordLess_ordLeq by auto |
|
1126 qed |
|
1127 thus ?thesis using assms unfolding phi_def by blast |
|
1128 qed |
|
1129 |
|
1130 |
|
1131 corollary card_of_Times_same_infinite: |
|
1132 assumes "infinite A" |
|
1133 shows "|A \<times> A| =o |A|" |
|
1134 proof- |
|
1135 let ?r = "|A|" |
|
1136 have "Field ?r = A \<and> Card_order ?r" |
|
1137 using Field_card_of card_of_Card_order[of A] by fastforce |
|
1138 hence "|A \<times> A| \<le>o |A|" |
|
1139 using Card_order_Times_same_infinite[of ?r] assms by auto |
|
1140 thus ?thesis using card_of_Times3 ordIso_iff_ordLeq by blast |
|
1141 qed |
|
1142 |
|
1143 |
|
1144 lemma card_of_Times_infinite: |
|
1145 assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|" |
|
1146 shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|" |
|
1147 proof- |
|
1148 have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|" |
|
1149 using assms by (simp add: card_of_Times1 card_of_Times2) |
|
1150 moreover |
|
1151 {have "|A \<times> B| \<le>o |A \<times> A| \<and> |B \<times> A| \<le>o |A \<times> A|" |
|
1152 using LEQ card_of_Times_mono1 card_of_Times_mono2 by blast |
|
1153 moreover have "|A \<times> A| =o |A|" using INF card_of_Times_same_infinite by blast |
|
1154 ultimately have "|A \<times> B| \<le>o |A| \<and> |B \<times> A| \<le>o |A|" |
|
1155 using ordLeq_ordIso_trans[of "|A \<times> B|"] ordLeq_ordIso_trans[of "|B \<times> A|"] by auto |
|
1156 } |
|
1157 ultimately show ?thesis by (simp add: ordIso_iff_ordLeq) |
|
1158 qed |
|
1159 |
|
1160 |
|
1161 corollary card_of_Times_infinite_simps: |
|
1162 "\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|" |
|
1163 "\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|" |
|
1164 "\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|" |
|
1165 "\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|" |
|
1166 by (auto simp add: card_of_Times_infinite ordIso_symmetric) |
|
1167 |
|
1168 |
|
1169 corollary Card_order_Times_infinite: |
|
1170 assumes INF: "infinite(Field r)" and CARD: "Card_order r" and |
|
1171 NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r" |
|
1172 shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r" |
|
1173 proof- |
|
1174 have "|Field r \<times> Field p| =o |Field r| \<and> |Field p \<times> Field r| =o |Field r|" |
|
1175 using assms by (simp add: card_of_Times_infinite card_of_mono2) |
|
1176 thus ?thesis |
|
1177 using assms card_of_Field_ordIso[of r] |
|
1178 ordIso_transitive[of "|Field r \<times> Field p|"] |
|
1179 ordIso_transitive[of _ "|Field r|"] by blast |
|
1180 qed |
|
1181 |
|
1182 |
|
1183 lemma card_of_Sigma_ordLeq_infinite: |
|
1184 assumes INF: "infinite B" and |
|
1185 LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|" |
|
1186 shows "|SIGMA i : I. A i| \<le>o |B|" |
|
1187 proof(cases "I = {}", simp add: card_of_empty) |
|
1188 assume *: "I \<noteq> {}" |
|
1189 have "|SIGMA i : I. A i| \<le>o |I \<times> B|" |
|
1190 using LEQ card_of_Sigma_Times by blast |
|
1191 moreover have "|I \<times> B| =o |B|" |
|
1192 using INF * LEQ_I by (auto simp add: card_of_Times_infinite) |
|
1193 ultimately show ?thesis using ordLeq_ordIso_trans by blast |
|
1194 qed |
|
1195 |
|
1196 |
|
1197 lemma card_of_Sigma_ordLeq_infinite_Field: |
|
1198 assumes INF: "infinite (Field r)" and r: "Card_order r" and |
|
1199 LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r" |
|
1200 shows "|SIGMA i : I. A i| \<le>o r" |
|
1201 proof- |
|
1202 let ?B = "Field r" |
|
1203 have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso |
|
1204 ordIso_symmetric by blast |
|
1205 hence "|I| \<le>o |?B|" "\<forall>i \<in> I. |A i| \<le>o |?B|" |
|
1206 using LEQ_I LEQ ordLeq_ordIso_trans by blast+ |
|
1207 hence "|SIGMA i : I. A i| \<le>o |?B|" using INF LEQ |
|
1208 card_of_Sigma_ordLeq_infinite by blast |
|
1209 thus ?thesis using 1 ordLeq_ordIso_trans by blast |
|
1210 qed |
|
1211 |
|
1212 |
|
1213 lemma card_of_Times_ordLeq_infinite_Field: |
|
1214 "\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk> |
|
1215 \<Longrightarrow> |A <*> B| \<le>o r" |
|
1216 by(simp add: card_of_Sigma_ordLeq_infinite_Field) |
|
1217 |
|
1218 |
|
1219 lemma card_of_UNION_ordLeq_infinite: |
|
1220 assumes INF: "infinite B" and |
|
1221 LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|" |
|
1222 shows "|\<Union> i \<in> I. A i| \<le>o |B|" |
|
1223 proof(cases "I = {}", simp add: card_of_empty) |
|
1224 assume *: "I \<noteq> {}" |
|
1225 have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|" |
|
1226 using card_of_UNION_Sigma by blast |
|
1227 moreover have "|SIGMA i : I. A i| \<le>o |B|" |
|
1228 using assms card_of_Sigma_ordLeq_infinite by blast |
|
1229 ultimately show ?thesis using ordLeq_transitive by blast |
|
1230 qed |
|
1231 |
|
1232 |
|
1233 corollary card_of_UNION_ordLeq_infinite_Field: |
|
1234 assumes INF: "infinite (Field r)" and r: "Card_order r" and |
|
1235 LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r" |
|
1236 shows "|\<Union> i \<in> I. A i| \<le>o r" |
|
1237 proof- |
|
1238 let ?B = "Field r" |
|
1239 have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso |
|
1240 ordIso_symmetric by blast |
|
1241 hence "|I| \<le>o |?B|" "\<forall>i \<in> I. |A i| \<le>o |?B|" |
|
1242 using LEQ_I LEQ ordLeq_ordIso_trans by blast+ |
|
1243 hence "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ |
|
1244 card_of_UNION_ordLeq_infinite by blast |
|
1245 thus ?thesis using 1 ordLeq_ordIso_trans by blast |
|
1246 qed |
|
1247 |
|
1248 |
|
1249 lemma card_of_Plus_infinite1: |
|
1250 assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|" |
|
1251 shows "|A <+> B| =o |A|" |
|
1252 proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric) |
|
1253 let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b" let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b" |
|
1254 assume *: "B \<noteq> {}" |
|
1255 then obtain b1 where 1: "b1 \<in> B" by blast |
|
1256 show ?thesis |
|
1257 proof(cases "B = {b1}") |
|
1258 assume Case1: "B = {b1}" |
|
1259 have 2: "bij_betw ?Inl A ((?Inl ` A))" |
|
1260 unfolding bij_betw_def inj_on_def by auto |
|
1261 hence 3: "infinite (?Inl ` A)" |
|
1262 using INF bij_betw_finite[of ?Inl A] by blast |
|
1263 let ?A' = "?Inl ` A \<union> {?Inr b1}" |
|
1264 obtain g where "bij_betw g (?Inl ` A) ?A'" |
|
1265 using 3 infinite_imp_bij_betw2[of "?Inl ` A"] by auto |
|
1266 moreover have "?A' = A <+> B" using Case1 by blast |
|
1267 ultimately have "bij_betw g (?Inl ` A) (A <+> B)" by simp |
|
1268 hence "bij_betw (g o ?Inl) A (A <+> B)" |
|
1269 using 2 by (auto simp add: bij_betw_trans) |
|
1270 thus ?thesis using card_of_ordIso ordIso_symmetric by blast |
|
1271 next |
|
1272 assume Case2: "B \<noteq> {b1}" |
|
1273 with * 1 obtain b2 where 3: "b1 \<noteq> b2 \<and> {b1,b2} \<le> B" by fastforce |
|
1274 obtain f where "inj_on f B \<and> f ` B \<le> A" |
|
1275 using LEQ card_of_ordLeq[of B] by fastforce |
|
1276 with 3 have "f b1 \<noteq> f b2 \<and> {f b1, f b2} \<le> A" |
|
1277 unfolding inj_on_def by auto |
|
1278 with 3 have "|A <+> B| \<le>o |A \<times> B|" |
|
1279 by (auto simp add: card_of_Plus_Times) |
|
1280 moreover have "|A \<times> B| =o |A|" |
|
1281 using assms * by (simp add: card_of_Times_infinite_simps) |
|
1282 ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis |
|
1283 thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast |
|
1284 qed |
|
1285 qed |
|
1286 |
|
1287 |
|
1288 lemma card_of_Plus_infinite2: |
|
1289 assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|" |
|
1290 shows "|B <+> A| =o |A|" |
|
1291 using assms card_of_Plus_commute card_of_Plus_infinite1 |
|
1292 ordIso_equivalence by blast |
|
1293 |
|
1294 |
|
1295 lemma card_of_Plus_infinite: |
|
1296 assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|" |
|
1297 shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|" |
|
1298 using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2) |
|
1299 |
|
1300 |
|
1301 corollary Card_order_Plus_infinite: |
|
1302 assumes INF: "infinite(Field r)" and CARD: "Card_order r" and |
|
1303 LEQ: "p \<le>o r" |
|
1304 shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r" |
|
1305 proof- |
|
1306 have "| Field r <+> Field p | =o | Field r | \<and> |
|
1307 | Field p <+> Field r | =o | Field r |" |
|
1308 using assms by (simp add: card_of_Plus_infinite card_of_mono2) |
|
1309 thus ?thesis |
|
1310 using assms card_of_Field_ordIso[of r] |
|
1311 ordIso_transitive[of "|Field r <+> Field p|"] |
|
1312 ordIso_transitive[of _ "|Field r|"] by blast |
|
1313 qed |
|
1314 |
|
1315 |
|
1316 lemma card_of_Un_infinite: |
|
1317 assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|" |
|
1318 shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|" |
|
1319 proof- |
|
1320 have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq) |
|
1321 moreover have "|A <+> B| =o |A|" |
|
1322 using assms by (metis card_of_Plus_infinite) |
|
1323 ultimately have "|A \<union> B| \<le>o |A|" using ordLeq_ordIso_trans by blast |
|
1324 hence "|A \<union> B| =o |A|" using card_of_Un1 ordIso_iff_ordLeq by blast |
|
1325 thus ?thesis using Un_commute[of B A] by auto |
|
1326 qed |
|
1327 |
|
1328 |
|
1329 lemma card_of_Un_diff_infinite: |
|
1330 assumes INF: "infinite A" and LESS: "|B| <o |A|" |
|
1331 shows "|A - B| =o |A|" |
|
1332 proof- |
|
1333 obtain C where C_def: "C = A - B" by blast |
|
1334 have "|A \<union> B| =o |A|" |
|
1335 using assms ordLeq_iff_ordLess_or_ordIso card_of_Un_infinite by blast |
|
1336 moreover have "C \<union> B = A \<union> B" unfolding C_def by auto |
|
1337 ultimately have 1: "|C \<union> B| =o |A|" by auto |
|
1338 (* *) |
|
1339 {assume *: "|C| \<le>o |B|" |
|
1340 moreover |
|
1341 {assume **: "finite B" |
|
1342 hence "finite C" |
|
1343 using card_of_ordLeq_finite * by blast |
|
1344 hence False using ** INF card_of_ordIso_finite 1 by blast |
|
1345 } |
|
1346 hence "infinite B" by auto |
|
1347 ultimately have False |
|
1348 using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis |
|
1349 } |
|
1350 hence 2: "|B| \<le>o |C|" using card_of_Well_order ordLeq_total by blast |
|
1351 {assume *: "finite C" |
|
1352 hence "finite B" using card_of_ordLeq_finite 2 by blast |
|
1353 hence False using * INF card_of_ordIso_finite 1 by blast |
|
1354 } |
|
1355 hence "infinite C" by auto |
|
1356 hence "|C| =o |A|" |
|
1357 using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis |
|
1358 thus ?thesis unfolding C_def . |
|
1359 qed |
|
1360 |
|
1361 |
|
1362 lemma card_of_Plus_ordLess_infinite: |
|
1363 assumes INF: "infinite C" and |
|
1364 LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|" |
|
1365 shows "|A <+> B| <o |C|" |
|
1366 proof(cases "A = {} \<or> B = {}") |
|
1367 assume Case1: "A = {} \<or> B = {}" |
|
1368 hence "|A| =o |A <+> B| \<or> |B| =o |A <+> B|" |
|
1369 using card_of_Plus_empty1 card_of_Plus_empty2 by blast |
|
1370 hence "|A <+> B| =o |A| \<or> |A <+> B| =o |B|" |
|
1371 using ordIso_symmetric[of "|A|"] ordIso_symmetric[of "|B|"] by blast |
|
1372 thus ?thesis using LESS1 LESS2 |
|
1373 ordIso_ordLess_trans[of "|A <+> B|" "|A|"] |
|
1374 ordIso_ordLess_trans[of "|A <+> B|" "|B|"] by blast |
|
1375 next |
|
1376 assume Case2: "\<not>(A = {} \<or> B = {})" |
|
1377 {assume *: "|C| \<le>o |A <+> B|" |
|
1378 hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast |
|
1379 hence 1: "infinite A \<or> infinite B" using finite_Plus by blast |
|
1380 {assume Case21: "|A| \<le>o |B|" |
|
1381 hence "infinite B" using 1 card_of_ordLeq_finite by blast |
|
1382 hence "|A <+> B| =o |B|" using Case2 Case21 |
|
1383 by (auto simp add: card_of_Plus_infinite) |
|
1384 hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1385 } |
|
1386 moreover |
|
1387 {assume Case22: "|B| \<le>o |A|" |
|
1388 hence "infinite A" using 1 card_of_ordLeq_finite by blast |
|
1389 hence "|A <+> B| =o |A|" using Case2 Case22 |
|
1390 by (auto simp add: card_of_Plus_infinite) |
|
1391 hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast |
|
1392 } |
|
1393 ultimately have False using ordLeq_total card_of_Well_order[of A] |
|
1394 card_of_Well_order[of B] by blast |
|
1395 } |
|
1396 thus ?thesis using ordLess_or_ordLeq[of "|A <+> B|" "|C|"] |
|
1397 card_of_Well_order[of "A <+> B"] card_of_Well_order[of "C"] by auto |
|
1398 qed |
|
1399 |
|
1400 |
|
1401 lemma card_of_Plus_ordLess_infinite_Field: |
|
1402 assumes INF: "infinite (Field r)" and r: "Card_order r" and |
|
1403 LESS1: "|A| <o r" and LESS2: "|B| <o r" |
|
1404 shows "|A <+> B| <o r" |
|
1405 proof- |
|
1406 let ?C = "Field r" |
|
1407 have 1: "r =o |?C| \<and> |?C| =o r" using r card_of_Field_ordIso |
|
1408 ordIso_symmetric by blast |
|
1409 hence "|A| <o |?C|" "|B| <o |?C|" |
|
1410 using LESS1 LESS2 ordLess_ordIso_trans by blast+ |
|
1411 hence "|A <+> B| <o |?C|" using INF |
|
1412 card_of_Plus_ordLess_infinite by blast |
|
1413 thus ?thesis using 1 ordLess_ordIso_trans by blast |
|
1414 qed |
|
1415 |
|
1416 |
|
1417 lemma infinite_card_of_insert: |
|
1418 assumes "infinite A" |
|
1419 shows "|insert a A| =o |A|" |
|
1420 proof- |
|
1421 have iA: "insert a A = A \<union> {a}" by simp |
|
1422 show ?thesis |
|
1423 using infinite_imp_bij_betw2[OF assms] unfolding iA |
|
1424 by (metis bij_betw_inv card_of_ordIso) |
|
1425 qed |
|
1426 |
|
1427 |
|
1428 subsection {* Cardinals versus lists *} |
|
1429 |
|
1430 |
|
1431 text{* The next is an auxiliary operator, which shall be used for inductive |
|
1432 proofs of facts concerning the cardinality of @{text "List"} : *} |
|
1433 |
|
1434 definition nlists :: "'a set \<Rightarrow> nat \<Rightarrow> 'a list set" |
|
1435 where "nlists A n \<equiv> {l. set l \<le> A \<and> length l = n}" |
|
1436 |
|
1437 |
|
1438 lemma lists_def2: "lists A = {l. set l \<le> A}" |
|
1439 using in_listsI by blast |
|
1440 |
|
1441 |
|
1442 lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)" |
|
1443 unfolding lists_def2 nlists_def by blast |
|
1444 |
|
1445 |
|
1446 lemma card_of_lists: "|A| \<le>o |lists A|" |
|
1447 proof- |
|
1448 let ?h = "\<lambda> a. [a]" |
|
1449 have "inj_on ?h A \<and> ?h ` A \<le> lists A" |
|
1450 unfolding inj_on_def lists_def2 by auto |
|
1451 thus ?thesis by (metis card_of_ordLeq) |
|
1452 qed |
|
1453 |
|
1454 |
|
1455 lemma nlists_0: "nlists A 0 = {[]}" |
|
1456 unfolding nlists_def by auto |
|
1457 |
|
1458 |
|
1459 lemma nlists_not_empty: |
|
1460 assumes "A \<noteq> {}" |
|
1461 shows "nlists A n \<noteq> {}" |
|
1462 proof(induct n, simp add: nlists_0) |
|
1463 fix n assume "nlists A n \<noteq> {}" |
|
1464 then obtain a and l where "a \<in> A \<and> l \<in> nlists A n" using assms by auto |
|
1465 hence "a # l \<in> nlists A (Suc n)" unfolding nlists_def by auto |
|
1466 thus "nlists A (Suc n) \<noteq> {}" by auto |
|
1467 qed |
|
1468 |
|
1469 |
|
1470 lemma Nil_in_lists: "[] \<in> lists A" |
|
1471 unfolding lists_def2 by auto |
|
1472 |
|
1473 |
|
1474 lemma lists_not_empty: "lists A \<noteq> {}" |
|
1475 using Nil_in_lists by blast |
|
1476 |
|
1477 |
|
1478 lemma card_of_nlists_Succ: "|nlists A (Suc n)| =o |A \<times> (nlists A n)|" |
|
1479 proof- |
|
1480 let ?B = "A \<times> (nlists A n)" let ?h = "\<lambda>(a,l). a # l" |
|
1481 have "inj_on ?h ?B \<and> ?h ` ?B \<le> nlists A (Suc n)" |
|
1482 unfolding inj_on_def nlists_def by auto |
|
1483 moreover have "nlists A (Suc n) \<le> ?h ` ?B" |
|
1484 proof(auto) |
|
1485 fix l assume "l \<in> nlists A (Suc n)" |
|
1486 hence 1: "length l = Suc n \<and> set l \<le> A" unfolding nlists_def by auto |
|
1487 then obtain a and l' where 2: "l = a # l'" by (auto simp: length_Suc_conv) |
|
1488 hence "a \<in> A \<and> set l' \<le> A \<and> length l' = n" using 1 by auto |
|
1489 thus "l \<in> ?h ` ?B" using 2 unfolding nlists_def by auto |
|
1490 qed |
|
1491 ultimately have "bij_betw ?h ?B (nlists A (Suc n))" |
|
1492 unfolding bij_betw_def by auto |
|
1493 thus ?thesis using card_of_ordIso ordIso_symmetric by blast |
|
1494 qed |
|
1495 |
|
1496 |
|
1497 lemma card_of_nlists_infinite: |
|
1498 assumes "infinite A" |
|
1499 shows "|nlists A n| \<le>o |A|" |
|
1500 proof(induct n) |
|
1501 have "A \<noteq> {}" using assms by auto |
|
1502 thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq) |
|
1503 next |
|
1504 fix n assume IH: "|nlists A n| \<le>o |A|" |
|
1505 have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|" |
|
1506 using card_of_nlists_Succ by blast |
|
1507 moreover |
|
1508 {have "nlists A n \<noteq> {}" using assms nlists_not_empty[of A] by blast |
|
1509 hence "|A \<times> (nlists A n)| =o |A|" |
|
1510 using assms IH by (auto simp add: card_of_Times_infinite) |
|
1511 } |
|
1512 ultimately show "|nlists A (Suc n)| \<le>o |A|" |
|
1513 using ordIso_transitive ordIso_iff_ordLeq by blast |
|
1514 qed |
|
1515 |
|
1516 |
|
1517 lemma card_of_lists_infinite: |
|
1518 assumes "infinite A" |
|
1519 shows "|lists A| =o |A|" |
|
1520 proof- |
|
1521 have "|lists A| \<le>o |A|" |
|
1522 using assms |
|
1523 by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite |
|
1524 infinite_iff_card_of_nat card_of_nlists_infinite) |
|
1525 thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast |
|
1526 qed |
|
1527 |
|
1528 |
|
1529 lemma Card_order_lists_infinite: |
|
1530 assumes "Card_order r" and "infinite(Field r)" |
|
1531 shows "|lists(Field r)| =o r" |
|
1532 using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast |
|
1533 |
|
1534 |
|
1535 |
|
1536 subsection {* The cardinal $\omega$ and the finite cardinals *} |
|
1537 |
|
1538 |
|
1539 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict |
|
1540 order relation on |
|
1541 @{text "nat"}, that we abbreviate by @{text "natLeq"}. The finite cardinals |
|
1542 shall be the restrictions of these relations to the numbers smaller than |
|
1543 fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *} |
|
1544 |
|
1545 abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}" |
|
1546 abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}" |
|
1547 |
|
1548 abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set" |
|
1549 where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}" |
|
1550 |
|
1551 lemma infinite_cartesian_product: |
|
1552 assumes "infinite A" "infinite B" |
|
1553 shows "infinite (A \<times> B)" |
|
1554 proof |
|
1555 assume "finite (A \<times> B)" |
|
1556 from assms(1) have "A \<noteq> {}" by auto |
|
1557 with `finite (A \<times> B)` have "finite B" using finite_cartesian_productD2 by auto |
|
1558 with assms(2) show False by simp |
|
1559 qed |
|
1560 |
|
1561 |
|
1562 |
|
1563 subsubsection {* First as well-orders *} |
|
1564 |
|
1565 |
|
1566 lemma Field_natLeq: "Field natLeq = (UNIV::nat set)" |
|
1567 by(unfold Field_def, auto) |
|
1568 |
|
1569 |
|
1570 lemma natLeq_Refl: "Refl natLeq" |
|
1571 unfolding refl_on_def Field_def by auto |
|
1572 |
|
1573 |
|
1574 lemma natLeq_trans: "trans natLeq" |
|
1575 unfolding trans_def by auto |
|
1576 |
|
1577 |
|
1578 lemma natLeq_Preorder: "Preorder natLeq" |
|
1579 unfolding preorder_on_def |
|
1580 by (auto simp add: natLeq_Refl natLeq_trans) |
|
1581 |
|
1582 |
|
1583 lemma natLeq_antisym: "antisym natLeq" |
|
1584 unfolding antisym_def by auto |
|
1585 |
|
1586 |
|
1587 lemma natLeq_Partial_order: "Partial_order natLeq" |
|
1588 unfolding partial_order_on_def |
|
1589 by (auto simp add: natLeq_Preorder natLeq_antisym) |
|
1590 |
|
1591 |
|
1592 lemma natLeq_Total: "Total natLeq" |
|
1593 unfolding total_on_def by auto |
|
1594 |
|
1595 |
|
1596 lemma natLeq_Linear_order: "Linear_order natLeq" |
|
1597 unfolding linear_order_on_def |
|
1598 by (auto simp add: natLeq_Partial_order natLeq_Total) |
|
1599 |
|
1600 |
|
1601 lemma natLeq_natLess_Id: "natLess = natLeq - Id" |
|
1602 by auto |
|
1603 |
|
1604 |
|
1605 lemma natLeq_Well_order: "Well_order natLeq" |
|
1606 unfolding well_order_on_def |
|
1607 using natLeq_Linear_order wf_less natLeq_natLess_Id by auto |
|
1608 |
|
1609 |
|
1610 corollary natLeq_well_order_on: "well_order_on UNIV natLeq" |
|
1611 using natLeq_Well_order Field_natLeq by auto |
|
1612 |
|
1613 |
|
1614 lemma natLeq_wo_rel: "wo_rel natLeq" |
|
1615 unfolding wo_rel_def using natLeq_Well_order . |
|
1616 |
|
1617 |
|
1618 lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV" |
|
1619 using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto |
|
1620 |
|
1621 |
|
1622 lemma closed_nat_set_iff: |
|
1623 assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" |
|
1624 shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" |
|
1625 proof- |
|
1626 {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast |
|
1627 moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast |
|
1628 ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)" |
|
1629 using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce |
|
1630 have "A = {0 ..< n}" |
|
1631 proof(auto simp add: 1) |
|
1632 fix m assume *: "m \<in> A" |
|
1633 {assume "n \<le> m" with assms * have "n \<in> A" by blast |
|
1634 hence False using 1 by auto |
|
1635 } |
|
1636 thus "m < n" by fastforce |
|
1637 qed |
|
1638 hence "\<exists>n. A = {0 ..< n}" by blast |
|
1639 } |
|
1640 thus ?thesis by blast |
|
1641 qed |
|
1642 |
|
1643 |
|
1644 lemma Field_natLeq_on: "Field (natLeq_on n) = {0 ..< n}" |
|
1645 unfolding Field_def by auto |
|
1646 |
|
1647 |
|
1648 lemma natLeq_underS_less: "rel.underS natLeq n = {0 ..< n}" |
|
1649 unfolding rel.underS_def by auto |
|
1650 |
|
1651 |
|
1652 lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n" |
|
1653 by auto |
|
1654 |
|
1655 |
|
1656 lemma Restr_natLeq2: |
|
1657 "Restr natLeq (rel.underS natLeq n) = natLeq_on n" |
|
1658 by (auto simp add: Restr_natLeq natLeq_underS_less) |
|
1659 |
|
1660 |
|
1661 lemma natLeq_on_Well_order: "Well_order(natLeq_on n)" |
|
1662 using Restr_natLeq[of n] natLeq_Well_order |
|
1663 Well_order_Restr[of natLeq "{0..<n}"] by auto |
|
1664 |
|
1665 |
|
1666 corollary natLeq_on_well_order_on: "well_order_on {0 ..< n} (natLeq_on n)" |
|
1667 using natLeq_on_Well_order Field_natLeq_on by auto |
|
1668 |
|
1669 |
|
1670 lemma natLeq_on_wo_rel: "wo_rel(natLeq_on n)" |
|
1671 unfolding wo_rel_def using natLeq_on_Well_order . |
|
1672 |
|
1673 |
|
1674 lemma natLeq_on_ofilter_less_eq: |
|
1675 "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}" |
|
1676 by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def, |
|
1677 simp add: Field_natLeq_on, unfold rel.under_def, auto) |
|
1678 |
|
1679 |
|
1680 lemma natLeq_on_ofilter_iff: |
|
1681 "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})" |
|
1682 proof(rule iffI) |
|
1683 assume *: "wo_rel.ofilter (natLeq_on m) A" |
|
1684 hence 1: "A \<le> {0..<m}" |
|
1685 by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on) |
|
1686 hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A" |
|
1687 using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def) |
|
1688 hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast |
|
1689 thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast |
|
1690 next |
|
1691 assume "(\<exists>n\<le>m. A = {0 ..< n})" |
|
1692 thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq) |
|
1693 qed |
|
1694 |
|
1695 |
|
1696 |
|
1697 subsubsection {* Then as cardinals *} |
|
1698 |
|
1699 |
|
1700 lemma natLeq_Card_order: "Card_order natLeq" |
|
1701 proof(auto simp add: natLeq_Well_order |
|
1702 Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq) |
|
1703 fix n have "finite(Field (natLeq_on n))" |
|
1704 unfolding Field_natLeq_on by auto |
|
1705 moreover have "infinite(UNIV::nat set)" by auto |
|
1706 ultimately show "natLeq_on n <o |UNIV::nat set|" |
|
1707 using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"] |
|
1708 Field_card_of[of "UNIV::nat set"] |
|
1709 card_of_Well_order[of "UNIV::nat set"] natLeq_on_Well_order[of n] by auto |
|
1710 qed |
|
1711 |
|
1712 |
|
1713 corollary card_of_Field_natLeq: |
|
1714 "|Field natLeq| =o natLeq" |
|
1715 using Field_natLeq natLeq_Card_order Card_order_iff_ordIso_card_of[of natLeq] |
|
1716 ordIso_symmetric[of natLeq] by blast |
|
1717 |
|
1718 |
|
1719 corollary card_of_nat: |
|
1720 "|UNIV::nat set| =o natLeq" |
|
1721 using Field_natLeq card_of_Field_natLeq by auto |
|
1722 |
|
1723 |
|
1724 corollary infinite_iff_natLeq_ordLeq: |
|
1725 "infinite A = ( natLeq \<le>o |A| )" |
|
1726 using infinite_iff_card_of_nat[of A] card_of_nat |
|
1727 ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast |
|
1728 |
|
1729 |
|
1730 corollary finite_iff_ordLess_natLeq: |
|
1731 "finite A = ( |A| <o natLeq)" |
|
1732 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess |
|
1733 card_of_Well_order natLeq_Well_order by blast |
|
1734 |
|
1735 |
|
1736 lemma ordIso_natLeq_on_imp_finite: |
|
1737 "|A| =o natLeq_on n \<Longrightarrow> finite A" |
|
1738 unfolding ordIso_def iso_def[abs_def] |
|
1739 by (auto simp: Field_natLeq_on bij_betw_finite Field_card_of) |
|
1740 |
|
1741 |
|
1742 lemma natLeq_on_Card_order: "Card_order (natLeq_on n)" |
|
1743 proof(unfold card_order_on_def, |
|
1744 auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on) |
|
1745 fix r assume "well_order_on {0..<n} r" |
|
1746 thus "natLeq_on n \<le>o r" |
|
1747 using finite_atLeastLessThan natLeq_on_well_order_on |
|
1748 finite_well_order_on_ordIso ordIso_iff_ordLeq by blast |
|
1749 qed |
|
1750 |
|
1751 |
|
1752 corollary card_of_Field_natLeq_on: |
|
1753 "|Field (natLeq_on n)| =o natLeq_on n" |
|
1754 using Field_natLeq_on natLeq_on_Card_order |
|
1755 Card_order_iff_ordIso_card_of[of "natLeq_on n"] |
|
1756 ordIso_symmetric[of "natLeq_on n"] by blast |
|
1757 |
|
1758 |
|
1759 corollary card_of_less: |
|
1760 "|{0 ..< n}| =o natLeq_on n" |
|
1761 using Field_natLeq_on card_of_Field_natLeq_on by auto |
|
1762 |
|
1763 |
|
1764 lemma natLeq_on_ordLeq_less_eq: |
|
1765 "((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)" |
|
1766 proof |
|
1767 assume "natLeq_on m \<le>o natLeq_on n" |
|
1768 then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}" |
|
1769 unfolding ordLeq_def using |
|
1770 embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] |
|
1771 embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast |
|
1772 thus "m \<le> n" using atLeastLessThan_less_eq2 by blast |
|
1773 next |
|
1774 assume "m \<le> n" |
|
1775 hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto |
|
1776 hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast |
|
1777 thus "natLeq_on m \<le>o natLeq_on n" |
|
1778 using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast |
|
1779 qed |
|
1780 |
|
1781 |
|
1782 lemma natLeq_on_ordLeq_less: |
|
1783 "((natLeq_on m) <o (natLeq_on n)) = (m < n)" |
|
1784 using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"] |
|
1785 natLeq_on_Well_order natLeq_on_ordLeq_less_eq by auto |
|
1786 |
|
1787 |
|
1788 |
|
1789 subsubsection {* "Backwards compatibility" with the numeric cardinal operator for finite sets *} |
|
1790 |
|
1791 |
|
1792 lemma finite_card_of_iff_card2: |
|
1793 assumes FIN: "finite A" and FIN': "finite B" |
|
1794 shows "( |A| \<le>o |B| ) = (card A \<le> card B)" |
|
1795 using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast |
|
1796 |
|
1797 |
|
1798 lemma finite_imp_card_of_natLeq_on: |
|
1799 assumes "finite A" |
|
1800 shows "|A| =o natLeq_on (card A)" |
|
1801 proof- |
|
1802 obtain h where "bij_betw h A {0 ..< card A}" |
|
1803 using assms ex_bij_betw_finite_nat by blast |
|
1804 thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast |
|
1805 qed |
|
1806 |
|
1807 |
|
1808 lemma finite_iff_card_of_natLeq_on: |
|
1809 "finite A = (\<exists>n. |A| =o natLeq_on n)" |
|
1810 using finite_imp_card_of_natLeq_on[of A] |
|
1811 by(auto simp add: ordIso_natLeq_on_imp_finite) |
|
1812 |
|
1813 |
|
1814 |
|
1815 subsection {* The successor of a cardinal *} |
|
1816 |
|
1817 |
|
1818 text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"} |
|
1819 being a successor cardinal of @{text "r"}. Although the definition does |
|
1820 not require @{text "r"} to be a cardinal, only this case will be meaningful. *} |
|
1821 |
|
1822 |
|
1823 definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool" |
|
1824 where |
|
1825 "isCardSuc r r' \<equiv> |
|
1826 Card_order r' \<and> r <o r' \<and> |
|
1827 (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')" |
|
1828 |
|
1829 |
|
1830 text{* Now we introduce the cardinal-successor operator @{text "cardSuc"}, |
|
1831 by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}. |
|
1832 Again, the picked item shall be proved unique up to order-isomorphism. *} |
|
1833 |
|
1834 |
|
1835 definition cardSuc :: "'a rel \<Rightarrow> 'a set rel" |
|
1836 where |
|
1837 "cardSuc r \<equiv> SOME r'. isCardSuc r r'" |
|
1838 |
|
1839 |
|
1840 lemma exists_minim_Card_order: |
|
1841 "\<lbrakk>R \<noteq> {}; \<forall>r \<in> R. Card_order r\<rbrakk> \<Longrightarrow> \<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'" |
|
1842 unfolding card_order_on_def using exists_minim_Well_order by blast |
|
1843 |
|
1844 |
|
1845 lemma exists_isCardSuc: |
|
1846 assumes "Card_order r" |
|
1847 shows "\<exists>r'. isCardSuc r r'" |
|
1848 proof- |
|
1849 let ?R = "{(r'::'a set rel). Card_order r' \<and> r <o r'}" |
|
1850 have "|Pow(Field r)| \<in> ?R \<and> (\<forall>r \<in> ?R. Card_order r)" using assms |
|
1851 by (simp add: card_of_Card_order Card_order_Pow) |
|
1852 then obtain r where "r \<in> ?R \<and> (\<forall>r' \<in> ?R. r \<le>o r')" |
|
1853 using exists_minim_Card_order[of ?R] by blast |
|
1854 thus ?thesis unfolding isCardSuc_def by auto |
|
1855 qed |
|
1856 |
|
1857 |
|
1858 lemma cardSuc_isCardSuc: |
|
1859 assumes "Card_order r" |
|
1860 shows "isCardSuc r (cardSuc r)" |
|
1861 unfolding cardSuc_def using assms |
|
1862 by (simp add: exists_isCardSuc someI_ex) |
|
1863 |
|
1864 |
|
1865 lemma cardSuc_Card_order: |
|
1866 "Card_order r \<Longrightarrow> Card_order(cardSuc r)" |
|
1867 using cardSuc_isCardSuc unfolding isCardSuc_def by blast |
|
1868 |
|
1869 |
|
1870 lemma cardSuc_greater: |
|
1871 "Card_order r \<Longrightarrow> r <o cardSuc r" |
|
1872 using cardSuc_isCardSuc unfolding isCardSuc_def by blast |
|
1873 |
|
1874 |
|
1875 lemma cardSuc_ordLeq: |
|
1876 "Card_order r \<Longrightarrow> r \<le>o cardSuc r" |
|
1877 using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast |
|
1878 |
|
1879 |
|
1880 text{* The minimality property of @{text "cardSuc"} originally present in its definition |
|
1881 is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *} |
|
1882 |
|
1883 lemma cardSuc_least_aux: |
|
1884 "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'" |
|
1885 using cardSuc_isCardSuc unfolding isCardSuc_def by blast |
|
1886 |
|
1887 |
|
1888 text{* But from this we can infer general minimality: *} |
|
1889 |
|
1890 lemma cardSuc_least: |
|
1891 assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'" |
|
1892 shows "cardSuc r \<le>o r'" |
|
1893 proof- |
|
1894 let ?p = "cardSuc r" |
|
1895 have 0: "Well_order ?p \<and> Well_order r'" |
|
1896 using assms cardSuc_Card_order unfolding card_order_on_def by blast |
|
1897 {assume "r' <o ?p" |
|
1898 then obtain r'' where 1: "Field r'' < Field ?p" and 2: "r' =o r'' \<and> r'' <o ?p" |
|
1899 using internalize_ordLess[of r' ?p] by blast |
|
1900 (* *) |
|
1901 have "Card_order r''" using CARD' Card_order_ordIso2 2 by blast |
|
1902 moreover have "r <o r''" using LESS 2 ordLess_ordIso_trans by blast |
|
1903 ultimately have "?p \<le>o r''" using cardSuc_least_aux CARD by blast |
|
1904 hence False using 2 not_ordLess_ordLeq by blast |
|
1905 } |
|
1906 thus ?thesis using 0 ordLess_or_ordLeq by blast |
|
1907 qed |
|
1908 |
|
1909 |
|
1910 lemma cardSuc_ordLess_ordLeq: |
|
1911 assumes CARD: "Card_order r" and CARD': "Card_order r'" |
|
1912 shows "(r <o r') = (cardSuc r \<le>o r')" |
|
1913 proof(auto simp add: assms cardSuc_least) |
|
1914 assume "cardSuc r \<le>o r'" |
|
1915 thus "r <o r'" using assms cardSuc_greater ordLess_ordLeq_trans by blast |
|
1916 qed |
|
1917 |
|
1918 |
|
1919 lemma cardSuc_ordLeq_ordLess: |
|
1920 assumes CARD: "Card_order r" and CARD': "Card_order r'" |
|
1921 shows "(r' <o cardSuc r) = (r' \<le>o r)" |
|
1922 proof- |
|
1923 have "Well_order r \<and> Well_order r'" |
|
1924 using assms unfolding card_order_on_def by auto |
|
1925 moreover have "Well_order(cardSuc r)" |
|
1926 using assms cardSuc_Card_order card_order_on_def by blast |
|
1927 ultimately show ?thesis |
|
1928 using assms cardSuc_ordLess_ordLeq[of r r'] |
|
1929 not_ordLeq_iff_ordLess[of r r'] not_ordLeq_iff_ordLess[of r' "cardSuc r"] by blast |
|
1930 qed |
|
1931 |
|
1932 |
|
1933 lemma cardSuc_mono_ordLeq: |
|
1934 assumes CARD: "Card_order r" and CARD': "Card_order r'" |
|
1935 shows "(cardSuc r \<le>o cardSuc r') = (r \<le>o r')" |
|
1936 using assms cardSuc_ordLeq_ordLess cardSuc_ordLess_ordLeq cardSuc_Card_order by blast |
|
1937 |
|
1938 |
|
1939 lemma cardSuc_invar_ordIso: |
|
1940 assumes CARD: "Card_order r" and CARD': "Card_order r'" |
|
1941 shows "(cardSuc r =o cardSuc r') = (r =o r')" |
|
1942 proof- |
|
1943 have 0: "Well_order r \<and> Well_order r' \<and> Well_order(cardSuc r) \<and> Well_order(cardSuc r')" |
|
1944 using assms by (simp add: card_order_on_well_order_on cardSuc_Card_order) |
|
1945 thus ?thesis |
|
1946 using ordIso_iff_ordLeq[of r r'] ordIso_iff_ordLeq |
|
1947 using cardSuc_mono_ordLeq[of r r'] cardSuc_mono_ordLeq[of r' r] assms by blast |
|
1948 qed |
|
1949 |
|
1950 |
|
1951 lemma cardSuc_natLeq_on_Suc: |
|
1952 "cardSuc(natLeq_on n) =o natLeq_on(Suc n)" |
|
1953 proof- |
|
1954 obtain r r' p where r_def: "r = natLeq_on n" and |
|
1955 r'_def: "r' = cardSuc(natLeq_on n)" and |
|
1956 p_def: "p = natLeq_on(Suc n)" by blast |
|
1957 (* Preliminary facts: *) |
|
1958 have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def |
|
1959 using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast |
|
1960 hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p" |
|
1961 unfolding card_order_on_def by force |
|
1962 have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}" |
|
1963 unfolding r_def p_def Field_natLeq_on by simp |
|
1964 hence FIN: "finite (Field r)" by force |
|
1965 have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast |
|
1966 hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast |
|
1967 hence LESS: "|Field r| <o |Field r'|" |
|
1968 using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast |
|
1969 (* Main proof: *) |
|
1970 have "r' \<le>o p" using CARD unfolding r_def r'_def p_def |
|
1971 using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast |
|
1972 moreover have "p \<le>o r'" |
|
1973 proof- |
|
1974 {assume "r' <o p" |
|
1975 then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force |
|
1976 let ?q = "Restr p (f ` Field r')" |
|
1977 have 1: "embed r' p f" using 0 unfolding embedS_def by force |
|
1978 hence 2: "f ` Field r' < {0..<(Suc n)}" |
|
1979 using WELL FIELD 0 by (auto simp add: embedS_iff) |
|
1980 have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast |
|
1981 then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}" |
|
1982 unfolding p_def by (auto simp add: natLeq_on_ofilter_iff) |
|
1983 hence 4: "m \<le> n" using 2 by force |
|
1984 (* *) |
|
1985 have "bij_betw f (Field r') (f ` (Field r'))" |
|
1986 using 1 WELL embed_inj_on unfolding bij_betw_def by force |
|
1987 moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force |
|
1988 ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))" |
|
1989 using bij_betw_same_card bij_betw_finite by metis |
|
1990 hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force |
|
1991 hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast |
|
1992 hence False using LESS not_ordLess_ordLeq by auto |
|
1993 } |
|
1994 thus ?thesis using WELL CARD by (fastforce simp: not_ordLess_iff_ordLeq) |
|
1995 qed |
|
1996 ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast |
|
1997 qed |
|
1998 |
|
1999 |
|
2000 lemma card_of_cardSuc_finite: |
|
2001 "finite(Field(cardSuc |A| )) = finite A" |
|
2002 proof |
|
2003 assume *: "finite (Field (cardSuc |A| ))" |
|
2004 have 0: "|Field(cardSuc |A| )| =o cardSuc |A|" |
|
2005 using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast |
|
2006 hence "|A| \<le>o |Field(cardSuc |A| )|" |
|
2007 using card_of_Card_order[of A] cardSuc_ordLeq[of "|A|"] ordIso_symmetric |
|
2008 ordLeq_ordIso_trans by blast |
|
2009 thus "finite A" using * card_of_ordLeq_finite by blast |
|
2010 next |
|
2011 assume "finite A" |
|
2012 then obtain n where "|A| =o natLeq_on n" using finite_iff_card_of_natLeq_on by blast |
|
2013 hence "cardSuc |A| =o cardSuc(natLeq_on n)" |
|
2014 using card_of_Card_order cardSuc_invar_ordIso natLeq_on_Card_order by blast |
|
2015 hence "cardSuc |A| =o natLeq_on(Suc n)" |
|
2016 using cardSuc_natLeq_on_Suc ordIso_transitive by blast |
|
2017 hence "cardSuc |A| =o |{0..<(Suc n)}|" using card_of_less ordIso_equivalence by blast |
|
2018 moreover have "|Field (cardSuc |A| ) | =o cardSuc |A|" |
|
2019 using card_of_Field_ordIso cardSuc_Card_order card_of_Card_order by blast |
|
2020 ultimately have "|Field (cardSuc |A| ) | =o |{0..<(Suc n)}|" |
|
2021 using ordIso_equivalence by blast |
|
2022 thus "finite (Field (cardSuc |A| ))" |
|
2023 using card_of_ordIso_finite finite_atLeastLessThan by blast |
|
2024 qed |
|
2025 |
|
2026 |
|
2027 lemma cardSuc_finite: |
|
2028 assumes "Card_order r" |
|
2029 shows "finite (Field (cardSuc r)) = finite (Field r)" |
|
2030 proof- |
|
2031 let ?A = "Field r" |
|
2032 have "|?A| =o r" using assms by (simp add: card_of_Field_ordIso) |
|
2033 hence "cardSuc |?A| =o cardSuc r" using assms |
|
2034 by (simp add: card_of_Card_order cardSuc_invar_ordIso) |
|
2035 moreover have "|Field (cardSuc |?A| ) | =o cardSuc |?A|" |
|
2036 by (simp add: card_of_card_order_on Field_card_of card_of_Field_ordIso cardSuc_Card_order) |
|
2037 moreover |
|
2038 {have "|Field (cardSuc r) | =o cardSuc r" |
|
2039 using assms by (simp add: card_of_Field_ordIso cardSuc_Card_order) |
|
2040 hence "cardSuc r =o |Field (cardSuc r) |" |
|
2041 using ordIso_symmetric by blast |
|
2042 } |
|
2043 ultimately have "|Field (cardSuc |?A| ) | =o |Field (cardSuc r) |" |
|
2044 using ordIso_transitive by blast |
|
2045 hence "finite (Field (cardSuc |?A| )) = finite (Field (cardSuc r))" |
|
2046 using card_of_ordIso_finite by blast |
|
2047 thus ?thesis by (simp only: card_of_cardSuc_finite) |
|
2048 qed |
|
2049 |
|
2050 |
|
2051 lemma card_of_Plus_ordLeq_infinite_Field: |
|
2052 assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" |
|
2053 and c: "Card_order r" |
|
2054 shows "|A <+> B| \<le>o r" |
|
2055 proof- |
|
2056 let ?r' = "cardSuc r" |
|
2057 have "Card_order ?r' \<and> infinite (Field ?r')" using assms |
|
2058 by (simp add: cardSuc_Card_order cardSuc_finite) |
|
2059 moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c |
|
2060 by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess) |
|
2061 ultimately have "|A <+> B| <o ?r'" |
|
2062 using card_of_Plus_ordLess_infinite_Field by blast |
|
2063 thus ?thesis using c r |
|
2064 by (simp add: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess) |
|
2065 qed |
|
2066 |
|
2067 |
|
2068 lemma card_of_Un_ordLeq_infinite_Field: |
|
2069 assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r" |
|
2070 and "Card_order r" |
|
2071 shows "|A Un B| \<le>o r" |
|
2072 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq |
|
2073 ordLeq_transitive by blast |
|
2074 |
|
2075 |
|
2076 |
|
2077 subsection {* Regular cardinals *} |
|
2078 |
|
2079 |
|
2080 definition cofinal where |
|
2081 "cofinal A r \<equiv> |
|
2082 ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r" |
|
2083 |
|
2084 |
|
2085 definition regular where |
|
2086 "regular r \<equiv> |
|
2087 ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r" |
|
2088 |
|
2089 |
|
2090 definition relChain where |
|
2091 "relChain r As \<equiv> |
|
2092 ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j" |
|
2093 |
|
2094 lemma regular_UNION: |
|
2095 assumes r: "Card_order r" "regular r" |
|
2096 and As: "relChain r As" |
|
2097 and Bsub: "B \<le> (UN i : Field r. As i)" |
|
2098 and cardB: "|B| <o r" |
|
2099 shows "EX i : Field r. B \<le> As i" |
|
2100 proof- |
|
2101 let ?phi = "%b j. j : Field r \<and> b : As j" |
|
2102 have "ALL b : B. EX j. ?phi b j" using Bsub by blast |
|
2103 then obtain f where f: "!! b. b : B \<Longrightarrow> ?phi b (f b)" |
|
2104 using bchoice[of B ?phi] by blast |
|
2105 let ?K = "f ` B" |
|
2106 {assume 1: "!! i. i : Field r \<Longrightarrow> ~ B \<le> As i" |
|
2107 have 2: "cofinal ?K r" |
|
2108 unfolding cofinal_def proof auto |
|
2109 fix i assume i: "i : Field r" |
|
2110 with 1 obtain b where b: "b : B \<and> b \<notin> As i" by blast |
|
2111 hence "i \<noteq> f b \<and> ~ (f b,i) : r" |
|
2112 using As f unfolding relChain_def by auto |
|
2113 hence "i \<noteq> f b \<and> (i, f b) : r" using r |
|
2114 unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
2115 total_on_def using i f b by auto |
|
2116 with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast |
|
2117 qed |
|
2118 moreover have "?K \<le> Field r" using f by blast |
|
2119 ultimately have "|?K| =o r" using 2 r unfolding regular_def by blast |
|
2120 moreover |
|
2121 { |
|
2122 have "|?K| <=o |B|" using card_of_image . |
|
2123 hence "|?K| <o r" using cardB ordLeq_ordLess_trans by blast |
|
2124 } |
|
2125 ultimately have False using not_ordLess_ordIso by blast |
|
2126 } |
|
2127 thus ?thesis by blast |
|
2128 qed |
|
2129 |
|
2130 |
|
2131 lemma infinite_cardSuc_regular: |
|
2132 assumes r_inf: "infinite (Field r)" and r_card: "Card_order r" |
|
2133 shows "regular (cardSuc r)" |
|
2134 proof- |
|
2135 let ?r' = "cardSuc r" |
|
2136 have r': "Card_order ?r'" |
|
2137 "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')" |
|
2138 using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess) |
|
2139 show ?thesis |
|
2140 unfolding regular_def proof auto |
|
2141 fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'" |
|
2142 hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1) |
|
2143 also have 22: "|Field ?r'| =o ?r'" |
|
2144 using r' by (simp add: card_of_Field_ordIso[of ?r']) |
|
2145 finally have "|K| \<le>o ?r'" . |
|
2146 moreover |
|
2147 {let ?L = "UN j : K. rel.underS ?r' j" |
|
2148 let ?J = "Field r" |
|
2149 have rJ: "r =o |?J|" |
|
2150 using r_card card_of_Field_ordIso ordIso_symmetric by blast |
|
2151 assume "|K| <o ?r'" |
|
2152 hence "|K| <=o r" using r' card_of_Card_order[of K] by blast |
|
2153 hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast |
|
2154 moreover |
|
2155 {have "ALL j : K. |rel.underS ?r' j| <o ?r'" |
|
2156 using r' 1 by (auto simp: card_of_underS) |
|
2157 hence "ALL j : K. |rel.underS ?r' j| \<le>o r" |
|
2158 using r' card_of_Card_order by blast |
|
2159 hence "ALL j : K. |rel.underS ?r' j| \<le>o |?J|" |
|
2160 using rJ ordLeq_ordIso_trans by blast |
|
2161 } |
|
2162 ultimately have "|?L| \<le>o |?J|" |
|
2163 using r_inf card_of_UNION_ordLeq_infinite by blast |
|
2164 hence "|?L| \<le>o r" using rJ ordIso_symmetric ordLeq_ordIso_trans by blast |
|
2165 hence "|?L| <o ?r'" using r' card_of_Card_order by blast |
|
2166 moreover |
|
2167 { |
|
2168 have "Field ?r' \<le> ?L" |
|
2169 using 2 unfolding rel.underS_def cofinal_def by auto |
|
2170 hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1) |
|
2171 hence "?r' \<le>o |?L|" |
|
2172 using 22 ordIso_ordLeq_trans ordIso_symmetric by blast |
|
2173 } |
|
2174 ultimately have "|?L| <o |?L|" using ordLess_ordLeq_trans by blast |
|
2175 hence False using ordLess_irreflexive by blast |
|
2176 } |
|
2177 ultimately show "|K| =o ?r'" |
|
2178 unfolding ordLeq_iff_ordLess_or_ordIso by blast |
|
2179 qed |
|
2180 qed |
|
2181 |
|
2182 lemma cardSuc_UNION: |
|
2183 assumes r: "Card_order r" and "infinite (Field r)" |
|
2184 and As: "relChain (cardSuc r) As" |
|
2185 and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)" |
|
2186 and cardB: "|B| <=o r" |
|
2187 shows "EX i : Field (cardSuc r). B \<le> As i" |
|
2188 proof- |
|
2189 let ?r' = "cardSuc r" |
|
2190 have "Card_order ?r' \<and> |B| <o ?r'" |
|
2191 using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order |
|
2192 card_of_Card_order by blast |
|
2193 moreover have "regular ?r'" |
|
2194 using assms by(simp add: infinite_cardSuc_regular) |
|
2195 ultimately show ?thesis |
|
2196 using As Bsub cardB regular_UNION by blast |
|
2197 qed |
|
2198 |
|
2199 |
|
2200 subsection {* Others *} |
|
2201 |
|
2202 lemma card_of_infinite_diff_finite: |
|
2203 assumes "infinite A" and "finite B" |
|
2204 shows "|A - B| =o |A|" |
|
2205 by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2) |
|
2206 |
|
2207 (* function space *) |
|
2208 definition Func where |
|
2209 "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}" |
|
2210 |
|
2211 lemma Func_empty: |
|
2212 "Func {} B = {\<lambda>x. undefined}" |
|
2213 unfolding Func_def by auto |
|
2214 |
|
2215 lemma Func_elim: |
|
2216 assumes "g \<in> Func A B" and "a \<in> A" |
|
2217 shows "\<exists> b. b \<in> B \<and> g a = b" |
|
2218 using assms unfolding Func_def by (cases "g a = undefined") auto |
|
2219 |
|
2220 definition curr where |
|
2221 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined" |
|
2222 |
|
2223 lemma curr_in: |
|
2224 assumes f: "f \<in> Func (A <*> B) C" |
|
2225 shows "curr A f \<in> Func A (Func B C)" |
|
2226 using assms unfolding curr_def Func_def by auto |
|
2227 |
|
2228 lemma curr_inj: |
|
2229 assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C" |
|
2230 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2" |
|
2231 proof safe |
|
2232 assume c: "curr A f1 = curr A f2" |
|
2233 show "f1 = f2" |
|
2234 proof (rule ext, clarify) |
|
2235 fix a b show "f1 (a, b) = f2 (a, b)" |
|
2236 proof (cases "(a,b) \<in> A <*> B") |
|
2237 case False |
|
2238 thus ?thesis using assms unfolding Func_def by auto |
|
2239 next |
|
2240 case True hence a: "a \<in> A" and b: "b \<in> B" by auto |
|
2241 thus ?thesis |
|
2242 using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp |
|
2243 qed |
|
2244 qed |
|
2245 qed |
|
2246 |
|
2247 lemma curr_surj: |
|
2248 assumes "g \<in> Func A (Func B C)" |
|
2249 shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g" |
|
2250 proof |
|
2251 let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined" |
|
2252 show "curr A ?f = g" |
|
2253 proof (rule ext) |
|
2254 fix a show "curr A ?f a = g a" |
|
2255 proof (cases "a \<in> A") |
|
2256 case False |
|
2257 hence "g a = undefined" using assms unfolding Func_def by auto |
|
2258 thus ?thesis unfolding curr_def using False by simp |
|
2259 next |
|
2260 case True |
|
2261 obtain g1 where "g1 \<in> Func B C" and "g a = g1" |
|
2262 using assms using Func_elim[OF assms True] by blast |
|
2263 thus ?thesis using True unfolding Func_def curr_def by auto |
|
2264 qed |
|
2265 qed |
|
2266 show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto |
|
2267 qed |
|
2268 |
|
2269 lemma bij_betw_curr: |
|
2270 "bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))" |
|
2271 unfolding bij_betw_def inj_on_def image_def |
|
2272 using curr_in curr_inj curr_surj by blast |
|
2273 |
|
2274 lemma card_of_Func_Times: |
|
2275 "|Func (A <*> B) C| =o |Func A (Func B C)|" |
|
2276 unfolding card_of_ordIso[symmetric] |
|
2277 using bij_betw_curr by blast |
|
2278 |
|
2279 definition Func_map where |
|
2280 "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined" |
|
2281 |
|
2282 lemma Func_map: |
|
2283 assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2" |
|
2284 shows "Func_map B2 f1 f2 g \<in> Func B2 B1" |
|
2285 using assms unfolding Func_def Func_map_def mem_Collect_eq by auto |
|
2286 |
|
2287 lemma Func_non_emp: |
|
2288 assumes "B \<noteq> {}" |
|
2289 shows "Func A B \<noteq> {}" |
|
2290 proof- |
|
2291 obtain b where b: "b \<in> B" using assms by auto |
|
2292 hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto |
|
2293 thus ?thesis by blast |
|
2294 qed |
|
2295 |
|
2296 lemma Func_is_emp: |
|
2297 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") |
|
2298 proof |
|
2299 assume L: ?L |
|
2300 moreover {assume "A = {}" hence False using L Func_empty by auto} |
|
2301 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis} |
|
2302 ultimately show ?R by blast |
|
2303 next |
|
2304 assume R: ?R |
|
2305 moreover |
|
2306 {fix f assume "f \<in> Func A B" |
|
2307 moreover obtain a where "a \<in> A" using R by blast |
|
2308 ultimately obtain b where "b \<in> B" unfolding Func_def by(cases "f a = undefined", force+) |
|
2309 with R have False by auto |
|
2310 } |
|
2311 thus ?L by blast |
|
2312 qed |
|
2313 |
|
2314 lemma Func_map_surj: |
|
2315 assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2" |
|
2316 and B2A2: "B2 = {} \<Longrightarrow> A2 = {}" |
|
2317 shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" |
|
2318 proof(cases "B2 = {}") |
|
2319 case True |
|
2320 thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) |
|
2321 next |
|
2322 case False note B2 = False |
|
2323 show ?thesis |
|
2324 proof safe |
|
2325 fix h assume h: "h \<in> Func B2 B1" |
|
2326 def j1 \<equiv> "inv_into A1 f1" |
|
2327 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast |
|
2328 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis |
|
2329 {fix b2 assume b2: "b2 \<in> B2" |
|
2330 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto |
|
2331 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto |
|
2332 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast |
|
2333 } note kk = this |
|
2334 obtain b22 where b22: "b22 \<in> B2" using B2 by auto |
|
2335 def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22" |
|
2336 have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto |
|
2337 have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2" |
|
2338 using kk unfolding j2_def by auto |
|
2339 def g \<equiv> "Func_map A2 j1 j2 h" |
|
2340 have "Func_map B2 f1 f2 g = h" |
|
2341 proof (rule ext) |
|
2342 fix b2 show "Func_map B2 f1 f2 g b2 = h b2" |
|
2343 proof(cases "b2 \<in> B2") |
|
2344 case True |
|
2345 show ?thesis |
|
2346 proof (cases "h b2 = undefined") |
|
2347 case True |
|
2348 hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto |
|
2349 show ?thesis using A2 f_inv_into_f[OF b1] |
|
2350 unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto |
|
2351 qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, |
|
2352 auto intro: f_inv_into_f) |
|
2353 qed(insert h, unfold Func_def Func_map_def, auto) |
|
2354 qed |
|
2355 moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) |
|
2356 using inv_into_into j2A2 B1 A2 inv_into_into |
|
2357 unfolding j1_def image_def by fast+ |
|
2358 ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1" |
|
2359 unfolding Func_map_def[abs_def] unfolding image_def by auto |
|
2360 qed(insert B1 Func_map[OF _ _ A2(2)], auto) |
|
2361 qed |
|
2362 |
|
2363 lemma card_of_Pow_Func: |
|
2364 "|Pow A| =o |Func A (UNIV::bool set)|" |
|
2365 proof- |
|
2366 def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False) |
|
2367 else undefined" |
|
2368 have "bij_betw F (Pow A) (Func A (UNIV::bool set))" |
|
2369 unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI) |
|
2370 fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2" |
|
2371 thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm) |
|
2372 next |
|
2373 show "F ` Pow A = Func A UNIV" |
|
2374 proof safe |
|
2375 fix f assume f: "f \<in> Func A (UNIV::bool set)" |
|
2376 show "f \<in> F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI) |
|
2377 let ?A1 = "{a \<in> A. f a = True}" |
|
2378 show "f = F ?A1" unfolding F_def apply(rule ext) |
|
2379 using f unfolding Func_def mem_Collect_eq by auto |
|
2380 qed auto |
|
2381 qed(unfold Func_def mem_Collect_eq F_def, auto) |
|
2382 qed |
|
2383 thus ?thesis unfolding card_of_ordIso[symmetric] by blast |
|
2384 qed |
|
2385 |
|
2386 lemma card_of_Func_mono: |
|
2387 fixes A1 A2 :: "'a set" and B :: "'b set" |
|
2388 assumes A12: "A1 \<subseteq> A2" and B: "B \<noteq> {}" |
|
2389 shows "|Func A1 B| \<le>o |Func A2 B|" |
|
2390 proof- |
|
2391 obtain bb where bb: "bb \<in> B" using B by auto |
|
2392 def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b) a. if a \<in> A2 then (if a \<in> A1 then f1 a else bb) |
|
2393 else undefined" |
|
2394 show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI) |
|
2395 show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe |
|
2396 fix f g assume f: "f \<in> Func A1 B" and g: "g \<in> Func A1 B" and eq: "F f = F g" |
|
2397 show "f = g" |
|
2398 proof(rule ext) |
|
2399 fix a show "f a = g a" |
|
2400 proof(cases "a \<in> A1") |
|
2401 case True |
|
2402 thus ?thesis using eq A12 unfolding F_def fun_eq_iff |
|
2403 by (elim allE[of _ a]) auto |
|
2404 qed(insert f g, unfold Func_def, fastforce) |
|
2405 qed |
|
2406 qed |
|
2407 qed(insert bb, unfold Func_def F_def, force) |
|
2408 qed |
|
2409 |
|
2410 lemma ordLeq_Func: |
|
2411 assumes "{b1,b2} \<subseteq> B" "b1 \<noteq> b2" |
|
2412 shows "|A| \<le>o |Func A B|" |
|
2413 unfolding card_of_ordLeq[symmetric] proof(intro exI conjI) |
|
2414 let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then b1 else b2) else undefined" |
|
2415 show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto |
|
2416 show "?F ` A \<subseteq> Func A B" using assms unfolding Func_def by auto |
|
2417 qed |
|
2418 |
|
2419 lemma infinite_Func: |
|
2420 assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2" |
|
2421 shows "infinite (Func A B)" |
|
2422 using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite) |
|
2423 |
|
2424 lemma card_of_Func_UNIV: |
|
2425 "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \<Rightarrow> 'b. range f \<subseteq> B}|" |
|
2426 apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI) |
|
2427 let ?F = "\<lambda> f (a::'a). ((f a)::'b)" |
|
2428 show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)" |
|
2429 unfolding bij_betw_def inj_on_def proof safe |
|
2430 fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B" |
|
2431 hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto |
|
2432 then obtain f where f: "\<forall> a. h a = f a" by metis |
|
2433 hence "range f \<subseteq> B" using h unfolding Func_def by auto |
|
2434 thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto |
|
2435 qed(unfold Func_def fun_eq_iff, auto) |
|
2436 qed |
|
2437 |
|
2438 end |