1(* ===================================================================== *) 2(* FILE : Drule.sml *) 3(* DESCRIPTION : Derived theorems and rules. Largely translated from *) 4(* hol88. *) 5(* *) 6(* AUTHORS : (c) Mike Gordon and *) 7(* Tom Melham, University of Cambridge, for hol88 *) 8(* TRANSLATOR : Konrad Slind, University of Calgary *) 9(* DATE : September 11, 1991 *) 10(* ===================================================================== *) 11 12structure Drule :> Drule = 13struct 14 15open Feedback HolKernel Parse boolTheory boolSyntax Abbrev; 16 17val ERR = mk_HOL_ERR "Drule" 18 19(*---------------------------------------------------------------------------* 20 * Eta-conversion * 21 * * 22 * "(\x.t x)" ---> |- (\x.t x) = t (if x not free in t) * 23 *---------------------------------------------------------------------------*) 24 25(* Cursory profiling indicates that an implementation of ETA_CONV as a 26 primitive inference rule in Thm is about 20 times faster than this 27 implementation, which instantiates ETA_AX. The difference in overall 28 HOL build time, however, is negligible. *) 29 30fun ETA_CONV t = 31 let 32 val (var, cmb) = dest_abs t 33 val tysubst = [alpha |-> type_of var, beta |-> type_of cmb] 34 val th = SPEC (rator cmb) (INST_TYPE tysubst ETA_AX) 35 in 36 TRANS (ALPHA t (lhs (concl th))) th 37 end 38 handle HOL_ERR _ => raise ERR "ETA_CONV" "" 39 40(*---------------------------------------------------------------------------* 41 * A |- t = (\x.f x) * 42 * --------------------- x not free in f * 43 * A |- t = f * 44 *---------------------------------------------------------------------------*) 45 46fun RIGHT_ETA thm = 47 TRANS thm (ETA_CONV (rhs (concl thm))) 48 handle HOL_ERR _ => raise ERR "RIGHT_ETA" "" 49 50(*---------------------------------------------------------------------------* 51 * Add an assumption * 52 * * 53 * A |- t' * 54 * ----------- * 55 * A,t |- t' * 56 *---------------------------------------------------------------------------*) 57 58fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t) 59 60(*---------------------------------------------------------------------------* 61 * Transitivity of ==> * 62 * * 63 * A1 |- t1 ==> t2 A2 |- t2 ==> t3 * 64 * --------------------------------------------- * 65 * A1 u A2 |- t1 ==> t3 * 66 *---------------------------------------------------------------------------*) 67 68fun IMP_TRANS th1 th2 = 69 let 70 val (ant, conseq) = dest_imp (concl th1) 71 in 72 DISCH ant (MP th2 (MP th1 (ASSUME ant))) 73 end 74 handle HOL_ERR _ => raise ERR "IMP_TRANS" "" 75 76(*---------------------------------------------------------------------------* 77 * A1 |- t1 ==> t2 A2 |- t2 ==> t1 * 78 * ----------------------------------------- * 79 * A1 u A2 |- t1 = t2 * 80 *---------------------------------------------------------------------------*) 81 82 fun IMP_ANTISYM_RULE th1 th2 = 83 let 84 val (ant, conseq) = dest_imp (concl th1) 85 in 86 MP (MP (SPEC conseq (SPEC ant IMP_ANTISYM_AX)) th1) th2 87 end 88 handle HOL_ERR _ => raise ERR "IMP_ANTISYM_RULE" "" 89 90(*---------------------------------------------------------------------------* 91 * Introduce =T * 92 * * 93 * A |- t * 94 * ------------ * 95 * A |- t=T * 96 *---------------------------------------------------------------------------*) 97 98local 99 val eq_thm = 100 let 101 val (Bvar, _) = dest_forall (concl boolTheory.EQ_CLAUSES) 102 val thm = CONJUNCT1 (CONJUNCT2 (SPEC Bvar boolTheory.EQ_CLAUSES)) 103 in 104 GEN Bvar (SYM thm) 105 end 106in 107 fun EQT_INTRO th = EQ_MP (SPEC (concl th) eq_thm) th 108 handle HOL_ERR _ => raise ERR "EQT_INTRO" "" 109end 110 111(*---------------------------------------------------------------------------* 112 * |- !x. t ----> x', |- t[x'/x] * 113 *---------------------------------------------------------------------------*) 114 115fun SPEC_VAR th = 116 let 117 val (Bvar, _) = dest_forall (concl th) 118 val bv' = prim_variant (HOLset.listItems (hyp_frees th)) Bvar 119 in 120 (bv', SPEC bv' th) 121 end 122 123(*---------------------------------------------------------------------------* 124 * A |- (!x. t1 = t2) * 125 * --------------------------- * 126 * A |- (?x.t1) = (?x.t2) * 127 *---------------------------------------------------------------------------*) 128 129fun MK_EXISTS bodyth = 130 let 131 val (x, sth) = SPEC_VAR bodyth 132 val (a, b) = dest_eq (concl sth) 133 val (abimp, baimp) = EQ_IMP_RULE sth 134 fun HALF (p, q) pqimp = 135 let 136 val xp = mk_exists (x, p) 137 and xq = mk_exists (x, q) 138 in 139 DISCH xp (CHOOSE (x, ASSUME xp) 140 (EXISTS (xq, x) (MP pqimp (ASSUME p)))) 141 end 142 in 143 IMP_ANTISYM_RULE (HALF (a, b) abimp) (HALF (b, a) baimp) 144 end 145 handle HOL_ERR _ => raise ERR "MK_EXISTS" "" 146 147(*---------------------------------------------------------------------------* 148 * A |- t1 = t2 * 149 * ------------------------------------------- (xi not free in A) * 150 * A |- (?x1 ... xn. t1) = (?x1 ... xn. t2) * 151 *---------------------------------------------------------------------------*) 152 153fun LIST_MK_EXISTS l th = itlist (fn x => fn th => MK_EXISTS (GEN x th)) l th 154 155fun SIMPLE_EXISTS v th = EXISTS (mk_exists (v, concl th), v) th 156 157fun SIMPLE_CHOOSE v th = 158 case HOLset.find (fn _ => true) (Thm.hypset th) of 159 SOME h => CHOOSE (v, ASSUME (boolSyntax.mk_exists (v, h))) th 160 | NONE => raise ERR "SIMPLE_CHOOSE" "" 161 162(*---------------------------------------------------------------------------* 163 * A1 |- t1 = u1 ... An |- tn = un A |- t[ti] * 164 * ------------------------------------------------------- * 165 * A1 u ... An u A |- t[ui] * 166 *---------------------------------------------------------------------------*) 167 168local 169 fun combine [] [] = [] 170 | combine (v :: rst1) (t :: rst2) = (v |-> t) :: combine rst1 rst2 171 | combine _ _ = raise ERR "GSUBS.combine" "Different length lists" 172in 173 fun GSUBS substfn ths th = 174 let 175 val ls = map (lhs o concl) ths 176 val vars = map (genvar o type_of) ls 177 val w = substfn (combine ls vars) (concl th) 178 in 179 SUBST (combine vars ths) w th 180 end 181end 182 183fun SUBS ths th = GSUBS subst ths th handle HOL_ERR _ => raise ERR "SUBS" "" 184 185fun SUBS_OCCS nlths th = 186 let 187 val (nll, ths) = unzip nlths 188 in 189 GSUBS (subst_occs nll) ths th 190 end 191 handle HOL_ERR _ => raise ERR "SUBS_OCCS" "" 192 193(*---------------------------------------------------------------------------* 194 * A |- ti == ui * 195 * -------------------- * 196 * A |- t[ti] = t[ui] * 197 *---------------------------------------------------------------------------*) 198 199fun SUBST_CONV theta template tm = 200 let 201 fun retheta {redex, residue} = (redex |-> genvar (type_of redex)) 202 val theta0 = map retheta theta 203 val theta1 = map (op |-> o (#residue ## #residue)) (zip theta0 theta) 204 in 205 SUBST theta1 (mk_eq (tm, subst theta0 template)) (REFL tm) 206 end 207 handle HOL_ERR _ => raise ERR "SUBST_CONV" "" 208 209(*---------------------------------------------------------------------------* 210 * Extensionality * 211 * * 212 * A |- !x. t1 x = t2 x * 213 * ---------------------- (x not free in A, t1 or t2) * 214 * A |- t1 = t2 * 215 *---------------------------------------------------------------------------*) 216 217fun EXT th = 218 let 219 val (Bvar, _) = dest_forall (concl th) 220 val th1 = SPEC Bvar th 221 (* th1 = |- t1 x = t2 x *) 222 val (t1x, t2x) = dest_eq (concl th1) 223 val x = rand t1x 224 val th2 = ABS x th1 225 (* th2 = |- (\x. t1 x) = (\x. t2 x) *) 226 in 227 TRANS (TRANS (SYM (ETA_CONV (mk_abs (x, t1x)))) th2) 228 (ETA_CONV (mk_abs (x, t2x))) 229 end 230 handle HOL_ERR _ => raise ERR "EXT" "" 231 232(*---------------------------------------------------------------------------* 233 * A |- !x. (t1 = t2) * 234 * ---------------------- * 235 * A |- (\x.t1) = (\x.t2) * 236 *---------------------------------------------------------------------------*) 237 238fun MK_ABS qth = 239 let 240 val (Bvar, Body) = dest_forall (concl qth) 241 val ufun = mk_abs (Bvar, lhs Body) 242 and vfun = mk_abs (Bvar, rhs Body) 243 val gv = genvar (type_of Bvar) 244 in 245 EXT (GEN gv (TRANS (TRANS (BETA_CONV (mk_comb (ufun, gv))) (SPEC gv qth)) 246 (SYM (BETA_CONV (mk_comb (vfun, gv)))))) 247 end 248 handle HOL_ERR _ => raise ERR "MK_ABS" "" 249 250(*---------------------------------------------------------------------------* 251 * Contradiction rule * 252 * * 253 * A |- F * 254 * ------ * 255 * A |- t * 256 *---------------------------------------------------------------------------*) 257 258fun CONTR tm th = 259 MP (SPEC tm FALSITY) th handle HOL_ERR _ => raise ERR "CONTR" "" 260 261(*---------------------------------------------------------------------------* 262 * "t1 /\ ... /\ tn" ---> [t1, ..., tn] |- t1 /\ ... /\ tn * 263 * * 264 * constructs a theorem proving conjunction from individual conjuncts * 265 *---------------------------------------------------------------------------*) 266 267fun ASSUME_CONJS tm = 268 let val (tm1, tm2) = dest_conj tm ; 269 in CONJ (ASSUME_CONJS tm1) (ASSUME_CONJS tm2) end 270 handle _ => ASSUME tm ; 271 272(*---------------------------------------------------------------------------* 273 * Undischarging - UNDISCH * 274 * * 275 * A |- t1 ==> t2 * 276 * -------------- * 277 * A, t1 |- t2 * 278 * * 279 * UNDISCH_TM also returns t1, UNDISCH_SPLIT splits t1 into its conjuncts * 280 *---------------------------------------------------------------------------*) 281 282fun UNDISCH th = 283 MP th (ASSUME (fst (dest_imp (concl th)))) 284 handle HOL_ERR _ => raise ERR "UNDISCH" "" 285 286fun UNDISCH_TM th = 287 let val (ant, conseq) = dest_imp (concl th) ; 288 in (ant, MP th (ASSUME ant)) end 289 handle HOL_ERR _ => raise ERR "UNDISCH_TM" "" 290 291fun UNDISCH_SPLIT th = 292 let val (ant, conseq) = dest_imp (concl th) ; 293 in MP th (ASSUME_CONJS ant) end 294 handle HOL_ERR _ => raise ERR "UNDISCH_SPLIT" "" 295 296(*---------------------------------------------------------------------------* 297 * =T elimination * 298 * * 299 * A |- t = T * 300 * ------------ * 301 * A |- t * 302 *---------------------------------------------------------------------------*) 303 304fun EQT_ELIM th = 305 EQ_MP (SYM th) TRUTH handle HOL_ERR _ => raise ERR "EQT_ELIM" "" 306 307(*---------------------------------------------------------------------------* 308 * |- !x1 ... xn. t[xi] * 309 * -------------------------- SPECL [t1, ..., tn] * 310 * |- t[ti] * 311 *---------------------------------------------------------------------------*) 312 313fun SPECL tml th = 314 rev_itlist SPEC tml th handle HOL_ERR _ => raise ERR "SPECL" "" 315 316(*---------------------------------------------------------------------------* 317 * SELECT introduction * 318 * * 319 * A |- P t * 320 * ----------------- * 321 * A |- P($@ P) * 322 *---------------------------------------------------------------------------*) 323 324fun SELECT_INTRO th = 325 let 326 val (Rator, Rand) = dest_comb (concl th) 327 val SELECT_AX' = INST_TYPE [alpha |-> type_of Rand] SELECT_AX 328 in 329 MP (SPEC Rand (SPEC Rator SELECT_AX')) th 330 end 331 handle HOL_ERR _ => raise ERR "SELECT_INTRO" "" 332 333(* --------------------------------------------------------------------------* 334 * SELECT elimination (cases) * 335 * * 336 * A1 |- P($@ P) A2, "P v" |- t * 337 * ---------------------------------------- (v occurs nowhere else in th2) * 338 * A1 u A2 |- t * 339 * * 340 * In line with the documentation in REFERENCE, this function succeeds even * 341 * if v occurs in t (giving a rather useless result). It also succeeds no * 342 * matter what the rand of the conclusion of th1 is. * 343 * * 344 * --------------------------------------------------------------------------*) 345 346fun SELECT_ELIM th1 (v, th2) = 347 let 348 val (Rator, Rand) = dest_comb (concl th1) 349 val th3 = DISCH (mk_comb (Rator, v)) th2 350 (* th3 = |- P v ==> t *) 351 in 352 MP (SPEC Rand (GEN v th3)) th1 353 end 354 handle HOL_ERR _ => raise ERR "SELECT_ELIM" "" 355 356(*---------------------------------------------------------------------------* 357 * SELECT introduction * 358 * * 359 * A |- ?x. t[x] * 360 * ----------------- * 361 * A |- t[@x.t[x]] * 362 *---------------------------------------------------------------------------*) 363 364fun SELECT_RULE th = 365 let 366 val (tm as (Bvar, Body)) = dest_exists (concl th) 367 val v = genvar (type_of Bvar) 368 val P = mk_abs (Bvar, Body) 369 val SELECT_AX' = INST_TYPE [alpha |-> type_of Bvar] SELECT_AX 370 val th1 = SPEC v (SPEC P SELECT_AX') 371 val (ant, conseq) = dest_imp (concl th1) 372 val th2 = BETA_CONV ant 373 and th3 = BETA_CONV conseq 374 val th4 = EQ_MP th3 (MP th1 (EQ_MP (SYM th2) (ASSUME (rhs (concl th2))))) 375 in 376 CHOOSE (v, th) th4 377 end 378 handle HOL_ERR _ => raise ERR "SELECT_RULE" "" 379 380(*---------------------------------------------------------------------------* 381 * ! abstraction * 382 * * 383 * A |- t1 = t2 * 384 * ----------------------- * 385 * A |- (!x.t1) = (!x.t2) * 386 *---------------------------------------------------------------------------*) 387 388fun FORALL_EQ x = 389 let 390 val forall = AP_TERM (inst [alpha |-> type_of x] boolSyntax.universal) 391 in 392 fn th => forall (ABS x th) 393 end 394 handle HOL_ERR _ => raise ERR "FORALL_EQ" "" 395 396(*---------------------------------------------------------------------------* 397 * ? abstraction * 398 * * 399 * A |- t1 = t2 * 400 * ----------------------- * 401 * A |- (?x.t1) = (?x.t2) * 402 *---------------------------------------------------------------------------*) 403 404fun EXISTS_EQ x = 405 let 406 val exists = AP_TERM (inst [alpha |-> type_of x] boolSyntax.existential) 407 in 408 fn th => exists (ABS x th) 409 end 410 handle HOL_ERR _ => raise ERR "EXISTS_EQ" "" 411 412(*---------------------------------------------------------------------------* 413 * @ abstraction * 414 * * 415 * A |- t1 = t2 * 416 * ----------------------- * 417 * A |- (@x.t1) = (@x.t2) * 418 *---------------------------------------------------------------------------*) 419 420fun SELECT_EQ x = 421 let 422 val ty = type_of x 423 val choose = inst [alpha |-> ty] boolSyntax.select 424 in 425 fn th => AP_TERM choose (ABS x th) 426 end 427 handle HOL_ERR _ => raise ERR "SELECT_EQ" "" 428 429(*---------------------------------------------------------------------------* 430 * Beta-conversion to the rhs of an equation * 431 * * 432 * A |- t1 = (\x.t2)t3 * 433 * -------------------- * 434 * A |- t1 = t2[t3/x] * 435 *---------------------------------------------------------------------------*) 436 437fun RIGHT_BETA th = 438 TRANS th (BETA_CONV (rhs (concl th))) 439 handle HOL_ERR _ => raise ERR "RIGHT_BETA" "" 440 441(*---------------------------------------------------------------------------* 442 * "(\x1 ... xn.t)t1 ... tn" --> * 443 * |- (\x1 ... xn.t)t1 ... tn = t[t1/x1] ... [tn/xn] * 444 *---------------------------------------------------------------------------*) 445 446fun LIST_BETA_CONV tm = 447 let 448 val (Rator, Rand) = dest_comb tm 449 in 450 RIGHT_BETA (AP_THM (LIST_BETA_CONV Rator) Rand) 451 end 452 handle HOL_ERR _ => REFL tm 453 454fun RIGHT_LIST_BETA th = TRANS th (LIST_BETA_CONV (rhs (concl th))) 455 456(*---------------------------------------------------------------------------* 457 * "A |- t1 /\ ... /\ tn" ---> ["A|-t1", ..., "A|-tn"], where n>0 * 458 * * 459 * Flattens out all conjuncts, regardless of grouping * 460 *---------------------------------------------------------------------------*) 461 462val CONJUNCTS = 463 let 464 fun aux acc th = 465 aux (aux acc (CONJUNCT2 th)) (CONJUNCT1 th) 466 handle HOL_ERR _ => th :: acc 467 in 468 aux [] 469 end 470 471(*---------------------------------------------------------------------------* 472 * |- t1 = t2 if t1 and t2 are equivalent using idempotence, symmetry and * 473 * associativity of /\. * 474 *---------------------------------------------------------------------------*) 475 476fun CONJUNCTS_AC (t1, t2) = 477 let 478 fun conjuncts dict th = 479 conjuncts (conjuncts dict (CONJUNCT1 th)) (CONJUNCT2 th) 480 handle HOL_ERR _ => Redblackmap.insert (dict, concl th, th) 481 fun prove_conj dict t = 482 let 483 val (l, r) = dest_conj t 484 in 485 CONJ (prove_conj dict l) (prove_conj dict r) 486 end 487 handle HOL_ERR _ => Redblackmap.find (dict, t) 488 val empty = Redblackmap.mkDict compare 489 val t1_imp_t2 = prove_conj (conjuncts empty (ASSUME t1)) t2 490 val t2_imp_t1 = prove_conj (conjuncts empty (ASSUME t2)) t1 491 in 492 IMP_ANTISYM_RULE (DISCH t1 t1_imp_t2) (DISCH t2 t2_imp_t1) 493 end 494 handle HOL_ERR _ => raise ERR "CONJUNCTS_AC" "" 495 | Redblackmap.NotFound => raise ERR "CONJUNCTS_AC" "" 496 497(*---------------------------------------------------------------------------* 498 * |- t1 = t2 if t1 and t2 are equivalent using idempotence, symmetry and * 499 * associativity of \/. * 500 *---------------------------------------------------------------------------*) 501 502(* 503 504 The implementation is dual to that of CONJUNCTS_AC. We first show that t2 505 follows from each of its disjuncts. These intermediate theorems are stored in 506 a dictionary with logarithmic time access. Combining them, we then show that 507 since each disjunct of t1 implies t2, t1 implies t2. 508 509 Note that deriving t2 from each of its disjuncts is not completely 510 straightforward. An implementation that, for each disjunct, assumes the 511 disjunct and derives t2 by disjunction introduction would have quadratic 512 complexity. The given implementation achieves linearithmic complexity by 513 assuming t2, and then deriving "l |- t2" and "r |- t2" from "l \/ r |- t2". 514 515 We found the implementation of this inference step that is used in "disjuncts" 516 (below) to be roughly twice as fast as one that instantiates a proforma 517 theorem "(l \/ r ==> t2) ==> l ==> t2" (and a similar proforma theorem for r). 518 Still, it is relatively expensive. If the number of disjuncts is small, an 519 implementation with quadratic complexity (as outlined above) is faster. Of 520 course, these figures very much depend on the primitive inference rules 521 available and their performance relative to each other. 522 523*) 524 525fun DISJUNCTS_AC (t1, t2) = 526 let 527 fun disjuncts dict (t, th) = 528 let 529 val (l, r) = dest_disj t 530 val th = DISCH t th 531 val l_th = MP th (DISJ1 (ASSUME l) r) 532 val r_th = MP th (DISJ2 l (ASSUME r)) 533 in 534 disjuncts (disjuncts dict (l, l_th)) (r, r_th) 535 end 536 handle HOL_ERR _ => Redblackmap.insert (dict, t, th) 537 fun prove_from_disj dict t = 538 let 539 val (l, r) = dest_disj t 540 in 541 DISJ_CASES (ASSUME t) (prove_from_disj dict l) 542 (prove_from_disj dict r) 543 end 544 handle HOL_ERR _ => Redblackmap.find (dict, t) 545 val empty = Redblackmap.mkDict compare 546 val t1_imp_t2 = prove_from_disj (disjuncts empty (t2, ASSUME t2)) t1 547 val t2_imp_t1 = prove_from_disj (disjuncts empty (t1, ASSUME t1)) t2 548 in 549 IMP_ANTISYM_RULE (DISCH t1 t1_imp_t2) (DISCH t2 t2_imp_t1) 550 end 551 handle HOL_ERR _ => raise ERR "DISJUNCTS_AC" "" 552 | Redblackmap.NotFound => raise ERR "DISJUNCTS_AC" "" 553 554(*---------------------------------------------------------------------------* 555 * A,t |- t1 = t2 * 556 * ----------------------------- * 557 * A |- (t /\ t1) = (t /\ t2) * 558 *---------------------------------------------------------------------------*) 559 560fun CONJ_DISCH t th = 561 let 562 val (lhs, rhs) = dest_eq (concl th) 563 and th1 = DISCH t th 564 val left_t = mk_conj (t, lhs) 565 val right_t = mk_conj (t, rhs) 566 val th2 = ASSUME left_t 567 and th3 = ASSUME right_t 568 val th4 = DISCH left_t 569 (CONJ (CONJUNCT1 th2) 570 (EQ_MP (MP th1 (CONJUNCT1 th2)) 571 (CONJUNCT2 th2))) 572 and th5 = DISCH right_t 573 (CONJ (CONJUNCT1 th3) 574 (EQ_MP (SYM (MP th1 (CONJUNCT1 th3))) 575 (CONJUNCT2 th3))) 576 in 577 IMP_ANTISYM_RULE th4 th5 578 end 579 580(*---------------------------------------------------------------------------* 581 * A,t1,...,tn |- t = u * 582 * -------------------------------------------------------- * 583 * A |- (t1 /\ ... /\ tn /\ t) = (t1 /\ ... /\ tn /\ u) * 584 *---------------------------------------------------------------------------*) 585 586val CONJ_DISCHL = itlist CONJ_DISCH 587 588(*---------------------------------------------------------------------------* 589 * A,t1 |- t2 A,t |- F * 590 * -------------- -------- * 591 * A |- t1 ==> t2 A |- ~t * 592 *---------------------------------------------------------------------------*) 593 594fun NEG_DISCH t th = 595 (if concl th = boolSyntax.F then NOT_INTRO (DISCH t th) else DISCH t th) 596 handle HOL_ERR _ => raise ERR "NEG_DISCH" "" 597 598(*---------------------------------------------------------------------------* 599 * A |- ~(t1 = t2) * 600 * ----------------- * 601 * A |- ~(t2 = t1) * 602 *---------------------------------------------------------------------------*) 603 604fun NOT_EQ_SYM th = 605 let 606 val t = (mk_eq o Lib.swap o dest_eq o dest_neg o concl) th 607 in 608 MP (SPEC t IMP_F) (DISCH t (MP th (SYM (ASSUME t)))) 609 end 610 611(* --------------------------------------------------------------------------* 612 * EQF_INTRO: inference rule for introducing equality with "F". * 613 * * 614 * ~tm * 615 * ----------- EQF_INTRO * 616 * tm = F * 617 * * 618 * [TFM 90.05.08] * 619 * --------------------------------------------------------------------------*) 620 621local 622 val Fth = ASSUME F 623in 624 fun EQF_INTRO th = 625 IMP_ANTISYM_RULE (NOT_ELIM th) 626 (DISCH F (CONTR (dest_neg (concl th)) Fth)) 627 handle HOL_ERR _ => raise ERR "EQF_INTRO" "" 628end 629 630(* --------------------------------------------------------------------------* 631 * EQF_ELIM: inference rule for eliminating equality with "F". * 632 * * 633 * |- tm = F * 634 * ----------- EQF_ELIM * 635 * |- ~ tm * 636 * * 637 * [TFM 90.08.23] * 638 * --------------------------------------------------------------------------*) 639 640fun EQF_ELIM th = 641 let 642 val (lhs, rhs) = dest_eq (concl th) 643 val _ = assert (equal boolSyntax.F) rhs 644 in 645 NOT_INTRO (DISCH lhs (EQ_MP th (ASSUME lhs))) 646 end 647 handle HOL_ERR _ => raise ERR "EQF_ELIM" "" 648 649(* --------------------------------------------------------------------------* 650 * ISPEC: specialization, with type instantation if necessary. * 651 * * 652 * A |- !x:ty.tm * 653 * ----------------------- ISPEC "t:ty'" * 654 * A |- tm[t/x] * 655 * * 656 * (where t is free for x in tm, and ty' is an instance of ty) * 657 * --------------------------------------------------------------------------*) 658 659local 660 fun err s = raise ERR "ISPEC" (": " ^ s) 661in 662 fun ISPEC t th = 663 let 664 val (Bvar, _) = 665 dest_forall (concl th) 666 handle HOL_ERR _ => err "input theorem not universally quantified" 667 val (_, inst) = 668 match_term Bvar t 669 handle HOL_ERR _ => err "can't type-instantiate input theorem" 670 in 671 SPEC t (INST_TYPE inst th) 672 handle HOL_ERR _ => err "type variable free in assumptions" 673 end 674end 675 676(* --------------------------------------------------------------------------* 677 * ISPECL: iterated specialization, with type instantiation if necessary. * 678 * * 679 * A |- !x1...xn.tm * 680 * --------------------------------- ISPECL ["t1",...,"tn"] * 681 * A |- tm[t1/x1,...,tn/xn] * 682 * * 683 * (where ti is free for xi in tm) * 684 * * 685 * Note: the following is simpler but it DOESN'T WORK. * 686 * * 687 * fun ISPECL tms th = rev_itlist ISPEC tms th * 688 * * 689 * --------------------------------------------------------------------------*) 690 691local 692 fun strip [] _ = [] (* Returns a list of (pat,ob) pairs. *) 693 | strip (tm :: tml) M = 694 let 695 val (Bvar, Body) = dest_forall M 696 in 697 (type_of Bvar, type_of tm)::strip tml Body 698 end 699 fun merge [] theta = theta 700 | merge ((x as {redex, residue})::rst) theta = 701 case subst_assoc (equal redex) theta of 702 NONE => x :: merge rst theta 703 | SOME rdue => if residue = rdue then merge rst theta 704 else raise ERR "ISPECL" "" 705 fun err s = raise ERR "ISPECL" s 706in 707 fun ISPECL [] = I 708 | ISPECL [tm] = ISPEC tm 709 | ISPECL tms = 710 fn th => 711 let 712 val pairs = 713 strip tms (concl th) 714 handle HOL_ERR _ => err "list of terms too long for theorem" 715 val inst = 716 rev_itlist 717 (fn (pat, ob) => fn ty_theta => 718 let 719 val theta = Type.match_type pat ob 720 in 721 merge theta ty_theta 722 end) pairs [] 723 handle HOL_ERR _ => err "can't type-instantiate input theorem" 724 in 725 SPECL tms (INST_TYPE inst th) 726 handle HOL_ERR _ => err "type variable free in assumptions" 727 end 728end 729 730(*---------------------------------------------------------------------------* 731 * Generalise a theorem over all variables free in conclusion but not in hyps* 732 * * 733 * A |- t[x1,...,xn] * 734 * ---------------------------- * 735 * A |- !x1...xn.t[x1,...,xn] * 736 *---------------------------------------------------------------------------*) 737 738fun GEN_ALL th = 739 HOLset.foldl (Lib.uncurry GEN) th 740 (HOLset.difference (FVL [concl th] empty_tmset, hyp_frees th)) 741 742(*---------------------------------------------------------------------------* 743 * Discharge all hypotheses * 744 * * 745 * t1, ... , tn |- t * 746 * ------------------------------ * 747 * |- t1 ==> ... ==> tn ==> t * 748 *---------------------------------------------------------------------------*) 749 750fun DISCH_ALL th = HOLset.foldl (Lib.uncurry DISCH) th (hypset th) 751 752(*---------------------------------------------------------------------------* 753 * A |- t1 ==> ... ==> tn ==> t * 754 * ------------------------------- * 755 * A, t1, ..., tn |- t * 756 *---------------------------------------------------------------------------*) 757 758fun UNDISCH_ALL th = if is_imp (concl th) then UNDISCH_ALL (UNDISCH th) else th 759 760(* --------------------------------------------------------------------------* 761 * SPEC_ALL : thm -> thm * 762 * * 763 * A |- !x1 ... xn. t[xi] * 764 * ------------------------ where the xi' are distinct * 765 * A |- t[xi'/xi] and not free in the input theorem * 766 * * 767 * BUGFIX: added the "distinct" part and code to make the xi's not free * 768 * in the conclusion !x1...xn.t[xi]. [TFM 90.10.04] * 769 * * 770 * OLD CODE: * 771 * * 772 * let SPEC_ALL th = * 773 * let vars,() = strip_forall(concl th) in * 774 * SPECL (map (variant (freesl (hyp th))) vars) th;; * 775 * --------------------------------------------------------------------------*) 776 777local 778 fun varyAcc v (V, l) = let val v' = prim_variant V v in (v'::V, v'::l) end 779in 780 fun SPEC_ALL th = 781 if is_forall (concl th) then 782 let 783 val (hvs, con) = (HOLset.listItems ## I) (hyp_frees th, concl th) 784 val fvs = free_vars con 785 val vars = fst (strip_forall con) 786 in 787 SPECL (snd (itlist varyAcc vars (hvs @ fvs, []))) th 788 end 789 else th 790end 791 792(*---------------------------------------------------------------------------* 793 * !x. A ==> !y. B ==> !z. C ==> !w. D * 794 * ----------------------------------- * 795 * C ==> B ==> A ==> D' (for example) * 796 * * 797 * reorders antecedents, modifies the conclusion D * 798 *---------------------------------------------------------------------------*) 799 800fun REORDER_ANTS_MOD f g th = 801 let val (ants, uth) = strip_gen_left (UNDISCH_TM o SPEC_ALL) th ; 802 in Lib.itlist DISCH (f ants) (g (SPEC_ALL uth)) end ; 803 804fun REORDER_ANTS f th = REORDER_ANTS_MOD f (fn c => c) th ; 805fun MODIFY_CONS g th = REORDER_ANTS_MOD (fn hs => hs) g th ; 806 807(*---------------------------------------------------------------------------* 808 * Use the conclusion of the first theorem to delete a hypothesis of * 809 * the second theorem. * 810 * * 811 * A |- t1 B, t1 |- t2 * 812 * ----------------------- * 813 * A u B |- t2 * 814 *---------------------------------------------------------------------------*) 815 816fun PROVE_HYP ath bth = MP (DISCH (concl ath) bth) ath 817 818(*---------------------------------------------------------------------------* 819 * A |- t1 /\ t2 ---> A |- t1, A |- t2 * 820 *---------------------------------------------------------------------------*) 821 822fun CONJ_PAIR th = (CONJUNCT1 th, CONJUNCT2 th) 823 handle HOL_ERR _ => raise ERR "CONJ_PAIR" "" 824 825(*---------------------------------------------------------------------------* 826 * ["A1|-t1", ..., "An|-tn"] ---> "A1u...uAn|-t1 /\ ... /\ tn", where n>0 * 827 *---------------------------------------------------------------------------*) 828 829val LIST_CONJ = end_itlist CONJ 830 831(*---------------------------------------------------------------------------* 832 * "A |- t1 /\ (...(... /\ tn)...)" * 833 * ---> * 834 * [ "A|-t1", ..., "A|-tn"], where n>0 * 835 * * 836 * Inverse of LIST_CONJ : flattens only right conjuncts. * 837 * You must specify n, since tn could itself be a conjunction * 838 *---------------------------------------------------------------------------*) 839 840fun CONJ_LIST 1 th = [th] 841 | CONJ_LIST n th = CONJUNCT1 th :: CONJ_LIST (n - 1) (CONJUNCT2 th) 842 handle HOL_ERR _ => raise ERR "CONJ_LIST" "" 843 844(*---------------------------------------------------------------------------* 845 * "|- !x. (t1 /\ ...) /\ ... (!y. ... /\ tn)" * 846 * ---> [ "|-t1", ..., "|-tn"], where n>0 * 847 * * 848 * Flattens out conjuncts even in bodies of forall's * 849 *---------------------------------------------------------------------------*) 850 851fun BODY_CONJUNCTS th = 852 if is_forall (concl th) 853 then BODY_CONJUNCTS (SPEC_ALL th) 854 else if is_conj (concl th) 855 then (BODY_CONJUNCTS (CONJUNCT1 th) @ BODY_CONJUNCTS (CONJUNCT2 th)) 856 else [th] 857 858(*---------------------------------------------------------------------------* 859 * Put a theorem * 860 * * 861 * |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t * 862 * * 863 * into canonical form by stripping out quantifiers and splitting * 864 * conjunctions apart. * 865 * * 866 * t1 /\ t2 ---> t1, t2 * 867 * (t1/\t2)==>t ---> t1==> (t2==>t) * 868 * (t1\/t2)==>t ---> t1==>t, t2==>t * 869 * (?x.t1)==>t2 ---> t1[x'/x] ==> t2 * 870 * !x.t1 ---> t1[x'/x] * 871 *---------------------------------------------------------------------------*) 872 873fun IMP_CANON th = 874 let 875 val w = concl th 876 in 877 if is_forall w 878 then IMP_CANON (SPEC_ALL th) 879 else if is_conj w 880 then IMP_CANON (CONJUNCT1 th) @ IMP_CANON (CONJUNCT2 th) 881 else if is_imp w 882 then let 883 val (ant, _) = dest_imp w 884 in 885 if is_conj ant 886 then let 887 val (conj1, conj2) = dest_conj ant 888 in 889 IMP_CANON 890 (DISCH conj1 891 (DISCH conj2 892 (MP th (CONJ (ASSUME conj1) 893 (ASSUME conj2))))) 894 end 895 else if is_disj ant 896 then let 897 val (disj1, disj2) = dest_disj ant 898 in 899 IMP_CANON 900 (DISCH disj1 901 (MP th (DISJ1 (ASSUME disj1) disj2))) @ 902 IMP_CANON 903 (DISCH disj2 (MP th (DISJ2 disj1 (ASSUME disj2)))) 904 end 905 else if is_exists ant 906 then let 907 val (Bvar, Body) = dest_exists ant 908 val bv' = variant (thm_frees th) Bvar 909 val body' = subst [Bvar |-> bv'] Body 910 in 911 IMP_CANON 912 (DISCH body' 913 (MP th (EXISTS (ant, bv') (ASSUME body')))) 914 end 915 else map (DISCH ant) (IMP_CANON (UNDISCH th)) 916 end 917 else [th] 918 end 919 920(*--------------------------------------------------------------------------- 921 | MP_CANON puts a theorem 922 | 923 | |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t 924 | 925 | into canonical form for applying MATCH_MP_TAC by moving quantifiers to 926 | the outmost level and combining implications 927 | 928 | t1 ==> !x. t2 ---> !x. t1 ==> t2 929 | t1 ==> t2 ==> t3 ---> t1 /\ t2 ==> t3 930 | 931 | It might be useful to replace equivalences with implications while 932 | normalising. MP_GENEQ_CANON gets a list of boolean values as an extra 933 | argument to configure such replacements. The occuring equations are split 934 | according to the elements of this list. true focuses on the left hand side, 935 | i.e. the right-hand side is put into the antecedent. false focuses on the 936 | right hand side. If the list is empty, the equation is not splitted. 937 | 938 | MP_GENEQ_CANON [true] |- !x. A x ==> (!y. (B1 x y):bool = B2 y) ---> 939 | !x y. A x /\ B2 y ===> B1 x y 940 | MP_GENEQ_CANON [false] |- !x. A x ==> (!y. (B1 x y):bool = B2 y) ---> 941 | !x y. A x /\ B1 x y ===> B2 y 942 | 943 | For convinience the most common cases of this parameter are introduced 944 | own functions 945 | 946 | val MP_CANON = MP_GENEQ_CANON [] 947 | val MP_LEQ_CANON = MP_GENEQ_CANON [true] 948 | val MP_REQ_CANON = MP_GENEQ_CANON [false] 949 |---------------------------------------------------------------------------*) 950 951local 952 fun RIGHT_IMP_IMP_FORALL_RULE th = 953 let 954 val w = concl th 955 in 956 if is_imp_only w 957 then let 958 val (ant, conc) = dest_imp w 959 in 960 if is_forall conc 961 then let 962 val (Bvar, Body) = dest_forall conc 963 val bv' = variant (thm_frees th) Bvar 964 val th1 = MP th (ASSUME ant) 965 val th2 = SPEC bv' th1 966 val th3 = DISCH ant th2 967 val th4 = RIGHT_IMP_IMP_FORALL_RULE th3 968 val th5 = GEN bv' th4 969 in 970 th5 971 end 972 else if is_imp_only conc 973 then let 974 val (ant2, conc2) = dest_imp conc 975 val conc_t = mk_conj (ant, ant2) 976 val conc_thm = ASSUME conc_t 977 val th1 = MP th (CONJUNCT1 conc_thm) 978 val th2 = MP th1 (CONJUNCT2 conc_thm) 979 val th3 = DISCH conc_t th2 980 in 981 RIGHT_IMP_IMP_FORALL_RULE th3 982 end 983 else th 984 end 985 else th 986 end 987in 988 fun MP_GENEQ_CANON eqL th = 989 let 990 val w = concl th 991 in 992 if is_forall w 993 then let 994 val (Bvar, Body) = dest_forall w 995 val bv' = variant (thm_frees th) Bvar 996 val th1 = MP_GENEQ_CANON eqL (SPEC bv' th) 997 val th2 = GEN bv' th1 998 in 999 th2 1000 end 1001 else if is_imp_only w 1002 then let 1003 val (ant, conc) = dest_imp w 1004 val th1 = MP th (ASSUME ant) 1005 val th2 = MP_GENEQ_CANON eqL th1 1006 val th3 = DISCH ant th2 1007 val th4 = RIGHT_IMP_IMP_FORALL_RULE th3 1008 in 1009 th4 1010 end 1011 else if not (null eqL) andalso is_eq w 1012 then MP_GENEQ_CANON (tl eqL) 1013 ((if hd eqL then snd else fst) (EQ_IMP_RULE th)) 1014 handle HOL_ERR _ => th 1015 else th 1016 end 1017end 1018 1019val MP_CANON = MP_GENEQ_CANON [] 1020val MP_LEQ_CANON = MP_GENEQ_CANON [true] 1021val MP_REQ_CANON = MP_GENEQ_CANON [false] 1022 1023(*---------------------------------------------------------------------------* 1024 * A1 |- t1 ... An |- tn A |- t1==>...==>tn==>t * 1025 * ----------------------------------------------------- * 1026 * A u A1 u ... u An |- t * 1027 *---------------------------------------------------------------------------*) 1028 1029val LIST_MP = rev_itlist (fn x => fn y => MP y x) 1030 1031(*---------------------------------------------------------------------------* 1032 * A |-t1 ==> t2 * 1033 * ----------------- * 1034 * A |- ~t2 ==> ~t1 * 1035 * * 1036 * Rewritten by MJCG to return "~t2 ==> ~t1" rather than "~t2 ==> t1 ==>F". * 1037 *---------------------------------------------------------------------------*) 1038 1039local 1040 val imp_th = GEN_ALL (el 5 (CONJUNCTS (SPEC_ALL IMP_CLAUSES))) 1041in 1042 fun CONTRAPOS impth = 1043 let 1044 val (ant, conseq) = dest_imp (concl impth) 1045 val notb = mk_neg conseq 1046 in 1047 DISCH notb 1048 (EQ_MP (SPEC ant imp_th) 1049 (DISCH ant (MP (ASSUME notb) (MP impth (ASSUME ant))))) 1050 end 1051 handle HOL_ERR _ => raise ERR "CONTRAPOS" "" 1052end 1053 1054(*---------------------------------------------------------------------------* 1055 * A |- t1 \/ t2 * 1056 * -------------------- * 1057 * A |- ~ t1 ==> t2 * 1058 *---------------------------------------------------------------------------*) 1059 1060fun DISJ_IMP dth = 1061 let 1062 val (disj1, disj2) = dest_disj (concl dth) 1063 val nota = mk_neg disj1 1064 in 1065 DISCH nota 1066 (DISJ_CASES dth (CONTR disj2 (MP (ASSUME nota) (ASSUME disj1))) 1067 (ASSUME disj2)) 1068 end 1069 handle HOL_ERR _ => raise ERR "DISJ_IMP" "" 1070 1071(*---------------------------------------------------------------------------* 1072 * A |- t1 ==> t2 * 1073 * --------------- * 1074 * A |- ~t1 \/ t2 * 1075 *---------------------------------------------------------------------------*) 1076 1077fun IMP_ELIM th = 1078 let 1079 val (ant, conseq) = dest_imp (concl th) 1080 val not_t1 = mk_neg ant 1081 in 1082 DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) 1083 (DISJ2 not_t1 (MP th (ASSUME ant))) 1084 (DISJ1 (ASSUME not_t1) conseq) 1085 end 1086 handle HOL_ERR _ => raise ERR "IMP_ELIM" "" 1087 1088(*---------------------------------------------------------------------------* 1089 * A |- t1 \/ t2 A1, t1 |- t3 A2, t2 |- t4 * 1090 * ------------------------------------------------ * 1091 * A u A1 u A2 |- t3 \/ t4 * 1092 *---------------------------------------------------------------------------*) 1093 1094fun DISJ_CASES_UNION dth ath bth = 1095 DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth) 1096 1097(*---------------------------------------------------------------------------* 1098 * * 1099 * |- A1 \/ ... \/ An [H1,A1 |- M, ..., Hn,An |- M] * 1100 * --------------------------------------------------------- * 1101 * H1 u ... u Hn |- M * 1102 * * 1103 * The order of the theorems in the list doesn't matter: an operation akin * 1104 * to sorting lines them up with the disjuncts in the theorem. * 1105 *---------------------------------------------------------------------------*) 1106 1107local 1108 fun ishyp tm th = HOLset.member (hypset th, tm) 1109 fun organize (tm :: rst) (alist as (_ :: _)) = 1110 let 1111 val (th, next) = Lib.pluck (ishyp tm) alist 1112 in 1113 th :: organize rst next 1114 end 1115 | organize [] [] = [] 1116 | organize other wise = 1117 raise ERR "DISJ_CASESL.organize" "length difference" 1118in 1119 fun DISJ_CASESL disjth thl = 1120 let 1121 val cases = strip_disj (concl disjth) 1122 val thl' = organize cases thl 1123 fun DL th [] = raise ERR "DISJ_CASESL" "no cases" 1124 | DL th [th1] = PROVE_HYP th th1 1125 | DL th [th1, th2] = DISJ_CASES th th1 th2 1126 | DL th (th1 :: rst) = 1127 DISJ_CASES th th1 (DL (ASSUME (snd (dest_disj (concl th)))) rst) 1128 in 1129 DL disjth thl' 1130 end 1131 handle e => raise wrap_exn "Drule" "DISJ_CASESL" e 1132end 1133 1134(*---------------------------------------------------------------------------* 1135 * Rename the bound variable of a lambda-abstraction * 1136 * * 1137 * "x" "(\y.t)" ---> |- "\y.t = \x. t[x/y]" * 1138 *---------------------------------------------------------------------------*) 1139 1140local 1141 fun err s = raise ERR "ALPHA_CONV" s 1142in 1143 fun ALPHA_CONV x t = 1144 let 1145 (* avoid calling dest_abs *) 1146 val (dty, _) = dom_rng (type_of t) 1147 handle HOL_ERR _ => err "Second term not an abstraction" 1148 val (xstr, xty) = with_exn dest_var x 1149 (ERR "ALPHA_CONV" "First term not a variable") 1150 val _ = Type.compare (dty, xty) = EQUAL 1151 orelse err "Type of variable not compatible with abstraction" 1152 val t' = rename_bvar xstr t 1153 in 1154 ALPHA t t' 1155 end 1156end 1157 1158(*---------------------------------------------------------------------------- 1159 Version of ALPHA_CONV that renames "x" when necessary, but then it doesn't 1160 meet the specification. Is that really a problem? Notice that this version 1161 of ALPHA_CONV is more efficient. 1162 1163 fun ALPHA_CONV x t = 1164 if Term.free_in x t 1165 then ALPHA_CONV (variant (free_vars t) x) t 1166 else ALPHA t (mk_abs{Bvar = x, 1167 Body = Term.beta_conv(mk_comb{Rator = t,Rand = x})}) 1168 ----------------------------------------------------------------------------*) 1169 1170(*---------------------------------------------------------------------------* 1171 * Rename bound variables * 1172 * * 1173 * "x" "(\y.t)" ---> |- "\y.t = \x. t[x/y]" * 1174 * "x" "(!y.t)" ---> |- "!y.t = !x. t[x/y]" * 1175 * "x" "(?y.t)" ---> |- "?y.t = ?x. t[x/y]" * 1176 * "x" "(?!y.t)" ---> |- "?!y.t = ?!x. t[x/y]" * 1177 * "x" "(@y.t)" ---> |- "@y.t = @x. t[x/y]" * 1178 *---------------------------------------------------------------------------*) 1179 1180fun GEN_ALPHA_CONV x t = 1181 if is_abs t 1182 then ALPHA_CONV x t 1183 else let 1184 val (Rator, Rand) = dest_comb t 1185 in 1186 AP_TERM Rator (ALPHA_CONV x Rand) 1187 end 1188 handle HOL_ERR _ => raise ERR "GEN_ALPHA_CONV" "" 1189 1190(* --------------------------------------------------------------------------* 1191 * A1 |- P ==> Q A2 |- R ==> S * 1192 * --------------------------------- IMP_CONJ * 1193 * A1 u A2 |- P /\ R ==> Q /\ S * 1194 * --------------------------------------------------------------------------*) 1195 1196fun IMP_CONJ th1 th2 = 1197 let 1198 val (A1, _) = dest_imp (concl th1) 1199 and (A2, _) = dest_imp (concl th2) 1200 val conj = mk_conj (A1, A2) 1201 val (a1, a2) = CONJ_PAIR (ASSUME conj) 1202 in 1203 DISCH conj (CONJ (MP th1 a1) (MP th2 a2)) 1204 end 1205 1206(* --------------------------------------------------------------------------* 1207 * EXISTS_IMP : existentially quantify the antecedent and conclusion * 1208 * of an implication. * 1209 * * 1210 * A |- P ==> Q * 1211 * -------------------------- EXISTS_IMP `x` * 1212 * A |- (?x.P) ==> (?x.Q) * 1213 * --------------------------------------------------------------------------*) 1214 1215fun EXISTS_IMP x th = 1216 if not (is_var x) 1217 then raise ERR "EXISTS_IMP" "first argument not a variable" 1218 else let 1219 val (ant, conseq) = dest_imp (concl th) 1220 val th1 = EXISTS (mk_exists (x, conseq), x) (UNDISCH th) 1221 val asm = mk_exists (x, ant) 1222 in 1223 DISCH asm (CHOOSE (x, ASSUME asm) th1) 1224 end 1225 handle HOL_ERR _ => raise ERR "EXISTS_IMP" "variable free in assumptions" 1226 1227(*---------------------------------------------------------------------------* 1228 * Instantiate terms and types of a theorem. This is pretty slow, because * 1229 * it makes two full traversals of the theorem. * 1230 *---------------------------------------------------------------------------*) 1231 1232fun INST_TY_TERM (Stm, Sty) th = INST Stm (INST_TYPE Sty th) 1233 1234(*---------------------------------------------------------------------------* 1235 * Instantiate terms and types of a theorem, also returning a list of * 1236 * substituted hypotheses in the same order as in hyp th * 1237 * (required for predictability of order of new subgoals from (prim_)irule) * 1238 *---------------------------------------------------------------------------*) 1239 1240fun INST_TT_HYPS subs th = 1241 let val nhyps = HOLset.numItems (hypset th) ; 1242 val thd = DISCH_ALL th ; 1243 val thdsub = INST_TY_TERM subs thd ; 1244 (* UNDISCH_TM nhyps times only *) 1245 fun UNDISCH_TM_L (th, tms) = 1246 let val (tm, th') = UNDISCH_TM th ; 1247 in (th', tm :: tms) end ; 1248 in Lib.funpow nhyps UNDISCH_TM_L (thdsub, []) end ; 1249 1250(*---------------------------------------------------------------------------* 1251 * |- !x y z. w ---> |- w[g1/x][g2/y][g3/z] * 1252 *---------------------------------------------------------------------------*) 1253 1254fun GSPEC th = 1255 let 1256 val (_, w) = dest_thm th 1257 in 1258 if is_forall w 1259 then GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th) 1260 else th 1261 end 1262 1263(*---------------------------------------------------------------------------* 1264 * Match a given part of "th" to a term, instantiating "th". The part * 1265 * should be free in the theorem, except for outer bound variables. * 1266 *---------------------------------------------------------------------------*) 1267 1268fun PART_MATCH partfn th = 1269 let 1270 val th = SPEC_ALL th 1271 val conclfvs = Term.FVL [concl th] empty_tmset 1272 val hypfvs = Thm.hyp_frees th 1273 val hyptyvars = HOLset.listItems (Thm.hyp_tyvars th) 1274 val pat = partfn (concl th) 1275 val matchfn = 1276 match_terml hyptyvars (HOLset.intersection (conclfvs, hypfvs)) pat 1277 in 1278 fn tm => INST_TY_TERM (matchfn tm) th 1279 end 1280 1281(*---------------------------------------------------------------------------* 1282 * version of PART_MATCH which allows substituting in assumptions * 1283 *---------------------------------------------------------------------------*) 1284fun PART_MATCH_A partfn th = 1285 let 1286 val pat = partfn (concl (SPEC_ALL th)) 1287 in 1288 fn tm => INST_TY_TERM (match_term pat tm) th 1289 end 1290 1291(* --------------------------------------------------------------------------* 1292 EXISTS_LEFT, EXISTS_LEFT1 1293 existentially quantifying variables which appear only in the hypotheses 1294 1295 [x = y, y = z] |- x = z 1296 (eg) -------------------------------- EXISTS_LEFT1 ``y`` 1297 [���y. (x = y) ��� (y = z)] |- x = z (UOK) 1298 1299 * --------------------------------------------------------------------------*) 1300 1301(* EXISTS_LEFT' : bool -> 1302 term list -> {fvs: term list, hyp: term} list -> term list -> thm -> thm 1303 used below, saves hyps, their free vars, and free vars of conclusion, 1304 across recursive calls 1305 arg1 - whether to ignore errors, ie, free vars which are either in the 1306 conclusion or not in any hypothesis 1307 arg2 - list of free vars in the conclusion 1308 arg3 - list of assumptions of the theorem, each with the list of free vars 1309 which it contains 1310 arg4 - list of free vars to become existentially quantified 1311*) 1312 1313fun EXISTS_LEFT' strict fvs_c hfvs [] th = th 1314 | EXISTS_LEFT' strict fvs_c hfvs (fv :: fvs) th = 1315 let 1316 val _ = if is_var fv then () 1317 else raise mk_HOL_ERR "Drule" "EXISTS_LEFT'" "not free variable" ; 1318 (* following raises Bind if fv in conclusion *) 1319 val _ = List.all (not o aconv fv) fvs_c orelse raise Bind 1320 fun hyp_ctns_fv {hyp, fvs} = List.exists (Lib.equal fv) fvs ; 1321 val (hyps_ctg_fv, hyps_nc) = List.partition hyp_ctns_fv hfvs ; 1322 (* following raises Bind if fv not in any hypothesis *) 1323 val _ = not (null hyps_ctg_fv) orelse raise Bind 1324 (* select and conjoin the hyps containing fv *) 1325 val conj_tm = list_mk_conj (map #hyp hyps_ctg_fv) ; 1326 (* using CONJ_LIST gives original hyps, even if they are conjunctions *) 1327 val sep_ths = CONJ_LIST (length hyps_ctg_fv) (ASSUME conj_tm) ; 1328 (* replace the previous hyps with the single new one, which is 1329 conjunction of the previous ones *) 1330 val th2 = Lib.itlist PROVE_HYP sep_ths th ; 1331 val ex_conj_tm = mk_exists (fv, conj_tm) ; 1332 val the = CHOOSE (fv, ASSUME ex_conj_tm) th2 ; 1333 val thex = EXISTS_LEFT' strict fvs_c 1334 ({hyp = ex_conj_tm, fvs = free_vars ex_conj_tm} :: hyps_nc) fvs the ; 1335 in thex end 1336 handle Bind => 1337 if strict then 1338 raise mk_HOL_ERR "Drule" "EXISTS_LEFT'" 1339 "free variable in conclusion or not in any hypothesis" 1340 else EXISTS_LEFT' strict fvs_c hfvs fvs th ; 1341 1342(* EXISTS_LEFT : term list -> thm -> thm 1343 for each free var in turn, do the following: 1344 replace hyps containing the free var by their conjunction, 1345 existentially quantified over the free var; 1346 ignore free vars for which this can't be done *) 1347fun EXISTS_LEFT [] th = th 1348 | EXISTS_LEFT fvs th = 1349 let val hfvs = map (fn h => {hyp = h, fvs = free_vars h}) (Thm.hyp th) ; 1350 val fvs_c = free_vars (concl th) ; 1351 in EXISTS_LEFT' false fvs_c hfvs fvs th end ; 1352 1353(* EXISTS_LEFT1 : term -> thm -> thm 1354 for the free var argument, replace hyps containing the free var 1355 by their conjunction, existentially quantified over the free var; 1356 error if this can't be done for a free var *) 1357fun EXISTS_LEFT1 fv th = 1358 let val hfvs = map (fn h => {hyp = h, fvs = free_vars h}) (Thm.hyp th) ; 1359 val fvs_c = free_vars (concl th) ; 1360 in EXISTS_LEFT' true fvs_c hfvs [fv] th end ; 1361 1362(* --------------------------------------------------------------------------* 1363 * SPEC_UNDISCH_EXL: strips !x, ant ==>, (splitting conjuncts of ant) * 1364 * then EXISTS_LEFT for stripped vars * 1365 * --------------------------------------------------------------------------*) 1366 1367fun SPEC_UNDISCH_EXL thm = 1368 let val (fvs, th1) = strip_gen_left (SPEC_VAR o repeat UNDISCH_SPLIT) thm ; 1369 val th2 = repeat UNDISCH_SPLIT th1 ; 1370 val th3 = EXISTS_LEFT (rev fvs) th2 ; 1371 in th3 end ; 1372 1373(* --------------------------------------------------------------------------* 1374 * MATCH_MP: Matching Modus Ponens for implications. * 1375 * * 1376 * |- !x1 ... xn. P ==> Q |- P' * 1377 * --------------------------------------- * 1378 * |- Q' * 1379 * * 1380 * Matches all types in conclusion except those mentioned in hypotheses. * 1381 * --------------------------------------------------------------------------*) 1382 1383local 1384 fun variants (_, []) = [] 1385 | variants (av, h::rst) = 1386 let val vh = variant av h in vh :: variants (vh :: av, rst) end 1387 fun rassoc_total x theta = Option.getOpt (subst_assoc (equal x) theta, x) 1388 fun req {redex, residue} = (redex = residue) 1389in 1390 fun MATCH_MP ith = 1391 let 1392 val bod = fst (dest_imp (snd (strip_forall (concl ith)))) 1393 val hyptyvars = HOLset.listItems (hyp_tyvars ith) 1394 val lconsts = HOLset.intersection 1395 (FVL [concl ith] empty_tmset, hyp_frees ith) 1396 in 1397 fn th => 1398 let 1399 val mfn = C (Term.match_terml hyptyvars lconsts) (concl th) 1400 val tth = INST_TYPE (snd (mfn bod)) ith 1401 val tbod = fst (dest_imp (snd (strip_forall (concl tth)))) 1402 val tmin = fst (mfn tbod) 1403 val hy1 = HOLset.listItems (hyp_frees tth) 1404 and hy2 = HOLset.listItems (hyp_frees th) 1405 val (avs, (ant, conseq)) = 1406 (I ## dest_imp) (strip_forall (concl tth)) 1407 val (rvs, fvs) = partition (C free_in ant) (free_vars conseq) 1408 val afvs = Lib.set_diff fvs (Lib.set_diff hy1 avs) 1409 val cvs = free_varsl (map (C rassoc_total tmin) rvs) 1410 val vfvs = 1411 map (op |->) (zip afvs (variants (cvs @ hy1 @ hy2, afvs))) 1412 val atmin = (filter (op not o op req) vfvs) @ tmin 1413 val (spl, ill) = partition (C mem avs o #redex) atmin 1414 val fspl = map (C rassoc_total spl) avs 1415 val mth = MP (SPECL fspl (INST ill tth)) th 1416 fun loop [] = [] 1417 | loop (tm :: rst) = 1418 case subst_assoc (equal tm) vfvs of 1419 NONE => loop rst 1420 | SOME x => x :: loop rst 1421 in 1422 GENL (loop avs) mth 1423 end 1424 end 1425end 1426 1427(*---------------------------------------------------------------------------* 1428 * Now higher-order versions of PART_MATCH and MATCH_MP * 1429 *---------------------------------------------------------------------------*) 1430 1431(* IMPORTANT: See the bottom of this file for a longish discussion of some 1432 of the ways this implementation attempts to keep bound variable 1433 names sensible. 1434*) 1435 1436(*---------------------------------------------------------------------------* 1437 * Attempt alpha conversion. * 1438 *---------------------------------------------------------------------------*) 1439 1440fun tryalpha v tm = 1441 let 1442 val (Bvar, Body) = dest_abs tm 1443 in 1444 if v = Bvar 1445 then tm 1446 else if var_occurs v Body 1447 then tryalpha (variant (free_vars tm) v) tm 1448 else mk_abs (v, subst [Bvar |-> v] Body) 1449 end 1450 1451(*---------------------------------------------------------------------------* 1452 * Match up bound variables names. * 1453 *---------------------------------------------------------------------------*) 1454 1455(* first argument is actual term, second is from theorem being matched *) 1456 1457fun match_bvs t1 t2 acc = 1458 case (dest_term t1, dest_term t2) of 1459 (LAMB (v1, b1), LAMB (v2, b2)) => 1460 let 1461 val n1 = fst (dest_var v1) 1462 val n2 = fst (dest_var v2) 1463 val newacc = if n1 = n2 then acc else insert (n1, n2) acc 1464 in 1465 match_bvs b1 b2 newacc 1466 end 1467 | (COMB (l1, r1), COMB (l2, r2)) => match_bvs l1 l2 (match_bvs r1 r2 acc) 1468 | otherwise => acc 1469 1470(* bindings come from match_bvs, telling us which bound variables are going 1471 to get renamed, and thmc is the conclusion of the pattern theorem. 1472 acc is a set of free variables that need to get instantiated away *) 1473 1474fun look_for_avoids bindings thmc acc = 1475 let 1476 val lfa = look_for_avoids bindings 1477 in 1478 case dest_term thmc of 1479 LAMB (v, b) => 1480 let 1481 val (thm_n, _) = dest_var v 1482 in 1483 case Lib.total (rev_assoc thm_n) bindings of 1484 SOME n => 1485 let 1486 val fvs = FVL [b] empty_tmset 1487 fun f (v, acc) = 1488 if #1 (dest_var v) = n 1489 then HOLset.add (acc, v) 1490 else acc 1491 in 1492 lfa b (HOLset.foldl f acc fvs) 1493 end 1494 | NONE => lfa b acc 1495 end 1496 | COMB (l, r) => lfa l (lfa r acc) 1497 | _ => acc 1498 end 1499 1500(*---------------------------------------------------------------------------* 1501 * Modify bound variable names at depth. (Not very efficient...) * 1502 *---------------------------------------------------------------------------*) 1503 1504fun deep_alpha [] tm = tm 1505 | deep_alpha env tm = 1506 case dest_term tm of 1507 LAMB (Bvar, Body) => 1508 (let 1509 val (Name, Ty) = dest_var Bvar 1510 val ((vn', _), newenv) = Lib.pluck (fn (_, x) => x = Name) env 1511 val tm' = tryalpha (mk_var (vn', Ty)) tm 1512 val (iv, ib) = dest_abs tm' 1513 in 1514 mk_abs (iv, deep_alpha newenv ib) 1515 end 1516 handle HOL_ERR _ => mk_abs (Bvar, deep_alpha env Body)) 1517 | COMB (Rator, Rand) => 1518 mk_comb (deep_alpha env Rator, deep_alpha env Rand) 1519 | otherwise => tm 1520 1521(* ------------------------------------------------------------------------- 1522 BETA_VAR 1523 1524 Set up beta-conversion for head instances of free variable v in tm. 1525 1526 EXAMPLES 1527 1528 BETA_VAR (--`x:num`--) (--`(P:num->num->bool) x x`--); 1529 BETA_VAR (--`x:num`--) (--`x + 1`--); 1530 1531 Note (kxs): I am defining this before Conv, so some conversion(al)s are 1532 p(re)-defined here. Ugh. 1533 1534 ========================================================================= 1535 PART_MATCH 1536 1537 Match (higher-order) part of a theorem to a term. 1538 1539 PART_MATCH (snd o strip_forall) BOOL_CASES_AX (--`(P = T) \/ (P = F)`--); 1540 val f = PART_MATCH lhs; 1541 profile2 f NOT_FORALL_THM (--`~!x. (P:num->num->bool) x y`--); 1542 profile2 f NOT_EXISTS_THM (--`?x. ~(P:num->num->bool) x y`--); 1543 profile2 f LEFT_AND_EXISTS_THM 1544 (--`(?x. (P:num->num->bool) x x) /\ Q (y:num)`--); 1545 profile LEFT_AND_EXISTS_CONV 1546 (--`(?x. (P:num->num->bool) x x) /\ Q (x:num)`--); 1547 profile2 f NOT_FORALL_THM (--`~!x. (P:num->num->bool) y x`--); 1548 profile NOT_FORALL_CONV (--`~!x. (P:num->num->bool) y x`--); 1549 val f = PART_MATCH (lhs o snd o strip_imp); 1550 val CRW_THM = mk_thm([],(--`P x ==> Q x (y:num) ==> (x + 0 = x)`--)); 1551 f CRW_THM (--`y + 0`--); 1552 1553 val beta_thm = prove(--`(\x:'a. P x) b = (P b:'b)`--)--, 1554 BETA_TAC THEN REFL_TAC); 1555 val f = profile PART_MATCH lhs beta_thm; 1556 profile f (--`(\x. I x) 1`--); 1557 profile f (--`(\x. x) 1`--); 1558 profile f (--`(\x. P x x:num) 1`--); 1559 1560 The current version attempts to keep variable names constant. This 1561 is courtesy of JRH. 1562 1563 Non renaming version (also courtesy of JRH!!) 1564 1565 fun PART_MATCH partfn th = 1566 let val sth = SPEC_ALL th 1567 val bod = concl sth 1568 val possbetas = mapfilter (fn v => (v,BETA_VAR v bod)) (free_vars bod) 1569 fun finish_fn tyin bvs = 1570 let val npossbetas = map (inst tyin ## I) possbetas 1571 in CONV_RULE (EVERY_CONV (mapfilter (C assoc npossbetas) bvs)) 1572 end 1573 val pbod = partfn bod 1574 in fn tm => 1575 let val (tmin,tyin) = match_term pbod tm 1576 val th0 = INST tmin (INST_TYPE tyin sth) 1577 in finish_fn tyin (map #redex tmin) th0 1578 end 1579 end; 1580 1581 EXAMPLES: 1582 1583 val CET = mk_thm([],(--`(!c. P ($COND c x y) c) = (P x T /\ P y F)`--)); 1584 1585 PART_MATCH lhs FORALL_SIMP (--`!x. y + 1 = 2`--); 1586 PART_MATCH lhs FORALL_SIMP (--`!x. x + 1 = 2`--); (* fails *) 1587 PART_MATCH lhs CET (--`!b. ~(f (b => t | e))`--); 1588 PART_MATCH lhs option_CASE_ELIM (--`!b. ~(P (option_CASE e f b))`--); 1589 PART_MATCH lhs (MK_FORALL (--`c:bool`--) COND_ELIM_THM) 1590 (--`!b. ~(f (b => t | e))`--); 1591 PART_MATCH lhs (MK_FORALL (--`c:bool`--) COND_ELIM_THM) 1592 (--`!b. ~(f (b => t | e))`--); 1593 ho_term_match [] (--`!c. P ($COND c x y)`--) 1594 1595 BUG FIXES & TEST CASES 1596 1597 Variable Renaming: 1598 PART_MATCH (lhs o snd o strip_forall) SKOLEM_THM (--`!p. ?GI. Q GI p`--); 1599 Before renaming this produced: |- (!x. ?y. Q y x) = (?y. !x. Q (y x) x) 1600 After renaming this produced: |- (!p. ?GI. Q GI p) = (?GI. !p. Q (GI p) p) 1601 1602 Variable renaming problem (DRS, Feb 1996): 1603 PART_MATCH lhs NOT_FORALL_THM (--`~!y. P x`--); 1604 Before fix produced: |- ~(!x'. P x) = (?x'. ~(P x)) : thm 1605 After fix produced: |- ~(!y. P x) = (?y. ~(P x)) 1606 Fix: 1607 val bvms = match_bvs tm (inst tyin pbod) [] 1608 Became: 1609 val bvms = match_bvs tm (partfn (concl th0)) [] 1610 1611 Variable renaming problem (DRS, Feb 1996): 1612 PART_MATCH lhs NOT_FORALL_THM (--`~!x. (\y. t) T`--); 1613 Before fix produced (--`?y. ~(\y. t) T`--); 1614 After fix produced (--`?x. ~(\y. t) T`--); 1615 Fix: 1616 Moved beta reduction to be before alpha renaming. This makes 1617 match_bvs more accurate. This was not a problem before the previous 1618 fix. 1619 1620 Another bug (unfixed). bvms = [("x","y"),("E'","x")] 1621 PART_MATCH lhs SWAP_EXISTS_THM (--`?E' x const'. 1622 ((s = s') /\ 1623 (E = E') /\ 1624 (val = Val_Constr (const',x)) /\ 1625 (sym = const)) /\ 1626 (a1 = NONE) /\ 1627 ~(const = const')`--) 1628 ------------------------------------------------------------------------- *) 1629 1630nonfix THENC 1631 1632local 1633 fun COMB_CONV2 c1 c2 M = 1634 let val (f, x) = dest_comb M in MK_COMB (c1 f, c2 x) end 1635 fun ABS_CONV c M = 1636 let val (Bvar, Body) = dest_abs M in ABS Bvar (c Body) end 1637 fun RAND_CONV c M = 1638 let val (Rator, Rand) = dest_comb M in AP_TERM Rator (c Rand) end 1639 fun RATOR_CONV c M = 1640 let val (Rator, Rand) = dest_comb M in AP_THM (c Rator) Rand end 1641 fun TRY_CONV c M = c M handle HOL_ERR _ => REFL M 1642 fun THENC c1 c2 M = 1643 let val th = c1 M in TRANS th (c2 (rhs (concl th))) end 1644 fun EVERY_CONV convl = itlist THENC convl REFL 1645 fun CONV_RULE conv th = EQ_MP (conv (concl th)) th 1646 fun BETA_CONVS n = 1647 if n = 1 then TRY_CONV BETA_CONV 1648 else THENC (RATOR_CONV (BETA_CONVS (n - 1))) (TRY_CONV BETA_CONV) 1649in 1650 fun BETA_VAR v tm = 1651 if is_abs tm 1652 then let 1653 val (Bvar, Body) = dest_abs tm 1654 in 1655 if v = Bvar 1656 then failwith "BETA_VAR: UNCHANGED" 1657 else ABS_CONV (BETA_VAR v Body) end 1658 else case strip_comb tm of 1659 (_, []) => failwith "BETA_VAR: UNCHANGED" 1660 | (oper, args) => 1661 if oper = v 1662 then BETA_CONVS (length args) 1663 else let 1664 val (Rator, Rand) = dest_comb tm 1665 in 1666 let 1667 val lconv = BETA_VAR v Rator 1668 in 1669 let 1670 val rconv = BETA_VAR v Rand 1671 in 1672 COMB_CONV2 lconv rconv 1673 end 1674 handle HOL_ERR _ => RATOR_CONV lconv 1675 end 1676 handle HOL_ERR _ => RAND_CONV (BETA_VAR v Rand) 1677 end 1678 1679 structure Map = Redblackmap 1680 1681 (* count from zero to indicate last argument, up to #args - 1 to indicate 1682 first argument *) 1683 1684 fun arg_CONV 0 c = RAND_CONV c 1685 | arg_CONV n c = RATOR_CONV (arg_CONV (n - 1) c) 1686 1687 fun foldri f acc list = 1688 let 1689 fun foldthis (e, (acc, n)) = (f (n, e, acc), n + 1) 1690 in 1691 #1 (foldr foldthis (acc, 0) list) 1692 end 1693 1694 fun munge_bvars absmap th = 1695 let 1696 fun recurse curposn bvarposns (donebvars, acc) t = 1697 case dest_term t of 1698 LAMB (bv, body) => 1699 let 1700 val newposnmap = Map.insert (bvarposns, bv, curposn) 1701 val (newdonemap, restore) = 1702 (HOLset.delete (donebvars, bv), 1703 fn m => HOLset.add (m, bv)) 1704 handle HOLset.NotFound => 1705 (donebvars, (fn m => HOLset.delete (m, bv) 1706 handle HOLset.NotFound => m)) 1707 val (dbvars, actions) = 1708 recurse 1709 (curposn o ABS_CONV) newposnmap (newdonemap, acc) body 1710 in 1711 (restore dbvars, actions) 1712 end 1713 | COMB _ => 1714 let 1715 val (f, args) = strip_comb t 1716 fun argfold (n, arg, A) = 1717 recurse (curposn o arg_CONV n) bvarposns A arg 1718 in 1719 case Map.peek (absmap, f) of 1720 NONE => foldri argfold (donebvars, acc) args 1721 | SOME abs_t => 1722 let 1723 val (abs_bvars, _) = strip_abs abs_t 1724 val paired_up = ListPair.zip (args, abs_bvars) 1725 fun foldthis 1726 ((arg, absv), acc as (dbvars, actionlist)) = 1727 if HOLset.member (dbvars, arg) 1728 then acc 1729 else case Map.peek (bvarposns, arg) of 1730 NONE => acc 1731 | SOME p => 1732 (HOLset.add (dbvars, arg), 1733 p (ALPHA_CONV absv) :: actionlist) 1734 val (A as (newdbvars, newacc)) = 1735 List.foldl foldthis (donebvars, acc) paired_up 1736 in 1737 foldri argfold A args 1738 end 1739 end 1740 | _ => (donebvars, acc) 1741 in 1742 recurse I (Map.mkDict Term.compare) (empty_tmset, []) (concl th) 1743 end 1744 1745 (* Modified HO_PART_MATCH by PVH on Apr. 25, 2005: code was broken; 1746 repaired by tightening "foldthis" condition for entry to "bound_to_abs"; 1747 see longish note at bottom for more details. *) 1748 1749 (* "bound_vars" returns set of bound variables within term t *) 1750 (* "t" argument is actual term, "acc" is accumulating set, orig. empty *) 1751 1752 local 1753 fun bound_vars1 t acc = 1754 case dest_term t of 1755 LAMB (v, b) => bound_vars1 b (HOLset.add (acc, v)) 1756 | COMB (l, r) => bound_vars1 l (bound_vars1 r acc) 1757 | otherwise => acc 1758 in 1759 fun bound_vars t = bound_vars1 t empty_tmset 1760 end 1761 1762 fun HO_PART_MATCH partfn th = 1763 let 1764 val sth = SPEC_ALL th 1765 val bod = concl sth 1766 val pbod = partfn bod 1767 val possbetas = 1768 mapfilter (fn v => (v, BETA_VAR v bod)) 1769 (filter (can dom_rng o type_of) (free_vars bod)) 1770 fun finish_fn tyin ivs = 1771 let 1772 val npossbetas = 1773 if null tyin 1774 then possbetas 1775 else map (inst tyin ## I) possbetas 1776 in 1777 if null npossbetas 1778 then Lib.I 1779 else CONV_RULE 1780 (EVERY_CONV 1781 (mapfilter (TRY_CONV o C assoc npossbetas) ivs)) 1782 end 1783 val lconsts = 1784 HOLset.intersection (FVL [pbod] empty_tmset, hyp_frees th) 1785 val ltyconsts = HOLset.listItems (hyp_tyvars th) 1786 in 1787 fn tm => 1788 let 1789 val (tmin, tyin) = ho_match_term ltyconsts lconsts pbod tm 1790 val tmbvs = bound_vars tm 1791 fun foldthis ({redex, residue}, acc) = 1792 if is_abs residue 1793 andalso all (fn v => HOLset.member (tmbvs, v)) 1794 (fst (strip_abs residue)) 1795 then Map.insert (acc, redex, residue) else acc 1796 val bound_to_abs = 1797 List.foldl foldthis (Map.mkDict Term.compare) tmin 1798 val sth0 = INST_TYPE tyin sth 1799 val sth0c = concl sth0 1800 val (sth1, tmin') = 1801 case match_bvs tm (partfn sth0c) [] of 1802 [] => (sth0, tmin) 1803 | bvms => 1804 let 1805 val avoids = look_for_avoids bvms sth0c empty_tmset 1806 fun f (v, acc) = (v |-> genvar (type_of v)) :: acc 1807 val newinst = HOLset.foldl f [] avoids 1808 val newthm = INST newinst sth0 1809 val tmin' = map (fn {residue, redex} => 1810 {residue = residue, 1811 redex = Term.subst newinst redex}) 1812 tmin 1813 val thmc = concl newthm 1814 in 1815 (EQ_MP (ALPHA thmc (deep_alpha bvms thmc)) newthm, 1816 tmin') 1817 end 1818 val sth2 = 1819 if Map.numItems bound_to_abs = 0 1820 then sth1 1821 else CONV_RULE 1822 (EVERY_CONV (#2 (munge_bvars bound_to_abs sth1))) 1823 sth1 1824 val th0 = INST tmin' sth2 1825 val th1 = finish_fn tyin (map #redex tmin) th0 1826 in 1827 th1 1828 end 1829 end 1830end 1831 1832fun HO_MATCH_MP ith = 1833 let 1834 val sth = 1835 let 1836 val tm = concl ith 1837 val (avs, bod) = strip_forall tm 1838 val (ant, _) = dest_imp_only bod 1839 in 1840 case partition (C free_in ant) avs of 1841 (_, []) => ith 1842 | (svs, pvs) => 1843 let 1844 val th1 = SPECL avs (ASSUME tm) 1845 val th2 = GENL svs (DISCH ant (GENL pvs (UNDISCH th1))) 1846 in 1847 MP (DISCH tm th2) ith 1848 end 1849 end 1850 handle HOL_ERR _ => raise ERR "MATCH_MP" "Not an implication" 1851 val match_fun = HO_PART_MATCH (fst o dest_imp_only) sth 1852 in 1853 fn th => 1854 MP (match_fun (concl th)) th 1855 handle HOL_ERR _ => raise ERR "MATCH_MP" "No match" 1856 end 1857 1858(* ===================================================================== 1859 The "resolution" tactics for HOL (outmoded technology, but 1860 sometimes useful) uses RES_CANON and SPEC_ALL 1861 ===================================================================== 1862 1863 Put a theorem 1864 1865 |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t 1866 1867 into canonical form for resolution by splitting conjunctions apart 1868 (like IMP_CANON but without the stripping out of quantifiers and only 1869 outermost negations being converted to implications). 1870 1871 ~t ---> t ==> F (at outermost level) 1872 t1 /\ t2 ---> t1, t2 1873 (t1/\t2)==>t ---> t1==> (t2==>t) 1874 (t1\/t2)==>t ---> t1==>t, t2==>t 1875 1876 Modification provided by David Shepherd of Inmos to make resolution 1877 work with equalities as well as implications. HOL88.1.08,23 jun 1989. 1878 1879 t1 = t2 ---> t1=t2, t1==>t2, t2==>t1 1880 1881 Modification provided by T Melham to deal with the scope of 1882 universal quantifiers. [TFM 90.04.24] 1883 1884 !x. t1 ==> t2 ---> t1 ==> !x.t2 (x not free in t1) 1885 1886 The old code is given below: 1887 1888 letrec RES_CANON_FUN th = 1889 let w = concl th in 1890 if is_conj w 1891 then RES_CANON_FUN(CONJUNCT1 th)@RES_CANON_FUN(CONJUNCT2 th) 1892 else if is_imp w & not(is_neg w) then 1893 let ante,conc = dest_imp w in 1894 if is_conj ante then 1895 let a,b = dest_conj ante in 1896 RES_CANON_FUN 1897 (DISCH a (DISCH b (MP th (CONJ (ASSUME a) (ASSUME b))))) 1898 else if is_disj ante then 1899 let a,b = dest_disj ante in 1900 RES_CANON_FUN (DISCH a (MP th (DISJ1 (ASSUME a) b))) @ 1901 RES_CANON_FUN (DISCH b (MP th (DISJ2 a (ASSUME b)))) 1902 else 1903 map (DISCH ante) (RES_CANON_FUN (UNDISCH th)) 1904 else [th]; 1905 1906 This version deleted for HOL 1.12 (see below) [TFM 91.01.17] 1907 1908 let RES_CANON = 1909 letrec FN th = 1910 let w = concl th in 1911 if (is_conj w) then FN(CONJUNCT1 th) @ FN(CONJUNCT2 th) else 1912 if ((is_imp w) & not(is_neg w)) then 1913 let ante,conc = dest_imp w in 1914 if (is_conj ante) then 1915 let a,b = dest_conj ante in 1916 let ath = ASSUME a and bth = ASSUME b 1917 in FN (DISCH a (DISCH b (MP th (CONJ ath bth)))) else 1918 if is_disj ante then 1919 let a,b = dest_disj ante in 1920 let ath = ASSUME a and bth = ASSUME b 1921 in FN (DISCH a (MP th (DISJ1 ath b))) @ 1922 FN (DISCH b (MP th (DISJ2 a bth))) 1923 else map (GEN_ALL o (DISCH ante)) (FN (UNDISCH th)) 1924 else if is_eq w then 1925 let l,r = dest_eq w in 1926 if (type_of l = ":bool") 1927 then let (th1,th2) = EQ_IMP_RULE th 1928 in (GEN_ALL th) . ((FN th1) @ (FN th2)) 1929 else [GEN_ALL th] 1930 else [GEN_ALL th] in 1931 \th. (let vars,w = strip_forall(concl th) in 1932 let th1 = if (is_neg w) 1933 then NOT_ELIM(SPEC_ALL th) 1934 else (SPEC_ALL th) in 1935 map GEN_ALL (FN th1) ? failwith `RES_CANON`); 1936 1937 --------------------------------------------------------------------- 1938 New RES_CANON for version 1.12. [TFM 90.12.07] 1939 1940 The complete list of transformations is now: 1941 1942 ~t ---> t ==> F (at outermost level) 1943 t1 /\ t2 ---> t1, t2 (at outermost level) 1944 (t1/\t2)==>t ---> t1==>(t2==>t), t2==>(t1==>t) 1945 (t1\/t2)==>t ---> t1==>t, t2==>t 1946 t1 = t2 ---> t1==>t2, t2==>t1 1947 !x. t1 ==> t2 ---> t1 ==> !x.t2 (x not free in t1) 1948 (?x.t1) ==> t2 ---> !x'. t1[x'/x] ==> t2 1949 1950 The function now fails if no implications can be derived from the 1951 input theorem. 1952 1953 =====================================================================*) 1954 1955local 1956 fun not_elim th = 1957 if is_neg (concl th) then (true, NOT_ELIM th) else (false, th) 1958 fun canon (fl, th) = 1959 let 1960 val w = concl th 1961 in 1962 if is_conj w 1963 then let 1964 val (th1, th2) = CONJ_PAIR th 1965 in 1966 canon (fl, th1) @ canon (fl, th2) 1967 end 1968 else if is_imp w andalso not (is_neg w) 1969 then 1970 let 1971 val (ant, _) = dest_imp w 1972 in 1973 if is_conj ant 1974 then 1975 let 1976 val (conj1, conj2) = dest_conj ant 1977 val cth = MP th (CONJ (ASSUME conj1) (ASSUME conj2)) 1978 val th1 = DISCH conj2 cth 1979 and th2 = DISCH conj1 cth 1980 in 1981 canon (true, DISCH conj1 th1) @ 1982 canon (true, DISCH conj2 th2) 1983 end 1984 else if is_disj ant 1985 then 1986 let 1987 val (disj1, disj2) = dest_disj ant 1988 val ath = DISJ1 (ASSUME disj1) disj2 1989 and bth = DISJ2 disj1 (ASSUME disj2) 1990 val th1 = DISCH disj1 (MP th ath) 1991 and th2 = DISCH disj2 (MP th bth) 1992 in 1993 canon (true, th1) @ canon (true, th2) 1994 end 1995 else if is_exists ant 1996 then 1997 let 1998 val (Bvar, Body) = dest_exists ant 1999 val newv = variant (thm_frees th) Bvar 2000 val newa = subst [Bvar |-> newv] Body 2001 val th1 = MP th (EXISTS (ant, newv) (ASSUME newa)) 2002 in 2003 canon (true, DISCH newa th1) 2004 end 2005 else map (GEN_ALL o (DISCH ant)) (canon (true, UNDISCH th)) 2006 end 2007 else if is_eq w andalso type_of (rand w) = Type.bool 2008 then 2009 let 2010 val (th1, th2) = EQ_IMP_RULE th 2011 in 2012 (if fl then [GEN_ALL th] else []) @ 2013 canon (true, th1) @ canon (true, th2) 2014 end 2015 else if is_forall w 2016 then 2017 let 2018 val (vs, _) = strip_forall w 2019 val fvs = HOLset.listItems (FVL [concl th] (hyp_frees th)) 2020 val nvs = 2021 itlist (fn v => fn nv => variant (nv @ fvs) v::nv) vs [] 2022 in 2023 canon (fl, SPECL nvs th) 2024 end 2025 else if fl 2026 then [GEN_ALL th] 2027 else [] 2028 end 2029in 2030 fun RES_CANON th = 2031 let 2032 val conjlist = CONJUNCTS (SPEC_ALL th) 2033 fun operate th accum = 2034 accum @ map GEN_ALL (canon (not_elim (SPEC_ALL th))) 2035 val imps = Lib.rev_itlist operate conjlist [] 2036 in 2037 Lib.assert (op not o null) imps 2038 end 2039 handle HOL_ERR _ => 2040 raise ERR "RES_CANON" 2041 "No implication is derivable from input thm" 2042end 2043 2044(* ---------------------------------------------------------------------- 2045 IRULE_CANON 2046 2047 Aggressive canonicalisation of introduction rules so that it takes on 2048 the form 2049 2050 |- !vs. cs ==> concl 2051 2052 where vs all appear in concl, and may appear among cs. 2053 2054 The cs may not be present at all, but if so is a conjunction of 2055 exhyps, where each exhyp is of the form 2056 2057 ?e1 e2 .. en. c1 /\ c2 /\ .. cm 2058 2059 ---------------------------------------------------------------------- *) 2060 2061 2062local 2063 fun AIMP_RULE th = 2064 let 2065 val (l, r) = dest_imp (concl th) 2066 val (c1, c2) = dest_conj l 2067 val cth = CONJ (ASSUME c1) (ASSUME c2) 2068 in 2069 DISCH c1 (DISCH c2 (MP th cth)) 2070 end 2071 2072 fun (s1 - s2) = HOLset.difference(s1,s2) 2073 fun norm th = 2074 if is_forall (concl th) then norm (SPEC_ALL th) 2075 else 2076 case Lib.total dest_imp (concl th) of 2077 NONE => th 2078 | SOME (l,r) => 2079 if is_conj l then norm (AIMP_RULE th) 2080 else norm (UNDISCH th) 2081 2082fun group_hyps gfvs tlist = 2083 let 2084 fun overlaps fvset (tfvs,_) = 2085 not (HOLset.isEmpty (HOLset.intersection(fvset, tfvs))) 2086 fun union ((fvset1, tlist1), (fvset2, tlist2)) = 2087 (HOLset.union(fvset1, fvset2), tlist1 @ tlist2) 2088 fun recurse acc tlist = 2089 case tlist of 2090 [] => acc 2091 | t::ts => 2092 let 2093 val tfvs = FVL [t] empty_tmset - gfvs 2094 in 2095 case List.partition (overlaps tfvs) acc of 2096 ([], _) => recurse ((tfvs,[t])::acc) ts 2097 | (ovlaps, rest) => 2098 recurse (List.foldl union (tfvs, [t]) ovlaps :: rest) ts 2099 end 2100 in 2101 recurse [] tlist 2102 end 2103 2104fun CHOOSEL vs t th = 2105 let 2106 fun foldthis (v,(t,th)) = 2107 let val ext = mk_exists(v,t) 2108 in 2109 (ext, CHOOSE (v,ASSUME ext) th) 2110 end 2111 in 2112 List.foldr foldthis (t,th) vs 2113 end 2114 2115fun CONJL ts th = let 2116 val c = list_mk_conj ts 2117 val cths = CONJUNCTS (ASSUME c) 2118in 2119 (List.foldl (fn (c,th) => PROVE_HYP c th) th cths, c) 2120end 2121 2122fun reconstitute groups th = 2123 let 2124 fun recurse acc groups th = 2125 case groups of 2126 [] => (acc, th) 2127 | (fvset, ts) :: rest => 2128 let 2129 val (th1,c) = CONJL ts th 2130 val (ext, th2) = CHOOSEL (HOLset.listItems fvset) c th1 2131 in 2132 recurse (ext::acc) rest th2 2133 end 2134 in 2135 recurse [] groups th 2136 end 2137in 2138fun IRULE_CANON th = 2139 let 2140 val th1 = norm (GEN_ALL th) 2141 val orighyps = hypset th 2142 val origl = HOLset.listItems orighyps 2143 val gfvs = FVL (concl th1 :: origl) empty_tmset 2144 val newhyps = hypset th1 - orighyps 2145 val grouped = group_hyps gfvs (HOLset.listItems newhyps) 2146 val (cs, th2) = reconstitute grouped th1 2147 in 2148 case cs of 2149 [] => GEN_ALL th2 2150 | _ => 2151 let 2152 val (th3,c) = CONJL cs th2 2153 in 2154 DISCH c th3 |> GEN_ALL 2155 end 2156 end 2157end (* local *) 2158 2159(*---------------------------------------------------------------------------* 2160 * Routines supporting the definition of types * 2161 * * 2162 * AUTHOR : (c) Tom Melham, University of Cambridge * 2163 * * 2164 * NAME: define_new_type_bijections * 2165 * * 2166 * DESCRIPTION: define isomorphism constants based on a type definition. * 2167 * * 2168 * USAGE: define_new_type_bijections name ABS REP tyax * 2169 * * 2170 * ARGUMENTS: tyax -- a type-defining axiom of the form returned by * 2171 * new_type_definition. For example: * 2172 * * 2173 * ?rep. TYPE_DEFINITION P rep * 2174 * * 2175 * ABS --- the name of the required abstraction function * 2176 * * 2177 * REP --- the name of the required representation function * 2178 * * 2179 * name --- the name under which the definition is stored * 2180 * * 2181 * SIDE EFFECTS: Introduces a definition for two constants `ABS` and * 2182 * (--`REP`--) by the constant specification: * 2183 * * 2184 * |- ?ABS REP. (!a. ABS(REP a) = a) /\ * 2185 * (!r. P r = (REP(ABS r) = r) * 2186 * * 2187 * The resulting constant specification is stored under * 2188 * the name given as the first argument. * 2189 * * 2190 * FAILURE: if input theorem of wrong form. * 2191 * * 2192 * RETURNS: The defining property of the representation and abstraction * 2193 * functions, given by: * 2194 * * 2195 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2196 *---------------------------------------------------------------------------*) 2197 2198fun define_new_type_bijections {name, ABS, REP, tyax} = 2199 if not (HOLset.isEmpty (hypset tyax)) 2200 then raise ERR "define_new_type_bijections" 2201 "input theorem must have no assumptions" 2202 else 2203 let 2204 val (P, rep) = case strip_comb (snd (dest_exists (concl tyax))) of 2205 (_, [P, rep]) => (P, rep) 2206 | _ => raise Match 2207 val (a, r) = Type.dom_rng (type_of rep) 2208 in 2209 Rsyntax.new_specification 2210 {name = name, 2211 sat_thm = 2212 MP (SPEC P (INST_TYPE [beta |-> a, alpha |-> r] ABS_REP_THM)) tyax, 2213 consts = [{const_name = REP, fixity = NONE}, 2214 {const_name = ABS, fixity = NONE}]} 2215 end 2216 handle e => 2217 raise (wrap_exn "Drule" 2218 ("define_new_type_bijections {name=\""^name^"\"...}") 2219 e) 2220 2221(* --------------------------------------------------------------------------* 2222 * NAME: prove_rep_fn_one_one * 2223 * * 2224 * DESCRIPTION: prove that a type representation function is one-to-one. * 2225 * * 2226 * USAGE: if th is a theorem of the kind returned by the ML function * 2227 * define_new_type_bijections: * 2228 * * 2229 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2230 * * 2231 * then prove_rep_fn_one_one th will prove and return a theorem * 2232 * stating that the representation function REP is one-to-one: * 2233 * * 2234 * |- !a a'. (REP a = REP a') = (a = a') * 2235 * * 2236 *---------------------------------------------------------------------------*) 2237 2238fun prove_rep_fn_one_one th = 2239 let 2240 val thm = CONJUNCT1 th 2241 val (_, Body) = dest_forall (concl thm) 2242 val (A, Rand) = dest_comb (lhs Body) 2243 val (R, _)= dest_comb Rand 2244 val (aty, rty) = case Type.dest_type (type_of R) of 2245 (_, [aty, rty]) => (aty, rty) 2246 | _ => raise Match 2247 val a = mk_primed_var ("a", aty) 2248 val a' = variant [a] a 2249 val a_eq_a' = mk_eq (a, a') 2250 and Ra_eq_Ra' = mk_eq (mk_comb (R, a), mk_comb (R, a')) 2251 val th1 = AP_TERM A (ASSUME Ra_eq_Ra') 2252 val ga1 = genvar aty 2253 and ga2 = genvar aty 2254 val th2 = SUBST [ga1 |-> SPEC a thm, ga2 |-> SPEC a' thm] 2255 (mk_eq (ga1, ga2)) th1 2256 val th3 = DISCH a_eq_a' (AP_TERM R (ASSUME a_eq_a')) 2257 in 2258 GEN a (GEN a' (IMP_ANTISYM_RULE (DISCH Ra_eq_Ra' th2) th3)) 2259 end 2260 handle HOL_ERR _ => raise ERR "prove_rep_fn_one_one" "" 2261 | Bind => raise ERR "prove_rep_fn_one_one" 2262 ("Theorem not of right form: must be\n\ 2263 \ |- (!a. to (from a) = a) /\\\ 2264 \ (!r. P r = (from (to r) = r))") 2265 2266(* --------------------------------------------------------------------------* 2267 * NAME: prove_rep_fn_onto * 2268 * * 2269 * DESCRIPTION: prove that a type representation function is onto. * 2270 * * 2271 * USAGE: if th is a theorem of the kind returned by the ML function * 2272 * define_new_type_bijections: * 2273 * * 2274 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2275 * * 2276 * then prove_rep_fn_onto th will prove and return a theorem * 2277 * stating that the representation function REP is onto: * 2278 * * 2279 * |- !r. P r = (?a. r = REP a) * 2280 * * 2281 *---------------------------------------------------------------------------*) 2282 2283fun prove_rep_fn_onto th = 2284 let 2285 val (th1, th2) = case CONJUNCTS th of 2286 [th1, th2] => (th1, th2) 2287 | _ => raise Match 2288 val (Bvar, Body) = dest_forall (concl th2) 2289 val (_, eq) = dest_eq Body 2290 val (RE, ar) = dest_comb (lhs eq) 2291 val a = mk_primed_var ("a", type_of ar) 2292 val sra = mk_eq (Bvar, mk_comb (RE, a)) 2293 val ex = mk_exists (a, sra) 2294 val imp1 = EXISTS (ex, ar) (SYM (ASSUME eq)) 2295 val v = genvar (type_of Bvar) 2296 and A = rator ar 2297 and ass = AP_TERM RE (SPEC a th1) 2298 val th = SUBST [v |-> SYM (ASSUME sra)] 2299 (mk_eq (mk_comb (RE, mk_comb (A, v)), v)) ass 2300 val imp2 = CHOOSE (a, ASSUME ex) th 2301 val swap = IMP_ANTISYM_RULE (DISCH eq imp1) (DISCH ex imp2) 2302 in 2303 GEN Bvar (TRANS (SPEC Bvar th2) swap) 2304 end 2305 handle HOL_ERR _ => raise ERR "prove_rep_fn_onto" "" 2306 | Bind => raise ERR "prove_rep_fn_onto" 2307 ("Theorem not of right form: must be\n\ 2308 \ (!a. to (from a) = a) /\\\ 2309 \ (!r. P r = (from (to r) = r))") 2310 2311(* --------------------------------------------------------------------------* 2312 * NAME: prove_abs_fn_onto * 2313 * * 2314 * DESCRIPTION: prove that a type abstraction function is onto. * 2315 * * 2316 * USAGE: if th is a theorem of the kind returned by the ML function * 2317 * define_new_type_bijections: * 2318 * * 2319 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2320 * * 2321 * then prove_abs_fn_onto th will prove and return a theorem * 2322 * stating that the abstraction function ABS is onto: * 2323 * * 2324 * |- !a. ?r. (a = ABS r) /\ P r * 2325 * * 2326 * --------------------------------------------------------------------------*) 2327 2328fun prove_abs_fn_onto th = 2329 let 2330 val (th1, th2) = case CONJUNCTS th of 2331 [th1, th2] => (th1, th2) 2332 | _ => raise Match 2333 val (bv_th1, Body) = dest_forall (concl th1) 2334 val (A, Rand) = dest_comb (lhs Body) 2335 val R = rator Rand 2336 val rb = mk_comb (R, bv_th1) 2337 val bth1 = SPEC bv_th1 th1 2338 val thm1 = EQT_ELIM (TRANS (SPEC rb th2) (EQT_INTRO (AP_TERM R bth1))) 2339 val thm2 = SYM bth1 2340 val (r, Body) = dest_forall (concl th2) 2341 val P = rator (lhs Body) 2342 val ex = 2343 mk_exists (r, mk_conj (mk_eq (bv_th1, mk_comb (A, r)), mk_comb (P, r))) 2344 in 2345 GEN bv_th1 (EXISTS (ex, rb) (CONJ thm2 thm1)) 2346 end 2347 handle HOL_ERR _ => raise ERR "prove_abs_fn_onto" "" 2348 | Bind => raise ERR "prove_abs_fn_one_onto" 2349 ("Theorem not of right form: must be\n\ 2350 \ |- (!a. to (from a) = a) /\\\ 2351 \ (!r. P r = (from (to r) = r))") 2352 2353(* --------------------------------------------------------------------------* 2354 * NAME: prove_abs_fn_one_one * 2355 * * 2356 * DESCRIPTION: prove that a type abstraction function is one-to-one. * 2357 * * 2358 * USAGE: if th is a theorem of the kind returned by the ML function * 2359 * define_new_type_bijections: * 2360 * * 2361 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2362 * * 2363 * then prove_abs_fn_one_one th will prove and return a theorem * 2364 * stating that the abstraction function ABS is one-to-one: * 2365 * * 2366 * |- !r r'. P r ==> * 2367 * P r' ==> * 2368 * (ABS r = ABS r') ==> (r = r') * 2369 * * 2370 * --------------------------------------------------------------------------*) 2371 2372fun prove_abs_fn_one_one th = 2373 let 2374 val (th1, th2) = case CONJUNCTS th of 2375 [th1, th2] => (th1, th2) 2376 | _ => raise Match 2377 val (r, Body) = dest_forall (concl th2) 2378 val P = rator (lhs Body) 2379 val (A, Rand) = dest_comb (lhs (snd (dest_forall (concl th1)))) 2380 val R = rator Rand 2381 val r' = variant [r] r 2382 val r_eq_r' = mk_eq (r, r') 2383 val Pr = mk_comb (P, r) 2384 val Pr' = mk_comb (P, r') 2385 val as1 = ASSUME Pr 2386 and as2 = ASSUME Pr' 2387 val t1 = EQ_MP (SPEC r th2) as1 2388 and t2 = EQ_MP (SPEC r' th2) as2 2389 val eq = mk_eq (mk_comb (A, r), mk_comb (A, r')) 2390 val v1 = genvar (type_of r) 2391 and v2 = genvar (type_of r) 2392 val i1 = DISCH eq (SUBST [v1 |-> t1, v2 |-> t2] 2393 (mk_eq (v1, v2)) (AP_TERM R (ASSUME eq))) 2394 val i2 = DISCH r_eq_r' (AP_TERM A (ASSUME r_eq_r')) 2395 val thm = IMP_ANTISYM_RULE i1 i2 2396 val disch = DISCH Pr (DISCH Pr' thm) 2397 in 2398 GEN r (GEN r' disch) 2399 end 2400 handle HOL_ERR _ => raise ERR "prove_abs_fn_one_one" "" 2401 | Bind => raise ERR "prove_abs_fn_one_one" 2402 ("Theorem not of right form: must be\n\ 2403 \ |- (!a. to (from a) = a) /\\\ 2404 \ (!r. P r = (from (to r) = r))") 2405 2406(*---------------------------------------------------------------------------* 2407 * Take an AC pair, normalize them, then prove left-commutativity * 2408 *---------------------------------------------------------------------------*) 2409 2410local 2411 (* Rules related to "semantic tags" for controlling rewriting *) 2412 val is_comm = can (match_term comm_tm) 2413 val is_assoc = can (match_term assoc_tm) 2414 2415 fun regen th = GENL (free_vars_lr (concl th)) th 2416 2417 fun err () = (HOL_MESG "unable to AC-normalize input" 2418 ; raise ERR "norm_ac" "failed") 2419 2420 (* Classify a pair of theorems as one assoc. thm and one comm. thm. Then 2421 return pair (A,C) where A has the form |- f(x,f(y,z)) = f(f(x,y),z) *) 2422 2423 fun norm_ac (th1, th2) = 2424 let 2425 val th1' = SPEC_ALL th1 2426 val th2' = SPEC_ALL th2 2427 val tm1 = concl th1' 2428 val tm2 = concl th2' 2429 in 2430 if is_comm tm2 2431 then if is_assoc tm1 2432 then (regen th1', regen th2') 2433 else let 2434 val th1a = SYM th1' 2435 in 2436 if is_assoc (concl th1a) 2437 then (regen th1a, regen th2') 2438 else err () 2439 end 2440 else if is_comm tm1 2441 then if is_assoc tm2 2442 then (regen th2', regen th1') 2443 else let 2444 val th2a = SYM th2' 2445 in 2446 if is_assoc (concl th2a) 2447 then (regen th2a, regen th1') 2448 else err () 2449 end 2450 else err () 2451 end 2452in 2453 fun MK_AC_LCOMM (th1, th2) = 2454 let 2455 val (a, c) = norm_ac (th1, th2) 2456 val lcomm = MATCH_MP (MATCH_MP LCOMM_THM a) c 2457 in 2458 (regen (SYM (SPEC_ALL a)), c, lcomm) 2459 end 2460end 2461 2462end (* Drule *) 2463 2464(* ====================================================================== 2465 HO_PART_MATCH and bound variables 2466 ====================================================================== 2467 2468Given 2469 2470 val th = GSYM RIGHT_EXISTS_AND_THM 2471 = |- P /\ (?x. Q x) = ?x. P /\ Q x 2472 2473the old implementation would come back from 2474 2475 HO_REWR_CONV th ``P x /\ ?y. Q y`` 2476 2477with 2478 2479 (P x /\ ?y. Q y) = (?x'. P x /\ Q x') 2480 2481This is because of the following: in HO_PART_MATCH, there is code that 2482attempts to rename bound variables from the rewrite theorem so that 2483they match the bound variables in the original term. 2484 2485After performing the ho_match_term, and doing the instantiation, the 2486resulting theorem is 2487 2488 (P x /\ ?x. Q x) = (?x'. P x /\ Q x') 2489 2490The renaming on the rhs has to happen to avoid unsoundness, and 2491happens immediately in the name-carrying kernel, and will happen 2492whenever a dest_abs is done in the dB kernel. Anyway, in the fixup 2493phase, the implementation first notices that ?x.Q x in the pattern 2494corresponds to ?y. Q y in the term. It then passes over the term 2495replacing bound x's with y's. (In the dB kernel, it can't see that 2496the bound variable on the right is actually still an x because 2497dest_abs will rename the x to x'.) 2498 2499So, I thought I would fix this by doing the bound-variable fixup on 2500the pattern theorem before it was instantiated. So, I look at 2501 2502 P /\ ?x. Q x 2503 2504compare it to P x /\ ?y. Q y, and see that bound x needs to be 2505replaced by y throughout the theorem, giving 2506 2507 (P /\ ?y. Q y) = (?y. P /\ Q y) 2508 2509Then the instantiation can be done, producing 2510 2511 (P x /\ ?y. Q y) = (?y. P x /\ Q y) 2512 2513and it's all lovely. (This is also more efficient than the current 2514method because the traversal is only of the original theorem, not its 2515possibly much larger instantiation.) 2516 2517Unfortunately, there are still problems. Consider, this LHS 2518 2519 p /\ ?P. FINITE P 2520 2521when you do the bound variable fix to the rewrite theorem early, you 2522get 2523 2524 (P /\ ?P. Q P) = (?P'. P /\ Q P') 2525 2526The free variables in the theorem itself get in the way. The fix is 2527to examine whether or not the new bound variable clashes with a named 2528variable in the body of the theorem. If so, then the theorem has that 2529variable instantiated to a genvar. (The instantiation returned by 2530ho_match_term also needs to be adjusted because it may be expecting to 2531instantiate some of the pattern theorem's free variables.) 2532 2533So, the code in match_bvs figures out what renamings of bound 2534variables need to happen, and then a traversal of the *whole* theorem 2535takes to see what free variables need to be instantiated into genvars. 2536Then, given the example, the main code in HO_PART_MATCH will produce 2537 2538 (%gv /\ ?x. Q x) = (?x. %gv /\ Q x) 2539 2540before then fixing the bound variables to produce 2541 2542 (%gv /\ ?P. Q P) = (?P. %gv /\ Q P) 2543 2544Finally, this theorem will be instantiated with bindings for Q and 2545%gv [%gv |-> p, Q |-> FINITE]. 2546 2547 ------------------------------ 2548 2549Part 2. 2550 2551Even with the above in place, the ho-part matcher can make a mess of 2552things like the congruence rule for RES_FORALL_CONG, 2553 2554 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==> 2555 (RES_FORALL P f = RES_FORALL Q g) 2556 2557HO_PART_MATCH only gets called with its "partfn" being to look at the 2558LHS of the last equation. Then, when the side conditions are looked 2559over, x gets picked as a bound variable, and any bound variable in f 2560gets ignored. 2561 2562The code in munge_bvars gets around this failing by searching the 2563whole theorem for instances of variables that are going to be 2564instantiated with abstractions that are next to bound variables. (In 2565the example, this search will find f applied to the bound x.) If such 2566a situation is found, it specifies that the bound variable be renamed 2567to match the bound variable of the abstraction. 2568 2569In this way 2570 2571 !y::P. Q y 2572 2573won't get rewritten to 2574 2575 !x::P'. Q' x 2576 2577 ------------------------------ 2578 2579Part 3. (By Peter V. Homeier) 2580 2581The above code was broken for higher order rewriting, such as 2582 2583val th = ASSUME ``!f:'a->'b. A (\x:'c. B (f (C x)) :'d) = (\x. f x)``; 2584val tm = ``A (\rose:'c. B (g (C rose :'a) (C rose) :'b) :'d) : 'a->'b``; 2585HO_PART_MATCH lhs th tm; 2586 2587produced 2588 2589 A (\rose. B (g (C rose) (C rose))) = (\gvar. g gvar gvar) 2590 2591where gvar was a freshly generated "genvar", instead of the correct 2592 2593 A (\rose. B (g (C rose) (C rose))) = (\rose. g rose rose) 2594 2595The reason the prior code did not work was that not only was the 2596match of f with (\y. Q y) recognized for the Part 2 example above, 2597but also the match of f with (\gvar. g gvar gvar) in the "rose" example. 2598The code then "munged" the result by trying to change instances of the 2599"rose" bound variable to "gvar". 2600 2601This was fixed by tightening the condition for entrance to the set of 2602bound variables which are to be so "munged", by adding the condition 2603that the bound variables ("y" in the Part 2 example, "gvar" in this one) 2604must all be contained within the set of bound variables within the term 2605"tm". If they are not, then the "munge" operation is not needed, since 2606that attempts to alter bound variable names to fit the given term, 2607and if the suggested new variable names did not come from the term, 2608there is no reason to change the old ones. 2609*) 2610