1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6(* --------------------------------------------------------------------- *) 7(* Definitions and theorems for higher order quotients package. *) 8(* Version that attempts to avoid the use of the Axiom of Choice. *) 9(* *) 10(* Fails in that from FUN_QUOTIENT can be derived the existance of *) 11(* an operator satisfying the axiom of the Hilbert choice operator. *) 12(* --------------------------------------------------------------------- *) 13 14 15val _ = new_theory "quotient"; 16 17(* 18load "dep_rewrite"; 19*) 20 21open prim_recTheory; 22open combinTheory; 23open pairTheory; 24open pairLib; 25open sumTheory; 26open listTheory; 27open rich_listTheory; 28open optionTheory; 29open listLib; 30open pred_setTheory; 31open bossLib; 32open res_quanTheory; 33open res_quanLib; 34open dep_rewrite; 35 36 37val REWRITE_THM = fn th => REWRITE_TAC[th]; 38val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th]; 39val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th]) 40 THEN REWRITE_TAC[th]; 41 42val POP_TAC = POP_ASSUM (fn th => ALL_TAC); 43 44 45(* =================================================================== *) 46(* To form a ABS / REP function or a equivalence relation REL from *) 47(* the corresponding functions/relations of the constituent subtypes *) 48(* of the main type, use the following table of operators: *) 49(* *) 50(* Type Operator Constructor Abstraction Equivalence *) 51(* *) 52(* Identity I x I $= *) 53(* Product (ty1 # ty2) (a,b) (abs1 ## abs2) (R1 ### R2) *) 54(* Sum (ty1 + ty2) (INL x) (abs1 ++ abs2) (R1 +++ R2) *) 55(* List (ty list) (CONS h t) (MAP abs) (LIST_REL R) *) 56(* Option (ty option) (SOME x) (OPTION_MAP abs) (OPTION_REL R) *) 57(* Function (ty1 -> ty2) (\x. f x) (rep1 --> abs2) (R1 ===> R2) *) 58(* *) 59(* =================================================================== *) 60 61 62 63val QUOTIENT_def = 64 Define 65 `QUOTIENT R (abs:'a->'b) = 66 (!a. ?r. R r r /\ (abs r = a)) /\ 67 (!r s. R r s = R r r /\ R s s /\ (abs r = abs s))`; 68 69val QUOTIENT_REP = store_thm 70 ("QUOTIENT_REP", 71 (--`!R (abs:'a->'b). QUOTIENT R abs ==> (!a. ?r. R r r /\ (abs r = a))`--), 72 REWRITE_TAC[QUOTIENT_def] 73 THEN REPEAT STRIP_TAC 74 ); 75 76val QUOTIENT_REL = store_thm 77 ("QUOTIENT_REL", 78 (--`!R (abs:'a->'b). QUOTIENT R abs ==> 79 (!r s. R r s = R r r /\ R s s /\ (abs r = abs s))`--), 80 REWRITE_TAC[QUOTIENT_def] 81 THEN REPEAT STRIP_TAC 82 ); 83 84val QUOTIENT_REL_ABS = store_thm 85 ("QUOTIENT_REL_ABS", 86 (--`!R (abs:'a->'b). QUOTIENT R abs ==> 87 (!r s. R r s ==> (abs r = abs s))`--), 88 REWRITE_TAC[QUOTIENT_def] 89 THEN REPEAT STRIP_TAC 90 THEN RES_TAC 91 ); 92 93val QUOTIENT_REL_ABS_EQ = store_thm 94 ("QUOTIENT_REL_ABS_EQ", 95 (--`!R (abs:'a->'b). QUOTIENT R abs ==> 96 (!r s. R r r ==> R s s ==> 97 (R r s = (abs r = abs s)))`--), 98 REWRITE_TAC[QUOTIENT_def] 99 THEN REPEAT GEN_TAC 100 THEN STRIP_TAC 101 THEN POP_ASSUM (fn th => REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[th]) 102 THEN ASM_REWRITE_TAC[] 103 ); 104 105 106 107 108val IDENTITY_EQUIV = store_thm 109 ("IDENTITY_EQUIV", 110 (--`!x y:'a. (x = y) = ($= x = $= y)`--), 111 REPEAT GEN_TAC 112 THEN EQ_TAC 113 THEN DISCH_THEN REWRITE_THM 114 ); 115 116val IDENTITY_QUOTIENT = store_thm 117 ("IDENTITY_QUOTIENT", 118 (--`QUOTIENT $= (I:'a->'a)`--), 119 REWRITE_TAC[QUOTIENT_def] 120 THEN REWRITE_TAC[I_THM] 121 THEN GEN_TAC 122 THEN EXISTS_TAC (--`a:'a`--) 123 THEN REFL_TAC 124 ); 125 126 127 128val EQUIV_REFL_SYM_TRANS = store_thm 129 ("EQUIV_REFL_SYM_TRANS", 130 (--`!R. 131 (!x y:'a. R x y = (R x = R y)) 132 = 133 (!x. R x x) /\ 134 (!x y. R x y ==> R y x) /\ 135 (!x y z. R x y /\ R y z ==> R x z)`--), 136 GEN_TAC 137 THEN EQ_TAC 138 THEN STRIP_TAC 139 THEN REPEAT CONJ_TAC 140 THEN REPEAT GEN_TAC 141 THENL (* 4 subgoals *) 142 [ 143 PURE_ASM_REWRITE_TAC[] 144 THEN REFL_TAC, 145 146 PURE_ASM_REWRITE_TAC[] 147 THEN MATCH_ACCEPT_TAC EQ_SYM, 148 149 PURE_ASM_REWRITE_TAC[] 150 THEN MATCH_ACCEPT_TAC EQ_TRANS, 151 152 CONV_TAC (RAND_CONV FUN_EQ_CONV) 153 THEN EQ_TAC 154 THEN DISCH_TAC 155 THENL 156 [ GEN_TAC 157 THEN EQ_TAC 158 THEN DISCH_TAC 159 THEN RES_TAC 160 THEN RES_TAC, 161 162 PURE_ASM_REWRITE_TAC[] 163 ] 164 ] 165 ); 166 167 168val QUOTIENT_SYM = store_thm 169 ("QUOTIENT_SYM", 170 (--`!R (abs:'a -> 'b). QUOTIENT R abs ==> 171 !x y. R x y ==> R y x`--), 172 REPEAT GEN_TAC 173 THEN STRIP_TAC 174 THEN REPEAT GEN_TAC 175 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 176 THEN STRIP_TAC 177 THEN ASM_REWRITE_TAC[] 178 ); 179 180val QUOTIENT_TRANS = store_thm 181 ("QUOTIENT_TRANS", 182 (--`!R (abs:'a -> 'b). QUOTIENT R abs ==> 183 !x y z. R x y /\ R y z ==> R x z`--), 184 REPEAT GEN_TAC 185 THEN STRIP_TAC 186 THEN REPEAT GEN_TAC 187 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 188 THEN STRIP_TAC 189 THEN ASM_REWRITE_TAC[] 190 ); 191 192 193 194 195(* for LIST_REP or LIST_ABS, just use MAP! See Theorem MAP. *) 196 197val LIST_MAP_I = 198 store_thm 199 ("LIST_MAP_I", 200 (--`MAP (I:'a -> 'a) = I`--), 201 REWRITE_TAC[FUN_EQ_THM] 202 THEN Induct 203 THEN ASM_REWRITE_TAC[MAP,I_THM] 204 ); 205 206(* for list equivalence relation, use prefix LIST_REL, defined here: *) 207 208(* Almost MAP2, but this is totally defined: *) 209val LIST_REL_def = 210 Define 211 `(LIST_REL R [] [] = T) /\ 212 (LIST_REL R ((a:'a)::as) [] = F) /\ 213 (LIST_REL R [] ((b:'a)::bs) = F) /\ 214 (LIST_REL R (a::as) (b::bs) = (R a b /\ LIST_REL R as bs))`; 215 216val LIST_REL_ind = fetch "-" "LIST_REL_ind"; 217 218val LIST_REL_EQ = store_thm 219 ("LIST_REL_EQ", 220 (--`(LIST_REL ($= : 'a->'a->bool)) = $=`--), 221 CONV_TAC FUN_EQ_CONV 222 THEN CONV_TAC (RAND_CONV (ABS_CONV FUN_EQ_CONV)) 223 THEN Induct 224 THENL [ ALL_TAC, GEN_TAC ] 225 THEN Induct 226 THEN REWRITE_TAC[LIST_REL_def,NOT_CONS_NIL,NOT_NIL_CONS] 227 THEN GEN_TAC 228 THEN ASM_REWRITE_TAC[CONS_11] 229 ); 230 231val LIST_REL_REFL = store_thm 232 ("LIST_REL_REFL", 233 (--`!R. (!x y:'a. R x y = (R x = R y)) ==> 234 !x. LIST_REL R x x`--), 235 GEN_TAC 236 THEN DISCH_TAC 237 THEN Induct 238 THEN REWRITE_TAC[LIST_REL_def] 239 THEN GEN_TAC 240 THEN ASM_REWRITE_TAC[] 241 ); 242 243val LIST_EQUIV = store_thm 244 ("LIST_EQUIV", 245 (--`!R. (!x y:'a. R x y = (R x = R y)) ==> 246 (!x y. LIST_REL R x y = (LIST_REL R x = LIST_REL R y))`--), 247 GEN_TAC 248 THEN DISCH_TAC 249 THEN Induct THENL [ALL_TAC, GEN_TAC] 250 THEN Induct 251 THEN REWRITE_TAC[LIST_REL_def] 252 THENL 253 [ PROVE_TAC[LIST_REL_def], 254 255 PROVE_TAC[LIST_REL_def], 256 257 GEN_TAC 258 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 259 THEN EQ_TAC 260 THENL 261 [ STRIP_TAC 262 THEN Cases 263 THEN REWRITE_TAC[LIST_REL_def] 264 THEN PROVE_TAC[], 265 266 DISCH_THEN (MP_TAC o GEN ``c:'a`` o GEN ``cs:'a list`` 267 o SPEC ``(c:'a)::cs``) 268 THEN REWRITE_TAC[LIST_REL_def] 269 THEN IMP_RES_TAC LIST_REL_REFL 270 THEN PROVE_TAC[] 271 ] 272 ] 273 ); 274 275val LIST_REL_REL = store_thm 276 ("LIST_REL_REL", 277 (--`!R (abs:'a -> 'b). QUOTIENT R abs ==> 278 !r s. LIST_REL R r s = LIST_REL R r r /\ LIST_REL R s s /\ 279 (MAP abs r = MAP abs s)`--), 280 REPEAT GEN_TAC 281 THEN STRIP_TAC 282 THEN Induct 283 THENL [ ALL_TAC, GEN_TAC ] 284 THEN Cases 285 THEN ONCE_REWRITE_TAC[LIST_REL_def] 286 THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS] 287 THEN REWRITE_TAC[CONS_11] 288 THEN IMP_RES_THEN 289 (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th)))) 290 QUOTIENT_REL 291 THEN POP_ASSUM 292 (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th)))) 293 THEN PROVE_TAC[] 294 ); 295 296val LIST_QUOTIENT = store_thm 297 ("LIST_QUOTIENT", 298 (--`!R (abs:'a -> 'b). QUOTIENT R abs ==> 299 QUOTIENT (LIST_REL R) (MAP abs)`--), 300 REPEAT STRIP_TAC 301 THEN REWRITE_TAC[QUOTIENT_def] 302 THEN REPEAT CONJ_TAC 303 THENL (* 2 subgoals *) 304 [ IMP_RES_TAC QUOTIENT_REP 305 THEN Induct 306 THEN PROVE_TAC[MAP,LIST_REL_def], 307 308 Induct 309 THENL [ ALL_TAC, GEN_TAC ] 310 THEN Cases 311 THEN ONCE_REWRITE_TAC[LIST_REL_def] 312 THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS] 313 THEN REWRITE_TAC[CONS_11] 314 THEN IMP_RES_THEN 315 (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th)))) 316 QUOTIENT_REL 317 THEN IMP_RES_THEN 318 (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th)))) 319 LIST_REL_REL 320 THEN PROVE_TAC[] 321 ] 322 ); 323 324 325(* for OPTION_ABS or OPTION_REP, use OPTION_MAP abs or OPTION_MAP rep, 326 as defined in theory "option". *) 327 328val OPTION_MAP_I = store_thm 329 ("OPTION_MAP_I", 330 (--`OPTION_MAP I = (I : 'a option -> 'a option)`--), 331 CONV_TAC FUN_EQ_CONV 332 THEN Cases 333 THEN REWRITE_TAC[OPTION_MAP_DEF,I_THM] 334 ); 335 336(* Here is the definition of OPTION_REL: *) 337 338val OPTION_REL_def = 339 Define 340 `(OPTION_REL R (NONE) (NONE) = T) /\ 341 (OPTION_REL R (SOME (x:'a)) (NONE) = F) /\ 342 (OPTION_REL R (NONE) (SOME (y:'a)) = F) /\ 343 (OPTION_REL R (SOME (x:'a)) (SOME (y:'a)) = R x y)`; 344 345val OPTION_REL_EQ = store_thm 346 ("OPTION_REL_EQ", 347 (--`(OPTION_REL ($= : 'a->'a->bool)) = $=`--), 348 CONV_TAC FUN_EQ_CONV 349 THEN CONV_TAC (RAND_CONV (ABS_CONV FUN_EQ_CONV)) 350 THEN Cases 351 THEN Cases 352 THEN REWRITE_TAC[OPTION_REL_def,option_CLAUSES] 353 ); 354 355val OPTION_EQUIV = store_thm 356 ("OPTION_EQUIV", 357 (--`!R. (!x y:'a. R x y = (R x = R y)) ==> 358 (!x y. OPTION_REL R x y = (OPTION_REL R x = OPTION_REL R y))`--), 359 GEN_TAC 360 THEN DISCH_TAC 361 THEN Cases 362 THEN Cases (* 4 subgoals *) 363 THEN ASM_REWRITE_TAC[OPTION_REL_def] 364 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 365 THENL 366 [ DISCH_THEN (MP_TAC o SPEC ``NONE :'a option``) 367 THEN ASM_REWRITE_TAC[OPTION_REL_def], 368 369 DISCH_THEN (MP_TAC o SPEC ``NONE :'a option``) 370 THEN ASM_REWRITE_TAC[OPTION_REL_def], 371 372 EQ_TAC 373 THENL 374 [ STRIP_TAC 375 THEN Cases 376 THEN ASM_REWRITE_TAC[OPTION_REL_def], 377 378 DISCH_THEN (MP_TAC o SPEC ``SOME x :'a option``) 379 THEN ASM_REWRITE_TAC[OPTION_REL_def] 380 ] 381 ] 382 ); 383 384val OPTION_QUOTIENT = store_thm 385 ("OPTION_QUOTIENT", 386 (--`!R (abs:'a -> 'b). QUOTIENT R abs ==> 387 QUOTIENT (OPTION_REL R) (OPTION_MAP abs)`--), 388 REPEAT GEN_TAC 389 THEN STRIP_TAC 390 THEN REWRITE_TAC[QUOTIENT_def] 391 THEN IMP_RES_TAC QUOTIENT_REP 392 THEN CONJ_TAC 393 THENL 394 [ Cases 395 THENL 396 [ EXISTS_TAC (--`NONE:'a option`--) 397 THEN REWRITE_TAC[OPTION_MAP_DEF,OPTION_REL_def,option_CLAUSES], 398 399 POP_ASSUM (STRIP_ASSUME_TAC o SPEC (--`x:'b`--)) 400 THEN EXISTS_TAC (--`SOME r:'a option`--) 401 THEN ASM_REWRITE_TAC[OPTION_MAP_DEF,OPTION_REL_def,option_CLAUSES] 402 ], 403 404 REPEAT Cases 405 THEN ASM_REWRITE_TAC[OPTION_MAP_DEF,OPTION_REL_def,option_CLAUSES] 406 THEN IMP_RES_THEN (fn th => CONV_TAC (LAND_CONV (REWR_CONV th))) 407 QUOTIENT_REL 408 THEN REFL_TAC 409 ] 410 ); 411 412 413(* to create PROD (i.e., PAIR) ABS and REP functions, use infix ## *) 414(* See PAIR_MAP_THM, PAIR_MAP. *) 415 416val PAIR_MAP_I = store_thm 417 ("PAIR_MAP_I", 418 (--`(I ## I) = (I : 'a # 'b -> 'a # 'b)`--), 419 CONV_TAC FUN_EQ_CONV 420 THEN Cases 421 THEN REWRITE_TAC[PAIR_MAP_THM,I_THM] 422 ); 423 424(* just like RPROD_DEF, except infix: *) 425 426val PAIR_REL = 427 new_infixr_definition 428 ("PAIR_REL", 429 (--`$### R1 R2 = \(a:'a,b:'b) (c:'c,d:'d). R1 a c /\ R2 b d`--), 430 450); 431 432val PAIR_REL_THM = store_thm 433 ("PAIR_REL_THM", 434 (--`!R1 R2 (a:'a) (b:'b) (c:'c) (d:'d). 435 (R1 ### R2) (a,b) (c,d) = R1 a c /\ R2 b d`--), 436 REPEAT GEN_TAC 437 THEN PURE_ONCE_REWRITE_TAC[PAIR_REL] 438 THEN GEN_BETA_TAC 439 THEN REFL_TAC 440 ); 441 442val PAIR_REL_EQ = store_thm 443 ("PAIR_REL_EQ", 444 (--`($= ### $=) = ($= : 'a # 'b -> 'a # 'b -> bool)`--), 445 CONV_TAC FUN_EQ_CONV 446 THEN Cases 447 THEN CONV_TAC FUN_EQ_CONV 448 THEN Cases 449 THEN REWRITE_TAC[PAIR_REL_THM,PAIR_EQ] 450 ); 451 452val PAIR_REL_REFL = store_thm 453 ("PAIR_REL_REFL", 454 (--`!R1 R2. (!x y:'a. R1 x y = (R1 x = R1 y)) /\ 455 (!x y:'b. R2 x y = (R2 x = R2 y)) ==> 456 !x. (R1 ### R2) x x`--), 457 REPEAT GEN_TAC 458 THEN STRIP_TAC 459 THEN Cases 460 THEN REWRITE_TAC[PAIR_REL_THM] 461 THEN ASM_REWRITE_TAC[] 462 ); 463 464val PAIR_EQUIV = store_thm 465 ("PAIR_EQUIV", 466 (--`!R1 R2. (!x y:'a. R1 x y = (R1 x = R1 y)) ==> 467 (!x y:'b. R2 x y = (R2 x = R2 y)) ==> 468 (!x y. (R1 ### R2) x y = ((R1 ### R2) x = (R1 ### R2) y))`--), 469 REPEAT GEN_TAC 470 THEN REPEAT DISCH_TAC 471 THEN Cases 472 THEN Cases 473 THEN REWRITE_TAC[PAIR_REL_THM] 474 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 475 THEN EQ_TAC 476 THENL 477 [ STRIP_TAC 478 THEN Cases 479 THEN REWRITE_TAC[PAIR_REL_THM] 480 THEN PROVE_TAC[], 481 482 DISCH_THEN (MP_TAC o GEN ``a:'a`` o GEN ``b:'b`` 483 o SPEC ``(a:'a, b:'b)``) 484 THEN REWRITE_TAC[PAIR_REL_THM] 485 THEN IMP_RES_TAC PAIR_REL_REFL 486 THEN PROVE_TAC[] 487 ] 488 ); 489 490val PAIR_QUOTIENT = store_thm 491 ("PAIR_QUOTIENT", 492 (--`!R1 (abs1:'a -> 'c). QUOTIENT R1 abs1 ==> 493 !R2 (abs2:'b -> 'd). QUOTIENT R2 abs2 ==> 494 QUOTIENT (R1 ### R2) (abs1 ## abs2)`--), 495 REPEAT STRIP_TAC 496 THEN REWRITE_TAC[QUOTIENT_def] 497 THEN CONJ_TAC 498 THENL 499 [ Cases 500 THEN IMP_RES_TAC QUOTIENT_REP 501 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``q:'c``) 502 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``r:'d``) 503 THEN EXISTS_TAC ``(r':'a,r'':'b)`` 504 THEN ASM_REWRITE_TAC[PAIR_MAP,PAIR_REL_THM,PAIR_EQ], 505 506 REPEAT Cases 507 THEN REWRITE_TAC[PAIR_REL_THM,PAIR_MAP_THM,PAIR_EQ] 508 THEN IMP_RES_THEN 509 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th]))) 510 QUOTIENT_REL 511 THEN PROVE_TAC[] 512 ] 513 ); 514 515 516 517(* for SUM of ABS / REP functions, use infix ++, defined here: *) 518 519val _ = Lib.try add_infix("++", 450, HOLgrammars.RIGHT) 520 521val SUM_MAP_def = xDefine "SUM_MAP" 522 `(($++ f g) (INL (a:'a)) = INL ((f a):'c)) /\ 523 (($++ f g) (INR (b:'b)) = INR ((g b):'d))`; 524 525val SUM_MAP = store_thm 526 ("SUM_MAP", 527 (--`!f g (z:'a + 'b). 528 (f ++ g) z = (if ISL z then INL (f (OUTL z)) 529 else INR (g (OUTR z))) :'c + 'd`--), 530 GEN_TAC 531 THEN GEN_TAC 532 THEN Cases 533 THEN REWRITE_TAC[SUM_MAP_def,ISL,OUTL,OUTR] 534 ); 535 536val SUM_MAP_CASE = store_thm 537 ("SUM_MAP_CASE", 538 (--`!f g (z:'a + 'b). 539 (f ++ g) z = sum_case (INL o f) (INR o g) z :'c + 'd`--), 540 GEN_TAC 541 THEN GEN_TAC 542 THEN Cases 543 THEN REWRITE_TAC[SUM_MAP_def,sum_case_def,o_THM] 544 ); 545 546val SUM_MAP_I = store_thm 547 ("SUM_MAP_I", 548 (--`(I ++ I) = (I : 'a + 'b -> 'a + 'b)`--), 549 CONV_TAC FUN_EQ_CONV 550 THEN Cases 551 THEN REWRITE_TAC[SUM_MAP_def,I_THM] 552 ); 553 554(* for SUM of equivalence relations, use infix +++, defined here: *) 555 556val _ = Lib.try add_infix("+++", 450, HOLgrammars.RIGHT) 557 558val SUM_REL_def = xDefine "SUM_REL" 559 `(($+++ R1 R2) (INL (a1:'a)) (INL (a2:'a)) = R1 a1 a2) /\ 560 (($+++ R1 R2) (INR (b1:'b)) (INR (b2:'b)) = R2 b1 b2) /\ 561 (($+++ R1 R2) (INL a1) (INR b2) = F) /\ 562 (($+++ R1 R2) (INR b1) (INL a2) = F)`; 563 564val SUM_REL_EQ = store_thm 565 ("SUM_REL_EQ", 566 (--`($= +++ $=) = ($= : 'a + 'b -> 'a + 'b -> bool)`--), 567 CONV_TAC FUN_EQ_CONV 568 THEN Cases 569 THEN CONV_TAC FUN_EQ_CONV 570 THEN Cases 571 THEN REWRITE_TAC[SUM_REL_def,INR_INL_11,sum_distinct,sum_distinct1] 572 ); 573 574val SUM_EQUIV = store_thm 575 ("SUM_EQUIV", 576 (--`!R1 R2. (!x y:'a. R1 x y = (R1 x = R1 y)) ==> 577 (!x y:'b. R2 x y = (R2 x = R2 y)) ==> 578 (!x y. (R1 +++ R2) x y = ((R1 +++ R2) x = (R1 +++ R2) y))`--), 579 REPEAT GEN_TAC 580 THEN REPEAT DISCH_TAC 581 THEN Cases 582 THEN Cases (* 4 subgoals *) 583 THEN ASM_REWRITE_TAC[SUM_REL_def] 584 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 585 THENL 586 [ EQ_TAC 587 THENL 588 [ STRIP_TAC 589 THEN Cases 590 THEN ASM_REWRITE_TAC[SUM_REL_def], 591 592 DISCH_THEN (MP_TAC o SPEC ``INL x :'a + 'b``) 593 THEN ASM_REWRITE_TAC[SUM_REL_def] 594 ], 595 596 DISCH_THEN (MP_TAC o SPEC ``INL x' :'a + 'b``) 597 THEN ASM_REWRITE_TAC[SUM_REL_def], 598 599 DISCH_THEN (MP_TAC o SPEC ``INR y :'a + 'b``) 600 THEN ASM_REWRITE_TAC[SUM_REL_def], 601 602 EQ_TAC 603 THENL 604 [ STRIP_TAC 605 THEN Cases 606 THEN ASM_REWRITE_TAC[SUM_REL_def], 607 608 DISCH_THEN (MP_TAC o SPEC ``INR y'' :'a + 'b``) 609 THEN ASM_REWRITE_TAC[SUM_REL_def] 610 ] 611 ] 612 ); 613 614val SUM_QUOTIENT = store_thm 615 ("SUM_QUOTIENT", 616 (--`!R1 (abs1:'a -> 'c). QUOTIENT R1 abs1 ==> 617 !R2 (abs2:'b -> 'd). QUOTIENT R2 abs2 ==> 618 QUOTIENT (R1 +++ R2) (abs1 ++ abs2)`--), 619 REPEAT STRIP_TAC 620 THEN REWRITE_TAC[QUOTIENT_def] 621 THEN CONJ_TAC 622 THENL 623 [ IMP_RES_TAC QUOTIENT_REP 624 THEN Cases 625 THENL 626 [ FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``x:'c``) 627 THEN EXISTS_TAC ``INL r : 'a + 'b``, 628 629 FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``y:'d``) 630 THEN EXISTS_TAC ``INR r : 'a + 'b`` 631 ] 632 THEN ASM_REWRITE_TAC[SUM_REL_def,SUM_MAP_def], 633 634 REPEAT Cases 635 THEN REWRITE_TAC[SUM_REL_def,SUM_MAP_def] 636 THEN REWRITE_TAC[INR_INL_11,sum_distinct,GSYM sum_distinct] 637 THEN IMP_RES_THEN 638 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th]))) 639 QUOTIENT_REL 640 THEN REFL_TAC 641 ] 642 ); 643 644 645 646(* FUNCTIONS: *) 647 648val IMAGE_I = store_thm 649 ("IMAGE_I", 650 (--`(IMAGE (I:'a->'a)) = I`--), 651 ONCE_REWRITE_TAC[FUN_EQ_THM] 652 THEN REWRITE_TAC[EXTENSION] 653 THEN REWRITE_TAC[IN_IMAGE,I_THM] 654 THEN REPEAT GEN_TAC 655 THEN EQ_TAC 656 THEN STRIP_TAC 657 THEN TRY (EXISTS_TAC ``x':'a``) 658 THEN ASM_REWRITE_TAC[] 659 ); 660 661val EQ_SING = store_thm 662 ("EQ_SING", 663 (--`!x. $= (x:'a) = {x}`--), 664 REWRITE_TAC[EXTENSION,IN_SING] 665 THEN REWRITE_TAC[SPECIFICATION] 666 THEN MATCH_ACCEPT_TAC EQ_SYM_EQ 667 ); 668 669val IMAGE_SING = store_thm 670 ("IMAGE_SING", 671 (--`!(f:'a->'b) x. IMAGE f {x} = {f x}`--), 672 REWRITE_TAC[EXTENSION,IN_IMAGE,IN_SING] 673 THEN REPEAT GEN_TAC 674 THEN EQ_TAC 675 THEN STRIP_TAC 676 THEN TRY (EXISTS_TAC ``x:'a``) 677 THEN ASM_REWRITE_TAC[] 678 ); 679 680val SELECT1_EXISTS = TAC_PROOF(([], 681 (--`?f. !P. !(x:'a). P x ==> (!y. P y ==> (x = y)) ==> P (f P)`--)), 682 EXISTS_TAC ``$@ :('a -> bool) -> 'a`` 683 THEN REPEAT STRIP_TAC 684 THEN IMP_RES_TAC SELECT_AX 685 ); 686 687local 688open Rsyntax 689in 690val SELECT1_DEF = 691 new_specification 692 {name = "SELECT1_DEF", 693 consts = [{const_name = "@!", fixity = Binder}], 694 sat_thm = SELECT1_EXISTS} 695 696val _ = Parse.add_binder("@!", 0) 697end; 698 699val SELECT1_SING = store_thm 700 ("SELECT1_SING", 701 (--`!x:'a. $@! {x} = x`--), 702 GEN_TAC 703 THEN MP_TAC (SPEC ``x:'a`` (ISPEC ``$= (x:'a)`` SELECT1_DEF)) 704 THEN REWRITE_TAC[GSYM EQ_SING] 705 THEN DISCH_THEN (REWRITE_THM o GSYM) 706 ); 707 708val THE_LEAST_NUM_IS_ZERO = TAC_PROOF(([], 709 (--`(@!n. !m. n <= m) = 0`--)), 710 MP_TAC (SPEC ``0`` (ISPEC ``\n. !m. n <= m`` SELECT1_DEF)) 711 THEN BETA_TAC 712 THEN CONV_TAC (DEPTH_CONV RIGHT_IMP_FORALL_CONV) 713 THEN DISCH_THEN (MP_TAC o SPEC ``0``) 714 THEN REWRITE_TAC[arithmeticTheory.LESS_EQ_0, AND_IMP_INTRO] 715 THEN DISCH_THEN MATCH_MP_TAC 716 THEN REWRITE_TAC[arithmeticTheory.ZERO_LESS_EQ] 717 THEN Cases 718 THEN REWRITE_TAC[] 719 THEN DISCH_THEN (MP_TAC o SPEC ``0``) 720 THEN REWRITE_TAC[arithmeticTheory.NOT_SUC_LESS_EQ_0] 721 ); 722 723(* version using skolemization, which secretly involves @: 724 725val CONTENTS_EXISTS1 = TAC_PROOF(([], 726 (--`!P. ?e. !(x:'a). P x ==> (!y. P y ==> (x = y)) ==> P e`--)), 727 GEN_TAC 728 THEN ASM_CASES_TAC ``?z:'a. P z`` 729 THENL 730 [ POP_ASSUM STRIP_ASSUME_TAC 731 THEN EXISTS_TAC ``z:'a`` 732 THEN ASM_REWRITE_TAC[], 733 734 POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) 735 THEN ASM_REWRITE_TAC[] 736 ] 737 ); 738 739val CONTENTS_EXISTS = CONV_RULE SKOLEM_CONV CONTENTS_EXISTS1; 740 741val CONTENTS_DEF = 742 new_specification 743 {name = "CONTENTS_DEF", 744 consts = [{const_name = "CONTENTS", fixity = Prefix}], 745 sat_thm = CONTENTS_EXISTS}; 746 747*) 748 749(* for ABS of functions, 750 use ((abs1 // R1) --> abs2) *) 751 752val _ = hide "//"; 753 754val FUN_REP = 755 new_infixr_definition 756 ("FUN_REP", 757 (--`$// (f:'a->'b) R = 758 \a r. R r r /\ (f r = a)`--), 759 450); 760 761val FUN_REP_THM = store_thm 762 ("FUN_REP_THM", 763 (--`!(f:'a -> 'b) R a r. 764 (f // R) a r = R r r /\ (f r = a)`--), 765 REPEAT GEN_TAC 766 THEN PURE_ONCE_REWRITE_TAC[FUN_REP] 767 THEN BETA_TAC 768 THEN REFL_TAC 769 ); 770 771val FUN_REP_ELEM = store_thm 772 ("FUN_REP_ELEM", 773 (--`!(f:'a -> 'b) R r. 774 r IN (f // R) (f r) = R r r`--), 775 REPEAT GEN_TAC 776 THEN REWRITE_TAC[SPECIFICATION,FUN_REP_THM] 777 ); 778 779val FUN_REP_IDENTITY = store_thm 780 ("FUN_REP_IDENTITY", 781 (--`(I:'a->'a // $=) = $=`--), 782 REWRITE_TAC[FUN_EQ_THM,FUN_REP_THM,I_THM] 783 THEN MATCH_ACCEPT_TAC EQ_SYM_EQ 784 ); 785 786val _ = hide "-->"; 787 788val FUN_MAP = 789 new_infixr_definition 790 ("FUN_MAP", 791 (--`$--> (rep:'c->'a->bool) (abs:'b->'d) = 792 \h x. $@! (IMAGE abs (IMAGE h (rep x)))`--), 793 450); 794 795 796val FUN_MAP_THM = store_thm 797 ("FUN_MAP_THM", 798 (--`!(rep:'c -> 'a -> bool) (abs:'b -> 'd) h x. 799 (rep --> abs) h x = $@! (IMAGE abs (IMAGE h (rep x)))`--), 800 REPEAT GEN_TAC 801 THEN PURE_ONCE_REWRITE_TAC[FUN_MAP] 802 THEN BETA_TAC 803 THEN REFL_TAC 804 ); 805 806val FUN_MAP_EQ_I = store_thm 807 ("FUN_MAP_EQ_I", 808 (--`(($= :'a->'a->bool) --> (I:'b->'b)) = I`--), 809 REPEAT (CONV_TAC FUN_EQ_CONV ORELSE GEN_TAC) 810 THEN REWRITE_TAC[FUN_MAP_THM] 811 THEN REWRITE_TAC[IMAGE_I,I_THM] 812 THEN REWRITE_TAC[EQ_SING,IMAGE_SING,SELECT1_SING] 813 THEN ONCE_REWRITE_TAC[GSYM SPECIFICATION] 814 THEN REWRITE_TAC[IN_SING] 815 ); 816 817 818 819(* The strong version of FUN_REL: *) 820 821val FUN_REL = 822 new_infixr_definition 823 ("FUN_REL", 824 (--`$===> (R1:'a->'a->bool) (R2:'b->'b->bool) f g = 825 !x y. R1 x y ==> R2 (f x) (g y)`--), 826 450); 827 828(* NOTE: R1 ===> R2 is NOT an equivalence relation, but a partial 829 equivalence relation, and it does satisfy a quotient theorem. *) 830 831 832val FUN_REL_EQ = store_thm 833 ("FUN_REL_EQ", 834 (--`(($= :'a -> 'a -> bool) ===> ($= :'b -> 'b -> bool)) = $=`--), 835 CONV_TAC FUN_EQ_CONV 836 THEN GEN_TAC 837 THEN CONV_TAC FUN_EQ_CONV 838 THEN GEN_TAC 839 THEN PURE_ONCE_REWRITE_TAC[FUN_REL] 840 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 841 THEN PROVE_TAC[] 842 ); 843 844val IMAGE_o = store_thm 845 ("IMAGE_o", 846 (--`!(f:'b->'c) g (s:'a -> bool). 847 IMAGE f (IMAGE g s) = IMAGE (f o g) s`--), 848 REWRITE_TAC[EXTENSION] 849 THEN REPEAT GEN_TAC 850 THEN REWRITE_TAC[IN_IMAGE,o_THM] 851 THEN PROVE_TAC[] 852 ); 853 854val SELECT1_IMAGE = store_thm 855 ("SELECT1_IMAGE", 856 (--`!(f:'a->'b) s x. 857 x IN s ==> 858 (!x y. x IN s /\ y IN s ==> (f x = f y)) ==> 859 ($@! (IMAGE f s) = f x)`--), 860 REPEAT STRIP_TAC 861 THEN MP_TAC (SPEC ``(f:'a->'b) x`` 862 (ISPEC ``IMAGE (f:'a->'b) s`` SELECT1_DEF)) 863 THEN REWRITE_TAC[REWRITE_RULE[SPECIFICATION] IN_IMAGE] 864 THEN SUBGOAL_THEN ``?x'. ((f:'a->'b) x = f x') /\ s x'`` REWRITE_THM 865 THENL 866 [ EXISTS_TAC ``x:'a`` 867 THEN REWRITE_TAC[] 868 THEN ASM_REWRITE_TAC[GSYM SPECIFICATION], 869 870 ALL_TAC 871 ] 872 THEN SUBGOAL_THEN ``!y:'b. (?x:'a. (y = f x) /\ s x) ==> (f x = y)`` 873 REWRITE_THM 874 (* 2 subgoals, which are both solved by the following tactic: *) 875 THEN REPEAT GEN_TAC 876 THEN STRIP_TAC 877 THEN ASM_REWRITE_TAC[] 878 THEN FIRST_ASSUM MATCH_MP_TAC 879 THEN ASM_REWRITE_TAC[] 880 THEN ASM_REWRITE_TAC[SPECIFICATION] 881 ); 882 883 884val FUN_REP_MAP = store_thm 885 ("FUN_REP_MAP", 886 (--`!R1 (abs1:'a -> 'c) R2 (abs2:'b -> 'd) a r. 887 QUOTIENT R1 abs1 ==> 888 QUOTIENT R2 abs2 ==> 889 (((R1 ===> R2) r r /\ (((abs1 // R1) --> abs2) r = a)) = 890 (!x. R1 x x ==> (abs2 // R2) (a (abs1 x)) (r x)) )`--), 891 REPEAT GEN_TAC 892 THEN DISCH_TAC 893 THEN DISCH_TAC 894 THEN REWRITE_TAC[FUN_EQ_THM] 895 THEN REWRITE_TAC[FUN_REL,FUN_REP_THM,FUN_MAP_THM] 896 THEN EQ_TAC 897 THEN REPEAT STRIP_TAC 898 THENL 899 [ FIRST_ASSUM MATCH_MP_TAC 900 THEN FIRST_ASSUM ACCEPT_TAC, 901 902 EVERY_ASSUM (ONCE_REWRITE_THM o GSYM) 903 THEN REWRITE_TAC[IMAGE_o] 904 THEN IMP_RES_THEN (ASSUME_TAC o ISPEC ``abs1:'a -> 'c``) FUN_REP_ELEM 905 THEN IMP_RES_THEN (fn th => DEP_REWRITE_TAC[th]) SELECT1_IMAGE 906 THEN REWRITE_TAC[o_THM] 907 THEN REWRITE_TAC[SPECIFICATION,FUN_REP_THM] 908 THEN REPEAT STRIP_TAC 909 THEN IMP_RES_THEN (fn th => TRY (MATCH_MP_TAC th)) QUOTIENT_REL_ABS 910 THEN FIRST_ASSUM MATCH_MP_TAC 911 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 912 THEN ASM_REWRITE_TAC[], 913 914 POP_ASSUM MP_TAC 915 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 916 THEN REPEAT STRIP_TAC 917 THEN RES_TAC 918 THEN ASM_REWRITE_TAC[], 919 920 REWRITE_TAC[IMAGE_o] 921 THEN IMP_RES_TAC QUOTIENT_REP 922 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``x:'c``) 923 THEN POP_ASSUM (REWRITE_THM o SYM) 924 THEN IMP_RES_THEN (ASSUME_TAC o ISPEC ``abs1:'a -> 'c``) FUN_REP_ELEM 925 THEN IMP_RES_THEN (fn th => DEP_REWRITE_TAC[th]) SELECT1_IMAGE 926 THEN RES_TAC 927 THEN ASM_REWRITE_TAC[o_THM] 928 THEN REWRITE_TAC[SPECIFICATION,FUN_REP_THM] 929 THEN REPEAT STRIP_TAC 930 THEN IMP_RES_THEN (fn th => TRY (MATCH_MP_TAC th)) QUOTIENT_REL_ABS 931 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 932 THEN RES_TAC 933 THEN ASM_REWRITE_TAC[] 934 ] 935 ); 936 937 938 939val FUN_QUOTIENT = store_thm 940 ("FUN_QUOTIENT", 941 (--`!R1 (abs1:'a -> 'c). QUOTIENT R1 abs1 ==> 942 !R2 (abs2:'b -> 'd). QUOTIENT R2 abs2 ==> 943 QUOTIENT (R1 ===> R2) ((abs1 // R1) --> abs2)`--), 944 REPEAT STRIP_TAC 945 THEN REWRITE_TAC[QUOTIENT_def] 946 THEN CONJ_TAC 947 THENL (* 2 subgoals *) 948 [ 949 950 GEN_TAC 951 THEN IMP_RES_THEN MP_TAC QUOTIENT_REP 952(* WARNING!!! The next line uses the AXIOM OF CHOICE!!! *) 953 THEN CONV_TAC (ONCE_DEPTH_CONV SKOLEM_CONV) 954 THEN REPEAT STRIP_TAC 955 THEN EXISTS_TAC ``(r':'d->'b) o a o (abs1:'a->'c)`` 956 THEN REWRITE_TAC[FUN_EQ_THM] 957 THEN ASM_REWRITE_TAC[FUN_REL,FUN_MAP_THM,FUN_REP_THM,o_THM] 958 THEN CONJ_TAC 959 THENL 960 [ IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 961 THEN REPEAT GEN_TAC 962 THEN STRIP_TAC 963 THEN ASM_REWRITE_TAC[], 964 965 GEN_TAC 966 THEN REWRITE_TAC[IMAGE_o] 967 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``x:'c``) 968 THEN IMP_RES_THEN (MP_TAC o ISPEC ``abs1:'a -> 'c``) FUN_REP_ELEM 969 THEN ASM_REWRITE_TAC[] 970 THEN DISCH_TAC 971 THEN IMP_RES_THEN (fn th => DEP_REWRITE_TAC[th]) SELECT1_IMAGE 972 THEN ASM_REWRITE_TAC[o_THM] 973 THEN REWRITE_TAC[SPECIFICATION,FUN_REP_THM] 974 THEN REPEAT STRIP_TAC 975 THEN ASM_REWRITE_TAC[] 976 ], 977 978 REPEAT GEN_TAC 979 THEN CONV_TAC (RAND_CONV (RAND_CONV (RAND_CONV FUN_EQ_CONV))) 980 THEN REWRITE_TAC[FUN_REL] 981 THEN EQ_TAC 982 THEN REPEAT STRIP_TAC 983 THENL (* 4 subgoals *) 984 [ PROVE_TAC[QUOTIENT_REL], 985 986 PROVE_TAC[QUOTIENT_REL], 987 988 REWRITE_TAC[FUN_MAP_THM] 989 THEN AP_TERM_TAC 990 THEN REWRITE_TAC[IMAGE_o] 991 THEN REWRITE_TAC[EXTENSION,IN_IMAGE] 992 THEN REWRITE_TAC[SPECIFICATION,FUN_REP_THM] 993 THEN X_GEN_TAC ``y:'d`` 994 THEN REWRITE_TAC[o_THM] 995 THEN EQ_TAC 996 THEN STRIP_TAC 997 THEN PROVE_TAC[QUOTIENT_REL], 998 999 POP_ASSUM MP_TAC 1000 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 1001 THEN POP_ASSUM MP_TAC 1002 THEN REWRITE_TAC[FUN_MAP_THM,IMAGE_o] 1003 THEN STRIP_TAC 1004 THEN STRIP_TAC 1005 THEN RES_THEN REWRITE_THM 1006 THEN FIRST_ASSUM (MP_TAC o SPEC ``(abs1:'a -> 'c) x``) 1007 THEN IMP_RES_THEN (ASSUME_TAC o ISPEC ``abs1:'a->'c``) FUN_REP_ELEM 1008 THEN IMP_RES_THEN (fn th => DEP_REWRITE_TAC[th]) SELECT1_IMAGE 1009 THEN REWRITE_TAC[o_THM,SPECIFICATION,FUN_REP_THM] 1010 THEN REPEAT STRIP_TAC 1011 THEN ASM_REWRITE_TAC[] 1012 THEN IMP_RES_THEN (fn th => TRY (MATCH_MP_TAC th)) QUOTIENT_REL_ABS 1013 THEN FIRST_ASSUM MATCH_MP_TAC 1014 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL 1015 THEN ASM_REWRITE_TAC[] 1016 ] 1017 ] 1018 ); 1019 1020 1021 1022val ABSTRACTION_QUOTIENT = store_thm 1023 ("ABSTRACTION_QUOTIENT", 1024 (--`!f:'a->'b. ONTO f ==> QUOTIENT (\r s. f r = f s) f`--), 1025 GEN_TAC 1026 THEN REWRITE_TAC[ONTO_DEF,QUOTIENT_def] 1027 THEN BETA_TAC 1028 THEN REWRITE_TAC[] 1029 THEN REPEAT STRIP_TAC 1030 THEN FIRST_ASSUM (STRIP_ASSUME_TAC o SPEC ``a:'b``) 1031 THEN EXISTS_TAC ``x:'a`` 1032 THEN FIRST_ASSUM (ACCEPT_TAC o SYM) 1033 ); 1034 1035val PARTIAL_ABSTRACTION_QUOTIENT = store_thm 1036 ("PARTIAL_ABSTRACTION_QUOTIENT", 1037 (--`!(f:'a->'b) P. 1038 (!a. ?r. P r /\ (f r = a)) ==> 1039 QUOTIENT (\r s. P r /\ P s /\ (f r = f s)) f`--), 1040 REPEAT GEN_TAC 1041 THEN REWRITE_TAC[ONTO_DEF,QUOTIENT_def] 1042 THEN BETA_TAC 1043 THEN REWRITE_TAC[] 1044 ); 1045 1046local 1047 val ith = INST_TYPE [alpha |-> delta] IDENTITY_QUOTIENT 1048 val f_ = ``f:'b -> 'd`` 1049 val ath = UNDISCH (ISPEC f_ ABSTRACTION_QUOTIENT) 1050 val fth = MATCH_MP (MATCH_MP FUN_QUOTIENT ith) ath 1051 val eth = SPEC ``I:'d->'d`` (MATCH_MP QUOTIENT_REP fth) 1052 val th1 = BETA_RULE (REWRITE_RULE[FUN_REL,FUN_REP_IDENTITY,FUN_MAP] eth) 1053 val th2 = REWRITE_RULE [GSYM EQ_SING] (REWRITE_RULE[EQ_SING,IMAGE_SING,SELECT1_SING] th1) 1054in 1055 val ONTO_FUN_EXISTS_CHOICE = GEN_ALL (DISCH_ALL th2) 1056end; 1057 1058val ONTO_FUNCTION_INVERSE = store_thm 1059 ("ONTO_FUNCTION_INVERSE", 1060 (--`!(f :'a -> 'b). ONTO f ==> ?g. f o g = I`--), 1061 REPEAT STRIP_TAC 1062 THEN IMP_RES_TAC ONTO_FUN_EXISTS_CHOICE 1063 THEN POP_ASSUM MP_TAC 1064 THEN REWRITE_TAC[FUN_EQ_THM,o_THM,I_THM] 1065 THEN BETA_TAC 1066 THEN DISCH_TAC 1067 THEN EXISTS_TAC ``r:'b -> 'a`` 1068 THEN FIRST_ASSUM ACCEPT_TAC 1069 ); 1070 1071(* 1072 ONTO_FUNCTION_INVERSE: |- !f. ONTO f ==> ?g. f o g = I 1073*) 1074 1075val ONTO_PARTIAL_FUNCTION = store_thm 1076 ("ONTO_PARTIAL_FUNCTION", 1077 (--`!Q. ?(P,a:'a). (P = Q) /\ ((?x. P x) ==> P a)`--), 1078 GEN_TAC 1079 THEN ASM_CASES_TAC ``?x:'a. Q x`` 1080 THEN POP_ASSUM STRIP_ASSUME_TAC 1081 THEN PairRules.PEXISTS_TAC ``(Q:'a->bool, x:'a)`` 1082 THEN ASM_REWRITE_TAC[] 1083 ); 1084 1085val ONTO_PARTIAL_FUNCTION1 = store_thm 1086 ("ONTO_PARTIAL_FUNCTION1", 1087 (--`!Q. ?p. ((?x:'a. FST p x) ==> FST p (SND p)) /\ (FST p = Q)`--), 1088 GEN_TAC 1089 THEN PairRules.PSTRIP_ASSUME_TAC (SPEC_ALL ONTO_PARTIAL_FUNCTION) 1090 THEN PairRules.PEXISTS_TAC ``(P:'a -> bool, a:'a)`` 1091 THEN REWRITE_TAC[FST,SND] 1092 THEN CONJ_TAC 1093 THEN FIRST_ASSUM ACCEPT_TAC 1094 ); 1095 1096local 1097 val ith = INST_TYPE [alpha |-> (alpha --> bool)] IDENTITY_QUOTIENT 1098 val f1 = ``FST:(('a -> bool) # 'a) -> ('a -> bool)`` 1099 val Q1 = ``\(P,a). (?x:'a. P x) ==> P a`` 1100 val ath = ISPECL [f1,Q1] PARTIAL_ABSTRACTION_QUOTIENT 1101 val bth = MP (PairRules.PBETA_RULE ath) ONTO_PARTIAL_FUNCTION1 1102 val fth = MATCH_MP (MATCH_MP FUN_QUOTIENT ith) bth 1103 val i1 = ``I:('a -> bool) -> ('a -> bool)`` 1104 val eth = SPEC i1 (MATCH_MP QUOTIENT_REP fth) 1105 val th1 = PairRules.PBETA_RULE 1106 (REWRITE_RULE[FUN_REL,FUN_REP_IDENTITY,FUN_MAP] eth) 1107 val th2 = REWRITE_RULE [GSYM EQ_SING] 1108 (REWRITE_RULE[EQ_SING,IMAGE_SING,SELECT1_SING] th1) 1109in 1110 val CHOICE_FUN_PAIR_EXISTS = th2 1111end; 1112 1113 1114 1115(* 1116option_case_def: 1117 |- (!u f. case u f NONE = u) /\ !u f x. case u f (SOME x) = f x 1118 1119 1120SPEC ``I:bool->bool`` 1121 (MATCH_MP QUOTIENT_REP_EXISTS 1122 (MATCH_MP 1123 (MATCH_MP FUN_QUOTIENT (INST_TYPE [alpha |-> bool] IDENTITY_QUOTIENT)) 1124 (UNDISCH (ISPEC ``P:'a -> bool`` ABSTRACTION_QUOTIENT)))) 1125 1126 1127By QUOTIENT ($= :bool->bool->bool) (I:bool->bool) ($= :bool->bool->bool) 1128(IDENTITY_QUOTIENT, the identity quotient on booleans), and 1129by QUOTIENT (\r s:'a. P r = P s) (P:'a -> bool) (\(a:bool) (r:'a). P r = a) 1130as assumptions to the FUN_QUOTIENT, we have 1131QUOTIENT ($= ===> (\r s:'a. P r = P s)) 1132 (I --> P) 1133 (($= >-- (\ (a:bool) (r:'a). P r = a)) $=) 1134from which by QUOTIENT_REP_EXISTS, 1135 !g. ?f. (($= >-- (\ (a:bool) (r:'a). P r = a)) $=) g f 1136*) 1137 1138 1139val NEW_CHOICE_EXISTS = store_thm 1140 ("NEW_CHOICE_EXISTS", 1141 (--`?c. !P (x:'a). P x ==> P (c P)`--), 1142 STRIP_ASSUME_TAC CHOICE_FUN_PAIR_EXISTS 1143 THEN EXISTS_TAC ``SND o (r:('a -> bool) -> (('a -> bool) # 'a))`` 1144 THEN POP_ASSUM MP_TAC 1145 THEN REWRITE_TAC[FUN_EQ_THM,I_THM,o_THM] 1146 THEN BETA_TAC 1147 THEN DISCH_THEN (fn th => REWRITE_ALL_THM th THEN ASSUME_TAC th) 1148 THEN REPEAT STRIP_TAC 1149 THEN FIRST_ASSUM (MP_TAC o SPECL[ ``P:'a -> bool``, ``P:'a -> bool``]) 1150 THEN REWRITE_TAC[] 1151 THEN DISCH_THEN MATCH_MP_TAC 1152 THEN EXISTS_TAC ``x:'a`` 1153 THEN FIRST_ASSUM ACCEPT_TAC 1154 ); 1155 1156local 1157open Rsyntax 1158in 1159val NEW_CHOICE = 1160 new_specification { name = "NEW_CHOICE", 1161 consts = [ { const_name = "@@", 1162 fixity = Binder } ], 1163 sat_thm = NEW_CHOICE_EXISTS } 1164end; 1165 1166 1167 1168 1169 1170 1171val _ = export_theory(); 1172 1173val _ = print_theory_to_file "-" "quotient.lst"; 1174 1175val _ = html_theory "quotient"; 1176 1177fun print_theory_size () = 1178 (print "The theory "; 1179 print (current_theory ()); 1180 print " has "; 1181 print (Int.toString (length (types (current_theory ())))); 1182 print " types, "; 1183 print (Int.toString (length (axioms "-"))); 1184 print " axioms, "; 1185 print (Int.toString (length (definitions "-"))); 1186 print " definitions, and "; 1187 print (Int.toString (length (theorems "-"))); 1188 print " theorems."; 1189 print "\n" ); 1190 1191val _ = (*tactics.*)print_theory_size(); 1192