cardinalScript.sml
1Theory cardinal[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 = simpLib.ASM_SIMP_TAC (srw_ss()) ths
10fun csimp ths = simp(SF CONJ_ss::ths)
11fun dsimp ths = simp(SF DNF_ss::ths)
12fun gvs ths = simpLib.global_simp_tac
13 {elimvars = true, strip = true,
14 droptrues = true, oldestfirst = true}
15 (srw_ss()) ths
16fun gs ths = simpLib.global_simp_tac
17 {elimvars = false, strip = true,
18 droptrues = true, oldestfirst = true}
19 (srw_ss()) ths
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 "𝟚" = “{T;F}”
36Overload "ℵ₀" = “univ(:num)”
37
38Definition cardeq_def:
39 cardeq s1 s2 <=> ?f. BIJ f s1 s2
40End
41val _ = set_fixity "=~" (Infix(NONASSOC, 450));
42val _ = Unicode.unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
43val _ = TeX_notation {hol = "=~", TeX = ("\\ensuremath{\\approx}", 1)};
44val _ = TeX_notation {hol = UTF8.chr 0x2248, TeX = ("\\ensuremath{\\approx}", 1)};
45
46Overload "=~" = ``cardeq``
47
48Overload "≉" = “λa b. ¬(a ≈ b)”
49val _ = 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 "<<=" = ``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 _ = set_fixity "<</=" (Infix(NONASSOC, 450));
310
311val _ = Unicode.unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
312val _ = TeX_notation {hol = "<</=", TeX = ("\\ensuremath{\\prec}", 1)};
313val _ = TeX_notation {hol = UTF8.chr 0x227A, TeX = ("\\ensuremath{\\prec}", 1)};
314
315Overload cardlt = ``\s1 s2. ~(cardleq s2 s1)``(* cardlt *)
316Overload "<</=" = ``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
755Overload "**" = “set_exp”
756
757Theorem exp_c :
758 !(s :'a set) (t :'b set).
759 s ** t =
760 {f | (!x. x IN t ==> f x IN s) /\ (!x. ~(x IN t) ==> f x = ARB)}
761Proof
762 rw [set_exp_def, Once EXTENSION]
763QED
764
765Theorem UNIV_fun_exp:
766 univ(:'a -> 'b) = univ(:'b) ** univ(:'a)
767Proof
768 simp[set_exp_def]
769QED
770
771(* |- univ(:'b) ** univ(:'a) = univ(:'a -> 'b) *)
772Theorem CARD_EXP_UNIV = GSYM UNIV_fun_exp
773
774Theorem BIJ_functions_agree:
775 !f g s t. BIJ f s t /\ (!x. x IN s ==> (f x = g x)) ==> BIJ g s t
776Proof
777 simp[BIJ_DEF, SURJ_DEF, INJ_DEF] >> rw[] >>
778 full_simp_tac (srw_ss() ++ boolSimps.CONJ_ss) []
779QED
780
781Theorem CARD_CARDEQ_I:
782 FINITE s1 /\ FINITE s2 /\ (CARD s1 = CARD s2) ==> s1 =~ s2
783Proof
784 Cases_on `FINITE s1` >> simp[] >> qid_spec_tac `s2` >> pop_assum mp_tac >>
785 qid_spec_tac `s1` >> ho_match_mp_tac FINITE_INDUCT >> simp[] >> conj_tac
786 >- metis_tac [CARD_EQ_0, cardeq_REFL, CARDEQ_0] >>
787 qx_gen_tac `s1` >> strip_tac >> qx_gen_tac `a` >> strip_tac >>
788 qx_gen_tac `s2` >>
789 ‘(s2 = {}) \/ ?b s. (s2 = b INSERT s) /\ b NOTIN s’
790 by metis_tac [SET_CASES] >>
791 csimp[] >> strip_tac >> `s1 =~ s` by metis_tac[] >>
792 `?f. BIJ f s1 s` by metis_tac [cardeq_def] >>
793 simp[cardeq_def] >> qexists_tac `\x. if x = a then b else f x` >>
794 simp[BIJ_INSERT] >>
795 `(b INSERT s) DELETE b = s` by (simp[EXTENSION] >> metis_tac[]) >>
796 match_mp_tac BIJ_functions_agree >> qexists_tac `f` >> rw[]
797QED
798
799Theorem CARDEQ_CARD_EQN:
800 FINITE s1 /\ FINITE s2 ==> (s1 =~ s2 <=> (CARD s1 = CARD s2))
801Proof
802 metis_tac [CARD_CARDEQ_I, CARDEQ_CARD]
803QED
804
805Theorem CARDLEQ_CARD:
806 FINITE s1 /\ FINITE s2 ==> (s1 <<= s2 <=> CARD s1 <= CARD s2)
807Proof
808 rw[EQ_IMP_THM] >-
809 metis_tac[cardleq_def,INJ_CARD] >>
810 Cases_on`CARD s1 = CARD s2` >-
811 metis_tac[cardleq_lteq,CARDEQ_CARD_EQN] >>
812 simp[Once cardleq_lteq] >> disj1_tac >>
813 simp[cardleq_def] >>
814 gen_tac >> match_mp_tac PHP >>
815 srw_tac[ARITH_ss][]
816QED
817
818Theorem CARD_LT_CARD:
819 FINITE s1 /\ FINITE s2 ==> (s1 <</= s2 <=> CARD s1 < CARD s2)
820Proof
821 rw[] >> simp[cardlt_lenoteq,CARDLEQ_CARD,CARDEQ_CARD_EQN, SF ARITH_ss]
822QED
823
824Theorem EMPTY_set_exp:
825 A ** {} = { K ARB } /\ (B <> {} ==> {} ** B = {})
826Proof
827 simp[set_exp_def] >> conj_tac >- simp[EXTENSION, FUN_EQ_THM] >>
828 strip_tac >> qsuff_tac `(!b. b NOTIN B) = F`
829 >- (disch_then SUBST_ALL_TAC >> simp[]) >>
830 gvs[EXTENSION] >> metis_tac[]
831QED
832
833Theorem EMPTY_set_exp_CARD:
834 A ** {} =~ count 1
835Proof
836 simp[EMPTY_set_exp, CARDEQ_CARD_EQN]
837QED
838
839Theorem SING_set_exp:
840 {x} ** B = { (\b. if b IN B then x else ARB) } /\
841 A ** {x} = { (\b. if b = x then a else ARB) | a IN A }
842Proof
843 rw[set_exp_def, EXTENSION] >> rw[FUN_EQ_THM, EQ_IMP_THM] >> rw[] >>
844 metis_tac[]
845QED
846
847Theorem SING_set_exp_CARD:
848 {x} ** B =~ count 1 /\ A ** {x} =~ A
849Proof
850 simp[SING_set_exp, CARDEQ_CARD_EQN] >> simp[Once cardeq_SYM] >>
851 simp[cardeq_def] >> qexists `\a b. if b = x then a else ARB` >>
852 qmatch_abbrev_tac `BIJ f A s` >>
853 qsuff_tac `s = IMAGE f A`
854 >- (rw[] >> match_mp_tac (GEN_ALL INJ_BIJ_SUBSET) >>
855 map_every qexists_tac [`IMAGE f A`, `A`] >> rw[INJ_DEF, Abbr`f`]
856 >- metis_tac[]
857 >> (gvs[FUN_EQ_THM] >> first_x_assum (qspec_then `x` mp_tac) >> simp[])) >>
858 rw[Abbr`s`, Abbr`f`, EXTENSION]
859QED
860
861Theorem POW_TWO_set_exp:
862 POW A =~ count 2 ** A
863Proof
864 simp[POW_DEF, set_exp_def, BIJ_IFF_INV, cardeq_def] >>
865 qexists_tac `\s a. if a IN A then if a IN s then 1 else 0
866 else ARB` >> simp[] >> conj_tac
867 >- (qx_gen_tac `s` >> strip_tac >> qx_gen_tac `b` >> strip_tac >>
868 Cases_on `b IN s` >> simp[]) >>
869 qexists `\f. { a | a IN A /\ f a = 1 }` >> simp[] >> rpt conj_tac
870 >- simp[SUBSET_DEF]
871 >- (qx_gen_tac `s` >> csimp[] >> simp[EXTENSION, SUBSET_DEF] >>
872 rw[] >> rw[]) >>
873 qx_gen_tac `f` >> simp[FUN_EQ_THM] >> strip_tac >> qx_gen_tac `a` >>
874 Cases_on `a IN A` >> simp[] >>
875 `?n. n < 2 /\ (f a = n)` by metis_tac[] >>
876 rw[] >> DECIDE_TAC
877QED
878
879Theorem set_exp_card_cong:
880 (a1:'a1 set) =~ (a2:'a2 set) ==> (b1:'b1 set) =~ (b2:'b2 set) ==>
881 (a1 ** b1 =~ a2 ** b2)
882Proof
883 rw[cardeq_def, BIJ_IFF_INV] >>
884 rename [‘_ IN a1 ** b1 ==> _ IN a2 ** b2’,
885 ‘_ IN a1 ==> rf1 _ IN a2’, ‘_ IN a2 ==> rf2 _ IN a1’,
886 ‘_ IN b1 ==> df1 _ IN b2’, ‘_ IN b2 ==> df2 _ IN b1’] >>
887 qexists ‘λf b. if b IN b2 then
888 if f (df2 b) IN a1 then rf1 $ f $ df2 b else ARB
889 else ARB’ >>
890 simp[set_exp_def, FUN_EQ_THM] >>
891 qexists ‘λg b. if b IN b1 then
892 if g (df1 b) IN a2 then rf2 $ g $ df1 b else ARB
893 else ARB’ >>
894 simp[] >> metis_tac[]
895QED
896
897Theorem set_exp_cardle_cong:
898 (b = {} ==> d = {}) ==>
899 (a:'a set) <<= (b:'b set) /\ (c:'c set) <<= (d:'d set) ==>
900 a ** c <<= b ** d
901Proof
902 simp[set_exp_def, cardleq_def] >> strip_tac >>
903 disch_then (CONJUNCTS_THEN2 (qx_choose_then `abf` assume_tac)
904 (qx_choose_then `cdf` assume_tac)) >>
905 qexists ‘
906 λcaf di. if di IN d then
907 case some ci. ci IN c /\ (cdf ci = di) of
908 NONE => CHOICE b
909 | SOME ci => abf (caf ci)
910 else ARB
911 ’ >>
912 Cases_on ‘b = {}’ >> gvs[]
913 >- simp[INJ_DEF, FUN_EQ_THM] >>
914 rw[INJ_DEF]
915 >- (rename [‘_ IN c /\ cdf _ = di’] >>
916 DEEP_INTRO_TAC some_intro >> simp[] >>
917 rpt strip_tac >- metis_tac[INJ_DEF] >>
918 simp[CHOICE_DEF]) >>
919 rename [‘caf1 = caf2’] >> simp[FUN_EQ_THM] >>
920 qx_gen_tac ‘ci’ >> Cases_on‘ci IN c’ >> simp[] >>
921 ‘cdf ci IN d’ by metis_tac[INJ_DEF] >>
922 ‘(some ci'. ci' IN c /\ (cdf ci' = cdf ci)) = SOME ci’
923 by (DEEP_INTRO_TAC some_intro >> simp[] >>
924 metis_tac[INJ_DEF]) >>
925 first_assum (fn th => Q_TAC (mp_tac o AP_THM th) ‘cdf ci’) >> BETA_TAC >>
926 simp[] >> metis_tac[INJ_DEF]
927QED
928
929Theorem exp_INSERT_cardeq:
930 e NOTIN s ==> (A ** (e INSERT s) =~ A CROSS A ** s)
931Proof
932 simp[set_exp_def, cardeq_def] >> strip_tac >> simp[BIJ_IFF_INV] >>
933 qexists_tac ‘\f. (f e, (λa. if a = e then ARB else f a))’ >> conj_tac
934 >- (qx_gen_tac `f` >> strip_tac >> simp[] >> metis_tac[]) >>
935 qexists ‘λ(a1,f) a2. if a2 = e then a1 else f a2’ >>
936 simp[pairTheory.FORALL_PROD] >> rpt conj_tac
937 >- (rw[] >> rw[])
938 >- (qx_gen_tac `f` >> strip_tac >> simp[FUN_EQ_THM] >> qx_gen_tac `a` >>
939 simp[AllCaseEqs()]) >>
940 rw[FUN_EQ_THM] >> rw[]
941QED
942
943Theorem exp_count_cardeq:
944 INFINITE A /\ 0 < n ==> A ** count n =~ A
945Proof
946 strip_tac >> Induct_on `n` >> simp[] >>
947 `(n = 0) \/ ?m. n = SUC m` by (Cases_on `n` >> simp[])
948 >- simp[COUNT_ONE, SING_set_exp_CARD] >>
949 simp_tac (srw_ss()) [COUNT_SUC] >>
950 `A ** (n INSERT count n) =~ A CROSS A ** count n`
951 by simp[exp_INSERT_cardeq] >>
952 `A ** count n =~ A` by simp[] >>
953 `A CROSS A ** count n =~ A CROSS A` by metis_tac[CARDEQ_CROSS, cardeq_REFL] >>
954 `A CROSS A =~ A` by simp[SET_SQUARED_CARDEQ_SET] >>
955 metis_tac [cardeq_TRANS]
956QED
957
958Theorem K_lemma[local]:
959 (!x. f x = y) <=> f = K y
960Proof
961 simp[FUN_EQ_THM]
962QED
963
964Theorem finite_image_lemma[local]:
965 !A. FINITE (IMAGE f A) /\ (!x y. x IN A /\ y IN A /\ f x = f y ==> x = y) ==>
966 FINITE A
967Proof
968 Induct_on ‘FINITE’ >> simp[] >> rw[] >>
969 rename [‘IMAGE f A = e0 INSERT A0’] >>
970 ‘?e. e IN A /\ f e = e0’
971 by (qpat_x_assum ‘IMAGE f A = _’ mp_tac >> simp[EXTENSION] >> metis_tac[])>>
972 ‘IMAGE f (A DELETE e) = A0’
973 by (qpat_x_assum ‘IMAGE f A = _’ mp_tac >> simp[EXTENSION] >> metis_tac[])>>
974 ‘FINITE (A DELETE e)’ suffices_by simp[] >>
975 first_x_assum irule >> simp[]
976QED
977
978Theorem FINITE_setexp[simp]:
979 FINITE ((A:'a set) ** (B:'b set)) <=>
980 B = {} \/ A <<= {()} \/ FINITE A /\ FINITE B
981Proof
982 simp[set_exp_def, EQ_IMP_THM] >> rpt strip_tac >> gvs[K_lemma]
983 >- (Cases_on ‘B = {}’ >> simp[] >>
984 Cases_on ‘A = {}’ >> gvs[] >>
985 Cases_on ‘?a. A = {a}’ >> gvs[]
986 >- (simp[cardleq_def] >> disj1_tac >> qexists_tac ‘K ()’ >>
987 simp[INJ_IFF]) >> disj2_tac >>
988 ‘?a1 a2. a1 <> a2 /\ a1 IN A /\ a2 IN A’
989 by (pop_assum mp_tac >> simp[EXTENSION] >> gs[GSYM MEMBER_NOT_EMPTY] >>
990 metis_tac[]) >> conj_tac
991 >- (CCONTR_TAC >>
992 qpat_x_assum ‘FINITE _’ mp_tac >> simp[] >>
993 ‘?b. b IN B’ by simp[MEMBER_NOT_EMPTY] >>
994 qabbrev_tac ‘ff = λa b. if b IN B then a else ARB’ >>
995 ‘(!a1 a2. ff a1 = ff a2 ==> a1 = a2)’
996 by (simp[Abbr‘ff’, FUN_EQ_THM, AllCaseEqs()] >> metis_tac[]) >>
997 drule_then (drule_then assume_tac) IMAGE_11_INFINITE >>
998 qmatch_abbrev_tac ‘INFINITE s’ >>
999 ‘IMAGE ff A SUBSET s’ suffices_by metis_tac[SUBSET_FINITE] >>
1000 simp[Abbr‘ff’, Abbr‘s’, SUBSET_DEF, PULL_EXISTS]) >>
1001 CCONTR_TAC >> qpat_x_assum ‘FINITE _’ mp_tac >> simp[] >>
1002 qabbrev_tac ‘ff = λb1 b2. if b1 NOTIN B then ARB
1003 else if b2 NOTIN B then ARB
1004 else if b1 = b2 then a2 else a1’ >>
1005 ‘(!b1 b2. b1 IN B /\ b2 IN B /\ ff b1 = ff b2 ==> b1 = b2)’
1006 by (simp[Abbr‘ff’, FUN_EQ_THM, SF CONJ_ss] >>
1007 rpt strip_tac >> CCONTR_TAC >>
1008 first_x_assum $ qspec_then‘b1’ mp_tac >> simp[]) >>
1009 drule_at (Pos last) finite_image_lemma >> simp[] >> strip_tac >>
1010 qmatch_abbrev_tac ‘INFINITE s’ >>
1011 ‘IMAGE ff B SUBSET s’ suffices_by metis_tac[SUBSET_FINITE] >>
1012 first_x_assum $ qspecl_then [‘ARB : 'b’, ‘ARB : 'b’] kall_tac >>
1013 simp[Abbr‘ff’, Abbr‘s’, SUBSET_DEF, PULL_EXISTS, AllCaseEqs()] >>
1014 metis_tac[])
1015 >- (Cases_on ‘A = {}’ >> gvs[]
1016 >- (csimp[K_lemma] >> Cases_on ‘!b. b NOTIN B’ >> simp[]) >>
1017 ‘?a. A = {a}’
1018 by (gs[cardleq_def, INJ_IFF, GSYM MEMBER_NOT_EMPTY] >>
1019 rename [‘a IN A’] >> qexists_tac ‘a’ >> simp[EXTENSION] >>
1020 metis_tac[]) >>
1021 gvs[] >> qmatch_abbrev_tac ‘FINITE s’ >>
1022 ‘s = {λb. if b IN B then a else ARB}’ suffices_by simp[] >>
1023 simp[Abbr‘s’, Once FUN_EQ_THM, AllCaseEqs(), EQ_IMP_THM] >>
1024 rpt strip_tac >> csimp[FUN_EQ_THM, AllCaseEqs()])
1025 >- (‘FINITE (A CROSS B)’ by simp[] >>
1026 ‘FINITE (POW (A CROSS B))’ by simp[] >>
1027 first_assum $ C (resolve_then (Pos hd) irule) CARDLEQ_FINITE >>
1028 simp[INJ_IFF, cardleq_def, IN_POW, SUBSET_DEF, FORALL_PROD] >>
1029 qexists_tac ‘λf. { (a,b) | b IN B /\ f b = a }’ >>
1030 simp[] >> rw[] >~
1031 [‘GSPEC _ = GSPEC _ <=> _ = _’]
1032 >- (simp[EXTENSION] >> simp[FUN_EQ_THM, FORALL_PROD] >>
1033 simp[Once EQ_IMP_THM] >> rw[] >> rename [‘f1 a = f2 a’] >>
1034 metis_tac[]) >>
1035 metis_tac[])
1036QED
1037
1038Theorem CARD_LE_EXP:
1039 {T; F} <<= B ==> (A:'a set) <<= (B:'b set) ** A
1040Proof
1041 simp[cardleq_def, set_exp_def, INJ_IFF] >>
1042 disch_then $ qx_choose_then ‘bf’ strip_assume_tac >>
1043 qexists_tac ‘λa1 a2. if a1 = a2 then bf T
1044 else if a2 IN A then bf F
1045 else ARB’ >>
1046 simp[] >> rw[]
1047 >- rw[]
1048 >- metis_tac[] >>
1049 simp[EQ_IMP_THM] >>
1050 disch_then (assume_tac o SRULE[FUN_EQ_THM]) >>
1051 pop_assum $ qspec_then ‘x’ mp_tac >> simp[] >> rw[]
1052QED
1053
1054Theorem INFINITE_Unum:
1055 INFINITE A <=> univ(:num) <<= A
1056Proof
1057 simp[infinite_num_inj, cardleq_def]
1058QED
1059
1060Theorem cardleq_SURJ:
1061 A <<= B <=> (?f. SURJ f B A) \/ (A = {})
1062Proof
1063 simp[cardleq_def, EQ_IMP_THM] >>
1064 metis_tac [SURJ_INJ_INV, inj_surj, INJ_EMPTY]
1065QED
1066
1067Theorem INFINITE_cardleq_INSERT:
1068 INFINITE A ==> (x INSERT s <<= A <=> s <<= A)
1069Proof
1070 simp[cardleq_def, INJ_INSERT, EQ_IMP_THM] >> strip_tac >> conj_tac
1071 >- metis_tac[] >>
1072 disch_then (Q.X_CHOOSE_THEN `f` strip_assume_tac) >>
1073 Cases_on `x IN s` >- (qexists_tac `f` >> gvs[INJ_DEF]) >>
1074 Q.UNDISCH_THEN `INFINITE A` mp_tac >>
1075 simp[INFINITE_Unum, cardleq_def] >>
1076 disch_then (Q.X_CHOOSE_THEN `g` assume_tac) >>
1077 qexists_tac `\y. if y = x then g 0
1078 else case some n. f y = g n of
1079 NONE => f y
1080 | SOME m => g (m + 1)` >>
1081 rpt conj_tac
1082 >- (simp[INJ_DEF] >> conj_tac
1083 >- (qx_gen_tac `y` >> strip_tac >> rw[] >- gvs[] >>
1084 Cases_on `some n. f y = g n` >> gvs[INJ_DEF]) >>
1085 map_every qx_gen_tac [`i`, `j`] >> strip_tac >> Cases_on `i = x` >>
1086 Cases_on `j = x` >> simp[]
1087 >- (DEEP_INTRO_TAC some_intro >> simp[] >> gvs[INJ_DEF])
1088 >- (DEEP_INTRO_TAC some_intro >> simp[] >> gvs[INJ_DEF]) >>
1089 ntac 2 (DEEP_INTRO_TAC some_intro) >> simp[] >>
1090 gvs[INJ_DEF] >> qx_gen_tac `m` >> strip_tac >>
1091 qx_gen_tac `n` >> rpt strip_tac >>
1092 metis_tac [DECIDE ``(n + 1 = m + 1) <=> (m = n)``])
1093 >- gvs[INJ_DEF] >>
1094 qx_gen_tac `y` >> simp[] >> Cases_on `x = y` >> simp[] >>
1095 Cases_on `y IN s` >> simp[] >> DEEP_INTRO_TAC some_intro >>
1096 simp[] >> gvs[INJ_DEF] >> metis_tac [DECIDE ``0 <> n + 1``]
1097QED
1098
1099Theorem CARDEQ_CROSS_1:
1100 {x} CROSS A =~ A /\ A CROSS {x} =~ A
1101Proof
1102 simp[cardeq_def] >> conj_tac >| [qexists ‘SND’, qexists ‘FST’] >>
1103 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD]
1104QED
1105
1106fun qxchl qs thtac = case qs of [] => thtac
1107 | q::rest => Q.X_CHOOSE_THEN q (qxchl rest thtac)
1108
1109
1110Theorem disjoint_countable_decomposition:
1111 !s. INFINITE s ==>
1112 ?A. (BIGUNION A = s) /\
1113 (!a. a IN A ==> INFINITE a /\ countable a) /\
1114 !a1 a2. a1 IN A /\ a2 IN A /\ a1 <> a2 ==> DISJOINT a1 a2
1115Proof
1116 rpt strip_tac >>
1117 qabbrev_tac `
1118 Ds = { D | BIGUNION D SUBSET s /\
1119 (!d. d IN D ==> INFINITE d /\ countable d) /\
1120 !d1 d2. d1 IN D /\ d2 IN D /\ d1 <> d2 ==> DISJOINT d1 d2}` >>
1121 `?f. INJ f univ(:num) s` by metis_tac [infinite_num_inj] >>
1122 qabbrev_tac `s_nums = IMAGE f univ(:num)` >>
1123 `{s_nums} IN Ds`
1124 by (markerLib.WITHOUT_ABBREVS (simp[]) >> simp[Abbr`s_nums`] >>
1125 conj_tac >- (gvs[SUBSET_DEF, INJ_DEF] >> metis_tac[])>>
1126 gvs[FINITE_IMAGE_INJ', INJ_IFF]) >>
1127 `Ds <> {}` by (simp[EXTENSION] >>metis_tac[]) >>
1128 qabbrev_tac `R = {(D1,D2) | D1 IN Ds /\ D2 IN Ds /\ D1 SUBSET D2}` >>
1129 `partial_order R Ds`
1130 by (simp[Abbr`R`, partial_order_def, domain_def, range_def, reflexive_def,
1131 transitive_def, antisym_def] THEN REPEAT CONJ_TAC
1132 THENL [
1133 simp[SUBSET_DEF] >> metis_tac[],
1134 simp[SUBSET_DEF] >> metis_tac[],
1135 metis_tac[SUBSET_TRANS],
1136 metis_tac[SUBSET_ANTISYM]
1137 ]) >>
1138 `!t. chain t R ==> upper_bounds t R <> {}`
1139 by (simp[Abbr`R`, upper_bounds_def, chain_def] >>
1140 simp[Once EXTENSION, range_def] >>
1141 qx_gen_tac `t` >> strip_tac >>
1142 qabbrev_tac `UBD =BIGUNION t` >>
1143 qexists_tac `UBD` >>
1144 `UBD IN Ds`
1145 by (markerLib.WITHOUT_ABBREVS (simp[]) >>
1146 conj_tac
1147 >- (simp[BIGUNION_SUBSET, Abbr`UBD`] >>
1148 qx_gen_tac `s0` >>
1149 disch_then (qxchl [`t0`] strip_assume_tac) >>
1150 `t0 IN Ds` by metis_tac[] >> pop_assum mp_tac >>
1151 markerLib.WITHOUT_ABBREVS (simp[]) >>
1152 simp[BIGUNION_SUBSET]) >>
1153 conj_tac
1154 >- (qx_gen_tac `s0` >>
1155 disch_then (qxchl [`t0`] strip_assume_tac) >>
1156 `t0 IN Ds` by metis_tac[] >> pop_assum mp_tac >>
1157 markerLib.WITHOUT_ABBREVS (simp[])) >>
1158 map_every qx_gen_tac [`d1`, `d2`] >>
1159 disch_then (CONJUNCTS_THEN2
1160 (qxchl [`t1`] strip_assume_tac)
1161 (CONJUNCTS_THEN2
1162 (qxchl [`t2`] strip_assume_tac)
1163 assume_tac)) >>
1164 `t1 IN Ds /\ t2 IN Ds` by metis_tac[] >>
1165 ntac 2 (pop_assum mp_tac) >>
1166 markerLib.WITHOUT_ABBREVS (simp[]) >>
1167 simp[BIGUNION_SUBSET] >>
1168 `t1 SUBSET t2 \/ t2 SUBSET t1` suffices_by
1169 metis_tac[SUBSET_DEF] >>
1170 metis_tac[]) >>
1171 simp[] >> conj_tac >- (qexists_tac `UBD` >> simp[]) >>
1172 qx_gen_tac `t0` >> Cases_on `t0 IN t` >> simp[] >>
1173 `t0 IN Ds` by metis_tac[] >> simp[] >>
1174 pop_assum mp_tac >> markerLib.WITHOUT_ABBREVS (simp[]) >>
1175 simp[Abbr`UBD`, BIGUNION_SUBSET] >> strip_tac >>
1176 simp[SUBSET_DEF] >> metis_tac[]) >>
1177 `?M. M IN maximal_elements Ds R` by metis_tac [zorns_lemma] >>
1178 pop_assum mp_tac >> simp[maximal_elements_def] >> strip_tac >>
1179 Q.UNDISCH_THEN `M IN Ds` (fn th => mp_tac th >> assume_tac th) >>
1180 markerLib.WITHOUT_ABBREVS (simp_tac (srw_ss()) []) >> strip_tac >>
1181 Cases_on `BIGUNION M = s` >- metis_tac[] >>
1182 `M <> {}`
1183 by (strip_tac >>
1184 `(M,{s_nums}) IN R` by (simp[Abbr`R`] >> gvs[]) >>
1185 `M = {s_nums}` by metis_tac[] >> gvs[]) >>
1186 Cases_on `FINITE (s DIFF BIGUNION M)`
1187 >- (`?M0. M0 IN M` by metis_tac [IN_INSERT, SET_CASES] >>
1188 qexists_tac `(M0 UNION (s DIFF BIGUNION M)) INSERT (M DELETE M0)` >>
1189 dsimp[finite_countable] >> rpt strip_tac >| [
1190 simp[Once EXTENSION] >> qx_gen_tac `e` >> eq_tac
1191 >- (strip_tac >> gvs[BIGUNION_SUBSET] >>
1192 metis_tac [SUBSET_DEF]) >>
1193 simp[] >> Cases_on `e IN M0` >> simp[] >>
1194 Cases_on `e IN BIGUNION M` >> pop_assum mp_tac >> simp[] >>
1195 metis_tac[],
1196 `a2 SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1197 simp[DISJOINT_DEF, EXTENSION] >> qx_gen_tac `e` >>
1198 Cases_on `e IN s` >> simp[] >> Cases_on `e IN a2` >> simp[] >>
1199 `e IN BIGUNION M` by metis_tac[SUBSET_DEF] >>
1200 gvs[] >> metis_tac[],
1201 `a1 SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1202 simp[DISJOINT_DEF, EXTENSION] >> qx_gen_tac `e` >>
1203 Cases_on `e IN s` >> simp[] >> Cases_on `e IN a1` >> simp[] >>
1204 `e IN BIGUNION M` by metis_tac[SUBSET_DEF] >>
1205 gvs[] >> metis_tac[]
1206 ]) >>
1207 qabbrev_tac `M0 = s DIFF BIGUNION M` >>
1208 `?g. INJ g univ(:num) M0` by metis_tac[infinite_num_inj] >>
1209 qabbrev_tac`g_nums = IMAGE g univ(:num)` >>
1210 `INFINITE g_nums /\ countable g_nums`
1211 by (simp[Abbr`g_nums`] >> gvs[FINITE_IMAGE_INJ', INJ_IFF]) >>
1212 qabbrev_tac `M' = g_nums INSERT M` >>
1213 `g_nums SUBSET M0` by (simp[Abbr`g_nums`, SUBSET_DEF] >>
1214 full_simp_tac(srw_ss() ++ DNF_ss)[INJ_DEF]) >>
1215 `M' IN Ds`
1216 by (markerLib.WITHOUT_ABBREVS(simp[]) >> dsimp[] >>
1217 `M0 SUBSET s` by simp[Abbr`M0`] >>
1218 `g_nums SUBSET s` by metis_tac[SUBSET_TRANS] >> simp[] >>
1219 qmatch_abbrev_tac `PP /\ QQ` >>
1220 `PP` suffices_by metis_tac[DISJOINT_SYM] >>
1221 map_every markerLib.UNABBREV_TAC ["PP", "QQ"] >>
1222 qx_gen_tac `d2` >> strip_tac >> simp[DISJOINT_DEF, EXTENSION] >>
1223 qx_gen_tac `e` >> SPOSE_NOT_THEN STRIP_ASSUME_TAC >>
1224 `e IN M0 /\ e IN BIGUNION M` by metis_tac[IN_BIGUNION, SUBSET_DEF] >>
1225 metis_tac[IN_DIFF]) >>
1226 `(M,M') IN R` by simp[Abbr`R`, Abbr`M'`, SUBSET_DEF] >>
1227 `M = M'` by metis_tac[] >>
1228 `g_nums NOTIN M` suffices_by metis_tac[IN_INSERT] >> strip_tac >>
1229 `g_nums SUBSET BIGUNION M` by (simp[SUBSET_DEF] >> metis_tac[]) >>
1230 `g 0 IN g_nums` by simp[Abbr`g_nums`] >>
1231 metis_tac[IN_DIFF, SUBSET_DEF]
1232QED
1233
1234(* this proof inspired by one generated by DeepSeek in early January, 2025;
1235 original query was
1236 "prove that every infinite set can be partitioned into sets that are
1237 countably infinite"
1238
1239 natural language proof was pretty good, though it wanted to first well-
1240 order the infinite set (s), which is unnecessary given that you separately
1241 establish the bijection with s CROSS univ(:num).
1242
1243 I then asked it to render the proof in HOL4, which it did something along
1244 the lines of below. It invented plenty of theorem names. I've retained its
1245 comments. It's less than half the size of the one above that explicitly
1246 uses Zorn's Lemma.
1247*)
1248Theorem disjoint_countable_decomposition2:
1249 !s. INFINITE s ==>
1250 ?A. (BIGUNION A = s) /\
1251 (!a. a IN A ==> INFINITE a /\ countable a) /\
1252 pairwise (RC DISJOINT) A
1253Proof
1254 rpt strip_tac >>
1255
1256 (* Step 1: Establish cardinal equivalence |A| = |A × ℕ| *)
1257 ‘s =~ s CROSS univ(:num)’ by (
1258 irule cardleq_ANTISYM >> conj_tac >~
1259 [‘s <<= s CROSS univ(:num)’]
1260 >- (simp[cardleq_def] >> qexists_tac ‘\a. (a,0)’ >>
1261 simp[INJ_DEF]) >>
1262 ‘s CROSS univ(:num) <<= univ(:num) CROSS s’
1263 by (simp[cardleq_def] >> qexists_tac ‘λ(a,b). (b,a)’ >>
1264 simp[INJ_DEF, FORALL_PROD]) >>
1265 drule_then irule cardleq_TRANS >>
1266 irule CARD_MUL_ABSORB_LE >>
1267 metis_tac[INFINITE_Unum]
1268 ) >>
1269
1270 (* Step 2: Construct bijection *)
1271 qabbrev_tac ‘f = @f. BIJ f s (s CROSS univ(:num))’ >>
1272 ‘BIJ f s (s CROSS UNIV)’ by (
1273 simp[Abbr‘f’] >> SELECT_ELIM_TAC >>
1274 metis_tac[cardeq_def]
1275 ) >>
1276
1277 (* Step 3: Define partition as fibers *)
1278 qabbrev_tac ‘P = IMAGE (\a. {b | b IN s /\ ?n. f b = (a,n)}) s’ >>
1279
1280 (* Verification *)
1281 ‘BIGUNION P = s’ by (
1282 simp[Abbr`P`, Once EXTENSION, PULL_EXISTS, FORALL_PROD, EQ_IMP_THM] >>
1283 gvs[BIJ_DEF, FORALL_PROD, INJ_IFF, SURJ_DEF] >>
1284 metis_tac[pair_CASES, FST, PAIR]
1285 ) >>
1286 ‘pairwise (RC DISJOINT) P’ by (
1287 simp[Abbr‘P’, pairwise_def, PULL_EXISTS, relationTheory.RC_DEF] >>
1288 rw[] >> CCONTR_TAC >> gvs[DISJOINT_DEF, GSYM MEMBER_NOT_EMPTY]
1289 ) >>
1290 ‘!X. X IN P ==> INFINITE X /\ countable X’ by (
1291 simp[Abbr`P`] >> rw[] >~
1292 [‘INFINITE { b | b IN s /\ ?n. f b = (a,n) }(* g *)’]
1293 >- (
1294 drule_then (qx_choose_then ‘g’ strip_assume_tac) BIJ_INV >>
1295 gvs[FORALL_PROD] >>
1296 simp[infinite_num_inj] >> qexists_tac ‘λn. g (a,n)’ >>
1297 simp[INJ_DEF] >> gvs[BIJ_DEF, INJ_IFF]
1298 ) >>
1299 simp[countable_def] >> qexists_tac ‘SND o f’ >>
1300 gvs[INJ_IFF, BIJ_DEF, PULL_EXISTS, EQ_IMP_THM, SF CONJ_ss]
1301 ) >>
1302 metis_tac[]
1303QED
1304
1305Theorem count_cardle[simp]:
1306 count n <<= A <=> (FINITE A ==> n <= CARD A)
1307Proof
1308 simp[cardleq_def] >> Cases_on ‘FINITE A’ >> simp[]
1309 >- (eq_tac
1310 >- metis_tac[DECIDE “x:num <= y <=> ~(y < x)”, PHP, CARD_COUNT,
1311 FINITE_COUNT] >>
1312 metis_tac[FINITE_COUNT, CARDLEQ_CARD, cardleq_def, CARD_COUNT]) >>
1313 pop_assum mp_tac >> qid_spec_tac ‘A’ >> Induct_on ‘n’ >>
1314 simp[] >> rpt strip_tac >> simp[COUNT_SUC, INJ_INSERT] >>
1315 first_x_assum (drule_then strip_assume_tac) >>
1316 ‘?a. a IN A /\ !m. m < n ==> f m <> a’
1317 by (‘?a. a IN (A DIFF IMAGE f (count n))’
1318 suffices_by (simp[] >> metis_tac[]) >>
1319 irule INFINITE_INHAB >>
1320 metis_tac [IMAGE_FINITE, FINITE_COUNT, FINITE_DIFF_down]) >>
1321 qexists_tac ‘\m. if m < n then f m else a’ >> simp[] >> conj_tac
1322 >- gvs[INJ_DEF] >>
1323 rw[]
1324QED
1325
1326Theorem CANTOR[simp]:
1327 A <</= POW A
1328Proof
1329 strip_tac >> gvs[cardleq_def, INJ_IFF, IN_POW] >>
1330 qabbrev_tac ‘CS = {f s | s | s SUBSET A /\ f s NOTIN s}’ >>
1331 ‘!s. s IN CS <=> ?t. t SUBSET A /\ f t NOTIN t /\ (f t = s)’
1332 by (simp[Abbr`CS`] >> metis_tac[]) >>
1333 ‘CS SUBSET A’ by (simp[Abbr`CS`] >> ONCE_REWRITE_TAC[SUBSET_DEF] >>
1334 simp[PULL_EXISTS]) >>
1335 irule (DECIDE “(p ==> ~p) /\ (~p ==> p) ==> Q”) >>
1336 qexists_tac ‘f CS IN CS’ >> conj_tac >> strip_tac >>
1337 qpat_x_assum ‘!s. s IN CS <=> P’ (fn th => REWRITE_TAC [th]) >>
1338 csimp[] >> simp[] >> metis_tac[]
1339QED
1340
1341Theorem cardlt_cardle:
1342 A <</= B ==> A <<= B
1343Proof
1344 metis_tac[cardlt_lenoteq]
1345QED
1346
1347Theorem set_exp_product:
1348 (A ** B1) ** B2 =~ A ** (B1 CROSS B2)
1349Proof
1350 simp[cardeq_def] >>
1351 qexists ‘\cf bp. if bp IN B1 CROSS B2 then cf (SND bp) (FST bp) else ARB’ >>
1352 simp[BIJ_DEF, INJ_IFF, SURJ_DEF, set_exp_def, FORALL_PROD] >>
1353 rpt strip_tac >> simp[]
1354 >- (simp[FUN_EQ_THM, FORALL_PROD] >> iff_tac >> simp[] >> metis_tac[]) >>
1355 rename [‘uf (_,_) IN A’] >>
1356 qexists ‘\b2. if b2 IN B2 then
1357 \b1. if b1 IN B1 then uf(b1,b2) else ARB
1358 else ARB’ >> simp[] >>
1359 simp[FUN_EQ_THM, FORALL_PROD] >> metis_tac[]
1360QED
1361
1362Theorem CARD1_SING:
1363 (A:'a set) =~ {()} <=> ?a. A = {a}
1364Proof
1365 simp[cardeq_def, EQ_IMP_THM, PULL_EXISTS, BIJ_IFF_INV] >>
1366 rpt strip_tac
1367 >- (rename [‘g () IN A’] >> qexists_tac ‘g()’ >> simp[EXTENSION] >>
1368 metis_tac[]) >>
1369 qexists_tac ‘K a’ >> simp[]
1370QED
1371
1372Theorem cardleq_setexp:
1373 x <<= x ** e <=> x = {} \/ x =~ {()} \/ e <> {}
1374Proof
1375 Cases_on ‘x = {}’ >> simp[] >>
1376 Cases_on ‘e = {}’ >> simp[EMPTY_set_exp, CARD1_SING]
1377 >- (simp[INJ_IFF, EQ_IMP_THM, PULL_EXISTS] >> reverse (rpt strip_tac)
1378 >- (simp[INJ_IFF, cardleq_def] >> qexists_tac ‘λa. K ARB’ >> simp[]) >>
1379 gs[cardleq_def, INJ_IFF, GSYM MEMBER_NOT_EMPTY] >> simp[EXTENSION] >>
1380 metis_tac[]) >>
1381 simp[cardleq_def, INJ_IFF] >> gs[GSYM MEMBER_NOT_EMPTY] >>
1382 rename [‘X ** E’, ‘x IN X’, ‘e IN E’] >>
1383 qexists ‘λx0 e0. if e0 IN E then x0 else ARB’ >>
1384 simp[set_exp_def, FUN_EQ_THM] >> metis_tac[]
1385QED
1386
1387Theorem POW_EQ_X_EXP_X:
1388 INFINITE A ==> POW A =~ A ** A
1389Proof
1390 strip_tac >> irule cardleq_ANTISYM >> conj_tac
1391 >- (‘POW A =~ count 2 ** A’ by simp[POW_TWO_set_exp] >>
1392 ‘count 2 ** A <<= A ** A’
1393 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1394 irule set_exp_cardle_cong >> simp[]) >>
1395 ‘POW A =~ count 2 ** A’ by simp[POW_TWO_set_exp] >>
1396 ‘A ** A <<= count 2 ** A’
1397 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1398 ‘A <</= POW A’ by simp[] >>
1399 ‘A <<= POW A’ by simp[cardlt_cardle] >>
1400 ‘A ** A <<= POW A ** A’
1401 by metis_tac[set_exp_cardle_cong, cardleq_REFL, POW_EMPTY] >>
1402 ‘POW A ** A <<= count 2 ** A’ suffices_by metis_tac [cardleq_TRANS] >>
1403 ‘(count 2 ** A) ** A <<= count 2 ** A’
1404 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL, set_exp_card_cong] >>
1405 ‘count 2 ** (A CROSS A) <<= count 2 ** A’
1406 suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL, set_exp_product] >>
1407 irule set_exp_cardle_cong >> simp[] >> irule CARDEQ_SUBSET_CARDLEQ >>
1408 simp[SET_SQUARED_CARDEQ_SET]
1409QED
1410
1411Theorem setexp_eq_EMPTY[simp]:
1412 A ** B = {} <=> A = {} /\ B <> {}
1413Proof
1414 simp[set_exp_def] >> simp[SimpLHS, EXTENSION] >>
1415 simp[] >> eq_tac >> rpt strip_tac
1416 >- (Cases_on ‘B = {}’ >> gvs[]
1417 >- (pop_assum $ qspec_then ‘K ARB’ mp_tac >> simp[]) >>
1418 CCONTR_TAC >> gs[GSYM MEMBER_NOT_EMPTY] >>
1419 rename [‘_ IN B /\ _ NOTIN A’, ‘b IN B’, ‘a IN A’] >>
1420 first_x_assum $ qspec_then ‘λb0. if b0 IN B then a else ARB’ mp_tac>>
1421 csimp[] >> metis_tac[])
1422 >- (gvs[] >> pop_assum $ qspec_then ‘K ARB’ mp_tac >> simp[]) >>
1423 simp[] >> metis_tac[MEMBER_NOT_EMPTY]
1424QED
1425
1426Theorem FINITE_EXPONENT_SETEXP_UNCOUNTABLE:
1427 FINITE B /\ B <> {} /\ ~countable A ==>
1428 ~countable (A ** B)
1429Proof
1430 Induct_on ‘FINITE’ >> simp[] >> rpt strip_tac >>
1431 rename [‘A ** (e INSERT B) ’] >>
1432 ‘A ** (e INSERT B) =~ A CROSS (A ** B)’
1433 by simp[exp_INSERT_cardeq] >>
1434 drule_all (iffLR countable_cardeq) >> simp[cross_countable_IFF] >>
1435 rpt strip_tac >> gvs[CARDEQ_0, setexp_eq_EMPTY]
1436QED
1437
1438Theorem FINITE_EXPONENT_SETEXP_COUNTABLE:
1439 FINITE (B:'b set) ==>
1440 (countable ((A:'a set) ** B) <=> B = {} \/ countable A)
1441Proof
1442 simp[EQ_IMP_THM, IMP_CONJ_THM] >> conj_tac
1443 >- metis_tac[FINITE_EXPONENT_SETEXP_UNCOUNTABLE] >>
1444 ‘!(A:'a set) (B:'b set). FINITE B /\ countable A ==> countable (A ** B)’
1445 suffices_by (rw[] >> simp[EMPTY_set_exp]) >>
1446 Induct_on ‘FINITE’ >> simp[EMPTY_set_exp] >> rpt strip_tac >>
1447 ‘A ** (e INSERT B) =~ A CROSS (A ** B)’ by simp[exp_INSERT_cardeq] >>
1448 drule_then irule (iffRL countable_cardeq) >> simp[cross_countable_IFF]
1449QED
1450
1451Theorem FINITE_012:
1452 FINITE A ==> A = {} \/ A =~ {()} \/ 2 <= CARD A
1453Proof
1454 Induct_on ‘FINITE’ >> simp[] >> rw[] >> gvs[CARD1_SING, SF ARITH_ss]
1455QED
1456
1457(* cf. permutesTheory.permutes_alt_bijns *)
1458Definition bijns_def:
1459 bijns A = { f | BIJ f A A /\ !a. a NOTIN A ==> f a = a }
1460End
1461
1462Theorem bijns_alt_permutes:
1463 !f s. f IN bijns s <=> f permutes s
1464Proof
1465 simp[permutes_alt, bijns_def]
1466QED
1467
1468Theorem cardeq_bijns_cong:
1469 A =~ B ==> bijns A =~ bijns B
1470Proof
1471 strip_tac >> ONCE_REWRITE_TAC [cardeq_SYM] >>
1472 gvs[cardeq_def, bijns_def] >>
1473 RULE_ASSUM_TAC (REWRITE_RULE [BIJ_IFF_INV]) >> gvs[] >>
1474 qexists ‘\bf a. if a IN A then g (bf (f a)) else a’ >>
1475 ‘!a1 a2. a1 IN A /\ a2 IN A ==> (f a1 = f a2 <=> a1 = a2)’ by metis_tac[] >>
1476 ‘!b1 b2. b1 IN B /\ b2 IN B ==> (g b1 = g b2 <=> b1 = b2)’ by metis_tac[] >>
1477 simp[BIJ_DEF, INJ_IFF, SURJ_DEF] >> rpt strip_tac >> csimp[]
1478 >- metis_tac[]
1479 >- (simp[EQ_IMP_THM, FUN_EQ_THM] >> rw[] >>
1480 rename [‘bf1 b = bf2 b’] >> reverse (Cases_on ‘b IN B’) >> simp[] >>
1481 ‘b = f (g b)’ by metis_tac[] >> pop_assum SUBST1_TAC >>
1482 ‘g b IN A’ by metis_tac[] >> first_x_assum (qspec_then ‘g b’ mp_tac) >>
1483 simp[])
1484 >- metis_tac[]
1485 >- (simp[PULL_EXISTS] >> csimp[] >>
1486 rename [‘(ff:'a -> 'a) _ = ff _ <=> _’] >>
1487 qexists ‘\b. if b IN B then f (ff (g b)) else b’ >>
1488 simp[] >> rpt strip_tac >> csimp[] >> metis_tac[] >>
1489 simp[FUN_EQ_THM] >> metis_tac[])
1490QED
1491
1492Theorem bijections_cardeq:
1493 INFINITE s ==> bijns s =~ POW s
1494Proof
1495 strip_tac >>
1496 irule cardleq_ANTISYM >> conj_tac
1497 >- (‘POW s =~ s ** s’ by simp[POW_EQ_X_EXP_X] >>
1498 ‘bijns s <<= s ** s’ suffices_by metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1499 simp[cardleq_def] >>
1500 simp[bijns_def, BIJ_DEF, INJ_IFF, set_exp_def] >>
1501 qexists ‘λf x. if x IN s then f x else ARB’ >> simp[] >>
1502 rpt strip_tac >> simp[FUN_EQ_THM] >> metis_tac[]) >>
1503 ‘s =~ {T;F} CROSS s’ by simp[SET_SUM_CARDEQ_SET] >>
1504 ‘bijns s =~ bijns ({T;F} CROSS s)’ by metis_tac[cardeq_bijns_cong] >>
1505 ‘POW s <<= bijns ({T;F} CROSS s)’
1506 suffices_by metis_tac[CARDEQ_CARDLEQ,cardeq_REFL] >>
1507 simp[cardleq_def] >>
1508 qexists_tac ‘\ss (bool,a). if a IN s then if a IN ss then (bool,a)
1509 else (~bool,a)
1510 else (bool,a)’ >>
1511 simp[INJ_IFF, IN_POW, bijns_def, FORALL_PROD] >> rpt strip_tac
1512 >- (simp[BIJ_DEF, INJ_IFF, SURJ_DEF, FORALL_PROD] >> rpt strip_tac
1513 >- rw[]
1514 >- (rw[] >> metis_tac[])
1515 >- rw[] >>
1516 simp[pairTheory.EXISTS_PROD] >> csimp[] >>
1517 dsimp[AllCaseEqs()] >> metis_tac[]) >>
1518 simp[SimpLHS,FUN_EQ_THM] >> iff_tac >> rw[] >>
1519 simp[EXTENSION] >> qx_gen_tac `a` >> reverse (Cases_on `a IN s`)
1520 >- metis_tac[SUBSET_DEF] >>
1521 rename [‘a IN ss1 <=> a IN ss2’] >>
1522 Cases_on `a IN ss1` >> simp[]
1523 >- (first_x_assum (qspecl_then [‘T’, ‘a’] mp_tac) >> simp[] >> rw[])
1524 >- (first_x_assum (qspecl_then [‘F’, ‘a’] mp_tac) >> simp[] >> rw[])
1525QED
1526
1527(* ------------------------------------------------------------------------- *)
1528(* misc. *)
1529(* ------------------------------------------------------------------------- *)
1530
1531Theorem FORALL_IN_GSPEC :
1532 (!P f. (!z. z IN {f x | P x} ==> Q z) <=> (!x. P x ==> Q(f x))) /\
1533 (!P f. (!z. z IN {f x y | P x y} ==> Q z) <=>
1534 (!x y. P x y ==> Q(f x y))) /\
1535 (!P f. (!z. z IN {f w x y | P w x y} ==> Q z) <=>
1536 (!w x y. P w x y ==> Q(f w x y)))
1537Proof
1538 SRW_TAC [][] THEN SET_TAC []
1539QED
1540
1541Theorem EXISTS_IN_GSPEC :
1542 (!P f. (?z. z IN {f x | P x} /\ Q z) <=> (?x. P x /\ Q(f x))) /\
1543 (!P f. (?z. z IN {f x y | P x y} /\ Q z) <=>
1544 (?x y. P x y /\ Q(f x y))) /\
1545 (!P f. (?z. z IN {f w x y | P w x y} /\ Q z) <=>
1546 (?w x y. P w x y /\ Q(f w x y)))
1547Proof
1548 SRW_TAC [][] THEN SET_TAC []
1549QED
1550
1551Theorem LEFT_IMP_EXISTS_THM:
1552 !P Q. (?x. P x) ==> Q <=> (!x. P x ==> Q)
1553Proof
1554 SIMP_TAC std_ss [PULL_EXISTS]
1555QED
1556
1557Theorem LEFT_IMP_FORALL_THM:
1558 !P Q. (!x. P x) ==> Q <=> (?x. P x ==> Q)
1559Proof
1560 METIS_TAC [GSYM LEFT_FORALL_IMP_THM]
1561QED
1562
1563Theorem RIGHT_IMP_EXISTS_THM:
1564 !P Q. P ==> (?x. Q x) <=> (?x. P ==> Q x)
1565Proof
1566 REWRITE_TAC [GSYM RIGHT_EXISTS_IMP_THM]
1567QED
1568
1569Theorem RIGHT_IMP_FORALL_THM:
1570 !P Q. P ==> (!x. Q x) <=> (!x. P ==> Q x)
1571Proof
1572 REWRITE_TAC [GSYM RIGHT_FORALL_IMP_THM]
1573QED
1574
1575(* old name IMP_CONJ seems to be a conv function *)
1576Theorem CONJ_EQ_IMP :
1577 !p q r. p /\ q ==> r <=> p ==> q ==> r
1578Proof
1579 REWRITE_TAC [AND_IMP_INTRO]
1580QED
1581
1582Theorem IMP_CONJ_ALT :
1583 !p q r. p /\ q ==> r <=> q ==> p ==> r
1584Proof
1585 METIS_TAC [AND_IMP_INTRO]
1586QED
1587
1588Theorem lemma[local]:
1589 (!x. x IN s ==> (g(f(x)) = x)) <=>
1590 (!y x. x IN s /\ (y = f x) ==> (g y = x))
1591Proof
1592 MESON_TAC []
1593QED
1594
1595Theorem INJECTIVE_ON_LEFT_INVERSE:
1596 !f s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) <=>
1597 (?g. !x. x IN s ==> (g(f(x)) = x))
1598Proof
1599 REWRITE_TAC[lemma] THEN SIMP_TAC std_ss [GSYM SKOLEM_THM] THEN METIS_TAC[]
1600QED
1601
1602Theorem SURJECTIVE_ON_RIGHT_INVERSE:
1603 !f t. (!y. y IN t ==> ?x. x IN s /\ (f(x) = y)) <=>
1604 (?g. !y. y IN t ==> g(y) IN s /\ (f(g(y)) = y))
1605Proof
1606 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM]
1607QED
1608
1609Theorem SURJECTIVE_RIGHT_INVERSE:
1610 (!y. ?x. f(x) = y) <=> (?g. !y. f(g(y)) = y)
1611Proof
1612 MESON_TAC[SURJECTIVE_ON_RIGHT_INVERSE, IN_UNIV]
1613QED
1614
1615Theorem FINITE_IMAGE_INJ_GENERAL:
1616 !(f:'a->'b) A s.
1617 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
1618 FINITE A
1619 ==> (FINITE {x | x IN s /\ f(x) IN A})
1620Proof
1621 REPEAT STRIP_TAC THEN
1622 FULL_SIMP_TAC std_ss [INJECTIVE_ON_LEFT_INVERSE] THEN ASSUME_TAC SUBSET_FINITE
1623 THEN POP_ASSUM (MP_TAC o Q.SPEC `IMAGE (g:'b->'a) A`) THEN
1624 KNOW_TAC ``FINITE (IMAGE g A)`` THENL [METIS_TAC [IMAGE_FINITE], DISCH_TAC
1625 THEN FULL_SIMP_TAC std_ss [] THEN DISCH_TAC THEN
1626 POP_ASSUM (MP_TAC o Q.SPEC `{x | x IN s /\ f x IN A}`) THEN DISCH_TAC
1627 THEN KNOW_TAC ``{x | x IN s /\ f x IN A} SUBSET IMAGE g A`` THENL
1628 [REWRITE_TAC [IMAGE_DEF, SUBSET_DEF] THEN GEN_TAC THEN
1629 SIMP_TAC std_ss [GSPECIFICATION] THEN METIS_TAC [] , METIS_TAC []]]
1630QED
1631
1632Theorem FINITE_IMAGE_INJ:
1633 !(f:'a->'b) A. (!x y. (f(x) = f(y)) ==> (x = y)) /\
1634 FINITE A ==> FINITE {x | f(x) IN A}
1635Proof
1636 REPEAT GEN_TAC THEN
1637 MP_TAC(SPECL [``f:'a->'b``, ``A:'b->bool``, ``UNIV:'a->bool``]
1638 FINITE_IMAGE_INJ_GENERAL) THEN REWRITE_TAC[IN_UNIV]
1639QED
1640
1641Theorem INFINITE_IMAGE_INJ:
1642 !f:'a->'b. (!x y. (f x = f y) ==> (x = y)) ==>
1643 !s. INFINITE s ==> INFINITE(IMAGE f s)
1644Proof
1645 metis_tac[FINITE_IMAGE_INJ_EQ]
1646QED
1647
1648Theorem INFINITE_NONEMPTY:
1649 !s. INFINITE(s) ==> ~(s = EMPTY)
1650Proof MESON_TAC[FINITE_EMPTY]
1651QED
1652
1653Theorem SURJECTIVE_IMAGE_THM:
1654 !f:'a->'b. (!y. ?x. f x = y) <=> (!P. IMAGE f {x | P(f x)} = {x | P x})
1655Proof
1656 GEN_TAC THEN SIMP_TAC std_ss [EXTENSION, IN_IMAGE, GSPECIFICATION] THEN
1657 EQ_TAC THENL [ALL_TAC, DISCH_THEN(MP_TAC o SPEC ``\y:'b. T``)] THEN
1658 METIS_TAC[]
1659QED
1660
1661Theorem SURJECTIVE_ON_IMAGE:
1662 !f:'a->'b u v.
1663 (!t. t SUBSET v ==> ?s. s SUBSET u /\ (IMAGE f s = t)) <=>
1664 (!y. y IN v ==> ?x. x IN u /\ (f x = y))
1665Proof
1666 REPEAT GEN_TAC THEN EQ_TAC THENL
1667 [DISCH_TAC THEN X_GEN_TAC ``y:'b`` THEN DISCH_TAC THEN
1668 FIRST_X_ASSUM(MP_TAC o SPEC ``{y:'b}``) THEN ASM_SET_TAC[],
1669 DISCH_TAC THEN X_GEN_TAC ``t:'b->bool`` THEN DISCH_TAC THEN
1670 EXISTS_TAC ``{x | x IN u /\ (f:'a->'b) x IN t}`` THEN ASM_SET_TAC[]]
1671QED
1672
1673Theorem SURJECTIVE_IMAGE:
1674 !f:'a->'b. (!t. ?s. IMAGE f s = t) <=> (!y. ?x. f x = y)
1675Proof
1676 GEN_TAC THEN
1677 MP_TAC (ISPECL [``f:'a->'b``,``univ(:'a)``,``univ(:'b)``] SURJECTIVE_ON_IMAGE) THEN
1678 SIMP_TAC std_ss [IN_UNIV, SUBSET_UNIV]
1679QED
1680
1681Theorem CARD_LE_INJ:
1682 !s t.
1683 FINITE s /\ FINITE t /\ CARD s <= CARD t ==>
1684 ?f:'a->'b. (IMAGE f s) SUBSET t /\
1685 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)
1686Proof
1687 rpt strip_tac >> drule_all (iffRL CARDLEQ_CARD) >>
1688 simp[cardleq_def, INJ_IFF, PULL_EXISTS] >> qx_gen_tac ‘f’ >> strip_tac >>
1689 qexists ‘f’ >> csimp[SUBSET_DEF, PULL_EXISTS]
1690QED
1691
1692Theorem CARD_EQ_BIJECTION:
1693 !s t. FINITE s /\ FINITE t /\ (CARD s = CARD t)
1694 ==> ?f:'a->'b. (!x. x IN s ==> f(x) IN t) /\
1695 (!y. y IN t ==> ?x. x IN s /\ (f x = y)) /\
1696 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)
1697Proof
1698 MP_TAC CARD_LE_INJ THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
1699 POP_ASSUM (MP_TAC o SPECL [``s:'a->bool``,``t:'b->bool``]) THEN
1700 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN
1701 ASM_REWRITE_TAC[LESS_EQ_REFL] THEN DISCH_THEN (X_CHOOSE_TAC ``f:'a->'b``) THEN
1702 EXISTS_TAC ``f:'a->'b`` THEN POP_ASSUM MP_TAC THEN
1703 ASM_SIMP_TAC std_ss [SURJECTIVE_IFF_INJECTIVE_GEN] THEN
1704 MESON_TAC[SUBSET_DEF, IN_IMAGE]
1705QED
1706
1707Theorem CARD_EQ_BIJECTIONS:
1708 !s t. FINITE s /\ FINITE t /\ (CARD s = CARD t)
1709 ==> ?f:'a->'b g. (!x. x IN s ==> f(x) IN t /\ (g(f x) = x)) /\
1710 (!y. y IN t ==> g(y) IN s /\ (f(g y) = y))
1711Proof
1712 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CARD_EQ_BIJECTION) THEN
1713 DISCH_THEN (X_CHOOSE_TAC ``f:'a->'b``) THEN
1714 EXISTS_TAC ``f:'a->'b`` THEN POP_ASSUM MP_TAC THEN
1715 SIMP_TAC std_ss [SURJECTIVE_ON_RIGHT_INVERSE] THEN
1716 SIMP_TAC std_ss [GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM] THEN
1717 METIS_TAC[]
1718QED
1719
1720Theorem SING_SUBSET:
1721 !s x. {x} SUBSET s <=> x IN s
1722Proof
1723 SET_TAC[]
1724QED
1725
1726Theorem INJECTIVE_ON_IMAGE:
1727 !f:'a->'b u. (!s t. s SUBSET u /\ t SUBSET u /\
1728 (IMAGE f s = IMAGE f t) ==> (s = t)) <=>
1729 (!x y. x IN u /\ y IN u /\ (f x = f y) ==> (x = y))
1730Proof
1731 REPEAT GEN_TAC THEN EQ_TAC THENL
1732 [DISCH_TAC, SET_TAC[]] THEN MAP_EVERY X_GEN_TAC [``x:'a``, ``y:'a``] THEN
1733 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [``{x:'a}``, ``{y:'a}``]) THEN
1734 ASM_REWRITE_TAC[SING_SUBSET, IMAGE_EMPTY, IMAGE_INSERT] THEN SET_TAC[]
1735QED
1736
1737Theorem INJECTIVE_IMAGE:
1738 !f:'a->'b. (!s t. (IMAGE f s = IMAGE f t) ==> (s = t)) <=>
1739 (!x y. (f x = f y) ==> (x = y))
1740Proof
1741 GEN_TAC THEN MP_TAC(ISPECL [``f:'a->'b``, ``univ(:'a)``] INJECTIVE_ON_IMAGE) THEN
1742 REWRITE_TAC[IN_UNIV, SUBSET_UNIV]
1743QED
1744
1745Theorem FINITE_FINITE_BIGUNION[local]:
1746 !s. FINITE(s) ==> (FINITE(BIGUNION s) <=> (!t. t IN s ==> FINITE(t)))
1747Proof
1748 metis_tac[FINITE_BIGUNION_EQ]
1749QED
1750
1751(* ------------------------------------------------------------------------- *)
1752(* This is often more useful as a rewrite. *)
1753(* ------------------------------------------------------------------------- *)
1754
1755val lemma = SET_RULE ``!a s. a IN s ==> (s = a INSERT (s DELETE a))``;
1756
1757Theorem HAS_SIZE_CLAUSES:
1758 !s. (s HAS_SIZE 0 <=> (s = {})) /\
1759 (s HAS_SIZE (SUC n) <=>
1760 ?a t. t HAS_SIZE n /\ ~(a IN t) /\ (s = a INSERT t))
1761Proof
1762 REWRITE_TAC[HAS_SIZE_0] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL
1763 [REWRITE_TAC[HAS_SIZE_SUC, GSYM MEMBER_NOT_EMPTY] THEN
1764 MESON_TAC[lemma, IN_DELETE],
1765 SIMP_TAC std_ss [LEFT_IMP_EXISTS_THM, HAS_SIZE, CARD_EMPTY, CARD_INSERT,
1766 FINITE_INSERT]]
1767QED
1768
1769Theorem CARD_SUBSET_EQ:
1770 !(a:'a->bool) b. FINITE b /\ a SUBSET b /\ (CARD a = CARD b) ==> (a = b)
1771Proof
1772 REPEAT STRIP_TAC THEN
1773 MP_TAC(SPECL [``a:'a->bool``] CARD_UNION) THEN
1774 SUBGOAL_THEN ``FINITE(a:'a->bool)`` ASSUME_TAC THENL
1775 [METIS_TAC[SUBSET_FINITE_I], ALL_TAC] THEN ASM_REWRITE_TAC [] THEN
1776 DISCH_THEN (MP_TAC o SPEC ``b DIFF (a:'a->bool)``) THEN
1777 SUBGOAL_THEN ``FINITE(b:'a->bool DIFF a)`` ASSUME_TAC THENL
1778 [MATCH_MP_TAC SUBSET_FINITE_I THEN EXISTS_TAC ``b:'a->bool`` THEN
1779 ASM_REWRITE_TAC[] THEN SET_TAC[], ALL_TAC] THEN
1780 SUBGOAL_THEN ``a:'a->bool INTER (b DIFF a) = EMPTY`` ASSUME_TAC THENL
1781 [SET_TAC[], ALL_TAC] THEN
1782 ASM_REWRITE_TAC[] THEN
1783 SUBGOAL_THEN ``a UNION (b:'a->bool DIFF a) = b`` ASSUME_TAC THENL
1784 [UNDISCH_TAC ``a:'a->bool SUBSET b`` THEN SET_TAC[], ALL_TAC] THEN
1785 ASM_REWRITE_TAC[] THEN
1786 REWRITE_TAC[ARITH_PROVE ``(a = a + b) <=> (b = 0:num)``] THEN DISCH_TAC THEN
1787 SUBGOAL_THEN ``b:'a->bool DIFF a = EMPTY`` MP_TAC THENL
1788 [REWRITE_TAC[GSYM HAS_SIZE_0] THEN
1789 FULL_SIMP_TAC std_ss [HAS_SIZE, CARD_EMPTY],
1790 UNDISCH_TAC ``a:'a->bool SUBSET b`` THEN SET_TAC[]]
1791QED
1792
1793Theorem CARD_BIGUNION_LE:
1794 !s t:'a->'b->bool m n.
1795 s HAS_SIZE m /\ (!x. x IN s ==> FINITE(t x) /\ CARD(t x) <= n) ==>
1796 CARD(BIGUNION {t(x) | x IN s}) <= m * n
1797Proof
1798 REWRITE_TAC[HAS_SIZE] >> Induct_on ‘FINITE’ >> simp[] >>
1799 REPEAT GEN_TAC >> STRIP_TAC >>
1800 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] >>
1801 rw[DISJ_IMP_THM, FORALL_AND_THM,
1802 SET_RULE “BIGUNION {t x | x = a \/ x IN s} =
1803 t(a) UNION BIGUNION {t x | x IN s}”] >>
1804 MATCH_MP_TAC LESS_EQ_TRANS >>
1805 EXISTS_TAC
1806 “CARD((t:'a->'b->bool) e) + CARD(BIGUNION {(t:'a->'b->bool) x | x IN s})” >>
1807 CONJ_TAC >| [
1808 MATCH_MP_TAC CARD_UNION_LE >> simp[PULL_EXISTS] >>
1809 REWRITE_TAC[SET_RULE ``{t x | x IN s} = IMAGE t s``] >> simp[],
1810 simp[ADD1, RIGHT_ADD_DISTRIB] >> first_x_assum drule >> DECIDE_TAC
1811 ]
1812QED
1813
1814(* ----------------------------------------------------------------------
1815 Cardinality of type bool
1816 ---------------------------------------------------------------------- *)
1817
1818(* simplifier gets all of these because it turns univ(:bool) into {T;F} *)
1819
1820Theorem HAS_SIZE_BOOL: univ(:bool) HAS_SIZE 2
1821Proof simp[HAS_SIZE]
1822QED
1823
1824Theorem CARD_BOOL[simp]:
1825 CARD univ(:bool) = 2
1826Proof simp[]
1827QED
1828
1829Theorem FINITE_BOOL[simp]: FINITE univ(:bool)
1830Proof simp[]
1831QED
1832
1833(* NOTE: This theorem has been moved to pred_setTheory with a different name *)
1834Theorem INFINITE_DIFF_FINITE = INFINITE_DIFF_FINITE'
1835
1836(* ------------------------------------------------------------------------- *)
1837(* misc. *)
1838(* ------------------------------------------------------------------------- *)
1839
1840Theorem INJECTIVE_LEFT_INVERSE:
1841 (!x y. (f x = f y) ==> (x = y)) <=> (?g. !x. g(f(x)) = x)
1842Proof
1843 metis_tac[INJECTIVE_ON_LEFT_INVERSE, IN_UNIV]
1844QED
1845
1846Theorem INTER_ACI:
1847 !p q. (p INTER q = q INTER p) /\
1848 ((p INTER q) INTER r = p INTER q INTER r) /\
1849 (p INTER q INTER r = q INTER p INTER r) /\
1850 (p INTER p = p) /\
1851 (p INTER p INTER q = p INTER q)
1852Proof
1853 SET_TAC[]
1854QED
1855
1856Theorem UNION_ACI:
1857 !p q. (p UNION q = q UNION p) /\
1858 ((p UNION q) UNION r = p UNION q UNION r) /\
1859 (p UNION q UNION r = q UNION p UNION r) /\
1860 (p UNION p = p) /\
1861 (p UNION p UNION q = p UNION q)
1862Proof
1863 SET_TAC[]
1864QED
1865
1866(* ------------------------------------------------------------------------- *)
1867(* Now bijectivity. *)
1868(* ------------------------------------------------------------------------- *)
1869
1870Theorem BIJECTIVE_INJECTIVE_SURJECTIVE:
1871 !f s t. (!x. x IN s ==> f(x) IN t) /\
1872 (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
1873 (!x. x IN s ==> f(x) IN t) /\
1874 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
1875 (!y. y IN t ==> ?x. x IN s /\ (f x = y))
1876Proof
1877 MESON_TAC[]
1878QED
1879
1880Theorem BIJECTIVE_INVERSES:
1881 !f s t. (!x. x IN s ==> f(x) IN t) /\
1882 (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) <=>
1883 (!x. x IN s ==> f(x) IN t) /\
1884 ?g. (!y. y IN t ==> g(y) IN s) /\
1885 (!y. y IN t ==> (f(g(y)) = y)) /\
1886 (!x. x IN s ==> (g(f(x)) = x))
1887Proof
1888 NTAC 3 GEN_TAC THEN
1889 REWRITE_TAC[BIJECTIVE_INJECTIVE_SURJECTIVE,
1890 INJECTIVE_ON_LEFT_INVERSE,
1891 SURJECTIVE_ON_RIGHT_INVERSE] THEN
1892 MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
1893 DISCH_TAC THEN SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM] THEN
1894 AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN METIS_TAC[]
1895QED
1896
1897(* ------------------------------------------------------------------------- *)
1898(* Cardinal comparisons (in HOL-light's notations) *)
1899(* ------------------------------------------------------------------------- *)
1900
1901val _ = set_fixity "<=_c" (Infix(NONASSOC, 450)); (* for cardleq *)
1902Overload "<=_c" = ``cardleq``
1903Overload "<<=" = ``$<=_c``(* defined in pred_setTheory *)
1904
1905val _ = set_fixity "<_c" (Infix(NONASSOC, 450)); (* for cardlt *)
1906Overload "<_c" = ``cardlt``
1907Overload "<</=" = ``$<_c``
1908
1909val _ = set_fixity ">=_c" (Infix(NONASSOC, 450)); (* for cardgeq *)
1910val _ = Unicode.unicode_version {u = UTF8.chr 0x227D, tmnm = ">=_c"};
1911val _ = TeX_notation {hol = ">=_c", TeX = ("\\ensuremath{\\succcurlyeq}", 1)};
1912val _ = TeX_notation {hol = UTF8.chr 0x227D, TeX = ("\\ensuremath{\\succcurlyeq}", 1)};
1913
1914val _ = set_fixity ">_c" (Infix(NONASSOC, 450)); (* for cardgt *)
1915val _ = Unicode.unicode_version {u = UTF8.chr 0x227B, tmnm = ">_c"};
1916val _ = TeX_notation {hol = ">_c", TeX = ("\\ensuremath{\\succ}", 1)};
1917val _ = TeX_notation {hol = UTF8.chr 0x227B, TeX = ("\\ensuremath{\\succ}", 1)};
1918
1919val _ = set_fixity "=_c" (Infix(NONASSOC, 450)); (* for cardeq *)
1920Overload "=_c" = ``cardeq``
1921Overload "=~" = ``$=_c``
1922
1923Theorem le_c:
1924 !s t. s <=_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
1925 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y))
1926Proof
1927 rpt GEN_TAC
1928 >> REWRITE_TAC [cardleq_def, INJ_DEF]
1929 >> PROVE_TAC []
1930QED
1931
1932Theorem lt_c:
1933 !s t. s <_c t <=> s <=_c t /\ ~(t <=_c s)
1934Proof
1935 rpt GEN_TAC
1936 >> EQ_TAC >> STRIP_TAC
1937 >> PROVE_TAC [cardlt_lenoteq]
1938QED
1939
1940Theorem eq_c:
1941 !s t. s =_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
1942 !y. y IN t ==> ?!x. x IN s /\ (f x = y)
1943Proof
1944 rpt GEN_TAC
1945 >> REWRITE_TAC [cardeq_def, BIJ_ALT, IN_FUNSET]
1946 >> `!f x y. (f x = y) = (y = f x)` by PROVE_TAC [EQ_SYM]
1947 >> ASM_REWRITE_TAC []
1948QED
1949
1950Definition cardgeq_def:
1951 cardgeq s t = cardleq t s
1952End
1953
1954Overload ">=_c" = ``cardgeq``
1955Theorem ge_c = cardgeq_def;
1956
1957Definition cardgt_def:
1958 cardgt s t = cardlt t s
1959End
1960
1961Overload ">_c" = ``cardgt``
1962Theorem gt_c = cardgt_def;
1963
1964Theorem LE_C:
1965 !s t. s <=_c t <=> ?g. !x. x IN s ==> ?y. y IN t /\ (g y = x)
1966Proof
1967 SIMP_TAC std_ss [le_c, INJECTIVE_ON_LEFT_INVERSE, SURJECTIVE_ON_RIGHT_INVERSE,
1968 GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM, GSYM RIGHT_EXISTS_AND_THM] THEN
1969 MESON_TAC[]
1970QED
1971
1972Theorem GE_C:
1973 !s t. s >=_c t <=> ?f. !y. y IN t ==> ?x. x IN s /\ (y = f x)
1974Proof
1975 REWRITE_TAC[ge_c, LE_C] THEN MESON_TAC[]
1976QED
1977
1978Theorem COUNTABLE: !t. COUNTABLE t <=> univ(:num) >=_c t
1979Proof
1980 REWRITE_TAC [countable_def, cardgeq_def, cardleq_def]
1981QED
1982
1983(* ------------------------------------------------------------------------- *)
1984(* Relational variant of =_c is sometimes useful. *)
1985(* ------------------------------------------------------------------------- *)
1986
1987Theorem EQ_C_BIJECTIONS :
1988 !(s :'a -> bool) (t :'b -> bool).
1989 s =_c t <=> ?f g. (!x. x IN s ==> f x IN t /\ g(f x) = x) /\
1990 (!y. y IN t ==> g y IN s /\ f(g y) = y)
1991Proof
1992 REPEAT GEN_TAC THEN SIMP_TAC std_ss [eq_c] THEN
1993 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
1994 Q.X_GEN_TAC ‘f’ THEN SIMP_TAC std_ss [] THEN
1995 EQ_TAC THENL [STRIP_TAC, MESON_TAC[]] THEN
1996 Q.EXISTS_TAC `(\y. @x. x IN s /\ f x = y)` THEN
1997(* HOL-Light's ASM_MESON_TAC seems more powerful than HOL4's:
1998 ASM_MESON_TAC[]
1999 *)
2000 rw [] >> SELECT_ELIM_TAC \\
2001 gvs [EXISTS_UNIQUE_DEF]
2002QED
2003
2004Theorem EQ_C:
2005 !s t. s =_c t <=>
2006 ?R:'a#'b->bool. (!x y. R(x,y) ==> x IN s /\ y IN t) /\
2007 (!x. x IN s ==> ?!y. y IN t /\ R(x,y)) /\
2008 (!y. y IN t ==> ?!x. x IN s /\ R(x,y))
2009Proof
2010 rpt GEN_TAC THEN
2011 REWRITE_TAC[eq_c] THEN EQ_TAC THENL
2012 [DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2013 EXISTS_TAC ``\(x:'a,y:'b). x IN s /\ y IN t /\ (y = f x)`` THEN
2014 SIMP_TAC std_ss [] THEN ASM_MESON_TAC[],
2015 METIS_TAC []]
2016QED
2017
2018(* ------------------------------------------------------------------------- *)
2019(* The "easy" ordering properties. *)
2020(* ------------------------------------------------------------------------- *)
2021
2022(* HOL Light aliases/names *)
2023Theorem CARD_EQ_REFL = cardeq_REFL
2024Theorem CARD_EQ_SYM = cardeq_SYM
2025Theorem CARD_EQ_TRANS = cardeq_TRANS
2026Theorem CARD_EQ_EMPTY = cj 1 CARDEQ_0
2027Theorem CARD_EQ_CARD = CARDEQ_CARD_EQN |> Q.GENL [‘s1’, ‘s2’]
2028Theorem CARD_EQ_IMP_LE = CARDEQ_SUBSET_CARDLEQ
2029
2030Theorem CARD_LE_REFL = cardleq_REFL
2031Theorem CARD_LE_TRANS = cardleq_TRANS
2032Theorem CARD_LE_ANTISYM = cardleq_ANTISYM_IFF
2033Theorem CARD_LT_REFL = cardlt_REFL
2034Theorem CARD_LET_TRANS = cardleq_lt_trans
2035Theorem CARD_LTE_TRANS = cardlt_leq_trans
2036Theorem CARD_LT_TRANS = cardlt_TRANS
2037Theorem CARD_LE_EMPTY = cardleq_empty
2038
2039Theorem CARD_LE_TOTAL = cardleq_dichotomy
2040Theorem CARD_LE_LT = cardleq_lteq
2041Theorem CARD_LE_CONG = CARDEQ_CARDLEQ
2042Theorem CARD_LE_SUBSET = SUBSET_CARDLEQ
2043
2044
2045Theorem CARD_LT_IMP_LE:
2046 !s t. s <_c t ==> s <=_c t
2047Proof
2048 ONCE_REWRITE_TAC [lt_c]
2049 THEN SIMP_TAC std_ss []
2050QED
2051
2052Theorem CARD_LE_RELATIONAL:
2053 !(R:'a->'b->bool) s.
2054 (!x y y'. x IN s /\ R x y /\ R x y' ==> (y = y')) ==>
2055 {y | ?x. x IN s /\ R x y} <=_c s
2056Proof
2057 rpt strip_tac >> REWRITE_TAC[le_c] >>
2058 qexists ‘\y:'b. @x:'a. x IN s /\ R x y’ >> simp[] >>
2059 METIS_TAC[]
2060QED
2061
2062(* ------------------------------------------------------------------------- *)
2063(* Other variants like "trichotomy of cardinals" now follow easily. *)
2064(* ------------------------------------------------------------------------- *)
2065
2066Theorem CARD_LET_TOTAL:
2067 !s:'a->bool t:'b->bool. s <=_c t \/ t <_c s
2068Proof
2069 REWRITE_TAC [EXCLUDED_MIDDLE]
2070QED
2071
2072Theorem CARD_LTE_TOTAL:
2073 !s:'a->bool t:'b->bool. s <_c t \/ t <=_c s
2074Proof
2075 MESON_TAC[]
2076QED
2077
2078Theorem CARD_LT_TOTAL:
2079 !s:'a->bool t:'b->bool. (s =_c t) \/ s <_c t \/ t <_c s
2080Proof
2081 MESON_TAC[cardleq_lteq]
2082QED
2083
2084(* this is an instance of reflexivity *)
2085Theorem CARD_NOT_LE:
2086 !s:'a->bool t:'b->bool. ~(s <=_c t) <=> t <_c s
2087Proof
2088 REWRITE_TAC []
2089QED
2090
2091(* ¬¬p = p *)
2092Theorem CARD_NOT_LT:
2093 !s:'a->bool t:'b->bool. ~(s <_c t) <=> t <=_c s
2094Proof
2095 REWRITE_TAC []
2096QED
2097
2098Theorem CARD_LT_LE:
2099 !s t. s <_c t <=> s <=_c t /\ ~(s =_c t)
2100Proof
2101 REWRITE_TAC[Once lt_c, GSYM CARD_LE_ANTISYM] THEN TAUT_TAC
2102QED
2103
2104
2105Theorem CARD_LT_CONG:
2106 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2107 s =_c s' /\ t =_c t' ==> (s <_c t <=> s' <_c t')
2108Proof
2109 REPEAT STRIP_TAC THEN
2110 AP_TERM_TAC THEN MATCH_MP_TAC CARD_LE_CONG THEN
2111 ASM_REWRITE_TAC[]
2112QED
2113
2114Theorem CARD_12[simp]:
2115 {()} <</= {T;F} /\ ~({()} =~ {T;F}) /\ ~({T;F} =~ {()}) /\ {()} <<= {T;F}
2116Proof
2117 conj_asm1_tac
2118 >- (simp[cardleq_def, INJ_IFF] >> qexistsl_tac [‘T’, ‘F’] >> simp[]) >>
2119 metis_tac[CARD_LT_CONG, CARD_LT_REFL, cardeq_REFL, cardleq_lteq]
2120QED
2121
2122
2123Theorem CARD_EQ_CONG:
2124 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2125 s =_c s' /\ t =_c t' ==> (s =_c t <=> s' =_c t')
2126Proof
2127 METIS_TAC[CARD_EQ_TRANS, CARD_EQ_SYM]
2128QED
2129
2130(* ------------------------------------------------------------------------- *)
2131(* Finiteness and infiniteness in terms of cardinality of N. *)
2132(* ------------------------------------------------------------------------- *)
2133
2134Theorem INFINITE_CARD_LE[local] = INFINITE_Unum
2135
2136Theorem FINITE_CARD_LT:
2137 !s:'a->bool. FINITE s <=> s <_c (UNIV:num->bool)
2138Proof
2139 ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
2140 REWRITE_TAC [Once (GSYM CARD_NOT_LT), INFINITE_CARD_LE]
2141QED
2142
2143
2144Theorem CARD_LE_UNIV:
2145 !s:'a->bool. s <=_c univ(:'a)
2146Proof
2147 GEN_TAC THEN MATCH_MP_TAC CARD_LE_SUBSET THEN REWRITE_TAC[SUBSET_UNIV]
2148QED
2149
2150Theorem CARD_LE_EQ_SUBSET:
2151 !s:'a->bool t:'b->bool. s <=_c t <=> ?u. u SUBSET t /\ (s =_c u)
2152Proof
2153 REPEAT GEN_TAC THEN EQ_TAC THENL
2154 [ALL_TAC,
2155 REPEAT STRIP_TAC THEN
2156 FIRST_ASSUM(MP_TAC o MATCH_MP CARD_LE_SUBSET) THEN
2157 MATCH_MP_TAC(TAUT `(a <=> b) ==> b ==> a`) THEN
2158 MATCH_MP_TAC CARD_LE_CONG THEN
2159 ASM_REWRITE_TAC[CARD_LE_CONG, CARD_EQ_REFL]] THEN
2160 REWRITE_TAC[le_c, eq_c] THEN
2161 DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2162 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM] THEN EXISTS_TAC ``IMAGE (f:'a->'b) s`` THEN
2163 EXISTS_TAC ``f:'a->'b`` THEN REWRITE_TAC[IN_IMAGE, SUBSET_DEF] THEN
2164 ASM_MESON_TAC[]
2165QED
2166
2167Theorem CARD_INFINITE_CONG:
2168 !s:'a->bool t:'b->bool. s =_c t ==> (INFINITE s <=> INFINITE t)
2169Proof
2170 REWRITE_TAC[INFINITE_CARD_LE] THEN REPEAT STRIP_TAC THEN
2171 MATCH_MP_TAC CARD_LE_CONG THEN ASM_SIMP_TAC std_ss [CARD_EQ_REFL]
2172QED
2173
2174Theorem CARD_FINITE_CONG:
2175 !s:'a->bool t:'b->bool. s =_c t ==> (FINITE s <=> FINITE t)
2176Proof
2177 ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
2178 SIMP_TAC std_ss [CARD_INFINITE_CONG]
2179QED
2180
2181Theorem CARD_LE_FINITE:
2182 !s:'a->bool t:'b->bool. FINITE t /\ s <=_c t ==> FINITE s
2183Proof
2184 ASM_MESON_TAC[CARD_LE_EQ_SUBSET, SUBSET_FINITE_I, CARD_FINITE_CONG]
2185QED
2186
2187Theorem CARD_EQ_FINITE:
2188 !s t:'a->bool. FINITE t /\ s =_c t ==> FINITE s
2189Proof
2190 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_FINITE]
2191QED
2192
2193Theorem CARD_LE_INFINITE:
2194 !s:'a->bool t:'b->bool. INFINITE s /\ s <=_c t ==> INFINITE t
2195Proof
2196 MESON_TAC[CARD_LE_FINITE]
2197QED
2198
2199Theorem CARD_LT_FINITE_INFINITE:
2200 !s:'a->bool t:'b->bool. FINITE s /\ INFINITE t ==> s <_c t
2201Proof
2202 ONCE_REWRITE_TAC[GSYM CARD_NOT_LE] THEN MESON_TAC[CARD_LE_FINITE]
2203QED
2204
2205Theorem CARD_LE_CARD_IMP:
2206 !s:'a->bool t:'b->bool. FINITE t /\ s <=_c t ==> CARD s <= CARD t
2207Proof
2208 REPEAT STRIP_TAC THEN
2209 SUBGOAL_THEN ``FINITE(s:'a->bool)`` ASSUME_TAC THENL
2210 [ASM_MESON_TAC[CARD_LE_FINITE], ALL_TAC] THEN
2211 UNDISCH_TAC ``s <=_c t`` THEN DISCH_TAC THEN
2212 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [le_c]) THEN
2213 DISCH_THEN(X_CHOOSE_THEN ``f:'a->'b`` STRIP_ASSUME_TAC) THEN
2214 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ``CARD(IMAGE (f:'a->'b) s)`` THEN
2215 CONJ_TAC THENL
2216 [MATCH_MP_TAC(ARITH_PROVE ``(m = n:num) ==> n <= m``) THEN
2217 MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[],
2218 KNOW_TAC ``(IMAGE (f :'a -> 'b) (s :'a -> bool)) SUBSET (t :'b -> bool)`` THENL
2219 [ASM_MESON_TAC[SUBSET_DEF, IN_IMAGE], ALL_TAC] THEN
2220 MATCH_MP_TAC (CARD_SUBSET) THEN ASM_REWRITE_TAC[]]
2221QED
2222
2223Theorem CARD_EQ_CARD_IMP:
2224 !s:'a->bool t:'b->bool. FINITE t /\ s =_c t ==> (CARD s = CARD t)
2225Proof
2226 METIS_TAC[CARD_FINITE_CONG, ARITH_PROVE ``m <= n /\ n <= m <=> (m = n:num)``,
2227 CARD_LE_ANTISYM, CARD_LE_CARD_IMP]
2228QED
2229
2230Theorem CARD_LE_CARD:
2231 !s:'a->bool t:'b->bool.
2232 FINITE s /\ FINITE t ==> (s <=_c t <=> CARD s <= CARD t)
2233Proof
2234 REPEAT STRIP_TAC THEN
2235 MATCH_MP_TAC(TAUT ‘(a ==> b) /\ (~a ==> ~b) ==> (a <=> b)’) THEN
2236 ASM_SIMP_TAC std_ss [CARD_LE_CARD_IMP] THEN
2237 REWRITE_TAC[NOT_LESS_EQUAL] THEN REWRITE_TAC[Once lt_c, LT_LE] THEN
2238 ASM_SIMP_TAC std_ss [CARD_LE_CARD_IMP] THEN
2239 MATCH_MP_TAC(TAUT ‘(c ==> a ==> b) ==> a /\ ~b ==> ~c’) THEN
2240 DISCH_TAC THEN simp[CARD_LE_EQ_SUBSET, SimpL “$==>”] THEN
2241 DISCH_THEN(qx_choose_then ‘u’ STRIP_ASSUME_TAC) THEN
2242 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2243 ‘u = s’ suffices_by ASM_MESON_TAC[CARD_EQ_SYM] THEN
2244 METIS_TAC[CARD_SUBSET_EQ, CARD_EQ_CARD_IMP, CARD_EQ_SYM]
2245QED
2246
2247
2248Theorem CARD_HAS_SIZE_CONG:
2249 !s:'a->bool t:'b->bool n. s HAS_SIZE n /\ s =_c t ==> t HAS_SIZE n
2250Proof
2251 REWRITE_TAC[HAS_SIZE] THEN
2252 MESON_TAC[CARD_EQ_CARD, CARD_FINITE_CONG]
2253QED
2254
2255Theorem CARD_LE_IMAGE = IMAGE_cardleq
2256
2257Theorem CARD_LE_IMAGE_GEN:
2258 !f:'a->'b s t. t SUBSET IMAGE f s ==> t <=_c s
2259Proof
2260 REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_LE_TRANS THEN
2261 EXISTS_TAC ``IMAGE (f:'a->'b) s`` THEN
2262 ASM_SIMP_TAC std_ss [CARD_LE_IMAGE, CARD_LE_SUBSET]
2263QED
2264
2265Theorem CARD_EQ_IMAGE:
2266 !f:'a->'b s.
2267 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
2268 ==> (IMAGE f s =_c s)
2269Proof
2270 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN
2271 REWRITE_TAC[eq_c] THEN EXISTS_TAC ``f:'a->'b`` THEN ASM_SET_TAC[]
2272QED
2273
2274(* ------------------------------------------------------------------------- *)
2275(* Cardinal arithmetic operations. *)
2276(* ------------------------------------------------------------------------- *)
2277
2278val add_c = disjUNION_def
2279
2280val _ = set_mapped_fixity {tok = "+_c", fixity = Infixl 500,
2281 term_name = "disjUNION"}
2282val _ = set_mapped_fixity {fixity = Infixl 500,
2283 term_name = "disjUNION",
2284 tok = UTF8.chr 0x2294}
2285
2286Overload "+"[local,inferior] = “disjUNION”;
2287
2288val _ = temp_set_fixity "*_c" (Infixl 600);
2289Overload "*_c"[local,inferior] = “pred_set$CROSS”;
2290
2291Theorem mul_c:
2292 !s t. s *_c t = {(x,y) | x IN s /\ y IN t}
2293Proof
2294 simp[EXTENSION, FORALL_PROD]
2295QED
2296
2297(* ------------------------------------------------------------------------- *)
2298(* Congruence properties for the arithmetic operators. *)
2299(* ------------------------------------------------------------------------- *)
2300
2301Theorem CARD_LE_ADD:
2302 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2303 s <=_c s' /\ t <=_c t' ==> s + t <=_c s' + t'
2304Proof
2305 rpt gen_tac >> simp[le_c, add_c, FORALL_SUM] >>
2306 DISCH_THEN(CONJUNCTS_THEN2
2307 (X_CHOOSE_THEN “f:'a->'b” STRIP_ASSUME_TAC)
2308 (X_CHOOSE_THEN “g:'c->'d” STRIP_ASSUME_TAC)) >>
2309 qexists ‘λs. case s of INL a => INL (f a) | INR b => INR (g b)’ >>
2310 simp[]
2311QED
2312
2313Theorem CARD_LE_MUL = CARDLEQ_CROSS_CONG
2314
2315Theorem CARD_ADD_CONG:
2316 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2317 s =_c s' /\ t =_c t' ==> (s +_c t) =_c (s' +_c t')
2318Proof
2319 SIMP_TAC std_ss [CARD_LE_ADD, GSYM CARD_LE_ANTISYM]
2320QED
2321
2322Theorem CARD_MUL_CONG = CARDEQ_CROSS
2323
2324(* ------------------------------------------------------------------------- *)
2325(* Misc lemmas. *)
2326(* ------------------------------------------------------------------------- *)
2327
2328Theorem IN_CARD_ADD = IN_disjUNION
2329
2330Theorem IN_CARD_MUL: !s t x y. (x,y) IN (s *_c t) <=> x IN s /\ y IN t
2331Proof simp[]
2332QED
2333
2334Theorem CARD_LE_SQUARE:
2335 !s:'a->bool. s <=_c (s *_c s)
2336Proof
2337 simp[le_c] >> gen_tac >> qexists ‘λx. (x,x)’ >> simp[]
2338QED
2339
2340Theorem CARD_SQUARE_NUM:
2341 univ(:num) *_c univ(:num) =_c univ(:num)
2342Proof
2343 simp[cardeq_def] >> metis_tac[NUM_2D_BIJ_INV, BIJ_INV]
2344QED
2345
2346Theorem UNION_LE_ADD_C:
2347 !s t:'a->bool. s UNION t <=_c s + t
2348Proof
2349 rw[le_c] >> qexists ‘λx. if x IN s then INL x else INR x’ >> rw[]
2350QED
2351
2352Theorem CARD_DISJOINT_UNION:
2353 !s t.
2354 FINITE s /\ FINITE t /\ s INTER t = {} ==>
2355 CARD (s UNION t) = CARD s + CARD t
2356Proof
2357 simp[CARD_UNION_EQN]
2358QED
2359
2360Theorem CARD_ADD_C = CARD_disjUNION
2361
2362(* ------------------------------------------------------------------------- *)
2363(* Various "arithmetical" lemmas. *)
2364(* ------------------------------------------------------------------------- *)
2365
2366Theorem CARD_ADD_SYM:
2367 !s:'a->bool t:'b->bool. (s +_c t) =_c (t +_c s)
2368Proof
2369 rw[cardeq_def] >> qexists ‘λx. case x of INL a => INR a | INR b => INL b’ >>
2370 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_SUM, AllCaseEqs()]
2371QED
2372
2373Theorem CARD_ADD_ASSOC:
2374 !s:'a->bool t:'b->bool u:'c->bool. (s +_c (t +_c u)) =_c ((s +_c t) +_c u)
2375Proof
2376 rw[cardeq_def] >>
2377 qexists ‘λx. case x of INL a => INL (INL a) | INR (INL b) => INL (INR b)
2378 | INR (INR c) => INR c’ >>
2379 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_SUM, AllCaseEqs()]
2380QED
2381
2382Theorem CARD_MUL_SYM = CARDEQ_CROSS_SYM
2383
2384Theorem CARD_MUL_ASSOC:
2385 !s:'a->bool t:'b->bool u:'c->bool. (s *_c (t *_c u)) =_c ((s *_c t) *_c u)
2386Proof
2387 rw[cardeq_def] >>
2388 qexists ‘λt. case t of (a,(b,c)) => ((a,b),c)’>>
2389 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD]
2390QED
2391
2392Theorem CARD_LDISTRIB:
2393 !s:'a->bool t:'b->bool u:'c->bool.
2394 (s *_c (t +_c u)) =_c ((s *_c t) +_c (s *_c u))
2395Proof
2396 rw[cardeq_def] >>
2397 qexists ‘λp. case p of (a,INL b) => INL (a,b) | (a, INR c) => INR (a, c)’ >>
2398 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD, FORALL_SUM,
2399 AllCaseEqs()]
2400QED
2401
2402Theorem CARD_RDISTRIB:
2403 !s:'a->bool t:'b->bool u:'c->bool.
2404 (s +_c t) *_c u =_c (s *_c u) +_c (t *_c u)
2405Proof
2406 rw[cardeq_def] >>
2407 qexists ‘λp. case p of (INL a, c) => INL (a,c) | (INR b, c) => INR (b,c)’ >>
2408 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, FORALL_PROD, EXISTS_PROD, FORALL_SUM,
2409 AllCaseEqs()]
2410QED
2411
2412Theorem CARD_LE_ADDR:
2413 !s:'a->bool t:'b->bool. s <=_c (s +_c t)
2414Proof
2415 REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
2416 EXISTS_TAC ``INL:'a->'a+'b`` THEN SIMP_TAC std_ss [IN_CARD_ADD, INR_11, INL_11]
2417QED
2418
2419Theorem CARD_LE_ADDL:
2420 !s:'a->bool t:'b->bool. t <=_c (s +_c t)
2421Proof
2422 REPEAT GEN_TAC THEN REWRITE_TAC[le_c] THEN
2423 EXISTS_TAC ``INR:'b->'a+'b`` THEN SIMP_TAC std_ss [IN_CARD_ADD, INR_11, INL_11]
2424QED
2425
2426(* ------------------------------------------------------------------------- *)
2427(* A rather special lemma but temporarily useful. *)
2428(* ------------------------------------------------------------------------- *)
2429
2430Theorem CARD_ADD_LE_MUL_INFINITE:
2431 !s:'a->bool. INFINITE s ==> (s +_c s) <=_c (s *_c s)
2432Proof
2433 GEN_TAC THEN REWRITE_TAC[INFINITE_CARD_LE, le_c, IN_UNIV] THEN
2434 DISCH_THEN(X_CHOOSE_THEN ``f:num->'a`` STRIP_ASSUME_TAC) THEN
2435 KNOW_TAC ``?h. (!x. h(INL x) = (f(0:num),x):'a#'a) /\ (!x. h(INR x) = (f(1),x))`` THENL
2436 [RW_TAC std_ss [sum_Axiom], ALL_TAC] THEN
2437 STRIP_TAC THEN EXISTS_TAC ``h:'a+'a->'a#'a`` THEN STRIP_TAC THENL
2438 [ONCE_REWRITE_TAC [METIS [] ``( x IN s +_c s ==> h x IN s *_c s) =
2439 (\x. x IN s +_c s ==> h x IN s *_c s) x``] THEN
2440 MATCH_MP_TAC sum_INDUCT THEN
2441 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ], ALL_TAC] THEN
2442 ONCE_REWRITE_TAC [METIS [] ``(!y. x IN s +_c s /\ y IN s +_c s /\ (h x = h y) ==> (x = y)) =
2443 (\x. !y. x IN s +_c s /\ y IN s +_c s /\ (h x = h y) ==> (x = y)) x``] THEN
2444 MATCH_MP_TAC sum_INDUCT THEN
2445 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ] THEN STRIP_TAC THEN STRIP_TAC THENL
2446 [ONCE_REWRITE_TAC [METIS [] ``(x IN s /\ y IN s +_c s /\ ((f (0:num),x) =
2447 (h :'a + 'a -> 'a # 'a) y) ==> (INL x = y)) =
2448 (\y:'a+'a. x IN s /\ y IN s +_c s /\ ((f (0:num),x) =
2449 (h :'a + 'a -> 'a # 'a) y) ==> (INL x = y)) y``],
2450 ONCE_REWRITE_TAC [METIS [] ``(x IN s /\ y IN s +_c s /\ ((f (1:num),x) =
2451 (h :'a + 'a -> 'a # 'a) y) ==> (INR x = y)) =
2452 (\y:'a+'a. x IN s /\ y IN s +_c s /\ ((f (1:num),x) =
2453 (h :'a + 'a -> 'a # 'a) y) ==> (INR x = y)) y``]] THEN
2454 MATCH_MP_TAC sum_INDUCT THEN
2455 ASM_SIMP_TAC std_ss [IN_CARD_ADD, IN_CARD_MUL, PAIR_EQ] THEN
2456 ASM_MESON_TAC[REDUCE_CONV ``1 = 0:num``]
2457QED
2458
2459(* ------------------------------------------------------------------------- *)
2460(* Relate cardinal addition to the simple union operation. *)
2461(* ------------------------------------------------------------------------- *)
2462
2463Theorem CARDEQ_DISJOINT_UNION:
2464 !s:'a->bool t. (s INTER t = EMPTY) ==> (s UNION t =_c (s +_c t))
2465Proof
2466 REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN
2467 STRIP_TAC THEN REWRITE_TAC[eq_c, IN_UNION] THEN
2468 EXISTS_TAC ``\x:'a. if x IN s then INL x else INR x`` THEN
2469 SIMP_TAC std_ss [FORALL_SUM, IN_CARD_ADD] THEN
2470 REWRITE_TAC[COND_RAND, COND_RATOR] THEN
2471 REWRITE_TAC[TAUT `(if b then x else y) <=> b /\ x \/ ~b /\ y`] THEN
2472 SIMP_TAC std_ss [sum_distinct, INL_11, INR_11, IN_CARD_ADD] THEN
2473 ASM_MESON_TAC[]
2474QED
2475
2476(* ------------------------------------------------------------------------- *)
2477(* The key to arithmetic on infinite cardinals: k^2 = k. *)
2478(* ------------------------------------------------------------------------- *)
2479
2480Theorem CARD_SQUARE_INFINITE = SET_SQUARED_CARDEQ_SET;
2481
2482(* ------------------------------------------------------------------------- *)
2483(* Preservation of finiteness. *)
2484(* ------------------------------------------------------------------------- *)
2485
2486Theorem CARD_ADD_FINITE:
2487 !s t. FINITE s /\ FINITE t ==> FINITE(s +_c t)
2488Proof
2489 SIMP_TAC std_ss [add_c, FINITE_UNION, GSYM IMAGE_DEF, IMAGE_FINITE]
2490QED
2491
2492Theorem CARD_ADD_FINITE_EQ:
2493 !s:'a->bool t:'b->bool. FINITE(s +_c t) <=> FINITE s /\ FINITE t
2494Proof
2495 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[CARD_ADD_FINITE] THEN
2496 DISCH_THEN(fn th => CONJ_TAC THEN MP_TAC th) THEN
2497 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) THEN
2498 REWRITE_TAC[CARD_LE_ADDL, CARD_LE_ADDR]
2499QED
2500
2501Theorem CARD_MUL_FINITE:
2502 !s t. FINITE s /\ FINITE t ==> FINITE(s *_c t)
2503Proof
2504 SIMP_TAC std_ss [mul_c, FINITE_PRODUCT]
2505QED
2506
2507(* ------------------------------------------------------------------------- *)
2508(* Hence the "absorption laws" for arithmetic with an infinite cardinal. *)
2509(* ------------------------------------------------------------------------- *)
2510
2511Theorem CARD_MUL2_ABSORB_LE:
2512 !s:'a->bool t:'b->bool u:'c->bool.
2513 INFINITE(u) /\ s <=_c u /\ t <=_c u ==> (s *_c t) <=_c u
2514Proof
2515 REPEAT STRIP_TAC THEN
2516 KNOW_TAC ``(s *_c t) <=_c ((s:'a->bool) *_c (u:'c->bool)) /\
2517 ((s:'a->bool) *_c (u:'c->bool)) <=_c u`` THENL
2518 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2519 ASM_SIMP_TAC std_ss [CARD_MUL_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_MUL THEN
2520 ASM_REWRITE_TAC[CARD_LE_REFL]
2521QED
2522
2523Theorem CARD_ADD_ABSORB_LE:
2524 !s:'a->bool t:'b->bool. INFINITE(t) /\ s <=_c t ==> (s +_c t) <=_c t
2525Proof
2526 REPEAT STRIP_TAC THEN
2527 KNOW_TAC ``(s +_c t) <=_c ((t:'b->bool) *_c t) /\
2528 ((t:'b->bool) *_c t) <=_c t`` THENL
2529 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2530 ASM_SIMP_TAC std_ss [CARD_SQUARE_INFINITE, CARD_EQ_IMP_LE] THEN
2531 KNOW_TAC ``(s +_c t) <=_c ((t:'b->bool) +_c t) /\
2532 ((t:'b->bool) +_c t) <=_c (t *_c t)`` THENL
2533 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2534 ASM_SIMP_TAC std_ss [CARD_ADD_LE_MUL_INFINITE, CARD_LE_ADD, CARD_LE_REFL]
2535QED
2536
2537Theorem CARD_ADD2_ABSORB_LE:
2538 !s:'a->bool t:'b->bool u:'c->bool.
2539 INFINITE(u) /\ s <=_c u /\ t <=_c u ==> (s +_c t) <=_c u
2540Proof
2541 REPEAT STRIP_TAC THEN
2542 KNOW_TAC ``(s +_c t) <=_c ((s:'a->bool) +_c (u:'c->bool)) /\
2543 ((s:'a->bool) +_c (u:'c->bool)) <=_c u`` THENL
2544 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2545 ASM_SIMP_TAC std_ss [CARD_ADD_ABSORB_LE] THEN MATCH_MP_TAC CARD_LE_ADD THEN
2546 ASM_REWRITE_TAC[CARD_LE_REFL]
2547QED
2548
2549Theorem CARD_MUL_ABSORB:
2550 !s:'a->bool t:'b->bool.
2551 INFINITE(t) /\ ~(s = {}) /\ s <=_c t ==> (s *_c t) =_c t
2552Proof
2553 SIMP_TAC std_ss [GSYM CARD_LE_ANTISYM, CARD_MUL_ABSORB_LE] THEN REPEAT STRIP_TAC THEN
2554 FIRST_X_ASSUM(X_CHOOSE_TAC ``a:'a`` o
2555 REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
2556 REWRITE_TAC[le_c] THEN EXISTS_TAC ``\x:'b. (a:'a,x)`` THEN
2557 ASM_SIMP_TAC std_ss [IN_CARD_MUL, PAIR_EQ]
2558QED
2559
2560Theorem CARD_ADD_ABSORB:
2561 !s:'a->bool t:'b->bool. INFINITE(t) /\ s <=_c t ==> (s +_c t) =_c t
2562Proof
2563 SIMP_TAC std_ss [GSYM CARD_LE_ANTISYM, CARD_LE_ADDL, CARD_ADD_ABSORB_LE]
2564QED
2565
2566Theorem CARD_ADD2_ABSORB_LT:
2567 !s:'a->bool t:'b->bool u:'c->bool.
2568 INFINITE u /\ s <_c u /\ t <_c u ==> (s +_c t) <_c u
2569Proof
2570 REPEAT GEN_TAC THEN
2571 STRIP_TAC THEN
2572 ASM_CASES_TAC ``FINITE((s:'a->bool) +_c (t:'b->bool))`` THEN
2573 ASM_SIMP_TAC std_ss [CARD_LT_FINITE_INFINITE] THEN
2574 DISJ_CASES_TAC(ISPECL [``s:'a->bool``, ``t:'b->bool``] CARD_LE_TOTAL) THENL
2575 [(* goal 1 (of 2) *)
2576 ASM_CASES_TAC ``FINITE(t:'b->bool)`` THENL
2577 [ASM_MESON_TAC[CARD_LE_FINITE, CARD_ADD_FINITE],
2578 KNOW_TAC ``(s +_c t) <=_c (t:'b->bool) /\
2579 (t:'b->bool) <_c u`` THENL
2580 [ALL_TAC, METIS_TAC [CARD_LET_TRANS]]],
2581 (* goal 2 (of 2) *)
2582 ASM_CASES_TAC ``FINITE(s:'a->bool)`` THENL
2583 [ASM_MESON_TAC[CARD_LE_FINITE, CARD_ADD_FINITE],
2584 KNOW_TAC ``(s +_c t) <=_c (s:'a->bool) /\
2585 (s:'a->bool) <_c u`` THENL
2586 [ALL_TAC, METIS_TAC [CARD_LET_TRANS]]]] THEN
2587 ASM_REWRITE_TAC[] THEN
2588 MATCH_MP_TAC CARD_ADD2_ABSORB_LE THEN
2589 ASM_REWRITE_TAC[CARD_LE_REFL]
2590QED
2591
2592Theorem CARD_LT_ADD:
2593 !s:'a->bool s':'b->bool t:'c->bool t':'d->bool.
2594 s <_c s' /\ t <_c t' ==> (s +_c t) <_c (s' +_c t')
2595Proof
2596 REPEAT GEN_TAC THEN
2597 STRIP_TAC THEN
2598 ASM_CASES_TAC ``FINITE((s':'b->bool) +_c (t':'d->bool))`` THENL
2599 [FIRST_X_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE
2600 [CARD_ADD_FINITE_EQ]) THEN
2601 SUBGOAL_THEN ``FINITE(s:'a->bool) /\ FINITE(t:'c->bool)``
2602 STRIP_ASSUME_TAC THENL
2603 [CONJ_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
2604 (REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_FINITE) o
2605 MATCH_MP CARD_LT_IMP_LE) THEN
2606 ASM_REWRITE_TAC[],
2607 MAP_EVERY UNDISCH_TAC
2608 [``(s:'a->bool) <_c (s':'b->bool)``,
2609 ``(t:'c->bool) <_c (t':'d->bool)``] THEN
2610 ASM_SIMP_TAC std_ss [CARD_LT_CARD, CARD_ADD_FINITE, CARD_ADD_C] THEN
2611 ARITH_TAC],
2612 MATCH_MP_TAC CARD_ADD2_ABSORB_LT THEN ASM_REWRITE_TAC[] THEN
2613 CONJ_TAC THENL
2614 [METIS_TAC [CARD_LTE_TRANS, CARD_LE_ADDR],
2615 METIS_TAC [CARD_LTE_TRANS, CARD_LE_ADDL]]]
2616QED
2617
2618(* ------------------------------------------------------------------------- *)
2619(* Cantor's theorem. *)
2620(* ------------------------------------------------------------------------- *)
2621
2622Theorem CANTOR_THM:
2623 !s:'a->bool. s <_c {t | t SUBSET s}
2624Proof
2625 simp[GSYM POW_DEF]
2626QED
2627
2628Theorem CANTOR_THM_UNIV:
2629 (UNIV:'a->bool) <_c (UNIV:('a->bool)->bool)
2630Proof
2631 ‘univ(:'a -> bool) = POW univ(:'a)’ suffices_by simp[] >>
2632 simp[EXTENSION, POW_DEF]
2633QED
2634
2635Theorem CARD_EXP_SING :
2636 !(s :'a -> bool) (b :'b). (s ** {b}) =_c s
2637Proof
2638 REWRITE_TAC [SING_set_exp_CARD]
2639QED
2640
2641Theorem CARD_EXP_CONG :
2642 !(s:'a->bool) (s':'b->bool) (t:'c->bool) (t':'d->bool).
2643 s =_c s' /\ t =_c t' ==> s ** t =_c s' ** t'
2644Proof
2645 rw [set_exp_card_cong]
2646QED
2647
2648Theorem CARD_LE_EXP_LEFT :
2649 !(s :'a -> bool) (s' :'b -> bool) (t :'c -> bool).
2650 s <=_c s' ==> s ** t <=_c s' ** t
2651Proof
2652 REPEAT GEN_TAC THEN REWRITE_TAC[le_c, exp_c] THEN
2653 DISCH_THEN(X_CHOOSE_TAC “f :'a -> 'b”) THEN
2654 rw [GSPECIFICATION] THEN
2655 EXISTS_TAC “\(g:'c->'a) (z:'c). if z IN t then f(g z):'b else ARB” THEN
2656 rw [FUN_EQ_THM] THEN
2657 METIS_TAC []
2658QED
2659
2660Theorem CARD_EXP_MUL :
2661 !(s:'a->bool) (t:'b->bool) (u:'c->bool).
2662 s ** (t *_c u) =_c (s ** t) ** u
2663Proof
2664 rw [Once cardeq_SYM, set_exp_product]
2665QED
2666
2667Theorem CARD_EXP_POWERSET :
2668 !s :'a -> bool. univ(:bool) ** s =_c {t | t SUBSET s}
2669Proof
2670 GEN_TAC
2671 >> REWRITE_TAC [exp_c, EQ_C_BIJECTIONS, IN_UNIV]
2672 >> qexistsl_tac [‘\P. {x | x IN s /\ P x}’,
2673 ‘\t x. if x IN s then x IN t else ARB’]
2674 >> SIMP_TAC std_ss [GSPECIFICATION]
2675 >> SET_TAC []
2676QED
2677
2678Theorem CARD_EXP_CANTOR :
2679 !s :'a -> bool. s <_c univ(:bool) ** s
2680Proof
2681 GEN_TAC THEN
2682 TRANS_TAC CARD_LTE_TRANS “{t :'a->bool | t SUBSET s}” THEN
2683 REWRITE_TAC[CANTOR_THM] THEN
2684 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2685 ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[CARD_EXP_POWERSET]
2686QED
2687
2688Theorem CARD_EXP_ABSORB :
2689 !(s :'a -> bool) (t :'b -> bool).
2690 INFINITE t /\ univ(:bool) <=_c s /\ s <=_c univ(:bool) ** t
2691 ==> s ** t =_c univ(:bool) ** t
2692Proof
2693 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN
2694 ASM_SIMP_TAC std_ss [CARD_LE_EXP_LEFT, CARD_LE_REFL] THEN
2695 TRANS_TAC CARD_LE_TRANS “(univ(:bool) ** t) ** (t:'b->bool)” THEN
2696 ASM_SIMP_TAC std_ss[CARD_LE_EXP_LEFT] THEN
2697 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
2698 TRANS_TAC CARD_EQ_TRANS “univ(:bool) ** ((t:'b->bool) *_c t)” THEN
2699 SIMP_TAC std_ss[ONCE_REWRITE_RULE[CARD_EQ_SYM] CARD_EXP_MUL] THEN
2700 MATCH_MP_TAC CARD_EXP_CONG THEN
2701 ASM_SIMP_TAC std_ss[CARD_SQUARE_INFINITE, CARD_EQ_REFL]
2702QED
2703
2704(* ------------------------------------------------------------------------- *)
2705(* Lemmas about countability. *)
2706(* ------------------------------------------------------------------------- *)
2707
2708Theorem NUM_COUNTABLE = num_countable
2709
2710Theorem COUNTABLE_ALT_cardleq:
2711 !s. COUNTABLE s <=> s <=_c univ(:num)
2712Proof
2713 REWRITE_TAC[COUNTABLE, ge_c]
2714QED
2715
2716Theorem COUNTABLE_CASES:
2717 !s. COUNTABLE s <=> FINITE s \/ s =_c univ(:num)
2718Proof
2719 GEN_TAC
2720 >> ONCE_REWRITE_TAC[COUNTABLE_ALT_cardleq, FINITE_CARD_LT]
2721 >> METIS_TAC [CARD_LE_LT]
2722QED
2723
2724(* changed ‘t:'a->bool’ to ‘t:'b->bool’ *)
2725Theorem CARD_LE_COUNTABLE :
2726 !s:'a->bool t:'b->bool. COUNTABLE t /\ s <=_c t ==> COUNTABLE s
2727Proof
2728 REWRITE_TAC [COUNTABLE, ge_c]
2729 >> rpt STRIP_TAC
2730 >> KNOW_TAC ``?(t :'b -> bool).
2731 (s :'a -> bool) <=_c t /\ t <=_c univ((:num) :num itself)``
2732 >- (EXISTS_TAC ``t:'b->bool`` >> ASM_REWRITE_TAC[])
2733 >> METIS_TAC [CARD_LE_TRANS]
2734QED
2735
2736Theorem countable_setexp:
2737 countable (A ** B) <=>
2738 B = {} \/ FINITE B /\ countable A \/ A =~ {()} \/ A = {}
2739Proof
2740 rw[EQ_IMP_THM] >~
2741 [‘countable (A ** {})’]
2742 >- (resolve_then (Pos hd) irule EMPTY_set_exp_CARD (iffRL countable_cardeq) >>
2743 simp[COUNTABLE_COUNT]) >~
2744 [‘countable ({} ** B)’]
2745 >- (Cases_on ‘B = {}’
2746 >- (simp[] >>
2747 resolve_then (Pos hd) irule EMPTY_set_exp_CARD
2748 (iffRL countable_cardeq) >>
2749 simp[COUNTABLE_COUNT]) >>
2750 simp[EMPTY_set_exp]) >~
2751 [‘FINITE B /\ countable A’]
2752 >- (Cases_on ‘B = {}’ >> simp[] >> Cases_on ‘A = {}’ >> simp[] >>
2753 Cases_on ‘A =~ {()}’ >> simp[] >>
2754 Cases_on ‘FINITE B’ >> simp[]
2755 >- metis_tac[FINITE_EXPONENT_SETEXP_UNCOUNTABLE] >>
2756 ‘~countable (POW B)’ by metis_tac[infinite_pow_uncountable] >>
2757 ‘~countable (count 2 ** B)’
2758 by metis_tac[countable_cardeq, POW_TWO_set_exp] >>
2759 pop_assum mp_tac >> simp[] >>
2760 ‘count 2 ** B <<= A ** B’ suffices_by metis_tac[CARD_LE_COUNTABLE] >>
2761 irule set_exp_cardle_cong >> simp[] >> metis_tac[FINITE_012]) >~
2762 [‘A =~ {()}’]
2763 >- gvs[CARD1_SING, SING_set_exp] >>
2764 metis_tac[FINITE_EXPONENT_SETEXP_COUNTABLE]
2765QED
2766
2767(* NOTE: Changed the type of ‘t’ to ‘:'b->bool’ (was: 'a->bool) *)
2768Theorem CARD_EQ_COUNTABLE :
2769 !s:'a->bool t:'b->bool. COUNTABLE t /\ s =_c t ==> COUNTABLE s
2770Proof
2771 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
2772QED
2773
2774(* NOTE: Changed the type of ‘t’ to ‘:'b->bool’ (was: 'a->bool) *)
2775Theorem CARD_COUNTABLE_CONG :
2776 !s:'a->bool t:'b->bool. s =_c t ==> (COUNTABLE s <=> COUNTABLE t)
2777Proof
2778 REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
2779QED
2780
2781Theorem COUNTABLE_RESTRICT:
2782 !s P. COUNTABLE s ==> COUNTABLE {x | x IN s /\ P x}
2783Proof
2784 REPEAT GEN_TAC THEN
2785 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2786 SET_TAC[]
2787QED
2788
2789Theorem FINITE_IMP_COUNTABLE:
2790 !s. FINITE s ==> COUNTABLE s
2791Proof
2792 SIMP_TAC std_ss [FINITE_CARD_LT, Once lt_c, COUNTABLE, ge_c]
2793QED
2794
2795Theorem COUNTABLE_IMAGE:
2796 !f:'a->'b s. COUNTABLE s ==> COUNTABLE (IMAGE f s)
2797Proof
2798 SIMP_TAC std_ss [COUNTABLE, ge_c] THEN REPEAT STRIP_TAC THEN
2799 KNOW_TAC ``IMAGE (f:'a->'b) s <=_c s /\ s <=_c univ(:num)`` THENL
2800 [ASM_SIMP_TAC std_ss [CARD_LE_IMAGE], METIS_TAC [CARD_LE_TRANS]]
2801QED
2802
2803Theorem COUNTABLE_IMAGE_INJ_GENERAL:
2804 !(f:'a->'b) A s.
2805 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
2806 COUNTABLE A
2807 ==> COUNTABLE {x | x IN s /\ f(x) IN A}
2808Proof
2809 REPEAT STRIP_TAC THEN
2810 UNDISCH_TAC ``!x y. x IN s /\ y IN s /\ ((f:'a->'b) x = f y) ==>
2811 (x = y)`` THEN DISCH_TAC THEN
2812 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [INJECTIVE_ON_LEFT_INVERSE]) THEN
2813 DISCH_THEN(X_CHOOSE_TAC ``g:'b->'a``) THEN
2814 MATCH_MP_TAC COUNTABLE_SUBSET THEN EXISTS_TAC ``IMAGE (g:'b->'a) A`` THEN
2815 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE] THEN ASM_SET_TAC[]
2816QED
2817
2818Theorem COUNTABLE_IMAGE_INJ_EQ:
2819 !(f:'a->'b) s.
2820 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==>
2821 (COUNTABLE(IMAGE f s) <=> COUNTABLE s)
2822Proof
2823 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE] THEN
2824 POP_ASSUM MP_TAC THEN REWRITE_TAC[AND_IMP_INTRO] THEN
2825 DISCH_THEN(MP_TAC o MATCH_MP COUNTABLE_IMAGE_INJ_GENERAL) THEN
2826 csimp[IMAGE_IN]
2827QED
2828
2829Theorem COUNTABLE_IMAGE_INJ:
2830 !(f:'a->'b) A.
2831 (!x y. (f(x) = f(y)) ==> (x = y)) /\
2832 COUNTABLE A
2833 ==> COUNTABLE {x | f(x) IN A}
2834Proof
2835 REPEAT GEN_TAC THEN
2836 MP_TAC(SPECL [``f:'a->'b``, ``A:'b->bool``, ``UNIV:'a->bool``]
2837 COUNTABLE_IMAGE_INJ_GENERAL) THEN SIMP_TAC std_ss [IN_UNIV]
2838QED
2839
2840Theorem COUNTABLE_EMPTY:
2841 COUNTABLE {}
2842Proof
2843 REWRITE_TAC [COUNTABLE, ge_c, le_c, NOT_IN_EMPTY]
2844QED
2845
2846Theorem COUNTABLE_INTER:
2847 !s t. COUNTABLE s \/ COUNTABLE t ==> COUNTABLE (s INTER t)
2848Proof
2849 REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
2850 REPEAT GEN_TAC THEN CONJ_TAC THEN
2851 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2852 SET_TAC[]
2853QED
2854
2855Theorem COUNTABLE_UNION_IMP:
2856 !s t:'a->bool. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s UNION t)
2857Proof
2858 REWRITE_TAC[COUNTABLE, ge_c] THEN REPEAT STRIP_TAC THEN
2859 KNOW_TAC ``s UNION t <=_c ((s:'a->bool) +_c (t:'a->bool)) /\
2860 ((s:'a->bool) +_c (t:'a->bool)) <=_c univ(:num)`` THENL
2861 [ALL_TAC, METIS_TAC [CARD_LE_TRANS]] THEN
2862 ASM_SIMP_TAC std_ss [CARD_ADD2_ABSORB_LE, num_INFINITE, UNION_LE_ADD_C]
2863QED
2864
2865Theorem COUNTABLE_UNION:
2866 !s t:'a->bool. COUNTABLE(s UNION t) <=> COUNTABLE s /\ COUNTABLE t
2867Proof
2868 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[COUNTABLE_UNION_IMP] THEN
2869 DISCH_THEN(fn th => CONJ_TAC THEN MP_TAC th) THEN
2870 MATCH_MP_TAC(REWRITE_RULE[CONJ_EQ_IMP] COUNTABLE_SUBSET) THEN
2871 SET_TAC[]
2872QED
2873
2874Theorem COUNTABLE_SING:
2875 !x. COUNTABLE {x}
2876Proof
2877 REWRITE_TAC [COUNTABLE, ge_c, le_c, IN_SING, IN_UNIV] THEN
2878 METIS_TAC []
2879QED
2880
2881Theorem COUNTABLE_INSERT[simp]:
2882 !x s. COUNTABLE(x INSERT s) <=> COUNTABLE s
2883Proof
2884 ONCE_REWRITE_TAC[SET_RULE ``x INSERT s = {x} UNION s``] THEN
2885 REWRITE_TAC[COUNTABLE_UNION, COUNTABLE_SING]
2886QED
2887
2888Theorem COUNTABLE_DELETE[simp]:
2889 !x:'a s. COUNTABLE(s DELETE x) <=> COUNTABLE s
2890Proof
2891 REPEAT GEN_TAC THEN ASM_CASES_TAC ``(x:'a) IN s`` THEN
2892 ASM_SIMP_TAC std_ss [SET_RULE ``~(x IN s) ==> (s DELETE x = s)``] THEN
2893 MATCH_MP_TAC EQ_TRANS THEN
2894 EXISTS_TAC ``COUNTABLE((x:'a) INSERT (s DELETE x))`` THEN CONJ_TAC THENL
2895 [REWRITE_TAC[COUNTABLE_INSERT], AP_TERM_TAC THEN ASM_SET_TAC[]]
2896QED
2897
2898Theorem COUNTABLE_DIFF_FINITE:
2899 !s t. FINITE s ==> (COUNTABLE(t DIFF s) <=> COUNTABLE t)
2900Proof
2901 Induct_on ‘FINITE’ >>
2902 simp[SET_RULE ``s DIFF (x INSERT t) = (s DIFF t) DELETE x``]
2903QED
2904
2905Theorem UNCOUNTABLE_DIFF_COUNTABLE :
2906 !s t. ~COUNTABLE s /\ COUNTABLE t ==> ~COUNTABLE (s DIFF t)
2907Proof
2908 rpt STRIP_TAC
2909 >> ‘s DIFF t UNION (s INTER t) = s’ by SET_TAC []
2910 >> ‘COUNTABLE (s INTER t)’ by simp [COUNTABLE_INTER]
2911 >> METIS_TAC [COUNTABLE_UNION]
2912QED
2913
2914Theorem UNCOUNTABLE_DIFF_FINITE :
2915 !s t. ~COUNTABLE s /\ FINITE t ==> ~COUNTABLE (s DIFF t)
2916Proof
2917 PROVE_TAC [FINITE_IMP_COUNTABLE, UNCOUNTABLE_DIFF_COUNTABLE]
2918QED
2919
2920Theorem COUNTABLE_CROSS:
2921 !s t. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s CROSS t)
2922Proof
2923 rpt GEN_TAC
2924 >> REWRITE_TAC [COUNTABLE, ge_c]
2925 >> STRIP_TAC
2926 >> MATCH_MP_TAC (Q.SPEC `UNIV`
2927 (INST_TYPE [``:'c`` |-> ``:num``]
2928 (ISPECL [``s :'a set``, ``t :'b set``] CARD_MUL2_ABSORB_LE)))
2929 >> ASM_REWRITE_TAC [num_INFINITE]
2930QED
2931
2932Theorem COUNTABLE_AS_IMAGE_SUBSET:
2933 !s. COUNTABLE s ==> ?f. s SUBSET (IMAGE f univ(:num))
2934Proof
2935 REWRITE_TAC[COUNTABLE, ge_c, LE_C, SUBSET_DEF, IN_IMAGE] THEN MESON_TAC[]
2936QED
2937
2938Theorem COUNTABLE_AS_IMAGE_SUBSET_EQ:
2939 !s:'a->bool. COUNTABLE s <=> ?f. s SUBSET (IMAGE f univ(:num))
2940Proof
2941 REWRITE_TAC[COUNTABLE, ge_c, LE_C, SUBSET_DEF, IN_IMAGE] THEN MESON_TAC[]
2942QED
2943
2944Theorem COUNTABLE_AS_IMAGE:
2945 !s:'a->bool. COUNTABLE s /\ ~(s = {}) ==> ?f. (s = IMAGE f univ(:num))
2946Proof
2947 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(X_CHOOSE_TAC ``a:'a`` o
2948 REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
2949 FIRST_X_ASSUM(MP_TAC o MATCH_MP COUNTABLE_AS_IMAGE_SUBSET) THEN
2950 DISCH_THEN(X_CHOOSE_TAC ``f:num->'a``) THEN
2951 EXISTS_TAC ``\n. if (f:num->'a) n IN s then f n else a`` THEN
2952 ASM_SET_TAC[]
2953QED
2954
2955Theorem FORALL_COUNTABLE_AS_IMAGE:
2956 (!d. COUNTABLE d ==> P d) <=> P {} /\ (!f. P(IMAGE f univ(:num)))
2957Proof
2958 MESON_TAC[COUNTABLE_AS_IMAGE, COUNTABLE_IMAGE, NUM_COUNTABLE,
2959 COUNTABLE_EMPTY]
2960QED
2961
2962Theorem COUNTABLE_AS_INJECTIVE_IMAGE:
2963 !s. COUNTABLE s /\ INFINITE s
2964 ==> ?f. (s = IMAGE f univ(:num)) /\ (!m n. (f(m) = f(n)) ==> (m = n))
2965Proof
2966 GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
2967 REWRITE_TAC[INFINITE_CARD_LE, COUNTABLE, ge_c] THEN
2968 SIMP_TAC std_ss [CARD_LE_ANTISYM, eq_c] THEN SET_TAC[]
2969QED
2970
2971Theorem COUNTABLE_BIGUNION = bigunion_countable
2972
2973Theorem IN_ELIM_PAIR_THM:
2974 !P a b. (a,b) IN {(x,y) | P x y} <=> P a b
2975Proof
2976 SRW_TAC [][]
2977QED
2978
2979Theorem COUNTABLE_PRODUCT_DEPENDENT:
2980 !f:'a->'b->'c s t.
2981 COUNTABLE s /\ (!x. x IN s ==> COUNTABLE(t x)) ==>
2982 COUNTABLE {f x y | x IN s /\ y IN (t x)}
2983Proof
2984 REPEAT GEN_TAC THEN DISCH_TAC THEN
2985 SUBGOAL_THEN “{(f:'a->'b->'c) x y | x IN s /\ y IN (t x)} =
2986 IMAGE (λ(x,y). f x y) {(x,y) | x IN s /\ y IN (t x)}”
2987 SUBST1_TAC THENL
2988 [SIMP_TAC std_ss [EXTENSION, IN_IMAGE, EXISTS_PROD, IN_ELIM_PAIR_THM] THEN
2989 SET_TAC[],
2990 MATCH_MP_TAC COUNTABLE_IMAGE THEN POP_ASSUM MP_TAC] THEN
2991 CONV_TAC $ LAND_CONV $ REWRITE_CONV [COUNTABLE_AS_IMAGE_SUBSET_EQ] THEN
2992 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC “f:num->'a”) MP_TAC) THEN
2993 DISCH_THEN (MP_TAC o SIMP_RULE std_ss [RIGHT_IMP_EXISTS_THM]) THEN
2994 SIMP_TAC std_ss [SKOLEM_THM] THEN
2995 DISCH_THEN(X_CHOOSE_TAC “g:'a->num->'b”) THEN
2996 MATCH_MP_TAC COUNTABLE_SUBSET THEN
2997 EXISTS_TAC “IMAGE (λ(m,n). (f:num->'a) m,(g:'a->num->'b)(f m) n)
2998 (univ(:num) CROSS univ(:num))” THEN
2999 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, COUNTABLE_CROSS, NUM_COUNTABLE] THEN
3000 SIMP_TAC std_ss [SUBSET_DEF, FORALL_IN_BIGUNION] THEN
3001 SIMP_TAC std_ss [IN_IMAGE, FORALL_PROD, IN_ELIM_PAIR_THM,
3002 EXISTS_PROD, IN_CROSS, IN_UNIV] THEN
3003 ASM_SET_TAC[]
3004QED
3005
3006Definition BIGPRODi_def:
3007 BIGPRODi (A : 'i -> ('a -> bool) option) =
3008 {tup : 'i -> 'a option |
3009 (!i. A i = NONE ==> tup i = NONE) /\
3010 !i s. A i = SOME s ==> ?a. tup i = SOME a /\ a IN s
3011 }
3012End
3013
3014(* A^0 = 1 *)
3015Theorem BIGPRODi_KNONE[simp]:
3016 BIGPRODi (K NONE) = {K NONE}
3017Proof
3018 simp[BIGPRODi_def, EXTENSION, FUN_EQ_THM]
3019QED
3020
3021Definition fnOfSet_def:
3022 fnOfSet s k = if ?!v. (k,v) IN s then SOME (@v. (k,v) IN s) else NONE
3023End
3024
3025Theorem fnOfSet_SING[simp]:
3026 fnOfSet {(k,v)} = (K NONE)(| k |-> SOME v |)
3027Proof
3028 simp[fnOfSet_def, FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM] >>
3029 rw[] >> gs[]
3030QED
3031
3032Theorem BIGPRODi_SING_EQ:
3033 BIGPRODi (fnOfSet {(i,s)}) = { (K NONE)(| i |-> SOME a |) | a IN s }
3034Proof
3035 simp[BIGPRODi_def, combinTheory.APPLY_UPDATE_THM, Once EXTENSION] >>
3036 simp[FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM, AllCaseEqs()] >>
3037 qx_gen_tac ‘tup’ >> simp[EQ_IMP_THM] >> rw[] >~
3038 [‘tup i = SOME a’] >- (first_assum $ irule_at Any >> metis_tac[]) >~
3039 [‘tup j = NONE’] >- metis_tac[] >>
3040 metis_tac[]
3041QED
3042
3043Theorem BIGPRODi_SING_CEQ:
3044 BIGPRODi (fnOfSet {(i,s)}) =~ s
3045Proof
3046 simp[BIGPRODi_SING_EQ, cardeq_def, BIJ_IFF_INV, PULL_EXISTS] >>
3047 qexistsl_tac [‘λx. THE (x i)’, ‘λa j. if j = i then SOME a else NONE’] >>
3048 simp[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> metis_tac[]
3049QED
3050
3051Theorem BIGPRODi_pair:
3052 i <> j ==>
3053 BIGPRODi (K NONE)(| i |-> SOME A1; j |-> SOME A2|) =~ A1 CROSS A2
3054Proof
3055 strip_tac >>
3056 simp[BIGPRODi_def, cardeq_def, BIJ_IFF_INV, FORALL_PROD, PULL_EXISTS] >>
3057 qexistsl_tac [‘λt. (THE (t i), THE (t j))’,
3058 ‘λp k. if k = i then SOME (FST p)
3059 else if k = j then SOME (SND p) else NONE’] >>
3060 rw[] >~
3061 [‘THE (tup i) IN A’] >- (first_x_assum $ qspec_then ‘i’ mp_tac >>
3062 gs[combinTheory.APPLY_UPDATE_THM, PULL_EXISTS]) >~
3063 [‘THE (tup i) IN A’] >- (first_x_assum $ qspec_then ‘i’ mp_tac >>
3064 gs[combinTheory.APPLY_UPDATE_THM, PULL_EXISTS]) >>
3065 gs[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> rw[] >>
3066 gs[AllCaseEqs(), DISJ_IMP_THM, FORALL_AND_THM]
3067QED
3068
3069Theorem BIGPRODi_EQ_EMPTY:
3070 BIGPRODi Af = {} <=> ?i. Af i = SOME {}
3071Proof
3072 simp[BIGPRODi_def] >> Cases_on ‘!i. Af i = NONE’ >> simp[]
3073 >- (simp[EXTENSION] >> qexists_tac ‘K NONE’ >> simp[]) >> gs[] >>
3074 simp[Once EXTENSION] >> eq_tac >>
3075 rpt strip_tac >> gvs[] >~
3076 [‘Af j = SOME {}’] >- (disj2_tac >> qexists_tac ‘j’ >> simp[]) >>
3077 CCONTR_TAC >>
3078 qpat_x_assum ‘!x. _’ mp_tac >> simp[] >>
3079 qexists_tac ‘λj. OPTION_MAP CHOICE (Af j)’ >>
3080 simp[SF DISJ_ss] >> gs[] >> metis_tac[CHOICE_DEF, SOME_11]
3081QED
3082
3083Definition BIGPROD_def:
3084 BIGPROD (A : ('a -> bool) -> bool) =
3085 BIGPRODi (λa. if a IN A then SOME a else NONE)
3086End
3087
3088Theorem BIGPROD_thm:
3089 BIGPROD A =
3090 { tup : ('a -> bool) -> 'a option |
3091 (!s. s IN A ==> ?a. tup s = SOME a /\ a IN s) /\
3092 (!s. s NOTIN A ==> tup s = NONE) }
3093Proof
3094 simp[BIGPROD_def, BIGPRODi_def, FORALL_AND_THM, CONJ_COMM]
3095QED
3096
3097Theorem BIGPROD_pair:
3098 A1 <> A2 ==>
3099 BIGPROD { A1; A2 } =~ A1 CROSS A2
3100Proof
3101 strip_tac >> simp[BIGPROD_def] >>
3102 ‘(\a. if a = A1 \/ a = A2 then SOME a else NONE) =
3103 (K NONE)(| A1 |-> SOME A1; A2 |-> SOME A2|)’
3104 by simp[Once FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM, AllCaseEqs(),
3105 SF DISJ_ss] >>
3106 simp[BIGPRODi_pair]
3107QED
3108
3109Theorem BIGPROD_SING:
3110 BIGPROD {A} =~ A
3111Proof
3112 simp[cardeq_def, BIGPROD_thm, BIJ_IFF_INV] >>
3113 qexists_tac ‘λt. THE (t A)’ >> simp[PULL_EXISTS] >>
3114 qexists_tac ‘\a s. if s = A then SOME a else NONE’ >> rw[] >>
3115 simp[Once FUN_EQ_THM] >> rw[]
3116QED
3117
3118Theorem BIGPROD_ONE:
3119 BIGPROD {} =~ {()}
3120Proof
3121 simp[BIGPROD_thm, cardeq_def]>> qexists_tac ‘K ()’ >>
3122 simp[BIJ_IFF_INV] >> qexists_tac ‘K (K NONE)’ >> simp[] >>
3123 rpt strip_tac >> simp[FUN_EQ_THM]
3124QED
3125
3126Theorem BIGPROD_EQ_EMPTY[simp]:
3127 BIGPROD As = {} <=> {} IN As
3128Proof
3129 simp[BIGPROD_def, BIGPRODi_EQ_EMPTY]
3130QED
3131
3132Theorem image_thms[simp,local]:
3133 IMAGE OUTL (IMAGE INL A) = A /\
3134 IMAGE OUTR (IMAGE INR B) = B /\
3135 ((!x. x IN AB ==> ISL x) ==> (IMAGE INL (IMAGE OUTL AB) = AB)) /\
3136 ((!x. x IN AB ==> ISR x) ==> (IMAGE INR (IMAGE OUTR AB) = AB))
3137Proof
3138 rw[EXTENSION, PULL_EXISTS] >> csimp[INR, INL]
3139QED
3140
3141Theorem BIGPROD_CONS:
3142 A CROSS BIGPROD As =~ BIGPROD (IMAGE INL A INSERT IMAGE (IMAGE INR) As)
3143Proof
3144 Cases_on ‘A = {}’ >> simp[iffRL BIGPROD_EQ_EMPTY, CARDEQ_0] >>
3145 Cases_on ‘{} IN As’ >> simp[iffRL BIGPROD_EQ_EMPTY, CARDEQ_0] >>
3146 simp[BIGPROD_thm, BIJ_IFF_INV, cardeq_def, FORALL_PROD] >>
3147 qexists_tac ‘λ(p : 'a # (('b -> bool) -> 'b option)) (s: 'a + 'b -> bool).
3148 if s = EMPTY then NONE : ('a + 'b) option
3149 else if (!x. x IN s ==> ISL x) then
3150 if IMAGE OUTL s = A then SOME (INL (FST p)) else NONE
3151 else if (!x. x IN s ==> ISR x) /\ IMAGE OUTR s IN As then
3152 SOME (INR (THE (SND p (IMAGE OUTR s))))
3153 else NONE’ >>
3154 rw[] >> simp[PULL_EXISTS]
3155 >- (metis_tac[THE_DEF, MEMBER_NOT_EMPTY])
3156 >- (rename [‘s = {}’, ‘s <> IMAGE INL A’] >>
3157 rpt (IF_CASES_TAC >> gvs[])
3158 >- (qpat_x_assum ‘s <> IMAGE INL _’ mp_tac >>
3159 rw[CONTRAPOS_THM] >> gvs[]) >>
3160 gvs[DISJ_EQ_IMP]) >>
3161 qexists_tac ‘λtup. (OUTL (THE (tup (IMAGE INL A))),
3162 (λB. if B IN As then
3163 SOME (OUTR (THE (tup (IMAGE INR B))))
3164 else NONE))’ >> rw[] >>
3165 gvs[DISJ_IMP_THM, FORALL_AND_THM, PULL_EXISTS]
3166 >- (first_x_assum drule >> simp[PULL_EXISTS])
3167 >- (simp[Once FUN_EQ_THM] >> rw[]
3168 >- gs[]
3169 >- metis_tac[MEMBER_NOT_EMPTY]
3170 >- metis_tac[MEMBER_NOT_EMPTY]
3171 >- (last_x_assum drule >> simp[PULL_EXISTS]))
3172 >- (simp[Once FUN_EQ_THM] >> qx_gen_tac ‘AB’ >> rw[]
3173 >- gs[]
3174 >- (first_x_assum irule >> rpt strip_tac >> gvs[PULL_EXISTS] >>
3175 metis_tac[MEMBER_NOT_EMPTY])
3176 >- (first_x_assum drule >> simp[PULL_EXISTS])
3177 >- (gs[] >> first_x_assum irule >> rpt strip_tac >> gvs[]))
3178QED
3179
3180Theorem tupNONE_IN_BIGPRODi:
3181 tup IN BIGPRODi Af ==> (tup i = NONE <=> Af i = NONE)
3182Proof
3183 simp[BIGPRODi_def, EQ_IMP_THM] >> rpt strip_tac >>
3184 first_x_assum $ qspec_then ‘i’ mp_tac >> simp[] >>
3185 Cases_on ‘Af i’ >> simp[]
3186QED
3187
3188Theorem BIGPRODi_11[simp]:
3189 (!i. Af i <> SOME {}) /\ (!i. Bf i <> SOME ({}:'b set)) ==>
3190 (BIGPRODi Af = BIGPRODi Bf <=> Af = Bf)
3191Proof
3192 rpt strip_tac >> simp[EQ_IMP_THM] >>
3193 simp[Once EXTENSION] >> strip_tac >>
3194 simp[FUN_EQ_THM] >> qx_gen_tac ‘j’ >>
3195 Cases_on ‘Af j = NONE \/ Bf j = NONE’
3196 >- (‘?t. t IN BIGPRODi Af’
3197 suffices_by metis_tac[tupNONE_IN_BIGPRODi] >>
3198 simp[MEMBER_NOT_EMPTY] >> simp[BIGPRODi_EQ_EMPTY]) >> gs[] >>
3199 ‘(?s1. Af j = SOME s1) /\ (?s2. Bf j = SOME s2)’
3200 by (map_every Cases_on [‘Af j’, ‘Bf j’] >> gs[]) >> simp[] >>
3201 CCONTR_TAC >>
3202 wlog_tac ‘?e. e IN s1 /\ e NOTIN s2’ [‘s1’, ‘s2’, ‘Bf’, ‘Af’]
3203 >- (gs[] >>
3204 ‘!A B. (!e:'b. e NOTIN A \/ e IN B) <=> A SUBSET B’
3205 by metis_tac[SUBSET_DEF] >> gs[] >>
3206 first_x_assum $ qspecl_then [‘s2’, ‘s1’, ‘Af’, ‘Bf’] mp_tac >> simp[] >>
3207 metis_tac[SUBSET_ANTISYM]) >>
3208 ‘!tup. tup IN BIGPRODi Bf ==> tup j <> SOME e’
3209 by (simp[BIGPRODi_def] >> rpt strip_tac >>
3210 first_x_assum $ qspec_then ‘j’ mp_tac >> simp[]) >>
3211 ‘?tup. tup IN BIGPRODi Af /\ tup j = SOME e’ suffices_by metis_tac[] >>
3212 ‘?tup0. tup0 IN BIGPRODi Af’
3213 by simp[MEMBER_NOT_EMPTY, BIGPRODi_EQ_EMPTY] >>
3214 qexists_tac ‘tup0(| j |-> SOME e |)’ >>
3215 pop_assum mp_tac >> REWRITE_TAC [BIGPRODi_def] >>
3216 simp[combinTheory.APPLY_UPDATE_THM] >> rw[AllCaseEqs()] >>
3217 metis_tac[SOME_11]
3218QED
3219
3220Theorem cardeq_addUnum:
3221 INFINITE (univ(:'a)) ==> univ(:num + 'a) =~ univ(:'a)
3222Proof
3223 strip_tac >> irule cardleq_ANTISYM >>
3224 ‘univ(:'a) <<= univ(:num + 'a)’
3225 by (simp[cardleq_def]>> qexists_tac ‘INR’ >>
3226 simp[INJ_DEF]) >> simp[] >>
3227 ‘univ(:num) <<= univ(:'a)’ by gs[INFINITE_Unum] >>
3228 simp[disjUNION_UNIV, CARD_ADD_ABSORB_LE]
3229QED
3230
3231Theorem wellorder_destWO =
3232 wellorder_ABSREP |> cj 2
3233 |> Q.SPEC ‘destWO r’
3234 |> REWRITE_RULE [mkWO_destWO]
3235
3236Theorem cardleq_copy_wellorders:
3237 univ(:'a) <<= univ(:'b) ==>
3238 !w1 : 'a wellorder. ?w2: 'b wellorder. orderiso w1 w2
3239Proof
3240 simp[orderiso_def, cardleq_def, INJ_IFF] >>
3241 disch_then $ qx_choose_then ‘f’ strip_assume_tac >>
3242 qx_gen_tac ‘w1’ >> qabbrev_tac ‘W2 = {(f x, f y) | (x,y) IN destWO w1 }’ >>
3243 ‘wellorder (destWO w1)’ by simp[wellorder_destWO] >>
3244 ‘wellorder W2’
3245 by (‘W2 = IMAGE (f ## f) (destWO w1)’
3246 by simp[Abbr‘W2’, EXTENSION, EXISTS_PROD] >>
3247 simp[] >> irule INJ_preserves_wellorder >>
3248 simp[wellorder_destWO] >> qexists_tac ‘UNIV’ >>
3249 simp[INJ_IFF]) >>
3250 qexistsl_tac [‘mkWO W2’, ‘f’] >>
3251 ‘elsOf (mkWO W2) = { f x | x IN elsOf w1}’
3252 by (simp[elsOf_def, Abbr‘W2’, destWO_mkWO, domain_def, range_def] >>
3253 dsimp[EXTENSION] >> metis_tac[]) >>
3254 simp[PULL_EXISTS] >>
3255 simp[destWO_mkWO] >> simp[strict_def, Abbr‘W2’]
3256QED
3257
3258Theorem finite_subsets_bijection:
3259 INFINITE A ==> A =~ { s | FINITE s /\ s SUBSET A }
3260Proof
3261 strip_tac >> match_mp_tac cardleq_ANTISYM >> conj_tac
3262 >- (simp[cardleq_def] >> qexists_tac `\a. {a}` >>
3263 simp[INJ_DEF]) >>
3264 ‘{s | FINITE s ∧ s ⊆ A} =
3265 BIGUNION (IMAGE (λn. { s | s ⊆ A ∧ s HAS_SIZE n }) univ(:num))’
3266 by (simp[Once EXTENSION, PULL_EXISTS, EQ_IMP_THM] >> rpt strip_tac >>
3267 gvs[HAS_SIZE]) >>
3268 simp[] >> irule CARD_BIGUNION >> simp[PULL_EXISTS] >> conj_tac >~
3269 [‘IMAGE _ _ ≼ A’]
3270 >- (irule IMAGE_cardleq_rwt >> gvs[INFINITE_Unum]) >>
3271 qx_gen_tac ‘n’ >> Cases_on ‘n = 0’
3272 >- (simp[HAS_SIZE_0, SF CONJ_ss] >> ‘A ≠ ∅’ by (strip_tac >> gvs[]) >>
3273 gvs[GSYM MEMBER_NOT_EMPTY] >> rename [‘a ∈ A’] >>
3274 simp[cardleq_def] >> qexists_tac ‘λx. a’ >> simp[INJ_DEF]) >>
3275 ‘0 < n’ by gvs[NOT_ZERO] >>
3276 drule_all_then (assume_tac o ONCE_REWRITE_RULE[cardeq_SYM])
3277 exp_count_cardeq >>
3278 resolve_then (Pos hd) (dxrule_then (irule o iffRL)) cardeq_REFL CARD_LE_CONG >>
3279 ‘∀s. s HAS_SIZE n ⇒ ∃f. SURJ f (count n) s ∧ ∀m. n ≤ m ⇒ f m = ARB’
3280 by (rpt (pop_assum kall_tac) >> simp[HAS_SIZE] >> qid_spec_tac ‘n’ >>
3281 Induct_on ‘FINITE’ >> simp[SURJ_EMPTY] >> rw[] >> simp[K_lemma] >>
3282 gvs[SURJ_DEF] >> rename [‘g _ ∈ A’, ‘e ∉ A’] >>
3283 qexists_tac
3284 ‘λn. if n < CARD A then g n else if n = CARD A then e else ARB’ >>
3285 simp[AllCaseEqs(), DISJ_IMP_THM, FORALL_AND_THM,
3286 DECIDE “x < SUC y ⇔ x = y ∨ x < y”] >>
3287 rw[] >> simp[SF ARITH_ss] >>
3288 metis_tac[LESS_REFL]) >>
3289 gvs[GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] >>
3290 rename [‘SURJ (FF _) (count n)’] >>
3291 simp[cardleq_def, INJ_DEF] >> qexists_tac ‘FF’ >> rw[] >~
3292 [‘FF A0 ∈ A ** count n’]
3293 >- (simp[set_exp_def] >> first_x_assum $ drule_then strip_assume_tac >>
3294 gvs[NOT_LESS, SURJ_DEF, SUBSET_DEF]) >>
3295 rename [‘A1 HAS_SIZE n’, ‘A2 HAS_SIZE n’, ‘FF A1 = FF A2’] >>
3296 CCONTR_TAC >>
3297 ‘∃a. a ∈ A1 ∧ a ∉ A2’
3298 suffices_by (strip_tac >>
3299 ‘∃i. FF A1 i = a ∧ i < n ∧ FF A2 i ≠ a’
3300 by metis_tac[SURJ_DEF]>>
3301 qpat_x_assum ‘FF A1 = FF A2’ mp_tac >>
3302 simp[FUN_EQ_THM] >> metis_tac[]) >>
3303 CCONTR_TAC >> gvs[] >> ‘A1 ⊆ A2’ by ASM_SET_TAC[] >>
3304 metis_tac[SUBSET_EQ_CARD, HAS_SIZE]
3305QED
3306
3307(* ------------------------------------------------------------------------- *)
3308(* Misc lemmas from HOL-Light's card.ml *)
3309(* ------------------------------------------------------------------------- *)
3310
3311Theorem MUL_C_UNIV = SYM CROSS_UNIV
3312Theorem CARD_MUL_FINITE_EQ = FINITE_CROSS_EQ
3313
3314Theorem INJECTIVE_ON_ALT :
3315 !P (f :'a -> 'b).
3316 (!x y. P x /\ P y /\ f x = f y ==> x = y) <=>
3317 (!x y. P x /\ P y ==> (f x = f y <=> x = y))
3318Proof
3319 MESON_TAC[]
3320QED
3321
3322Theorem INJECTIVE_ALT :
3323 !f :'a -> 'b. (!x y. f x = f y ==> x = y) <=> (!x y. f x = f y <=> x = y)
3324Proof
3325 MESON_TAC[]
3326QED