1(* --------------------------------------------------------------------- *) 2(* Boilerplate. *) 3(* --------------------------------------------------------------------- *) 4open HolKernel Parse boolLib; 5infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 6infixr -->; 7 8 9(* --------------------------------------------------------------------- *) 10(* Create the theory. *) 11(* --------------------------------------------------------------------- *) 12val _ = new_theory "more_set"; 13 14 15(* 16app load ["pairTheory", "listTheory", 17 "arithmeticTheory", "pred_setTheory", 18 "Num_induct", "listLib", "pred_setLib"]; 19*) 20 21(* --------------------------------------------------------------------- *) 22(* Autoload definitions and theorems from ancestor theories. *) 23(* --------------------------------------------------------------------- *) 24open prim_recTheory; 25open combinTheory; 26open pairTheory; 27open listTheory; 28open arithmeticTheory; 29open pred_setTheory; 30 31 32(* --------------------------------------------------------------------- *) 33(* Need the induction, list, and pred_set libraries. *) 34(* --------------------------------------------------------------------- *) 35open numLib; 36open listLib; 37open pred_setLib; 38 39 40(* For errors try <exp> handle e => Raise e; 41*) 42 43 44open tactics; 45 46 47 48val IN_NOT_IN = store_thm 49 ("IN_NOT_IN", 50 ���!s (x:'a) y. (x IN s) /\ ~(y IN s) ==> ~(x = y)���, 51 REPEAT STRIP_TAC 52 THEN POP_ASSUM REWRITE_ALL_THM 53 THEN RES_TAC 54 ); 55 56val NOT_IN_SUBSET = 57 store_thm 58 ("NOT_IN_SUBSET", 59 ���!s t (x:'a). ~(x IN s) /\ (t SUBSET s) ==> ~(x IN t)���, 60 REPEAT STRIP_TAC 61 THEN IMP_RES_TAC SUBSET_DEF 62 THEN RES_TAC 63 ); 64 65 66val IN_DISJOINT_IMP = 67 store_thm 68 ("IN_DISJOINT_IMP", 69 ���!s t (x:'a). DISJOINT s t ==> 70 ((x IN s ==> ~(x IN t)) /\ 71 (x IN t ==> ~(x IN s)))���, 72 REWRITE_TAC[DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY] 73 THEN REPEAT STRIP_TAC 74 THENL 75 [ POP_ASSUM (fn th1 => POP_ASSUM (fn th2 => 76 MP_TAC (CONJ th2 th1) )), 77 78 POP_ASSUM (fn th1 => POP_ASSUM (fn th2 => 79 MP_TAC (CONJ th1 th2) )) 80 ] 81 THEN MATCH_MP_TAC F_IMP 82 THEN ASM_REWRITE_TAC[] 83 ); 84 85 86val CONJ_11 = 87 store_thm 88 ("CONJ_11", 89 ���!a b c d. (a = b) /\ (c = d) ==> (a /\ c = b /\ d)���, 90 REPEAT STRIP_TAC 91 THEN ASM_REWRITE_TAC[] 92 ); 93 94 95val MAP_I = 96 store_thm 97 ("MAP_I", 98 ���!lst:('a)list. MAP I lst = lst���, 99 LIST_INDUCT_TAC 100 THEN ASM_REWRITE_TAC[MAP,I_THM] 101 ); 102 103val APPEND_LENGTH_EQ = rich_listTheory.APPEND_LENGTH_EQ; 104 105val APPEND_11 = 106 store_thm 107 ("APPEND_11", 108 ���!l1 l2 l3 l4:('a)list. 109 (LENGTH l3 = LENGTH l1) /\ (LENGTH l4 = LENGTH l2) ==> 110 ((APPEND l1 l2 = APPEND l3 l4) = ((l1 = l3) /\ (l2 = l4)))���, 111 PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] 112 THEN REPEAT STRIP_TAC 113 THEN PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] 114 THEN IMP_RES_TAC APPEND_LENGTH_EQ 115 ); 116 117 118val NULL_APPEND = 119 store_thm 120 ("NULL_APPEND", 121 ���!l1 l2:('a) list. 122 NULL (APPEND l1 l2) = NULL l1 /\ NULL l2���, 123 LIST_INDUCT_TAC 124 THEN REWRITE_TAC[NULL,APPEND] 125 ); 126 127 128val ONE_ONE = 129 store_thm 130 ("ONE_ONE", 131 ���!f:'a->'b. 132 ONE_ONE f = 133 (!x1 x2. (f x1 = f x2) = (x1 = x2))���, 134 REWRITE_TAC[ONE_ONE_THM] 135 THEN GEN_TAC 136 THEN EQ_TAC 137 THENL 138 [ REPEAT STRIP_TAC 139 THEN EQ_TAC 140 THEN DISCH_TAC 141 THENL 142 [ RES_TAC, 143 ASM_REWRITE_TAC[] 144 ], 145 146 DISCH_TAC 147 THEN ASM_REWRITE_TAC[] 148 ] 149 ); 150 151 152val ONTO_INVERSE = 153 store_thm 154 ("ONTO_INVERSE", 155 ���!(ss:'a->'b) y. 156 ONTO ss ==> (ss(@z. ss z = y) = y)���, 157 REWRITE_TAC[ONTO_THM] 158 THEN REPEAT STRIP_TAC 159 THEN CONV_TAC SELECT_CONV 160 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 161 THEN ASM_REWRITE_TAC[] 162 ); 163 164val o_ONTO_11 = 165 store_thm 166 ("o_ONTO_11", 167 ���!(ss:'a->'b) (s1:'b->'c) s2. 168 ONTO ss ==> ((s2 o ss = s1 o ss) = (s2 = s1))���, 169 REPEAT STRIP_TAC 170 THEN EQ_TAC 171 THENL 172 [ DISCH_TAC 173 THEN EXT_TAC ���y:'b��� 174 THEN GEN_TAC 175 THEN POP_ASSUM (fn th => 176 ASSUME_TAC (AP_THM th ���@z. (ss:'a->'b) z = y���)) 177 THEN UNDISCH_LAST_TAC 178 THEN IMP_RES_TAC ONTO_INVERSE 179 THEN ASM_REWRITE_TAC[o_THM], 180 181 DISCH_THEN REWRITE_THM 182 ] 183 ); 184 185 186val o_ONTO_IMP_11 = 187 store_thm 188 ("o_ONTO_IMP_11", 189 ���!(ss:'a->'b) (s1:'b->'c) s2. 190 ONTO ss /\ (s2 o ss = s1 o ss) ==> (s2 = s1)���, 191 REPEAT STRIP_TAC 192 THEN IMP_RES_TAC o_ONTO_11 193 ); 194 195val o_INVERSE = 196 store_thm 197 ("o_INVERSE", 198 ���!(ss:'a->'b). 199 ONE_ONE ss /\ ONTO ss ==> 200 (ss o (\y. @z. ss z = y) = I) /\ 201 ((\y. @z. ss z = y) o ss = I)���, 202 REWRITE_TAC[ONE_ONE] 203 THEN REPEAT STRIP_TAC 204 THENL [ EXT_TAC ���x:'b���, EXT_TAC ���x:'a��� ] 205 THEN GEN_TAC 206 THEN REWRITE_TAC[o_THM,I_THM] 207 THEN BETA_TAC 208 THENL 209 [ IMP_RES_THEN REWRITE_THM ONTO_INVERSE, 210 ASM_REWRITE_TAC[SELECT_REFL] 211 ] 212 ); 213 214val o_EQ_INVERSE = 215 store_thm 216 ("o_EQ_INVERSE", 217 ���!(ss:'a->'b) (s1:'b->'c) s2. 218 ONE_ONE ss /\ ONTO ss ==> 219 ((s1 o ss = s2) = (s1 = s2 o (\y. @z. ss z = y)))���, 220 REPEAT STRIP_TAC 221 THEN IMP_RES_TAC o_ONTO_11 222 THEN EQ_TAC 223 THENL [ DISCH_THEN (REWRITE_THM o SYM), 224 DISCH_THEN REWRITE_THM ] 225 THEN REWRITE_TAC[SYM(SPEC_ALL o_ASSOC)] 226 THEN IMP_RES2_THEN REWRITE_THM o_INVERSE 227 THEN REWRITE_TAC[I_o_ID] 228 ); 229 230val o_ONTO = 231 store_thm 232 ("o_ONTO", 233 ���!(ss1:'b->'c) (ss2:'a->'b). 234 ONTO ss1 /\ ONTO ss2 ==> 235 ONTO (ss1 o ss2)���, 236 REWRITE_TAC[ONTO_THM] 237 THEN REPEAT STRIP_TAC 238 THEN UNDISCH_ALL_TAC 239 THEN DISCH_THEN (STRIP_ASSUME_TAC o SPEC_ALL) 240 THEN DISCH_THEN (STRIP_ASSUME_TAC o SPEC ���x:'b���) 241 THEN EXISTS_TAC ���x':'a��� 242 THEN ASM_REWRITE_TAC[o_THM] 243 ); 244 245val o_ONE_ONE = 246 store_thm 247 ("o_ONE_ONE", 248 ���!(ss1:'b->'c) (ss2:'a->'b). 249 ONE_ONE ss1 /\ ONE_ONE ss2 ==> 250 ONE_ONE (ss1 o ss2)���, 251 REWRITE_TAC[ONE_ONE] 252 THEN REPEAT STRIP_TAC 253 THEN ASM_REWRITE_TAC[o_THM] 254 ); 255 256 257val biject_EQ_INVERSE = 258 store_thm 259 ("biject_EQ_INVERSE", 260 ���!y x (ss:'a->'b). 261 ONE_ONE ss /\ ONTO ss ==> 262 (((@z. ss z = y) = x) = (ss x = y))���, 263 REWRITE_TAC[ONE_ONE] 264 THEN REPEAT STRIP_TAC 265 THEN EQ_TAC 266 THEN DISCH_THEN (REWRITE_THM o SYM) 267 THENL 268 [ IMP_RES_THEN REWRITE_THM ONTO_INVERSE, 269 270 ASM_REWRITE_TAC[SELECT_REFL] 271 ] 272 ); 273 274 275val biject_EQ_INVERSE1 = 276 store_thm 277 ("biject_EQ_INVERSE1", 278 ���!y x (ss:'a->'b). 279 ONE_ONE ss /\ ONTO ss ==> 280 ((x = (@z. ss z = y)) = (ss x = y))���, 281 REWRITE_TAC[ONE_ONE] 282 THEN REPEAT STRIP_TAC 283 THEN EQ_TAC 284 THENL 285 [ DISCH_THEN REWRITE_THM 286 THEN IMP_RES_THEN REWRITE_THM ONTO_INVERSE, 287 288 DISCH_THEN (REWRITE_THM o SYM) 289 THEN ASM_REWRITE_TAC[SELECT_REFL] 290 ] 291 ); 292 293 294val INVERSE_biject = 295 store_thm 296 ("INVERSE_biject", 297 ���!ss:'a->'b. 298 ONE_ONE ss /\ ONTO ss ==> 299 ONE_ONE (\y. @z. ss z = y) /\ ONTO (\y. @z. ss z = y)���, 300 REPEAT STRIP_TAC 301 THENL 302 [ REWRITE_TAC[ONE_ONE] 303 THEN BETA_TAC 304 THEN IMP_RES2_THEN REWRITE_THM biject_EQ_INVERSE1 305 THEN IMP_RES_THEN REWRITE_THM ONTO_INVERSE, 306 307 REWRITE_TAC[ONTO_THM] 308 THEN GEN_TAC 309 THEN BETA_TAC 310 THEN IMP_RES2_THEN REWRITE_THM biject_EQ_INVERSE1 311 THEN EXISTS_TAC ���(ss:'a->'b) y��� 312 THEN ASM_REWRITE_TAC[] 313 ] 314 ); 315 316 317val IN_IDENT_subst = 318 store_thm 319 ("IN_IDENT_subst", 320 ���!s ss (z:'a). 321 (!x. (x IN s) ==> (ss x = x)) /\ ONE_ONE ss ==> 322 ((ss z IN s) = (z IN s))���, 323 REWRITE_TAC[ONE_ONE] 324 THEN REPEAT STRIP_TAC 325 THEN EQ_TAC 326 THEN STRIP_TAC 327 THEN RES_TAC 328 THENL 329 [ UNDISCH_LAST_TAC 330 THEN ASM_REWRITE_TAC[] 331 THEN DISCH_THEN REWRITE_ALL_THM 332 THEN ASM_REWRITE_TAC[], 333 334 ASM_REWRITE_TAC[] 335 ] 336 ); 337 338 339val MEMBER_IMP_POS_CARD = store_thm 340 ("MEMBER_IMP_POS_CARD", 341 ���!s. FINITE s ==> !(x:'a). x IN s ==> (0 < CARD s)���, 342 REPEAT STRIP_TAC 343 THEN MATCH_MP_TAC (DISJ_IMP (SPEC_ALL LESS_0_CASES)) 344 THEN PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] 345 THEN IMP_RES_THEN ONCE_REWRITE_THM CARD_EQ_0 346 THEN PURE_ONCE_REWRITE_TAC[SYM(SPEC_ALL MEMBER_NOT_EMPTY)] 347 THEN EXISTS_TAC ���x:'a��� 348 THEN ASM_REWRITE_TAC[] 349 ); 350 351 352val SUB1_SUC = store_thm 353 ("SUB1_SUC", 354 ���!m. (0 < m) ==> (SUC (m - 1) = m)���, 355 INDUCT_TAC 356 THENL [REWRITE_TAC[NOT_LESS_0], 357 REWRITE_TAC[LESS_0,SUC_SUB1] 358 ] 359 ); 360 361 362val UNION_INTER = 363 store_thm 364 ("UNION_INTER", 365 ���!s1 s2 s3 :'a->bool. 366 (s1 UNION s2) INTER s3 = 367 ((s1 INTER s3) UNION (s2 INTER s3))���, 368 ONCE_REWRITE_TAC[INTER_COMM] 369 THEN REWRITE_TAC[UNION_OVER_INTER] 370 ); 371 372val UNION_THM = 373 store_thm 374 ("UNION_THM", 375 ���!s t (x:'a). 376 (EMPTY UNION t = t) /\ 377 (s UNION EMPTY = s) /\ 378 ((x INSERT s) UNION t = x INSERT (s UNION t)) /\ 379 (s UNION (x INSERT t) = x INSERT (s UNION t))���, 380 REWRITE_TAC[UNION_EMPTY,INSERT_UNION_EQ] 381 THEN ONCE_REWRITE_TAC[UNION_COMM] 382 THEN REWRITE_TAC[INSERT_UNION_EQ] 383 ); 384 385 386val UNION_SUBSET = 387 store_thm 388 ("UNION_SUBSET", 389 ���!(s:'a->bool) t u. 390 ((s UNION t) SUBSET u) = ((s SUBSET u) /\ (t SUBSET u))���, 391 REWRITE_TAC[SUBSET_DEF,IN_UNION] 392 THEN REPEAT GEN_TAC 393 THEN EQ_TAC 394 THEN REPEAT STRIP_TAC 395 THEN RES_TAC 396 ); 397 398 399val UNION_DIFF = 400 store_thm 401 ("UNION_DIFF", 402 ���!s t r:'a->bool. (s UNION t) DIFF r = ((s DIFF r) UNION (t DIFF r))���, 403 REWRITE_TAC[EXTENSION,IN_UNION,IN_DIFF] 404 THEN REPEAT GEN_TAC 405 THEN EQ_TAC 406 THEN STRIP_TAC 407 THEN ASM_REWRITE_TAC[] 408 ); 409 410val SUBSET_DIFF = 411 store_thm 412 ("SUBSET_DIFF", 413 ���!s t r:'a->bool. (s SUBSET t) ==> (s DIFF r SUBSET t DIFF r)���, 414 REWRITE_TAC[SUBSET_DEF,IN_DIFF] 415 THEN REPEAT GEN_TAC 416 THEN DISCH_TAC 417 THEN GEN_TAC 418 THEN STRIP_TAC 419 THEN RES_TAC 420 THEN ASM_REWRITE_TAC[] 421 ); 422 423val SUBSETS_UNION = 424 store_thm 425 ("SUBSETS_UNION", 426 ���!(s1:'a->bool) s2 t1 t2. 427 s1 SUBSET t1 /\ s2 SUBSET t2 ==> 428 (s1 UNION s2) SUBSET (t1 UNION t2)���, 429 REWRITE_TAC[SUBSET_DEF] 430 THEN REWRITE_TAC[IN_UNION] 431 THEN REPEAT STRIP_TAC (* 2 subgoals *) 432 THEN RES_TAC 433 THEN ASM_REWRITE_TAC[] 434 ); 435 436 437(* Theorems about DISJOINT: *) 438 439val DISJOINT_INSERT2 = store_thm 440 ("DISJOINT_INSERT2", 441 ���!s t (x:'a). DISJOINT s (x INSERT t) = (DISJOINT s t /\ ~(x IN s))���, 442 ONCE_REWRITE_TAC[DISJOINT_SYM] 443 THEN REWRITE_TAC[DISJOINT_INSERT] 444 ); 445 446val DISJOINT_UNION2 = store_thm 447 ("DISJOINT_UNION2", 448 ���!s t r:'a->bool. DISJOINT s (t UNION r) = (DISJOINT s t /\ DISJOINT s r)���, 449 ONCE_REWRITE_TAC[DISJOINT_SYM] 450 THEN REWRITE_TAC[DISJOINT_UNION] 451 ); 452 453val DISJOINT_SUBSET = 454 store_thm 455 ("DISJOINT_SUBSET", 456 ���!s t r:'a->bool. s SUBSET t /\ DISJOINT t r ==> DISJOINT s r���, 457 REWRITE_TAC[SUBSET_DEF,IN_DISJOINT] 458 THEN CONV_TAC (ONCE_DEPTH_CONV NOT_EXISTS_CONV) 459 THEN REWRITE_TAC[DE_MORGAN_THM] 460 THEN REPEAT STRIP_TAC 461 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x:'a���) 462 THENL 463 [ FIRST_ASSUM (IMP_RES_TAC o CONTRAPOS o SPEC ���x:'a���) 464 THEN ASM_REWRITE_TAC[], 465 466 ASM_REWRITE_TAC[] 467 ] 468 ); 469 470val UNION_DELETE = 471 store_thm 472 ("UNION_DELETE", 473 ���!s t (e:'a). 474 s UNION t DELETE e = (s DELETE e) UNION (t DELETE e)���, 475 REWRITE_TAC[EXTENSION] 476 THEN REPEAT GEN_TAC 477 THEN REWRITE_TAC[IN_UNION,IN_DELETE] 478 THEN EQ_TAC 479 THEN STRIP_TAC 480 THEN ASM_REWRITE_TAC[] 481 ); 482 483 484val IN = save_thm("IN", CONJ NOT_IN_EMPTY IN_INSERT); 485 486val UNION = save_thm("UNION", CONJ UNION_EMPTY INSERT_UNION_EQ); 487 488val INTER = save_thm("INTER", CONJ INTER_EMPTY INSERT_INTER); 489 490val DELETE = save_thm("DELETE", CONJ EMPTY_DELETE DELETE_INSERT); 491 492val SUBSET = save_thm("SUBSET", CONJ EMPTY_SUBSET INSERT_SUBSET); 493 494val IMAGE = save_thm("IMAGE", CONJ IMAGE_EMPTY IMAGE_INSERT); 495 496val DIFFF = save_thm("DIFFF", CONJ DIFF_EMPTY DIFF_INSERT); 497 498 499 500(* ======================================================================== *) 501(* UNION_SET is a function which takes a set of sets and produces the union *) 502(* of all of them, that is, if S = {Si} then UNION_SET S = S1 U ... U Sn. *) 503(* ======================================================================== *) 504 505val UNION_SET_EXISTS = 506 TAC_PROOF 507 (([], ���!s:('a->bool)->bool. 508 ?t. !x. x IN t = ?si. si IN s /\ x IN si���), 509 GEN_TAC 510 THEN EXISTS_TAC ���\x:'a. ?si. si IN s /\ x IN si��� 511 THEN REWRITE_TAC[SPECIFICATION] 512 THEN BETA_TAC 513 THEN REWRITE_TAC[] 514 ); 515 516 517local 518open Rsyntax 519in 520val IN_UNION_SET = 521 let val th1 = CONV_RULE SKOLEM_CONV UNION_SET_EXISTS in 522 new_specification{name="IN_UNION_SET", 523 consts=[{const_name="UNION_SET",fixity=NONE}], 524 sat_thm=th1} 525 end 526end; 527 528 529val UNION_SET_EMPTY_LEMMA = TAC_PROOF 530 (([], ���UNION_SET EMPTY = (EMPTY:'a->bool)���), 531 REWRITE_TAC [EXTENSION, IN_UNION_SET, IN] 532 ); 533 534val UNION_SET_INSERT_LEMMA = TAC_PROOF 535 (([], ���! (si:'a->bool) (s:('a->bool)->bool) . 536 UNION_SET (si INSERT s) = si UNION (UNION_SET s)���), 537 REWRITE_TAC [EXTENSION, IN_UNION_SET, IN_UNION, IN] 538 THEN REPEAT GEN_TAC 539 THEN EQ_TAC 540 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 541 THEN REPEAT STRIP_TAC 542 THENL [ ALL_TAC, 543 544 DISJ2_TAC 545 THEN EXISTS_TAC ���si':'a->bool���, 546 547 EXISTS_TAC ���si:'a->bool���, 548 549 EXISTS_TAC ���si':'a->bool��� 550 ] 551 THEN ASM_REWRITE_TAC [] 552 ); 553 554 555val UNION_SET = save_thm ("UNION_SET", 556 CONJ UNION_SET_EMPTY_LEMMA UNION_SET_INSERT_LEMMA); 557 558 559val UNION_SET_UNION = 560 store_thm 561 ("UNION_SET_UNION", 562 ���!s t : ('a->bool)->bool. 563 UNION_SET (s UNION t) = 564 UNION_SET s UNION UNION_SET t���, 565 REWRITE_TAC[EXTENSION,IN_UNION,IN_UNION_SET] 566 THEN REPEAT GEN_TAC 567 THEN EQ_TAC 568 THEN REPEAT STRIP_TAC 569 THENL [ DISJ1_TAC, DISJ2_TAC, ALL_TAC, ALL_TAC ] 570 THEN EXISTS_TAC ���si:'a->bool��� 571 THEN ASM_REWRITE_TAC[] 572 ); 573 574 575val EMPTY_UNION_SET = 576 store_thm 577 ("EMPTY_UNION_SET", 578 ���!s. (UNION_SET s = {}) = (!si:'a->bool. si IN s ==> (si = {}))���, 579 REWRITE_TAC[EXTENSION,IN,IN_UNION_SET] 580 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 581 THEN REWRITE_TAC[DE_MORGAN_THM,(SYM o SPEC_ALL)IMP_DISJ_THM] 582 THEN CONV_TAC (DEPTH_CONV RIGHT_IMP_FORALL_CONV) 583 THEN GEN_TAC 584 THEN EQ_TAC 585 THEN DISCH_THEN REWRITE_THM 586 ); 587 588 589val UNION_SET_EMPTY = 590 store_thm 591 ("UNION_SET_EMPTY", 592 ���!s:('a->bool)->bool. (UNION_SET s = {}) = ((s = {}) \/ (s = {{}}))���, 593 GEN_TAC 594 THEN ASM_CASES_TAC ���s = ({}:('a->bool)->bool)��� 595 THEN ASM_REWRITE_TAC[UNION_SET] 596 THEN UNDISCH_ALL_TAC 597 THEN REWRITE_TAC[EXTENSION] 598 THEN REWRITE_TAC[IN,IN_UNION_SET] 599 THEN CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) 600 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 601 THEN REWRITE_TAC[DE_MORGAN_THM] 602 THEN STRIP_TAC 603 THEN CONV_TAC (ONCE_DEPTH_CONV FORALL_SYM_CONV) 604 THEN REWRITE_TAC[(SYM o SPEC_ALL)IMP_DISJ_THM] 605 THEN CONV_TAC (DEPTH_CONV FORALL_IMP_CONV) 606 THEN EQ_TAC 607 THENL 608 [ DISCH_TAC 609 THEN GEN_TAC 610 THEN EQ_TAC 611 THENL 612 [ ASM_REWRITE_TAC[EXTENSION,IN], 613 614 DISCH_THEN REWRITE_THM 615 THEN RES_TAC 616 THEN ASM_CASES_TAC ���x = ({}:'a->bool)��� 617 THENL 618 [ POP_ASSUM (ASM_REWRITE_THM o SYM), 619 620 POP_ASSUM MP_TAC 621 THEN REWRITE_TAC[(SYM o SPEC_ALL)MEMBER_NOT_EMPTY] 622 THEN ASM_REWRITE_TAC[] 623 ] 624 ], 625 626 DISCH_THEN REWRITE_THM 627 THEN GEN_TAC 628 THEN DISCH_THEN REWRITE_THM 629 THEN REWRITE_TAC[IN] 630 ] 631 ); 632 633 634val UNION_SET_EMPTY_INSERT = 635 store_thm 636 ("UNION_SET_EMPTY_INSERT", 637 ���!s:('a->bool)->bool. UNION_SET ({} INSERT s) = UNION_SET s���, 638 REWRITE_TAC[UNION_SET,UNION_EMPTY] 639 ); 640 641val UNION_SET_DELETE = 642 store_thm 643 ("UNION_SET_DELETE", 644 ���!(s:('a->bool)->bool) e. 645 UNION_SET {si DELETE e | si IN s} = (UNION_SET s) DELETE e���, 646 REWRITE_TAC[EXTENSION] 647 THEN REWRITE_TAC[IN_UNION_SET,IN_DELETE,GSPECIFICATION] 648 THEN BETA_TAC 649 THEN REWRITE_TAC[PAIR_EQ] 650 THEN REPEAT GEN_TAC 651 THEN EQ_TAC 652 THENL 653 [ STRIP_TAC 654 THEN CONJ_TAC 655 THENL [ EXISTS_TAC ���x':'a->bool���, ALL_TAC ] 656 THEN POP_ASSUM MP_TAC 657 THEN ASM_REWRITE_TAC[IN_DELETE] 658 THEN DISCH_THEN REWRITE_THM, 659 660 STRIP_TAC 661 THEN EXISTS_TAC ���si DELETE (e:'a)��� 662 THEN ASM_REWRITE_TAC[IN_DELETE] 663 THEN EXISTS_TAC ���si:'a->bool��� 664 THEN ASM_REWRITE_TAC[] 665 ] 666 ); 667 668 669val FINITE_UNION_SET_IMP_LEMMA = 670 TAC_PROOF 671 (([], ���!s. FINITE s ==> (!si:'a->bool. si IN s ==> FINITE si) ==> 672 FINITE (UNION_SET s)���), 673 SET_INDUCT_TAC 674 THEN REWRITE_TAC[IN,UNION_SET,FINITE_EMPTY,FINITE_UNION] 675 THEN REPEAT STRIP_TAC 676 THENL 677 [ FIRST_ASSUM MATCH_MP_TAC 678 THEN REWRITE_TAC[], 679 680 FIRST_ASSUM (MATCH_MP_TAC o (test (dest_imp o concl))) 681 THEN REPEAT STRIP_TAC 682 THEN FIRST_ASSUM MATCH_MP_TAC 683 THEN ASM_REWRITE_TAC[] 684 ] 685 ); 686 687 688val FINITE_UNION_SET_IMP = 689 store_thm 690 ("FINITE_UNION_SET_IMP", 691 ���!s. FINITE s /\ (!si:'a->bool. si IN s ==> FINITE si) ==> 692 FINITE (UNION_SET s)���, 693 REPEAT STRIP_TAC 694 THEN IMP_RES_TAC FINITE_UNION_SET_IMP_LEMMA 695 ); 696 697 698val FINITE_UNION_SET_LEMMA1 = 699 TAC_PROOF 700 (([], ���!s. FINITE (UNION_SET s) ==> 701 (!si:'a->bool. si IN s ==> FINITE si)���), 702 GEN_TAC 703 THEN CONV_TAC CONTRAPOS_CONV 704 THEN CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) 705 THEN REWRITE_TAC[NOT_IMP] 706 THEN STRIP_TAC 707 THEN UNDISCH_ALL_TAC 708 THEN ONCE_REWRITE_TAC[DECOMPOSITION] 709 THEN STRIP_TAC 710 THEN STRIP_TAC 711 THEN ASM_REWRITE_TAC[UNION_SET,FINITE_UNION] 712 ); 713 714 715val FINITE_UNION_SET = 716 store_thm 717 ("FINITE_UNION_SET", 718 ���!(s:('a->bool)->bool). FINITE s ==> 719 (FINITE (UNION_SET s) = (!si. si IN s ==> FINITE si))���, 720 GEN_TAC 721 THEN STRIP_TAC 722 THEN EQ_TAC 723 THENL 724 [ REWRITE_TAC[FINITE_UNION_SET_LEMMA1], 725 726 IMP_RES_TAC FINITE_UNION_SET_IMP_LEMMA 727 ] 728 ); 729 730 731val GSPEC_EMPTY_LEMMA = 732 TAC_PROOF 733 (([], ���!s (e:'a). ({si DELETE e | si IN s} = {}) = (s = {})���), 734 REPEAT GEN_TAC 735 THEN EQ_TAC 736 THENL 737 [ CONV_TAC (RATOR_CONV (RAND_CONV (REWRITE_CONV[EXTENSION]))) 738 THEN REWRITE_TAC[IN] 739 THEN REWRITE_TAC[GSPECIFICATION] 740 THEN BETA_TAC 741 THEN REWRITE_TAC[PAIR_EQ] 742 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 743 THEN REWRITE_TAC[DE_MORGAN_THM] 744 THEN ONCE_REWRITE_TAC[DISJ_SYM] 745 THEN CONV_TAC (ONCE_DEPTH_CONV FORALL_SYM_CONV) 746 THEN CONV_TAC (DEPTH_CONV FORALL_OR_CONV) 747 THEN CONV_TAC (DEPTH_CONV FORALL_NOT_CONV) 748 THEN SUBGOAL_THEN ���!y. ?x. x = y DELETE (e:'a)��� REWRITE_THM 749 THENL 750 [ GEN_TAC 751 THEN EXISTS_TAC ���y DELETE (e:'a)��� 752 THEN REFL_TAC, 753 754 CONV_TAC (DEPTH_CONV FORALL_NOT_CONV) 755 THEN REWRITE_TAC[MEMBER_NOT_EMPTY] 756 ], 757 758 DISCH_THEN REWRITE_THM 759 THEN REWRITE_TAC[EXTENSION] 760 THEN REWRITE_TAC[IN] 761 THEN REWRITE_TAC[GSPECIFICATION] 762 THEN BETA_TAC 763 THEN REWRITE_TAC[PAIR_EQ] 764 ] 765 ); 766 767 768val _ = export_theory(); 769 770val _ = print_theory_to_file "-" "more_set.lst"; 771 772val _ = html_theory "more_set"; 773