1(* interactive mode 2loadPath := ["../ho_prover","../subtypes","../rsa"] @ !loadPath; 3app load ["bossLib","subtypeTheory","HurdUseful","extra_boolTheory", 4 "boolContext","extra_listTheory","listContext", 5 "state_transformerTheory"]; 6quietdec := true; 7*) 8 9open HolKernel Parse boolLib bossLib arithmeticTheory combinTheory 10 pred_setTheory HurdUseful boolContext listTheory 11 res_quanTools res_quanTheory subtypeTheory subtypeTools 12 extra_listTheory ho_proverTools listContext extra_numTheory 13 pairTheory state_transformerTheory simpLib; 14 15(* interactive mode 16quietdec := false; 17*) 18 19val _ = new_theory "extra_pred_set"; 20 21(* ------------------------------------------------------------------------- *) 22(* Tools. *) 23(* ------------------------------------------------------------------------- *) 24 25val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC; 26 27val std_pc = precontext_mergel [bool_pc, list_pc]; 28val std_c = precontext_compile std_pc; 29 30val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS std_c; 31 32val Strip = S_TAC; 33val Simplify = R_TAC; 34val bool_ss = boolSimps.bool_ss; 35val Cond = 36 MATCH_MP_TAC (PROVE [] ``!a b c. a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 37 >> CONJ_TAC; 38 39(* ------------------------------------------------------------------------- *) 40(* Definitions. *) 41(* ------------------------------------------------------------------------- *) 42 43val IMAGE2_def = Define `IMAGE2 f s t = {f x y | x IN s /\ y IN t}`; 44 45val UNIONL_def = Define `(UNIONL [] = {}) 46 /\ (UNIONL (s::ss) = (s:'a->bool) UNION UNIONL ss)`; 47 48val DISJOINTL_def = Define `(DISJOINTL [] = T) 49 /\ (DISJOINTL (s::ss) = DISJOINT (s:'a->bool) (UNIONL ss) /\ DISJOINTL ss)`; 50 51val (list_elts_def, list_elts_ind) = ((Q.GEN `s` ## I) o Defn.tprove) 52 let val d = Defn.Hol_defn "list_elts" `list_elts (s:'a->bool) 53 = if FINITE s then 54 (if s = {} then [] 55 else (CHOICE s)::(list_elts (s DELETE (CHOICE s)))) 56 else ARB` 57 val m = `measure CARD` 58 in (d, 59 WF_REL_TAC m 60 >> RW_TAC std_ss [] 61 >> MP_TAC (Q.SPEC `s` CARD_DELETE) 62 >> ASM_REWRITE_TAC [] 63 >> DISCH_THEN (MP_TAC o Q.SPEC `CHOICE s`) 64 >> RW_TAC arith_ss [CHOICE_DEF] 65 >> MP_TAC (Q.SPEC `s` CARD_EQ_0) 66 >> RW_TAC arith_ss []) 67 end; 68 69val _ = save_thm ("list_elts_def", list_elts_def); 70val _ = save_thm ("list_elts_ind", list_elts_ind); 71 72val set_def = Define `set p s = s SUBSET p`; 73 74val nonempty_def = Define `nonempty s = ~(s = {})`; 75 76val range_def = Define `range f = IMAGE f UNIV`; 77 78(* ------------------------------------------------------------------------- *) 79(* Theorems. *) 80(* ------------------------------------------------------------------------- *) 81 82val IN_o = store_thm 83 ("IN_o", 84 ``!x f s. x IN (s o f) = f x IN s``, 85 RW_TAC std_ss [SPECIFICATION, o_THM]); 86 87val UNION_DEF_ALT = store_thm 88 ("UNION_DEF_ALT", 89 ``!s t. s UNION t = (\x:'a. s x \/ t x)``, 90 REPEAT STRIP_TAC 91 >> Suff `!v:'a. v IN (s UNION t) = v IN (\x. s x \/ t x)` 92 >- (PURE_REWRITE_TAC [SPECIFICATION] 93 >> PROVE_TAC [EQ_EXT]) 94 >> RW_TAC std_ss [UNION_DEF, GSPECIFICATION] 95 >> RW_TAC std_ss [SPECIFICATION]); 96 97val INTER_UNION_RDISTRIB = store_thm 98 ("INTER_UNION_RDISTRIB", 99 ``!(p:'a->bool) q r. (p UNION q) INTER r = p INTER r UNION q INTER r``, 100 RW_TAC std_ss [EXTENSION, IN_UNION, IN_INTER] 101 >> PROVE_TAC []); 102 103val INTER_IS_EMPTY = store_thm 104 ("INTER_IS_EMPTY", 105 ``!(s:'a->bool) t. (s INTER t = {}) = (!x. ~s x \/ ~t x)``, 106 RW_TAC std_ss [INTER_DEF, EXTENSION, GSPECIFICATION] 107 >> RW_TAC std_ss [SPECIFICATION, EMPTY_DEF]); 108 109val GSPEC_DEF_ALT = store_thm 110 ("GSPEC_DEF_ALT", 111 ``!(f:'a -> 'b # bool). GSPEC f = (\v. ?x. (v, T) = f x)``, 112 RW_TAC std_ss [EXTENSION, GSPECIFICATION] 113 >> RW_TAC std_ss [SPECIFICATION]); 114 115val UNION_DISJOINT_SPLIT = store_thm 116 ("UNION_DISJOINT_SPLIT", 117 ``!(s:'a->bool) t u. (s UNION t = s UNION u) 118 /\ (s INTER t = {}) /\ (s INTER u = {}) 119 ==> (t = u)``, 120 RW_TAC std_ss [UNION_DEF_ALT, EXTENSION, INTER_IS_EMPTY, SPECIFICATION] 121 >> PROVE_TAC []); 122 123val INSERT_THM1 = store_thm 124 ("INSERT_THM1", 125 ``!(x:'a) s. x IN (x INSERT s)``, RW_TAC std_ss [IN_INSERT]); 126 127val INSERT_THM2 = store_thm 128 ("INSERT_THM2", 129 ``!(x:'a) y s. x IN s ==> x IN (y INSERT s)``, RW_TAC std_ss [IN_INSERT]); 130 131val IMAGE_THM = store_thm 132 ("IMAGE_THM", 133 ``!(f:'a->'b) x s. x IN s ==> f x IN IMAGE f s``, 134 RW_TAC std_ss [IN_IMAGE] 135 >> PROVE_TAC []); 136 137val ELT_IN_DELETE = store_thm 138 ("ELT_IN_DELETE", 139 ``!x s. ~(x IN (s DELETE x))``, 140 RW_TAC std_ss [IN_DELETE]); 141 142val FINITE_INTER = store_thm 143 ("FINITE_INTER", 144 ``!s. FINITE s ==> !t. FINITE (t INTER s)``, 145 PROVE_TAC [INTER_FINITE, INTER_COMM]); 146 147val IN_IMAGE2 = store_thm 148 ("IN_IMAGE2", 149 ``!x f s t. x IN IMAGE2 f s t = ?a b. a IN s /\ b IN t /\ (f a b = x)``, 150 RW_TAC std_ss [IMAGE2_def, GSPECIFICATION] 151 >> EQ_TAC >| 152 [RW_TAC std_ss [] 153 >> POP_ASSUM MP_TAC 154 >> Cases_on `x'` 155 >> RW_TAC std_ss [] 156 >> PROVE_TAC [], 157 RW_TAC std_ss [] 158 >> Q.EXISTS_TAC `(a, b)` 159 >> RW_TAC std_ss []]); 160 161val CONJ_IMAGE2 = store_thm 162 ("CONJ_IMAGE2", 163 ``!a b s t. 164 (b ==> a IN s) /\ (a ==> b IN t) ==> 165 ((a /\ b) IN ({F} UNION IMAGE2 $/\ s t))``, 166 RW_TAC std_ss [IN_UNION, IN_IMAGE2, IN_INSERT, NOT_IN_EMPTY] 167 >> Suff `a /\ b ==> ?a' b'. a' IN s /\ b' IN t /\ (a' /\ b' = a /\ b)` 168 >- (Q.SPEC_TAC (`?a' b'. a' IN s /\ b' IN t /\ (a' /\ b' = a /\ b)`, `q`) 169 >> PROVE_TAC []) 170 >> RW_TAC std_ss [] 171 >> PROVE_TAC []); 172 173val INJ_SUBSET = store_thm 174 ("INJ_SUBSET", 175 ``!f s s' t. INJ f s t /\ s' SUBSET s ==> INJ f s' t``, 176 RW_TAC std_ss [INJ_DEF, SUBSET_DEF]); 177 178val CARD_IMAGE = store_thm 179 ("CARD_IMAGE", 180 ``!f s t. FINITE s /\ INJ f s t ==> (CARD (IMAGE f s) = CARD s)``, 181 Suff `!s. FINITE s ==> !f t. INJ f s t ==> (CARD (IMAGE f s) = CARD s)` 182 >- PROVE_TAC [] 183 >> HO_MATCH_MP_TAC FINITE_INDUCT 184 >> RW_TAC std_ss [IMAGE_EMPTY, CARD_DEF, IMAGE_INSERT] 185 >> Know `~(f e IN IMAGE f s)` 186 >- (rpt (POP_ASSUM MP_TAC) 187 >> RW_TAC std_ss [IN_INSERT, IN_IMAGE, INJ_DEF] 188 >> PROVE_TAC []) 189 >> MP_TAC (Q.SPEC `s` IMAGE_FINITE) 190 >> RW_TAC std_ss [CARD_INSERT] 191 >> Suff `INJ f s t` >- PROVE_TAC [] 192 >> MATCH_MP_TAC INJ_SUBSET 193 >> RW_TAC std_ss [SUBSET_DEF] 194 >> PROVE_TAC [IN_INSERT]); 195 196val CARD_SUBSET_PROPER = store_thm 197 ("CARD_SUBSET_PROPER", 198 ``!(s:'a->bool) t. 199 FINITE t /\ s SUBSET t ==> ((CARD s = CARD t) = (s = t))``, 200 RW_TAC std_ss [] 201 >> Cases_on `s = t` >- PROVE_TAC [] 202 >> Know `s PSUBSET t` >- PROVE_TAC [PSUBSET_DEF] 203 >> STRIP_TAC 204 >> MP_TAC (Q.SPEC `t` CARD_PSUBSET) 205 >> ASM_REWRITE_TAC [] 206 >> DISCH_THEN (MP_TAC o Q.SPEC `s`) 207 >> RW_TAC arith_ss []); 208 209val LIST_ELTS = store_thm 210 ("LIST_ELTS", 211 ``!(s:'a->bool). FINITE s ==> (!v. MEM v (list_elts s) = v IN s)``, 212 recInduct list_elts_ind 213 >> RW_TAC std_ss [] 214 >> Cases_on `s = {}` 215 >- (MP_TAC (Q.SPEC `s` list_elts_def) 216 >> RW_TAC std_ss [FINITE_EMPTY, MEM, NOT_IN_EMPTY]) 217 >> Know `FINITE (s DELETE CHOICE s)` >- PROVE_TAC [FINITE_DELETE] 218 >> S_TAC 219 >> RES_TAC 220 >> NTAC 2 (POP_ASSUM (K ALL_TAC)) 221 >> ONCE_REWRITE_TAC [list_elts_def] 222 >> RW_TAC std_ss [] 223 >> Cases_on `v = CHOICE s` 224 >- (RW_TAC std_ss [CHOICE_DEF] 225 >> RW_TAC std_ss [SPECIFICATION, MEM]) 226 >> Q.PAT_X_ASSUM `!v. P v` (MP_TAC o Q.SPEC `v`) 227 >> MP_TAC (Q.SPECL [`s`, `v`, `CHOICE s`] IN_DELETE) 228 >> ASM_REWRITE_TAC [] 229 >> RW_TAC std_ss [MEM, SPECIFICATION]); 230 231val FINITE_UNIONL = store_thm 232 ("FINITE_UNIONL", 233 ``!(ss:('a->bool) list). FINITE (UNIONL ss) = EVERY FINITE ss``, 234 Induct >- RW_TAC list_ss [UNIONL_def, FINITE_EMPTY] 235 >> RW_TAC list_ss [UNIONL_def, FINITE_UNION]); 236 237val CARD_UNIONL = store_thm 238 ("CARD_UNIONL", 239 ``!(ss:('a->bool) list). EVERY FINITE ss /\ DISJOINTL ss 240 ==> (CARD (UNIONL ss) = sum (MAP CARD ss))``, 241 Induct >- RW_TAC list_ss [DISJOINTL_def, UNIONL_def, sum_def, CARD_DEF] 242 >> RW_TAC list_ss [DISJOINTL_def, UNIONL_def, sum_def] 243 >> Know `FINITE (UNIONL ss)` >- RW_TAC std_ss [FINITE_UNIONL] 244 >> MP_TAC (Q.SPECL [`h`] CARD_UNION) 245 >> ASM_REWRITE_TAC [] 246 >> DISCH_THEN (MP_TAC o Q.SPEC `UNIONL ss`) 247 >> Q.PAT_X_ASSUM `DISJOINT a b` MP_TAC 248 >> RW_TAC arith_ss [DISJOINT_DEF, CARD_DEF]); 249 250val IN_UNIONL = store_thm 251 ("IN_UNIONL", 252 ``!l (v:'a). v IN UNIONL l = (?s. MEM s l /\ v IN s)``, 253 Induct >- RW_TAC std_ss [UNIONL_def, MEM, NOT_IN_EMPTY] 254 >> RW_TAC std_ss [UNIONL_def, MEM, NOT_IN_EMPTY, IN_UNION] 255 >> PROVE_TAC []); 256 257val DISJOINT_UNION1 = DISJOINT_UNION; 258val DISJOINT_UNION2 = ONCE_REWRITE_RULE [DISJOINT_SYM] DISJOINT_UNION1; 259 260val DISJOINT_UNIONL2 = store_thm 261 ("DISJOINT_UNIONL2", 262 ``!l (x:'a->bool). DISJOINT x (UNIONL l) = (!y. MEM y l ==> DISJOINT x y)``, 263 Induct >- RW_TAC std_ss [UNIONL_def, MEM, DISJOINT_DEF, INTER_EMPTY] 264 >> RW_TAC std_ss [UNIONL_def, MEM, DISJOINT_UNION2] 265 >> PROVE_TAC []); 266val DISJOINT_UNIONL1 = ONCE_REWRITE_RULE [DISJOINT_SYM] DISJOINT_UNIONL2; 267 268val DISJOINTL_KILL_DUPS = store_thm 269 ("DISJOINTL_KILL_DUPS", 270 ``!(l:('a->bool) list). DISJOINTL (kill_dups l) 271 = (!x y. MEM x l /\ MEM y l ==> (x = y) \/ DISJOINT x y)``, 272 Induct >- RW_TAC list_ss [DISJOINTL_def, MEM, kill_dups_def, FOLDR] 273 >> REWRITE_TAC [kill_dups_def, FOLDR] 274 >> (RW_TAC std_ss [GSYM kill_dups_def, MEM, DISJOINTL_def, MEM_KILL_DUPS, 275 DISJOINT_UNIONL2] 276 >> EQ_TAC 277 >> RW_TAC std_ss [] 278 >> PROVE_TAC [DISJOINT_SYM])); 279 280val NUM_TO_FINITE = store_thm 281 ("NUM_TO_FINITE", 282 ``!s (f:num->'a). 283 FINITE s /\ (!n. f n IN s) ==> ?i j. i < j /\ (f i = f j)``, 284 Suff `!s. FINITE s ==> !(f:num->'a). (!n. f n IN s) 285 ==> ?i j. i < j /\ (f i = f j)` 286 >- PROVE_TAC [] 287 >> HO_MATCH_MP_TAC FINITE_INDUCT 288 >> REWRITE_TAC [NOT_IN_EMPTY] 289 >> RW_TAC std_ss [IN_INSERT] 290 >> Cases_on `?n. !m. m >= n ==> ~(f m = e)` >| 291 [POP_ASSUM MP_TAC 292 >> STRIP_TAC 293 >> Q.PAT_X_ASSUM `!f. (!n. P f n) ==> Q f` (MP_TAC o Q.SPEC `(\x. f (x + n))`) 294 >> Know `!n'. f (n + n') IN s` 295 >- (STRIP_TAC 296 >> Suff `n + n' >= n` >- PROVE_TAC [] 297 >> DECIDE_TAC) 298 >> RW_TAC arith_ss [] 299 >> Suff `i + n < j + n` >- PROVE_TAC [] 300 >> DECIDE_TAC, 301 POP_ASSUM MP_TAC 302 >> RW_TAC std_ss [] 303 >> POP_ASSUM (fn th => MP_TAC th >> MP_TAC (Q.SPEC `0` th)) 304 >> RW_TAC std_ss [] 305 >> POP_ASSUM (MP_TAC o Q.SPEC `SUC m`) 306 >> RW_TAC arith_ss [] 307 >> Suff `m < m'` >- PROVE_TAC [] 308 >> DECIDE_TAC]); 309 310val SURJ_ALT = store_thm 311 ("SURJ_ALT", 312 ``!f s t. SURJ f s t = f IN (s -> t) /\ (!y :: t. ?x :: s. y = f x)``, 313 S_TAC 314 >> R_TAC [SURJ_DEF] 315 >> RESQ_TAC 316 >> R_TAC [IN_FUNSET, IN_DFUNSET] 317 >> PROVE_TAC []); 318 319val BIJ_ALT_RES = store_thm 320 ("BIJ_ALT_RES", 321 ``!f s t. BIJ f s t = f IN (s -> t) /\ (!y :: t. ?!x :: s. y = f x)``, 322 S_TAC 323 >> R_TAC [BIJ_DEF, INJ_DEF, SURJ_DEF, RES_EXISTS_UNIQUE_ALT] 324 >> RESQ_TAC 325 >> R_TAC [IN_FUNSET, IN_DFUNSET, GSYM CONJ_ASSOC] 326 >> Know `!a b c. (a ==> (b = c)) ==> (a /\ b = a /\ c)` >- PROVE_TAC [] 327 >> DISCH_THEN MATCH_MP_TAC 328 >> REPEAT (STRIP_TAC ORELSE EQ_TAC) >| 329 [PROVE_TAC [], 330 Q.PAT_X_ASSUM `!x. P x` 331 (fn th => 332 MP_TAC (Q.SPEC `(f:'a->'b) x` th) 333 >> MP_TAC (Q.SPEC `(f:'a->'b) y` th)) 334 >> Cond >- PROVE_TAC [] 335 >> STRIP_TAC 336 >> Cond >- PROVE_TAC [] 337 >> STRIP_TAC 338 >> PROVE_TAC [], 339 PROVE_TAC []]); 340 341val DELETE_THEN_INSERT = store_thm 342 ("DELETE_THEN_INSERT", 343 ``!s. !x :: s. x INSERT (s DELETE x) = s``, 344 RESQ_TAC 345 >> R_TAC [INSERT_DELETE]); 346 347val BIJ_INSERT_NOTIN = store_thm 348 ("BIJ_INSERT_NOTIN", 349 ``!f e s t. 350 ~(e IN s) /\ BIJ f (e INSERT s) t ==> 351 ?u. (f e INSERT u = t) /\ ~(f e IN u) /\ BIJ f s u``, 352 R_TAC [BIJ_ALT_RES] 353 >> S_TAC 354 >> Q.EXISTS_TAC `t DELETE f e` 355 >> AR_TAC [IN_FUNSET, DELETE_THEN_INSERT, ELT_IN_DELETE, IN_INSERT, 356 DISJ_IMP_THM] 357 >> RESQ_TAC 358 >> AR_TAC [IN_DELETE, IN_INSERT] 359 >> REPEAT STRIP_TAC 360 >> METIS_TAC []); 361 362val FINITE_MAXIMAL = store_thm 363 ("FINITE_MAXIMAL", 364 ``!f s. FINITE s /\ ~(s = {}) ==> ?x :: s. !y :: s. (f y:num) <= f x``, 365 STRIP_TAC 366 >> R_TAC [GSYM AND_IMP_INTRO] 367 >> HO_MATCH_MP_TAC FINITE_INDUCT 368 >> R_TAC [] 369 >> S_TAC 370 >> Cases_on `s = {}` 371 >- (Q_RESQ_EXISTS_TAC `e` 372 >> AR_TAC [] 373 >> S_TAC 374 >> AR_TAC [IN_SING]) 375 >> RES_TAC 376 >> S_TAC 377 >> Know `(f:'a->num) e <= f x \/ f x <= f e` >- DECIDE_TAC 378 >> S_TAC >| 379 [Q_RESQ_EXISTS_TAC `x` 380 >> R_TAC [] 381 >> S_TAC 382 >> POP_ASSUM MP_TAC 383 >> R_TAC [IN_INSERT] 384 >> S_TAC >- R_TAC [] 385 >> Q.PAT_X_ASSUM `!y :: s. f y <= f x` (MP_TAC o Q_RESQ_SPEC `y`) 386 >> R_TAC [], 387 Q_RESQ_EXISTS_TAC `e` 388 >> R_TAC [] 389 >> S_TAC 390 >> POP_ASSUM MP_TAC 391 >> R_TAC [IN_INSERT] 392 >> S_TAC >- R_TAC [] 393 >> Q.PAT_X_ASSUM `!y :: s. f y <= f x` (MP_TAC o Q_RESQ_SPEC `y`) 394 >> DECIDE_TAC]); 395 396val EMPTY_UNION_ALT = store_thm 397 ("EMPTY_UNION_ALT", 398 ``!s t. ({} = s UNION t) = (s = {}) /\ (t = {})``, 399 PROVE_TAC [EMPTY_UNION]); 400 401val IN_SET = store_thm 402 ("IN_SET", 403 ``!s p. s IN set p = s SUBSET p``, 404 RW_TAC std_ss [SPECIFICATION, set_def]); 405 406val IN_NONEMPTY = store_thm 407 ("IN_NONEMPTY", 408 ``!s p. s IN nonempty = ~(s = {})``, 409 RW_TAC std_ss [SPECIFICATION, nonempty_def]); 410 411val IN_FINITE = store_thm 412 ("IN_FINITE", 413 ``!s. s IN FINITE = FINITE s``, 414 RW_TAC std_ss [SPECIFICATION]); 415 416val EMPTY_SUBTYPE = store_thm 417 ("EMPTY_SUBTYPE", 418 ``!x. {} IN (set x INTER FINITE)``, 419 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET]); 420 421val INSERT_SUBTYPE = store_thm 422 ("INSERT_SUBTYPE", 423 ``!x. $INSERT IN ((x -> set x -> set x) INTER 424 (UNIV -> FINITE -> FINITE) INTER 425 (UNIV -> UNIV -> nonempty))``, 426 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 427 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INSERT, 428 IN_NONEMPTY, NOT_INSERT_EMPTY]); 429 430val INTER_SUBTYPE = store_thm 431 ("INTER_SUBTYPE", 432 ``!x. $INTER IN ((set x -> UNIV -> set x) INTER 433 (UNIV -> set x -> set x) INTER 434 (UNIV -> FINITE -> FINITE) INTER 435 (FINITE -> UNIV -> FINITE))``, 436 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 437 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INTER, 438 INTER_FINITE, SUBSET_DEF]); 439 440val UNION_SUBTYPE = store_thm 441 ("UNION_SUBTYPE", 442 ``!x. $UNION IN ((set x -> set x -> set x) INTER 443 (FINITE -> FINITE -> FINITE) INTER 444 (UNIV -> nonempty -> nonempty))``, 445 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 446 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INTER, 447 INTER_FINITE, SUBSET_DEF, FINITE_UNION, IN_UNION, 448 IN_NONEMPTY, EMPTY_UNION] 449 >> PROVE_TAC []); 450 451val CHOICE_SUBTYPE = store_thm 452 ("CHOICE_SUBTYPE", 453 ``!x. CHOICE IN ((nonempty INTER set x) -> x)``, 454 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 455 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INTER, 456 INTER_FINITE, SUBSET_DEF, FINITE_UNION, IN_UNION, IN_NONEMPTY, 457 CHOICE_DEF]); 458 459val REST_SUBTYPE = store_thm 460 ("REST_SUBTYPE", 461 ``!x. REST IN ((FINITE -> FINITE) INTER 462 (set x -> set x))``, 463 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 464 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INTER, 465 INTER_FINITE, SUBSET_DEF, FINITE_UNION, IN_UNION, IN_NONEMPTY, 466 CHOICE_DEF, REST_DEF, FINITE_DELETE, IN_DELETE]); 467 468val DELETE_SUBTYPE = store_thm 469 ("DELETE_SUBTYPE", 470 ``!x. $DELETE IN ((set x -> UNIV -> set x) INTER 471 (FINITE -> UNIV -> FINITE))``, 472 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 473 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INSERT, 474 IN_NONEMPTY, NOT_INSERT_EMPTY, FINITE_DELETE, SUBSET_DEF, 475 IN_DELETE]); 476 477val IMAGE_SUBTYPE = store_thm 478 ("IMAGE_SUBTYPE", 479 ``!x y. IMAGE IN (((x -> y) -> set x -> set y) INTER 480 (UNIV -> nonempty -> nonempty) INTER 481 (UNIV -> FINITE -> FINITE))``, 482 RW_TAC std_ss [IN_SET, IN_INTER, IN_FINITE, FINITE_EMPTY, EMPTY_SUBSET, 483 IN_FUNSET, IN_UNIV, INSERT_SUBSET, FINITE_INSERT, 484 IN_NONEMPTY, NOT_INSERT_EMPTY, FINITE_DELETE, SUBSET_DEF, 485 IN_DELETE, IN_IMAGE, IMAGE_EQ_EMPTY, IMAGE_FINITE] 486 >> PROVE_TAC []); 487 488val SET_UNIV = store_thm 489 ("SET_UNIV", 490 ``set UNIV = UNIV``, 491 SET_EQ_TAC 492 >> RW_TAC std_ss [IN_SET, IN_UNIV, SUBSET_UNIV]); 493 494val SET_SUBSET = store_thm 495 ("SET_SUBSET", 496 ``!x y. x SUBSET y ==> set x SUBSET set y``, 497 RW_TAC std_ss [IN_SET, SUBSET_DEF]); 498 499val FINITE_SUBTYPE_JUDGEMENT = store_thm 500 ("FINITE_SUBTYPE_JUDGEMENT", 501 ``!s. FINITE s ==> s IN FINITE``, 502 RW_TAC std_ss [SPECIFICATION]); 503 504val FINITE_SUBTYPE_REWRITE = store_thm 505 ("FINITE_SUBTYPE_REWRITE", 506 ``!s. s IN FINITE ==> FINITE s``, 507 RW_TAC std_ss [SPECIFICATION]); 508 509val NONEMPTY_SUBTYPE_JUDGEMENT = store_thm 510 ("NONEMPTY_SUBTYPE_JUDGEMENT", 511 ``!s x. (x IN s) \/ ~(s = {}) \/ ~({} = s) ==> s IN nonempty``, 512 REWRITE_TAC [IN_NONEMPTY] 513 >> SET_EQ_TAC 514 >> RW_TAC std_ss [NOT_IN_EMPTY] 515 >> PROVE_TAC []); 516 517val NONEMPTY_SUBTYPE_REWRITE = store_thm 518 ("NONEMPTY_SUBTYPE_REWRITE", 519 ``!s. s IN nonempty ==> ~(s = {}) /\ ~({} = s)``, 520 RW_TAC std_ss [SPECIFICATION, IN_NONEMPTY] 521 >> PROVE_TAC []); 522 523val CARD_SUBTYPE = store_thm 524 ("CARD_SUBTYPE", 525 ``CARD IN ((FINITE INTER nonempty) -> gtnum 0)``, 526 R_TAC [IN_FUNSET, IN_NONEMPTY, IN_GTNUM, IN_INTER, IN_FINITE] 527 >> S_TAC 528 >> Suff `~(CARD x = 0)` >- DECIDE_TAC 529 >> PROVE_TAC [CARD_EQ_0]); 530 531val INTER_DEF_ALT = store_thm 532 ("INTER_DEF_ALT", 533 ``!s t. s INTER t = (\x. s x /\ t x)``, 534 SET_EQ_TAC 535 >> R_TAC [IN_INTER] 536 >> R_TAC [SPECIFICATION]); 537 538val FINITE_INTER_DISJ = store_thm 539 ("FINITE_INTER_DISJ", 540 ``!s t. FINITE s \/ FINITE t ==> FINITE (s INTER t)``, 541 PROVE_TAC [FINITE_INTER, INTER_FINITE]); 542 543val FINITE_SUBSET_CARD_EQ = store_thm 544 ("FINITE_SUBSET_CARD_EQ", 545 ``!s t. FINITE t /\ s SUBSET t /\ (CARD s = CARD t) ==> (s = t)``, 546 S_TAC 547 >> Suff `s SUBSET t /\ t SUBSET s` 548 >- (KILL_TAC 549 >> SET_EQ_TAC 550 >> R_TAC [SUBSET_DEF] 551 >> PROVE_TAC []) 552 >> R_TAC [] 553 >> Know `FINITE s` >- PROVE_TAC [SUBSET_FINITE] 554 >> S_TAC 555 >> Know `FINITE t /\ s SUBSET t /\ (CARD s = CARD t)` >- PROVE_TAC [] 556 >> Q.SPEC_TAC (`t`, `t`) 557 >> POP_ASSUM MP_TAC 558 >> Q.SPEC_TAC (`s`, `s`) 559 >> KILL_TAC 560 >> HO_MATCH_MP_TAC FINITE_INDUCT 561 >> CONJ_TAC >- (R_TAC [CARD_EMPTY, SUBSET_EMPTY] >> PROVE_TAC [CARD_EQ_0]) 562 >> S_TAC 563 >> Know `?t'. ~(e IN t') /\ (t = e INSERT t')` 564 >- (Q.EXISTS_TAC `t DELETE e` 565 >> R_TAC [IN_DELETE] 566 >> MATCH_MP_TAC (GSYM INSERT_DELETE) 567 >> AR_TAC [INSERT_SUBSET]) 568 >> S_TAC 569 >> POP_ASSUM (fn th => AR_TAC [th, FINITE_INSERT, CARD_INSERT]) 570 >> R_TAC [INSERT_SUBSET, SUBSET_INSERT, IN_INSERT] 571 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 572 >> Q.PAT_X_ASSUM `x SUBSET y` MP_TAC 573 >> R_TAC [INSERT_SUBSET, SUBSET_INSERT, IN_INSERT]); 574 575val SUBSET_INTER1 = store_thm 576 ("SUBSET_INTER1", 577 ``!s t. s SUBSET t ==> (s INTER t = s)``, 578 SET_EQ_TAC 579 >> Simplify [SUBSET_DEF, IN_INTER]); 580 581val SUBSET_INTER2 = store_thm 582 ("SUBSET_INTER2", 583 ``!s t. s SUBSET t ==> (t INTER s = s)``, 584 SET_EQ_TAC 585 >> Simplify [SUBSET_DEF, IN_INTER]); 586 587val FINITE_LESS = store_thm 588 ("FINITE_LESS", 589 ``!n. FINITE (\x : num. x < n)``, 590 Induct 591 >- (Suff `(\x : num. x < 0) = {}` 592 >- Simplify [FINITE_EMPTY] 593 >> SET_EQ_TAC 594 >> Simplify [] 595 >> Simplify [SPECIFICATION] 596 >> DECIDE_TAC) 597 >> Suff `(\x. x < SUC n) = n INSERT (\x. x < n)` 598 >- Simplify [FINITE_INSERT] 599 >> SET_EQ_TAC 600 >> Simplify [IN_INSERT] 601 >> Simplify [SPECIFICATION] 602 >> DECIDE_TAC); 603 604val FINITE_LESS1 = store_thm 605 ("FINITE_LESS1", 606 ``!n s. FINITE (\x : num. x < n /\ s x)``, 607 Strip 608 >> Simplify [GSYM INTER_DEF_ALT] 609 >> MATCH_MP_TAC FINITE_INTER_DISJ 610 >> Simplify [FINITE_LESS]); 611 612val FINITE_LESS2 = store_thm 613 ("FINITE_LESS2", 614 ``!n s. FINITE (\x : num. s x /\ x < n)``, 615 Strip 616 >> Simplify [GSYM INTER_DEF_ALT] 617 >> MATCH_MP_TAC FINITE_INTER_DISJ 618 >> Simplify [FINITE_LESS]); 619 620val CARD_LESS = store_thm 621 ("CARD_LESS", 622 ``!n. CARD (\x. x < n) = n``, 623 Induct 624 >- (Suff `(\x : num. x < 0) = {}` 625 >- Simplify [CARD_EMPTY] 626 >> SET_EQ_TAC 627 >> Simplify [] 628 >> Simplify [SPECIFICATION] 629 >> DECIDE_TAC) 630 >> ASSUME_TAC (Q.SPEC `n` FINITE_LESS) 631 >> Know `(\x. x < SUC n) = n INSERT (\x. x < n)` 632 >- (SET_EQ_TAC 633 >> Simplify [IN_INSERT] 634 >> Simplify [SPECIFICATION] 635 >> DECIDE_TAC) 636 >> Simplify [CARD_INSERT] 637 >> DISCH_THEN K_TAC 638 >> Suff `~(n IN (\x. x < n))` >- Simplify [] 639 >> Simplify [SPECIFICATION] 640 >> DECIDE_TAC); 641 642val INJ_IMAGE_BIJ = store_thm 643 ("INJ_IMAGE_BIJ", 644 ``!s f. (?t. INJ f s t) ==> BIJ f s (IMAGE f s)``, 645 RW_TAC std_ss [INJ_DEF, BIJ_DEF, SURJ_DEF, IN_IMAGE] 646 >> PROVE_TAC []); 647 648val BIJ_SYM_IMP = store_thm 649 ("BIJ_SYM_IMP", 650 ``!s t. (?f. BIJ f s t) ==> (?g. BIJ g t s)``, 651 RW_TAC std_ss [BIJ_DEF, SURJ_DEF, INJ_DEF] 652 >> Suff `?(g : 'b -> 'a). !x. x IN t ==> g x IN s /\ (f (g x) = x)` 653 >- (Strip 654 >> Q.EXISTS_TAC `g` 655 >> RW_TAC std_ss [] 656 >> PROVE_TAC []) 657 >> POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [boolTheory.EXISTS_DEF]) 658 >> RW_TAC std_ss [] 659 >> Q.EXISTS_TAC `\x. @y. y IN s /\ (f y = x)` 660 >> RW_TAC std_ss []); 661 662val BIJ_SYM = store_thm 663 ("BIJ_SYM", 664 ``!s t. (?f. BIJ f s t) = (?g. BIJ g t s)``, 665 PROVE_TAC [BIJ_SYM_IMP]); 666 667val BIJ_TRANS = store_thm 668 ("BIJ_TRANS", 669 ``!s t u. 670 (?f. BIJ f s t) /\ (?g. BIJ g t u) ==> (?h : 'a -> 'b. BIJ h s u)``, 671 RW_TAC std_ss [] 672 >> Q.EXISTS_TAC `g o f` 673 >> PROVE_TAC [BIJ_COMPOSE]); 674 675val SURJ_IMP_INJ = store_thm 676 ("SURJ_IMP_INJ", 677 ``!s t. (?f. SURJ f s t) ==> (?g. INJ g t s)``, 678 RW_TAC std_ss [SURJ_DEF, INJ_DEF] 679 >> Suff `?g. !x. x IN t ==> g x IN s /\ (f (g x) = x)` 680 >- PROVE_TAC [] 681 >> Q.EXISTS_TAC `\y. @x. x IN s /\ (f x = y)` 682 >> POP_ASSUM MP_TAC 683 >> RW_TAC std_ss [boolTheory.EXISTS_DEF]); 684 685val ENUMERATE = store_thm 686 ("ENUMERATE", 687 ``!s. (?f : num -> 'a. BIJ f UNIV s) = BIJ (enumerate s) UNIV s``, 688 RW_TAC std_ss [boolTheory.EXISTS_DEF, enumerate_def]); 689 690val FINITE_REST = store_thm 691 ("FINITE_REST", 692 ``!s. FINITE (REST s) = FINITE s``, 693 RW_TAC std_ss [REST_DEF, FINITE_DELETE]); 694 695val EXPLICIT_ENUMERATE_MONO = store_thm 696 ("EXPLICIT_ENUMERATE_MONO", 697 ``!n s. FUNPOW REST n s SUBSET s``, 698 Induct >- RW_TAC std_ss [FUNPOW, SUBSET_DEF] 699 >> RW_TAC std_ss [FUNPOW_SUC] 700 >> PROVE_TAC [SUBSET_TRANS, REST_SUBSET]); 701 702val EXPLICIT_ENUMERATE_NOT_EMPTY = store_thm 703 ("EXPLICIT_ENUMERATE_NOT_EMPTY", 704 ``!n s. INFINITE s ==> ~(FUNPOW REST n s = {})``, 705 REWRITE_TAC [] 706 >> Induct >- (RW_TAC std_ss [FUNPOW] >> PROVE_TAC [FINITE_EMPTY]) 707 >> RW_TAC std_ss [FUNPOW] 708 >> Q.PAT_X_ASSUM `!s. P s` (MP_TAC o Q.SPEC `REST s`) 709 >> PROVE_TAC [FINITE_REST]); 710 711val INFINITE_EXPLICIT_ENUMERATE = store_thm 712 ("INFINITE_EXPLICIT_ENUMERATE", 713 ``!s. INFINITE s ==> INJ (\n : num. CHOICE (FUNPOW REST n s)) UNIV s``, 714 RW_TAC std_ss [INJ_DEF, IN_UNIV] 715 >- (Suff `CHOICE (FUNPOW REST n s) IN FUNPOW REST n s` 716 >- PROVE_TAC [SUBSET_DEF, EXPLICIT_ENUMERATE_MONO] 717 >> RW_TAC std_ss [GSYM CHOICE_DEF, EXPLICIT_ENUMERATE_NOT_EMPTY]) 718 >> rpt (POP_ASSUM MP_TAC) 719 >> Q.SPEC_TAC (`s`, `s`) 720 >> Q.SPEC_TAC (`n'`, `y`) 721 >> Q.SPEC_TAC (`n`, `x`) 722 >> (Induct >> Cases) >| 723 [PROVE_TAC [], 724 rpt STRIP_TAC 725 >> Suff `~(CHOICE (FUNPOW REST 0 s) IN FUNPOW REST (SUC n) s)` 726 >- (RW_TAC std_ss [] 727 >> MATCH_MP_TAC CHOICE_DEF 728 >> PROVE_TAC [EXPLICIT_ENUMERATE_NOT_EMPTY]) 729 >> POP_ASSUM K_TAC 730 >> RW_TAC std_ss [FUNPOW] 731 >> Suff `~(CHOICE s IN REST s)` 732 >- PROVE_TAC [SUBSET_DEF, EXPLICIT_ENUMERATE_MONO] 733 >> PROVE_TAC [CHOICE_NOT_IN_REST], 734 rpt STRIP_TAC 735 >> POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) 736 >> Suff `~(CHOICE (FUNPOW REST 0 s) IN FUNPOW REST (SUC x) s)` 737 >- (RW_TAC std_ss [] 738 >> MATCH_MP_TAC CHOICE_DEF 739 >> PROVE_TAC [EXPLICIT_ENUMERATE_NOT_EMPTY]) 740 >> POP_ASSUM K_TAC 741 >> RW_TAC std_ss [FUNPOW] 742 >> Suff `~(CHOICE s IN REST s)` 743 >- PROVE_TAC [SUBSET_DEF, EXPLICIT_ENUMERATE_MONO] 744 >> PROVE_TAC [CHOICE_NOT_IN_REST], 745 RW_TAC std_ss [FUNPOW] 746 >> Q.PAT_X_ASSUM `!y. P y` (MP_TAC o Q.SPECL [`n`, `REST s`]) 747 >> PROVE_TAC [FINITE_REST]]); 748 749val DIFF_ALT = store_thm 750 ("DIFF_ALT", 751 ``!s t. s DIFF t = s INTER (COMPL t)``, 752 RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER, IN_COMPL]); 753 754val DIFF_SUBSET = store_thm 755 ("DIFF_SUBSET", 756 ``!a b. a DIFF b SUBSET a``, 757 RW_TAC std_ss [SUBSET_DEF, EXTENSION, IN_DIFF]); 758 759val NUM_2D_BIJ = store_thm 760 ("NUM_2D_BIJ", 761 ``?f. 762 BIJ f ((UNIV : num -> bool) CROSS (UNIV : num -> bool)) 763 (UNIV : num -> bool)``, 764 MATCH_MP_TAC BIJ_INJ_SURJ 765 >> REVERSE CONJ_TAC 766 >- (Q.EXISTS_TAC `FST` 767 >> RW_TAC std_ss [SURJ_DEF, IN_UNIV, IN_CROSS] 768 >> Q.EXISTS_TAC `(x, 0)` 769 >> RW_TAC std_ss [FST]) 770 >> Q.EXISTS_TAC `UNCURRY ind_type$NUMPAIR` 771 >> RW_TAC std_ss [INJ_DEF, IN_UNIV, IN_CROSS] 772 >> Cases_on `x` 773 >> Cases_on `y` 774 >> POP_ASSUM MP_TAC 775 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ]); 776 777val NUM_2D_BIJ_INV = store_thm 778 ("NUM_2D_BIJ_INV", 779 ``?f. 780 BIJ f (UNIV : num -> bool) 781 ((UNIV : num -> bool) CROSS (UNIV : num -> bool))``, 782 PROVE_TAC [NUM_2D_BIJ, BIJ_SYM]); 783 784val BIJ_FINITE_SUBSET = store_thm 785 ("BIJ_FINITE_SUBSET", 786 ``!(f : num -> 'a) s t. 787 BIJ f UNIV s /\ FINITE t /\ t SUBSET s ==> 788 ?N. !n. N <= n ==> ~(f n IN t)``, 789 RW_TAC std_ss [] 790 >> POP_ASSUM MP_TAC 791 >> POP_ASSUM MP_TAC 792 >> Q.SPEC_TAC (`t`, `t`) 793 >> HO_MATCH_MP_TAC FINITE_INDUCT 794 >> RW_TAC std_ss [EMPTY_SUBSET, NOT_IN_EMPTY, INSERT_SUBSET, IN_INSERT] 795 >> Know `?!k. f k = e` 796 >- (Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 797 >> RW_TAC std_ss [BIJ_ALT_RES, RES_EXISTS_UNIQUE_UNIV, RES_FORALL] 798 >> PROVE_TAC []) 799 >> CONV_TAC (DEPTH_CONV EXISTS_UNIQUE_CONV) 800 >> RW_TAC std_ss [] 801 >> RES_TAC 802 >> Q.EXISTS_TAC `MAX N (SUC k)` 803 >> RW_TAC std_ss [MAX_LE_X] 804 >> STRIP_TAC 805 >> Know `n = k` >- PROVE_TAC [] 806 >> DECIDE_TAC); 807 808val NUM_2D_BIJ_SMALL_SQUARE = store_thm 809 ("NUM_2D_BIJ_SMALL_SQUARE", 810 ``!(f : num -> num # num) k. 811 BIJ f UNIV (UNIV CROSS UNIV) ==> 812 ?N. count k CROSS count k SUBSET IMAGE f (count N)``, 813 Strip 814 >> (MP_TAC o 815 Q.SPECL [`f`, `UNIV CROSS UNIV`, `count k CROSS count k`] o 816 INST_TYPE [``:'a`` |-> ``:num # num``]) BIJ_FINITE_SUBSET 817 >> RW_TAC std_ss [CROSS_SUBSET, SUBSET_UNIV, FINITE_CROSS, FINITE_COUNT] 818 >> Q.EXISTS_TAC `N` 819 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] 820 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 821 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV, IN_CROSS] 822 >> POP_ASSUM (MP_TAC o Q.SPEC `x`) 823 >> RW_TAC std_ss [] 824 >> Q.EXISTS_TAC `y` 825 >> RW_TAC std_ss [] 826 >> Suff `~(N <= y)` >- DECIDE_TAC 827 >> PROVE_TAC []); 828 829val NUM_2D_BIJ_BIG_SQUARE = store_thm 830 ("NUM_2D_BIJ_BIG_SQUARE", 831 ``!(f : num -> num # num) N. 832 BIJ f UNIV (UNIV CROSS UNIV) ==> 833 ?k. IMAGE f (count N) SUBSET count k CROSS count k``, 834 RW_TAC std_ss [IN_CROSS, IN_COUNT, SUBSET_DEF, IN_IMAGE, IN_COUNT] 835 >> Induct_on `N` >- RW_TAC arith_ss [] 836 >> Strip 837 >> Cases_on `f N` 838 >> REWRITE_TAC [prim_recTheory.LESS_THM] 839 >> Q.EXISTS_TAC `SUC (MAX k (MAX q r))` 840 >> Know `!a b. a < SUC b = a <= b` 841 >- (KILL_TAC 842 >> DECIDE_TAC) 843 >> RW_TAC std_ss [] 844 >> RW_TAC std_ss [] 845 >> PROVE_TAC [X_LE_MAX, LESS_EQ_REFL, LESS_IMP_LESS_OR_EQ]); 846 847val BIGUNION_EQ_EMPTY = store_thm 848 ("BIGUNION_EQ_EMPTY", 849 ``!a. (BIGUNION a = {}) = (!s. s IN a ==> (s = {}))``, 850 RW_TAC std_ss [EXTENSION, IN_BIGUNION, NOT_IN_EMPTY] 851 >> PROVE_TAC []); 852 853val IN_BIGUNION_IMAGE = store_thm 854 ("IN_BIGUNION_IMAGE", 855 ``!f s y. y IN BIGUNION (IMAGE f s) = ?x. x IN s /\ y IN f x``, 856 RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE] 857 >> PROVE_TAC []); 858 859val FINITE_SUBSET_COUNT = store_thm 860 ("FINITE_SUBSET_COUNT", 861 ``!s. FINITE s = ?n. s SUBSET count n``, 862 STRIP_TAC 863 >> REVERSE EQ_TAC >- PROVE_TAC [FINITE_COUNT, SUBSET_FINITE] 864 >> REWRITE_TAC [FINITE_DEF] 865 >> DISCH_THEN (MP_TAC o Q.SPEC `\s. ?N. !n. n IN s ==> n <= N`) 866 >> RW_TAC std_ss [SUBSET_DEF, IN_COUNT] 867 >> Suff `?N. !n. n IN s ==> n <= N` 868 >- (RW_TAC std_ss [] 869 >> Q.EXISTS_TAC `SUC N` 870 >> Know `!x y. x < SUC y = x <= y` >- DECIDE_TAC 871 >> RW_TAC std_ss []) 872 >> POP_ASSUM MATCH_MP_TAC 873 >> RW_TAC std_ss [IN_INSERT, NOT_IN_EMPTY] 874 >> Q.EXISTS_TAC `MAX N e` 875 >> RW_TAC std_ss [] 876 >> RW_TAC std_ss [X_LE_MAX, LESS_EQ_REFL]); 877 878val INFINITE_DIFF_FINITE_EQ = store_thm 879 ("INFINITE_DIFF_FINITE_EQ", 880 ``!s t. FINITE t ==> (INFINITE (s DIFF t) = INFINITE s)``, 881 RW_TAC std_ss [] 882 >> REVERSE EQ_TAC >- PROVE_TAC [SUBSET_FINITE, DIFF_SUBSET] 883 >> Suff `s SUBSET (t UNION (s DIFF t))` 884 >- PROVE_TAC [FINITE_UNION, SUBSET_FINITE] 885 >> RW_TAC std_ss [SUBSET_DEF, IN_UNION, IN_DIFF]); 886 887val INFINITE_DELETE = store_thm 888 ("INFINITE_DELETE", 889 ``!x s. INFINITE (s DELETE x) = INFINITE s``, 890 RW_TAC std_ss [DELETE_DEF] 891 >> PROVE_TAC [INFINITE_DIFF_FINITE_EQ, FINITE_SING, SING]); 892 893val FINITE_TL = store_thm 894 ("FINITE_TL", 895 ``!s : bool list -> bool. FINITE (IMAGE TL s) = FINITE s``, 896 RW_TAC std_ss [] 897 >> REVERSE EQ_TAC >- PROVE_TAC [IMAGE_FINITE] 898 >> RW_TAC std_ss [] 899 >> Know `FINITE (IMAGE (\l. {T::l; F::l; []}) (IMAGE TL s))` 900 >- PROVE_TAC [IMAGE_FINITE] 901 >> STRIP_TAC 902 >> Know `FINITE (BIGUNION (IMAGE (\l. {T::l; F::l; []}) (IMAGE TL s)))` 903 >- (MATCH_MP_TAC FINITE_BIGUNION 904 >> RW_TAC std_ss [IN_IMAGE] 905 >> RW_TAC std_ss [FINITE_INSERT, FINITE_EMPTY]) 906 >> Suff `s SUBSET BIGUNION (IMAGE (\l. {T::l; F::l; []}) (IMAGE TL s))` 907 >- PROVE_TAC [SUBSET_FINITE] 908 >> KILL_TAC 909 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION_IMAGE, IN_IMAGE, IN_INSERT, 910 NOT_IN_EMPTY] 911 >> Cases_on `x` 912 >- (RW_TAC std_ss [] 913 >> PROVE_TAC []) 914 >> Cases_on `h` 915 >> RW_TAC std_ss [] 916 >> PROVE_TAC [TL]); 917 918val IMAGE_o_INV = store_thm 919 ("IMAGE_o_INV", 920 ``!s f. (IMAGE f (s o f)) SUBSET s /\ s SUBSET ((IMAGE f s) o f)``, 921 RW_TAC std_ss [IN_o, IN_IMAGE, SUBSET_DEF] 922 >> PROVE_TAC []); 923 924val BIGUNION_PAIR = store_thm 925 ("BIGUNION_PAIR", 926 ``!s t. BIGUNION {s; t} = s UNION t``, 927 RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_UNION, IN_INSERT, NOT_IN_EMPTY] 928 >> PROVE_TAC []); 929 930val BIGUNION_IMAGE_UNIV = store_thm 931 ("BIGUNION_IMAGE_UNIV", 932 ``!f N. 933 (!n. N <= n ==> (f n = {})) ==> 934 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE f (count N)))``, 935 RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_COUNT, 936 NOT_IN_EMPTY] 937 >> REVERSE EQ_TAC >- PROVE_TAC [] 938 >> RW_TAC std_ss [] 939 >> PROVE_TAC [NOT_LESS]); 940 941val PREIMAGE_DISJOINT = store_thm 942 ("PREIMAGE_DISJOINT", 943 ``!f s t. DISJOINT s t ==> DISJOINT (PREIMAGE f s) (PREIMAGE f t)``, 944 RW_TAC std_ss [DISJOINT_DEF, GSYM PREIMAGE_INTER, PREIMAGE_EMPTY]); 945 946val PREIMAGE_SUBSET = store_thm 947 ("PREIMAGE_SUBSET", 948 ``!f s t. s SUBSET t ==> PREIMAGE f s SUBSET PREIMAGE f t``, 949 RW_TAC std_ss [SUBSET_DEF, PREIMAGE_def, GSPECIFICATION]); 950 951val SUBSET_ADD = store_thm 952 ("SUBSET_ADD", 953 ``!f n d. 954 (!n. f n SUBSET f (SUC n)) ==> 955 f n SUBSET f (n + d)``, 956 RW_TAC std_ss [] 957 >> Induct_on `d` >- RW_TAC arith_ss [SUBSET_REFL] 958 >> RW_TAC std_ss [ADD_CLAUSES] 959 >> MATCH_MP_TAC SUBSET_TRANS 960 >> Q.EXISTS_TAC `f (n + d)` 961 >> RW_TAC std_ss []); 962 963val DISJOINT_DIFFS = store_thm 964 ("DISJOINT_DIFFS", 965 ``!f m n. 966 (!n. f n SUBSET f (SUC n)) /\ 967 (!n. g n = f (SUC n) DIFF f n) /\ ~(m = n) ==> 968 DISJOINT (g m) (g n)``, 969 RW_TAC std_ss [] 970 >> Know `SUC m <= n \/ SUC n <= m` >- DECIDE_TAC 971 >> REWRITE_TAC [LESS_EQ_EXISTS] 972 >> STRIP_TAC >| 973 [Know `f (SUC m) SUBSET f n` >- PROVE_TAC [SUBSET_ADD] 974 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, 975 NOT_IN_EMPTY, IN_DIFF, SUBSET_DEF] 976 >> PROVE_TAC [], 977 Know `f (SUC n) SUBSET f m` >- PROVE_TAC [SUBSET_ADD] 978 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, 979 NOT_IN_EMPTY, IN_DIFF, SUBSET_DEF] 980 >> PROVE_TAC []]); 981 982val PREIMAGE_COMP = store_thm 983 ("PREIMAGE_COMP", 984 ``!f g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g o f) s``, 985 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, o_THM]); 986 987val PREIMAGE_K = store_thm 988 ("PREIMAGE_K", 989 ``!x s. PREIMAGE (K x) s = if x IN s then UNIV else {}``, 990 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, K_THM, IN_UNIV, NOT_IN_EMPTY]); 991 992val INSERT_CASES = store_thm 993 ("INSERT_CASES", 994 ``!P. P {} /\ (!x s. ~(x IN s) ==> P (x INSERT s)) ==> (!s. P s)``, 995 RW_TAC std_ss [] 996 >> MP_TAC (Q.SPEC `s` SET_CASES) 997 >> RW_TAC std_ss [] 998 >> PROVE_TAC []); 999 1000val BOOL_SET_CASES = store_thm 1001 ("BOOL_SET_CASES", 1002 ``!P. P {} /\ P {T} /\ P {F} /\ P UNIV ==> (!x. P x)``, 1003 NTAC 2 STRIP_TAC 1004 >> HO_MATCH_MP_TAC INSERT_CASES 1005 >> ASM_REWRITE_TAC [] 1006 >> STRIP_TAC 1007 >> HO_MATCH_MP_TAC INSERT_CASES 1008 >> (Cases_on `x` 1009 >> ASM_REWRITE_TAC [] 1010 >> Cases 1011 >> RW_TAC std_ss [IN_INSERT]) >| 1012 [Suff `T INSERT F INSERT x'' = UNIV` 1013 >- PROVE_TAC [] 1014 >> RW_TAC std_ss [EXTENSION, IN_UNIV, IN_INSERT], 1015 Suff `F INSERT T INSERT x'' = UNIV` 1016 >- PROVE_TAC [] 1017 >> RW_TAC std_ss [EXTENSION, IN_UNIV, IN_INSERT]]); 1018 1019val COMPL_INTER = store_thm 1020 ("COMPL_INTER", 1021 ``!s t. COMPL (s INTER t) = COMPL s UNION COMPL t``, 1022 RW_TAC std_ss [EXTENSION, IN_COMPL, IN_INTER, IN_UNION]); 1023 1024val COUNTABLE_BIGUNION = store_thm 1025 ("COUNTABLE_BIGUNION", 1026 ``!c. 1027 countable c /\ (!s. s IN c ==> countable s) ==> countable (BIGUNION c)``, 1028 PROVE_TAC [bigunion_countable]); 1029 1030val COUNTABLE_BOOL_LIST = store_thm 1031 ("COUNTABLE_BOOL_LIST", 1032 ``!s : bool list -> bool. countable s``, 1033 STRIP_TAC 1034 >> MATCH_MP_TAC COUNTABLE_SUBSET 1035 >> Q.EXISTS_TAC `UNIV` 1036 >> RW_TAC std_ss [SUBSET_UNIV] 1037 >> Know 1038 `(UNIV : bool list -> bool) = 1039 BIGUNION (IMAGE (\x. PREIMAGE LENGTH {x}) UNIV)` 1040 >- RW_TAC std_ss [EXTENSION, IN_UNIV, IN_BIGUNION_IMAGE, IN_PREIMAGE, 1041 IN_SING] 1042 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1043 >> MATCH_MP_TAC COUNTABLE_BIGUNION 1044 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, IN_IMAGE, IN_UNIV] 1045 >> Induct_on `x` 1046 >- (RW_TAC std_ss [COUNTABLE_ALT, IN_PREIMAGE, IN_SING, LENGTH_NIL] 1047 >> Q.EXISTS_TAC `K []` 1048 >> RW_TAC std_ss [K_THM]) 1049 >> Know 1050 `PREIMAGE LENGTH {SUC x} = 1051 IMAGE (CONS T) (PREIMAGE LENGTH {x}) UNION 1052 IMAGE (CONS F) (PREIMAGE LENGTH {x})` 1053 >- (RW_TAC std_ss [EXTENSION, IN_PREIMAGE, IN_IMAGE, IN_SING, IN_UNION] 1054 >> Cases_on `x'` >- RW_TAC std_ss [LENGTH] 1055 >> RW_TAC std_ss [LENGTH] 1056 >> PROVE_TAC []) 1057 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1058 >> MATCH_MP_TAC union_countable 1059 >> RW_TAC std_ss [image_countable]); 1060 1061val INTER_BIGUNION = store_thm 1062 ("INTER_BIGUNION", 1063 ``!s a. s INTER BIGUNION a = BIGUNION (IMAGE ($INTER s) a)``, 1064 RW_TAC std_ss [EXTENSION, IN_INTER, IN_BIGUNION_IMAGE] 1065 >> RW_TAC std_ss [IN_BIGUNION] 1066 >> PROVE_TAC []); 1067 1068val FINITE_DISJOINT_ENUM = store_thm 1069 ("FINITE_DISJOINT_ENUM", 1070 ``!c. 1071 FINITE c /\ (!s t. s IN c /\ t IN c /\ ~(s = t) ==> DISJOINT s t) ==> 1072 ?f : num -> 'a -> bool. 1073 f IN (UNIV -> ({} INSERT c)) /\ 1074 (BIGUNION c = BIGUNION (IMAGE f UNIV)) /\ 1075 (!m n. ~(m = n) ==> DISJOINT (f m) (f n))``, 1076 RW_TAC std_ss [] 1077 >> REPEAT (POP_ASSUM MP_TAC) 1078 >> Q.SPEC_TAC (`c`, `c`) 1079 >> HO_MATCH_MP_TAC FINITE_INDUCT 1080 >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INSERT] 1081 >- (Q.EXISTS_TAC `K {}` 1082 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, EXTENSION, IN_SING, K_THM, 1083 DISJOINT_EMPTY, IN_BIGUNION, IN_IMAGE, NOT_IN_EMPTY] 1084 >> PROVE_TAC []) 1085 >> Q.PAT_X_ASSUM `X ==> Y` MP_TAC 1086 >> Know `!s t. s IN c /\ t IN c /\ ~(s = t) ==> DISJOINT s t` 1087 >- PROVE_TAC [] 1088 >> RW_TAC std_ss [] 1089 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1090 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INSERT] 1091 >> Q.EXISTS_TAC `\x. num_CASE x e f` 1092 >> CONJ_TAC 1093 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INSERT] 1094 >> Cases_on `x` 1095 >> RW_TAC std_ss [num_case_def] 1096 >> PROVE_TAC []) 1097 >> CONJ_TAC 1098 >- (Q.PAT_X_ASSUM `X = Y` MP_TAC 1099 >> RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE] 1100 >> POP_ASSUM MP_TAC 1101 >> RW_TAC std_ss [IN_INSERT, IN_IMAGE, IN_UNIV, IN_BIGUNION] 1102 >> EQ_TAC >| 1103 [RW_TAC std_ss [] >| 1104 [Q.EXISTS_TAC `0` 1105 >> RW_TAC std_ss [num_case_def], 1106 Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1107 >> Know `?s. x IN s /\ s IN c` >- PROVE_TAC [] 1108 >> RW_TAC std_ss [] 1109 >> Q.EXISTS_TAC `SUC x'` 1110 >> RW_TAC std_ss [num_case_def]], 1111 RW_TAC std_ss [] 1112 >> (Cases_on `x'` 1113 >> POP_ASSUM MP_TAC 1114 >> RW_TAC std_ss [num_case_def]) 1115 >- PROVE_TAC [] 1116 >> PROVE_TAC [NOT_IN_EMPTY]]) 1117 >> (Cases >> Cases) 1118 >> RW_TAC arith_ss [num_case_def] 1119 >> PROVE_TAC [DISJOINT_EMPTY]); 1120 1121val COUNTABLE_DISJOINT_ENUM = store_thm 1122 ("COUNTABLE_DISJOINT_ENUM", 1123 ``!c. 1124 countable c /\ (!s t. s IN c /\ t IN c /\ ~(s = t) ==> DISJOINT s t) ==> 1125 ?f : num -> 'a -> bool. 1126 f IN (UNIV -> ({} INSERT c)) /\ 1127 (BIGUNION c = BIGUNION (IMAGE f UNIV)) /\ 1128 (!m n. ~(m = n) ==> DISJOINT (f m) (f n))``, 1129 RW_TAC std_ss [COUNTABLE_ALT_BIJ] 1130 >- (MP_TAC (Q.SPEC `c` FINITE_DISJOINT_ENUM) 1131 >> RW_TAC std_ss []) 1132 >> Q.EXISTS_TAC `enumerate c` 1133 >> REPEAT (POP_ASSUM MP_TAC) 1134 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV, IN_FUNSET, IN_INSERT, 1135 EXTENSION, IN_BIGUNION_IMAGE, IN_BIGUNION, INJ_DEF] 1136 >> PROVE_TAC []); 1137 1138val COMPL_BIGINTER = store_thm 1139 ("COMPL_BIGINTER", 1140 ``!s. COMPL (BIGINTER s) = BIGUNION (IMAGE COMPL s)``, 1141 RW_TAC std_ss [EXTENSION, IN_COMPL, IN_BIGINTER, IN_BIGUNION_IMAGE]); 1142 1143val IN_BIGINTER_IMAGE = store_thm 1144 ("IN_BIGINTER_IMAGE", 1145 ``!x f s. x IN BIGINTER (IMAGE f s) = (!y. y IN s ==> x IN f y)``, 1146 RW_TAC std_ss [IN_BIGINTER, IN_IMAGE] 1147 >> PROVE_TAC []); 1148 1149val IMAGE_K = store_thm 1150 ("IMAGE_K", 1151 ``!x s. IMAGE (K x) s = if s = {} then {} else {x}``, 1152 RW_TAC std_ss [EXTENSION, IN_IMAGE, K_THM, NOT_IN_EMPTY, IN_SING] 1153 >> PROVE_TAC []); 1154 1155val FINITE_BOOL = store_thm 1156 ("FINITE_BOOL", 1157 ``!s : bool -> bool. FINITE s``, 1158 Suff `FINITE (UNIV : bool -> bool)` >- PROVE_TAC [SUBSET_FINITE, SUBSET_UNIV] 1159 >> Suff `UNIV = {T; F}` 1160 >- RW_TAC std_ss [FINITE_INSERT, FINITE_EMPTY] 1161 >> RW_TAC std_ss [EXTENSION, IN_UNIV, IN_INSERT, NOT_IN_EMPTY]); 1162 1163val COUNTABLE_BOOL = store_thm 1164 ("COUNTABLE_BOOL", 1165 ``!s : bool -> bool. countable s``, 1166 PROVE_TAC [finite_countable, FINITE_BOOL]); 1167 1168val COUNTABLE_SING = store_thm 1169 ("COUNTABLE_SING", 1170 ``!x. countable {x}``, 1171 PROVE_TAC [finite_countable, FINITE_SING]); 1172 1173val ALWAYS_IN_RANGE = store_thm 1174 ("ALWAYS_IN_RANGE", 1175 ``!f x. f x IN range f``, 1176 RW_TAC std_ss [range_def, IN_IMAGE, IN_UNIV] 1177 >> PROVE_TAC []); 1178 1179val RANGE_NONEMPTY = store_thm 1180 ("RANGE_NONEMPTY", 1181 ``!f. ~(range f = {})``, 1182 RW_TAC std_ss [range_def, EXTENSION, NOT_IN_EMPTY, IN_IMAGE, IN_UNIV]); 1183 1184val PREIMAGE_INTER_RANGE = store_thm 1185 ("PREIMAGE_INTER_RANGE", 1186 ``!f s. PREIMAGE f (s INTER range f) = PREIMAGE f s``, 1187 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, IN_INTER, ALWAYS_IN_RANGE]); 1188 1189val PREIMAGE_INTER_SUPER_RANGE = store_thm 1190 ("PREIMAGE_INTER_SUPER_RANGE", 1191 ``!f s t. range f SUBSET t ==> (PREIMAGE f (s INTER t) = PREIMAGE f s)``, 1192 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, IN_INTER, SUBSET_DEF] 1193 >> PROVE_TAC [ALWAYS_IN_RANGE]); 1194 1195val RANGE_BIND = store_thm 1196 ("RANGE_BIND", 1197 ``!f g. 1198 range (FST o BIND f g) SUBSET 1199 BIGUNION (IMAGE (range o (\x. FST o g x)) (range (FST o f)))``, 1200 RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION_IMAGE, range_def, IN_IMAGE, IN_UNIV, 1201 o_THM, BIND_DEF, UNCURRY] 1202 >> PROVE_TAC [FST, SND]); 1203 1204val GEMPTY = store_thm 1205 ("GEMPTY", 1206 ``{s | F} = {}``, 1207 RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY]); 1208 1209val GUNIV = store_thm 1210 ("GUNIV", 1211 ``{s | T} = UNIV``, 1212 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_UNIV]); 1213 1214val GSPEC_DEST = store_thm 1215 ("GSPEC_DEST", 1216 ``!p. {s | p s} = p``, 1217 RW_TAC std_ss [EXTENSION, GSPECIFICATION] 1218 >> RW_TAC std_ss [SPECIFICATION]); 1219 1220val GUNION = store_thm 1221 ("GUNION", 1222 ``!p q. {s | p s \/ q s} = {s | p s} UNION {s | q s}``, 1223 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_UNION]); 1224 1225val GDEST = store_thm 1226 ("GDEST", 1227 ``!p. {s | s IN p} = p``, 1228 RW_TAC std_ss [EXTENSION, GSPECIFICATION]); 1229 1230val GBIGUNION_IMAGE = store_thm 1231 ("GBIGUNION_IMAGE", 1232 ``!s p n. {s | ?n. p s n} = BIGUNION (IMAGE (\n. {s | p s n}) UNIV)``, 1233 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_UNIV]); 1234 1235val GINTER = store_thm 1236 ("GINTER", 1237 ``!p q. {s | p s /\ q s} = {s | p s} INTER {s | q s}``, 1238 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER]); 1239 1240val BIGUNION_IMAGE_INSIDE = store_thm 1241 ("BIGUNION_IMAGE_INSIDE", 1242 ``!f g s. 1243 BIGUNION (IMAGE f (BIGUNION (IMAGE g s))) = 1244 BIGUNION (IMAGE (BIGUNION o IMAGE f o g) s)``, 1245 SET_EQ_TAC 1246 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, o_THM] 1247 >> PROVE_TAC []); 1248 1249val GCOMPL = store_thm 1250 ("GCOMPL", 1251 ``!p. {s | ~p s} = COMPL {s | p s}``, 1252 SET_EQ_TAC 1253 >> RW_TAC std_ss [GSPECIFICATION, IN_COMPL]); 1254 1255val IN_I = store_thm 1256 ("IN_I", 1257 ``!x. x IN I = x``, 1258 RW_TAC std_ss [SPECIFICATION, I_THM]); 1259 1260val COMPL_o = store_thm 1261 ("COMPL_o", 1262 ``!p q. COMPL p o q = COMPL (p o q)``, 1263 SET_EQ_TAC 1264 >> RW_TAC std_ss [IN_COMPL, IN_o]); 1265 1266val FST_o_UNIT = store_thm 1267 ("FST_o_UNIT", 1268 ``!p a. p o FST o UNIT a = if a IN p then UNIV else {}``, 1269 SET_EQ_TAC 1270 >> RW_TAC std_ss [o_THM, UNIT_DEF, IN_o, IN_UNIV, NOT_IN_EMPTY]); 1271 1272val IS_SOME_MMAP = store_thm 1273 ("IS_SOME_MMAP", 1274 ``!f. {x | IS_SOME x} o FST o MMAP SOME f = UNIV``, 1275 SET_EQ_TAC 1276 >> RW_TAC std_ss [IN_UNIV, IN_o, o_THM, MMAP_DEF, BIND_DEF, UNCURRY, 1277 UNIT_DEF, GSPECIFICATION]); 1278 1279val IS_SOME_INTER_MMAP = store_thm 1280 ("IS_SOME_INTER_MMAP", 1281 ``!p f. 1282 ((p o THE) INTER {x | IS_SOME x}) o FST o MMAP SOME f = p o FST o f``, 1283 SET_EQ_TAC 1284 >> RW_TAC std_ss [o_THM, MMAP_DEF, BIND_DEF, UNCURRY, UNIT_DEF, IN_INTER, 1285 IN_o, GSPECIFICATION]); 1286 1287val SET_PAIR_BOOL = store_thm 1288 ("SET_PAIR_BOOL", 1289 ``!s. 1290 s = 1291 (if (T, T) IN s then {(T, T)} else {}) UNION 1292 (if (T, F) IN s then {(T, F)} else {}) UNION 1293 (if (F, T) IN s then {(F, T)} else {}) UNION 1294 (if (F, F) IN s then {(F, F)} else {})``, 1295 STRIP_TAC 1296 >> SET_EQ_TAC 1297 >> Cases 1298 >> Cases_on `q` 1299 >> Cases_on `r` 1300 >> RW_TAC std_ss [IN_UNION, IN_SING, NOT_IN_EMPTY]); 1301 1302val FINITE_PAIR_BOOL = store_thm 1303 ("FINITE_PAIR_BOOL", 1304 ``!s:bool#bool->bool. FINITE s``, 1305 RW_TAC std_ss [] 1306 >> ONCE_REWRITE_TAC [SET_PAIR_BOOL] 1307 >> RW_TAC std_ss [FINITE_UNION, FINITE_INSERT, FINITE_EMPTY]); 1308 1309val _ = export_theory (); 1310