cardinalityCoreScript.sml
1Theory cardinalityCore[bare]
2Ancestors
3 prim_rec arithmetic pred_set pair sum option wellorder set_relation permutes
4Libs
5 HolKernel Parse boolLib BasicProvers pred_setLib simpLib metisLib
6 TotalDefn QLib numSimps numLib boolSimps mesonLib tautLib wlogLib
7
8(* emulation of bossLib environment *)
9fun simp ths g ctxt = simpLib.ASM_SIMP_TAC (srw_ss_of ctxt) ths g ctxt
10fun csimp ths = simp(SF CONJ_ss::ths)
11fun dsimp ths = simp(SF DNF_ss::ths)
12fun gvs ths g ctxt = simpLib.global_simp_tac
13 {elimvars = true, strip = true,
14 droptrues = true, oldestfirst = true}
15 (srw_ss_of ctxt) ths g ctxt
16fun gs ths g ctxt = simpLib.global_simp_tac
17 {elimvars = false, strip = true,
18 droptrues = true, oldestfirst = true}
19 (srw_ss_of ctxt) ths g ctxt
20fun rw ths = BasicProvers.SRW_TAC[]ths
21val metis_tac = METIS_TAC
22val decide_tac = DECIDE_TAC
23val AllCaseEqs = TypeBase.AllCaseEqs
24val op >~ = Q.>~
25fun kall_tac x = ALL_TAC
26fun SRULE ths = SIMP_RULE (srw_ss()) ths
27val METIS = metisLib.METIS_PROVE
28
29(* ------------------------------------------------------------------------- *)
30(* Cardinal comparisons *)
31(* ------------------------------------------------------------------------- *)
32
33(* first of these clashes with indicator_fn in extreal etc *)
34Overload "𝟙"[local] = “{()}”
35Overload "𝟚"[local] = “{T;F}”
36Overload "ℵ₀"[local] = “univ(:num)”
37
38Definition cardeq_def:
39 cardeq s1 s2 <=> ?f. BIJ f s1 s2
40End
41val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
42val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
43val _ = temp_TeX_notation {hol = "=~", TeX = ("\\ensuremath{\\approx}", 1)};
44val _ = temp_TeX_notation {hol = UTF8.chr 0x2248, TeX = ("\\ensuremath{\\approx}", 1)};
45
46Overload "=~"[local] = ``cardeq``
47
48Overload "≉"[local] = “λa b. ¬(a ≈ b)”
49val _ = temp_set_fixity "≉" (Infix(NONASSOC, 450))
50
51Theorem cardeq_REFL[simp]:
52 !s. s =~ s
53Proof
54 rw[cardeq_def] >> qexists_tac `\x. x` >> rw[BIJ_IFF_INV] >>
55 qexists_tac `\x. x` >> simp[]
56QED
57
58Theorem cardeq_SYMlemma[local]:
59 !s t. s =~ t ==> t =~ s
60Proof
61 rw[cardeq_def] >> metis_tac [BIJ_LINV_BIJ]
62QED
63
64Theorem cardeq_SYM:
65 !s:'a set t:'b set. s =~ t <=> t =~ s
66Proof
67 metis_tac [cardeq_SYMlemma]
68QED
69
70Theorem cardeq_TRANS:
71 !s t u. s =~ t /\ t =~ u ==> s =~ u
72Proof
73 metis_tac [BIJ_COMPOSE, cardeq_def]
74QED
75
76(* less-or-equal *)
77Definition cardleq_def:
78 cardleq s1 s2 <=> ?f. INJ f s1 s2
79End
80
81Overload "<<="[local] = ``cardleq``
82
83Theorem cardleq_REFL[simp]:
84 !s:'a set. s <<= s
85Proof
86 rw[cardleq_def] >> qexists_tac `\x. x` >> rw[INJ_ID]
87QED
88
89Theorem cardleq_TRANS:
90 !s:'a set t:'b set u:'c set. s <<= t /\ t <<= u ==> s <<= u
91Proof
92 rw[cardleq_def] >> metis_tac [INJ_COMPOSE]
93QED
94
95(* Schroeder-Bernstein theorem *)
96Theorem cardleq_ANTISYM:
97 !s t. s <<= t /\ t <<= s ==> s =~ t
98Proof
99 REWRITE_TAC [cardleq_def, cardeq_def]
100 >> REWRITE_TAC [SCHROEDER_BERNSTEIN]
101QED
102
103Theorem CARDEQ_FINITE:
104 s1 =~ s2 ==> (FINITE s1 <=> FINITE s2)
105Proof
106 metis_tac [cardeq_def, BIJ_FINITE, BIJ_LINV_BIJ]
107QED
108
109Theorem CARDEQ_CARD:
110 s1 =~ s2 /\ FINITE s1 ==> (CARD s1 = CARD s2)
111Proof
112 metis_tac [cardeq_def, FINITE_BIJ_CARD_EQ, CARDEQ_FINITE]
113QED
114
115Theorem CARDEQ_0:
116 (x =~ {} <=> (x = {})) /\ (({} =~ x) <=> (x = {}))
117Proof
118 rw[cardeq_def, BIJ_EMPTY]
119QED
120
121Theorem cardeq_INSERT:
122 (x INSERT s) =~ s <=> x IN s \/ INFINITE s
123Proof
124 simp[EQ_IMP_THM] >> conj_tac
125 >- (Cases_on `FINITE s` >> simp[] >> strip_tac >>
126 `CARD (x INSERT s) = CARD s` by metis_tac [CARDEQ_CARD, cardeq_SYM] >>
127 pop_assum mp_tac >> SRW_TAC[ARITH_ss][]) >>
128 Cases_on `x IN s` >- metis_tac [ABSORPTION, cardeq_REFL] >> rw[] >>
129 match_mp_tac cardleq_ANTISYM >> Tactical.REVERSE conj_tac
130 >- (rw[cardleq_def] >> qexists_tac `\x. x` >> rw[INJ_DEF]) >>
131 rw[cardleq_def] >> gvs[infinite_num_inj] >>
132 qexists_tac `\e. if e = x then f 0
133 else case some n. e = f n of
134 NONE => e
135 | SOME n => f (n + 1)` >>
136 gvs[INJ_DEF] >>
137 `!x y. (f x = f y) <=> (x = y)` by metis_tac[] >> rw[] >| [
138 rw[option_case_compute],
139 DEEP_INTRO_TAC some_intro >> rw[] >>
140 metis_tac [DECIDE ``0 <> x + 1``],
141 DEEP_INTRO_TAC some_intro >> rw[] >>
142 metis_tac [DECIDE ``0 <> x + 1``],
143 pop_assum mp_tac >>
144 DEEP_INTRO_TAC some_intro >> simp[] >>
145 DEEP_INTRO_TAC some_intro >> simp[]
146 ]
147QED
148
149(* !s. INFINITE s ==> x INSERT s =~ s
150
151 more useful then CARDEQ_INSERT as a (conditional) "rewrite", when
152 working with the =~ congruence (rather than equality) *)
153Theorem CARDEQ_INSERT_RWT =
154 ``INFINITE (s:'a set)`` |> ASSUME |> DISJ2 ``(x:'a) IN s``
155 |> EQ_MP (SYM cardeq_INSERT) |> DISCH_ALL
156 |> Q.GEN `s`
157
158Theorem EMPTY_CARDLEQ[simp]:
159 {} <<= t
160Proof
161 simp[cardleq_def, INJ_EMPTY]
162QED
163
164Theorem FINITE_CLE_INFINITE:
165 FINITE s /\ INFINITE t ==> s <<= t
166Proof
167 qsuff_tac `INFINITE t ==> !s. FINITE s ==> s <<= t` >- metis_tac[] >>
168 strip_tac >> Induct_on `FINITE` >> conj_tac >- simp[] >>
169 simp[cardleq_def] >> gen_tac >>
170 disch_then (CONJUNCTS_THEN2 assume_tac
171 (Q.X_CHOOSE_THEN `f` assume_tac)) >>
172 qx_gen_tac `e` >> strip_tac >>
173 `FINITE (IMAGE f s)` by simp[] >>
174 `?y. y IN t /\ y NOTIN IMAGE f s` by metis_tac [IN_INFINITE_NOT_FINITE] >>
175 qexists_tac `\x. if x = e then y else f x` >>
176 gvs[INJ_DEF] >> asm_simp_tac (srw_ss() ++ DNF_ss) [] >> rw[] >> metis_tac[]
177QED
178
179val FORALL_PROD = pairTheory.FORALL_PROD
180Theorem CARDEQ_CROSS:
181 s1 =~ s2 /\ t1 =~ t2 ==> (s1 CROSS t1 =~ s2 CROSS t2)
182Proof
183 simp[cardeq_def] >>
184 disch_then (CONJUNCTS_THEN2 (Q.X_CHOOSE_THEN `f` assume_tac)
185 (Q.X_CHOOSE_THEN `g` assume_tac)) >>
186 qexists_tac `f ## g` >>
187 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD,
188 pairTheory.EXISTS_PROD] >>
189 gvs[BIJ_DEF, INJ_DEF, SURJ_DEF] >> metis_tac []
190QED
191
192Theorem CARDEQ_CROSS_SYM:
193 s CROSS t =~ t CROSS s
194Proof
195 simp[cardeq_def] >>
196 qexists_tac`\p. (SND p,FST p)` >>
197 simp[BIJ_IFF_INV] >>
198 qexists_tac`\p. (SND p,FST p)` >>
199 simp[]
200QED
201
202Theorem CARDEQ_SUBSET_CARDLEQ:
203 s =~ t ==> s <<= t
204Proof
205 rw[cardeq_def, cardleq_def, BIJ_DEF] >> metis_tac[]
206QED
207
208Theorem cardleq_ANTISYM_IFF:
209 ∀s t. s ≼ t ∧ t ≼ s ⇔ s ≈ t
210Proof
211 simp[EQ_IMP_THM, cardleq_ANTISYM] >>
212 metis_tac[CARDEQ_SUBSET_CARDLEQ, cardeq_SYM]
213QED
214
215Theorem CARDEQ_CARDLEQ:
216 s1 =~ s2 /\ t1 =~ t2 ==> (s1 <<= t1 <=> s2 <<= t2)
217Proof
218 metis_tac[cardeq_SYM, CARDEQ_SUBSET_CARDLEQ, cardleq_TRANS]
219QED
220
221Theorem CARDLEQ_FINITE:
222 !s1 s2. FINITE s2 /\ s1 <<= s2 ==> FINITE s1
223Proof
224 metis_tac[cardleq_def,FINITE_INJ]
225QED
226
227Theorem INFINITE_UNIV_INF[simp]:
228 INFINITE univ(:'a inf)
229Proof
230 simp[INFINITE_UNIV] >> qexists_tac `SUM_MAP SUC I` >>
231 simp[sumTheory.FORALL_SUM] >> qexists_tac `INL 0` >> simp[]
232QED
233
234Theorem IMAGE_cardleq[simp]:
235 !f s. IMAGE f s <<= s
236Proof
237 simp[cardleq_def] >> metis_tac [SURJ_IMAGE, SURJ_INJ_INV]
238QED
239
240Theorem CARDLEQ_CROSS_CONG:
241 !x1 x2 y1 y2. x1 <<= x2 /\ y1 <<= y2 ==> x1 CROSS y1 <<= x2 CROSS y2
242Proof
243 rpt gen_tac \\
244 simp[cardleq_def] >>
245 disch_then (CONJUNCTS_THEN2 (Q.X_CHOOSE_THEN `f1` assume_tac)
246 (Q.X_CHOOSE_THEN `f2` assume_tac)) >>
247 gvs[INJ_DEF] >>
248 qexists_tac `\(x,y). (f1 x, f2 y)` >>
249 simp[FORALL_PROD]
250QED
251
252Theorem SUBSET_CARDLEQ:
253 !x y. x SUBSET y ==> x <<= y
254Proof
255 rpt gen_tac \\
256 simp[SUBSET_DEF, cardleq_def] >> strip_tac >> qexists_tac `I` >>
257 simp[INJ_DEF]
258QED
259
260Theorem IMAGE_cardleq_rwt:
261 !s t. s <<= t ==> IMAGE f s <<= t
262Proof
263 metis_tac [cardleq_TRANS, IMAGE_cardleq]
264QED
265
266Theorem countable_thm:
267 !s. countable s <=> s <<= univ(:num)
268Proof
269 simp[countable_def, cardleq_def]
270QED
271
272Theorem countable_cardeq:
273 !s t. s =~ t ==> (countable s <=> countable t)
274Proof
275 simp[countable_def, cardeq_def, EQ_IMP_THM] >>
276 metis_tac [INJ_COMPOSE, BIJ_DEF, BIJ_LINV_BIJ]
277QED
278
279Theorem cardleq_dichotomy:
280 !s t. s <<= t \/ t <<= s
281Proof
282 rpt gen_tac \\
283 `(?w1. elsOf w1 = s) /\ (?w2. elsOf w2 = t)`
284 by metis_tac [allsets_wellorderable] >>
285 `orderlt w1 w2 \/ orderiso w1 w2 \/ orderlt w2 w1`
286 by metis_tac [orderlt_trichotomy]
287 >| [
288 `?f x. BIJ f s (elsOf (wobound x w2))`
289 by metis_tac[orderlt_def, orderiso_thm] >>
290 `elsOf (wobound x w2) SUBSET t`
291 by (simp[elsOf_wobound, SUBSET_DEF] >> metis_tac [WIN_elsOf]) >>
292 rw[] >> qsuff_tac `elsOf w1 <<= elsOf w2` >- simp[] >>
293 simp[cardleq_def] >> qexists_tac `f` >>
294 gvs[BIJ_DEF, INJ_DEF, SUBSET_DEF],
295
296 `?f. BIJ f s t` by metis_tac [orderiso_thm] >>
297 gvs[BIJ_DEF, cardleq_def] >> metis_tac[],
298
299 `?f x. BIJ f t (elsOf (wobound x w1))`
300 by metis_tac[orderlt_def, orderiso_thm] >>
301 `elsOf (wobound x w1) SUBSET s`
302 by (simp[elsOf_wobound, SUBSET_DEF] >> metis_tac [WIN_elsOf]) >>
303 rw[] >> qsuff_tac `elsOf w2 <<= elsOf w1` >- simp[] >>
304 simp[cardleq_def] >> qexists_tac `f` >>
305 gvs[BIJ_DEF, INJ_DEF, SUBSET_DEF]
306 ]
307QED
308
309val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
310
311val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
312val _ = temp_TeX_notation {hol = "<</=", TeX = ("\\ensuremath{\\prec}", 1)};
313val _ = temp_TeX_notation {hol = UTF8.chr 0x227A, TeX = ("\\ensuremath{\\prec}", 1)};
314
315Overload cardlt[local] = ``\s1 s2. ~(cardleq s2 s1)``(* cardlt *)
316Overload "<</="[local] = ``cardlt``
317
318Theorem cardleq_lteq:
319 !s1 s2. s1 <<= s2 <=> s1 <</= s2 \/ (s1 =~ s2)
320Proof
321 metis_tac [cardleq_ANTISYM, cardleq_dichotomy, CARDEQ_SUBSET_CARDLEQ]
322QED
323
324Theorem cardlt_REFL:
325 !s. ~(s <</= s)
326Proof
327 simp[cardleq_REFL]
328QED
329
330Theorem cardlt_lenoteq:
331 !s t. s <</= t <=> s <<= t /\ ~(s =~ t)
332Proof
333 metis_tac [cardleq_dichotomy, CARDEQ_SUBSET_CARDLEQ, cardeq_SYM,
334 cardleq_ANTISYM, cardeq_REFL]
335QED
336
337Theorem cardlt_TRANS:
338 !s t u:'a set. s <</= t /\ t <</= u ==> s <</= u
339Proof
340 metis_tac [cardleq_TRANS, cardleq_ANTISYM, CARDEQ_SUBSET_CARDLEQ,
341 cardeq_SYM, cardlt_lenoteq]
342QED
343
344Theorem cardlt_leq_trans:
345 !r s t. r <</= s /\ s <<= t ==> r <</= t
346Proof
347 rw[cardlt_lenoteq] >- metis_tac[cardleq_TRANS] >>
348 metis_tac[CARDEQ_CARDLEQ,cardeq_REFL,cardleq_ANTISYM]
349QED
350
351Theorem cardleq_lt_trans:
352 !r s t. r <<= s /\ s <</= t ==> r <</= t
353Proof
354 rw[cardlt_lenoteq] >- metis_tac[cardleq_TRANS] >>
355 metis_tac[CARDEQ_CARDLEQ,cardeq_REFL,cardleq_ANTISYM]
356QED
357
358Theorem cardleq_empty[simp]:
359 !x. x <<= {} <=> (x = {})
360Proof
361 simp[cardleq_lteq,CARDEQ_0]
362QED
363
364val better_BIJ = BIJ_DEF |> SIMP_RULE (srw_ss() ++ CONJ_ss) [INJ_DEF, SURJ_DEF]
365
366fun unabbrev_in_goal s = let
367 fun check th = let
368 val c = concl th
369 val _ = match_term ``Abbrev b`` c
370 val (v,ty) = c |> rand |> lhand |> dest_var
371 in
372 if v = s then let
373 val th' = PURE_REWRITE_RULE [markerTheory.Abbrev_def] th
374 in
375 SUBST1_TAC th'
376 end
377 else NO_TAC
378 end
379in
380 first_assum check
381end
382
383Theorem set_binomial2:
384 (A UNION B) CROSS (A UNION B) =
385 A CROSS A UNION A CROSS B UNION B CROSS A UNION B CROSS B
386Proof
387 simp[EXTENSION, FORALL_PROD] >>
388 simp_tac (srw_ss() ++ DNF_ss) [DISJ_ASSOC]
389QED
390
391Theorem lemma1[local]:
392 INFINITE M /\ M =~ M CROSS M ==>
393 M =~ {T;F} CROSS M /\
394 !A B. DISJOINT A B /\ A =~ M /\ B =~ M ==> A UNION B =~ M
395Proof
396 strip_tac >> CONJ_ASM1_TAC
397 >- (match_mp_tac cardleq_ANTISYM >> conj_tac
398 >- (simp[cardleq_def] >> qexists_tac `\x. (T,x)` >> simp[INJ_DEF]) >>
399 `M CROSS M <<= M` by metis_tac [CARDEQ_CARDLEQ, cardleq_REFL, cardeq_REFL] >>
400 qsuff_tac `{T;F} CROSS M <<= M CROSS M` >- metis_tac [cardleq_TRANS] >>
401 match_mp_tac CARDLEQ_CROSS_CONG >> simp[FINITE_CLE_INFINITE]) >>
402 simp[DISJOINT_DEF, EXTENSION] >> rpt strip_tac >>
403 `(?f1. BIJ f1 A M) /\ (?f2. BIJ f2 B M)` by metis_tac[cardeq_def] >>
404 qsuff_tac `A UNION B =~ {T;F} CROSS M`
405 >- metis_tac [cardeq_TRANS, cardeq_SYM] >>
406 simp[cardeq_def] >>
407 qexists_tac `\x. if x IN A then (T,f1 x) else (F,f2 x)` >>
408 simp[better_BIJ] >> rpt conj_tac
409 >- (gvs[better_BIJ] >> rw[])
410 >- (map_every qx_gen_tac [`a`, `b`] >> strip_tac >> simp[] >>
411 metis_tac[BIJ_DEF, INJ_DEF, pairTheory.PAIR_EQ]) >>
412 simp[FORALL_PROD] >> map_every qx_gen_tac [`test`, `m`] >> strip_tac >>
413 Cases_on `test`
414 >- (`?a. a IN A /\ (f1 a = m)` by metis_tac [BIJ_DEF, SURJ_DEF] >>
415 qexists_tac `a` >> simp[]) >>
416 `?b. b IN B /\ (f2 b = m)` by metis_tac [BIJ_DEF, SURJ_DEF] >>
417 qexists_tac `b` >> simp[] >> metis_tac[]
418QED
419
420fun PRINT_TAC s = goalStack.note_tac ("** " ^ s)
421
422Theorem SET_SQUARED_CARDEQ_SET:
423 !s. INFINITE s ==> (s CROSS s =~ s)
424Proof
425 PRINT_TAC "beginning s CROSS s =~ s proof" >>
426 rpt strip_tac >>
427 qabbrev_tac `
428 A = { (As,f) | INFINITE As /\ As SUBSET s /\ BIJ f As (As CROSS As) /\
429 !x. x NOTIN As ==> (f x = ARB) }` >>
430 qabbrev_tac `
431 rr = {((s1:'a set,f1),(s2,f2)) | (s1,f1) IN A /\ (s2,f2) IN A /\
432 s1 SUBSET s2 /\
433 !x. x IN s1 ==> (f1 x = f2 x)} ` >>
434 `partial_order rr A`
435 by (simp[partial_order_def] >> rpt conj_tac
436 >- (simp[domain_def, Abbr`rr`, SUBSET_DEF] >> rw[] >> rw[])
437 >- (simp[range_def, Abbr`rr`, SUBSET_DEF] >> rw[] >> rw[])
438 >- (simp[transitive_def, Abbr`rr`] >> rw[] >>
439 metis_tac [SUBSET_TRANS, SUBSET_DEF])
440 >- simp[reflexive_def, Abbr`rr`, FORALL_PROD] >>
441 simp[antisym_def, Abbr`rr`, FORALL_PROD] >>
442 map_every qx_gen_tac [`s1`, `f1`, `s2`, `f2`] >>
443 strip_tac >> `s1 = s2` by metis_tac [SUBSET_ANTISYM] >>
444 gvs[Abbr`A`] >> simp[FUN_EQ_THM] >> metis_tac[]) >>
445 `A <> {}`
446 by (`?Nf. INJ Nf univ(:num) s` by metis_tac [infinite_num_inj] >>
447 qabbrev_tac `
448 Nfn = \a. case some m. Nf m = a of
449 NONE => ARB
450 | SOME m => (Nf (nfst m), Nf (nsnd m))` >>
451 `(IMAGE Nf univ(:num), Nfn) IN A`
452 by (`!x y. (Nf x = Nf y) = (x = y)`
453 by metis_tac [INJ_DEF, IN_UNIV] >>
454 simp[Abbr`A`] >> conj_tac
455 >- (gvs[SUBSET_DEF, INJ_DEF] >> metis_tac[]) >>
456 simp[better_BIJ] >>
457 asm_simp_tac (srw_ss() ++ DNF_ss) [FORALL_PROD] >>
458 simp[Abbr`Nfn`] >> conj_tac
459 >- (map_every qx_gen_tac [`m`, `p`] >> strip_tac >>
460 map_every (fn q => qspec_then q (SUBST1_TAC o SYM)
461 numpairTheory.npair)
462 [`m`, `p`] >> simp[]) >>
463 simp[FORALL_PROD] >>
464 map_every qx_gen_tac [`m`, `p`] >> qexists_tac `m *, p` >>
465 simp[]) >>
466 strip_tac >> gvs[]) >>
467 `!t. chain t rr ==> upper_bounds t rr <> {}`
468 by (PRINT_TAC "beginning proof that chains have upper bound" >>
469 gen_tac >>
470 simp[chain_def] >> strip_tac >>
471 `!s0 f. (s0,f) IN t ==> BIJ f s0 (s0 CROSS s0) /\ s0 SUBSET s /\ (s0,f) IN A /\
472 !x. x NOTIN s0 ==> (f x = ARB)`
473 by (rpt gen_tac >> strip_tac >>
474 pop_assum (fn th => first_x_assum (fn impth =>
475 mp_tac (MATCH_MP impth (CONJ th th)))) >>
476 rw[Abbr`rr`, Abbr`A`]) >>
477 simp[upper_bounds_def] >> simp[EXTENSION] >>
478 `!s1 f1 s2 f2 x. (s1,f1) IN t /\ (s2,f2) IN t /\ x IN s1 /\ x IN s2 ==>
479 (f1 x = f2 x)`
480 by (rpt strip_tac >>
481 Q.UNDISCH_THEN `(s1,f1) IN t` (fn th1 =>
482 Q.UNDISCH_THEN `(s2,f2) IN t` (fn th2 =>
483 first_x_assum (fn impth =>
484 mp_tac
485 (MATCH_MP impth (CONJ th1 th2))))) >>
486 simp[Abbr`rr`] >> rw[] >> rw[]) >>
487 qabbrev_tac `BigSet = BIGUNION (IMAGE FST t)` >>
488 qabbrev_tac `BigF = (\a. case some (s,f). (s,f) IN t /\ a IN s of
489 NONE => ARB
490 | SOME (_, f) => f a)` >>
491 Cases_on `t = {}`
492 >- (simp[range_def] >>
493 `?x. x IN A` by (gvs[EXTENSION] >> metis_tac[]) >>
494 map_every qexists_tac [`x`, `x`] >>
495 simp[Abbr`rr`] >> Cases_on `x` >> simp[]) >>
496 `(BigSet,BigF) IN A` by
497 (unabbrev_in_goal "A" >> simp[] >> rpt conj_tac
498 >- (simp[Abbr`BigSet`] >> DISJ2_TAC >>
499 simp[pairTheory.EXISTS_PROD] >>
500 `?pr. pr IN t` by simp[MEMBER_NOT_EMPTY] >>
501 Cases_on `pr` >> res_tac >> gvs[Abbr`A`] >> metis_tac[])
502 >- (simp_tac (srw_ss() ++ DNF_ss)
503 [BIGUNION_SUBSET, FORALL_PROD, Abbr`BigSet`] >>
504 metis_tac[])
505 >- ((* showing function is a bijection *)
506 asm_simp_tac (srw_ss() ++ DNF_ss)
507 [better_BIJ, FORALL_PROD, Abbr`BigF`,
508 Abbr`BigSet`, pairTheory.EXISTS_PROD] >>
509 rpt conj_tac
510 >- ((* function hits target set *)
511 map_every qx_gen_tac [`a`, `ss`, `sf`] >>
512 strip_tac >>
513 map_every qexists_tac [`ss`, `sf`, `ss`, `sf`] >>
514 simp[] >>
515 qmatch_abbrev_tac `FST XX IN ss /\ SND XX IN ss` >>
516 `XX = sf a`
517 by (simp[Abbr`XX`] >>
518 DEEP_INTRO_TAC some_intro >>
519 simp[FORALL_PROD] >> metis_tac[]) >>
520 `BIJ sf ss (ss CROSS ss)` by metis_tac[] >> simp[] >>
521 pop_assum mp_tac >> simp_tac (srw_ss())[better_BIJ] >>
522 simp[])
523 >- ((* function is injective *)
524 map_every qx_gen_tac
525 [`a1`, `a2`, `s1`, `f1`, `s2`, `f2`] >>
526 strip_tac >>
527 qmatch_abbrev_tac `(XX1 = XX2) ==> (a1 = a2)` >>
528 `XX1 = f1 a1`
529 by (simp[Abbr`XX1`] >>
530 DEEP_INTRO_TAC some_intro >>
531 simp[FORALL_PROD] >> metis_tac[]) >>
532 `XX2 = f2 a2`
533 by (simp[Abbr`XX2`] >>
534 DEEP_INTRO_TAC some_intro >>
535 simp[FORALL_PROD] >> metis_tac[]) >>
536 map_every markerLib.RM_ABBREV_TAC ["XX1", "XX2"] >>
537 rw[] >>
538 Q.UNDISCH_THEN `(s1,f1) IN t` (fn th1 =>
539 (Q.UNDISCH_THEN `(s2,f2) IN t` (fn th2 =>
540 (first_x_assum (fn impth =>
541 mp_tac (MATCH_MP impth (CONJ th1 th2))))))) >>
542 simp[Abbr`rr`, Abbr`A`] >> rw[]
543 >- (`f1 a1 = f2 a1` by metis_tac[] >>
544 `a1 IN s2` by metis_tac [SUBSET_DEF] >>
545 metis_tac [BIJ_DEF, INJ_DEF]) >>
546 `f2 a2 = f1 a2` by metis_tac[] >>
547 `a2 IN s1` by metis_tac [SUBSET_DEF] >>
548 metis_tac [BIJ_DEF, INJ_DEF]) >>
549 (* function is surjective *)
550 map_every qx_gen_tac [`a`, `b`, `s1`, `f1`, `s2`, `f2`] >>
551 strip_tac >>
552 Q.UNDISCH_THEN `(s1,f1) IN t` (fn th1 =>
553 (Q.UNDISCH_THEN `(s2,f2) IN t` (fn th2 =>
554 (first_assum (fn impth =>
555 mp_tac (MATCH_MP impth (CONJ th1 th2)) >>
556 assume_tac th1 >> assume_tac th2))))) >>
557 unabbrev_in_goal "rr" >> simp_tac(srw_ss())[] >> rw[]
558 >- (`a IN s2` by metis_tac [SUBSET_DEF] >>
559 `(a,b) IN s2 CROSS s2` by simp[] >>
560 `?x. x IN s2 /\ (f2 x = (a,b))`
561 by metis_tac [SURJ_DEF, BIJ_DEF] >>
562 map_every qexists_tac [`x`, `s2`, `f2`] >>
563 simp[] >> DEEP_INTRO_TAC some_intro >>
564 simp[FORALL_PROD] >>
565 Tactical.REVERSE conj_tac >- metis_tac[] >>
566 map_every qx_gen_tac [`s3`, `f3`] >> strip_tac >>
567 Q.UNDISCH_THEN `(s2,f2) IN t` (fn th1 =>
568 (Q.UNDISCH_THEN `(s3,f3) IN t` (fn th2 =>
569 (first_x_assum (fn impth =>
570 mp_tac (MATCH_MP impth (CONJ th1 th2))))))) >>
571 unabbrev_in_goal "rr" >> simp[] >> rw[] >> metis_tac[]) >>
572 `b IN s1` by metis_tac [SUBSET_DEF] >>
573 `(a,b) IN s1 CROSS s1` by simp[] >>
574 `?x. x IN s1 /\ (f1 x = (a,b))`
575 by metis_tac[BIJ_DEF, SURJ_DEF] >>
576 map_every qexists_tac [`x`, `s1`, `f1`] >> simp[] >>
577 DEEP_INTRO_TAC some_intro >>
578 simp[FORALL_PROD] >>
579 Tactical.REVERSE conj_tac >- metis_tac[] >>
580 map_every qx_gen_tac [`s3`, `f3`] >> strip_tac >>
581 Q.UNDISCH_THEN `(s1,f1) IN t` (fn th1 =>
582 (Q.UNDISCH_THEN `(s3,f3) IN t` (fn th2 =>
583 (first_x_assum (fn impth =>
584 mp_tac (MATCH_MP impth (CONJ th1 th2))))))) >>
585 unabbrev_in_goal "rr" >> simp[] >> rw[] >> metis_tac[]) >>
586 (* function is ARB outside of domain *)
587 qx_gen_tac `x` >>
588 asm_simp_tac (srw_ss() ++ DNF_ss)
589 [Abbr`BigF`, Abbr`BigSet`,
590 DECIDE ``~p\/q = (p ==> q)``, FORALL_PROD]>>
591 strip_tac >> DEEP_INTRO_TAC some_intro >>
592 simp[FORALL_PROD] >> metis_tac[]) >>
593 qexists_tac `(BigSet, BigF)` >> conj_tac
594 >- ((* (BigSet, BigF) IN range rr *)
595 simp[range_def] >> qexists_tac `(BigSet,BigF)` >>
596 simp[Abbr`rr`]) >>
597 (* upper bound really is bigger than arbitrary element of chain *)
598 simp[FORALL_PROD] >> map_every qx_gen_tac [`s1`, `f1`] >>
599 Cases_on `(s1,f1) IN t` >> simp[] >>
600 unabbrev_in_goal "rr" >> simp[] >> conj_tac
601 >- (simp[Abbr`BigSet`] >> match_mp_tac SUBSET_BIGUNION_I >>
602 simp[pairTheory.EXISTS_PROD] >> metis_tac[]) >>
603 qx_gen_tac `x` >> strip_tac >> simp[Abbr`BigF`] >>
604 DEEP_INTRO_TAC some_intro >>
605 simp[FORALL_PROD] >> metis_tac[]) >>
606 PRINT_TAC "proved that upper bound works" >>
607 `?Mf. Mf IN maximal_elements A rr` by metis_tac [zorns_lemma] >>
608 `?M mf. Mf = (M,mf)` by metis_tac [pairTheory.pair_CASES] >>
609 pop_assum SUBST_ALL_TAC >>
610 gvs[maximal_elements_def] >>
611 Q.UNDISCH_THEN `(M,mf) IN A` mp_tac >> unabbrev_in_goal "A" >> simp[] >>
612 strip_tac >>
613 `M =~ M CROSS M` by metis_tac[cardeq_def] >>
614 Cases_on `M =~ s` >- metis_tac [CARDEQ_CROSS, cardeq_TRANS, cardeq_SYM] >>
615 `M <<= s` by simp[SUBSET_CARDLEQ] >>
616 `M =~ {T;F} CROSS M` by metis_tac [lemma1] >>
617 `s = M UNION (s DIFF M)` by (gvs[EXTENSION, SUBSET_DEF] >> metis_tac[]) >>
618 `~(s DIFF M <<= M)`
619 by (strip_tac >>
620 qsuff_tac `s <<= M` >- metis_tac [cardleq_ANTISYM] >>
621 qsuff_tac `s <<= {T;F} CROSS M` >- metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
622 `?f0. INJ f0 (s DIFF M) M` by metis_tac[cardleq_def] >>
623 simp[cardleq_def, INJ_DEF] >>
624 qexists_tac `\a. if a IN M then (T,a) else (F,f0 a)` >>
625 simp[] >> conj_tac
626 >- (rw[] >> metis_tac [IN_DIFF, INJ_DEF]) >>
627 rw[] >> prove_tac[IN_DIFF, INJ_DEF]) >>
628 `~(s DIFF M =~ M)` by metis_tac [CARDEQ_SUBSET_CARDLEQ] >>
629 `?f. INJ f M (s DIFF M)` by metis_tac [cardleq_def, cardlt_lenoteq] >>
630 qabbrev_tac `E = IMAGE f M` >>
631 `E SUBSET s DIFF M` by (gvs[INJ_DEF, SUBSET_DEF, Abbr`E`] >> metis_tac[]) >>
632 `INJ f M E` by (gvs[Abbr`E`, INJ_DEF] >> metis_tac[]) >>
633 `SURJ f M E` by simp[Abbr`E`] >>
634 `M =~ E` by metis_tac[cardeq_def, BIJ_DEF] >>
635 `E CROSS E =~ M` by metis_tac [CARDEQ_CROSS, cardeq_SYM, cardeq_TRANS] >>
636 `E CROSS M =~ M` by metis_tac [CARDEQ_CROSS, cardeq_SYM, cardeq_TRANS] >>
637 `M CROSS E =~ M` by metis_tac [CARDEQ_CROSS, cardeq_SYM, cardeq_TRANS] >>
638 `DISJOINT (E CROSS M) (E CROSS E)`
639 by (simp[DISJOINT_DEF, EXTENSION, FORALL_PROD] >>
640 metis_tac [SUBSET_DEF, IN_DIFF]) >>
641 `(E CROSS M) UNION (E CROSS E) =~ M` by metis_tac [lemma1] >>
642 `DISJOINT (M CROSS E) (E CROSS M UNION E CROSS E)`
643 by (simp[DISJOINT_DEF, EXTENSION, FORALL_PROD] >>
644 metis_tac [SUBSET_DEF, IN_DIFF]) >>
645 `M CROSS E UNION (E CROSS M UNION E CROSS E) =~ M` by metis_tac[lemma1] >>
646 `M CROSS E UNION E CROSS M UNION E CROSS E =~ E`
647 by metis_tac[UNION_ASSOC, cardeq_TRANS] >>
648 pop_assum mp_tac >> qmatch_abbrev_tac `ME =~ E ==> s CROSS s =~ s` >>
649 strip_tac >>
650 `?f0. BIJ f0 E ME` by metis_tac [cardeq_def, cardeq_SYM] >>
651 qabbrev_tac `FF = \m. if m IN M then mf m else if m IN E then f0 m else ARB` >>
652 `(M UNION E) CROSS (M UNION E) = M CROSS M UNION ME`
653 by simp[Abbr`ME`, UNION_ASSOC, set_binomial2] >>
654 qabbrev_tac `MM = M CROSS M` >>
655 `DISJOINT M E`
656 by (simp[DISJOINT_DEF, EXTENSION] >> metis_tac[IN_DIFF, SUBSET_DEF]) >>
657 `DISJOINT MM ME`
658 by (pop_assum mp_tac >>
659 simp[DISJOINT_DEF, EXTENSION, Abbr`ME`, Abbr`MM`, FORALL_PROD] >>
660 metis_tac[]) >>
661 PRINT_TAC "proving properties of new (can't exist) bijection" >>
662 `BIJ FF (M UNION E) ((M UNION E) CROSS (M UNION E))`
663 by (simp[better_BIJ, Abbr`FF`] >> rpt conj_tac
664 >- (qx_gen_tac `m` >> Cases_on `m IN M` >> simp[] >>
665 gvs[better_BIJ] >> strip_tac >>
666 map_every qunabbrev_tac [`ME`, `MM`] >>
667 gvs[] >> metis_tac[])
668 >- (map_every qx_gen_tac [`m1`, `m2`] >>
669 strip_tac >> gvs[better_BIJ, DISJOINT_DEF, EXTENSION] >>
670 metis_tac[])
671 >- (simp[FORALL_PROD] >> map_every qx_gen_tac [`m1`, `m2`] >>
672 strip_tac
673 >- (gvs[better_BIJ] >> qsuff_tac `(m1,m2) IN MM` >- metis_tac[] >>
674 simp[Abbr`MM`]) >>
675 (Q.UNDISCH_THEN `DISJOINT M E` mp_tac >>
676 simp[DISJOINT_DEF, EXTENSION] >> strip_tac >>
677 gvs[better_BIJ] >>
678 qsuff_tac `(m1,m2) IN ME` >- metis_tac[] >>
679 simp[Abbr`ME`]))) >>
680 `(M UNION E, FF) IN A`
681 by (simp[Abbr`A`] >> conj_tac >- (gvs[SUBSET_DEF] >> metis_tac[]) >>
682 simp[Abbr`FF`]) >>
683 `(M,mf) <> (M UNION E, FF)`
684 by (`M <> {}` by metis_tac[FINITE_EMPTY] >>
685 simp[] >> simp[EXTENSION] >>
686 gvs[DISJOINT_DEF, EXTENSION] >> metis_tac[CARDEQ_0, MEMBER_NOT_EMPTY]) >>
687 qsuff_tac `((M,mf), (M UNION E, FF)) IN rr` >- metis_tac[] >>
688 simp[Abbr`rr`] >> conj_tac >- simp[Abbr`A`] >>
689 simp[Abbr`FF`]
690QED
691
692Theorem SET_SUM_CARDEQ_SET:
693 INFINITE s ==>
694 s =~ {T;F} CROSS s /\
695 !A B. DISJOINT A B /\ A =~ s /\ B =~ s ==> A UNION B =~ s
696Proof
697 metis_tac[lemma1, SET_SQUARED_CARDEQ_SET, cardeq_SYM]
698QED
699
700Theorem CARD_BIGUNION:
701 INFINITE k /\ s1 <<= k /\ (!e. e IN s1 ==> e <<= k) ==> BIGUNION s1 <<= k
702Proof
703 `BIGUNION s1 = BIGUNION (s1 DELETE {})` by (simp[EXTENSION] >> metis_tac[]) >>
704 pop_assum SUBST1_TAC >>
705 Cases_on `INFINITE k` >> simp[cardleq_def] >>
706 disch_then (CONJUNCTS_THEN2
707 (Q.X_CHOOSE_THEN `f` strip_assume_tac) strip_assume_tac) >>
708 qabbrev_tac `s = s1 DELETE {}` >>
709 `INJ f s k` by gvs[INJ_DEF, Abbr`s`] >>
710 `(s = {}) \/ ?ff. SURJ ff k s` by metis_tac [inj_surj] >- simp[INJ_EMPTY] >>
711 `{} NOTIN s` by simp[Abbr`s`] >>
712 qsuff_tac `?fg. SURJ fg k (BIGUNION s)` >- metis_tac[SURJ_INJ_INV] >>
713 `k =~ k CROSS k` by metis_tac [SET_SQUARED_CARDEQ_SET, cardeq_SYM] >>
714 `?kkf. BIJ kkf k (k CROSS k)` by metis_tac [cardeq_def] >>
715 qsuff_tac `?fg. SURJ fg (k CROSS k) (BIGUNION s)`
716 >- (strip_tac >> qexists_tac `fg o kkf` >> match_mp_tac SURJ_COMPOSE >>
717 metis_tac[BIJ_DEF]) >>
718 `!e. e IN s ==> ?g. SURJ g k e` by metis_tac[inj_surj, IN_DELETE] >>
719 pop_assum (Q.X_CHOOSE_THEN `g` assume_tac o
720 CONV_RULE (BINDER_CONV RIGHT_IMP_EXISTS_CONV THENC
721 SKOLEM_CONV)) >>
722 qexists_tac `λ(k1,k2). g (ff k1) k2` >>
723 asm_simp_tac (srw_ss() ++ DNF_ss)
724 [SURJ_DEF, FORALL_PROD, pairTheory.EXISTS_PROD] >>
725 gvs[SURJ_DEF] >> metis_tac[]
726QED
727
728Theorem CARD_MUL_ABSORB_LE:
729 !s t. INFINITE t /\ s <<= t ==> s CROSS t <<= t
730Proof
731 metis_tac[CARDLEQ_CROSS_CONG,SET_SQUARED_CARDEQ_SET,
732 cardleq_lteq,cardleq_TRANS,cardleq_REFL]
733QED
734
735Theorem CARD_MUL_LT_LEMMA:
736 !s t. s <<= t /\ t <</= u /\ INFINITE u ==> s CROSS t <</= u
737Proof
738 rw[] >>
739 Cases_on`FINITE t` >- (
740 metis_tac[CARDLEQ_FINITE,FINITE_CROSS] ) >>
741 metis_tac[CARD_MUL_ABSORB_LE,cardleq_lt_trans]
742QED
743
744Theorem CARD_MUL_LT_INFINITE:
745 !s t. s <</= t /\ t <</= u /\ INFINITE u ==> s CROSS t <</= u
746Proof
747 metis_tac[CARD_MUL_LT_LEMMA,cardleq_lteq]
748QED
749
750(* set exponentiation *)
751Definition set_exp_def:
752 set_exp A B = { f | (!b. b IN B ==> ?a. a IN A /\ (f b = a)) /\
753 !b. b NOTIN B ==> (f b = ARB) }
754End
755(* local: the datatype package needs this theory, so what it exports
756 reaches every theory, and ** is the exponent of the numbers, the
757 words and the rationals too *)
758Overload "**"[local] = “set_exp”
759
760Theorem exp_c :
761 !(s :'a set) (t :'b set).
762 s ** t =
763 {f | (!x. x IN t ==> f x IN s) /\ (!x. ~(x IN t) ==> f x = ARB)}
764Proof
765 rw [set_exp_def, Once EXTENSION]
766QED
767
768Theorem UNIV_fun_exp:
769 univ(:'a -> 'b) = univ(:'b) ** univ(:'a)
770Proof
771 simp[set_exp_def]
772QED
773
774(* |- univ(:'b) ** univ(:'a) = univ(:'a -> 'b) *)
775Theorem CARD_EXP_UNIV = GSYM UNIV_fun_exp
776
777Theorem BIJ_functions_agree:
778 !f g s t. BIJ f s t /\ (!x. x IN s ==> (f x = g x)) ==> BIJ g s t
779Proof
780 simp[BIJ_DEF, SURJ_DEF, INJ_DEF] >> rw[] >>
781 full_simp_tac (srw_ss() ++ boolSimps.CONJ_ss) []
782QED
783
784Theorem CARD_CARDEQ_I:
785 FINITE s1 /\ FINITE s2 /\ (CARD s1 = CARD s2) ==> s1 =~ s2
786Proof
787 Cases_on `FINITE s1` >> simp[] >> qid_spec_tac `s2` >> pop_assum mp_tac >>
788 qid_spec_tac `s1` >> ho_match_mp_tac FINITE_INDUCT >> simp[] >> conj_tac
789 >- metis_tac [CARD_EQ_0, cardeq_REFL, CARDEQ_0] >>
790 qx_gen_tac `s1` >> strip_tac >> qx_gen_tac `a` >> strip_tac >>
791 qx_gen_tac `s2` >>
792 ‘(s2 = {}) \/ ?b s. (s2 = b INSERT s) /\ b NOTIN s’
793 by metis_tac [SET_CASES] >>
794 csimp[] >> strip_tac >> `s1 =~ s` by metis_tac[] >>
795 `?f. BIJ f s1 s` by metis_tac [cardeq_def] >>
796 simp[cardeq_def] >> qexists_tac `\x. if x = a then b else f x` >>
797 simp[BIJ_INSERT] >>
798 `(b INSERT s) DELETE b = s` by (simp[EXTENSION] >> metis_tac[]) >>
799 match_mp_tac BIJ_functions_agree >> qexists_tac `f` >> rw[]
800QED
801
802Theorem CARDEQ_CARD_EQN:
803 FINITE s1 /\ FINITE s2 ==> (s1 =~ s2 <=> (CARD s1 = CARD s2))
804Proof
805 metis_tac [CARD_CARDEQ_I, CARDEQ_CARD]
806QED
807
808Theorem CARDLEQ_CARD:
809 FINITE s1 /\ FINITE s2 ==> (s1 <<= s2 <=> CARD s1 <= CARD s2)
810Proof
811 rw[EQ_IMP_THM] >-
812 metis_tac[cardleq_def,INJ_CARD] >>
813 Cases_on`CARD s1 = CARD s2` >-
814 metis_tac[cardleq_lteq,CARDEQ_CARD_EQN] >>
815 simp[Once cardleq_lteq] >> disj1_tac >>
816 simp[cardleq_def] >>
817 gen_tac >> match_mp_tac PHP >>
818 srw_tac[ARITH_ss][]
819QED
820
821Theorem CARD_LT_CARD:
822 FINITE s1 /\ FINITE s2 ==> (s1 <</= s2 <=> CARD s1 < CARD s2)
823Proof
824 rw[] >> simp[cardlt_lenoteq,CARDLEQ_CARD,CARDEQ_CARD_EQN, SF ARITH_ss]
825QED
826
827Theorem EMPTY_set_exp:
828 A ** {} = { K ARB } /\ (B <> {} ==> {} ** B = {})
829Proof
830 simp[set_exp_def] >> conj_tac >- simp[EXTENSION, FUN_EQ_THM] >>
831 strip_tac >> qsuff_tac `(!b. b NOTIN B) = F`
832 >- (disch_then SUBST_ALL_TAC >> simp[]) >>
833 gvs[EXTENSION] >> metis_tac[]
834QED
835
836Theorem EMPTY_set_exp_CARD:
837 A ** {} =~ count 1
838Proof
839 simp[EMPTY_set_exp, CARDEQ_CARD_EQN]
840QED
841
842Theorem SING_set_exp:
843 {x} ** B = { (\b. if b IN B then x else ARB) } /\
844 A ** {x} = { (\b. if b = x then a else ARB) | a IN A }
845Proof
846 rw[set_exp_def, EXTENSION] >> rw[FUN_EQ_THM, EQ_IMP_THM] >> rw[] >>
847 metis_tac[]
848QED
849
850Theorem SING_set_exp_CARD:
851 {x} ** B =~ count 1 /\ A ** {x} =~ A
852Proof
853 simp[SING_set_exp, CARDEQ_CARD_EQN] >> simp[Once cardeq_SYM] >>
854 simp[cardeq_def] >> qexists `\a b. if b = x then a else ARB` >>
855 qmatch_abbrev_tac `BIJ f A s` >>
856 qsuff_tac `s = IMAGE f A`
857 >- (rw[] >> match_mp_tac (GEN_ALL INJ_BIJ_SUBSET) >>
858 map_every qexists_tac [`IMAGE f A`, `A`] >> rw[INJ_DEF, Abbr`f`]
859 >- metis_tac[]
860 >> (gvs[FUN_EQ_THM] >> first_x_assum (qspec_then `x` mp_tac) >> simp[])) >>
861 rw[Abbr`s`, Abbr`f`, EXTENSION]
862QED
863
864Theorem POW_TWO_set_exp:
865 POW A =~ count 2 ** A
866Proof
867 simp[POW_DEF, set_exp_def, BIJ_IFF_INV, cardeq_def] >>
868 qexists_tac `\s a. if a IN A then if a IN s then 1 else 0
869 else ARB` >> simp[] >> conj_tac
870 >- (qx_gen_tac `s` >> strip_tac >> qx_gen_tac `b` >> strip_tac >>
871 Cases_on `b IN s` >> simp[]) >>
872 qexists `\f. { a | a IN A /\ f a = 1 }` >> simp[] >> rpt conj_tac
873 >- simp[SUBSET_DEF]
874 >- (qx_gen_tac `s` >> csimp[] >> simp[EXTENSION, SUBSET_DEF] >>
875 rw[] >> rw[]) >>
876 qx_gen_tac `f` >> simp[FUN_EQ_THM] >> strip_tac >> qx_gen_tac `a` >>
877 Cases_on `a IN A` >> simp[] >>
878 `?n. n < 2 /\ (f a = n)` by metis_tac[] >>
879 rw[] >> DECIDE_TAC
880QED
881
882Theorem set_exp_card_cong:
883 (a1:'a1 set) =~ (a2:'a2 set) ==> (b1:'b1 set) =~ (b2:'b2 set) ==>
884 (a1 ** b1 =~ a2 ** b2)
885Proof
886 rw[cardeq_def, BIJ_IFF_INV] >>
887 rename [‘_ IN a1 ** b1 ==> _ IN a2 ** b2’,
888 ‘_ IN a1 ==> rf1 _ IN a2’, ‘_ IN a2 ==> rf2 _ IN a1’,
889 ‘_ IN b1 ==> df1 _ IN b2’, ‘_ IN b2 ==> df2 _ IN b1’] >>
890 qexists ‘λf b. if b IN b2 then
891 if f (df2 b) IN a1 then rf1 $ f $ df2 b else ARB
892 else ARB’ >>
893 simp[set_exp_def, FUN_EQ_THM] >>
894 qexists ‘λg b. if b IN b1 then
895 if g (df1 b) IN a2 then rf2 $ g $ df1 b else ARB
896 else ARB’ >>
897 simp[] >> metis_tac[]
898QED
899
900Theorem set_exp_cardle_cong:
901 (b = {} ==> d = {}) ==>
902 (a:'a set) <<= (b:'b set) /\ (c:'c set) <<= (d:'d set) ==>
903 a ** c <<= b ** d
904Proof
905 simp[set_exp_def, cardleq_def] >> strip_tac >>
906 disch_then (CONJUNCTS_THEN2 (qx_choose_then `abf` assume_tac)
907 (qx_choose_then `cdf` assume_tac)) >>
908 qexists ‘
909 λcaf di. if di IN d then
910 case some ci. ci IN c /\ (cdf ci = di) of
911 NONE => CHOICE b
912 | SOME ci => abf (caf ci)
913 else ARB
914 ’ >>
915 Cases_on ‘b = {}’ >> gvs[]
916 >- simp[INJ_DEF, FUN_EQ_THM] >>
917 rw[INJ_DEF]
918 >- (rename [‘_ IN c /\ cdf _ = di’] >>
919 DEEP_INTRO_TAC some_intro >> simp[] >>
920 rpt strip_tac >- metis_tac[INJ_DEF] >>
921 simp[CHOICE_DEF]) >>
922 rename [‘caf1 = caf2’] >> simp[FUN_EQ_THM] >>
923 qx_gen_tac ‘ci’ >> Cases_on‘ci IN c’ >> simp[] >>
924 ‘cdf ci IN d’ by metis_tac[INJ_DEF] >>
925 ‘(some ci'. ci' IN c /\ (cdf ci' = cdf ci)) = SOME ci’
926 by (DEEP_INTRO_TAC some_intro >> simp[] >>
927 metis_tac[INJ_DEF]) >>
928 first_assum (fn th => Q_TAC (mp_tac o AP_THM th) ‘cdf ci’) >> BETA_TAC >>
929 simp[] >> metis_tac[INJ_DEF]
930QED
931
932Theorem exp_INSERT_cardeq:
933 e NOTIN s ==> (A ** (e INSERT s) =~ A CROSS A ** s)
934Proof
935 simp[set_exp_def, cardeq_def] >> strip_tac >> simp[BIJ_IFF_INV] >>
936 qexists_tac ‘\f. (f e, (λa. if a = e then ARB else f a))’ >> conj_tac
937 >- (qx_gen_tac `f` >> strip_tac >> simp[] >> metis_tac[]) >>
938 qexists ‘λ(a1,f) a2. if a2 = e then a1 else f a2’ >>
939 simp[pairTheory.FORALL_PROD] >> rpt conj_tac
940 >- (rw[] >> rw[])
941 >- (qx_gen_tac `f` >> strip_tac >> simp[FUN_EQ_THM] >> qx_gen_tac `a` >>
942 simp[AllCaseEqs()]) >>
943 rw[FUN_EQ_THM] >> rw[]
944QED
945
946Theorem exp_count_cardeq:
947 INFINITE A /\ 0 < n ==> A ** count n =~ A
948Proof
949 strip_tac >> Induct_on `n` >> simp[] >>
950 `(n = 0) \/ ?m. n = SUC m` by (Cases_on `n` >> simp[])
951 >- simp[COUNT_ONE, SING_set_exp_CARD] >>
952 simp_tac (srw_ss()) [COUNT_SUC] >>
953 `A ** (n INSERT count n) =~ A CROSS A ** count n`
954 by simp[exp_INSERT_cardeq] >>
955 `A ** count n =~ A` by simp[] >>
956 `A CROSS A ** count n =~ A CROSS A` by metis_tac[CARDEQ_CROSS, cardeq_REFL] >>
957 `A CROSS A =~ A` by simp[SET_SQUARED_CARDEQ_SET] >>
958 metis_tac [cardeq_TRANS]
959QED
960
961Theorem K_lemma[local]:
962 (!x. f x = y) <=> f = K y
963Proof
964 simp[FUN_EQ_THM]
965QED
966
967Theorem finite_image_lemma[local]:
968 !A. FINITE (IMAGE f A) /\ (!x y. x IN A /\ y IN A /\ f x = f y ==> x = y) ==>
969 FINITE A
970Proof
971 Induct_on ‘FINITE’ >> simp[] >> rw[] >>
972 rename [‘IMAGE f A = e0 INSERT A0’] >>
973 ‘?e. e IN A /\ f e = e0’
974 by (qpat_x_assum ‘IMAGE f A = _’ mp_tac >> simp[EXTENSION] >> metis_tac[])>>
975 ‘IMAGE f (A DELETE e) = A0’
976 by (qpat_x_assum ‘IMAGE f A = _’ mp_tac >> simp[EXTENSION] >> metis_tac[])>>
977 ‘FINITE (A DELETE e)’ suffices_by simp[] >>
978 first_x_assum irule >> simp[]
979QED
980
981Theorem FINITE_setexp[simp]:
982 FINITE ((A:'a set) ** (B:'b set)) <=>
983 B = {} \/ A <<= {()} \/ FINITE A /\ FINITE B
984Proof
985 simp[set_exp_def, EQ_IMP_THM] >> rpt strip_tac >> gvs[K_lemma]
986 >- (Cases_on ‘B = {}’ >> simp[] >>
987 Cases_on ‘A = {}’ >> gvs[] >>
988 Cases_on ‘?a. A = {a}’ >> gvs[]
989 >- (simp[cardleq_def] >> disj1_tac >> qexists_tac ‘K ()’ >>
990 simp[INJ_IFF]) >> disj2_tac >>
991 ‘?a1 a2. a1 <> a2 /\ a1 IN A /\ a2 IN A’
992 by (pop_assum mp_tac >> simp[EXTENSION] >> gs[GSYM MEMBER_NOT_EMPTY] >>
993 metis_tac[]) >> conj_tac
994 >- (CCONTR_TAC >>
995 qpat_x_assum ‘FINITE _’ mp_tac >> simp[] >>
996 ‘?b. b IN B’ by simp[MEMBER_NOT_EMPTY] >>
997 qabbrev_tac ‘ff = λa b. if b IN B then a else ARB’ >>
998 ‘(!a1 a2. ff a1 = ff a2 ==> a1 = a2)’
999 by (simp[Abbr‘ff’, FUN_EQ_THM, AllCaseEqs()] >> metis_tac[]) >>
1000 drule_then (drule_then assume_tac) IMAGE_11_INFINITE >>
1001 qmatch_abbrev_tac ‘INFINITE s’ >>
1002 ‘IMAGE ff A SUBSET s’ suffices_by metis_tac[SUBSET_FINITE] >>
1003 simp[Abbr‘ff’, Abbr‘s’, SUBSET_DEF, PULL_EXISTS]) >>
1004 CCONTR_TAC >> qpat_x_assum ‘FINITE _’ mp_tac >> simp[] >>
1005 qabbrev_tac ‘ff = λb1 b2. if b1 NOTIN B then ARB
1006 else if b2 NOTIN B then ARB
1007 else if b1 = b2 then a2 else a1’ >>
1008 ‘(!b1 b2. b1 IN B /\ b2 IN B /\ ff b1 = ff b2 ==> b1 = b2)’
1009 by (simp[Abbr‘ff’, FUN_EQ_THM, SF CONJ_ss] >>
1010 rpt strip_tac >> CCONTR_TAC >>
1011 first_x_assum $ qspec_then‘b1’ mp_tac >> simp[]) >>
1012 drule_at (Pos last) finite_image_lemma >> simp[] >> strip_tac >>
1013 qmatch_abbrev_tac ‘INFINITE s’ >>
1014 ‘IMAGE ff B SUBSET s’ suffices_by metis_tac[SUBSET_FINITE] >>
1015 first_x_assum $ qspecl_then [‘ARB : 'b’, ‘ARB : 'b’] kall_tac >>
1016 simp[Abbr‘ff’, Abbr‘s’, SUBSET_DEF, PULL_EXISTS, AllCaseEqs()] >>
1017 metis_tac[])
1018 >- (Cases_on ‘A = {}’ >> gvs[]
1019 >- (csimp[K_lemma] >> Cases_on ‘!b. b NOTIN B’ >> simp[]) >>
1020 ‘?a. A = {a}’
1021 by (gs[cardleq_def, INJ_IFF, GSYM MEMBER_NOT_EMPTY] >>
1022 rename [‘a IN A’] >> qexists_tac ‘a’ >> simp[EXTENSION] >>
1023 metis_tac[]) >>
1024 gvs[] >> qmatch_abbrev_tac ‘FINITE s’ >>
1025 ‘s = {λb. if b IN B then a else ARB}’ suffices_by simp[] >>
1026 simp[Abbr‘s’, Once FUN_EQ_THM, AllCaseEqs(), EQ_IMP_THM] >>
1027 rpt strip_tac >> csimp[FUN_EQ_THM, AllCaseEqs()])
1028 >- (‘FINITE (A CROSS B)’ by simp[] >>
1029 ‘FINITE (POW (A CROSS B))’ by simp[] >>
1030 first_assum $ C (resolve_then (Pos hd) irule) CARDLEQ_FINITE >>
1031 simp[INJ_IFF, cardleq_def, IN_POW, SUBSET_DEF, FORALL_PROD] >>
1032 qexists_tac ‘λf. { (a,b) | b IN B /\ f b = a }’ >>
1033 simp[] >> rw[] >~
1034 [‘GSPEC _ = GSPEC _ <=> _ = _’]
1035 >- (simp[EXTENSION] >> simp[FUN_EQ_THM, FORALL_PROD] >>
1036 simp[Once EQ_IMP_THM] >> rw[] >> rename [‘f1 a = f2 a’] >>
1037 metis_tac[]) >>
1038 metis_tac[])
1039QED
1040
1041Theorem CARD_LE_EXP:
1042 {T; F} <<= B ==> (A:'a set) <<= (B:'b set) ** A
1043Proof
1044 simp[cardleq_def, set_exp_def, INJ_IFF] >>
1045 disch_then $ qx_choose_then ‘bf’ strip_assume_tac >>
1046 qexists_tac ‘λa1 a2. if a1 = a2 then bf T
1047 else if a2 IN A then bf F
1048 else ARB’ >>
1049 simp[] >> rw[]
1050 >- rw[]
1051 >- metis_tac[] >>
1052 simp[EQ_IMP_THM] >>
1053 disch_then (assume_tac o SRULE[FUN_EQ_THM]) >>
1054 pop_assum $ qspec_then ‘x’ mp_tac >> simp[] >> rw[]
1055QED
1056
1057Theorem INFINITE_Unum:
1058 INFINITE A <=> univ(:num) <<= A
1059Proof
1060 simp[infinite_num_inj, cardleq_def]
1061QED
1062
1063Theorem cardleq_SURJ:
1064 A <<= B <=> (?f. SURJ f B A) \/ (A = {})
1065Proof
1066 simp[cardleq_def, EQ_IMP_THM] >>
1067 metis_tac [SURJ_INJ_INV, inj_surj, INJ_EMPTY]
1068QED
1069
1070Theorem INFINITE_cardleq_INSERT:
1071 INFINITE A ==> (x INSERT s <<= A <=> s <<= A)
1072Proof
1073 simp[cardleq_def, INJ_INSERT, EQ_IMP_THM] >> strip_tac >> conj_tac
1074 >- metis_tac[] >>
1075 disch_then (Q.X_CHOOSE_THEN `f` strip_assume_tac) >>
1076 Cases_on `x IN s` >- (qexists_tac `f` >> gvs[INJ_DEF]) >>
1077 Q.UNDISCH_THEN `INFINITE A` mp_tac >>
1078 simp[INFINITE_Unum, cardleq_def] >>
1079 disch_then (Q.X_CHOOSE_THEN `g` assume_tac) >>
1080 qexists_tac `\y. if y = x then g 0
1081 else case some n. f y = g n of
1082 NONE => f y
1083 | SOME m => g (m + 1)` >>
1084 rpt conj_tac
1085 >- (simp[INJ_DEF] >> conj_tac
1086 >- (qx_gen_tac `y` >> strip_tac >> rw[] >- gvs[] >>
1087 Cases_on `some n. f y = g n` >> gvs[INJ_DEF]) >>
1088 map_every qx_gen_tac [`i`, `j`] >> strip_tac >> Cases_on `i = x` >>
1089 Cases_on `j = x` >> simp[]
1090 >- (DEEP_INTRO_TAC some_intro >> simp[] >> gvs[INJ_DEF])
1091 >- (DEEP_INTRO_TAC some_intro >> simp[] >> gvs[INJ_DEF]) >>
1092 ntac 2 (DEEP_INTRO_TAC some_intro) >> simp[] >>
1093 gvs[INJ_DEF] >> qx_gen_tac `m` >> strip_tac >>
1094 qx_gen_tac `n` >> rpt strip_tac >>
1095 metis_tac [DECIDE ``(n + 1 = m + 1) <=> (m = n)``])
1096 >- gvs[INJ_DEF] >>
1097 qx_gen_tac `y` >> simp[] >> Cases_on `x = y` >> simp[] >>
1098 Cases_on `y IN s` >> simp[] >> DEEP_INTRO_TAC some_intro >>
1099 simp[] >> gvs[INJ_DEF] >> metis_tac [DECIDE ``0 <> n + 1``]
1100QED
1101
1102Theorem CARDEQ_CROSS_1:
1103 {x} CROSS A =~ A /\ A CROSS {x} =~ A
1104Proof
1105 simp[cardeq_def] >> conj_tac >| [qexists ‘SND’, qexists ‘FST’] >>
1106 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD]
1107QED
1108
1109fun qxchl qs thtac = case qs of [] => thtac
1110 | q::rest => Q.X_CHOOSE_THEN q (qxchl rest thtac)
1111
1112
1113Theorem disjoint_countable_decomposition:
1114 !s. INFINITE s ==>
1115 ?A. (BIGUNION A = s) /\
1116 (!a. a IN A ==> INFINITE a /\ countable a) /\
1117 !a1 a2. a1 IN A /\ a2 IN A /\ a1 <> a2 ==> DISJOINT a1 a2
1118Proof
1119 rpt strip_tac >>
1120 qabbrev_tac `
1121 Ds = { D | BIGUNION D SUBSET s /\
1122 (!d. d IN D ==> INFINITE d /\ countable d) /\
1123 !d1 d2. d1 IN D /\ d2 IN D /\ d1 <> d2 ==> DISJOINT d1 d2}` >>
1124 `?f. INJ f univ(:num) s` by metis_tac [infinite_num_inj] >>
1125 qabbrev_tac `s_nums = IMAGE f univ(:num)` >>
1126 `{s_nums} IN Ds`
1127 by (markerLib.WITHOUT_ABBREVS (simp[]) >> simp[Abbr`s_nums`] >>
1128 conj_tac >- (gvs[SUBSET_DEF, INJ_DEF] >> metis_tac[])>>
1129 gvs[FINITE_IMAGE_INJ', INJ_IFF]) >>
1130 `Ds <> {}` by (simp[EXTENSION] >>metis_tac[]) >>
1131 qabbrev_tac `R = {(D1,D2) | D1 IN Ds /\ D2 IN Ds /\ D1 SUBSET D2}` >>
1132 `partial_order R Ds`
1133 by (simp[Abbr`R`, partial_order_def, domain_def, range_def, reflexive_def,
1134 transitive_def, antisym_def] THEN REPEAT CONJ_TAC
1135 THENL [
1136 simp[SUBSET_DEF] >> metis_tac[],
1137 simp[SUBSET_DEF] >> metis_tac[],
1138 metis_tac[SUBSET_TRANS],
1139 metis_tac[SUBSET_ANTISYM]
1140 ]) >>
1141 `!t. chain t R ==> upper_bounds t R <> {}`
1142 by (simp[Abbr`R`, upper_bounds_def, chain_def] >>
1143 simp[Once EXTENSION, range_def] >>
1144 qx_gen_tac `t` >> strip_tac >>
1145 qabbrev_tac `UBD =BIGUNION t` >>
1146 qexists_tac `UBD` >>
1147 `UBD IN Ds`
1148 by (markerLib.WITHOUT_ABBREVS (simp[]) >>
1149 conj_tac
1150 >- (simp[BIGUNION_SUBSET, Abbr`UBD`] >>
1151 qx_gen_tac `s0` >>
1152 disch_then (qxchl [`t0`] strip_assume_tac) >>
1153 `t0 IN Ds` by metis_tac[] >> pop_assum mp_tac >>
1154 markerLib.WITHOUT_ABBREVS (simp[]) >>
1155 simp[BIGUNION_SUBSET]) >>
1156 conj_tac
1157 >- (qx_gen_tac `s0` >>
1158 disch_then (qxchl [`t0`] strip_assume_tac) >>
1159 `t0 IN Ds` by metis_tac[] >> pop_assum mp_tac >>
1160 markerLib.WITHOUT_ABBREVS (simp[])) >>
1161 map_every qx_gen_tac [`d1`, `d2`] >>
1162 disch_then (CONJUNCTS_THEN2
1163 (qxchl [`t1`] strip_assume_tac)
1164 (CONJUNCTS_THEN2
1165 (qxchl [`t2`] strip_assume_tac)
1166 assume_tac)) >>
1167 `t1 IN Ds /\ t2 IN Ds` by metis_tac[] >>
1168 ntac 2 (pop_assum mp_tac) >>
1169 markerLib.WITHOUT_ABBREVS (simp[]) >>
1170 simp[BIGUNION_SUBSET] >>
1171 `t1 SUBSET t2 \/ t2 SUBSET t1` suffices_by
1172 metis_tac[SUBSET_DEF] >>
1173 metis_tac[]) >>
1174 simp[] >> conj_tac >- (qexists_tac `UBD` >> simp[]) >>
1175 qx_gen_tac `t0` >> Cases_on `t0 IN t` >> simp[] >>
1176 `t0 IN Ds` by metis_tac[] >> simp[] >>
1177 pop_assum mp_tac >> markerLib.WITHOUT_ABBREVS (simp[]) >>
1178 simp[Abbr`UBD`, BIGUNION_SUBSET] >> strip_tac >>
1179 simp[SUBSET_DEF] >> metis_tac[]) >>
1180 `?M. M IN maximal_elements Ds R` by metis_tac [zorns_lemma] >>
1181 pop_assum mp_tac >> simp[maximal_elements_def] >> strip_tac >>
1182 Q.UNDISCH_THEN `M IN Ds` (fn th => mp_tac th >> assume_tac th) >>
1183 markerLib.WITHOUT_ABBREVS (simp_tac (srw_ss()) []) >> strip_tac >>
1184 Cases_on `BIGUNION M = s` >- metis_tac[] >>
1185 `M <> {}`
1186 by (strip_tac >>
1187 `(M,{s_nums}) IN R` by (simp[Abbr`R`] >> gvs[]) >>
1188 `M = {s_nums}` by metis_tac[] >> gvs[]) >>
1189 Cases_on `FINITE (s DIFF BIGUNION M)`
1190 >- (`?M0. M0 IN M` by metis_tac [IN_INSERT, SET_CASES] >>
1191 qexists_tac `(M0 UNION (s DIFF BIGUNION M)) INSERT (M DELETE M0)` >>
1192 dsimp[finite_countable] >> rpt strip_tac >| [
1193 simp[Once EXTENSION] >> qx_gen_tac `e` >> eq_tac
1194 >- (strip_tac >> gvs[BIGUNION_SUBSET] >>
1195 metis_tac [SUBSET_DEF]) >>
1196 simp[] >> Cases_on `e IN M0` >> simp[] >>
1197 Cases_on `e IN BIGUNION M` >> pop_assum mp_tac >> simp[] >>
1198 metis_tac[],
1199 `a2 SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1200 simp[DISJOINT_DEF, EXTENSION] >> qx_gen_tac `e` >>
1201 Cases_on `e IN s` >> simp[] >> Cases_on `e IN a2` >> simp[] >>
1202 `e IN BIGUNION M` by metis_tac[SUBSET_DEF] >>
1203 gvs[] >> metis_tac[],
1204 `a1 SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1205 simp[DISJOINT_DEF, EXTENSION] >> qx_gen_tac `e` >>
1206 Cases_on `e IN s` >> simp[] >> Cases_on `e IN a1` >> simp[] >>
1207 `e IN BIGUNION M` by metis_tac[SUBSET_DEF] >>
1208 gvs[] >> metis_tac[]
1209 ]) >>
1210 qabbrev_tac `M0 = s DIFF BIGUNION M` >>
1211 `?g. INJ g univ(:num) M0` by metis_tac[infinite_num_inj] >>
1212 qabbrev_tac`g_nums = IMAGE g univ(:num)` >>
1213 `INFINITE g_nums /\ countable g_nums`
1214 by (simp[Abbr`g_nums`] >> gvs[FINITE_IMAGE_INJ', INJ_IFF]) >>
1215 qabbrev_tac `M' = g_nums INSERT M` >>
1216 `g_nums SUBSET M0` by (simp[Abbr`g_nums`, SUBSET_DEF] >>
1217 full_simp_tac(srw_ss() ++ DNF_ss)[INJ_DEF]) >>
1218 `M' IN Ds`
1219 by (markerLib.WITHOUT_ABBREVS(simp[]) >> dsimp[] >>
1220 `M0 SUBSET s` by simp[Abbr`M0`] >>
1221 `g_nums SUBSET s` by metis_tac[SUBSET_TRANS] >> simp[] >>
1222 qmatch_abbrev_tac `PP /\ QQ` >>
1223 `PP` suffices_by metis_tac[DISJOINT_SYM] >>
1224 map_every markerLib.UNABBREV_TAC ["PP", "QQ"] >>
1225 qx_gen_tac `d2` >> strip_tac >> simp[DISJOINT_DEF, EXTENSION] >>
1226 qx_gen_tac `e` >> SPOSE_NOT_THEN STRIP_ASSUME_TAC >>
1227 `e IN M0 /\ e IN BIGUNION M` by metis_tac[IN_BIGUNION, SUBSET_DEF] >>
1228 metis_tac[IN_DIFF]) >>
1229 `(M,M') IN R` by simp[Abbr`R`, Abbr`M'`, SUBSET_DEF] >>
1230 `M = M'` by metis_tac[] >>
1231 `g_nums NOTIN M` suffices_by metis_tac[IN_INSERT] >> strip_tac >>
1232 `g_nums SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1233 `g 0 IN g_nums` by simp[Abbr`g_nums`] >>
1234 metis_tac[IN_DIFF, SUBSET_DEF]
1235QED
1236
1237(* this proof inspired by one generated by DeepSeek in early January, 2025;
1238 original query was
1239 "prove that every infinite set can be partitioned into sets that are
1240 countably infinite"
1241
1242 natural language proof was pretty good, though it wanted to first well-
1243 order the infinite set (s), which is unnecessary given that you separately
1244 establish the bijection with s CROSS univ(:num).
1245
1246 I then asked it to render the proof in HOL4, which it did something along
1247 the lines of below. It invented plenty of theorem names. I've retained its
1248 comments. It's less than half the size of the one above that explicitly
1249 uses Zorn's Lemma.
1250*)
1251Theorem disjoint_countable_decomposition2:
1252 !s. INFINITE s ==>
1253 ?A. (BIGUNION A = s) /\
1254 (!a. a IN A ==> INFINITE a /\ countable a) /\
1255 pairwise (RC DISJOINT) A
1256Proof
1257 rpt strip_tac >>
1258
1259 (* Step 1: Establish cardinal equivalence |A| = |A × ℕ| *)
1260 ‘s =~ s CROSS univ(:num)’ by (
1261 irule cardleq_ANTISYM >> conj_tac >~
1262 [‘s <<= s CROSS univ(:num)’]
1263 >- (simp[cardleq_def] >> qexists_tac ‘\a. (a,0)’ >>
1264 simp[INJ_DEF]) >>
1265 ‘s CROSS univ(:num) <<= univ(:num) CROSS s’
1266 by (simp[cardleq_def] >> qexists_tac ‘λ(a,b). (b,a)’ >>
1267 simp[INJ_DEF, FORALL_PROD]) >>
1268 drule_then irule cardleq_TRANS >>
1269 irule CARD_MUL_ABSORB_LE >>
1270 metis_tac[INFINITE_Unum]
1271 ) >>
1272
1273 (* Step 2: Construct bijection *)
1274 qabbrev_tac ‘f = @f. BIJ f s (s CROSS univ(:num))’ >>
1275 ‘BIJ f s (s CROSS UNIV)’ by (
1276 simp[Abbr‘f’] >> SELECT_ELIM_TAC >>
1277 metis_tac[cardeq_def]
1278 ) >>
1279
1280 (* Step 3: Define partition as fibers *)
1281 qabbrev_tac ‘P = IMAGE (\a. {b | b IN s /\ ?n. f b = (a,n)}) s’ >>
1282
1283 (* Verification *)
1284 ‘BIGUNION P = s’ by (
1285 simp[Abbr`P`, Once EXTENSION, PULL_EXISTS, FORALL_PROD, EQ_IMP_THM] >>
1286 gvs[BIJ_DEF, FORALL_PROD, INJ_IFF, SURJ_DEF] >>
1287 metis_tac[pair_CASES, FST, PAIR]
1288 ) >>
1289 ‘pairwise (RC DISJOINT) P’ by (
1290 simp[Abbr‘P’, pairwise_def, PULL_EXISTS, relationTheory.RC_DEF] >>
1291 rw[] >> CCONTR_TAC >> gvs[DISJOINT_DEF, GSYM MEMBER_NOT_EMPTY]
1292 ) >>
1293 ‘!X. X IN P ==> INFINITE X /\ countable X’ by (
1294 simp[Abbr`P`] >> rw[] >~
1295 [‘INFINITE { b | b IN s /\ ?n. f b = (a,n) }(* g *)’]
1296 >- (
1297 drule_then (qx_choose_then ‘g’ strip_assume_tac) BIJ_INV >>
1298 gvs[FORALL_PROD] >>
1299 simp[infinite_num_inj] >> qexists_tac ‘λn. g (a,n)’ >>
1300 simp[INJ_DEF] >> gvs[BIJ_DEF, INJ_IFF]
1301 ) >>
1302 simp[countable_def] >> qexists_tac ‘SND o f’ >>
1303 gvs[INJ_IFF, BIJ_DEF, PULL_EXISTS, EQ_IMP_THM, SF CONJ_ss]
1304 ) >>
1305 metis_tac[]
1306QED
1307
1308Theorem count_cardle[simp]:
1309 count n <<= A <=> (FINITE A ==> n <= CARD A)
1310Proof
1311 simp[cardleq_def] >> Cases_on ‘FINITE A’ >> simp[]
1312 >- (eq_tac
1313 >- metis_tac[DECIDE “x:num <= y <=> ~(y < x)”, PHP, CARD_COUNT,
1314 FINITE_COUNT] >>
1315 metis_tac[FINITE_COUNT, CARDLEQ_CARD, cardleq_def, CARD_COUNT]) >>
1316 pop_assum mp_tac >> qid_spec_tac ‘A’ >> Induct_on ‘n’ >>
1317 simp[] >> rpt strip_tac >> simp[COUNT_SUC, INJ_INSERT] >>
1318 first_x_assum (drule_then strip_assume_tac) >>
1319 ‘?a. a IN A /\ !m. m < n ==> f m <> a’
1320 by (‘?a. a IN (A DIFF IMAGE f (count n))’
1321 suffices_by (simp[] >> metis_tac[]) >>
1322 irule INFINITE_INHAB >>
1323 metis_tac [IMAGE_FINITE, FINITE_COUNT, FINITE_DIFF_down]) >>
1324 qexists_tac ‘\m. if m < n then f m else a’ >> simp[] >> conj_tac
1325 >- gvs[INJ_DEF] >>
1326 rw[]
1327QED
1328
1329Theorem CANTOR[simp]:
1330 A <</= POW A
1331Proof
1332 strip_tac >> gvs[cardleq_def, INJ_IFF, IN_POW] >>
1333 qabbrev_tac ‘CS = {f s | s | s SUBSET A /\ f s NOTIN s}’ >>
1334 ‘!s. s IN CS <=> ?t. t SUBSET A /\ f t NOTIN t /\ (f t = s)’
1335 by (simp[Abbr`CS`] >> metis_tac[]) >>
1336 ‘CS SUBSET A’ by (simp[Abbr`CS`] >> ONCE_REWRITE_TAC[SUBSET_DEF] >>
1337 simp[PULL_EXISTS]) >>
1338 irule (DECIDE “(p ==> ~p) /\ (~p ==> p) ==> Q”) >>
1339 qexists_tac ‘f CS IN CS’ >> conj_tac >> strip_tac >>
1340 qpat_x_assum ‘!s. s IN CS <=> P’ (fn th => REWRITE_TAC [th]) >>
1341 csimp[] >> simp[] >> metis_tac[]
1342QED
1343
1344Theorem cardlt_cardle:
1345 A <</= B ==> A <<= B
1346Proof
1347 metis_tac[cardlt_lenoteq]
1348QED
1349
1350Theorem set_exp_product:
1351 (A ** B1) ** B2 =~ A ** (B1 CROSS B2)
1352Proof
1353 simp[cardeq_def] >>
1354 qexists ‘\cf bp. if bp IN B1 CROSS B2 then cf (SND bp) (FST bp) else ARB’ >>
1355 simp[BIJ_DEF, INJ_IFF, SURJ_DEF, set_exp_def, FORALL_PROD] >>
1356 rpt strip_tac >> simp[]
1357 >- (simp[FUN_EQ_THM, FORALL_PROD] >> iff_tac >> simp[] >> metis_tac[]) >>
1358 rename [‘uf (_,_) IN A’] >>
1359 qexists ‘\b2. if b2 IN B2 then
1360 \b1. if b1 IN B1 then uf(b1,b2) else ARB
1361 else ARB’ >> simp[] >>
1362 simp[FUN_EQ_THM, FORALL_PROD] >> metis_tac[]
1363QED
1364
1365Theorem CARD1_SING:
1366 (A:'a set) =~ {()} <=> ?a. A = {a}
1367Proof
1368 simp[cardeq_def, EQ_IMP_THM, PULL_EXISTS, BIJ_IFF_INV] >>
1369 rpt strip_tac
1370 >- (rename [‘g () IN A’] >> qexists_tac ‘g()’ >> simp[EXTENSION] >>
1371 metis_tac[]) >>
1372 qexists_tac ‘K a’ >> simp[]
1373QED
1374
1375Theorem cardleq_setexp:
1376 x <<= x ** e <=> x = {} \/ x =~ {()} \/ e <> {}
1377Proof
1378 Cases_on ‘x = {}’ >> simp[] >>
1379 Cases_on ‘e = {}’ >> simp[EMPTY_set_exp, CARD1_SING]
1380 >- (simp[INJ_IFF, EQ_IMP_THM, PULL_EXISTS] >> reverse (rpt strip_tac)
1381 >- (simp[INJ_IFF, cardleq_def] >> qexists_tac ‘λa. K ARB’ >> simp[]) >>
1382 gs[cardleq_def, INJ_IFF, GSYM MEMBER_NOT_EMPTY] >> simp[EXTENSION] >>
1383 metis_tac[]) >>
1384 simp[cardleq_def, INJ_IFF] >> gs[GSYM MEMBER_NOT_EMPTY] >>
1385 rename [‘X ** E’, ‘x IN X’, ‘e IN E’] >>
1386 qexists ‘λx0 e0. if e0 IN E then x0 else ARB’ >>
1387 simp[set_exp_def, FUN_EQ_THM] >> metis_tac[]
1388QED
1389
1390Theorem POW_EQ_X_EXP_X:
1391 INFINITE A ==> POW A =~ A ** A
1392Proof
1393 strip_tac >> irule cardleq_ANTISYM >> conj_tac
1394 >- (‘POW A =~ count 2 ** A’ by simp[POW_TWO_set_exp] >>
1395 ‘count 2 ** A <<= A ** A’
1396 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1397 irule set_exp_cardle_cong >> simp[]) >>
1398 ‘POW A =~ count 2 ** A’ by simp[POW_TWO_set_exp] >>
1399 ‘A ** A <<= count 2 ** A’
1400 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1401 ‘A <</= POW A’ by simp[] >>
1402 ‘A <<= POW A’ by simp[cardlt_cardle] >>
1403 ‘A ** A <<= POW A ** A’
1404 by metis_tac[set_exp_cardle_cong, cardleq_REFL, POW_EMPTY] >>
1405 ‘POW A ** A <<= count 2 ** A’ suffices_by metis_tac [cardleq_TRANS] >>
1406 ‘(count 2 ** A) ** A <<= count 2 ** A’
1407 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL, set_exp_card_cong] >>
1408 ‘count 2 ** (A CROSS A) <<= count 2 ** A’
1409 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL, set_exp_product] >>
1410 irule set_exp_cardle_cong >> simp[] >> irule CARDEQ_SUBSET_CARDLEQ >>
1411 simp[SET_SQUARED_CARDEQ_SET]
1412QED
1413
1414Theorem setexp_eq_EMPTY[simp]:
1415 A ** B = {} <=> A = {} /\ B <> {}
1416Proof
1417 simp[set_exp_def] >> simp[SimpLHS, EXTENSION] >>
1418 simp[] >> eq_tac >> rpt strip_tac
1419 >- (Cases_on ‘B = {}’ >> gvs[]
1420 >- (pop_assum $ qspec_then ‘K ARB’ mp_tac >> simp[]) >>
1421 CCONTR_TAC >> gs[GSYM MEMBER_NOT_EMPTY] >>
1422 rename [‘_ IN B /\ _ NOTIN A’, ‘b IN B’, ‘a IN A’] >>
1423 first_x_assum $ qspec_then ‘λb0. if b0 IN B then a else ARB’ mp_tac>>
1424 csimp[] >> metis_tac[])
1425 >- (gvs[] >> pop_assum $ qspec_then ‘K ARB’ mp_tac >> simp[]) >>
1426 simp[] >> metis_tac[MEMBER_NOT_EMPTY]
1427QED
1428
1429Theorem FINITE_EXPONENT_SETEXP_UNCOUNTABLE:
1430 FINITE B /\ B <> {} /\ ~countable A ==>
1431 ~countable (A ** B)
1432Proof
1433 Induct_on ‘FINITE’ >> simp[] >> rpt strip_tac >>
1434 rename [‘A ** (e INSERT B) ’] >>
1435 ‘A ** (e INSERT B) =~ A CROSS (A ** B)’
1436 by simp[exp_INSERT_cardeq] >>
1437 drule_all (iffLR countable_cardeq) >> simp[cross_countable_IFF] >>
1438 rpt strip_tac >> gvs[CARDEQ_0, setexp_eq_EMPTY]
1439QED
1440
1441Theorem FINITE_EXPONENT_SETEXP_COUNTABLE:
1442 FINITE (B:'b set) ==>
1443 (countable ((A:'a set) ** B) <=> B = {} \/ countable A)
1444Proof
1445 simp[EQ_IMP_THM, IMP_CONJ_THM] >> conj_tac
1446 >- metis_tac[FINITE_EXPONENT_SETEXP_UNCOUNTABLE] >>
1447 ‘!(A:'a set) (B:'b set). FINITE B /\ countable A ==> countable (A ** B)’
1448 suffices_by (rw[] >> simp[EMPTY_set_exp]) >>
1449 Induct_on ‘FINITE’ >> simp[EMPTY_set_exp] >> rpt strip_tac >>
1450 ‘A ** (e INSERT B) =~ A CROSS (A ** B)’ by simp[exp_INSERT_cardeq] >>
1451 drule_then irule (iffRL countable_cardeq) >> simp[cross_countable_IFF]
1452QED
1453
1454Theorem FINITE_012:
1455 FINITE A ==> A = {} \/ A =~ {()} \/ 2 <= CARD A
1456Proof
1457 Induct_on ‘FINITE’ >> simp[] >> rw[] >> gvs[CARD1_SING, SF ARITH_ss]
1458QED
1459
1460(* cf. permutesTheory.permutes_alt_bijns *)
1461Definition bijns_def:
1462 bijns A = { f | BIJ f A A /\ !a. a NOTIN A ==> f a = a }
1463End
1464
1465Theorem bijns_alt_permutes:
1466 !f s. f IN bijns s <=> f permutes s
1467Proof
1468 simp[permutes_alt, bijns_def]
1469QED
1470
1471Theorem cardeq_bijns_cong:
1472 A =~ B ==> bijns A =~ bijns B
1473Proof
1474 strip_tac >> ONCE_REWRITE_TAC [cardeq_SYM] >>
1475 gvs[cardeq_def, bijns_def] >>
1476 RULE_ASSUM_TAC (REWRITE_RULE [BIJ_IFF_INV]) >> gvs[] >>
1477 qexists ‘\bf a. if a IN A then g (bf (f a)) else a’ >>
1478 ‘!a1 a2. a1 IN A /\ a2 IN A ==> (f a1 = f a2 <=> a1 = a2)’ by metis_tac[] >>
1479 ‘!b1 b2. b1 IN B /\ b2 IN B ==> (g b1 = g b2 <=> b1 = b2)’ by metis_tac[] >>
1480 simp[BIJ_DEF, INJ_IFF, SURJ_DEF] >> rpt strip_tac >> csimp[]
1481 >- metis_tac[]
1482 >- (simp[EQ_IMP_THM, FUN_EQ_THM] >> rw[] >>
1483 rename [‘bf1 b = bf2 b’] >> reverse (Cases_on ‘b IN B’) >> simp[] >>
1484 ‘b = f (g b)’ by metis_tac[] >> pop_assum SUBST1_TAC >>
1485 ‘g b IN A’ by metis_tac[] >> first_x_assum (qspec_then ‘g b’ mp_tac) >>
1486 simp[])
1487 >- metis_tac[]
1488 >- (simp[PULL_EXISTS] >> csimp[] >>
1489 rename [‘(ff:'a -> 'a) _ = ff _ <=> _’] >>
1490 qexists ‘\b. if b IN B then f (ff (g b)) else b’ >>
1491 simp[] >> rpt strip_tac >> csimp[] >> metis_tac[] >>
1492 simp[FUN_EQ_THM] >> metis_tac[])
1493QED
1494
1495Theorem bijections_cardeq:
1496 INFINITE s ==> bijns s =~ POW s
1497Proof
1498 strip_tac >>
1499 irule cardleq_ANTISYM >> conj_tac
1500 >- (‘POW s =~ s ** s’ by simp[POW_EQ_X_EXP_X] >>
1501 ‘bijns s <<= s ** s’ suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1502 simp[cardleq_def] >>
1503 simp[bijns_def, BIJ_DEF, INJ_IFF, set_exp_def] >>
1504 qexists ‘λf x. if x IN s then f x else ARB’ >> simp[] >>
1505 rpt strip_tac >> simp[FUN_EQ_THM] >> metis_tac[]) >>
1506 ‘s =~ {T;F} CROSS s’ by simp[SET_SUM_CARDEQ_SET] >>
1507 ‘bijns s =~ bijns ({T;F} CROSS s)’ by metis_tac[cardeq_bijns_cong] >>
1508 ‘POW s <<= bijns ({T;F} CROSS s)’
1509 suffices_by metis_tac[CARDEQ_CARDLEQ,cardeq_REFL] >>
1510 simp[cardleq_def] >>
1511 qexists_tac ‘\ss (bool,a). if a IN s then if a IN ss then (bool,a)
1512 else (~bool,a)
1513 else (bool,a)’ >>
1514 simp[INJ_IFF, IN_POW, bijns_def, FORALL_PROD] >> rpt strip_tac
1515 >- (simp[BIJ_DEF, INJ_IFF, SURJ_DEF, FORALL_PROD] >> rpt strip_tac
1516 >- rw[]
1517 >- (rw[] >> metis_tac[])
1518 >- rw[] >>
1519 simp[pairTheory.EXISTS_PROD] >> csimp[] >>
1520 dsimp[AllCaseEqs()] >> metis_tac[]) >>
1521 simp[SimpLHS,FUN_EQ_THM] >> iff_tac >> rw[] >>
1522 simp[EXTENSION] >> qx_gen_tac `a` >> reverse (Cases_on `a IN s`)
1523 >- metis_tac[SUBSET_DEF] >>
1524 rename [‘a IN ss1 <=> a IN ss2’] >>
1525 Cases_on `a IN ss1` >> simp[]
1526 >- (first_x_assum (qspecl_then [‘T’, ‘a’] mp_tac) >> simp[] >> rw[])
1527 >- (first_x_assum (qspecl_then [‘F’, ‘a’] mp_tac) >> simp[] >> rw[])
1528QED
1529
1530(* ------------------------------------------------------------------------- *)
1531(* misc. *)
1532(* ------------------------------------------------------------------------- *)
1533
1534Theorem FORALL_IN_GSPEC :
1535 (!P f. (!z. z IN {f x | P x} ==> Q z) <=> (!x. P x ==> Q(f x))) /\
1536 (!P f. (!z. z IN {f x y | P x y} ==> Q z) <=>
1537 (!x y. P x y ==> Q(f x y))) /\
1538 (!P f. (!z. z IN {f w x y | P w x y} ==> Q z) <=>
1539 (!w x y. P w x y ==> Q(f w x y)))
1540Proof
1541 SRW_TAC [][] THEN SET_TAC []
1542QED
1543
1544Theorem EXISTS_IN_GSPEC :
1545 (!P f. (?z. z IN {f x | P x} /\ Q z) <=> (?x. P x /\ Q(f x))) /\
1546 (!P f. (?z. z IN {f x y | P x y} /\ Q z) <=>
1547 (?x y. P x y /\ Q(f x y))) /\
1548 (!P f. (?z. z IN {f w x y | P w x y} /\ Q z) <=>
1549 (?w x y. P w x y /\ Q(f w x y)))
1550Proof
1551 SRW_TAC [][] THEN SET_TAC []
1552QED
1553
1554Theorem LEFT_IMP_EXISTS_THM:
1555 !P Q. (?x. P x) ==> Q <=> (!x. P x ==> Q)
1556Proof
1557 SIMP_TAC std_ss [PULL_EXISTS]
1558QED
1559
1560Theorem LEFT_IMP_FORALL_THM:
1561 !P Q. (!x. P x) ==> Q <=> (?x. P x ==> Q)
1562Proof
1563 METIS_TAC [GSYM LEFT_FORALL_IMP_THM]
1564QED
1565
1566Theorem RIGHT_IMP_EXISTS_THM:
1567 !P Q. P ==> (?x. Q x) <=> (?x. P ==> Q x)
1568Proof
1569 REWRITE_TAC [GSYM RIGHT_EXISTS_IMP_THM]
1570QED
1571
1572Theorem RIGHT_IMP_FORALL_THM:
1573 !P Q. P ==> (!x. Q x) <=> (!x. P ==> Q x)
1574Proof
1575 REWRITE_TAC [GSYM RIGHT_FORALL_IMP_THM]
1576QED
1577
1578(* old name IMP_CONJ seems to be a conv function *)
1579Theorem CONJ_EQ_IMP :
1580 !p q r. p /\ q ==> r <=> p ==> q ==> r
1581Proof
1582 REWRITE_TAC [AND_IMP_INTRO]
1583QED
1584
1585Theorem IMP_CONJ_ALT :
1586 !p q r. p /\ q ==> r <=> q ==> p ==> r
1587Proof
1588 METIS_TAC [AND_IMP_INTRO]
1589QED
1590
1591Theorem lemma[local]:
1592 (!x. x IN s ==> (g(f(x)) = x)) <=>
1593 (!y x. x IN s /\ (y = f x) ==> (g y = x))
1594Proof
1595 MESON_TAC []
1596QED
1597
1598Theorem INJECTIVE_ON_LEFT_INVERSE:
1599 !f s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) <=>
1600 (?g. !x. x IN s ==> (g(f(x)) = x))
1601Proof
1602 REWRITE_TAC[lemma] THEN SIMP_TAC std_ss [GSYM SKOLEM_THM] THEN METIS_TAC[]
1603QED
1604
1605Theorem SURJECTIVE_ON_RIGHT_INVERSE:
1606 !f t. (!y. y IN t ==> ?x. x IN s /\ (f(x) = y)) <=>
1607 (?g. !y. y IN t ==> g(y) IN s /\ (f(g(y)) = y))
1608Proof
1609 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM]
1610QED
1611
1612Theorem SURJECTIVE_RIGHT_INVERSE:
1613 (!y. ?x. f(x) = y) <=> (?g. !y. f(g(y)) = y)
1614Proof
1615 MESON_TAC[SURJECTIVE_ON_RIGHT_INVERSE, IN_UNIV]
1616QED
1617
1618Theorem FINITE_IMAGE_INJ_GENERAL:
1619 !(f:'a->'b) A s.
1620 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
1621 FINITE A
1622 ==> (FINITE {x | x IN s /\ f(x) IN A})
1623Proof
1624 REPEAT STRIP_TAC THEN
1625 FULL_SIMP_TAC std_ss [INJECTIVE_ON_LEFT_INVERSE] THEN ASSUME_TAC SUBSET_FINITE
1626 THEN POP_ASSUM (MP_TAC o Q.SPEC `IMAGE (g:'b->'a) A`) THEN
1627 KNOW_TAC ``FINITE (IMAGE g A)`` THENL [METIS_TAC [IMAGE_FINITE], DISCH_TAC
1628 THEN FULL_SIMP_TAC std_ss [] THEN DISCH_TAC THEN
1629 POP_ASSUM (MP_TAC o Q.SPEC `{x | x IN s /\ f x IN A}`) THEN DISCH_TAC
1630 THEN KNOW_TAC ``{x | x IN s /\ f x IN A} SUBSET IMAGE g A`` THENL
1631 [REWRITE_TAC [IMAGE_DEF, SUBSET_DEF] THEN GEN_TAC THEN
1632 SIMP_TAC std_ss [GSPECIFICATION] THEN METIS_TAC [] , METIS_TAC []]]
1633QED
1634
1635Theorem FINITE_IMAGE_INJ:
1636 !(f:'a->'b) A. (!x y. (f(x) = f(y)) ==> (x = y)) /\
1637 FINITE A ==> FINITE {x | f(x) IN A}
1638Proof
1639 REPEAT GEN_TAC THEN
1640 MP_TAC(SPECL [``f:'a->'b``, ``A:'b->bool``, ``UNIV:'a->bool``]
1641 FINITE_IMAGE_INJ_GENERAL) THEN REWRITE_TAC[IN_UNIV]
1642QED
1643
1644Theorem INFINITE_IMAGE_INJ:
1645 !f:'a->'b. (!x y. (f x = f y) ==> (x = y)) ==>
1646 !s. INFINITE s ==> INFINITE(IMAGE f s)
1647Proof
1648 metis_tac[FINITE_IMAGE_INJ_EQ]
1649QED
1650
1651Theorem INFINITE_NONEMPTY:
1652 !s. INFINITE(s) ==> ~(s = EMPTY)
1653Proof MESON_TAC[FINITE_EMPTY]
1654QED
1655
1656Theorem SURJECTIVE_IMAGE_THM:
1657 !f:'a->'b. (!y. ?x. f x = y) <=> (!P. IMAGE f {x | P(f x)} = {x | P x})
1658Proof
1659 GEN_TAC THEN SIMP_TAC std_ss [EXTENSION, IN_IMAGE, GSPECIFICATION] THEN
1660 EQ_TAC THENL [ALL_TAC, DISCH_THEN(MP_TAC o SPEC ``\y:'b. T``)] THEN
1661 METIS_TAC[]
1662QED
1663
1664Theorem SURJECTIVE_ON_IMAGE:
1665 !f:'a->'b u v.
1666 (!t. t SUBSET v ==> ?s. s SUBSET u /\ (IMAGE f s = t)) <=>
1667 (!y. y IN v ==> ?x. x IN u /\ (f x = y))
1668Proof
1669 REPEAT GEN_TAC THEN EQ_TAC THENL
1670 [DISCH_TAC THEN X_GEN_TAC ``y:'b`` THEN DISCH_TAC THEN
1671 FIRST_X_ASSUM(MP_TAC o SPEC ``{y:'b}``) THEN ASM_SET_TAC[],
1672 DISCH_TAC THEN X_GEN_TAC ``t:'b->bool`` THEN DISCH_TAC THEN
1673 EXISTS_TAC ``{x | x IN u /\ (f:'a->'b) x IN t}`` THEN ASM_SET_TAC[]]
1674QED
1675
1676Theorem SURJECTIVE_IMAGE:
1677 !f:'a->'b. (!t. ?s. IMAGE f s = t) <=> (!y. ?x. f x = y)
1678Proof
1679 GEN_TAC THEN
1680 MP_TAC (ISPECL [``f:'a->'b``,``univ(:'a)``,``univ(:'b)``] SURJECTIVE_ON_IMAGE) THEN
1681 SIMP_TAC std_ss [IN_UNIV, SUBSET_UNIV]
1682QED
1683
1684Theorem CARD_LE_INJ:
1685 !s t.
1686 FINITE s /\ FINITE t /\ CARD s <= CARD t ==>
1687 ?f:'a->'b. (IMAGE f s) SUBSET t /\
1688 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)
1689Proof
1690 rpt strip_tac >> drule_all (iffRL CARDLEQ_CARD) >>
1691 simp[cardleq_def, INJ_IFF, PULL_EXISTS] >> qx_gen_tac ‘f’ >> strip_tac >>
1692 qexists ‘f’ >> csimp[SUBSET_DEF, PULL_EXISTS]
1693QED
1694
1695Theorem CARD_EQ_BIJECTION:
1696 !s t. FINITE s /\ FINITE t /\ (CARD s = CARD t)
1697 ==> ?f:'a->'b. (!x. x IN s ==> f(x) IN t) /\
1698 (!y. y IN t ==> ?x. x IN s /\ (f x = y)) /\
1699 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)
1700Proof
1701 MP_TAC CARD_LE_INJ THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
1702 POP_ASSUM (MP_TAC o SPECL [``s:'a->bool``,``t:'b->bool``]) THEN
1703 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN
1704 ASM_REWRITE_TAC[LESS_EQ_REFL] THEN DISCH_THEN (X_CHOOSE_TAC ``f:'a->'b``) THEN
1705 EXISTS_TAC ``f:'a->'b`` THEN POP_ASSUM MP_TAC THEN
1706 ASM_SIMP_TAC std_ss [SURJECTIVE_IFF_INJECTIVE_GEN] THEN
1707 MESON_TAC[SUBSET_DEF, IN_IMAGE]
1708QED
1709
1710Theorem CARD_EQ_BIJECTIONS:
1711 !s t. FINITE s /\ FINITE t /\ (CARD s = CARD t)
1712 ==> ?f:'a->'b g. (!x. x IN s ==> f(x) IN t /\ (g(f x) = x)) /\
1713 (!y. y IN t ==> g(y) IN s /\ (f(g y) = y))
1714Proof
1715 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CARD_EQ_BIJECTION) THEN
1716 DISCH_THEN (X_CHOOSE_TAC ``f:'a->'b``) THEN
1717 EXISTS_TAC ``f:'a->'b`` THEN POP_ASSUM MP_TAC THEN
1718 SIMP_TAC std_ss [SURJECTIVE_ON_RIGHT_INVERSE] THEN
1719 SIMP_TAC std_ss [GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM] THEN
1720 METIS_TAC[]
1721QED
1722
1723Theorem SING_SUBSET:
1724 !s x. {x} SUBSET s <=> x IN s
1725Proof
1726 SET_TAC[]
1727QED
1728
1729Theorem INJECTIVE_ON_IMAGE:
1730 !f:'a->'b u. (!s t. s SUBSET u /\ t SUBSET u /\
1731 (IMAGE f s = IMAGE f t) ==> (s = t)) <=>
1732 (!x y. x IN u /\ y IN u /\ (f x = f y) ==> (x = y))
1733Proof
1734 REPEAT GEN_TAC THEN EQ_TAC THENL
1735 [DISCH_TAC, SET_TAC[]] THEN MAP_EVERY X_GEN_TAC [``x:'a``, ``y:'a``] THEN
1736 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [``{x:'a}``, ``{y:'a}``]) THEN
1737 ASM_REWRITE_TAC[SING_SUBSET, IMAGE_EMPTY, IMAGE_INSERT] THEN SET_TAC[]
1738QED
1739
1740Theorem INJECTIVE_IMAGE:
1741 !f:'a->'b. (!s t. (IMAGE f s = IMAGE f t) ==> (s = t)) <=>
1742 (!x y. (f x = f y) ==> (x = y))
1743Proof
1744 GEN_TAC THEN MP_TAC(ISPECL [``f:'a->'b``, ``univ(:'a)``] INJECTIVE_ON_IMAGE) THEN
1745 REWRITE_TAC[IN_UNIV, SUBSET_UNIV]
1746QED
1747
1748Theorem FINITE_FINITE_BIGUNION[local]:
1749 !s. FINITE(s) ==> (FINITE(BIGUNION s) <=> (!t. t IN s ==> FINITE(t)))
1750Proof
1751 metis_tac[FINITE_BIGUNION_EQ]
1752QED
1753
1754(* ------------------------------------------------------------------------- *)
1755(* This is often more useful as a rewrite. *)
1756(* ------------------------------------------------------------------------- *)
1757
1758val lemma = SET_RULE ``!a s. a IN s ==> (s = a INSERT (s DELETE a))``;
1759
1760Theorem HAS_SIZE_CLAUSES:
1761 !s. (s HAS_SIZE 0 <=> (s = {})) /\
1762 (s HAS_SIZE (SUC n) <=>
1763 ?a t. t HAS_SIZE n /\ ~(a IN t) /\ (s = a INSERT t))
1764Proof
1765 REWRITE_TAC[HAS_SIZE_0] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL
1766 [REWRITE_TAC[HAS_SIZE_SUC, GSYM MEMBER_NOT_EMPTY] THEN
1767 MESON_TAC[lemma, IN_DELETE],
1768 SIMP_TAC std_ss [LEFT_IMP_EXISTS_THM, HAS_SIZE, CARD_EMPTY, CARD_INSERT,
1769 FINITE_INSERT]]
1770QED
1771
1772Theorem CARD_SUBSET_EQ:
1773 !(a:'a->bool) b. FINITE b /\ a SUBSET b /\ (CARD a = CARD b) ==> (a = b)
1774Proof
1775 REPEAT STRIP_TAC THEN
1776 MP_TAC(SPECL [``a:'a->bool``] CARD_UNION) THEN
1777 SUBGOAL_THEN ``FINITE(a:'a->bool)`` ASSUME_TAC THENL
1778 [METIS_TAC[SUBSET_FINITE_I], ALL_TAC] THEN ASM_REWRITE_TAC [] THEN
1779 DISCH_THEN (MP_TAC o SPEC ``b DIFF (a:'a->bool)``) THEN
1780 SUBGOAL_THEN ``FINITE(b:'a->bool DIFF a)`` ASSUME_TAC THENL
1781 [MATCH_MP_TAC SUBSET_FINITE_I THEN EXISTS_TAC ``b:'a->bool`` THEN
1782 ASM_REWRITE_TAC[] THEN SET_TAC[], ALL_TAC] THEN
1783 SUBGOAL_THEN ``a:'a->bool INTER (b DIFF a) = EMPTY`` ASSUME_TAC THENL
1784 [SET_TAC[], ALL_TAC] THEN
1785 ASM_REWRITE_TAC[] THEN
1786 SUBGOAL_THEN ``a UNION (b:'a->bool DIFF a) = b`` ASSUME_TAC THENL
1787 [UNDISCH_TAC ``a:'a->bool SUBSET b`` THEN SET_TAC[], ALL_TAC] THEN
1788 ASM_REWRITE_TAC[] THEN
1789 REWRITE_TAC[ARITH_PROVE ``(a = a + b) <=> (b = 0:num)``] THEN DISCH_TAC THEN
1790 SUBGOAL_THEN ``b:'a->bool DIFF a = EMPTY`` MP_TAC THENL
1791 [REWRITE_TAC[GSYM HAS_SIZE_0] THEN
1792 FULL_SIMP_TAC std_ss [HAS_SIZE, CARD_EMPTY],
1793 UNDISCH_TAC ``a:'a->bool SUBSET b`` THEN SET_TAC[]]
1794QED
1795
1796Theorem CARD_BIGUNION_LE:
1797 !s t:'a->'b->bool m n.
1798 s HAS_SIZE m /\ (!x. x IN s ==> FINITE(t x) /\ CARD(t x) <= n) ==>
1799 CARD(BIGUNION {t(x) | x IN s}) <= m * n
1800Proof
1801 REWRITE_TAC[HAS_SIZE] >> Induct_on ‘FINITE’ >> simp[] >>
1802 REPEAT GEN_TAC >> STRIP_TAC >>
1803 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] >>
1804 rw[DISJ_IMP_THM, FORALL_AND_THM,
1805 SET_RULE “BIGUNION {t x | x = a \/ x IN s} =
1806 t(a) UNION BIGUNION {t x | x IN s}”] >>
1807 MATCH_MP_TAC LESS_EQ_TRANS >>
1808 EXISTS_TAC
1809 “CARD((t:'a->'b->bool) e) + CARD(BIGUNION {(t:'a->'b->bool) x | x IN s})” >>
1810 CONJ_TAC >| [
1811 MATCH_MP_TAC CARD_UNION_LE >> simp[PULL_EXISTS] >>
1812 REWRITE_TAC[SET_RULE ``{t x | x IN s} = IMAGE t s``] >> simp[],
1813 simp[ADD1, RIGHT_ADD_DISTRIB] >> first_x_assum drule >> DECIDE_TAC
1814 ]
1815QED
1816
1817(* ----------------------------------------------------------------------
1818 Cardinality of type bool
1819 ---------------------------------------------------------------------- *)
1820
1821(* simplifier gets all of these because it turns univ(:bool) into {T;F} *)
1822
1823Theorem HAS_SIZE_BOOL: univ(:bool) HAS_SIZE 2
1824Proof simp[HAS_SIZE]
1825QED
1826
1827Theorem CARD_BOOL[simp]:
1828 CARD univ(:bool) = 2
1829Proof simp[]
1830QED
1831
1832Theorem FINITE_BOOL[simp]: FINITE univ(:bool)
1833Proof simp[]
1834QED
1835
1836(* NOTE: This theorem has been moved to pred_setTheory with a different name *)
1837Theorem INFINITE_DIFF_FINITE = INFINITE_DIFF_FINITE'
1838
1839(* ------------------------------------------------------------------------- *)
1840(* misc. *)
1841(* ------------------------------------------------------------------------- *)
1842
1843Theorem INJECTIVE_LEFT_INVERSE:
1844 (!x y. (f x = f y) ==> (x = y)) <=> (?g. !x. g(f(x)) = x)
1845Proof
1846 metis_tac[INJECTIVE_ON_LEFT_INVERSE, IN_UNIV]
1847QED
1848
1849Theorem INTER_ACI:
1850 !p q. (p INTER q = q INTER p) /\
1851 ((p INTER q) INTER r = p INTER q INTER r) /\
1852 (p INTER q INTER r = q INTER p INTER r) /\
1853 (p INTER p = p) /\
1854 (p INTER p INTER q = p INTER q)
1855Proof
1856 SET_TAC[]
1857QED
1858
1859Theorem UNION_ACI:
1860 !p q. (p UNION q = q UNION p) /\
1861 ((p UNION q) UNION r = p UNION q UNION r) /\
1862 (p UNION q UNION r = q UNION p UNION r) /\
1863 (p UNION p = p) /\
1864 (p UNION p UNION q = p UNION q)
1865Proof
1866 SET_TAC[]
1867QED
1868
1869(* ------------------------------------------------------------------------- *)
1870(* Now bijectivity. *)
1871(* ------------------------------------------------------------------------- *)
1872
1873Theorem BIJECTIVE_INJECTIVE_SURJECTIVE:
1874 !f s t. (!x. x IN s ==> f(x) IN t) /\
1875 (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
1876 (!x. x IN s ==> f(x) IN t) /\
1877 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
1878 (!y. y IN t ==> ?x. x IN s /\ (f x = y))
1879Proof
1880 MESON_TAC[]
1881QED
1882
1883Theorem BIJECTIVE_INVERSES:
1884 !f s t. (!x. x IN s ==> f(x) IN t) /\
1885 (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
1886 (!x. x IN s ==> f(x) IN t) /\
1887 ?g. (!y. y IN t ==> g(y) IN s) /\
1888 (!y. y IN t ==> (f(g(y)) = y)) /\
1889 (!x. x IN s ==> (g(f(x)) = x))
1890Proof
1891 NTAC 3 GEN_TAC THEN
1892 REWRITE_TAC[BIJECTIVE_INJECTIVE_SURJECTIVE,
1893 INJECTIVE_ON_LEFT_INVERSE,
1894 SURJECTIVE_ON_RIGHT_INVERSE] THEN
1895 MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
1896 DISCH_TAC THEN SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM] THEN
1897 AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN METIS_TAC[]
1898QED
1899
1900(* ------------------------------------------------------------------------- *)
1901(* Cardinal comparisons (in HOL-light's notations) *)
1902(* ------------------------------------------------------------------------- *)
1903
1904val _ = temp_set_fixity "<=_c" (Infix(NONASSOC, 450)); (* for cardleq *)
1905Overload "<=_c"[local] = ``cardleq``
1906Overload "<<="[local] = ``$<=_c``(* defined in pred_setTheory *)
1907
1908val _ = temp_set_fixity "<_c" (Infix(NONASSOC, 450)); (* for cardlt *)
1909Overload "<_c"[local] = ``cardlt``
1910Overload "<</="[local] = ``$<_c``
1911
1912val _ = temp_set_fixity ">=_c" (Infix(NONASSOC, 450)); (* for cardgeq *)
1913val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227D, tmnm = ">=_c"};
1914val _ = temp_TeX_notation {hol = ">=_c", TeX = ("\\ensuremath{\\succcurlyeq}", 1)};
1915val _ = temp_TeX_notation {hol = UTF8.chr 0x227D, TeX = ("\\ensuremath{\\succcurlyeq}", 1)};
1916
1917val _ = temp_set_fixity ">_c" (Infix(NONASSOC, 450)); (* for cardgt *)
1918val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227B, tmnm = ">_c"};
1919val _ = temp_TeX_notation {hol = ">_c", TeX = ("\\ensuremath{\\succ}", 1)};
1920val _ = temp_TeX_notation {hol = UTF8.chr 0x227B, TeX = ("\\ensuremath{\\succ}", 1)};
1921
1922val _ = temp_set_fixity "=_c" (Infix(NONASSOC, 450)); (* for cardeq *)
1923Overload "=_c"[local] = ``cardeq``
1924Overload "=~"[local] = ``$=_c``
1925
1926Theorem le_c:
1927 !s t. s <=_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
1928 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y))
1929Proof
1930 rpt GEN_TAC
1931 >> REWRITE_TAC [cardleq_def, INJ_DEF]
1932 >> PROVE_TAC []
1933QED
1934
1935Theorem lt_c:
1936 !s t. s <_c t <=> s <=_c t /\ ~(t <=_c s)
1937Proof
1938 rpt GEN_TAC
1939 >> EQ_TAC >> STRIP_TAC
1940 >> PROVE_TAC [cardlt_lenoteq]
1941QED
1942
1943Theorem eq_c:
1944 !s t. s =_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
1945 !y. y IN t ==> ?!x. x IN s /\ (f x = y)
1946Proof
1947 rpt GEN_TAC
1948 >> REWRITE_TAC [cardeq_def, BIJ_ALT, IN_FUNSET]
1949 >> `!f x y. (f x = y) = (y = f x)` by PROVE_TAC [EQ_SYM]
1950 >> ASM_REWRITE_TAC []
1951QED
1952
1953Definition cardgeq_def:
1954 cardgeq s t = cardleq t s
1955End
1956
1957Overload ">=_c"[local] = ``cardgeq``
1958Theorem ge_c = cardgeq_def;
1959
1960Definition cardgt_def:
1961 cardgt s t = cardlt t s
1962End
1963
1964Overload ">_c"[local] = ``cardgt``
1965Theorem gt_c = cardgt_def;
1966
1967Theorem LE_C:
1968 !s t. s <=_c t <=> ?g. !x. x IN s ==> ?y. y IN t /\ (g y = x)
1969Proof
1970 SIMP_TAC std_ss [le_c, INJECTIVE_ON_LEFT_INVERSE, SURJECTIVE_ON_RIGHT_INVERSE,
1971 GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM, GSYM RIGHT_EXISTS_AND_THM] THEN
1972 MESON_TAC[]
1973QED
1974
1975Theorem GE_C:
1976 !s t. s >=_c t <=> ?f. !y. y IN t ==> ?x. x IN s /\ (y = f x)
1977Proof
1978 REWRITE_TAC[ge_c, LE_C] THEN MESON_TAC[]
1979QED
1980
1981Theorem COUNTABLE: !t. COUNTABLE t <=> univ(:num) >=_c t
1982Proof
1983 REWRITE_TAC [countable_def, cardgeq_def, cardleq_def]
1984QED
1985
1986(* ------------------------------------------------------------------------- *)
1987(* Relational variant of =_c is sometimes useful. *)
1988(* ------------------------------------------------------------------------- *)
1989
1990Theorem EQ_C_BIJECTIONS :
1991 !(s :'a -> bool) (t :'b -> bool).
1992 s =_c t <=> ?f g. (!x. x IN s ==> f x IN t /\ g(f x) = x) /\
1993 (!y. y IN t ==> g y IN s /\ f(g y) = y)
1994Proof
1995 REPEAT GEN_TAC THEN SIMP_TAC std_ss [eq_c] THEN
1996 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
1997 Q.X_GEN_TAC ‘f’ THEN SIMP_TAC std_ss [] THEN
1998 EQ_TAC THENL [STRIP_TAC, MESON_TAC[]] THEN
1999 Q.EXISTS_TAC `(\y. @x. x IN s /\ f x = y)` THEN
2000(* HOL-Light's ASM_MESON_TAC seems more powerful than HOL4's:
2001 ASM_MESON_TAC[]
2002 *)
2003 rw [] >> SELECT_ELIM_TAC \\
2004 gvs [EXISTS_UNIQUE_DEF]
2005QED
2006
2007Theorem EQ_C:
2008 !s t. s =_c t <=>
2009 ?R:'a#'b->bool. (!x y. R(x,y) ==> x IN s /\ y IN t) /\
2010 (!x. x IN s ==> ?!y. y IN t /\ R(x,y)) /\
2011 (!y. y IN t ==> ?!x. x IN s /\ R(x,y))
2012Proof
2013 rpt GEN_TAC THEN
2014 REWRITE_TAC[eq_c] THEN EQ_TAC THENL
2015 [DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2016 EXISTS_TAC ``\(x:'a,y:'b). x IN s /\ y IN t /\ (y = f x)`` THEN
2017 SIMP_TAC std_ss [] THEN ASM_MESON_TAC[],
2018 METIS_TAC []]
2019QED
2020
2021(* ------------------------------------------------------------------------- *)
2022(* The "easy" ordering properties. *)
2023(* ------------------------------------------------------------------------- *)
2024
2025(* HOL Light aliases/names *)
2026Theorem CARD_EQ_REFL = cardeq_REFL
2027Theorem CARD_EQ_SYM = cardeq_SYM
2028Theorem CARD_EQ_TRANS = cardeq_TRANS
2029Theorem CARD_EQ_EMPTY = cj 1 CARDEQ_0
2030Theorem CARD_EQ_CARD = CARDEQ_CARD_EQN |> Q.GENL [‘s1’, ‘s2’]
2031Theorem CARD_EQ_IMP_LE = CARDEQ_SUBSET_CARDLEQ
2032
2033Theorem CARD_LE_REFL = cardleq_REFL
2034Theorem CARD_LE_TRANS = cardleq_TRANS
2035Theorem CARD_LE_ANTISYM = cardleq_ANTISYM_IFF
2036Theorem CARD_LT_REFL = cardlt_REFL
2037Theorem CARD_LET_TRANS = cardleq_lt_trans
2038Theorem CARD_LTE_TRANS = cardlt_leq_trans
2039Theorem CARD_LT_TRANS = cardlt_TRANS
2040Theorem CARD_LE_EMPTY = cardleq_empty
2041
2042Theorem CARD_LE_TOTAL = cardleq_dichotomy
2043Theorem CARD_LE_LT = cardleq_lteq
2044Theorem CARD_LE_CONG = CARDEQ_CARDLEQ
2045Theorem CARD_LE_SUBSET = SUBSET_CARDLEQ
2046
2047
2048Theorem CARD_LT_IMP_LE:
2049 !s t. s <_c t ==> s <=_c t
2050Proof
2051 ONCE_REWRITE_TAC [lt_c]
2052 THEN SIMP_TAC std_ss []
2053QED
2054
2055Theorem CARD_LE_RELATIONAL:
2056 !(R:'a->'b->bool) s.
2057 (!x y y'. x IN s /\ R x y /\ R x y' ==> (y = y')) ==>
2058 {y | ?x. x IN s /\ R x y} <=_c s
2059Proof
2060 rpt strip_tac >> REWRITE_TAC[le_c] >>
2061 qexists ‘\y:'b. @x:'a. x IN s /\ R x y’ >> simp[] >>
2062 METIS_TAC[]
2063QED
2064
2065(* ------------------------------------------------------------------------- *)
2066(* Other variants like "trichotomy of cardinals" now follow easily. *)
2067(* ------------------------------------------------------------------------- *)
2068
2069Theorem CARD_LET_TOTAL:
2070 !s:'a->bool t:'b->bool. s <=_c t \/ t <_c s
2071Proof
2072 REWRITE_TAC [EXCLUDED_MIDDLE]
2073QED
2074
2075Theorem CARD_LTE_TOTAL:
2076 !s:'a->bool t:'b->bool. s <_c t \/ t <=_c s
2077Proof
2078 MESON_TAC[]
2079QED
2080
2081Theorem CARD_LT_TOTAL:
2082 !s:'a->bool t:'b->bool. (s =_c t) \/ s <_c t \/ t <_c s
2083Proof
2084 MESON_TAC[cardleq_lteq]
2085QED
2086
2087(* this is an instance of reflexivity *)
2088Theorem CARD_NOT_LE:
2089 !s:'a->bool t:'b->bool. ~(s <=_c t) <=> t <_c s
2090Proof
2091 REWRITE_TAC []
2092QED
2093
2094(* ¬¬p = p *)
2095Theorem CARD_NOT_LT:
2096 !s:'a->bool t:'b->bool. ~(s <_c t) <=> t <=_c s
2097Proof
2098 REWRITE_TAC []
2099QED
2100
2101Theorem CARD_LT_LE:
2102 !s t. s <_c t <=> s <=_c t /\ ~(s =_c t)
2103Proof
2104 REWRITE_TAC[Once lt_c, GSYM CARD_LE_ANTISYM] THEN TAUT_TAC
2105QED
2106
2107
2108Theorem CARD_LT_CONG:
2109 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2110 s =_c s' /\ t =_c t' ==> (s <_c t <=> s' <_c t')
2111Proof
2112 REPEAT STRIP_TAC THEN
2113 AP_TERM_TAC THEN MATCH_MP_TAC CARD_LE_CONG THEN
2114 ASM_REWRITE_TAC[]
2115QED
2116
2117Theorem CARD_12[simp]:
2118 {()} <</= {T;F} /\ ~({()} =~ {T;F}) /\ ~({T;F} =~ {()}) /\ {()} <<= {T;F}
2119Proof
2120 conj_asm1_tac
2121 >- (simp[cardleq_def, INJ_IFF] >> qexistsl_tac [‘T’, ‘F’] >> simp[]) >>
2122 metis_tac[CARD_LT_CONG, CARD_LT_REFL, cardeq_REFL, cardleq_lteq]
2123QED
2124
2125
2126Theorem CARD_EQ_CONG:
2127 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2128 s =_c s' /\ t =_c t' ==> (s =_c t <=> s' =_c t')
2129Proof
2130 METIS_TAC[CARD_EQ_TRANS, CARD_EQ_SYM]
2131QED
2132
2133(* ------------------------------------------------------------------------- *)
2134(* Finiteness and infiniteness in terms of cardinality of N. *)
2135(* ------------------------------------------------------------------------- *)
2136
2137Theorem INFINITE_CARD_LE[local] = INFINITE_Unum
2138
2139Theorem FINITE_CARD_LT:
2140 !s:'a->bool. FINITE s <=> s <_c (UNIV:num->bool)
2141Proof
2142 ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
2143 REWRITE_TAC [Once (GSYM CARD_NOT_LT), INFINITE_CARD_LE]
2144QED
2145
2146
2147Theorem CARD_LE_UNIV:
2148 !s:'a->bool. s <=_c univ(:'a)
2149Proof
2150 GEN_TAC THEN MATCH_MP_TAC CARD_LE_SUBSET THEN REWRITE_TAC[SUBSET_UNIV]
2151QED
2152
2153Theorem CARD_LE_EQ_SUBSET:
2154 !s:'a->bool t:'b->bool. s <=_c t <=> ?u. u SUBSET t /\ (s =_c u)
2155Proof
2156 REPEAT GEN_TAC THEN EQ_TAC THENL
2157 [ALL_TAC,
2158 REPEAT STRIP_TAC THEN
2159 FIRST_ASSUM(MP_TAC o MATCH_MP CARD_LE_SUBSET) THEN
2160 MATCH_MP_TAC(TAUT `(a <=> b) ==> b ==> a`) THEN
2161 MATCH_MP_TAC CARD_LE_CONG THEN
2162 ASM_REWRITE_TAC[CARD_LE_CONG, CARD_EQ_REFL]] THEN
2163 REWRITE_TAC[le_c, eq_c] THEN
2164 DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2165 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM] THEN EXISTS_TAC ``IMAGE (f:'a->'b) s`` THEN
2166 EXISTS_TAC ``f:'a->'b`` THEN REWRITE_TAC[IN_IMAGE, SUBSET_DEF] THEN
2167 ASM_MESON_TAC[]
2168QED
2169
2170Theorem CARD_INFINITE_CONG:
2171 !s:'a->bool t:'b->bool. s =_c t ==> (INFINITE s <=> INFINITE t)
2172Proof
2173 REWRITE_TAC[INFINITE_CARD_LE] THEN REPEAT STRIP_TAC THEN
2174 MATCH_MP_TAC CARD_LE_CONG THEN ASM_SIMP_TAC std_ss [CARD_EQ_REFL]
2175QED
2176
2177Theorem CARD_FINITE_CONG:
2178 !s:'a->bool t:'b->bool. s =_c t ==> (FINITE s <=> FINITE t)
2179Proof
2180 ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
2181 SIMP_TAC std_ss [CARD_INFINITE_CONG]
2182QED
2183
2184Theorem CARD_LE_FINITE:
2185 !s:'a->bool t:'b->bool. FINITE t /\ s <=_c t ==> FINITE s
2186Proof
2187 ASM_MESON_TAC[CARD_LE_EQ_SUBSET, SUBSET_FINITE_I, CARD_FINITE_CONG]
2188QED
2189
2190Theorem CARD_EQ_FINITE:
2191 !s t:'a->bool. FINITE t /\ s =_c t ==> FINITE s
2192Proof
2193 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_FINITE]
2194QED
2195
2196Theorem CARD_LE_INFINITE:
2197 !s:'a->bool t:'b->bool. INFINITE s /\ s <=_c t ==> INFINITE t
2198Proof
2199 MESON_TAC[CARD_LE_FINITE]
2200QED
2201
2202Theorem CARD_LT_FINITE_INFINITE:
2203 !s:'a->bool t:'b->bool. FINITE s /\ INFINITE t ==> s <_c t
2204Proof
2205 ONCE_REWRITE_TAC[GSYM CARD_NOT_LE] THEN MESON_TAC[CARD_LE_FINITE]
2206QED
2207
2208Theorem CARD_LE_CARD_IMP:
2209 !s:'a->bool t:'b->bool. FINITE t /\ s <=_c t ==> CARD s <= CARD t
2210Proof
2211 REPEAT STRIP_TAC THEN
2212 SUBGOAL_THEN ``FINITE(s:'a->bool)`` ASSUME_TAC THENL
2213 [ASM_MESON_TAC[CARD_LE_FINITE], ALL_TAC] THEN
2214 UNDISCH_TAC ``s <=_c t`` THEN DISCH_TAC THEN
2215 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [le_c]) THEN
2216 DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2217 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ``CARD(IMAGE (f:'a->'b) s)`` THEN
2218 CONJ_TAC THENL
2219 [MATCH_MP_TAC(ARITH_PROVE ``(m = n:num) ==> n <= m``) THEN
2220 MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[],
2221 KNOW_TAC ``(IMAGE (f :'a -> 'b) (s :'a -> bool)) SUBSET (t :'b -> bool)`` THENL
2222 [ASM_MESON_TAC[SUBSET_DEF, IN_IMAGE], ALL_TAC] THEN
2223 MATCH_MP_TAC (CARD_SUBSET) THEN ASM_REWRITE_TAC[]]
2224QED
2225
2226Theorem CARD_EQ_CARD_IMP:
2227 !s:'a->bool t:'b->bool. FINITE t /\ s =_c t ==> (CARD s = CARD t)
2228Proof
2229 METIS_TAC[CARD_FINITE_CONG, ARITH_PROVE ``m <= n /\ n <= m <=> (m = n:num)``,
2230 CARD_LE_ANTISYM, CARD_LE_CARD_IMP]
2231QED
2232
2233Theorem CARD_LE_CARD:
2234 !s:'a->bool t:'b->bool.
2235 FINITE s /\ FINITE t ==> (s <=_c t <=> CARD s <= CARD t)
2236Proof
2237 REPEAT STRIP_TAC THEN
2238 MATCH_MP_TAC(TAUT ‘(a ==> b) /\ (~a ==> ~b) ==> (a <=> b)’) THEN
2239 ASM_SIMP_TAC std_ss [CARD_LE_CARD_IMP] THEN
2240 REWRITE_TAC[NOT_LESS_EQUAL] THEN REWRITE_TAC[Once lt_c, LT_LE] THEN
2241 ASM_SIMP_TAC std_ss [CARD_LE_CARD_IMP] THEN
2242 MATCH_MP_TAC(TAUT ‘(c ==> a ==> b) ==> a /\ ~b ==> ~c’) THEN
2243 DISCH_TAC THEN simp[CARD_LE_EQ_SUBSET, SimpL “$==>”] THEN
2244 DISCH_THEN(qx_choose_then ‘u’ STRIP_ASSUME_TAC) THEN
2245 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2246 ‘u = s’ suffices_by ASM_MESON_TAC[CARD_EQ_SYM] THEN
2247 METIS_TAC[CARD_SUBSET_EQ, CARD_EQ_CARD_IMP, CARD_EQ_SYM]
2248QED
2249
2250
2251Theorem CARD_HAS_SIZE_CONG:
2252 !s:'a->bool t:'b->bool n. s HAS_SIZE n /\ s =_c t ==> t HAS_SIZE n
2253Proof
2254 REWRITE_TAC[HAS_SIZE] THEN
2255 MESON_TAC[CARD_EQ_CARD, CARD_FINITE_CONG]
2256QED
2257
2258Theorem CARD_LE_IMAGE = IMAGE_cardleq
2259
2260Theorem CARD_LE_IMAGE_GEN:
2261 !f:'a->'b s t. t SUBSET IMAGE f s ==> t <=_c s
2262Proof
2263 REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_LE_TRANS THEN
2264 EXISTS_TAC ``IMAGE (f:'a->'b) s`` THEN
2265 ASM_SIMP_TAC std_ss [CARD_LE_IMAGE, CARD_LE_SUBSET]
2266QED
2267
2268Theorem CARD_EQ_IMAGE:
2269 !f:'a->'b s.
2270 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
2271 ==> (IMAGE f s =_c s)
2272Proof
2273 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN
2274 REWRITE_TAC[eq_c] THEN EXISTS_TAC ``f:'a->'b`` THEN ASM_SET_TAC[]
2275QED
2276
2277(* ------------------------------------------------------------------------- *)
2278(* Cardinal arithmetic operations. *)
2279(* ------------------------------------------------------------------------- *)
2280
2281val add_c = disjUNION_def
2282
2283val _ = set_mapped_fixity {tok = "+_c", fixity = Infixl 500,
2284 term_name = "disjUNION"}
2285val _ = set_mapped_fixity {fixity = Infixl 500,
2286 term_name = "disjUNION",
2287 tok = UTF8.chr 0x2294}
2288
2289Overload "+"[local,inferior] = “disjUNION”;
2290
2291val _ = temp_set_fixity "*_c" (Infixl 600);
2292Overload "*_c"[local,inferior] = “pred_set$CROSS”;
2293
2294Theorem mul_c:
2295 !s t. s *_c t = {(x,y) | x IN s /\ y IN t}
2296Proof
2297 simp[EXTENSION, FORALL_PROD]
2298QED
2299
2300(* ------------------------------------------------------------------------- *)
2301(* Congruence properties for the arithmetic operators. *)
2302(* ------------------------------------------------------------------------- *)
2303
2304Theorem CARD_LE_ADD:
2305 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2306 s <=_c s' /\ t <=_c t' ==> s + t <=_c s' + t'
2307Proof
2308 rpt gen_tac >> simp[le_c, add_c, FORALL_SUM] >>
2309 DISCH_THEN(CONJUNCTS_THEN2
2310 (X_CHOOSE_THEN “f:'a->'b” STRIP_ASSUME_TAC)
2311 (X_CHOOSE_THEN “g:'c->'d” STRIP_ASSUME_TAC)) >>
2312 qexists ‘λs. case s of INL a => INL (f a) | INR b => INR (g b)’ >>
2313 simp[]
2314QED
2315
2316Theorem CARD_LE_MUL = CARDLEQ_CROSS_CONG
2317
2318Theorem CARD_ADD_CONG:
2319 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2320 s =_c s' /\ t =_c t' ==> (s +_c t) =_c (s' +_c t')
2321Proof
2322 SIMP_TAC std_ss [CARD_LE_ADD, GSYM CARD_LE_ANTISYM]
2323QED
2324
2325Theorem CARD_MUL_CONG = CARDEQ_CROSS
2326
2327(* ------------------------------------------------------------------------- *)
2328(* Misc lemmas. *)
2329(* ------------------------------------------------------------------------- *)
2330
2331Theorem IN_CARD_ADD = IN_disjUNION
2332
2333Theorem IN_CARD_MUL: !s t x y. (x,y) IN (s *_c t) <=> x IN s /\ y IN t
2334Proof simp[]
2335QED
2336
2337Theorem CARD_LE_SQUARE:
2338 !s:'a->bool. s <=_c (s *_c s)
2339Proof
2340 simp[le_c] >> gen_tac >> qexists ‘λx. (x,x)’ >> simp[]
2341QED
2342
2343Theorem CARD_SQUARE_NUM:
2344 univ(:num) *_c univ(:num) =_c univ(:num)
2345Proof
2346 simp[cardeq_def] >> metis_tac[NUM_2D_BIJ_INV, BIJ_INV]
2347QED
2348
2349Theorem UNION_LE_ADD_C:
2350 !s t:'a->bool. s UNION t <=_c s + t
2351Proof
2352 rw[le_c] >> qexists ‘λx. if x IN s then INL x else INR x’ >> rw[]
2353QED
2354
2355Theorem CARD_DISJOINT_UNION:
2356 !s t.
2357 FINITE s /\ FINITE t /\ s INTER t = {} ==>
2358 CARD (s UNION t) = CARD s + CARD t
2359Proof
2360 simp[CARD_UNION_EQN]
2361QED
2362
2363Theorem CARD_ADD_C = CARD_disjUNION
2364
2365(* ------------------------------------------------------------------------- *)
2366(* Various "arithmetical" lemmas. *)
2367(* ------------------------------------------------------------------------- *)
2368
2369Theorem CARD_ADD_SYM:
2370 !s:'a->bool t:'b->bool. (s +_c t) =_c (t +_c s)
2371Proof
2372 rw[cardeq_def] >> qexists ‘λx. case x of INL a => INR a | INR b => INL b’ >>
2373 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_SUM, AllCaseEqs()]
2374QED
2375
2376Theorem CARD_ADD_ASSOC:
2377 !s:'a->bool t:'b->bool u:'c->bool. (s +_c (t +_c u)) =_c ((s +_c t) +_c u)
2378Proof
2379 rw[cardeq_def] >>
2380 qexists ‘λx. case x of INL a => INL (INL a) | INR (INL b) => INL (INR b)
2381 | INR (INR c) => INR c’ >>
2382 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_SUM, AllCaseEqs()]
2383QED
2384
2385Theorem CARD_MUL_SYM = CARDEQ_CROSS_SYM
2386
2387Theorem CARD_MUL_ASSOC:
2388 !s:'a->bool t:'b->bool u:'c->bool. (s *_c (t *_c u)) =_c ((s *_c t) *_c u)
2389Proof
2390 rw[cardeq_def] >>
2391 qexists ‘λt. case t of (a,(b,c)) => ((a,b),c)’>>
2392 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD]
2393QED
2394
2395Theorem CARD_LDISTRIB:
2396 !s:'a->bool t:'b->bool u:'c->bool.
2397 (s *_c (t +_c u)) =_c ((s *_c t) +_c (s *_c u))
2398Proof
2399 rw[cardeq_def] >>
2400 qexists ‘λp. case p of (a,INL b) => INL (a,b) | (a, INR c) => INR (a, c)’ >>
2401 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD, FORALL_SUM,
2402 AllCaseEqs()]
2403QED
2404
2405Theorem CARD_RDISTRIB:
2406 !s:'a->bool t:'b->bool u:'c->bool.
2407 (s +_c t) *_c u =_c (s *_c u) +_c (t *_c u)
2408Proof
2409 rw[cardeq_def] >>
2410 qexists ‘λp. case p of (INL a, c) => INL (a,c) | (INR b, c) => INR (b,c)’ >>
2411 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD, FORALL_SUM,
2412 AllCaseEqs()]
2413QED
2414
2415Theorem CARD_LE_ADDR:
2416 !s:'a->bool t:'b->bool. s <=_c (s +_c t)
2417Proof
2418 REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
2419 EXISTS_TAC ``INL:'a->'a+'b`` THEN SIMP_TAC std_ss [IN_CARD_ADD, INR_11, INL_11]
2420QED
2421
2422Theorem CARD_LE_ADDL:
2423 !s:'a->bool t:'b->bool. t <=_c (s +_c t)
2424Proof
2425 REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
2426 EXISTS_TAC ``INR:'b->'a+'b`` THEN SIMP_TAC std_ss [IN_CARD_ADD, INR_11, INL_11]
2427QED
2428
2429(* ------------------------------------------------------------------------- *)
2430(* A rather special lemma but temporarily useful. *)
2431(* ------------------------------------------------------------------------- *)
2432
2433Theorem CARD_ADD_LE_MUL_INFINITE:
2434 !s:'a->bool. INFINITE s ==> (s +_c s) <=_c (s *_c s)
2435Proof
2436 GEN_TAC THEN REWRITE_TAC[INFINITE_CARD_LE, le_c, IN_UNIV] THEN
2437 DISCH_THEN(X_CHOOSE_THEN ``f:num->'a`` STRIP_ASSUME_TAC) THEN
2438 KNOW_TAC ``?h. (!x. h(INL x) = (f(0:num),x):'a#'a) /\ (!x. h(INR x) = (f(1),x))`` THENL
2439 [RW_TAC std_ss [sum_Axiom], ALL_TAC] THEN
2440 STRIP_TAC THEN EXISTS_TAC ``h:'a+'a->'a#'a`` THEN STRIP_TAC THENL
2441 [ONCE_REWRITE_TAC [METIS [] ``( x IN s +_c s ==> h x IN s *_c s) =
2442 (\x. x IN s +_c s ==> h x IN s *_c s) x``] THEN
2443 MATCH_MP_TAC sum_INDUCT THEN
2444 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ], ALL_TAC] THEN
2445 ONCE_REWRITE_TAC [METIS [] ``(!y. x IN s +_c s /\ y IN s +_c s /\ (h x = h y) ==> (x = y)) =
2446 (\x. !y. x IN s +_c s /\ y IN s +_c s /\ (h x = h y) ==> (x = y)) x``] THEN
2447 MATCH_MP_TAC sum_INDUCT THEN
2448 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ] THEN STRIP_TAC THEN STRIP_TAC THENL
2449 [ONCE_REWRITE_TAC [METIS [] ``(x IN s /\ y IN s +_c s /\ ((f (0:num),x) =
2450 (h :'a + 'a -> 'a # 'a) y) ==> (INL x = y)) =
2451 (\y:'a+'a. x IN s /\ y IN s +_c s /\ ((f (0:num),x) =
2452 (h :'a + 'a -> 'a # 'a) y) ==> (INL x = y)) y``],
2453 ONCE_REWRITE_TAC [METIS [] ``(x IN s /\ y IN s +_c s /\ ((f (1:num),x) =
2454 (h :'a + 'a -> 'a # 'a) y) ==> (INR x = y)) =
2455 (\y:'a+'a. x IN s /\ y IN s +_c s /\ ((f (1:num),x) =
2456 (h :'a + 'a -> 'a # 'a) y) ==> (INR x = y)) y``]] THEN
2457 MATCH_MP_TAC sum_INDUCT THEN
2458 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ] THEN
2459 ASM_MESON_TAC[REDUCE_CONV ``1 = 0:num``]
2460QED
2461
2462(* ------------------------------------------------------------------------- *)
2463(* Relate cardinal addition to the simple union operation. *)
2464(* ------------------------------------------------------------------------- *)
2465
2466Theorem CARDEQ_DISJOINT_UNION:
2467 !s:'a->bool t. (s INTER t = EMPTY) ==> (s UNION t =_c (s +_c t))
2468Proof
2469 REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN
2470 STRIP_TAC THEN REWRITE_TAC[eq_c, IN_UNION] THEN
2471 EXISTS_TAC ``\x:'a. if x IN s then INL x else INR x`` THEN
2472 SIMP_TAC std_ss [FORALL_SUM, IN_CARD_ADD] THEN
2473 REWRITE_TAC[COND_RAND, COND_RATOR] THEN
2474 REWRITE_TAC[TAUT `(if b then x else y) <=> b /\ x \/ ~b /\ y`] THEN
2475 SIMP_TAC std_ss [sum_distinct, INL_11, INR_11, IN_CARD_ADD] THEN
2476 ASM_MESON_TAC[]
2477QED
2478
2479(* ------------------------------------------------------------------------- *)
2480(* The key to arithmetic on infinite cardinals: k^2 = k. *)
2481(* ------------------------------------------------------------------------- *)
2482
2483Theorem CARD_SQUARE_INFINITE = SET_SQUARED_CARDEQ_SET;
2484
2485(* ------------------------------------------------------------------------- *)
2486(* Preservation of finiteness. *)
2487(* ------------------------------------------------------------------------- *)
2488
2489Theorem CARD_ADD_FINITE:
2490 !s t. FINITE s /\ FINITE t ==> FINITE(s +_c t)
2491Proof
2492 SIMP_TAC std_ss [add_c, FINITE_UNION, GSYM IMAGE_DEF, IMAGE_FINITE]
2493QED
2494
2495Theorem CARD_ADD_FINITE_EQ:
2496 !s:'a->bool t:'b->bool. FINITE(s +_c t) <=> FINITE s /\ FINITE t
2497Proof
2498 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[CARD_ADD_FINITE] THEN
2499 DISCH_THEN(fn th => CONJ_TAC THEN MP_TAC th) THEN
2500 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) THEN
2501 REWRITE_TAC[CARD_LE_ADDL, CARD_LE_ADDR]
2502QED
2503
2504Theorem CARD_MUL_FINITE:
2505 !s t. FINITE s /\ FINITE t ==> FINITE(s *_c t)
2506Proof
2507 SIMP_TAC std_ss [mul_c, FINITE_PRODUCT]
2508QED
2509
2510(* ------------------------------------------------------------------------- *)
2511(* Hence the "absorption laws" for arithmetic with an infinite cardinal. *)
2512(* ------------------------------------------------------------------------- *)
2513
2514Theorem CARD_MUL2_ABSORB_LE:
2515 !s:'a->bool t:'b->bool u:'c->bool.
2516 INFINITE(u) /\ s <=_c u /\ t <=_c u ==> (s *_c t) <=_c u
2517Proof
2518 REPEAT STRIP_TAC THEN
2519 KNOW_TAC ``(s *_c t) <=_c ((s:'a->bool) *_c (u:'c->bool)) /\
2520 ((s:'a->bool) *_c (u:'c->bool)) <=_c u`` THENL
2521 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2522 ASM_SIMP_TAC std_ss [CARD_MUL_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_MUL THEN
2523 ASM_REWRITE_TAC[CARD_LE_REFL]
2524QED
2525
2526Theorem CARD_ADD_ABSORB_LE:
2527 !s:'a->bool t:'b->bool. INFINITE(t) /\ s <=_c t ==> (s +_c t) <=_c t
2528Proof
2529 REPEAT STRIP_TAC THEN
2530 KNOW_TAC ``(s +_c t) <=_c ((t:'b->bool) *_c t) /\
2531 ((t:'b->bool) *_c t) <=_c t`` THENL
2532 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2533 ASM_SIMP_TAC std_ss [CARD_SQUARE_INFINITE, CARD_EQ_IMP_LE] THEN
2534 KNOW_TAC ``(s +_c t) <=_c ((t:'b->bool) +_c t) /\
2535 ((t:'b->bool) +_c t) <=_c (t *_c t)`` THENL
2536 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2537 ASM_SIMP_TAC std_ss [CARD_ADD_LE_MUL_INFINITE, CARD_LE_ADD, CARD_LE_REFL]
2538QED
2539
2540Theorem CARD_ADD2_ABSORB_LE:
2541 !s:'a->bool t:'b->bool u:'c->bool.
2542 INFINITE(u) /\ s <=_c u /\ t <=_c u ==> (s +_c t) <=_c u
2543Proof
2544 REPEAT STRIP_TAC THEN
2545 KNOW_TAC ``(s +_c t) <=_c ((s:'a->bool) +_c (u:'c->bool)) /\
2546 ((s:'a->bool) +_c (u:'c->bool)) <=_c u`` THENL
2547 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2548 ASM_SIMP_TAC std_ss [CARD_ADD_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_ADD THEN
2549 ASM_REWRITE_TAC[CARD_LE_REFL]
2550QED
2551
2552Theorem CARD_MUL_ABSORB:
2553 !s:'a->bool t:'b->bool.
2554 INFINITE(t) /\ ~(s = {}) /\ s <=_c t ==> (s *_c t) =_c t
2555Proof
2556 SIMP_TAC std_ss [GSYM CARD_LE_ANTISYM, CARD_MUL_ABSORB_LE] THEN REPEAT STRIP_TAC THEN
2557 FIRST_X_ASSUM(X_CHOOSE_TAC ``a:'a`` o
2558 REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
2559 REWRITE_TAC[le_c] THEN EXISTS_TAC ``\x:'b. (a:'a,x)`` THEN
2560 ASM_SIMP_TAC std_ss [IN_CARD_MUL, PAIR_EQ]
2561QED
2562
2563Theorem CARD_ADD_ABSORB:
2564 !s:'a->bool t:'b->bool. INFINITE(t) /\ s <=_c t ==> (s +_c t) =_c t
2565Proof
2566 SIMP_TAC std_ss [GSYM CARD_LE_ANTISYM, CARD_LE_ADDL, CARD_ADD_ABSORB_LE]
2567QED
2568
2569Theorem CARD_ADD2_ABSORB_LT:
2570 !s:'a->bool t:'b->bool u:'c->bool.
2571 INFINITE u /\ s <_c u /\ t <_c u ==> (s +_c t) <_c u
2572Proof
2573 REPEAT GEN_TAC THEN
2574 STRIP_TAC THEN
2575 ASM_CASES_TAC ``FINITE((s:'a->bool) +_c (t:'b->bool))`` THEN
2576 ASM_SIMP_TAC std_ss [CARD_LT_FINITE_INFINITE] THEN
2577 DISJ_CASES_TAC(ISPECL [``s:'a->bool``, ``t:'b->bool``] CARD_LE_TOTAL) THENL
2578 [(* goal 1 (of 2) *)
2579 ASM_CASES_TAC ``FINITE(t:'b->bool)`` THENL
2580 [ASM_MESON_TAC[CARD_LE_FINITE, CARD_ADD_FINITE],
2581 KNOW_TAC ``(s +_c t) <=_c (t:'b->bool) /\
2582 (t:'b->bool) <_c u`` THENL
2583 [ALL_TAC, METIS_TAC [CARD_LET_TRANS]]],
2584 (* goal 2 (of 2) *)
2585 ASM_CASES_TAC ``FINITE(s:'a->bool)`` THENL
2586 [ASM_MESON_TAC[CARD_LE_FINITE, CARD_ADD_FINITE],
2587 KNOW_TAC ``(s +_c t) <=_c (s:'a->bool) /\
2588 (s:'a->bool) <_c u`` THENL
2589 [ALL_TAC, METIS_TAC [CARD_LET_TRANS]]]] THEN
2590 ASM_REWRITE_TAC[] THEN
2591 MATCH_MP_TAC CARD_ADD2_ABSORB_LE THEN
2592 ASM_REWRITE_TAC[CARD_LE_REFL]
2593QED
2594
2595Theorem CARD_LT_ADD:
2596 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2597 s <_c s' /\ t <_c t' ==> (s +_c t) <_c (s' +_c t')
2598Proof
2599 REPEAT GEN_TAC THEN
2600 STRIP_TAC THEN
2601 ASM_CASES_TAC ``FINITE((s':'b->bool) +_c (t':'d->bool))`` THENL
2602 [FIRST_X_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE
2603 [CARD_ADD_FINITE_EQ]) THEN
2604 SUBGOAL_THEN ``FINITE(s:'a->bool) /\ FINITE(t:'c->bool)``
2605 STRIP_ASSUME_TAC THENL
2606 [CONJ_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
2607 (REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) o
2608 MATCH_MP CARD_LT_IMP_LE) THEN
2609 ASM_REWRITE_TAC[],
2610 MAP_EVERY UNDISCH_TAC
2611 [``(s:'a->bool) <_c (s':'b->bool)``,
2612 ``(t:'c->bool) <_c (t':'d->bool)``] THEN
2613 ASM_SIMP_TAC std_ss [CARD_LT_CARD, CARD_ADD_FINITE, CARD_ADD_C] THEN
2614 ARITH_TAC],
2615 MATCH_MP_TAC CARD_ADD2_ABSORB_LT THEN ASM_REWRITE_TAC[] THEN
2616 CONJ_TAC THENL
2617 [METIS_TAC [CARD_LTE_TRANS, CARD_LE_ADDR],
2618 METIS_TAC [CARD_LTE_TRANS, CARD_LE_ADDL]]]
2619QED
2620
2621(* ------------------------------------------------------------------------- *)
2622(* Cantor's theorem. *)
2623(* ------------------------------------------------------------------------- *)
2624
2625Theorem CANTOR_THM:
2626 !s:'a->bool. s <_c {t | t SUBSET s}
2627Proof
2628 simp[GSYM POW_DEF]
2629QED
2630
2631Theorem CANTOR_THM_UNIV:
2632 (UNIV:'a->bool) <_c (UNIV:('a->bool)->bool)
2633Proof
2634 ‘univ(:'a -> bool) = POW univ(:'a)’ suffices_by simp[] >>
2635 simp[EXTENSION, POW_DEF]
2636QED
2637
2638Theorem CARD_EXP_SING :
2639 !(s :'a -> bool) (b :'b). (s ** {b}) =_c s
2640Proof
2641 REWRITE_TAC [SING_set_exp_CARD]
2642QED
2643
2644Theorem CARD_EXP_CONG :
2645 !(s:'a->bool) (s':'b->bool) (t:'c->bool) (t':'d->bool).
2646 s =_c s' /\ t =_c t' ==> s ** t =_c s' ** t'
2647Proof
2648 rw [set_exp_card_cong]
2649QED
2650
2651Theorem CARD_LE_EXP_LEFT :
2652 !(s :'a -> bool) (s' :'b -> bool) (t :'c -> bool).
2653 s <=_c s' ==> s ** t <=_c s' ** t
2654Proof
2655 REPEAT GEN_TAC THEN REWRITE_TAC[le_c, exp_c] THEN
2656 DISCH_THEN(X_CHOOSE_TAC “f :'a -> 'b”) THEN
2657 rw [GSPECIFICATION] THEN
2658 EXISTS_TAC “\(g:'c->'a) (z:'c). if z IN t then f(g z):'b else ARB” THEN
2659 rw [FUN_EQ_THM] THEN
2660 METIS_TAC []
2661QED
2662
2663Theorem CARD_EXP_MUL :
2664 !(s:'a->bool) (t:'b->bool) (u:'c->bool).
2665 s ** (t *_c u) =_c (s ** t) ** u
2666Proof
2667 rw [Once cardeq_SYM, set_exp_product]
2668QED
2669
2670Theorem CARD_EXP_POWERSET :
2671 !s :'a -> bool. univ(:bool) ** s =_c {t | t SUBSET s}
2672Proof
2673 GEN_TAC
2674 >> REWRITE_TAC [exp_c, EQ_C_BIJECTIONS, IN_UNIV]
2675 >> qexistsl_tac [‘\P. {x | x IN s /\ P x}’,
2676 ‘\t x. if x IN s then x IN t else ARB’]
2677 >> SIMP_TAC std_ss [GSPECIFICATION]
2678 >> SET_TAC []
2679QED
2680
2681Theorem CARD_EXP_CANTOR :
2682 !s :'a -> bool. s <_c univ(:bool) ** s
2683Proof
2684 GEN_TAC THEN
2685 TRANS_TAC CARD_LTE_TRANS “{t :'a->bool | t SUBSET s}” THEN
2686 REWRITE_TAC[CANTOR_THM] THEN
2687 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2688 ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[CARD_EXP_POWERSET]
2689QED
2690
2691Theorem CARD_EXP_ABSORB :
2692 !(s :'a -> bool) (t :'b -> bool).
2693 INFINITE t /\ univ(:bool) <=_c s /\ s <=_c univ(:bool) ** t
2694 ==> s ** t =_c univ(:bool) ** t
2695Proof
2696 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN
2697 ASM_SIMP_TAC std_ss [CARD_LE_EXP_LEFT, CARD_LE_REFL] THEN
2698 TRANS_TAC CARD_LE_TRANS “(univ(:bool) ** t) ** (t:'b->bool)” THEN
2699 ASM_SIMP_TAC std_ss[CARD_LE_EXP_LEFT] THEN
2700 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2701 TRANS_TAC CARD_EQ_TRANS “univ(:bool) ** ((t:'b->bool) *_c t)” THEN
2702 SIMP_TAC std_ss[ONCE_REWRITE_RULE[CARD_EQ_SYM] CARD_EXP_MUL] THEN
2703 MATCH_MP_TAC CARD_EXP_CONG THEN
2704 ASM_SIMP_TAC std_ss[CARD_SQUARE_INFINITE, CARD_EQ_REFL]
2705QED
2706
2707(* ------------------------------------------------------------------------- *)
2708(* Lemmas about countability. *)
2709(* ------------------------------------------------------------------------- *)
2710
2711Theorem NUM_COUNTABLE = num_countable
2712
2713Theorem COUNTABLE_ALT_cardleq:
2714 !s. COUNTABLE s <=> s <=_c univ(:num)
2715Proof
2716 REWRITE_TAC[COUNTABLE, ge_c]
2717QED
2718
2719Theorem COUNTABLE_CASES:
2720 !s. COUNTABLE s <=> FINITE s \/ s =_c univ(:num)
2721Proof
2722 GEN_TAC
2723 >> ONCE_REWRITE_TAC[COUNTABLE_ALT_cardleq, FINITE_CARD_LT]
2724 >> METIS_TAC [CARD_LE_LT]
2725QED
2726
2727(* changed ‘t:'a->bool’ to ‘t:'b->bool’ *)
2728Theorem CARD_LE_COUNTABLE :
2729 !s:'a->bool t:'b->bool. COUNTABLE t /\ s <=_c t ==> COUNTABLE s
2730Proof
2731 REWRITE_TAC [COUNTABLE, ge_c]
2732 >> rpt STRIP_TAC
2733 >> KNOW_TAC ``?(t :'b -> bool).
2734 (s :'a -> bool) <=_c t /\ t <=_c univ((:num) :num itself)``
2735 >- (EXISTS_TAC ``t:'b->bool`` >> ASM_REWRITE_TAC[])
2736 >> METIS_TAC [CARD_LE_TRANS]
2737QED
2738
2739Theorem countable_setexp:
2740 countable (A ** B) <=>
2741 B = {} \/ FINITE B /\ countable A \/ A =~ {()} \/ A = {}
2742Proof
2743 rw[EQ_IMP_THM] >~
2744 [‘countable (A ** {})’]
2745 >- (resolve_then (Pos hd) irule EMPTY_set_exp_CARD (iffRL countable_cardeq) >>
2746 simp[COUNTABLE_COUNT]) >~
2747 [‘countable ({} ** B)’]
2748 >- (Cases_on ‘B = {}’
2749 >- (simp[] >>
2750 resolve_then (Pos hd) irule EMPTY_set_exp_CARD
2751 (iffRL countable_cardeq) >>
2752 simp[COUNTABLE_COUNT]) >>
2753 simp[EMPTY_set_exp]) >~
2754 [‘FINITE B /\ countable A’]
2755 >- (Cases_on ‘B = {}’ >> simp[] >> Cases_on ‘A = {}’ >> simp[] >>
2756 Cases_on ‘A =~ {()}’ >> simp[] >>
2757 Cases_on ‘FINITE B’ >> simp[]
2758 >- metis_tac[FINITE_EXPONENT_SETEXP_UNCOUNTABLE] >>
2759 ‘~countable (POW B)’ by metis_tac[infinite_pow_uncountable] >>
2760 ‘~countable (count 2 ** B)’
2761 by metis_tac[countable_cardeq, POW_TWO_set_exp] >>
2762 pop_assum mp_tac >> simp[] >>
2763 ‘count 2 ** B <<= A ** B’ suffices_by metis_tac[CARD_LE_COUNTABLE] >>
2764 irule set_exp_cardle_cong >> simp[] >> metis_tac[FINITE_012]) >~
2765 [‘A =~ {()}’]
2766 >- gvs[CARD1_SING, SING_set_exp] >>
2767 metis_tac[FINITE_EXPONENT_SETEXP_COUNTABLE]
2768QED
2769
2770(* NOTE: Changed the type of ‘t’ to ‘:'b->bool’ (was: 'a->bool) *)
2771Theorem CARD_EQ_COUNTABLE :
2772 !s:'a->bool t:'b->bool. COUNTABLE t /\ s =_c t ==> COUNTABLE s
2773Proof
2774 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
2775QED
2776
2777(* NOTE: Changed the type of ‘t’ to ‘:'b->bool’ (was: 'a->bool) *)
2778Theorem CARD_COUNTABLE_CONG :
2779 !s:'a->bool t:'b->bool. s =_c t ==> (COUNTABLE s <=> COUNTABLE t)
2780Proof
2781 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
2782QED
2783
2784Theorem COUNTABLE_RESTRICT:
2785 !s P. COUNTABLE s ==> COUNTABLE {x | x IN s /\ P x}
2786Proof
2787 REPEAT GEN_TAC THEN
2788 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2789 SET_TAC[]
2790QED
2791
2792Theorem FINITE_IMP_COUNTABLE:
2793 !s. FINITE s ==> COUNTABLE s
2794Proof
2795 SIMP_TAC std_ss [FINITE_CARD_LT, Once lt_c, COUNTABLE, ge_c]
2796QED
2797
2798Theorem COUNTABLE_IMAGE:
2799 !f:'a->'b s. COUNTABLE s ==> COUNTABLE (IMAGE f s)
2800Proof
2801 SIMP_TAC std_ss [COUNTABLE, ge_c] THEN REPEAT STRIP_TAC THEN
2802 KNOW_TAC ``IMAGE (f:'a->'b) s <=_c s /\ s <=_c univ(:num)`` THENL
2803 [ASM_SIMP_TAC std_ss [CARD_LE_IMAGE], METIS_TAC [CARD_LE_TRANS]]
2804QED
2805
2806Theorem COUNTABLE_IMAGE_INJ_GENERAL:
2807 !(f:'a->'b) A s.
2808 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
2809 COUNTABLE A
2810 ==> COUNTABLE {x | x IN s /\ f(x) IN A}
2811Proof
2812 REPEAT STRIP_TAC THEN
2813 UNDISCH_TAC ``!x y. x IN s /\ y IN s /\ ((f:'a->'b) x = f y) ==>
2814 (x = y)`` THEN DISCH_TAC THEN
2815 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [INJECTIVE_ON_LEFT_INVERSE]) THEN
2816 DISCH_THEN(X_CHOOSE_TAC ``g:'b->'a``) THEN
2817 MATCH_MP_TAC COUNTABLE_SUBSET THEN EXISTS_TAC ``IMAGE (g:'b->'a) A`` THEN
2818 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE] THEN ASM_SET_TAC[]
2819QED
2820
2821Theorem COUNTABLE_IMAGE_INJ_EQ:
2822 !(f:'a->'b) s.
2823 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==>
2824 (COUNTABLE(IMAGE f s) <=> COUNTABLE s)
2825Proof
2826 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE] THEN
2827 POP_ASSUM MP_TAC THEN REWRITE_TAC[AND_IMP_INTRO] THEN
2828 DISCH_THEN(MP_TAC o MATCH_MP COUNTABLE_IMAGE_INJ_GENERAL) THEN
2829 csimp[IMAGE_IN]
2830QED
2831
2832Theorem COUNTABLE_IMAGE_INJ:
2833 !(f:'a->'b) A.
2834 (!x y. (f(x) = f(y)) ==> (x = y)) /\
2835 COUNTABLE A
2836 ==> COUNTABLE {x | f(x) IN A}
2837Proof
2838 REPEAT GEN_TAC THEN
2839 MP_TAC(SPECL [``f:'a->'b``, ``A:'b->bool``, ``UNIV:'a->bool``]
2840 COUNTABLE_IMAGE_INJ_GENERAL) THEN SIMP_TAC std_ss [IN_UNIV]
2841QED
2842
2843Theorem COUNTABLE_EMPTY:
2844 COUNTABLE {}
2845Proof
2846 REWRITE_TAC [COUNTABLE, ge_c, le_c, NOT_IN_EMPTY]
2847QED
2848
2849Theorem COUNTABLE_INTER:
2850 !s t. COUNTABLE s \/ COUNTABLE t ==> COUNTABLE (s INTER t)
2851Proof
2852 REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
2853 REPEAT GEN_TAC THEN CONJ_TAC THEN
2854 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2855 SET_TAC[]
2856QED
2857
2858Theorem COUNTABLE_UNION_IMP:
2859 !s t:'a->bool. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s UNION t)
2860Proof
2861 REWRITE_TAC[COUNTABLE, ge_c] THEN REPEAT STRIP_TAC THEN
2862 KNOW_TAC ``s UNION t <=_c ((s:'a->bool) +_c (t:'a->bool)) /\
2863 ((s:'a->bool) +_c (t:'a->bool)) <=_c univ(:num)`` THENL
2864 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2865 ASM_SIMP_TAC std_ss [CARD_ADD2_ABSORB_LE, num_INFINITE, UNION_LE_ADD_C]
2866QED
2867
2868Theorem COUNTABLE_UNION:
2869 !s t:'a->bool. COUNTABLE(s UNION t) <=> COUNTABLE s /\ COUNTABLE t
2870Proof
2871 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[COUNTABLE_UNION_IMP] THEN
2872 DISCH_THEN(fn th => CONJ_TAC THEN MP_TAC th) THEN
2873 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2874 SET_TAC[]
2875QED
2876
2877Theorem COUNTABLE_SING:
2878 !x. COUNTABLE {x}
2879Proof
2880 REWRITE_TAC [COUNTABLE, ge_c, le_c, IN_SING, IN_UNIV] THEN
2881 METIS_TAC []
2882QED
2883
2884Theorem COUNTABLE_INSERT[simp]:
2885 !x s. COUNTABLE(x INSERT s) <=> COUNTABLE s
2886Proof
2887 ONCE_REWRITE_TAC[SET_RULE ``x INSERT s = {x} UNION s``] THEN
2888 REWRITE_TAC[COUNTABLE_UNION, COUNTABLE_SING]
2889QED
2890
2891Theorem COUNTABLE_DELETE[simp]:
2892 !x:'a s. COUNTABLE(s DELETE x) <=> COUNTABLE s
2893Proof
2894 REPEAT GEN_TAC THEN ASM_CASES_TAC ``(x:'a) IN s`` THEN
2895 ASM_SIMP_TAC std_ss [SET_RULE ``~(x IN s) ==> (s DELETE x = s)``] THEN
2896 MATCH_MP_TAC EQ_TRANS THEN
2897 EXISTS_TAC ``COUNTABLE((x:'a) INSERT (s DELETE x))`` THEN CONJ_TAC THENL
2898 [REWRITE_TAC[COUNTABLE_INSERT], AP_TERM_TAC THEN ASM_SET_TAC[]]
2899QED
2900
2901Theorem COUNTABLE_DIFF_FINITE:
2902 !s t. FINITE s ==> (COUNTABLE(t DIFF s) <=> COUNTABLE t)
2903Proof
2904 Induct_on ‘FINITE’ >>
2905 simp[SET_RULE ``s DIFF (x INSERT t) = (s DIFF t) DELETE x``]
2906QED
2907
2908Theorem UNCOUNTABLE_DIFF_COUNTABLE :
2909 !s t. ~COUNTABLE s /\ COUNTABLE t ==> ~COUNTABLE (s DIFF t)
2910Proof
2911 rpt STRIP_TAC
2912 >> ‘s DIFF t UNION (s INTER t) = s’ by SET_TAC []
2913 >> ‘COUNTABLE (s INTER t)’ by simp [COUNTABLE_INTER]
2914 >> METIS_TAC [COUNTABLE_UNION]
2915QED
2916
2917Theorem UNCOUNTABLE_DIFF_FINITE :
2918 !s t. ~COUNTABLE s /\ FINITE t ==> ~COUNTABLE (s DIFF t)
2919Proof
2920 PROVE_TAC [FINITE_IMP_COUNTABLE, UNCOUNTABLE_DIFF_COUNTABLE]
2921QED
2922
2923Theorem COUNTABLE_CROSS:
2924 !s t. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s CROSS t)
2925Proof
2926 rpt GEN_TAC
2927 >> REWRITE_TAC [COUNTABLE, ge_c]
2928 >> STRIP_TAC
2929 >> MATCH_MP_TAC (Q.SPEC `UNIV`
2930 (INST_TYPE [``:'c`` |-> ``:num``]
2931 (ISPECL [``s :'a set``, ``t :'b set``] CARD_MUL2_ABSORB_LE)))
2932 >> ASM_REWRITE_TAC [num_INFINITE]
2933QED
2934
2935Theorem COUNTABLE_AS_IMAGE_SUBSET:
2936 !s. COUNTABLE s ==> ?f. s SUBSET (IMAGE f univ(:num))
2937Proof
2938 REWRITE_TAC[COUNTABLE, ge_c, LE_C, SUBSET_DEF, IN_IMAGE] THEN MESON_TAC[]
2939QED
2940
2941Theorem COUNTABLE_AS_IMAGE_SUBSET_EQ:
2942 !s:'a->bool. COUNTABLE s <=> ?f. s SUBSET (IMAGE f univ(:num))
2943Proof
2944 REWRITE_TAC[COUNTABLE, ge_c, LE_C, SUBSET_DEF, IN_IMAGE] THEN MESON_TAC[]
2945QED
2946
2947Theorem COUNTABLE_AS_IMAGE:
2948 !s:'a->bool. COUNTABLE s /\ ~(s = {}) ==> ?f. (s = IMAGE f univ(:num))
2949Proof
2950 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC ``a:'a`` o
2951 REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
2952 FIRST_X_ASSUM(MP_TAC o MATCH_MP COUNTABLE_AS_IMAGE_SUBSET) THEN
2953 DISCH_THEN(X_CHOOSE_TAC ``f:num->'a``) THEN
2954 EXISTS_TAC ``\n. if (f:num->'a) n IN s then f n else a`` THEN
2955 ASM_SET_TAC[]
2956QED
2957
2958Theorem FORALL_COUNTABLE_AS_IMAGE:
2959 (!d. COUNTABLE d ==> P d) <=> P {} /\ (!f. P(IMAGE f univ(:num)))
2960Proof
2961 MESON_TAC[COUNTABLE_AS_IMAGE, COUNTABLE_IMAGE, NUM_COUNTABLE,
2962 COUNTABLE_EMPTY]
2963QED
2964
2965Theorem COUNTABLE_AS_INJECTIVE_IMAGE:
2966 !s. COUNTABLE s /\ INFINITE s
2967 ==> ?f. (s = IMAGE f univ(:num)) /\ (!m n. (f(m) = f(n)) ==> (m = n))
2968Proof
2969 GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
2970 REWRITE_TAC[INFINITE_CARD_LE, COUNTABLE, ge_c] THEN
2971 SIMP_TAC std_ss [CARD_LE_ANTISYM, eq_c] THEN SET_TAC[]
2972QED
2973
2974Theorem COUNTABLE_BIGUNION = bigunion_countable
2975
2976Theorem IN_ELIM_PAIR_THM:
2977 !P a b. (a,b) IN {(x,y) | P x y} <=> P a b
2978Proof
2979 SRW_TAC [][]
2980QED
2981
2982Theorem COUNTABLE_PRODUCT_DEPENDENT:
2983 !f:'a->'b->'c s t.
2984 COUNTABLE s /\ (!x. x IN s ==> COUNTABLE(t x)) ==>
2985 COUNTABLE {f x y | x IN s /\ y IN (t x)}
2986Proof
2987 REPEAT GEN_TAC THEN DISCH_TAC THEN
2988 SUBGOAL_THEN “{(f:'a->'b->'c) x y | x IN s /\ y IN (t x)} =
2989 IMAGE (λ(x,y). f x y) {(x,y) | x IN s /\ y IN (t x)}”
2990 SUBST1_TAC THENL
2991 [SIMP_TAC std_ss [EXTENSION, IN_IMAGE, EXISTS_PROD, IN_ELIM_PAIR_THM] THEN
2992 SET_TAC[],
2993 MATCH_MP_TAC COUNTABLE_IMAGE THEN POP_ASSUM MP_TAC] THEN
2994 CONV_TAC $ LAND_CONV $ REWRITE_CONV [COUNTABLE_AS_IMAGE_SUBSET_EQ] THEN
2995 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC “f:num->'a”) MP_TAC) THEN
2996 DISCH_THEN (MP_TAC o SIMP_RULE std_ss [RIGHT_IMP_EXISTS_THM]) THEN
2997 SIMP_TAC std_ss [SKOLEM_THM] THEN
2998 DISCH_THEN(X_CHOOSE_TAC “g:'a->num->'b”) THEN
2999 MATCH_MP_TAC COUNTABLE_SUBSET THEN
3000 EXISTS_TAC “IMAGE (λ(m,n). (f:num->'a) m,(g:'a->num->'b)(f m) n)
3001 (univ(:num) CROSS univ(:num))” THEN
3002 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, COUNTABLE_CROSS, NUM_COUNTABLE] THEN
3003 SIMP_TAC std_ss [SUBSET_DEF, FORALL_IN_BIGUNION] THEN
3004 SIMP_TAC std_ss [IN_IMAGE, FORALL_PROD, IN_ELIM_PAIR_THM,
3005 EXISTS_PROD, IN_CROSS, IN_UNIV] THEN
3006 ASM_SET_TAC[]
3007QED
3008
3009Definition BIGPRODi_def:
3010 BIGPRODi (A : 'i -> ('a -> bool) option) =
3011 {tup : 'i -> 'a option |
3012 (!i. A i = NONE ==> tup i = NONE) /\
3013 !i s. A i = SOME s ==> ?a. tup i = SOME a /\ a IN s
3014 }
3015End
3016
3017(* A^0 = 1 *)
3018Theorem BIGPRODi_KNONE[simp]:
3019 BIGPRODi (K NONE) = {K NONE}
3020Proof
3021 simp[BIGPRODi_def, EXTENSION, FUN_EQ_THM]
3022QED
3023
3024Definition fnOfSet_def:
3025 fnOfSet s k = if ?!v. (k,v) IN s then SOME (@v. (k,v) IN s) else NONE
3026End
3027
3028Theorem fnOfSet_SING[simp]:
3029 fnOfSet {(k,v)} = (K NONE)(| k |-> SOME v |)
3030Proof
3031 simp[fnOfSet_def, FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM] >>
3032 rw[] >> gs[]
3033QED
3034
3035Theorem BIGPRODi_SING_EQ:
3036 BIGPRODi (fnOfSet {(i,s)}) = { (K NONE)(| i |-> SOME a |) | a IN s }
3037Proof
3038 simp[BIGPRODi_def, combinTheory.APPLY_UPDATE_THM, Once EXTENSION] >>
3039 simp[FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM, AllCaseEqs()] >>
3040 qx_gen_tac ‘tup’ >> simp[EQ_IMP_THM] >> rw[] >~
3041 [‘tup i = SOME a’] >- (first_assum $ irule_at Any >> metis_tac[]) >~
3042 [‘tup j = NONE’] >- metis_tac[] >>
3043 metis_tac[]
3044QED
3045
3046Theorem BIGPRODi_SING_CEQ:
3047 BIGPRODi (fnOfSet {(i,s)}) =~ s
3048Proof
3049 simp[BIGPRODi_SING_EQ, cardeq_def, BIJ_IFF_INV, PULL_EXISTS] >>
3050 qexistsl_tac [‘λx. THE (x i)’, ‘λa j. if j = i then SOME a else NONE’] >>
3051 simp[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> metis_tac[]
3052QED
3053
3054Theorem BIGPRODi_pair:
3055 i <> j ==>
3056 BIGPRODi (K NONE)(| i |-> SOME A1; j |-> SOME A2|) =~ A1 CROSS A2
3057Proof
3058 strip_tac >>
3059 simp[BIGPRODi_def, cardeq_def, BIJ_IFF_INV, FORALL_PROD, PULL_EXISTS] >>
3060 qexistsl_tac [‘λt. (THE (t i), THE (t j))’,
3061 ‘λp k. if k = i then SOME (FST p)
3062 else if k = j then SOME (SND p) else NONE’] >>
3063 rw[] >~
3064 [‘THE (tup i) IN A’] >- (first_x_assum $ qspec_then ‘i’ mp_tac >>
3065 gs[combinTheory.APPLY_UPDATE_THM, PULL_EXISTS]) >~
3066 [‘THE (tup i) IN A’] >- (first_x_assum $ qspec_then ‘i’ mp_tac >>
3067 gs[combinTheory.APPLY_UPDATE_THM, PULL_EXISTS]) >>
3068 gs[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> rw[] >>
3069 gs[AllCaseEqs(), DISJ_IMP_THM, FORALL_AND_THM]
3070QED
3071
3072Theorem BIGPRODi_EQ_EMPTY:
3073 BIGPRODi Af = {} <=> ?i. Af i = SOME {}
3074Proof
3075 simp[BIGPRODi_def] >> Cases_on ‘!i. Af i = NONE’ >> simp[]
3076 >- (simp[EXTENSION] >> qexists_tac ‘K NONE’ >> simp[]) >> gs[] >>
3077 simp[Once EXTENSION] >> eq_tac >>
3078 rpt strip_tac >> gvs[] >~
3079 [‘Af j = SOME {}’] >- (disj2_tac >> qexists_tac ‘j’ >> simp[]) >>
3080 CCONTR_TAC >>
3081 qpat_x_assum ‘!x. _’ mp_tac >> simp[] >>
3082 qexists_tac ‘λj. OPTION_MAP CHOICE (Af j)’ >>
3083 simp[SF DISJ_ss] >> gs[] >> metis_tac[CHOICE_DEF, SOME_11]
3084QED
3085
3086Definition BIGPROD_def:
3087 BIGPROD (A : ('a -> bool) -> bool) =
3088 BIGPRODi (λa. if a IN A then SOME a else NONE)
3089End
3090
3091Theorem BIGPROD_thm:
3092 BIGPROD A =
3093 { tup : ('a -> bool) -> 'a option |
3094 (!s. s IN A ==> ?a. tup s = SOME a /\ a IN s) /\
3095 (!s. s NOTIN A ==> tup s = NONE) }
3096Proof
3097 simp[BIGPROD_def, BIGPRODi_def, FORALL_AND_THM, CONJ_COMM]
3098QED
3099
3100Theorem BIGPROD_pair:
3101 A1 <> A2 ==>
3102 BIGPROD { A1; A2 } =~ A1 CROSS A2
3103Proof
3104 strip_tac >> simp[BIGPROD_def] >>
3105 ‘(\a. if a = A1 \/ a = A2 then SOME a else NONE) =
3106 (K NONE)(| A1 |-> SOME A1; A2 |-> SOME A2|)’
3107 by simp[Once FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM, AllCaseEqs(),
3108 SF DISJ_ss] >>
3109 simp[BIGPRODi_pair]
3110QED
3111
3112Theorem BIGPROD_SING:
3113 BIGPROD {A} =~ A
3114Proof
3115 simp[cardeq_def, BIGPROD_thm, BIJ_IFF_INV] >>
3116 qexists_tac ‘λt. THE (t A)’ >> simp[PULL_EXISTS] >>
3117 qexists_tac ‘\a s. if s = A then SOME a else NONE’ >> rw[] >>
3118 simp[Once FUN_EQ_THM] >> rw[]
3119QED
3120
3121Theorem BIGPROD_ONE:
3122 BIGPROD {} =~ {()}
3123Proof
3124 simp[BIGPROD_thm, cardeq_def]>> qexists_tac ‘K ()’ >>
3125 simp[BIJ_IFF_INV] >> qexists_tac ‘K (K NONE)’ >> simp[] >>
3126 rpt strip_tac >> simp[FUN_EQ_THM]
3127QED
3128
3129Theorem BIGPROD_EQ_EMPTY[simp]:
3130 BIGPROD As = {} <=> {} IN As
3131Proof
3132 simp[BIGPROD_def, BIGPRODi_EQ_EMPTY]
3133QED
3134
3135Theorem image_thms[simp,local]:
3136 IMAGE OUTL (IMAGE INL A) = A /\
3137 IMAGE OUTR (IMAGE INR B) = B /\
3138 ((!x. x IN AB ==> ISL x) ==> (IMAGE INL (IMAGE OUTL AB) = AB)) /\
3139 ((!x. x IN AB ==> ISR x) ==> (IMAGE INR (IMAGE OUTR AB) = AB))
3140Proof
3141 rw[EXTENSION, PULL_EXISTS] >> csimp[INR, INL]
3142QED
3143
3144Theorem BIGPROD_CONS:
3145 A CROSS BIGPROD As =~ BIGPROD (IMAGE INL A INSERT IMAGE (IMAGE INR) As)
3146Proof
3147 Cases_on ‘A = {}’ >> simp[iffRL BIGPROD_EQ_EMPTY, CARDEQ_0] >>
3148 Cases_on ‘{} IN As’ >> simp[iffRL BIGPROD_EQ_EMPTY, CARDEQ_0] >>
3149 simp[BIGPROD_thm, BIJ_IFF_INV, cardeq_def, FORALL_PROD] >>
3150 qexists_tac ‘λ(p : 'a # (('b -> bool) -> 'b option)) (s: 'a + 'b -> bool).
3151 if s = EMPTY then NONE : ('a + 'b) option
3152 else if (!x. x IN s ==> ISL x) then
3153 if IMAGE OUTL s = A then SOME (INL (FST p)) else NONE
3154 else if (!x. x IN s ==> ISR x) /\ IMAGE OUTR s IN As then
3155 SOME (INR (THE (SND p (IMAGE OUTR s))))
3156 else NONE’ >>
3157 rw[] >> simp[PULL_EXISTS]
3158 >- (metis_tac[THE_DEF, MEMBER_NOT_EMPTY])
3159 >- (rename [‘s = {}’, ‘s <> IMAGE INL A’] >>
3160 rpt (IF_CASES_TAC >> gvs[])
3161 >- (qpat_x_assum ‘s <> IMAGE INL _’ mp_tac >>
3162 rw[CONTRAPOS_THM] >> gvs[]) >>
3163 gvs[DISJ_EQ_IMP]) >>
3164 qexists_tac ‘λtup. (OUTL (THE (tup (IMAGE INL A))),
3165 (λB. if B IN As then
3166 SOME (OUTR (THE (tup (IMAGE INR B))))
3167 else NONE))’ >> rw[] >>
3168 gvs[DISJ_IMP_THM, FORALL_AND_THM, PULL_EXISTS]
3169 >- (first_x_assum drule >> simp[PULL_EXISTS])
3170 >- (simp[Once FUN_EQ_THM] >> rw[]
3171 >- gs[]
3172 >- metis_tac[MEMBER_NOT_EMPTY]
3173 >- metis_tac[MEMBER_NOT_EMPTY]
3174 >- (last_x_assum drule >> simp[PULL_EXISTS]))
3175 >- (simp[Once FUN_EQ_THM] >> qx_gen_tac ‘AB’ >> rw[]
3176 >- gs[]
3177 >- (first_x_assum irule >> rpt strip_tac >> gvs[PULL_EXISTS] >>
3178 metis_tac[MEMBER_NOT_EMPTY])
3179 >- (first_x_assum drule >> simp[PULL_EXISTS])
3180 >- (gs[] >> first_x_assum irule >> rpt strip_tac >> gvs[]))
3181QED
3182
3183Theorem tupNONE_IN_BIGPRODi:
3184 tup IN BIGPRODi Af ==> (tup i = NONE <=> Af i = NONE)
3185Proof
3186 simp[BIGPRODi_def, EQ_IMP_THM] >> rpt strip_tac >>
3187 first_x_assum $ qspec_then ‘i’ mp_tac >> simp[] >>
3188 Cases_on ‘Af i’ >> simp[]
3189QED
3190
3191Theorem BIGPRODi_11[simp]:
3192 (!i. Af i <> SOME {}) /\ (!i. Bf i <> SOME ({}:'b set)) ==>
3193 (BIGPRODi Af = BIGPRODi Bf <=> Af = Bf)
3194Proof
3195 rpt strip_tac >> simp[EQ_IMP_THM] >>
3196 simp[Once EXTENSION] >> strip_tac >>
3197 simp[FUN_EQ_THM] >> qx_gen_tac ‘j’ >>
3198 Cases_on ‘Af j = NONE \/ Bf j = NONE’
3199 >- (‘?t. t IN BIGPRODi Af’
3200 suffices_by metis_tac[tupNONE_IN_BIGPRODi] >>
3201 simp[MEMBER_NOT_EMPTY] >> simp[BIGPRODi_EQ_EMPTY]) >> gs[] >>
3202 ‘(?s1. Af j = SOME s1) /\ (?s2. Bf j = SOME s2)’
3203 by (map_every Cases_on [‘Af j’, ‘Bf j’] >> gs[]) >> simp[] >>
3204 CCONTR_TAC >>
3205 wlog_tac ‘?e. e IN s1 /\ e NOTIN s2’ [‘s1’, ‘s2’, ‘Bf’, ‘Af’]
3206 >- (gs[] >>
3207 ‘!A B. (!e:'b. e NOTIN A \/ e IN B) <=> A SUBSET B’
3208 by metis_tac[SUBSET_DEF] >> gs[] >>
3209 first_x_assum $ qspecl_then [‘s2’, ‘s1’, ‘Af’, ‘Bf’] mp_tac >> simp[] >>
3210 metis_tac[SUBSET_ANTISYM]) >>
3211 ‘!tup. tup IN BIGPRODi Bf ==> tup j <> SOME e’
3212 by (simp[BIGPRODi_def] >> rpt strip_tac >>
3213 first_x_assum $ qspec_then ‘j’ mp_tac >> simp[]) >>
3214 ‘?tup. tup IN BIGPRODi Af /\ tup j = SOME e’ suffices_by metis_tac[] >>
3215 ‘?tup0. tup0 IN BIGPRODi Af’
3216 by simp[MEMBER_NOT_EMPTY, BIGPRODi_EQ_EMPTY] >>
3217 qexists_tac ‘tup0(| j |-> SOME e |)’ >>
3218 pop_assum mp_tac >> REWRITE_TAC [BIGPRODi_def] >>
3219 simp[combinTheory.APPLY_UPDATE_THM] >> rw[AllCaseEqs()] >>
3220 metis_tac[SOME_11]
3221QED
3222
3223Theorem cardeq_addUnum:
3224 INFINITE (univ(:'a)) ==> univ(:num + 'a) =~ univ(:'a)
3225Proof
3226 strip_tac >> irule cardleq_ANTISYM >>
3227 ‘univ(:'a) <<= univ(:num + 'a)’
3228 by (simp[cardleq_def]>> qexists_tac ‘INR’ >>
3229 simp[INJ_DEF]) >> simp[] >>
3230 ‘univ(:num) <<= univ(:'a)’ by gs[INFINITE_Unum] >>
3231 simp[disjUNION_UNIV, CARD_ADD_ABSORB_LE]
3232QED
3233
3234Theorem wellorder_destWO =
3235 wellorder_ABSREP |> cj 2
3236 |> Q.SPEC ‘destWO r’
3237 |> REWRITE_RULE [mkWO_destWO]
3238
3239Theorem cardleq_copy_wellorders:
3240 univ(:'a) <<= univ(:'b) ==>
3241 !w1 : 'a wellorder. ?w2: 'b wellorder. orderiso w1 w2
3242Proof
3243 simp[orderiso_def, cardleq_def, INJ_IFF] >>
3244 disch_then $ qx_choose_then ‘f’ strip_assume_tac >>
3245 qx_gen_tac ‘w1’ >> qabbrev_tac ‘W2 = {(f x, f y) | (x,y) IN destWO w1 }’ >>
3246 ‘wellorder (destWO w1)’ by simp[wellorder_destWO] >>
3247 ‘wellorder W2’
3248 by (‘W2 = IMAGE (f ## f) (destWO w1)’
3249 by simp[Abbr‘W2’, EXTENSION, EXISTS_PROD] >>
3250 simp[] >> irule INJ_preserves_wellorder >>
3251 simp[wellorder_destWO] >> qexists_tac ‘UNIV’ >>
3252 simp[INJ_IFF]) >>
3253 qexistsl_tac [‘mkWO W2’, ‘f’] >>
3254 ‘elsOf (mkWO W2) = { f x | x IN elsOf w1}’
3255 by (simp[elsOf_def, Abbr‘W2’, destWO_mkWO, domain_def, range_def] >>
3256 dsimp[EXTENSION] >> metis_tac[]) >>
3257 simp[PULL_EXISTS] >>
3258 simp[destWO_mkWO] >> simp[strict_def, Abbr‘W2’]
3259QED
3260
3261Theorem finite_subsets_bijection:
3262 INFINITE A ==> A =~ { s | FINITE s /\ s SUBSET A }
3263Proof
3264 strip_tac >> match_mp_tac cardleq_ANTISYM >> conj_tac
3265 >- (simp[cardleq_def] >> qexists_tac `\a. {a}` >>
3266 simp[INJ_DEF]) >>
3267 ‘{s | FINITE s ∧ s ⊆ A} =
3268 BIGUNION (IMAGE (λn. { s | s ⊆ A ∧ s HAS_SIZE n }) univ(:num))’
3269 by (simp[Once EXTENSION, PULL_EXISTS, EQ_IMP_THM] >> rpt strip_tac >>
3270 gvs[HAS_SIZE]) >>
3271 simp[] >> irule CARD_BIGUNION >> simp[PULL_EXISTS] >> conj_tac >~
3272 [‘IMAGE _ _ ≼ A’]
3273 >- (irule IMAGE_cardleq_rwt >> gvs[INFINITE_Unum]) >>
3274 qx_gen_tac ‘n’ >> Cases_on ‘n = 0’
3275 >- (simp[HAS_SIZE_0, SF CONJ_ss] >> ‘A ≠ ∅’ by (strip_tac >> gvs[]) >>
3276 gvs[GSYM MEMBER_NOT_EMPTY] >> rename [‘a ∈ A’] >>
3277 simp[cardleq_def] >> qexists_tac ‘λx. a’ >> simp[INJ_DEF]) >>
3278 ‘0 < n’ by gvs[NOT_ZERO] >>
3279 drule_all_then (assume_tac o ONCE_REWRITE_RULE[cardeq_SYM])
3280 exp_count_cardeq >>
3281 resolve_then (Pos hd) (dxrule_then (irule o iffRL)) cardeq_REFL CARD_LE_CONG >>
3282 ‘∀s. s HAS_SIZE n ⇒ ∃f. SURJ f (count n) s ∧ ∀m. n ≤ m ⇒ f m = ARB’
3283 by (rpt (pop_assum kall_tac) >> simp[HAS_SIZE] >> qid_spec_tac ‘n’ >>
3284 Induct_on ‘FINITE’ >> simp[SURJ_EMPTY] >> rw[] >> simp[K_lemma] >>
3285 gvs[SURJ_DEF] >> rename [‘g _ ∈ A’, ‘e ∉ A’] >>
3286 qexists_tac
3287 ‘λn. if n < CARD A then g n else if n = CARD A then e else ARB’ >>
3288 simp[AllCaseEqs(), DISJ_IMP_THM, FORALL_AND_THM,
3289 DECIDE “x < SUC y ⇔ x = y ∨ x < y”] >>
3290 rw[] >> simp[SF ARITH_ss] >>
3291 metis_tac[LESS_REFL]) >>
3292 gvs[GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] >>
3293 rename [‘SURJ (FF _) (count n)’] >>
3294 simp[cardleq_def, INJ_DEF] >> qexists_tac ‘FF’ >> rw[] >~
3295 [‘FF A0 ∈ A ** count n’]
3296 >- (simp[set_exp_def] >> first_x_assum $ drule_then strip_assume_tac >>
3297 gvs[NOT_LESS, SURJ_DEF, SUBSET_DEF]) >>
3298 rename [‘A1 HAS_SIZE n’, ‘A2 HAS_SIZE n’, ‘FF A1 = FF A2’] >>
3299 CCONTR_TAC >>
3300 ‘∃a. a ∈ A1 ∧ a ∉ A2’
3301 suffices_by (strip_tac >>
3302 ‘∃i. FF A1 i = a ∧ i < n ∧ FF A2 i ≠ a’
3303 by metis_tac[SURJ_DEF]>>
3304 qpat_x_assum ‘FF A1 = FF A2’ mp_tac >>
3305 simp[FUN_EQ_THM] >> metis_tac[]) >>
3306 CCONTR_TAC >> gvs[] >> ‘A1 ⊆ A2’ by ASM_SET_TAC[] >>
3307 metis_tac[SUBSET_EQ_CARD, HAS_SIZE]
3308QED
3309
3310(* ------------------------------------------------------------------------- *)
3311(* Misc lemmas from HOL-Light's card.ml *)
3312(* ------------------------------------------------------------------------- *)
3313
3314Theorem MUL_C_UNIV = SYM CROSS_UNIV
3315Theorem CARD_MUL_FINITE_EQ = FINITE_CROSS_EQ
3316
3317Theorem INJECTIVE_ON_ALT :
3318 !P (f :'a -> 'b).
3319 (!x y. P x /\ P y /\ f x = f y ==> x = y) <=>
3320 (!x y. P x /\ P y ==> (f x = f y <=> x = y))
3321Proof
3322 MESON_TAC[]
3323QED
3324
3325Theorem INJECTIVE_ALT :
3326 !f :'a -> 'b. (!x y. f x = f y ==> x = y) <=> (!x y. f x = f y <=> x = y)
3327Proof
3328 MESON_TAC[]
3329QED