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