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 aconv (concl th) boolSyntax.F then NOT_INTRO (DISCH t th) 596 else DISCH t th) 597 handle HOL_ERR _ => raise ERR "NEG_DISCH" "" 598 599(*---------------------------------------------------------------------------* 600 * A |- ~(t1 = t2) * 601 * ----------------- * 602 * A |- ~(t2 = t1) * 603 *---------------------------------------------------------------------------*) 604 605fun NOT_EQ_SYM th = 606 let 607 val t = (mk_eq o Lib.swap o dest_eq o dest_neg o concl) th 608 in 609 MP (SPEC t IMP_F) (DISCH t (MP th (SYM (ASSUME t)))) 610 end 611 612(* --------------------------------------------------------------------------* 613 * EQF_INTRO: inference rule for introducing equality with "F". * 614 * * 615 * ~tm * 616 * ----------- EQF_INTRO * 617 * tm = F * 618 * * 619 * [TFM 90.05.08] * 620 * --------------------------------------------------------------------------*) 621 622local 623 val Fth = ASSUME F 624in 625 fun EQF_INTRO th = 626 IMP_ANTISYM_RULE (NOT_ELIM th) 627 (DISCH F (CONTR (dest_neg (concl th)) Fth)) 628 handle HOL_ERR _ => raise ERR "EQF_INTRO" "" 629end 630 631(* --------------------------------------------------------------------------* 632 * EQF_ELIM: inference rule for eliminating equality with "F". * 633 * * 634 * |- tm = F * 635 * ----------- EQF_ELIM * 636 * |- ~ tm * 637 * * 638 * [TFM 90.08.23] * 639 * --------------------------------------------------------------------------*) 640 641fun EQF_ELIM th = 642 let 643 val (lhs, rhs) = dest_eq (concl th) 644 val _ = assert (aconv boolSyntax.F) rhs 645 in 646 NOT_INTRO (DISCH lhs (EQ_MP th (ASSUME lhs))) 647 end 648 handle HOL_ERR _ => raise ERR "EQF_ELIM" "" 649 650(* --------------------------------------------------------------------------* 651 * ISPEC: specialization, with type instantation if necessary. * 652 * * 653 * A |- !x:ty.tm * 654 * ----------------------- ISPEC "t:ty'" * 655 * A |- tm[t/x] * 656 * * 657 * (where t is free for x in tm, and ty' is an instance of ty) * 658 * --------------------------------------------------------------------------*) 659 660local 661 fun err s = raise ERR "ISPEC" (": " ^ s) 662in 663 fun ISPEC t th = 664 let 665 val (Bvar, _) = 666 dest_forall (concl th) 667 handle HOL_ERR _ => err "input theorem not universally quantified" 668 val (_, inst) = 669 match_term Bvar t 670 handle HOL_ERR _ => err "can't type-instantiate input theorem" 671 in 672 SPEC t (INST_TYPE inst th) 673 handle HOL_ERR _ => err "type variable free in assumptions" 674 end 675end 676 677(* --------------------------------------------------------------------------* 678 * ISPECL: iterated specialization, with type instantiation if necessary. * 679 * * 680 * A |- !x1...xn.tm * 681 * --------------------------------- ISPECL ["t1",...,"tn"] * 682 * A |- tm[t1/x1,...,tn/xn] * 683 * * 684 * (where ti is free for xi in tm) * 685 * * 686 * Note: the following is simpler but it DOESN'T WORK. * 687 * * 688 * fun ISPECL tms th = rev_itlist ISPEC tms th * 689 * * 690 * --------------------------------------------------------------------------*) 691 692local 693 fun strip [] _ = [] (* Returns a list of (pat,ob) pairs. *) 694 | strip (tm :: tml) M = 695 let 696 val (Bvar, Body) = dest_forall M 697 in 698 (type_of Bvar, type_of tm)::strip tml Body 699 end 700 fun merge [] theta = theta 701 | merge ((x as {redex, residue})::rst) theta = 702 case subst_assoc (equal redex) theta of 703 NONE => x :: merge rst theta 704 | SOME rdue => if residue = rdue then merge rst theta 705 else raise ERR "ISPECL" "" 706 fun err s = raise ERR "ISPECL" s 707in 708 fun ISPECL [] = I 709 | ISPECL [tm] = ISPEC tm 710 | ISPECL tms = 711 fn th => 712 let 713 val pairs = 714 strip tms (concl th) 715 handle HOL_ERR _ => err "list of terms too long for theorem" 716 val inst = 717 rev_itlist 718 (fn (pat, ob) => fn ty_theta => 719 let 720 val theta = Type.match_type pat ob 721 in 722 merge theta ty_theta 723 end) pairs [] 724 handle HOL_ERR _ => err "can't type-instantiate input theorem" 725 in 726 SPECL tms (INST_TYPE inst th) 727 handle HOL_ERR _ => err "type variable free in assumptions" 728 end 729end 730 731(*---------------------------------------------------------------------------* 732 * Generalise a theorem over all variables free in conclusion but not in hyps* 733 * * 734 * A |- t[x1,...,xn] * 735 * ---------------------------- * 736 * A |- !x1...xn.t[x1,...,xn] * 737 *---------------------------------------------------------------------------*) 738 739fun GEN_ALL th = 740 HOLset.foldl (Lib.uncurry GEN) th 741 (HOLset.difference (FVL [concl th] empty_tmset, hyp_frees th)) 742 743(*---------------------------------------------------------------------------* 744 * Discharge all hypotheses * 745 * * 746 * t1, ... , tn |- t * 747 * ------------------------------ * 748 * |- t1 ==> ... ==> tn ==> t * 749 *---------------------------------------------------------------------------*) 750 751fun DISCH_ALL th = HOLset.foldl (Lib.uncurry DISCH) th (hypset th) 752 753(*---------------------------------------------------------------------------* 754 * A |- t1 ==> ... ==> tn ==> t * 755 * ------------------------------- * 756 * A, t1, ..., tn |- t * 757 *---------------------------------------------------------------------------*) 758 759fun UNDISCH_ALL th = if is_imp (concl th) then UNDISCH_ALL (UNDISCH th) else th 760 761(* --------------------------------------------------------------------------* 762 * SPEC_ALL : thm -> thm * 763 * * 764 * A |- !x1 ... xn. t[xi] * 765 * ------------------------ where the xi' are distinct * 766 * A |- t[xi'/xi] and not free in the input theorem * 767 * * 768 * BUGFIX: added the "distinct" part and code to make the xi's not free * 769 * in the conclusion !x1...xn.t[xi]. [TFM 90.10.04] * 770 * * 771 * OLD CODE: * 772 * * 773 * let SPEC_ALL th = * 774 * let vars,() = strip_forall(concl th) in * 775 * SPECL (map (variant (freesl (hyp th))) vars) th;; * 776 * --------------------------------------------------------------------------*) 777 778local 779 fun varyAcc v (V, l) = let val v' = prim_variant V v in (v'::V, v'::l) end 780in 781 fun SPEC_ALL th = 782 if is_forall (concl th) then 783 let 784 val (hvs, con) = (HOLset.listItems ## I) (hyp_frees th, concl th) 785 val fvs = free_vars con 786 val vars = fst (strip_forall con) 787 in 788 SPECL (snd (itlist varyAcc vars (hvs @ fvs, []))) th 789 end 790 else th 791end 792 793(*---------------------------------------------------------------------------* 794 * !x. A ==> !y. B ==> !z. C ==> !w. D * 795 * ----------------------------------- * 796 * C ==> B ==> A ==> D' (for example) * 797 * * 798 * reorders antecedents, modifies the conclusion D * 799 *---------------------------------------------------------------------------*) 800 801fun REORDER_ANTS_MOD f g th = 802 let val (ants, uth) = strip_gen_left (UNDISCH_TM o SPEC_ALL) th ; 803 in Lib.itlist DISCH (f ants) (g (SPEC_ALL uth)) end ; 804 805fun REORDER_ANTS f th = REORDER_ANTS_MOD f (fn c => c) th ; 806fun MODIFY_CONS g th = REORDER_ANTS_MOD (fn hs => hs) g th ; 807 808(*---------------------------------------------------------------------------* 809 * Use the conclusion of the first theorem to delete a hypothesis of * 810 * the second theorem. * 811 * * 812 * A |- t1 B, t1 |- t2 * 813 * ----------------------- * 814 * A u B |- t2 * 815 *---------------------------------------------------------------------------*) 816 817fun PROVE_HYP ath bth = MP (DISCH (concl ath) bth) ath 818 819(*---------------------------------------------------------------------------* 820 * A |- t1 /\ t2 ---> A |- t1, A |- t2 * 821 *---------------------------------------------------------------------------*) 822 823fun CONJ_PAIR th = (CONJUNCT1 th, CONJUNCT2 th) 824 handle HOL_ERR _ => raise ERR "CONJ_PAIR" "" 825 826(*---------------------------------------------------------------------------* 827 * ["A1|-t1", ..., "An|-tn"] ---> "A1u...uAn|-t1 /\ ... /\ tn", where n>0 * 828 *---------------------------------------------------------------------------*) 829 830val LIST_CONJ = end_itlist CONJ 831 832(*---------------------------------------------------------------------------* 833 * "A |- t1 /\ (...(... /\ tn)...)" * 834 * ---> * 835 * [ "A|-t1", ..., "A|-tn"], where n>0 * 836 * * 837 * Inverse of LIST_CONJ : flattens only right conjuncts. * 838 * You must specify n, since tn could itself be a conjunction * 839 *---------------------------------------------------------------------------*) 840 841fun CONJ_LIST 1 th = [th] 842 | CONJ_LIST n th = CONJUNCT1 th :: CONJ_LIST (n - 1) (CONJUNCT2 th) 843 handle HOL_ERR _ => raise ERR "CONJ_LIST" "" 844 845(*---------------------------------------------------------------------------* 846 * "|- !x. (t1 /\ ...) /\ ... (!y. ... /\ tn)" * 847 * ---> [ "|-t1", ..., "|-tn"], where n>0 * 848 * * 849 * Flattens out conjuncts even in bodies of forall's * 850 *---------------------------------------------------------------------------*) 851 852fun BODY_CONJUNCTS th = 853 if is_forall (concl th) 854 then BODY_CONJUNCTS (SPEC_ALL th) 855 else if is_conj (concl th) 856 then (BODY_CONJUNCTS (CONJUNCT1 th) @ BODY_CONJUNCTS (CONJUNCT2 th)) 857 else [th] 858 859(*---------------------------------------------------------------------------* 860 * Put a theorem * 861 * * 862 * |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t * 863 * * 864 * into canonical form by stripping out quantifiers and splitting * 865 * conjunctions apart. * 866 * * 867 * t1 /\ t2 ---> t1, t2 * 868 * (t1/\t2)==>t ---> t1==> (t2==>t) * 869 * (t1\/t2)==>t ---> t1==>t, t2==>t * 870 * (?x.t1)==>t2 ---> t1[x'/x] ==> t2 * 871 * !x.t1 ---> t1[x'/x] * 872 *---------------------------------------------------------------------------*) 873 874fun IMP_CANON th = 875 let 876 val w = concl th 877 in 878 if is_forall w 879 then IMP_CANON (SPEC_ALL th) 880 else if is_conj w 881 then IMP_CANON (CONJUNCT1 th) @ IMP_CANON (CONJUNCT2 th) 882 else if is_imp w 883 then let 884 val (ant, _) = dest_imp w 885 in 886 if is_conj ant 887 then let 888 val (conj1, conj2) = dest_conj ant 889 in 890 IMP_CANON 891 (DISCH conj1 892 (DISCH conj2 893 (MP th (CONJ (ASSUME conj1) 894 (ASSUME conj2))))) 895 end 896 else if is_disj ant 897 then let 898 val (disj1, disj2) = dest_disj ant 899 in 900 IMP_CANON 901 (DISCH disj1 902 (MP th (DISJ1 (ASSUME disj1) disj2))) @ 903 IMP_CANON 904 (DISCH disj2 (MP th (DISJ2 disj1 (ASSUME disj2)))) 905 end 906 else if is_exists ant 907 then let 908 val (Bvar, Body) = dest_exists ant 909 val bv' = variant (thm_frees th) Bvar 910 val body' = subst [Bvar |-> bv'] Body 911 in 912 IMP_CANON 913 (DISCH body' 914 (MP th (EXISTS (ant, bv') (ASSUME body')))) 915 end 916 else map (DISCH ant) (IMP_CANON (UNDISCH th)) 917 end 918 else [th] 919 end 920 921(*--------------------------------------------------------------------------- 922 | MP_CANON puts a theorem 923 | 924 | |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t 925 | 926 | into canonical form for applying MATCH_MP_TAC by moving quantifiers to 927 | the outmost level and combining implications 928 | 929 | t1 ==> !x. t2 ---> !x. t1 ==> t2 930 | t1 ==> t2 ==> t3 ---> t1 /\ t2 ==> t3 931 | 932 | It might be useful to replace equivalences with implications while 933 | normalising. MP_GENEQ_CANON gets a list of boolean values as an extra 934 | argument to configure such replacements. The occuring equations are split 935 | according to the elements of this list. true focuses on the left hand side, 936 | i.e. the right-hand side is put into the antecedent. false focuses on the 937 | right hand side. If the list is empty, the equation is not splitted. 938 | 939 | MP_GENEQ_CANON [true] |- !x. A x ==> (!y. (B1 x y):bool = B2 y) ---> 940 | !x y. A x /\ B2 y ===> B1 x y 941 | MP_GENEQ_CANON [false] |- !x. A x ==> (!y. (B1 x y):bool = B2 y) ---> 942 | !x y. A x /\ B1 x y ===> B2 y 943 | 944 | For convinience the most common cases of this parameter are introduced 945 | own functions 946 | 947 | val MP_CANON = MP_GENEQ_CANON [] 948 | val MP_LEQ_CANON = MP_GENEQ_CANON [true] 949 | val MP_REQ_CANON = MP_GENEQ_CANON [false] 950 |---------------------------------------------------------------------------*) 951 952local 953 fun RIGHT_IMP_IMP_FORALL_RULE th = 954 let 955 val w = concl th 956 in 957 if is_imp_only w 958 then let 959 val (ant, conc) = dest_imp w 960 in 961 if is_forall conc 962 then let 963 val (Bvar, Body) = dest_forall conc 964 val bv' = variant (thm_frees th) Bvar 965 val th1 = MP th (ASSUME ant) 966 val th2 = SPEC bv' th1 967 val th3 = DISCH ant th2 968 val th4 = RIGHT_IMP_IMP_FORALL_RULE th3 969 val th5 = GEN bv' th4 970 in 971 th5 972 end 973 else if is_imp_only conc 974 then let 975 val (ant2, conc2) = dest_imp conc 976 val conc_t = mk_conj (ant, ant2) 977 val conc_thm = ASSUME conc_t 978 val th1 = MP th (CONJUNCT1 conc_thm) 979 val th2 = MP th1 (CONJUNCT2 conc_thm) 980 val th3 = DISCH conc_t th2 981 in 982 RIGHT_IMP_IMP_FORALL_RULE th3 983 end 984 else th 985 end 986 else th 987 end 988in 989 fun MP_GENEQ_CANON eqL th = 990 let 991 val w = concl th 992 in 993 if is_forall w 994 then let 995 val (Bvar, Body) = dest_forall w 996 val bv' = variant (thm_frees th) Bvar 997 val th1 = MP_GENEQ_CANON eqL (SPEC bv' th) 998 val th2 = GEN bv' th1 999 in 1000 th2 1001 end 1002 else if is_imp_only w 1003 then let 1004 val (ant, conc) = dest_imp w 1005 val th1 = MP th (ASSUME ant) 1006 val th2 = MP_GENEQ_CANON eqL th1 1007 val th3 = DISCH ant th2 1008 val th4 = RIGHT_IMP_IMP_FORALL_RULE th3 1009 in 1010 th4 1011 end 1012 else if not (null eqL) andalso is_eq w 1013 then MP_GENEQ_CANON (tl eqL) 1014 ((if hd eqL then snd else fst) (EQ_IMP_RULE th)) 1015 handle HOL_ERR _ => th 1016 else th 1017 end 1018end 1019 1020val MP_CANON = MP_GENEQ_CANON [] 1021val MP_LEQ_CANON = MP_GENEQ_CANON [true] 1022val MP_REQ_CANON = MP_GENEQ_CANON [false] 1023 1024(*---------------------------------------------------------------------------* 1025 * A1 |- t1 ... An |- tn A |- t1==>...==>tn==>t * 1026 * ----------------------------------------------------- * 1027 * A u A1 u ... u An |- t * 1028 *---------------------------------------------------------------------------*) 1029 1030val LIST_MP = rev_itlist (fn x => fn y => MP y x) 1031 1032(*---------------------------------------------------------------------------* 1033 * A |-t1 ==> t2 * 1034 * ----------------- * 1035 * A |- ~t2 ==> ~t1 * 1036 * * 1037 * Rewritten by MJCG to return "~t2 ==> ~t1" rather than "~t2 ==> t1 ==>F". * 1038 *---------------------------------------------------------------------------*) 1039 1040local 1041 val imp_th = GEN_ALL (el 5 (CONJUNCTS (SPEC_ALL IMP_CLAUSES))) 1042in 1043 fun CONTRAPOS impth = 1044 let 1045 val (ant, conseq) = dest_imp (concl impth) 1046 val notb = mk_neg conseq 1047 in 1048 DISCH notb 1049 (EQ_MP (SPEC ant imp_th) 1050 (DISCH ant (MP (ASSUME notb) (MP impth (ASSUME ant))))) 1051 end 1052 handle HOL_ERR _ => raise ERR "CONTRAPOS" "" 1053end 1054 1055(*---------------------------------------------------------------------------* 1056 * A |- t1 \/ t2 * 1057 * -------------------- * 1058 * A |- ~ t1 ==> t2 * 1059 *---------------------------------------------------------------------------*) 1060 1061fun DISJ_IMP dth = 1062 let 1063 val (disj1, disj2) = dest_disj (concl dth) 1064 val nota = mk_neg disj1 1065 in 1066 DISCH nota 1067 (DISJ_CASES dth (CONTR disj2 (MP (ASSUME nota) (ASSUME disj1))) 1068 (ASSUME disj2)) 1069 end 1070 handle HOL_ERR _ => raise ERR "DISJ_IMP" "" 1071 1072(*---------------------------------------------------------------------------* 1073 * A |- t1 ==> t2 * 1074 * --------------- * 1075 * A |- ~t1 \/ t2 * 1076 *---------------------------------------------------------------------------*) 1077 1078fun IMP_ELIM th = 1079 let 1080 val (ant, conseq) = dest_imp (concl th) 1081 val not_t1 = mk_neg ant 1082 in 1083 DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) 1084 (DISJ2 not_t1 (MP th (ASSUME ant))) 1085 (DISJ1 (ASSUME not_t1) conseq) 1086 end 1087 handle HOL_ERR _ => raise ERR "IMP_ELIM" "" 1088 1089(*---------------------------------------------------------------------------* 1090 * A |- t1 \/ t2 A1, t1 |- t3 A2, t2 |- t4 * 1091 * ------------------------------------------------ * 1092 * A u A1 u A2 |- t3 \/ t4 * 1093 *---------------------------------------------------------------------------*) 1094 1095fun DISJ_CASES_UNION dth ath bth = 1096 DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth) 1097 1098(*---------------------------------------------------------------------------* 1099 * * 1100 * |- A1 \/ ... \/ An [H1,A1 |- M, ..., Hn,An |- M] * 1101 * --------------------------------------------------------- * 1102 * H1 u ... u Hn |- M * 1103 * * 1104 * The order of the theorems in the list doesn't matter: an operation akin * 1105 * to sorting lines them up with the disjuncts in the theorem. * 1106 *---------------------------------------------------------------------------*) 1107 1108local 1109 fun ishyp tm th = HOLset.member (hypset th, tm) 1110 fun organize (tm :: rst) (alist as (_ :: _)) = 1111 let 1112 val (th, next) = Lib.pluck (ishyp tm) alist 1113 in 1114 th :: organize rst next 1115 end 1116 | organize [] [] = [] 1117 | organize other wise = 1118 raise ERR "DISJ_CASESL.organize" "length difference" 1119in 1120 fun DISJ_CASESL disjth thl = 1121 let 1122 val cases = strip_disj (concl disjth) 1123 val thl' = organize cases thl 1124 fun DL th [] = raise ERR "DISJ_CASESL" "no cases" 1125 | DL th [th1] = PROVE_HYP th th1 1126 | DL th [th1, th2] = DISJ_CASES th th1 th2 1127 | DL th (th1 :: rst) = 1128 DISJ_CASES th th1 (DL (ASSUME (snd (dest_disj (concl th)))) rst) 1129 in 1130 DL disjth thl' 1131 end 1132 handle e => raise wrap_exn "Drule" "DISJ_CASESL" e 1133end 1134 1135(*---------------------------------------------------------------------------* 1136 * Rename the bound variable of a lambda-abstraction * 1137 * * 1138 * "x" "(\y.t)" ---> |- "\y.t = \x. t[x/y]" * 1139 *---------------------------------------------------------------------------*) 1140 1141local 1142 fun err s = raise ERR "ALPHA_CONV" s 1143in 1144 fun ALPHA_CONV x t = 1145 let 1146 (* avoid calling dest_abs *) 1147 val (dty, _) = dom_rng (type_of t) 1148 handle HOL_ERR _ => err "Second term not an abstraction" 1149 val (xstr, xty) = with_exn dest_var x 1150 (ERR "ALPHA_CONV" "First term not a variable") 1151 val _ = Type.compare (dty, xty) = EQUAL 1152 orelse err "Type of variable not compatible with abstraction" 1153 val t' = rename_bvar xstr t 1154 in 1155 ALPHA t t' 1156 end 1157end 1158 1159(*---------------------------------------------------------------------------- 1160 Version of ALPHA_CONV that renames "x" when necessary, but then it doesn't 1161 meet the specification. Is that really a problem? Notice that this version 1162 of ALPHA_CONV is more efficient. 1163 1164 fun ALPHA_CONV x t = 1165 if Term.free_in x t 1166 then ALPHA_CONV (variant (free_vars t) x) t 1167 else ALPHA t (mk_abs{Bvar = x, 1168 Body = Term.beta_conv(mk_comb{Rator = t,Rand = x})}) 1169 ----------------------------------------------------------------------------*) 1170 1171(*---------------------------------------------------------------------------* 1172 * Rename bound variables * 1173 * * 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 * "x" "(@y.t)" ---> |- "@y.t = @x. t[x/y]" * 1179 *---------------------------------------------------------------------------*) 1180 1181fun GEN_ALPHA_CONV x t = 1182 if is_abs t 1183 then ALPHA_CONV x t 1184 else let 1185 val (Rator, Rand) = dest_comb t 1186 in 1187 AP_TERM Rator (ALPHA_CONV x Rand) 1188 end 1189 handle HOL_ERR _ => raise ERR "GEN_ALPHA_CONV" "" 1190 1191(* --------------------------------------------------------------------------* 1192 * A1 |- P ==> Q A2 |- R ==> S * 1193 * --------------------------------- IMP_CONJ * 1194 * A1 u A2 |- P /\ R ==> Q /\ S * 1195 * --------------------------------------------------------------------------*) 1196 1197fun IMP_CONJ th1 th2 = 1198 let 1199 val (A1, _) = dest_imp (concl th1) 1200 and (A2, _) = dest_imp (concl th2) 1201 val conj = mk_conj (A1, A2) 1202 val (a1, a2) = CONJ_PAIR (ASSUME conj) 1203 in 1204 DISCH conj (CONJ (MP th1 a1) (MP th2 a2)) 1205 end 1206 1207(* --------------------------------------------------------------------------* 1208 * EXISTS_IMP : existentially quantify the antecedent and conclusion * 1209 * of an implication. * 1210 * * 1211 * A |- P ==> Q * 1212 * -------------------------- EXISTS_IMP `x` * 1213 * A |- (?x.P) ==> (?x.Q) * 1214 * --------------------------------------------------------------------------*) 1215 1216fun EXISTS_IMP x th = 1217 if not (is_var x) 1218 then raise ERR "EXISTS_IMP" "first argument not a variable" 1219 else let 1220 val (ant, conseq) = dest_imp (concl th) 1221 val th1 = EXISTS (mk_exists (x, conseq), x) (UNDISCH th) 1222 val asm = mk_exists (x, ant) 1223 in 1224 DISCH asm (CHOOSE (x, ASSUME asm) th1) 1225 end 1226 handle HOL_ERR _ => raise ERR "EXISTS_IMP" "variable free in assumptions" 1227 1228(*---------------------------------------------------------------------------* 1229 * Instantiate terms and types of a theorem. This is pretty slow, because * 1230 * it makes two full traversals of the theorem. * 1231 *---------------------------------------------------------------------------*) 1232 1233fun INST_TY_TERM (Stm, Sty) th = INST Stm (INST_TYPE Sty th) 1234 1235(*---------------------------------------------------------------------------* 1236 * Instantiate terms and types of a theorem, also returning a list of * 1237 * substituted hypotheses in the same order as in hyp th * 1238 * (required for predictability of order of new subgoals from (prim_)irule) * 1239 *---------------------------------------------------------------------------*) 1240 1241fun INST_TT_HYPS subs th = 1242 let val nhyps = HOLset.numItems (hypset th) ; 1243 val thd = DISCH_ALL th ; 1244 val thdsub = INST_TY_TERM subs thd ; 1245 (* UNDISCH_TM nhyps times only *) 1246 fun UNDISCH_TM_L (th, tms) = 1247 let val (tm, th') = UNDISCH_TM th ; 1248 in (th', tm :: tms) end ; 1249 in Lib.funpow nhyps UNDISCH_TM_L (thdsub, []) end ; 1250 1251(*---------------------------------------------------------------------------* 1252 * |- !x y z. w ---> |- w[g1/x][g2/y][g3/z] * 1253 *---------------------------------------------------------------------------*) 1254 1255fun GSPEC th = 1256 let 1257 val (_, w) = dest_thm th 1258 in 1259 if is_forall w 1260 then GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th) 1261 else th 1262 end 1263 1264(*---------------------------------------------------------------------------* 1265 * Match a given part of "th" to a term, instantiating "th". The part * 1266 * should be free in the theorem, except for outer bound variables. * 1267 *---------------------------------------------------------------------------*) 1268 1269fun PART_MATCH partfn th = 1270 let 1271 val th = SPEC_ALL th 1272 val conclfvs = Term.FVL [concl th] empty_tmset 1273 val hypfvs = Thm.hyp_frees th 1274 val hyptyvars = HOLset.listItems (Thm.hyp_tyvars th) 1275 val pat = partfn (concl th) 1276 val matchfn = 1277 match_terml hyptyvars (HOLset.intersection (conclfvs, hypfvs)) pat 1278 in 1279 fn tm => INST_TY_TERM (matchfn tm) th 1280 end 1281 1282(*---------------------------------------------------------------------------* 1283 * version of PART_MATCH which allows substituting in assumptions * 1284 *---------------------------------------------------------------------------*) 1285fun PART_MATCH_A partfn th = 1286 let 1287 val pat = partfn (concl (SPEC_ALL th)) 1288 in 1289 fn tm => INST_TY_TERM (match_term pat tm) th 1290 end 1291 1292(* ---------------------------------------------------------------------- 1293 version of PART_MATCH that only specialises universally quantified 1294 variables that are necessary to make the match go through. 1295 Others are left as quantifiers 1296 ---------------------------------------------------------------------- *) 1297 1298fun avSPEC_ALL avds th = 1299 let 1300 fun recurse avds acc th = 1301 case Lib.total dest_forall (concl th) of 1302 SOME (v,bod) => 1303 let 1304 val v' = variant avds v 1305 in 1306 recurse (v'::avds) (v'::acc) (SPEC v' th) 1307 end 1308 | NONE => (List.rev acc, th) 1309 in 1310 recurse avds [] th 1311 end 1312 1313fun PART_MATCH' f th t = 1314 let 1315 val (vs, _) = strip_forall (concl th) 1316 val hypfvs_set = hyp_frees th 1317 val hypfvs = HOLset.listItems hypfvs_set 1318 val hyptyvs = HOLset.listItems (hyp_tyvars th) 1319 val tfvs = free_vars t 1320 val dontspec = op_union aconv tfvs hypfvs 1321 val (vs, speccedth) = avSPEC_ALL dontspec th 1322 val s as (tmsig,tysig) = 1323 match_terml hyptyvs hypfvs_set (f (concl speccedth)) t 1324 val dontgen = op_union aconv (map #redex tmsig) dontspec 1325 in 1326 GENL (op_set_diff aconv (map (Term.inst tysig) vs) dontgen) 1327 (INST_TY_TERM s speccedth) 1328 end 1329 1330(* --------------------------------------------------------------------------* 1331 EXISTS_LEFT, EXISTS_LEFT1 1332 existentially quantifying variables which appear only in the hypotheses 1333 1334 [x = y, y = z] |- x = z 1335 (eg) -------------------------------- EXISTS_LEFT1 ``y`` 1336 [���y. (x = y) ��� (y = z)] |- x = z (UOK) 1337 1338 * --------------------------------------------------------------------------*) 1339 1340(* EXISTS_LEFT' : bool -> 1341 term list -> {fvs: term list, hyp: term} list -> term list -> thm -> thm 1342 used below, saves hyps, their free vars, and free vars of conclusion, 1343 across recursive calls 1344 arg1 - whether to ignore errors, ie, free vars which are either in the 1345 conclusion or not in any hypothesis 1346 arg2 - list of free vars in the conclusion 1347 arg3 - list of assumptions of the theorem, each with the list of free vars 1348 which it contains 1349 arg4 - list of free vars to become existentially quantified 1350*) 1351 1352fun EXISTS_LEFT' strict fvs_c hfvs [] th = th 1353 | EXISTS_LEFT' strict fvs_c hfvs (fv :: fvs) th = 1354 let 1355 val _ = if is_var fv then () 1356 else raise mk_HOL_ERR "Drule" "EXISTS_LEFT'" "not free variable" ; 1357 (* following raises Bind if fv in conclusion *) 1358 val _ = List.all (not o aconv fv) fvs_c orelse raise Bind 1359 fun hyp_ctns_fv {hyp, fvs} = List.exists (aconv fv) fvs ; 1360 val (hyps_ctg_fv, hyps_nc) = List.partition hyp_ctns_fv hfvs ; 1361 (* following raises Bind if fv not in any hypothesis *) 1362 val _ = not (null hyps_ctg_fv) orelse raise Bind 1363 (* select and conjoin the hyps containing fv *) 1364 val conj_tm = list_mk_conj (map #hyp hyps_ctg_fv) ; 1365 (* using CONJ_LIST gives original hyps, even if they are conjunctions *) 1366 val sep_ths = CONJ_LIST (length hyps_ctg_fv) (ASSUME conj_tm) ; 1367 (* replace the previous hyps with the single new one, which is 1368 conjunction of the previous ones *) 1369 val th2 = Lib.itlist PROVE_HYP sep_ths th ; 1370 val ex_conj_tm = mk_exists (fv, conj_tm) ; 1371 val the = CHOOSE (fv, ASSUME ex_conj_tm) th2 ; 1372 val thex = EXISTS_LEFT' strict fvs_c 1373 ({hyp = ex_conj_tm, fvs = free_vars ex_conj_tm} :: hyps_nc) fvs the ; 1374 in thex end 1375 handle Bind => 1376 if strict then 1377 raise mk_HOL_ERR "Drule" "EXISTS_LEFT'" 1378 "free variable in conclusion or not in any hypothesis" 1379 else EXISTS_LEFT' strict fvs_c hfvs fvs th ; 1380 1381(* EXISTS_LEFT : term list -> thm -> thm 1382 for each free var in turn, do the following: 1383 replace hyps containing the free var by their conjunction, 1384 existentially quantified over the free var; 1385 ignore free vars for which this can't be done *) 1386fun EXISTS_LEFT [] th = th 1387 | EXISTS_LEFT fvs th = 1388 let val hfvs = map (fn h => {hyp = h, fvs = free_vars h}) (Thm.hyp th) ; 1389 val fvs_c = free_vars (concl th) ; 1390 in EXISTS_LEFT' false fvs_c hfvs fvs th end ; 1391 1392(* EXISTS_LEFT1 : term -> thm -> thm 1393 for the free var argument, replace hyps containing the free var 1394 by their conjunction, existentially quantified over the free var; 1395 error if this can't be done for a free var *) 1396fun EXISTS_LEFT1 fv th = 1397 let val hfvs = map (fn h => {hyp = h, fvs = free_vars h}) (Thm.hyp th) ; 1398 val fvs_c = free_vars (concl th) ; 1399 in EXISTS_LEFT' true fvs_c hfvs [fv] th end ; 1400 1401(* --------------------------------------------------------------------------* 1402 * SPEC_UNDISCH_EXL: strips !x, ant ==>, (splitting conjuncts of ant) * 1403 * then EXISTS_LEFT for stripped vars * 1404 * --------------------------------------------------------------------------*) 1405 1406fun SPEC_UNDISCH_EXL thm = 1407 let val (fvs, th1) = strip_gen_left (SPEC_VAR o repeat UNDISCH_SPLIT) thm ; 1408 val th2 = repeat UNDISCH_SPLIT th1 ; 1409 val th3 = EXISTS_LEFT (rev fvs) th2 ; 1410 in th3 end ; 1411 1412(* --------------------------------------------------------------------------* 1413 * MATCH_MP: Matching Modus Ponens for implications. * 1414 * * 1415 * |- !x1 ... xn. P ==> Q |- P' * 1416 * --------------------------------------- * 1417 * |- Q' * 1418 * * 1419 * Matches all types in conclusion except those mentioned in hypotheses. * 1420 * --------------------------------------------------------------------------*) 1421 1422local 1423 fun variants (_, []) = [] 1424 | variants (av, h::rst) = 1425 let val vh = variant av h in vh :: variants (vh :: av, rst) end 1426 fun rassoc_total x theta = Option.getOpt (subst_assoc (aconv x) theta, x) 1427 fun req {redex, residue} = aconv redex residue 1428in 1429 fun MATCH_MP ith = 1430 let 1431 val bod = fst (dest_imp (snd (strip_forall (concl ith)))) 1432 val hyptyvars = HOLset.listItems (hyp_tyvars ith) 1433 val lconsts = HOLset.intersection 1434 (FVL [concl ith] empty_tmset, hyp_frees ith) 1435 in 1436 fn th => 1437 let 1438 val mfn = C (Term.match_terml hyptyvars lconsts) (concl th) 1439 val tth = INST_TYPE (snd (mfn bod)) ith 1440 val tbod = fst (dest_imp (snd (strip_forall (concl tth)))) 1441 val tmin = fst (mfn tbod) 1442 val hy1 = HOLset.listItems (hyp_frees tth) 1443 and hy2 = HOLset.listItems (hyp_frees th) 1444 val (avs, (ant, conseq)) = 1445 (I ## dest_imp) (strip_forall (concl tth)) 1446 val (rvs, fvs) = partition (C free_in ant) (free_vars conseq) 1447 val afvs = op_set_diff aconv fvs (op_set_diff aconv hy1 avs) 1448 val cvs = free_varsl (map (C rassoc_total tmin) rvs) 1449 val vfvs = 1450 map (op |->) (zip afvs (variants (cvs @ hy1 @ hy2, afvs))) 1451 val atmin = (filter (op not o op req) vfvs) @ tmin 1452 val (spl, ill) = partition (C (op_mem aconv) avs o #redex) atmin 1453 val fspl = map (C rassoc_total spl) avs 1454 val mth = MP (SPECL fspl (INST ill tth)) th 1455 fun loop [] = [] 1456 | loop (tm :: rst) = 1457 case subst_assoc (aconv tm) vfvs of 1458 NONE => loop rst 1459 | SOME x => x :: loop rst 1460 in 1461 GENL (loop avs) mth 1462 end 1463 end 1464end 1465 1466(*---------------------------------------------------------------------------* 1467 * Now higher-order versions of PART_MATCH and MATCH_MP * 1468 *---------------------------------------------------------------------------*) 1469 1470(* IMPORTANT: See the bottom of this file for a longish discussion of some 1471 of the ways this implementation attempts to keep bound variable 1472 names sensible. 1473*) 1474 1475(*---------------------------------------------------------------------------* 1476 * Attempt alpha conversion. * 1477 *---------------------------------------------------------------------------*) 1478 1479fun tryalpha v tm = 1480 let 1481 val (Bvar, Body) = dest_abs tm 1482 in 1483 if aconv v Bvar then tm 1484 else if var_occurs v Body then 1485 tryalpha (variant (free_vars tm) v) tm 1486 else mk_abs (v, subst [Bvar |-> v] Body) 1487 end 1488 1489(*---------------------------------------------------------------------------* 1490 * Match up bound variables names. * 1491 *---------------------------------------------------------------------------*) 1492 1493(* first argument is actual term, second is from theorem being matched *) 1494 1495fun match_bvs t1 t2 acc = 1496 case (dest_term t1, dest_term t2) of 1497 (LAMB (v1, b1), LAMB (v2, b2)) => 1498 let 1499 val n1 = fst (dest_var v1) 1500 val n2 = fst (dest_var v2) 1501 val newacc = if n1 = n2 then acc else insert (n1, n2) acc 1502 in 1503 match_bvs b1 b2 newacc 1504 end 1505 | (COMB (l1, r1), COMB (l2, r2)) => match_bvs l1 l2 (match_bvs r1 r2 acc) 1506 | otherwise => acc 1507 1508(* bindings come from match_bvs, telling us which bound variables are going 1509 to get renamed, and thmc is the conclusion of the pattern theorem. 1510 acc is a set of free variables that need to get instantiated away *) 1511 1512fun look_for_avoids bindings thmc acc = 1513 let 1514 val lfa = look_for_avoids bindings 1515 in 1516 case dest_term thmc of 1517 LAMB (v, b) => 1518 let 1519 val (thm_n, _) = dest_var v 1520 in 1521 case Lib.total (rev_assoc thm_n) bindings of 1522 SOME n => 1523 let 1524 val fvs = FVL [b] empty_tmset 1525 fun f (v, acc) = 1526 if #1 (dest_var v) = n 1527 then HOLset.add (acc, v) 1528 else acc 1529 in 1530 lfa b (HOLset.foldl f acc fvs) 1531 end 1532 | NONE => lfa b acc 1533 end 1534 | COMB (l, r) => lfa l (lfa r acc) 1535 | _ => acc 1536 end 1537 1538(*---------------------------------------------------------------------------* 1539 * Modify bound variable names at depth. (Not very efficient...) * 1540 *---------------------------------------------------------------------------*) 1541 1542fun deep_alpha [] tm = tm 1543 | deep_alpha env tm = 1544 case dest_term tm of 1545 LAMB (Bvar, Body) => 1546 (let 1547 val (Name, Ty) = dest_var Bvar 1548 val ((vn', _), newenv) = Lib.pluck (fn (_, x) => x = Name) env 1549 val tm' = tryalpha (mk_var (vn', Ty)) tm 1550 val (iv, ib) = dest_abs tm' 1551 in 1552 mk_abs (iv, deep_alpha newenv ib) 1553 end 1554 handle HOL_ERR _ => mk_abs (Bvar, deep_alpha env Body)) 1555 | COMB (Rator, Rand) => 1556 mk_comb (deep_alpha env Rator, deep_alpha env Rand) 1557 | otherwise => tm 1558 1559(* ------------------------------------------------------------------------- 1560 BETA_VAR 1561 1562 Set up beta-conversion for head instances of free variable v in tm. 1563 1564 EXAMPLES 1565 1566 BETA_VAR (--`x:num`--) (--`(P:num->num->bool) x x`--); 1567 BETA_VAR (--`x:num`--) (--`x + 1`--); 1568 1569 Note (kxs): I am defining this before Conv, so some conversion(al)s are 1570 p(re)-defined here. Ugh. 1571 1572 ========================================================================= 1573 PART_MATCH 1574 1575 Match (higher-order) part of a theorem to a term. 1576 1577 PART_MATCH (snd o strip_forall) BOOL_CASES_AX (--`(P = T) \/ (P = F)`--); 1578 val f = PART_MATCH lhs; 1579 profile2 f NOT_FORALL_THM (--`~!x. (P:num->num->bool) x y`--); 1580 profile2 f NOT_EXISTS_THM (--`?x. ~(P:num->num->bool) x y`--); 1581 profile2 f LEFT_AND_EXISTS_THM 1582 (--`(?x. (P:num->num->bool) x x) /\ Q (y:num)`--); 1583 profile LEFT_AND_EXISTS_CONV 1584 (--`(?x. (P:num->num->bool) x x) /\ Q (x:num)`--); 1585 profile2 f NOT_FORALL_THM (--`~!x. (P:num->num->bool) y x`--); 1586 profile NOT_FORALL_CONV (--`~!x. (P:num->num->bool) y x`--); 1587 val f = PART_MATCH (lhs o snd o strip_imp); 1588 val CRW_THM = mk_thm([],(--`P x ==> Q x (y:num) ==> (x + 0 = x)`--)); 1589 f CRW_THM (--`y + 0`--); 1590 1591 val beta_thm = prove(--`(\x:'a. P x) b = (P b:'b)`--)--, 1592 BETA_TAC THEN REFL_TAC); 1593 val f = profile PART_MATCH lhs beta_thm; 1594 profile f (--`(\x. I x) 1`--); 1595 profile f (--`(\x. x) 1`--); 1596 profile f (--`(\x. P x x:num) 1`--); 1597 1598 The current version attempts to keep variable names constant. This 1599 is courtesy of JRH. 1600 1601 Non renaming version (also courtesy of JRH!!) 1602 1603 fun PART_MATCH partfn th = 1604 let val sth = SPEC_ALL th 1605 val bod = concl sth 1606 val possbetas = mapfilter (fn v => (v,BETA_VAR v bod)) (free_vars bod) 1607 fun finish_fn tyin bvs = 1608 let val npossbetas = map (inst tyin ## I) possbetas 1609 in CONV_RULE (EVERY_CONV (mapfilter (C assoc npossbetas) bvs)) 1610 end 1611 val pbod = partfn bod 1612 in fn tm => 1613 let val (tmin,tyin) = match_term pbod tm 1614 val th0 = INST tmin (INST_TYPE tyin sth) 1615 in finish_fn tyin (map #redex tmin) th0 1616 end 1617 end; 1618 1619 EXAMPLES: 1620 1621 val CET = mk_thm([],(--`(!c. P ($COND c x y) c) = (P x T /\ P y F)`--)); 1622 1623 PART_MATCH lhs FORALL_SIMP (--`!x. y + 1 = 2`--); 1624 PART_MATCH lhs FORALL_SIMP (--`!x. x + 1 = 2`--); (* fails *) 1625 PART_MATCH lhs CET (--`!b. ~(f (b => t | e))`--); 1626 PART_MATCH lhs option_CASE_ELIM (--`!b. ~(P (option_CASE e f b))`--); 1627 PART_MATCH lhs (MK_FORALL (--`c:bool`--) COND_ELIM_THM) 1628 (--`!b. ~(f (b => t | e))`--); 1629 PART_MATCH lhs (MK_FORALL (--`c:bool`--) COND_ELIM_THM) 1630 (--`!b. ~(f (b => t | e))`--); 1631 ho_term_match [] (--`!c. P ($COND c x y)`--) 1632 1633 BUG FIXES & TEST CASES 1634 1635 Variable Renaming: 1636 PART_MATCH (lhs o snd o strip_forall) SKOLEM_THM (--`!p. ?GI. Q GI p`--); 1637 Before renaming this produced: |- (!x. ?y. Q y x) = (?y. !x. Q (y x) x) 1638 After renaming this produced: |- (!p. ?GI. Q GI p) = (?GI. !p. Q (GI p) p) 1639 1640 Variable renaming problem (DRS, Feb 1996): 1641 PART_MATCH lhs NOT_FORALL_THM (--`~!y. P x`--); 1642 Before fix produced: |- ~(!x'. P x) = (?x'. ~(P x)) : thm 1643 After fix produced: |- ~(!y. P x) = (?y. ~(P x)) 1644 Fix: 1645 val bvms = match_bvs tm (inst tyin pbod) [] 1646 Became: 1647 val bvms = match_bvs tm (partfn (concl th0)) [] 1648 1649 Variable renaming problem (DRS, Feb 1996): 1650 PART_MATCH lhs NOT_FORALL_THM (--`~!x. (\y. t) T`--); 1651 Before fix produced (--`?y. ~(\y. t) T`--); 1652 After fix produced (--`?x. ~(\y. t) T`--); 1653 Fix: 1654 Moved beta reduction to be before alpha renaming. This makes 1655 match_bvs more accurate. This was not a problem before the previous 1656 fix. 1657 1658 Another bug (unfixed). bvms = [("x","y"),("E'","x")] 1659 PART_MATCH lhs SWAP_EXISTS_THM (--`?E' x const'. 1660 ((s = s') /\ 1661 (E = E') /\ 1662 (val = Val_Constr (const',x)) /\ 1663 (sym = const)) /\ 1664 (a1 = NONE) /\ 1665 ~(const = const')`--) 1666 ------------------------------------------------------------------------- *) 1667 1668nonfix THENC 1669 1670local 1671 fun COMB_CONV2 c1 c2 M = 1672 let val (f, x) = dest_comb M in MK_COMB (c1 f, c2 x) end 1673 fun ABS_CONV c M = 1674 let val (Bvar, Body) = dest_abs M in ABS Bvar (c Body) end 1675 fun RAND_CONV c M = 1676 let val (Rator, Rand) = dest_comb M in AP_TERM Rator (c Rand) end 1677 fun RATOR_CONV c M = 1678 let val (Rator, Rand) = dest_comb M in AP_THM (c Rator) Rand end 1679 fun TRY_CONV c M = c M handle HOL_ERR _ => REFL M 1680 fun THENC c1 c2 M = 1681 let val th = c1 M in TRANS th (c2 (rhs (concl th))) end 1682 fun EVERY_CONV convl = itlist THENC convl REFL 1683 fun CONV_RULE conv th = EQ_MP (conv (concl th)) th 1684 fun BETA_CONVS n = 1685 if n = 1 then TRY_CONV BETA_CONV 1686 else THENC (RATOR_CONV (BETA_CONVS (n - 1))) (TRY_CONV BETA_CONV) 1687in 1688 fun BETA_VAR v tm = 1689 if is_abs tm 1690 then let 1691 val (Bvar, Body) = dest_abs tm 1692 in 1693 if aconv v Bvar then failwith "BETA_VAR: UNCHANGED" 1694 else ABS_CONV (BETA_VAR v Body) end 1695 else case strip_comb tm of 1696 (_, []) => failwith "BETA_VAR: UNCHANGED" 1697 | (oper, args) => 1698 if aconv oper v then BETA_CONVS (length args) 1699 else let 1700 val (Rator, Rand) = dest_comb tm 1701 in 1702 let 1703 val lconv = BETA_VAR v Rator 1704 in 1705 let 1706 val rconv = BETA_VAR v Rand 1707 in 1708 COMB_CONV2 lconv rconv 1709 end 1710 handle HOL_ERR _ => RATOR_CONV lconv 1711 end 1712 handle HOL_ERR _ => RAND_CONV (BETA_VAR v Rand) 1713 end 1714 1715 structure Map = Redblackmap 1716 1717 (* count from zero to indicate last argument, up to #args - 1 to indicate 1718 first argument *) 1719 1720 fun arg_CONV 0 c = RAND_CONV c 1721 | arg_CONV n c = RATOR_CONV (arg_CONV (n - 1) c) 1722 1723 fun foldri f acc list = 1724 let 1725 fun foldthis (e, (acc, n)) = (f (n, e, acc), n + 1) 1726 in 1727 #1 (foldr foldthis (acc, 0) list) 1728 end 1729 1730 fun munge_bvars absmap th = 1731 let 1732 fun recurse curposn bvarposns (donebvars, acc) t = 1733 case dest_term t of 1734 LAMB (bv, body) => 1735 let 1736 val newposnmap = Map.insert (bvarposns, bv, curposn) 1737 val (newdonemap, restore) = 1738 (HOLset.delete (donebvars, bv), 1739 fn m => HOLset.add (m, bv)) 1740 handle HOLset.NotFound => 1741 (donebvars, (fn m => HOLset.delete (m, bv) 1742 handle HOLset.NotFound => m)) 1743 val (dbvars, actions) = 1744 recurse 1745 (curposn o ABS_CONV) newposnmap (newdonemap, acc) body 1746 in 1747 (restore dbvars, actions) 1748 end 1749 | COMB _ => 1750 let 1751 val (f, args) = strip_comb t 1752 fun argfold (n, arg, A) = 1753 recurse (curposn o arg_CONV n) bvarposns A arg 1754 in 1755 case Map.peek (absmap, f) of 1756 NONE => foldri argfold (donebvars, acc) args 1757 | SOME abs_t => 1758 let 1759 val (abs_bvars, _) = strip_abs abs_t 1760 val paired_up = ListPair.zip (args, abs_bvars) 1761 fun foldthis 1762 ((arg, absv), acc as (dbvars, actionlist)) = 1763 if HOLset.member (dbvars, arg) 1764 then acc 1765 else case Map.peek (bvarposns, arg) of 1766 NONE => acc 1767 | SOME p => 1768 (HOLset.add (dbvars, arg), 1769 p (ALPHA_CONV absv) :: actionlist) 1770 val (A as (newdbvars, newacc)) = 1771 List.foldl foldthis (donebvars, acc) paired_up 1772 in 1773 foldri argfold A args 1774 end 1775 end 1776 | _ => (donebvars, acc) 1777 in 1778 recurse I (Map.mkDict Term.compare) (empty_tmset, []) (concl th) 1779 end 1780 1781 (* Modified HO_PART_MATCH by PVH on Apr. 25, 2005: code was broken; 1782 repaired by tightening "foldthis" condition for entry to "bound_to_abs"; 1783 see longish note at bottom for more details. *) 1784 1785 (* "bound_vars" returns set of bound variables within term t *) 1786 (* "t" argument is actual term, "acc" is accumulating set, orig. empty *) 1787 1788 local 1789 fun bound_vars1 t acc = 1790 case dest_term t of 1791 LAMB (v, b) => bound_vars1 b (HOLset.add (acc, v)) 1792 | COMB (l, r) => bound_vars1 l (bound_vars1 r acc) 1793 | otherwise => acc 1794 in 1795 fun bound_vars t = bound_vars1 t empty_tmset 1796 end 1797 1798 fun HO_PART_MATCH partfn th = 1799 let 1800 val sth = SPEC_ALL th 1801 val bod = concl sth 1802 val pbod = partfn bod 1803 val possbetas = 1804 mapfilter (fn v => (v, BETA_VAR v bod)) 1805 (filter (can dom_rng o type_of) (free_vars bod)) 1806 fun finish_fn tyin ivs = 1807 let 1808 val npossbetas = 1809 if null tyin 1810 then possbetas 1811 else map (inst tyin ## I) possbetas 1812 in 1813 if null npossbetas then Lib.I 1814 else 1815 CONV_RULE 1816 (EVERY_CONV 1817 (mapfilter (TRY_CONV o C(op_assoc aconv) npossbetas) ivs)) 1818 end 1819 val lconsts = 1820 HOLset.intersection (FVL [pbod] empty_tmset, hyp_frees th) 1821 val ltyconsts = HOLset.listItems (hyp_tyvars th) 1822 in 1823 fn tm => 1824 let 1825 val (tmin, tyin) = ho_match_term ltyconsts lconsts pbod tm 1826 val tmbvs = bound_vars tm 1827 fun foldthis ({redex, residue}, acc) = 1828 if is_abs residue 1829 andalso all (fn v => HOLset.member (tmbvs, v)) 1830 (fst (strip_abs residue)) 1831 then Map.insert (acc, redex, residue) else acc 1832 val bound_to_abs = 1833 List.foldl foldthis (Map.mkDict Term.compare) tmin 1834 val sth0 = INST_TYPE tyin sth 1835 val sth0c = concl sth0 1836 val (sth1, tmin') = 1837 case match_bvs tm (partfn sth0c) [] of 1838 [] => (sth0, tmin) 1839 | bvms => 1840 let 1841 val avoids = look_for_avoids bvms sth0c empty_tmset 1842 fun f (v, acc) = (v |-> genvar (type_of v)) :: acc 1843 val newinst = HOLset.foldl f [] avoids 1844 val newthm = INST newinst sth0 1845 val tmin' = map (fn {residue, redex} => 1846 {residue = residue, 1847 redex = Term.subst newinst redex}) 1848 tmin 1849 val thmc = concl newthm 1850 in 1851 (EQ_MP (ALPHA thmc (deep_alpha bvms thmc)) newthm, 1852 tmin') 1853 end 1854 val sth2 = 1855 if Map.numItems bound_to_abs = 0 1856 then sth1 1857 else CONV_RULE 1858 (EVERY_CONV (#2 (munge_bvars bound_to_abs sth1))) 1859 sth1 1860 val th0 = INST tmin' sth2 1861 val th1 = finish_fn tyin (map #redex tmin) th0 1862 in 1863 th1 1864 end 1865 end 1866end 1867 1868fun HO_MATCH_MP ith = 1869 let 1870 val sth = 1871 let 1872 val tm = concl ith 1873 val (avs, bod) = strip_forall tm 1874 val (ant, _) = dest_imp_only bod 1875 in 1876 case partition (C free_in ant) avs of 1877 (_, []) => ith 1878 | (svs, pvs) => 1879 let 1880 val th1 = SPECL avs (ASSUME tm) 1881 val th2 = GENL svs (DISCH ant (GENL pvs (UNDISCH th1))) 1882 in 1883 MP (DISCH tm th2) ith 1884 end 1885 end 1886 handle HOL_ERR _ => raise ERR "MATCH_MP" "Not an implication" 1887 val match_fun = HO_PART_MATCH (fst o dest_imp_only) sth 1888 in 1889 fn th => 1890 MP (match_fun (concl th)) th 1891 handle HOL_ERR _ => raise ERR "MATCH_MP" "No match" 1892 end 1893 1894(* ===================================================================== 1895 The "resolution" tactics for HOL (outmoded technology, but 1896 sometimes useful) uses RES_CANON and SPEC_ALL 1897 ===================================================================== 1898 1899 Put a theorem 1900 1901 |- !x. t1 ==> !y. t2 ==> ... ==> tm ==> t 1902 1903 into canonical form for resolution by splitting conjunctions apart 1904 (like IMP_CANON but without the stripping out of quantifiers and only 1905 outermost negations being converted to implications). 1906 1907 ~t ---> t ==> F (at outermost level) 1908 t1 /\ t2 ---> t1, t2 1909 (t1/\t2)==>t ---> t1==> (t2==>t) 1910 (t1\/t2)==>t ---> t1==>t, t2==>t 1911 1912 Modification provided by David Shepherd of Inmos to make resolution 1913 work with equalities as well as implications. HOL88.1.08,23 jun 1989. 1914 1915 t1 = t2 ---> t1=t2, t1==>t2, t2==>t1 1916 1917 Modification provided by T Melham to deal with the scope of 1918 universal quantifiers. [TFM 90.04.24] 1919 1920 !x. t1 ==> t2 ---> t1 ==> !x.t2 (x not free in t1) 1921 1922 The old code is given below: 1923 1924 letrec RES_CANON_FUN th = 1925 let w = concl th in 1926 if is_conj w 1927 then RES_CANON_FUN(CONJUNCT1 th)@RES_CANON_FUN(CONJUNCT2 th) 1928 else if is_imp w & not(is_neg w) then 1929 let ante,conc = dest_imp w in 1930 if is_conj ante then 1931 let a,b = dest_conj ante in 1932 RES_CANON_FUN 1933 (DISCH a (DISCH b (MP th (CONJ (ASSUME a) (ASSUME b))))) 1934 else if is_disj ante then 1935 let a,b = dest_disj ante in 1936 RES_CANON_FUN (DISCH a (MP th (DISJ1 (ASSUME a) b))) @ 1937 RES_CANON_FUN (DISCH b (MP th (DISJ2 a (ASSUME b)))) 1938 else 1939 map (DISCH ante) (RES_CANON_FUN (UNDISCH th)) 1940 else [th]; 1941 1942 This version deleted for HOL 1.12 (see below) [TFM 91.01.17] 1943 1944 let RES_CANON = 1945 letrec FN th = 1946 let w = concl th in 1947 if (is_conj w) then FN(CONJUNCT1 th) @ FN(CONJUNCT2 th) else 1948 if ((is_imp w) & not(is_neg w)) then 1949 let ante,conc = dest_imp w in 1950 if (is_conj ante) then 1951 let a,b = dest_conj ante in 1952 let ath = ASSUME a and bth = ASSUME b 1953 in FN (DISCH a (DISCH b (MP th (CONJ ath bth)))) else 1954 if is_disj ante then 1955 let a,b = dest_disj ante in 1956 let ath = ASSUME a and bth = ASSUME b 1957 in FN (DISCH a (MP th (DISJ1 ath b))) @ 1958 FN (DISCH b (MP th (DISJ2 a bth))) 1959 else map (GEN_ALL o (DISCH ante)) (FN (UNDISCH th)) 1960 else if is_eq w then 1961 let l,r = dest_eq w in 1962 if (type_of l = ":bool") 1963 then let (th1,th2) = EQ_IMP_RULE th 1964 in (GEN_ALL th) . ((FN th1) @ (FN th2)) 1965 else [GEN_ALL th] 1966 else [GEN_ALL th] in 1967 \th. (let vars,w = strip_forall(concl th) in 1968 let th1 = if (is_neg w) 1969 then NOT_ELIM(SPEC_ALL th) 1970 else (SPEC_ALL th) in 1971 map GEN_ALL (FN th1) ? failwith `RES_CANON`); 1972 1973 --------------------------------------------------------------------- 1974 New RES_CANON for version 1.12. [TFM 90.12.07] 1975 1976 The complete list of transformations is now: 1977 1978 ~t ---> t ==> F (at outermost level) 1979 t1 /\ t2 ---> t1, t2 (at outermost level) 1980 (t1/\t2)==>t ---> t1==>(t2==>t), t2==>(t1==>t) 1981 (t1\/t2)==>t ---> t1==>t, t2==>t 1982 t1 = t2 ---> t1==>t2, t2==>t1 1983 !x. t1 ==> t2 ---> t1 ==> !x.t2 (x not free in t1) 1984 (?x.t1) ==> t2 ---> !x'. t1[x'/x] ==> t2 1985 1986 The function now fails if no implications can be derived from the 1987 input theorem. 1988 1989 =====================================================================*) 1990 1991local 1992 fun not_elim th = 1993 if is_neg (concl th) then (true, NOT_ELIM th) else (false, th) 1994 fun canon (fl, th) = 1995 let 1996 val w = concl th 1997 in 1998 if is_conj w 1999 then let 2000 val (th1, th2) = CONJ_PAIR th 2001 in 2002 canon (fl, th1) @ canon (fl, th2) 2003 end 2004 else if is_imp w andalso not (is_neg w) 2005 then 2006 let 2007 val (ant, _) = dest_imp w 2008 in 2009 if is_conj ant 2010 then 2011 let 2012 val (conj1, conj2) = dest_conj ant 2013 val cth = MP th (CONJ (ASSUME conj1) (ASSUME conj2)) 2014 val th1 = DISCH conj2 cth 2015 and th2 = DISCH conj1 cth 2016 in 2017 canon (true, DISCH conj1 th1) @ 2018 canon (true, DISCH conj2 th2) 2019 end 2020 else if is_disj ant 2021 then 2022 let 2023 val (disj1, disj2) = dest_disj ant 2024 val ath = DISJ1 (ASSUME disj1) disj2 2025 and bth = DISJ2 disj1 (ASSUME disj2) 2026 val th1 = DISCH disj1 (MP th ath) 2027 and th2 = DISCH disj2 (MP th bth) 2028 in 2029 canon (true, th1) @ canon (true, th2) 2030 end 2031 else if is_exists ant 2032 then 2033 let 2034 val (Bvar, Body) = dest_exists ant 2035 val newv = variant (thm_frees th) Bvar 2036 val newa = subst [Bvar |-> newv] Body 2037 val th1 = MP th (EXISTS (ant, newv) (ASSUME newa)) 2038 in 2039 canon (true, DISCH newa th1) 2040 end 2041 else map (GEN_ALL o (DISCH ant)) (canon (true, UNDISCH th)) 2042 end 2043 else if is_eq w andalso type_of (rand w) = Type.bool 2044 then 2045 let 2046 val (th1, th2) = EQ_IMP_RULE th 2047 in 2048 (if fl then [GEN_ALL th] else []) @ 2049 canon (true, th1) @ canon (true, th2) 2050 end 2051 else if is_forall w 2052 then 2053 let 2054 val (vs, _) = strip_forall w 2055 val fvs = HOLset.listItems (FVL [concl th] (hyp_frees th)) 2056 val nvs = 2057 itlist (fn v => fn nv => variant (nv @ fvs) v::nv) vs [] 2058 in 2059 canon (fl, SPECL nvs th) 2060 end 2061 else if fl 2062 then [GEN_ALL th] 2063 else [] 2064 end 2065in 2066 fun RES_CANON th = 2067 let 2068 val conjlist = CONJUNCTS (SPEC_ALL th) 2069 fun operate th accum = 2070 accum @ map GEN_ALL (canon (not_elim (SPEC_ALL th))) 2071 val imps = Lib.rev_itlist operate conjlist [] 2072 in 2073 Lib.assert (op not o null) imps 2074 end 2075 handle HOL_ERR _ => 2076 raise ERR "RES_CANON" 2077 "No implication is derivable from input thm" 2078end 2079 2080(* ---------------------------------------------------------------------- 2081 IRULE_CANON 2082 2083 Aggressive canonicalisation of introduction rules so that it takes on 2084 the form 2085 2086 |- !vs. cs ==> concl 2087 2088 where vs all appear in concl, and may appear among cs. 2089 2090 The cs may not be present at all, but if so is a conjunction of 2091 exhyps, where each exhyp is of the form 2092 2093 ?e1 e2 .. en. c1 /\ c2 /\ .. cm 2094 2095 ---------------------------------------------------------------------- *) 2096 2097 2098local 2099 fun AIMP_RULE th = 2100 let 2101 val (l, r) = dest_imp (concl th) 2102 val (c1, c2) = dest_conj l 2103 val cth = CONJ (ASSUME c1) (ASSUME c2) 2104 in 2105 DISCH c1 (DISCH c2 (MP th cth)) 2106 end 2107 2108 fun (s1 - s2) = HOLset.difference(s1,s2) 2109 fun norm th = 2110 if is_forall (concl th) then norm (SPEC_ALL th) 2111 else 2112 case Lib.total dest_imp_only (concl th) of 2113 NONE => th 2114 | SOME (l,r) => 2115 if is_conj l then norm (AIMP_RULE th) 2116 else norm (UNDISCH th) 2117 2118fun group_hyps gfvs tlist = 2119 let 2120 fun overlaps fvset (tfvs,_) = 2121 not (HOLset.isEmpty (HOLset.intersection(fvset, tfvs))) 2122 fun union ((fvset1, tlist1), (fvset2, tlist2)) = 2123 (HOLset.union(fvset1, fvset2), tlist1 @ tlist2) 2124 fun recurse acc tlist = 2125 case tlist of 2126 [] => acc 2127 | t::ts => 2128 let 2129 val tfvs = FVL [t] empty_tmset - gfvs 2130 in 2131 case List.partition (overlaps tfvs) acc of 2132 ([], _) => recurse ((tfvs,[t])::acc) ts 2133 | (ovlaps, rest) => 2134 recurse (List.foldl union (tfvs, [t]) ovlaps :: rest) ts 2135 end 2136 in 2137 recurse [] tlist 2138 end 2139 2140fun CHOOSEL vs t th = 2141 let 2142 fun foldthis (v,(t,th)) = 2143 let val ext = mk_exists(v,t) 2144 in 2145 (ext, CHOOSE (v,ASSUME ext) th) 2146 end 2147 in 2148 List.foldr foldthis (t,th) vs 2149 end 2150 2151fun CONJL ts th = let 2152 val c = list_mk_conj ts 2153 val cths = CONJUNCTS (ASSUME c) 2154in 2155 (List.foldl (fn (c,th) => PROVE_HYP c th) th cths, c) 2156end 2157 2158fun reconstitute groups th = 2159 let 2160 fun recurse acc groups th = 2161 case groups of 2162 [] => (acc, th) 2163 | (fvset, ts) :: rest => 2164 let 2165 val (th1,c) = CONJL ts th 2166 val (ext, th2) = CHOOSEL (HOLset.listItems fvset) c th1 2167 in 2168 recurse (ext::acc) rest th2 2169 end 2170 in 2171 recurse [] groups th 2172 end 2173in 2174fun IRULE_CANON th = 2175 let 2176 val th1 = norm (GEN_ALL th) 2177 val orighyps = hypset th 2178 val origl = HOLset.listItems orighyps 2179 val gfvs = FVL (concl th1 :: origl) empty_tmset 2180 val newhyps = hypset th1 - orighyps 2181 val grouped = group_hyps gfvs (HOLset.listItems newhyps) 2182 val (cs, th2) = reconstitute grouped th1 2183 in 2184 case cs of 2185 [] => GEN_ALL th2 2186 | _ => 2187 let 2188 val (th3,c) = CONJL cs th2 2189 in 2190 DISCH c th3 |> GEN_ALL 2191 end 2192 end 2193end (* local *) 2194 2195(*---------------------------------------------------------------------------* 2196 * Routines supporting the definition of types * 2197 * * 2198 * AUTHOR : (c) Tom Melham, University of Cambridge * 2199 * * 2200 * NAME: define_new_type_bijections * 2201 * * 2202 * DESCRIPTION: define isomorphism constants based on a type definition. * 2203 * * 2204 * USAGE: define_new_type_bijections name ABS REP tyax * 2205 * * 2206 * ARGUMENTS: tyax -- a type-defining axiom of the form returned by * 2207 * new_type_definition. For example: * 2208 * * 2209 * ?rep. TYPE_DEFINITION P rep * 2210 * * 2211 * ABS --- the name of the required abstraction function * 2212 * * 2213 * REP --- the name of the required representation function * 2214 * * 2215 * name --- the name under which the definition is stored * 2216 * * 2217 * SIDE EFFECTS: Introduces a definition for two constants `ABS` and * 2218 * (--`REP`--) by the constant specification: * 2219 * * 2220 * |- ?ABS REP. (!a. ABS(REP a) = a) /\ * 2221 * (!r. P r = (REP(ABS r) = r) * 2222 * * 2223 * The resulting constant specification is stored under * 2224 * the name given as the first argument. * 2225 * * 2226 * FAILURE: if input theorem of wrong form. * 2227 * * 2228 * RETURNS: The defining property of the representation and abstraction * 2229 * functions, given by: * 2230 * * 2231 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2232 *---------------------------------------------------------------------------*) 2233 2234fun define_new_type_bijections {name, ABS, REP, tyax} = 2235 if not (HOLset.isEmpty (hypset tyax)) 2236 then raise ERR "define_new_type_bijections" 2237 "input theorem must have no assumptions" 2238 else 2239 let 2240 val (P, rep) = case strip_comb (snd (dest_exists (concl tyax))) of 2241 (_, [P, rep]) => (P, rep) 2242 | _ => raise Match 2243 val (a, r) = Type.dom_rng (type_of rep) 2244 in 2245 Rsyntax.new_specification 2246 {name = name, 2247 sat_thm = 2248 MP (SPEC P (INST_TYPE [beta |-> a, alpha |-> r] ABS_REP_THM)) tyax, 2249 consts = [{const_name = REP, fixity = NONE}, 2250 {const_name = ABS, fixity = NONE}]} 2251 end 2252 handle e => 2253 raise (wrap_exn "Drule" 2254 ("define_new_type_bijections {name=\""^name^"\"...}") 2255 e) 2256 2257(* --------------------------------------------------------------------------* 2258 * NAME: prove_rep_fn_one_one * 2259 * * 2260 * DESCRIPTION: prove that a type representation function is one-to-one. * 2261 * * 2262 * USAGE: if th is a theorem of the kind returned by the ML function * 2263 * define_new_type_bijections: * 2264 * * 2265 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2266 * * 2267 * then prove_rep_fn_one_one th will prove and return a theorem * 2268 * stating that the representation function REP is one-to-one: * 2269 * * 2270 * |- !a a'. (REP a = REP a') = (a = a') * 2271 * * 2272 *---------------------------------------------------------------------------*) 2273 2274fun prove_rep_fn_one_one th = 2275 let 2276 val thm = CONJUNCT1 th 2277 val (_, Body) = dest_forall (concl thm) 2278 val (A, Rand) = dest_comb (lhs Body) 2279 val (R, _)= dest_comb Rand 2280 val (aty, rty) = case Type.dest_type (type_of R) of 2281 (_, [aty, rty]) => (aty, rty) 2282 | _ => raise Match 2283 val a = mk_primed_var ("a", aty) 2284 val a' = variant [a] a 2285 val a_eq_a' = mk_eq (a, a') 2286 and Ra_eq_Ra' = mk_eq (mk_comb (R, a), mk_comb (R, a')) 2287 val th1 = AP_TERM A (ASSUME Ra_eq_Ra') 2288 val ga1 = genvar aty 2289 and ga2 = genvar aty 2290 val th2 = SUBST [ga1 |-> SPEC a thm, ga2 |-> SPEC a' thm] 2291 (mk_eq (ga1, ga2)) th1 2292 val th3 = DISCH a_eq_a' (AP_TERM R (ASSUME a_eq_a')) 2293 in 2294 GEN a (GEN a' (IMP_ANTISYM_RULE (DISCH Ra_eq_Ra' th2) th3)) 2295 end 2296 handle HOL_ERR _ => raise ERR "prove_rep_fn_one_one" "" 2297 | Bind => raise ERR "prove_rep_fn_one_one" 2298 ("Theorem not of right form: must be\n\ 2299 \ |- (!a. to (from a) = a) /\\\ 2300 \ (!r. P r = (from (to r) = r))") 2301 2302(* --------------------------------------------------------------------------* 2303 * NAME: prove_rep_fn_onto * 2304 * * 2305 * DESCRIPTION: prove that a type representation function is onto. * 2306 * * 2307 * USAGE: if th is a theorem of the kind returned by the ML function * 2308 * define_new_type_bijections: * 2309 * * 2310 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2311 * * 2312 * then prove_rep_fn_onto th will prove and return a theorem * 2313 * stating that the representation function REP is onto: * 2314 * * 2315 * |- !r. P r = (?a. r = REP a) * 2316 * * 2317 *---------------------------------------------------------------------------*) 2318 2319fun prove_rep_fn_onto th = 2320 let 2321 val (th1, th2) = case CONJUNCTS th of 2322 [th1, th2] => (th1, th2) 2323 | _ => raise Match 2324 val (Bvar, Body) = dest_forall (concl th2) 2325 val (_, eq) = dest_eq Body 2326 val (RE, ar) = dest_comb (lhs eq) 2327 val a = mk_primed_var ("a", type_of ar) 2328 val sra = mk_eq (Bvar, mk_comb (RE, a)) 2329 val ex = mk_exists (a, sra) 2330 val imp1 = EXISTS (ex, ar) (SYM (ASSUME eq)) 2331 val v = genvar (type_of Bvar) 2332 and A = rator ar 2333 and ass = AP_TERM RE (SPEC a th1) 2334 val th = SUBST [v |-> SYM (ASSUME sra)] 2335 (mk_eq (mk_comb (RE, mk_comb (A, v)), v)) ass 2336 val imp2 = CHOOSE (a, ASSUME ex) th 2337 val swap = IMP_ANTISYM_RULE (DISCH eq imp1) (DISCH ex imp2) 2338 in 2339 GEN Bvar (TRANS (SPEC Bvar th2) swap) 2340 end 2341 handle HOL_ERR _ => raise ERR "prove_rep_fn_onto" "" 2342 | Bind => raise ERR "prove_rep_fn_onto" 2343 ("Theorem not of right form: must be\n\ 2344 \ (!a. to (from a) = a) /\\\ 2345 \ (!r. P r = (from (to r) = r))") 2346 2347(* --------------------------------------------------------------------------* 2348 * NAME: prove_abs_fn_onto * 2349 * * 2350 * DESCRIPTION: prove that a type abstraction function is onto. * 2351 * * 2352 * USAGE: if th is a theorem of the kind returned by the ML function * 2353 * define_new_type_bijections: * 2354 * * 2355 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2356 * * 2357 * then prove_abs_fn_onto th will prove and return a theorem * 2358 * stating that the abstraction function ABS is onto: * 2359 * * 2360 * |- !a. ?r. (a = ABS r) /\ P r * 2361 * * 2362 * --------------------------------------------------------------------------*) 2363 2364fun prove_abs_fn_onto th = 2365 let 2366 val (th1, th2) = case CONJUNCTS th of 2367 [th1, th2] => (th1, th2) 2368 | _ => raise Match 2369 val (bv_th1, Body) = dest_forall (concl th1) 2370 val (A, Rand) = dest_comb (lhs Body) 2371 val R = rator Rand 2372 val rb = mk_comb (R, bv_th1) 2373 val bth1 = SPEC bv_th1 th1 2374 val thm1 = EQT_ELIM (TRANS (SPEC rb th2) (EQT_INTRO (AP_TERM R bth1))) 2375 val thm2 = SYM bth1 2376 val (r, Body) = dest_forall (concl th2) 2377 val P = rator (lhs Body) 2378 val ex = 2379 mk_exists (r, mk_conj (mk_eq (bv_th1, mk_comb (A, r)), mk_comb (P, r))) 2380 in 2381 GEN bv_th1 (EXISTS (ex, rb) (CONJ thm2 thm1)) 2382 end 2383 handle HOL_ERR _ => raise ERR "prove_abs_fn_onto" "" 2384 | Bind => raise ERR "prove_abs_fn_one_onto" 2385 ("Theorem not of right form: must be\n\ 2386 \ |- (!a. to (from a) = a) /\\\ 2387 \ (!r. P r = (from (to r) = r))") 2388 2389(* --------------------------------------------------------------------------* 2390 * NAME: prove_abs_fn_one_one * 2391 * * 2392 * DESCRIPTION: prove that a type abstraction function is one-to-one. * 2393 * * 2394 * USAGE: if th is a theorem of the kind returned by the ML function * 2395 * define_new_type_bijections: * 2396 * * 2397 * |- (!a. ABS(REP a) = a) /\ (!r. P r = (REP(ABS r) = r) * 2398 * * 2399 * then prove_abs_fn_one_one th will prove and return a theorem * 2400 * stating that the abstraction function ABS is one-to-one: * 2401 * * 2402 * |- !r r'. P r ==> * 2403 * P r' ==> * 2404 * (ABS r = ABS r') ==> (r = r') * 2405 * * 2406 * --------------------------------------------------------------------------*) 2407 2408fun prove_abs_fn_one_one th = 2409 let 2410 val (th1, th2) = case CONJUNCTS th of 2411 [th1, th2] => (th1, th2) 2412 | _ => raise Match 2413 val (r, Body) = dest_forall (concl th2) 2414 val P = rator (lhs Body) 2415 val (A, Rand) = dest_comb (lhs (snd (dest_forall (concl th1)))) 2416 val R = rator Rand 2417 val r' = variant [r] r 2418 val r_eq_r' = mk_eq (r, r') 2419 val Pr = mk_comb (P, r) 2420 val Pr' = mk_comb (P, r') 2421 val as1 = ASSUME Pr 2422 and as2 = ASSUME Pr' 2423 val t1 = EQ_MP (SPEC r th2) as1 2424 and t2 = EQ_MP (SPEC r' th2) as2 2425 val eq = mk_eq (mk_comb (A, r), mk_comb (A, r')) 2426 val v1 = genvar (type_of r) 2427 and v2 = genvar (type_of r) 2428 val i1 = DISCH eq (SUBST [v1 |-> t1, v2 |-> t2] 2429 (mk_eq (v1, v2)) (AP_TERM R (ASSUME eq))) 2430 val i2 = DISCH r_eq_r' (AP_TERM A (ASSUME r_eq_r')) 2431 val thm = IMP_ANTISYM_RULE i1 i2 2432 val disch = DISCH Pr (DISCH Pr' thm) 2433 in 2434 GEN r (GEN r' disch) 2435 end 2436 handle HOL_ERR _ => raise ERR "prove_abs_fn_one_one" "" 2437 | Bind => raise ERR "prove_abs_fn_one_one" 2438 ("Theorem not of right form: must be\n\ 2439 \ |- (!a. to (from a) = a) /\\\ 2440 \ (!r. P r = (from (to r) = r))") 2441 2442(*---------------------------------------------------------------------------* 2443 * Take an AC pair, normalize them, then prove left-commutativity * 2444 *---------------------------------------------------------------------------*) 2445 2446local 2447 (* Rules related to "semantic tags" for controlling rewriting *) 2448 val is_comm = can (match_term comm_tm) 2449 val is_assoc = can (match_term assoc_tm) 2450 2451 fun regen th = GENL (free_vars_lr (concl th)) th 2452 2453 fun err () = (HOL_MESG "unable to AC-normalize input" 2454 ; raise ERR "norm_ac" "failed") 2455 2456 (* Classify a pair of theorems as one assoc. thm and one comm. thm. Then 2457 return pair (A,C) where A has the form |- f(x,f(y,z)) = f(f(x,y),z) *) 2458 2459 fun norm_ac (th1, th2) = 2460 let 2461 val th1' = SPEC_ALL th1 2462 val th2' = SPEC_ALL th2 2463 val tm1 = concl th1' 2464 val tm2 = concl th2' 2465 in 2466 if is_comm tm2 2467 then if is_assoc tm1 2468 then (regen th1', regen th2') 2469 else let 2470 val th1a = SYM th1' 2471 in 2472 if is_assoc (concl th1a) 2473 then (regen th1a, regen th2') 2474 else err () 2475 end 2476 else if is_comm tm1 2477 then if is_assoc tm2 2478 then (regen th2', regen th1') 2479 else let 2480 val th2a = SYM th2' 2481 in 2482 if is_assoc (concl th2a) 2483 then (regen th2a, regen th1') 2484 else err () 2485 end 2486 else err () 2487 end 2488in 2489 fun MK_AC_LCOMM (th1, th2) = 2490 let 2491 val (a, c) = norm_ac (th1, th2) 2492 val lcomm = MATCH_MP (MATCH_MP LCOMM_THM a) c 2493 in 2494 (regen (SYM (SPEC_ALL a)), c, lcomm) 2495 end 2496end 2497 2498 2499fun GEN_TYVARIFY th = 2500 let 2501 val concl_tyvs = HOLset.addList ( 2502 HOLset.empty Type.compare, 2503 type_vars_in_term (concl th) 2504 ) 2505 val tyvs = HOLset.difference(concl_tyvs, hyp_tyvars th) 2506 in 2507 INST_TYPE (gen_tyvar_sigma (HOLset.listItems tyvs)) th 2508 end 2509 2510fun FULL_GEN_TYVARIFY th = 2511 let 2512 val tyvs = HOLset.addList(hyp_tyvars th, type_vars_in_term (concl th)) 2513 in 2514 INST_TYPE (gen_tyvar_sigma (HOLset.listItems tyvs)) th 2515 end 2516 2517datatype AI = IMP of term | FA of {orig:term, new:term} 2518fun CONV_RULE c th = EQ_MP (c (concl th)) th 2519fun restore hs (acs, th) = 2520 case acs of 2521 [] => rev_itlist ADD_ASSUM hs th 2522 | IMP t :: rest => restore hs (rest, DISCH t th) 2523 | FA{orig,new} :: rest => 2524 if orig ~~ new then 2525 restore hs (rest, GEN orig th) 2526 else 2527 restore hs (rest, th |> GEN new |> CONV_RULE (GEN_ALPHA_CONV orig)) 2528fun AIdestAll th = 2529 case total dest_forall (concl th) of 2530 NONE => NONE 2531 | SOME (v,b) => 2532 let 2533 val hfvs = hyp_frees th 2534 in 2535 if HOLset.member(hfvs, v) then 2536 let val new = variant (HOLset.listItems hfvs) v 2537 in 2538 SOME (FA{orig=v,new=new}, SPEC new th) 2539 end 2540 else 2541 SOME (FA{orig=v,new=v}, SPEC v th) 2542 end 2543 2544fun underALLs f th = 2545 let 2546 fun getbase A th = 2547 case AIdestAll th of 2548 NONE => (A, f th) 2549 | SOME (act, th') => getbase (act::A) th' 2550 in 2551 restore [] (getbase [] th) 2552 end 2553fun underAIs f th = 2554 let 2555 fun getbase A th = 2556 case AIdestAll th of 2557 NONE => (case total dest_imp_only (concl th) of 2558 NONE => (A, f th) 2559 | SOME (l,r) => getbase (IMP l :: A) (UNDISCH th)) 2560 | SOME (act,th') => getbase (act::A) th' 2561 in 2562 restore (hyp th) (getbase [] th) 2563 end 2564 2565fun cj i = underAIs (el i o CONJUNCTS) 2566val iffLR = underAIs (#1 o EQ_IMP_RULE) 2567val iffRL = underAIs (#2 o EQ_IMP_RULE) 2568 2569fun promote f th = 2570 let 2571 val (H, _) = dest_imp (concl th) 2572 val hs = strip_conj H 2573 val th' = UNDISCH th 2574 val t = f hs 2575 val (_, rest) = pluck (aconv t) hs 2576 in 2577 if null rest then th 2578 else 2579 let 2580 val Cs = ASSUME_CONJS H 2581 val R = list_mk_conj rest 2582 val Cs' = CONJUNCTS (ASSUME R) 2583 val elim = rev_itlist PROVE_HYP (ASSUME t :: Cs') Cs 2584 in 2585 th' |> PROVE_HYP elim |> DISCH R |> DISCH t 2586 end 2587 end 2588 2589fun findq fvs patq ts = 2590 let 2591 open TermParse 2592 val pat_t = prim_ctxt_termS Parse.Absyn (term_grammar()) fvs patq|>seq.hd 2593 in 2594 case List.find (can (match_term pat_t)) ts of 2595 NONE => raise ERR "pp" "No hypothesis matching pattern" 2596 | SOME t => t 2597 end 2598 2599val notnot = NOT_CLAUSES |> CONJUNCTS |> hd |> SPEC_ALL |> EQ_IMP_RULE |> #2 2600val impf_intro = IMP_CLAUSES |> SPEC_ALL |> CONJUNCTS |> last |> SYM |> GEN_ALL 2601fun IMPF_INTRO th = EQ_MP (PART_MATCH lhs impf_intro (concl th)) th 2602val t_b = mk_var("t", bool) 2603fun notnotremove th = 2604 let val (l,r) = dest_imp (concl th) 2605 val l0 = dest_neg l 2606 val l00 = dest_neg l0 2607 in 2608 PROVE_HYP (notnot |> INST [t_b |-> l00] |> UNDISCH) (UNDISCH th) 2609 |> DISCH l00 2610 end handle HOL_ERR _ => th 2611val cpos = notnotremove o underAIs IMPF_INTRO o CONTRAPOS 2612 2613fun FORALL1 f th = 2614 let val (v,_) = dest_forall (concl th) 2615 in 2616 th |> SPEC v |> f |> GEN v 2617 end 2618 2619fun pushdown th = 2620 let val (v1,b0) = dest_forall (concl th) 2621 in 2622 let val (v2,b) = dest_forall b0 2623 in 2624 th |> SPEC v1 |> SPEC v2 |> GEN v1 |> pushdown |> GEN v2 2625 end handle HOL_ERR _ => 2626 let val (l,r) = dest_imp b0 2627 in 2628 th |> SPEC v1 |> UNDISCH |> GEN v1 |> DISCH l 2629 end 2630 end 2631 2632fun pushFAs fvs th = 2633 let val (v,b) = dest_forall (concl th) 2634 val finish = if tmem v fvs then (fn th => th) else pushdown 2635 in 2636 th |> FORALL1 (pushFAs fvs) |> finish 2637 end handle HOL_ERR _ => th 2638 2639fun pp pos th0 = 2640 let 2641 open thmpos_dtype 2642 val th = MP_CANON th0 2643 fun transform th = 2644 case pos of 2645 Any => promote hd th 2646 | Pos f => promote f th 2647 | Pat q => promote (findq (thm_frees th) q) th 2648 | Concl => cpos th 2649 fun clean_foralls th = 2650 let val (_,bod) = strip_forall (concl th) 2651 val (l,_) = dest_imp bod 2652 in 2653 pushFAs (free_vars l) th 2654 end 2655 in 2656 th |> underALLs transform |> clean_foralls 2657 end 2658 2659end (* Drule *) 2660 2661(* ====================================================================== 2662 HO_PART_MATCH and bound variables 2663 ====================================================================== 2664 2665Given 2666 2667 val th = GSYM RIGHT_EXISTS_AND_THM 2668 = |- P /\ (?x. Q x) = ?x. P /\ Q x 2669 2670the old implementation would come back from 2671 2672 HO_REWR_CONV th ``P x /\ ?y. Q y`` 2673 2674with 2675 2676 (P x /\ ?y. Q y) = (?x'. P x /\ Q x') 2677 2678This is because of the following: in HO_PART_MATCH, there is code that 2679attempts to rename bound variables from the rewrite theorem so that 2680they match the bound variables in the original term. 2681 2682After performing the ho_match_term, and doing the instantiation, the 2683resulting theorem is 2684 2685 (P x /\ ?x. Q x) = (?x'. P x /\ Q x') 2686 2687The renaming on the rhs has to happen to avoid unsoundness, and 2688happens immediately in the name-carrying kernel, and will happen 2689whenever a dest_abs is done in the dB kernel. Anyway, in the fixup 2690phase, the implementation first notices that ?x.Q x in the pattern 2691corresponds to ?y. Q y in the term. It then passes over the term 2692replacing bound x's with y's. (In the dB kernel, it can't see that 2693the bound variable on the right is actually still an x because 2694dest_abs will rename the x to x'.) 2695 2696So, I thought I would fix this by doing the bound-variable fixup on 2697the pattern theorem before it was instantiated. So, I look at 2698 2699 P /\ ?x. Q x 2700 2701compare it to P x /\ ?y. Q y, and see that bound x needs to be 2702replaced by y throughout the theorem, giving 2703 2704 (P /\ ?y. Q y) = (?y. P /\ Q y) 2705 2706Then the instantiation can be done, producing 2707 2708 (P x /\ ?y. Q y) = (?y. P x /\ Q y) 2709 2710and it's all lovely. (This is also more efficient than the current 2711method because the traversal is only of the original theorem, not its 2712possibly much larger instantiation.) 2713 2714Unfortunately, there are still problems. Consider, this LHS 2715 2716 p /\ ?P. FINITE P 2717 2718when you do the bound variable fix to the rewrite theorem early, you 2719get 2720 2721 (P /\ ?P. Q P) = (?P'. P /\ Q P') 2722 2723The free variables in the theorem itself get in the way. The fix is 2724to examine whether or not the new bound variable clashes with a named 2725variable in the body of the theorem. If so, then the theorem has that 2726variable instantiated to a genvar. (The instantiation returned by 2727ho_match_term also needs to be adjusted because it may be expecting to 2728instantiate some of the pattern theorem's free variables.) 2729 2730So, the code in match_bvs figures out what renamings of bound 2731variables need to happen, and then a traversal of the *whole* theorem 2732takes to see what free variables need to be instantiated into genvars. 2733Then, given the example, the main code in HO_PART_MATCH will produce 2734 2735 (%gv /\ ?x. Q x) = (?x. %gv /\ Q x) 2736 2737before then fixing the bound variables to produce 2738 2739 (%gv /\ ?P. Q P) = (?P. %gv /\ Q P) 2740 2741Finally, this theorem will be instantiated with bindings for Q and 2742%gv [%gv |-> p, Q |-> FINITE]. 2743 2744 ------------------------------ 2745 2746Part 2. 2747 2748Even with the above in place, the ho-part matcher can make a mess of 2749things like the congruence rule for RES_FORALL_CONG, 2750 2751 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==> 2752 (RES_FORALL P f = RES_FORALL Q g) 2753 2754HO_PART_MATCH only gets called with its "partfn" being to look at the 2755LHS of the last equation. Then, when the side conditions are looked 2756over, x gets picked as a bound variable, and any bound variable in f 2757gets ignored. 2758 2759The code in munge_bvars gets around this failing by searching the 2760whole theorem for instances of variables that are going to be 2761instantiated with abstractions that are next to bound variables. (In 2762the example, this search will find f applied to the bound x.) If such 2763a situation is found, it specifies that the bound variable be renamed 2764to match the bound variable of the abstraction. 2765 2766In this way 2767 2768 !y::P. Q y 2769 2770won't get rewritten to 2771 2772 !x::P'. Q' x 2773 2774 ------------------------------ 2775 2776Part 3. (By Peter V. Homeier) 2777 2778The above code was broken for higher order rewriting, such as 2779 2780val th = ASSUME ``!f:'a->'b. A (\x:'c. B (f (C x)) :'d) = (\x. f x)``; 2781val tm = ``A (\rose:'c. B (g (C rose :'a) (C rose) :'b) :'d) : 'a->'b``; 2782HO_PART_MATCH lhs th tm; 2783 2784produced 2785 2786 A (\rose. B (g (C rose) (C rose))) = (\gvar. g gvar gvar) 2787 2788where gvar was a freshly generated "genvar", instead of the correct 2789 2790 A (\rose. B (g (C rose) (C rose))) = (\rose. g rose rose) 2791 2792The reason the prior code did not work was that not only was the 2793match of f with (\y. Q y) recognized for the Part 2 example above, 2794but also the match of f with (\gvar. g gvar gvar) in the "rose" example. 2795The code then "munged" the result by trying to change instances of the 2796"rose" bound variable to "gvar". 2797 2798This was fixed by tightening the condition for entrance to the set of 2799bound variables which are to be so "munged", by adding the condition 2800that the bound variables ("y" in the Part 2 example, "gvar" in this one) 2801must all be contained within the set of bound variables within the term 2802"tm". If they are not, then the "munge" operation is not needed, since 2803that attempts to alter bound variable names to fit the given term, 2804and if the suggested new variable names did not come from the term, 2805there is no reason to change the old ones. 2806*) 2807