1(* Playing around with what is really Morse-Kelley set theory *) 2 3open HolKernel boolLib bossLib Parse 4open boolSimps 5 6val _ = new_theory "vbgset" 7val _ = ParseExtras.temp_loose_equality() 8 9(* hide constants from the existing (typed) set theory *) 10val _ = app (ignore o hide) ["UNION", "IN", "SUBSET", "EMPTY", "INSERT", 11 "CROSS", "INTER", "BIGINTER", "BIGUNION"] 12 13(* create a new type (of VBG classes) *) 14val _ = new_type("vbgc", 0) 15 16(* with this call, the syntax with ��� is enabled as well. *) 17val _ = new_constant ("IN", ``:vbgc -> vbgc -> bool``) 18 19(* similarly, this abbreviation also allows for ��� *) 20val _ = overload_on ("NOTIN", ``��x y. ~(x ��� y)``) 21 22val SET_def = Define` SET(x) = ���w. x ��� w ` 23val SUBSET_def = Define`x ��� y <=> ���u. u ��� x ��� u ��� y` 24 25val EXTENSION = new_axiom ("EXTENSION", ``(a = b) <=> (���x. x ��� a <=> x ��� b)``) 26 27val SPECIFICATION = new_axiom( 28 "SPECIFICATION", 29 ``���(P : vbgc -> bool). ���w. ���x. x ��� w <=> SET(x) ��� P(x)``); 30 31val SPEC0 = new_specification( 32 "SPEC0", 33 ["SPEC0"], 34 CONV_RULE SKOLEM_CONV SPECIFICATION); 35val _ = export_rewrites ["SPEC0"] 36 37val EMPTY_def = Define`EMPTY = SPEC0 (��x. F)` 38 39val NOT_IN_EMPTY = store_thm( 40 "NOT_IN_EMPTY", 41 ``x ��� {}``, 42 SRW_TAC [][EMPTY_def]); 43val _ = export_rewrites ["NOT_IN_EMPTY"] 44 45val EMPTY_UNIQUE = store_thm( 46 "EMPTY_UNIQUE", 47 ``(���x. x ��� u) ��� (u = {})``, 48 SRW_TAC [][EXTENSION]); 49 50val INFINITY = new_axiom( 51 "INFINITY", 52 ``���w. SET w ��� (���u. u ��� w ��� ���x. x ��� u) ��� 53 ���x. x ��� w ��� ���y. y ��� w ��� ���u. u ��� y <=> u ��� x ��� (u = x)``); 54 55val EMPTY_SET = store_thm( 56 "EMPTY_SET", 57 ``SET {}``, 58 STRIP_ASSUME_TAC INFINITY THEN 59 `u = {}` by SRW_TAC [][EMPTY_UNIQUE] THEN 60 `SET u` by METIS_TAC [SET_def] THEN 61 METIS_TAC []); 62val _ = export_rewrites ["EMPTY_SET"] 63 64val EMPTY_SUBSET = store_thm( 65 "EMPTY_SUBSET", 66 ``{} ��� A ��� (A ��� {} <=> (A = {}))``, 67 SRW_TAC [][SUBSET_def] THEN METIS_TAC [EMPTY_UNIQUE, NOT_IN_EMPTY]); 68val _ = export_rewrites ["EMPTY_SUBSET"] 69 70val SUBSET_REFL = store_thm( 71 "SUBSET_REFL", 72 ``A ��� A``, 73 SRW_TAC [][SUBSET_def]); 74val _ = export_rewrites ["SUBSET_REFL"] 75 76val SUBSET_ANTISYM = store_thm( 77 "SUBSET_ANTISYM", 78 ``(x = y) <=> x ��� y ��� y ��� x``, 79 SRW_TAC [][EXTENSION, SUBSET_def] THEN METIS_TAC []); 80 81val SUBSET_TRANS = store_thm( 82 "SUBSET_TRANS", 83 ``x ��� y ��� y ��� z ��� x ��� z``, 84 SRW_TAC [][SUBSET_def]) 85 86val Sets_def = Define`Sets = SPEC0 (��x. T)` 87 88val SET_Sets = store_thm( 89 "SET_Sets", 90 ``x ��� Sets <=> SET x``, 91 SRW_TAC [][Sets_def]); 92 93val SUBSET_Sets = store_thm( 94 "SUBSET_Sets", 95 ``x ��� Sets``, 96 SRW_TAC [][SUBSET_def, SET_Sets, SET_def] THEN METIS_TAC []); 97 98val RUS_def = Define` 99 RUS = SPEC0 (\x. x ��� x) 100`; 101 102(* gives result 103 ��� RUS ��� RUS ��� SET RUS ��� RUS ��� RUS 104*) 105val RUSlemma = 106``RUS ��� RUS`` 107 |> (SIMP_CONV bool_ss [RUS_def, Once SPEC0] THENC 108 SIMP_CONV bool_ss [GSYM RUS_def]) 109 110val RUS_not_SET = store_thm( 111 "RUS_not_SET", 112 ``�� SET RUS``, 113 METIS_TAC [RUSlemma]); 114 115val POW_def = Define`POW A = SPEC0 (��x. x ��� A)` 116val IN_POW = store_thm( 117 "IN_POW", 118 ``x ��� POW A ��� SET x ��� x ��� A``, 119 SRW_TAC [][POW_def]); 120val _ = export_rewrites ["IN_POW"] 121 122val POWERSET = new_axiom( 123 "POWERSET", 124 ``SET a ��� ���w. SET w ��� ���x. x ��� a ��� x ��� w``); 125 126val SUBSETS_ARE_SETS = store_thm( 127 "SUBSETS_ARE_SETS", 128 ``���A B. SET A ��� B ��� A ��� SET B``, 129 REPEAT STRIP_TAC THEN IMP_RES_TAC POWERSET THEN 130 `B ��� w` by METIS_TAC [] THEN 131 METIS_TAC [SET_def]); 132 133val POW_SET_CLOSED = store_thm( 134 "POW_SET_CLOSED", 135 ``���a. SET a ��� SET (POW a)``, 136 REPEAT STRIP_TAC THEN IMP_RES_TAC POWERSET THEN 137 MATCH_MP_TAC SUBSETS_ARE_SETS THEN 138 Q.EXISTS_TAC `w` THEN SRW_TAC [][Once SUBSET_def]); 139 140 141val SINGC_def = Define` 142 SINGC a = SPEC0 (��x. x = a) 143` 144 145 146val PCLASS_SINGC_EMPTY = store_thm( 147 "PCLASS_SINGC_EMPTY", 148 ``��SET a ��� (SINGC a = {})``, 149 SRW_TAC [][SINGC_def, Once EXTENSION]); 150 151val SET_IN_SINGC = store_thm( 152 "SET_IN_SINGC", 153 ``SET a ��� (x ��� SINGC a ��� (x = a))``, 154 SRW_TAC [CONJ_ss][SINGC_def]); 155 156val SINGC_11 = store_thm( 157 "SINGC_11", 158 ``SET x ��� SET y ��� ((SINGC x = SINGC y) = (x = y))``, 159 SRW_TAC [][Once EXTENSION, SimpLHS] THEN 160 SRW_TAC [][SET_IN_SINGC] THEN METIS_TAC []); 161val _ = export_rewrites ["SINGC_11"] 162 163 164val PAIRC_def = Define`PAIRC a b = SPEC0 (��x. (x = a) ��� (x = b))` 165 166val SINGC_PAIRC = store_thm( 167 "SINGC_PAIRC", 168 ``SINGC a = PAIRC a a``, 169 SRW_TAC [][SINGC_def, PAIRC_def]); 170 171val PCLASS_PAIRC_EMPTY = store_thm( 172 "PCLASS_PAIRC_EMPTY", 173 ``��SET a ��� ��SET b ��� (PAIRC a b = {})``, 174 SRW_TAC [][PAIRC_def, Once EXTENSION] THEN 175 Cases_on `x = a` THEN SRW_TAC [][] THEN 176 Cases_on `x = b` THEN SRW_TAC [][]); 177 178val SET_IN_PAIRC = store_thm( 179 "SET_IN_PAIRC", 180 ``SET a ��� SET b ��� (���x. x ��� PAIRC a b ��� (x = a) ��� (x = b))``, 181 SRW_TAC [CONJ_ss, DNF_ss][PAIRC_def]); 182 183val UNORDERED_PAIRS = new_axiom( 184 "UNORDERED_PAIRS", 185 ``SET a ��� SET b ��� ���w. SET w ��� a ��� w ��� b ��� w``); 186 187val PAIRC_SET_CLOSED = store_thm( 188 "PAIRC_SET_CLOSED", 189 ``SET a ��� SET b ��� SET (PAIRC a b)``, 190 DISCH_THEN (fn th => STRIP_ASSUME_TAC (MATCH_MP UNORDERED_PAIRS th) THEN 191 STRIP_ASSUME_TAC th) THEN 192 MATCH_MP_TAC SUBSETS_ARE_SETS THEN Q.EXISTS_TAC `w` THEN 193 SRW_TAC [][SUBSET_def, SET_IN_PAIRC] THEN SRW_TAC [][]); 194 195val SINGC_SET = store_thm( 196 "SINGC_SET", 197 ``SET (SINGC a)``, 198 Cases_on `SET a` THEN1 SRW_TAC [][SINGC_PAIRC, PAIRC_SET_CLOSED] THEN 199 SRW_TAC [][PCLASS_SINGC_EMPTY]); 200val _ = export_rewrites ["SINGC_SET"] 201 202(* UNION ish operations *) 203 204val UNION_def = Define`a ��� b = SPEC0 (��x. x ��� a ��� x ��� b)` 205 206val IN_UNION = store_thm( 207 "IN_UNION", 208 ``x ��� A ��� B ��� x ��� A ��� x ��� B``, 209 SRW_TAC [][UNION_def] THEN METIS_TAC [SET_def]); 210val _ = export_rewrites ["IN_UNION"] 211 212val BIGUNION_def = Define`BIGUNION A = SPEC0 (��x. ���y. y ��� A ��� x ��� y)` 213val IN_BIGUNION = store_thm( 214 "IN_BIGUNION", 215 ``x ��� BIGUNION A ��� ���y. y ��� A ��� x ��� y``, 216 SRW_TAC [][BIGUNION_def] THEN METIS_TAC [SET_def]); 217val _ = export_rewrites ["IN_BIGUNION"] 218 219val EMPTY_UNION = store_thm( 220 "EMPTY_UNION", 221 ``({} ��� A = A) ��� (A ��� {} = A)``, 222 SRW_TAC [][EXTENSION]); 223val _ = export_rewrites ["EMPTY_UNION"] 224 225val UNIONS = new_axiom( 226 "UNIONS", 227 ``SET a ��� ���w. SET w ��� ���x y. x ��� y ��� y ��� a ��� x ��� w``); 228 229val UNION_SET_CLOSED = store_thm( 230 "UNION_SET_CLOSED", 231 ``SET (A ��� B) ��� SET A ��� SET B``, 232 Tactical.REVERSE EQ_TAC >| [ 233 STRIP_TAC THEN 234 `SET (PAIRC A B)` by METIS_TAC [PAIRC_SET_CLOSED] THEN 235 POP_ASSUM (STRIP_ASSUME_TAC o MATCH_MP UNIONS) THEN 236 POP_ASSUM MP_TAC THEN 237 ASM_SIMP_TAC (srw_ss() ++ DNF_ss)[SET_IN_PAIRC] THEN 238 STRIP_TAC THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN Q.EXISTS_TAC `w` THEN 239 SRW_TAC [][SUBSET_def] THEN SRW_TAC [][], 240 strip_tac >> conj_tac >> match_mp_tac SUBSETS_ARE_SETS >> 241 qexists_tac `A ��� B` >> srw_tac [][SUBSET_def] 242 ]); 243val _ = export_rewrites ["UNION_SET_CLOSED"] 244 245val BIGUNION_SET_CLOSED = store_thm( 246 "BIGUNION_SET_CLOSED", 247 ``SET A ��� SET (BIGUNION A)``, 248 STRIP_TAC THEN IMP_RES_TAC UNIONS THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN 249 Q.EXISTS_TAC `w` THEN ASM_SIMP_TAC (srw_ss()) [SUBSET_def] THEN 250 METIS_TAC []); 251 252(* intersections *) 253val INTER_def = Define` 254 s1 INTER s2 = SPEC0 (��e. e ��� s1 ��� e ��� s2) 255`; 256 257val IN_INTER = store_thm( 258 "IN_INTER", 259 ``e ��� s1 ��� s2 ��� SET e ��� e ��� s1 ��� e ��� s2``, 260 rw [INTER_def]); 261val _ = export_rewrites ["IN_INTER"] 262 263val INTER_SET_CLOSED = store_thm( 264 "INTER_SET_CLOSED", 265 ``(SET s1 ��� SET (s1 ��� s2)) ��� (SET s2 ��� SET (s1 ��� s2))``, 266 rpt strip_tac >> match_mp_tac SUBSETS_ARE_SETS >| [ 267 qexists_tac `s1`, 268 qexists_tac `s2` 269 ] >> rw[SUBSET_def]); 270val _ = export_rewrites ["INTER_SET_CLOSED"] 271 272val INSERT_def = Define`x INSERT y = SINGC x ��� y` 273 274val IN_INSERT = store_thm( 275 "IN_INSERT", 276 ``x ��� a INSERT A ��� SET a ��� (x = a) ��� x ��� A``, 277 SRW_TAC [][INSERT_def] THEN Cases_on `SET a` THEN 278 SRW_TAC [][SET_IN_SINGC, PCLASS_SINGC_EMPTY]); 279val _ = export_rewrites ["IN_INSERT"] 280 281val SET_INSERT = store_thm( 282 "SET_INSERT", 283 ``SET (x INSERT b) = SET b``, 284 SRW_TAC [][INSERT_def]) 285val _ = export_rewrites ["SET_INSERT"] 286 287val INSERT_IDEM = store_thm( 288 "INSERT_IDEM", 289 ``a INSERT a INSERT s = a INSERT s``, 290 SRW_TAC [][Once EXTENSION] THEN METIS_TAC []); 291val _ = export_rewrites ["INSERT_IDEM"] 292 293val SUBSET_SING = store_thm( 294 "SUBSET_SING", 295 ``x ��� {a} ��� SET a ��� (x = {a}) ��� (x = {})``, 296 SRW_TAC [][SUBSET_def] THEN EQ_TAC THENL [ 297 Cases_on `SET a` THEN SRW_TAC [][] THENL [ 298 Cases_on `x = {}` THEN SRW_TAC [][] THEN 299 SRW_TAC [][Once EXTENSION] THEN 300 `���b. b ��� x` by METIS_TAC [EMPTY_UNIQUE] THEN 301 METIS_TAC [], 302 METIS_TAC [EMPTY_UNIQUE] 303 ], 304 SIMP_TAC (srw_ss()) [DISJ_IMP_THM] 305 ]); 306val _ = export_rewrites ["SUBSET_SING"] 307 308val BIGUNION_EMPTY = store_thm( 309 "BIGUNION_EMPTY", 310 ``(BIGUNION {} = {}) ��� (BIGUNION {{}} = {})``, 311 CONJ_TAC THEN SRW_TAC [][Once EXTENSION]); 312val _ = export_rewrites ["BIGUNION_EMPTY"] 313 314val BIGUNION_SING = store_thm( 315 "BIGUNION_SING", 316 ``SET a ��� (BIGUNION {a} = a)``, 317 SRW_TAC [][Once EXTENSION]); 318 319val BIGUNION_UNION = store_thm( 320 "BIGUNION_UNION", 321 ``SET a ��� SET b ��� (BIGUNION {a;b} = a ��� b)``, 322 SRW_TAC [DNF_ss][Once EXTENSION]); 323 324val POW_EMPTY = store_thm( 325 "POW_EMPTY", 326 ``POW {} = {{}}``, 327 SRW_TAC [][Once EXTENSION] THEN SRW_TAC [CONJ_ss][]); 328 329val POW_SING = store_thm( 330 "POW_SING", 331 ``SET a ��� (POW {a} = {{}; {a}})``, 332 SRW_TAC [][Once EXTENSION] THEN 333 ASM_SIMP_TAC (srw_ss() ++ CONJ_ss ++ DNF_ss) [] THEN 334 METIS_TAC []); 335 336(* "primitive ordered pair" *) 337val POPAIR_def = Define`POPAIR a b = {{a}; {a;b}}` 338 339val POPAIR_SET = store_thm( 340 "POPAIR_SET", 341 ``SET (POPAIR a b)``, 342 SRW_TAC [][POPAIR_def]); 343val _ = export_rewrites ["POPAIR_SET"] 344 345val SING_11 = store_thm( 346 "SING_11", 347 ``SET a ��� SET b ��� (({a} = {b}) = (a = b))``, 348 STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [SimpLHS, Once EXTENSION] THEN 349 SRW_TAC [][] THEN METIS_TAC []); 350 351val SING_EQ_PAIR = store_thm( 352 "SING_EQ_PAIR", 353 ``SET a ��� SET b ��� SET c ��� (({a;b} = {c}) = (a = b) ��� (b = c))``, 354 STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [SimpLHS, Once EXTENSION] THEN 355 SRW_TAC [][] THEN METIS_TAC []); 356 357val PAIR_EQ_PAIR = store_thm( 358 "PAIR_EQ_PAIR", 359 ``SET a ��� SET b ��� SET c ��� SET d ��� 360 (({a;b} = {c;d}) ��� (a = c) ��� (b = d) ��� (a = d) ��� (b = c))``, 361 STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [Once EXTENSION, SimpLHS] THEN 362 SRW_TAC [][] THEN METIS_TAC []); 363 364val POPAIR_INJ = store_thm( 365 "POPAIR_INJ", 366 ``SET a ��� SET b ��� SET c ��� SET d ��� 367 ((POPAIR a b = POPAIR c d) ��� (a = c) ��� (b = d))``, 368 STRIP_TAC THEN SRW_TAC [][SimpLHS, Once EXTENSION] THEN 369 SRW_TAC [][POPAIR_def] THEN REVERSE EQ_TAC THEN1 SRW_TAC [][] THEN 370 METIS_TAC [SING_11, SING_EQ_PAIR, PAIR_EQ_PAIR]); 371 372(* ordered pairs that work when classes are involved *) 373val OPAIR_def = Define` 374 OPAIR a b = SPEC0 (��x. ���y. y ��� a ��� (x = POPAIR {} y)) ��� 375 SPEC0 (��x. ���y. y ��� b ��� (x = POPAIR {{}} y)) 376`; 377 378val SET_OPAIR = store_thm( 379 "SET_OPAIR", 380 ``SET a ��� SET b ��� SET (OPAIR a b)``, 381 SRW_TAC [][OPAIR_def] THENL[ 382 SRW_TAC [][POPAIR_def] THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN 383 SRW_TAC [DNF_ss][SUBSET_def] THEN 384 Q.EXISTS_TAC `POW (POW (a ��� {{}}))` THEN 385 SRW_TAC [][POW_SET_CLOSED] THEN 386 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUBSET_def], 387 SRW_TAC [][POPAIR_def] THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN 388 SRW_TAC [DNF_ss][SUBSET_def] THEN 389 Q.EXISTS_TAC `POW (POW (b ��� {{{}}}))` THEN 390 SRW_TAC [][POW_SET_CLOSED] THEN 391 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUBSET_def] 392 ]); 393val _ = export_rewrites ["SET_OPAIR"] 394 395val ZERO_NEQ_ONE = store_thm( 396 "ZERO_NEQ_ONE", 397 ``{} ��� {{}}``, 398 SRW_TAC [][EXTENSION] THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][]); 399val _ = export_rewrites ["ZERO_NEQ_ONE"] 400 401val POPAIR_01 = store_thm( 402 "POPAIR_01", 403 ``POPAIR {} x ��� POPAIR {{}} y``, 404 SRW_TAC [][POPAIR_def] THEN SRW_TAC [][Once EXTENSION] THEN 405 Q.EXISTS_TAC `{{}}` THEN SRW_TAC [][SING_11] THEN 406 SRW_TAC [][Once EXTENSION] THEN Q.EXISTS_TAC `{{}}` THEN 407 SRW_TAC [][]); 408 409val OPAIR_11 = store_thm( 410 "OPAIR_11", 411 ``((OPAIR a b = OPAIR c d) ��� (a = c) ��� (b = d))``, 412 SRW_TAC [][Once EXTENSION, SimpLHS] THEN 413 SRW_TAC [][OPAIR_def] THEN 414 REVERSE EQ_TAC THEN1 SRW_TAC [][] THEN 415 REPEAT STRIP_TAC THENL [ 416 SIMP_TAC (srw_ss()) [EXTENSION, EQ_IMP_THM] THEN 417 Q.X_GEN_TAC `e` THEN REPEAT STRIP_TAC THEN 418 `SET e` by METIS_TAC [SET_def] THEN 419 FIRST_X_ASSUM (Q.SPEC_THEN `POPAIR {} e` MP_TAC) THEN 420 ASM_SIMP_TAC (srw_ss()) [POPAIR_01] THENL [ 421 DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #1 o 422 EQ_IMP_RULE), 423 DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #2 o 424 EQ_IMP_RULE) 425 ] THEN 426 DISCH_THEN (Q.SPEC_THEN `e` MP_TAC) THEN SRW_TAC [][] THEN 427 POP_ASSUM MP_TAC THEN 428 `SET y` by METIS_TAC [SET_def] THEN 429 SRW_TAC [][POPAIR_INJ], 430 431 SIMP_TAC (srw_ss()) [EXTENSION, EQ_IMP_THM] THEN 432 Q.X_GEN_TAC `e` THEN REPEAT STRIP_TAC THEN 433 `SET e` by METIS_TAC [SET_def] THEN 434 FIRST_X_ASSUM (Q.SPEC_THEN `POPAIR {{}} e` MP_TAC) THEN 435 ASM_SIMP_TAC (srw_ss()) [POPAIR_01] THENL [ 436 DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #1 o 437 EQ_IMP_RULE), 438 DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #2 o 439 EQ_IMP_RULE) 440 ] THEN 441 DISCH_THEN (Q.SPEC_THEN `e` MP_TAC) THEN SRW_TAC [][] THEN 442 POP_ASSUM MP_TAC THEN 443 `SET y` by METIS_TAC [SET_def] THEN 444 SRW_TAC [][POPAIR_INJ] 445 ]); 446val _ = export_rewrites ["OPAIR_11"] 447 448val _ = add_rule { fixity = Closefix, 449 term_name = "OPAIR", 450 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 451 paren_style = OnlyIfNecessary, 452 pp_elements = [TOK "���", TM, HardSpace 1, 453 TOK "��", BreakSpace(1,2), 454 TM, TOK "���"]} 455 456val CROSS_def = Define` 457 s1 CROSS s2 = SPEC0 (��x. ���a b. a ��� s1 ��� b ��� s2 ��� (x = ���a �� b���)) 458`; 459 460val FunSpace_def = Define` 461 FunSpace A B = SPEC0 (��f. f ��� A �� B ��� ���a. a ��� A ��� ���!b. ���a �� b��� ��� f) 462` 463 464val id_def = Define` 465 id A = SPEC0 (��x. ���a. a ��� A ��� (x = ���a��a���)) 466`; 467 468(* 469val apply_def = new_specification("apply_def", 470 ["apply"], 471 CONV_RULE SKOLEM_CONV 472 (prove(``���f x A B. f ��� FunSpace A B ��� x ��� A ��� 473 ���y. y ��� B ��� ���x��y��� ��� f``, 474 SRW_TAC [][FunSpace_def, SPEC0, CROSS_def] THEN 475 RES_TAC THEN 476 FULL_SIMP_TAC (srw_ss()) [EXISTS_UNIQUE_THM] THEN 477 Q.EXISTS_TAC `b` THEN SRW_TAC [][] THEN 478 FULL_SIMP_TAC (srw_ss()) [SUBSET_def, SPEC0] THEN 479 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [OPAIR_11]) 480*) 481 482 483(* 484val FORMATION = new_axiom( 485 486*) 487 488val FOUNDATION = new_axiom( 489 "FOUNDATION", 490 ``(���a. SET a ��� a ��� w ��� a ��� w) ��� ���a. SET a ��� a ��� w``); 491 492val IN_INDUCTION = store_thm( 493 "IN_INDUCTION", 494 ``(���a. SET a ��� (���x. x ��� a ��� P x) ��� P a) ��� ���a. SET a ��� P a``, 495 rpt strip_tac >> 496 MP_TAC (INST [``w:vbgc`` |-> ``SPEC0 (��x. P x)``] FOUNDATION) >> 497 rw[SUBSET_def]); 498val _ = IndDefLib.export_rule_induction "IN_INDUCTION" 499 500val IN_REFL = store_thm( 501 "IN_REFL", 502 ``x ��� x``, 503 Cases_on `SET x` >| [ 504 pop_assum mp_tac >> qid_spec_tac `x` >> 505 ho_match_mp_tac IN_INDUCTION >> metis_tac [], 506 fs[SET_def] 507 ]); 508val _ = export_rewrites ["IN_REFL"] 509 510val IN_ANTISYM = store_thm( 511 "IN_ANTISYM", 512 ``x ��� y ��� y ��� x ��� F``, 513 qsuff_tac `���x. SET x ��� ���y. y ��� x ��� x ��� y` >- metis_tac [SET_def] >> 514 Induct_on `SET x` >> metis_tac []); 515 516val IN3_ANTISYM = store_thm( 517 "IN3_ANTISYM", 518 ``x ��� y ��� y ��� z ��� z ��� x ��� F``, 519 qsuff_tac `���x. SET x ��� ���y z. y ��� z ��� z ��� x ��� x ��� y` >- metis_tac [SET_def] >> 520 Induct_on `SET x` >> metis_tac []); 521 522val FORMATION = new_axiom( 523 "FORMATION", 524 ``SET a ��� (���x. x ��� a ��� ���!y. P x y) ��� (���x y. x ��� a ��� P x y ��� SET y) ��� 525 ���w. SET w ��� ���y. y ��� w ��� ���x. x ��� a ��� P x y``); 526 527val bad_def = with_flag (computeLib.auto_import_definitions, false) Define` 528 bad f a = SET a ��� (���i. SET (f i)) ��� (f 0 = {a}) ��� 529 (���i x. x ��� f i ��� x ��� f (i + 1) ��� {}) 530`; 531 532val FOUNDATION2 = store_thm( 533 "FOUNDATION2", 534 ``�����f:num -> vbgc. 535 (���i. SET (f i)) ��� (���e. SET e ��� (f 0 = {e})) ��� 536 (���i x. x ��� f i ��� x ��� f (i + 1) ��� {})``, 537 qsuff_tac `���a. SET a ��� �����f. bad f a` 538 >- (rw[bad_def] >> 539 Tactical.REVERSE (Cases_on `���i. SET (f i)`) >- metis_tac [] >> 540 rw[] >> Cases_on `���e. f 0 = {e}` >> fs[] >> 541 Tactical.REVERSE (Cases_on `SET e`) 542 >- (DISJ1_TAC >> rw[Once EXTENSION]) >> 543 DISJ2_TAC >> 544 first_x_assum (qspec_then `e` mp_tac) >> rw[] >> 545 metis_tac []) >> 546 Induct_on `SET a` >> qx_gen_tac `a` >> Cases_on `SET a` >> simp[] >> 547 CONV_TAC CONTRAPOS_CONV >> rw[] >> 548 `a ��� f 0` by metis_tac [IN_INSERT, bad_def] >> 549 `a ��� f 1 ��� {}` by metis_tac [bad_def, DECIDE ``0 + 1 = 1``] >> 550 `���b. b ��� a ��� f 1` by metis_tac [EMPTY_UNIQUE] >> 551 qabbrev_tac ` 552 poor = ��p. (���i. p i ��� f (i + 1)) ��� b ��� p 0 ��� 553 (���i x. x ��� p i ��� x ��� f (i + 2) ��� p (i + 1)) 554 ` >> 555 qabbrev_tac `P = ��n. f (n + 1)` >> 556 `poor P` 557 by (srw_tac[ARITH_ss][Abbr`P`,Abbr`poor`] >> fs[] >> 558 rw[SUBSET_def]) >> 559 qabbrev_tac `N = ��n. SPEC0 (��x. ���p. poor p ��� x ��� p n)` >> 560 `b ��� N 0` 561 by (rw[Abbr`N`] >- metis_tac [SET_def] >> fs[Abbr`poor`]) >> 562 `poor N` 563 by (qpat_assum `Abbrev(poor = X)` 564 (fn th => ASSUME_TAC th THEN MP_TAC th) >> 565 disch_then (SUBST1_TAC o REWRITE_RULE [markerTheory.Abbrev_def]) >> 566 BETA_TAC >> ASM_REWRITE_TAC[] >> rpt strip_tac >| [ 567 qsuff_tac `N i ��� P i` >- metis_tac [SUBSET_def] >> 568 rw[Abbr`N`, SUBSET_def], 569 `���p. poor p ��� x ��� f(i + 2) ��� p (i + 1)` 570 by (rpt strip_tac >> 571 `x ��� p i` by fs[Abbr`N`, Abbr`poor`] >> 572 metis_tac []) >> 573 rw[Abbr`N`, SUBSET_def] >> metis_tac [SUBSET_def, IN_INTER] 574 ]) >> 575 qexists_tac `b` >> fs[] >> 576 `���p. poor p ��� ���n. SET (p n)` 577 by (rw[Abbr`poor`] >> match_mp_tac SUBSETS_ARE_SETS >> 578 qexists_tac `f (n + 1)` >> fs[bad_def]) >> 579 qexists_tac `N` >> rw[bad_def] >|[ 580 rw[Once EXTENSION, EQ_IMP_THM] >> 581 spose_not_then assume_tac >> 582 qpat_assum `x ��� N 0` mp_tac >> 583 qpat_assum `Abbrev(N = X)` 584 (fn th => ASSUME_TAC th >> 585 MP_TAC (REWRITE_RULE [markerTheory.Abbrev_def] th)) >> 586 disch_then SUBST1_TAC >> BETA_TAC >> rw[] >> DISJ2_TAC >> 587 qexists_tac `��n. if n = 0 then SPEC0 (��y. y ��� N 0 ��� y ��� x) else N n` >> 588 rw[] >> 589 qpat_assum `Abbrev(poor = X)` 590 (fn th => assume_tac th >> 591 SUBST1_TAC (REWRITE_RULE [markerTheory.Abbrev_def] th)) >> 592 BETA_TAC >> ASM_REWRITE_TAC [] THEN BETA_TAC >> simp[] >> conj_tac 593 >- (rw[SUBSET_def] >> 594 qpat_assum `poor N` mp_tac >> 595 rw[Abbr`poor`] >> metis_tac [SUBSET_def, DECIDE ``0 + 1 = 1``]) >> 596 map_every qx_gen_tac [`i`, `y`] >> 597 rw[] >> metis_tac [DECIDE ``(0 + 1 = 1) ��� (0 + 2 = 2)``], 598 `x ��� f (i + 1)` by metis_tac[SUBSET_def] >> 599 `x ��� f(i + 2) ��� N (i + 1)` by metis_tac [] >> 600 `x ��� f(i + 2) ��� {}` by metis_tac [bad_def, DECIDE ``i + 1 + 1 = i + 2``] >> 601 simp[EXTENSION] >> metis_tac[SET_def, EMPTY_UNIQUE, IN_INTER, SUBSET_def] 602 ]) 603 604val lemma0 = prove( 605 ``SET ss ��� SET ss ��� ���x. x ��� ss ��� SET (x ��� a)``, 606 rw[] >> match_mp_tac SUBSETS_ARE_SETS >> qexists_tac `x` >> 607 rw[SUBSET_def] >> metis_tac [SET_def]) 608val formlemma = 609 FORMATION |> Q.INST [`a` |-> `ss`, 610 `P` |-> `��x y. (y = x ��� a)`] 611 |> SIMP_RULE (srw_ss()) [] 612 |> C MP (UNDISCH lemma0) 613 614val FOUNDATION3 = store_thm( 615 "FOUNDATION3", 616 ``���a. a ��� {} ��� ���x. x ��� a ��� (x ��� a = {})``, 617 spose_not_then strip_assume_tac >> 618 `���b. b ��� a` by metis_tac [EMPTY_UNIQUE] >> 619 qabbrev_tac ` 620 m = PRIM_REC {b} (��s n. BIGUNION (SPEC0 (��y. ���x. x ��� s ��� (y = x ��� a)))) 621 ` >> 622 `���i. m i ��� a` 623 by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM, SUBSET_def] >> 624 fs[]) >> 625 `���i. SET (m i)` 626 by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >> 627 match_mp_tac BIGUNION_SET_CLOSED >> 628 qpat_assum `SET sss` mp_tac >> 629 qmatch_abbrev_tac `SET ss ��� SET sss` >> 630 qunabbrev_tac `sss` >> strip_tac >> 631 strip_assume_tac formlemma >> 632 qsuff_tac `SPEC0 (��y. ���x. x ��� ss ��� (y = x ��� a)) = w` >- rw[] >> 633 simp[Once EXTENSION, EQ_IMP_THM] >> 634 asm_simp_tac (srw_ss() ++ DNF_ss) [] >> qx_gen_tac `y` >> strip_tac >> 635 match_mp_tac SUBSETS_ARE_SETS >> qexists_tac `y` >> 636 metis_tac [SUBSET_def, SET_def, IN_INTER]) >> 637 `bad m b` 638 by (rw[bad_def] 639 >- metis_tac [SET_def] 640 >- rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] 641 >- (`x ��� a` by metis_tac [SUBSET_def] >> 642 `x ��� a ��� {}` by metis_tac [] >> 643 `���y. y ��� x ��� a` by metis_tac [EMPTY_UNIQUE] >> 644 `y ��� m (SUC i)` 645 by (rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >> 646 srw_tac [DNF_ss][] >> 647 qexists_tac `x` >> rw[] 648 >- (match_mp_tac SUBSETS_ARE_SETS >> 649 qexists_tac `x` >> 650 metis_tac [SUBSET_def, IN_INTER, SET_def]) 651 >- metis_tac [SET_def] 652 >> fs[]) >> 653 fs[arithmeticTheory.ADD1] >> 654 rw[Once EXTENSION] >> metis_tac [SET_def])) >> 655 MP_TAC (FOUNDATION2 |> SIMP_RULE bool_ss [] 656 |> Q.SPEC `m`) >> 657 simp[] >> conj_tac 658 >- (qexists_tac `b` >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >> 659 metis_tac [SET_def]) >> 660 metis_tac [bad_def]) 661 662val _ = delete_const "bad" 663 664val _ = export_theory() 665