1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6(* --------------------------------------------------------------------- *) 7(* Lifting the lambda calculus syntax to the abstract level. *) 8(* Version 2.1. *) 9(* Date: February 28, 2005 *) 10(* --------------------------------------------------------------------- *) 11 12 13val _ = new_theory "quotient_list"; 14 15open prim_recTheory; 16open combinTheory; 17open listTheory; 18open rich_listTheory; 19open listLib; 20open bossLib; 21open res_quanTheory; 22open res_quanLib; 23open dep_rewrite; 24open quotientTheory; 25 26 27val REWRITE_THM = fn th => REWRITE_TAC[th]; 28val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th]; 29val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th]) 30 THEN REWRITE_TAC[th]; 31 32val POP_TAC = POP_ASSUM (fn th => ALL_TAC); 33 34 35(* =================================================================== *) 36(* To form a ABS / REP function or a equivalence relation REL from *) 37(* the corresponding functions/relations of the constituent subtypes *) 38(* of the main type, use the following table of operators: *) 39(* *) 40(* Type Operator Constructor Abstraction Equivalence *) 41(* *) 42(* Identity I x I $= *) 43(* Product (ty1 # ty2) (a,b) (abs1 ## abs2) (R1 ### R2) *) 44(* Sum (ty1 + ty2) (INL x) (abs1 ++ abs2) (R1 +++ R2) *) 45(* List (ty list) (CONS h t) (MAP abs) (LIST_REL R) *) 46(* Option (ty option) (SOME x) (OPTION_MAP abs) (OPTION_REL R) *) 47(* Function (ty1 -> ty2) (\x. f x) (rep1 --> abs2) (rep1 =-> abs2) *) 48(* (Strong respect) (R1 ===> R2) *) 49(* *) 50(* =================================================================== *) 51 52 53 54 55(* for LIST_REP or LIST_ABS, just use MAP! See Theorem MAP. *) 56 57val LIST_MAP_I = 58 store_thm 59 ("LIST_MAP_I", 60 (���MAP (I:'a -> 'a) = I���), 61 REWRITE_TAC[FUN_EQ_THM] 62 THEN Induct 63 THEN ASM_REWRITE_TAC[MAP,I_THM] 64 ); 65 66(* for list equivalence relation, use prefix LIST_REL *) 67 68val LIST_REL_def = listTheory.LIST_REL_def 69 70val LIST_REL_EQ = store_thm 71 ("LIST_REL_EQ", 72 (���(LIST_REL ($= : 'a->'a->bool)) = $=���), 73 CONV_TAC FUN_EQ_CONV 74 THEN CONV_TAC (RAND_CONV (ABS_CONV FUN_EQ_CONV)) 75 THEN Induct 76 THENL [ ALL_TAC, GEN_TAC ] 77 THEN Induct 78 THEN REWRITE_TAC[LIST_REL_def,NOT_CONS_NIL,NOT_NIL_CONS] 79 THEN GEN_TAC 80 THEN ASM_REWRITE_TAC[CONS_11] 81 ); 82 83val LIST_REL_REFL = store_thm 84 ("LIST_REL_REFL", 85 (���!R. (!x y:'a. R x y = (R x = R y)) ==> 86 !x. LIST_REL R x x���), 87 GEN_TAC 88 THEN DISCH_TAC 89 THEN Induct 90 THEN REWRITE_TAC[LIST_REL_def] 91 THEN GEN_TAC 92 THEN ASM_REWRITE_TAC[] 93 ); 94 95val LIST_EQUIV = store_thm 96 ("LIST_EQUIV", 97 (���!R:'a -> 'a -> bool. EQUIV R ==> EQUIV (LIST_REL R)���), 98 GEN_TAC 99 THEN REWRITE_TAC[EQUIV_def] 100 THEN DISCH_TAC 101 THEN Induct THENL [ALL_TAC, GEN_TAC] 102 THEN Induct 103 THEN REWRITE_TAC[LIST_REL_def] 104 THENL 105 [ PROVE_TAC[LIST_REL_def], 106 107 PROVE_TAC[LIST_REL_def], 108 109 GEN_TAC 110 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV) 111 THEN EQ_TAC 112 THENL 113 [ STRIP_TAC 114 THEN Cases 115 THEN REWRITE_TAC[LIST_REL_def] 116 THEN PROVE_TAC[], 117 118 DISCH_THEN (MP_TAC o GEN ``c:'a`` o GEN ``cs:'a list`` 119 o SPEC ``(c:'a)::cs``) 120 THEN REWRITE_TAC[LIST_REL_def] 121 THEN IMP_RES_TAC LIST_REL_REFL 122 THEN PROVE_TAC[] 123 ] 124 ] 125 ); 126 127Theorem LIST_REL_REL: 128 !R (abs:'a -> 'b) rep. 129 QUOTIENT R abs rep ==> 130 !r s. LIST_REL R r s <=> LIST_REL R r r /\ LIST_REL R s s /\ 131 (MAP abs r = MAP abs s) 132Proof 133 REPEAT GEN_TAC 134 THEN STRIP_TAC 135 THEN Induct 136 THENL [ ALL_TAC, GEN_TAC ] 137 THEN Cases 138 THEN ONCE_REWRITE_TAC[LIST_REL_def] 139 THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS] 140 THEN REWRITE_TAC[CONS_11] 141 THEN IMP_RES_THEN 142 (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th)))) 143 QUOTIENT_REL 144 THEN POP_ASSUM 145 (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th)))) 146 THEN PROVE_TAC[] 147QED 148 149val LIST_QUOTIENT = store_thm 150 ("LIST_QUOTIENT", 151 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 152 QUOTIENT (LIST_REL R) (MAP abs) (MAP rep)���), 153 REPEAT STRIP_TAC 154 THEN REWRITE_TAC[QUOTIENT_def] 155 THEN REPEAT CONJ_TAC 156 THENL (* 3 subgoals *) 157 [ IMP_RES_TAC QUOTIENT_ABS_REP 158 THEN Induct 159 THEN ASM_REWRITE_TAC[MAP], 160 161 IMP_RES_TAC QUOTIENT_REP_REFL 162 THEN Induct 163 THEN ASM_REWRITE_TAC[MAP,LIST_REL_def], 164 165 Induct 166 THENL [ ALL_TAC, GEN_TAC ] 167 THEN Cases 168 THEN ONCE_REWRITE_TAC[LIST_REL_def] 169 THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS] 170 THEN REWRITE_TAC[CONS_11] 171 THEN IMP_RES_THEN 172 (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th)))) 173 QUOTIENT_REL 174 THEN IMP_RES_THEN 175 (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th)))) 176 LIST_REL_REL 177 THEN PROVE_TAC[] 178 ] 179 ); 180 181 182 183 184(* Here are some definitional and well-formedness theorems 185 for some standard polymorphic operators. 186*) 187 188 189 190(* list theory: CONS, NIL, MAP, LENGTH, APPEND, FLAT, REVERSE, FILTER, 191 NULL, EVERY (ALL_EL), EXISTS (SOME_EL), FOLDL, FOLDR *) 192 193val CONS_PRS = store_thm 194 ("CONS_PRS", 195 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 196 !t h. CONS h t = (MAP abs) (CONS (rep h) (MAP rep t))���), 197 REPEAT GEN_TAC 198 THEN DISCH_TAC 199 THEN Induct 200 THEN ASM_REWRITE_TAC[MAP] 201 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP 202 ); 203 204val CONS_RSP = store_thm 205 ("CONS_RSP", 206 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 207 !t1 t2 h1 h2. 208 R h1 h2 /\ (LIST_REL R) t1 t2 ==> 209 (LIST_REL R) (CONS h1 t1) (CONS h2 t2)���), 210 REPEAT GEN_TAC 211 THEN DISCH_TAC 212 THEN Cases 213 THEN Cases 214 THEN REPEAT GEN_TAC 215 THEN REWRITE_TAC[LIST_REL_def] 216 ); 217 218 219val NIL_PRS = store_thm 220 ("NIL_PRS", 221 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 222 ([] = (MAP abs) [])���), 223 REPEAT STRIP_TAC 224 THEN REWRITE_TAC[MAP] 225 ); 226 227val NIL_RSP = store_thm 228 ("NIL_RSP", 229 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 230 (LIST_REL R) [] []���), 231 REPEAT STRIP_TAC 232 THEN REWRITE_TAC[LIST_REL_def] 233 ); 234 235 236val MAP_PRS = store_thm 237 ("MAP_PRS", 238 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 239 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 240 !l f. MAP f l = (MAP abs2) (MAP ((abs1 --> rep2) f) (MAP rep1 l))���), 241 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC) 242 THEN Induct 243 THEN ASM_REWRITE_TAC[MAP] 244 THEN REPEAT GEN_TAC 245 THEN REWRITE_TAC[CONS_11] 246 THEN ASM_REWRITE_TAC[FUN_MAP_THM] 247 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP 248 ); 249 250val MAP_RSP = store_thm 251 ("MAP_RSP", 252 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 253 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 254 !l1 l2 f1 f2. 255 (R1 ===> R2) f1 f2 /\ (LIST_REL R1) l1 l2 ==> 256 (LIST_REL R2) (MAP f1 l1) (MAP f2 l2)���), 257 REPEAT GEN_TAC 258 THEN DISCH_TAC 259 THEN REPEAT GEN_TAC 260 THEN DISCH_TAC 261 THEN Induct 262 THENL [ ALL_TAC, GEN_TAC ] 263 THEN Induct 264 THEN REPEAT GEN_TAC 265 THEN REWRITE_TAC[MAP,LIST_REL_def] 266 THEN STRIP_TAC 267 THEN CONJ_TAC 268 THENL 269 [ IMP_RES_TAC FUN_REL_MP, 270 271 FIRST_ASSUM MATCH_MP_TAC 272 THEN ASM_REWRITE_TAC[] 273 ] 274 ); 275 276val LENGTH_PRS = store_thm 277 ("LENGTH_PRS", 278 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 279 !l. LENGTH l = LENGTH (MAP rep l)���), 280 REPEAT GEN_TAC 281 THEN DISCH_TAC 282 THEN Induct 283 THEN ASM_REWRITE_TAC[LENGTH,MAP] 284 ); 285 286val LENGTH_RSP = store_thm 287 ("LENGTH_RSP", 288 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 289 !l1 l2. 290 (LIST_REL R) l1 l2 ==> 291 (LENGTH l1 = LENGTH l2)���), 292 REPEAT GEN_TAC 293 THEN DISCH_TAC 294 THEN Induct 295 THENL [ ALL_TAC, GEN_TAC ] 296 THEN Induct 297 THEN REPEAT GEN_TAC 298 THEN REWRITE_TAC[LENGTH,LIST_REL_def] 299 THEN STRIP_TAC 300 THEN REWRITE_TAC[INV_SUC_EQ] 301 THEN FIRST_ASSUM MATCH_MP_TAC 302 THEN FIRST_ASSUM ACCEPT_TAC 303 ); 304 305val APPEND_PRS = store_thm 306 ("APPEND_PRS", 307 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 308 !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))���), 309 REPEAT GEN_TAC 310 THEN DISCH_TAC 311 THEN Induct 312 THENL [ ALL_TAC, GEN_TAC ] 313 THEN Induct 314 THEN ASM_REWRITE_TAC[APPEND,MAP] 315 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP 316 THEN GEN_TAC 317 THEN POP_ASSUM MP_TAC 318 THEN REWRITE_TAC[APPEND,MAP] 319 THEN DISCH_THEN (REWRITE_THM o SYM) 320 ); 321 322val APPEND_RSP = store_thm 323 ("APPEND_RSP", 324 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 325 !l1 l2 m1 m2. 326 (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==> 327 (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)���), 328 REPEAT GEN_TAC 329 THEN DISCH_TAC 330 THEN Induct 331 THENL [ ALL_TAC, GEN_TAC ] 332 THEN Induct 333 THEN REPEAT GEN_TAC 334 THEN REWRITE_TAC[APPEND,LIST_REL_def] 335 THEN STRIP_TAC 336 THEN ASM_REWRITE_TAC[] 337 THEN FIRST_ASSUM MATCH_MP_TAC 338 THEN CONJ_TAC 339 THEN FIRST_ASSUM ACCEPT_TAC 340 ); 341 342val FLAT_PRS = store_thm 343 ("FLAT_PRS", 344 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 345 !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))���), 346 REPEAT GEN_TAC 347 THEN DISCH_TAC 348 THEN Induct 349 THEN ASM_REWRITE_TAC[FLAT,MAP] 350 THEN Induct 351 THEN REWRITE_TAC[MAP,APPEND] 352 THEN ASM_REWRITE_TAC[MAP_APPEND] 353 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP 354 ); 355 356val FLAT_RSP = store_thm 357 ("FLAT_RSP", 358 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 359 !l1 l2. 360 LIST_REL (LIST_REL R) l1 l2 ==> 361 (LIST_REL R) (FLAT l1) (FLAT l2)���), 362 REPEAT GEN_TAC 363 THEN DISCH_TAC 364 THEN Induct 365 THENL [ ALL_TAC, GEN_TAC ] 366 THEN Induct 367 THEN REPEAT GEN_TAC 368 THEN REWRITE_TAC[FLAT,LIST_REL_def] 369 THEN STRIP_TAC 370 THEN DEP_REWRITE_TAC[APPEND_RSP] 371 THEN EXISTS_TAC (���abs:'a -> 'b���) 372 THEN EXISTS_TAC (���rep:'b -> 'a���) 373 THEN ASM_REWRITE_TAC[] 374 THEN FIRST_ASSUM MATCH_MP_TAC 375 THEN FIRST_ASSUM ACCEPT_TAC 376 ); 377 378val REVERSE_PRS = store_thm 379 ("REVERSE_PRS", 380 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 381 !l. REVERSE l = MAP abs (REVERSE (MAP rep l))���), 382 REPEAT GEN_TAC 383 THEN DISCH_TAC 384 THEN Induct 385 THEN ASM_REWRITE_TAC[REVERSE_DEF,MAP] 386 THEN GEN_TAC 387 THEN ASM_REWRITE_TAC[MAP_APPEND,MAP] 388 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP 389 ); 390 391val REVERSE_RSP = store_thm 392 ("REVERSE_RSP", 393 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 394 !l1 l2. 395 LIST_REL R l1 l2 ==> 396 (LIST_REL R) (REVERSE l1) (REVERSE l2)���), 397 REPEAT GEN_TAC 398 THEN DISCH_TAC 399 THEN Induct 400 THENL [ ALL_TAC, GEN_TAC ] 401 THEN Induct 402 THEN REPEAT GEN_TAC 403 THEN REWRITE_TAC[REVERSE_DEF,LIST_REL_def] 404 THEN STRIP_TAC 405 THEN DEP_REWRITE_TAC[APPEND_RSP] 406 THEN EXISTS_TAC (���abs:'a -> 'b���) 407 THEN EXISTS_TAC (���rep:'b -> 'a���) 408 THEN ASM_REWRITE_TAC[LIST_REL_def] 409 THEN FIRST_ASSUM MATCH_MP_TAC 410 THEN FIRST_ASSUM ACCEPT_TAC 411 ); 412 413val FILTER_PRS = store_thm 414 ("FILTER_PRS", 415 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 416 !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l)) 417 ���), 418 REPEAT GEN_TAC 419 THEN DISCH_TAC 420 THEN GEN_TAC 421 THEN Induct 422 THEN ASM_REWRITE_TAC[FILTER,MAP] 423 THEN GEN_TAC 424 THEN IMP_RES_TAC QUOTIENT_ABS_REP 425 THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM] 426 THEN COND_CASES_TAC 427 THEN ASM_REWRITE_TAC[MAP] 428 ); 429 430val FILTER_RSP = store_thm 431 ("FILTER_RSP", 432 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 433 !P1 P2 l1 l2. 434 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> 435 (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)���), 436 REPEAT GEN_TAC 437 THEN DISCH_TAC 438 THEN GEN_TAC THEN GEN_TAC 439 THEN Induct 440 THENL [ ALL_TAC, GEN_TAC ] 441 THEN Induct 442 THEN REPEAT GEN_TAC 443 THEN REWRITE_TAC[FILTER,LIST_REL_def] 444 THEN REWRITE_TAC[FUN_REL] 445 THEN STRIP_TAC 446 THEN REPEAT COND_CASES_TAC 447 THEN REWRITE_TAC[LIST_REL_def] 448 THEN REPEAT CONJ_TAC 449 THENL (* 5 subgoals *) 450 [ FIRST_ASSUM ACCEPT_TAC, 451 452 FIRST_ASSUM MATCH_MP_TAC 453 THEN ASM_REWRITE_TAC[FUN_REL], 454 455 RES_TAC 456 THEN RES_TAC, 457 458 RES_TAC 459 THEN RES_TAC, 460 461 FIRST_ASSUM MATCH_MP_TAC 462 THEN ASM_REWRITE_TAC[FUN_REL] 463 ] 464 ); 465 466val NULL_PRS = store_thm 467 ("NULL_PRS", 468 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 469 !l. NULL l = NULL (MAP rep l)���), 470 REPEAT GEN_TAC 471 THEN DISCH_TAC 472 THEN Cases 473 THEN REWRITE_TAC[NULL,MAP] 474 ); 475 476val NULL_RSP = store_thm 477 ("NULL_RSP", 478 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 479 !l1 l2. 480 LIST_REL R l1 l2 ==> 481 (NULL l1 = NULL l2)���), 482 REPEAT GEN_TAC 483 THEN DISCH_TAC 484 THEN Induct 485 THENL [ ALL_TAC, GEN_TAC ] 486 THEN Induct 487 THEN REPEAT GEN_TAC 488 THEN REWRITE_TAC[NULL,LIST_REL_def] 489 ); 490 491val ALL_EL_PRS = store_thm 492 ("ALL_EL_PRS", 493 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 494 !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)���), 495 REPEAT GEN_TAC 496 THEN DISCH_TAC 497 THEN Induct 498 THEN ASM_REWRITE_TAC[ALL_EL,MAP] 499 THEN REPEAT GEN_TAC 500 THEN IMP_RES_TAC QUOTIENT_ABS_REP 501 THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM] 502 ); 503 504val ALL_EL_RSP = store_thm 505 ("ALL_EL_RSP", 506 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 507 !l1 l2 P1 P2. 508 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> 509 (ALL_EL P1 l1 = ALL_EL P2 l2)���), 510 REPEAT GEN_TAC 511 THEN DISCH_TAC 512 THEN Induct 513 THENL [ ALL_TAC, GEN_TAC ] 514 THEN Induct 515 THEN REPEAT GEN_TAC 516 THEN REWRITE_TAC[ALL_EL,LIST_REL_def] 517 THEN REWRITE_TAC[FUN_REL] 518 THEN STRIP_TAC 519 THEN MK_COMB_TAC 520 THENL 521 [ AP_TERM_TAC 522 THEN FIRST_ASSUM MATCH_MP_TAC 523 THEN FIRST_ASSUM ACCEPT_TAC, 524 525 FIRST_ASSUM MATCH_MP_TAC 526 THEN ASM_REWRITE_TAC[FUN_REL] 527 ] 528 ); 529 530val SOME_EL_PRS = store_thm 531 ("SOME_EL_PRS", 532 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 533 !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)���), 534 REPEAT GEN_TAC 535 THEN DISCH_TAC 536 THEN Induct 537 THEN ASM_REWRITE_TAC[SOME_EL,MAP] 538 THEN REPEAT GEN_TAC 539 THEN IMP_RES_TAC QUOTIENT_ABS_REP 540 THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM] 541 ); 542 543val SOME_EL_RSP = store_thm 544 ("SOME_EL_RSP", 545 (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> 546 !l1 l2 P1 P2. 547 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> 548 (SOME_EL P1 l1 = SOME_EL P2 l2)���), 549 REPEAT GEN_TAC 550 THEN DISCH_TAC 551 THEN Induct 552 THENL [ ALL_TAC, GEN_TAC ] 553 THEN Induct 554 THEN REPEAT GEN_TAC 555 THEN REWRITE_TAC[SOME_EL,LIST_REL_def] 556 THEN REWRITE_TAC[FUN_REL] 557 THEN STRIP_TAC 558 THEN MK_COMB_TAC 559 THENL 560 [ AP_TERM_TAC 561 THEN FIRST_ASSUM MATCH_MP_TAC 562 THEN FIRST_ASSUM ACCEPT_TAC, 563 564 FIRST_ASSUM MATCH_MP_TAC 565 THEN ASM_REWRITE_TAC[FUN_REL] 566 ] 567 ); 568 569 570val FOLDL_PRS = store_thm 571 ("FOLDL_PRS", 572 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 573 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 574 !l f e. FOLDL f e l = 575 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f) 576 (rep1 e) 577 (MAP rep2 l))���), 578 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC) 579 THEN IMP_RES_TAC QUOTIENT_ABS_REP 580 THEN Induct 581 THEN ASM_REWRITE_TAC[FOLDL,MAP,FUN_MAP_THM] 582 ); 583 584val FOLDL_RSP = store_thm 585 ("FOLDL_RSP", 586 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 587 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 588 !l1 l2 f1 f2 e1 e2. 589 (R1 ===> R2 ===> R1) f1 f2 /\ 590 R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==> 591 R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)���), 592 REPEAT GEN_TAC THEN DISCH_TAC 593 THEN REPEAT GEN_TAC THEN DISCH_TAC 594 THEN Induct 595 THENL [ ALL_TAC, GEN_TAC ] 596 THEN Induct 597 THEN REPEAT GEN_TAC 598 THEN REWRITE_TAC[FOLDL,LIST_REL_def] 599 THEN REWRITE_TAC[FUN_REL] 600 THEN STRIP_TAC 601 THEN FIRST_ASSUM MATCH_MP_TAC 602 THEN REWRITE_TAC[FUN_REL] 603 THEN REPEAT CONJ_TAC (* 3 subgoals *) 604 THEN TRY (FIRST_ASSUM ACCEPT_TAC) 605 THEN DEP_ONCE_ASM_REWRITE_TAC[] 606 THEN CONJ_TAC 607 THEN FIRST_ASSUM ACCEPT_TAC 608 ); 609 610 611val FOLDR_PRS = store_thm 612 ("FOLDR_PRS", 613 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 614 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 615 !l f e. FOLDR f e l = 616 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f) 617 (rep2 e) 618 (MAP rep1 l))���), 619 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC) 620 THEN IMP_RES_TAC QUOTIENT_ABS_REP 621 THEN Induct 622 THEN ASM_REWRITE_TAC[FOLDR,MAP,FUN_MAP_THM] 623 ); 624 625val FOLDR_RSP = store_thm 626 ("FOLDR_RSP", 627 (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> 628 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> 629 !l1 l2 f1 f2 e1 e2. 630 (R1 ===> R2 ===> R2) f1 f2 /\ 631 R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==> 632 R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)���), 633 REPEAT GEN_TAC THEN DISCH_TAC 634 THEN REPEAT GEN_TAC THEN DISCH_TAC 635 THEN Induct 636 THENL [ ALL_TAC, GEN_TAC ] 637 THEN Induct 638 THEN REPEAT GEN_TAC 639 THEN REWRITE_TAC[FOLDR,LIST_REL_def] 640 THEN REWRITE_TAC[FUN_REL] 641 THEN STRIP_TAC 642 THEN DEP_ONCE_ASM_REWRITE_TAC[] 643 THEN CONJ_TAC 644 THEN TRY (FIRST_ASSUM ACCEPT_TAC) 645 THEN FIRST_ASSUM MATCH_MP_TAC 646 THEN REWRITE_TAC[FUN_REL] 647 THEN REPEAT CONJ_TAC 648 THEN FIRST_ASSUM ACCEPT_TAC 649 ); 650 651 652 653 654val _ = export_theory(); 655 656val _ = print_theory_to_file "-" "quotient_list.lst"; 657 658val _ = html_theory "quotient_list"; 659