1(* ===================================================================== *) 2(* FILE : Tactic.sml *) 3(* DESCRIPTION : Tactics are from LCF. They are a fundamental proof *) 4(* method due to Robin Milner. This file has been *) 5(* translated from hol88. *) 6(* *) 7(* AUTHORS : (c) University of Edinburgh and *) 8(* University of Cambridge, for hol88 *) 9(* TRANSLATOR : Konrad Slind, University of Calgary *) 10(* DATE : September 11, 1991 *) 11(* ===================================================================== *) 12 13structure Tactic :> Tactic = 14struct 15 16open HolKernel Drule Conv Tactical Thm_cont boolTheory boolSyntax Abbrev; 17 18val ERR = mk_HOL_ERR "Tactic" 19 20fun empty th [] = th 21 | empty th _ = raise ERR "empty" "Bind Error" 22fun sing f [x] = f x 23 | sing f _ = raise ERR "sing" "Bind Error" 24fun pairths f [x, y] = f x y 25 | pairths f _ = raise ERR "pairths" "Bind Error" 26 27(*---------------------------------------------------------------------------* 28 * Accepts a theorem that satisfies the goal * 29 * * 30 * A * 31 * ========= ACCEPT_TAC "|-A" * 32 * - * 33 *---------------------------------------------------------------------------*) 34 35val ACCEPT_TAC: thm_tactic = 36 fn th => fn (asl, w) => 37 if aconv (concl th) w then ([], empty th) else raise ERR "ACCEPT_TAC" "" 38 39(* --------------------------------------------------------------------------* 40 * DISCARD_TAC: checks that a theorem is useless, then ignores it. * 41 * Revised: 90.06.15 TFM. * 42 * --------------------------------------------------------------------------*) 43 44fun DISCARD_TAC th (asl, w) = 45 if Lib.exists (aconv (concl th)) (boolSyntax.T :: asl) 46 then ALL_TAC (asl, w) 47 else raise ERR "DISCARD_TAC" "" 48 49(*---------------------------------------------------------------------------* 50 * Contradiction rule * 51 * * 52 * A * 53 * =========== CONTR_TAC "|- F" * 54 * - * 55 *---------------------------------------------------------------------------*) 56 57val CONTR_TAC: thm_tactic = 58 fn cth => fn (asl, w) => 59 let 60 val th = CONTR w cth 61 in 62 ([], empty th) 63 end 64 handle HOL_ERR _ => raise ERR "CONTR_TAC" "" 65 66(* --------------------------------------------------------------------------* 67 * OPPOSITE_TAC: proves the goal using the theorem p and an assumption ~p. * 68 * --------------------------------------------------------------------------*) 69 70local 71 fun resolve th th' = MP (MP (SPEC (concl th) F_IMP) th') th 72 73 fun target_rule tm = 74 if is_neg tm then (dest_neg tm, Lib.C resolve) else (mk_neg tm, resolve) 75in 76 fun OPPOSITE_TAC th (asl, w) = 77 let 78 val (opp, rule) = target_rule (concl th) 79 in 80 case List.find (aconv opp) asl of 81 NONE => raise ERR "OPPOSITE_TAC" "" 82 | SOME asm => CONTR_TAC (rule th (ASSUME asm)) (asl, w) 83 end 84end 85 86(*---------------------------------------------------------------------------* 87 * Classical contradiction rule * 88 * * 89 * A * 90 * =========== CCONTR_TAC * 91 * - * 92 *---------------------------------------------------------------------------*) 93 94fun CCONTR_TAC (asl, w) = ([(mk_neg w :: asl, boolSyntax.F)], sing (CCONTR w)) 95 96(*---------------------------------------------------------------------------* 97 * Put a theorem onto the assumption list. * 98 * Note: since an assumption B denotes a theorem B|-B, * 99 * you cannot instantiate types or variables in assumptions. * 100 * * 101 * A * 102 * =========== |- B * 103 * [B] A * 104 *---------------------------------------------------------------------------*) 105 106val ASSUME_TAC: thm_tactic = 107 fn bth => fn (asl, w) => ([(concl bth :: asl, w)], sing (PROVE_HYP bth)) 108 109val assume_tac = ASSUME_TAC 110 111(*---------------------------------------------------------------------------* 112 * "Freeze" a theorem to prevent instantiation * 113 * * 114 * A * 115 * =========== ttac "B|-B" * 116 * ... * 117 *---------------------------------------------------------------------------*) 118 119val FREEZE_THEN: thm_tactical = 120 fn ttac: thm_tactic => fn bth => fn g => 121 let 122 val (gl, prf) = ttac (ASSUME (concl bth)) g 123 in 124 (gl, PROVE_HYP bth o prf) 125 end 126 127(*---------------------------------------------------------------------------* 128 * Conjunction introduction * 129 * * 130 * A /\ B * 131 * =============== * 132 * A B * 133 *---------------------------------------------------------------------------*) 134 135val CONJ_TAC: tactic = 136 fn (asl, w) => 137 let 138 val (conj1, conj2) = dest_conj w 139 in 140 ([(asl, conj1), (asl, conj2)], 141 fn [th1, th2] => CONJ th1 th2 | _ => raise Match) 142 end 143 handle HOL_ERR _ => raise ERR "CONJ_TAC" "" 144val conj_tac = CONJ_TAC 145 146(* ASM1 & ASM2 variants assume the given conjunct when proving the other one *) 147 148val CONJ_ASM1_TAC = CONJ_TAC THEN_LT USE_SG_THEN ASSUME_TAC 1 2 ; 149val CONJ_ASM2_TAC = CONJ_TAC THEN_LT USE_SG_THEN ASSUME_TAC 2 1 ; 150val conj_asm1_tac = CONJ_ASM1_TAC 151val conj_asm2_tac = CONJ_ASM2_TAC 152 153(*---------------------------------------------------------------------------* 154 * Disjunction introduction * 155 * * 156 * A \/ B * 157 * ============== * 158 * A * 159 * * 160 *---------------------------------------------------------------------------*) 161 162fun DISJ1_TAC (asl, w) = 163 let 164 val (disj1, disj2) = dest_disj w 165 in 166 ([(asl, disj1)], sing (fn th => DISJ1 th disj2)) 167 end 168 handle HOL_ERR _ => raise ERR "DISJ1_TAC" "" 169val disj1_tac = DISJ1_TAC 170 171(*---------------------------------------------------------------------------* 172 * A \/ B * 173 * ============== * 174 * B * 175 * * 176 *---------------------------------------------------------------------------*) 177 178fun DISJ2_TAC (asl, w) = 179 let 180 val (disj1, disj2) = dest_disj w 181 in 182 ([(asl, disj2)], sing (DISJ2 disj1)) 183 end 184 handle HOL_ERR _ => raise ERR "DISJ2_TAC" "" 185val disj2_tac = DISJ2_TAC 186 187(*---------------------------------------------------------------------------* 188 * Implication elimination * 189 * * 190 * A * 191 * |- B ================ * 192 * B ==> A * 193 * * 194 *---------------------------------------------------------------------------*) 195 196fun MP_TAC thb (asl, w) = 197 ([(asl, mk_imp (concl thb, w))], sing (fn thimp => MP thimp thb)) 198val mp_tac = MP_TAC 199 200(*---------------------------------------------------------------------------* 201 * Equality Introduction * 202 * * 203 * A = B * 204 * ===================== * 205 * A ==> B B ==> A * 206 * * 207 *---------------------------------------------------------------------------*) 208 209val EQ_TAC: tactic = 210 fn (asl, t) => 211 let 212 val (lhs, rhs) = dest_eq t 213 in 214 ([(asl, mk_imp (lhs, rhs)), (asl, mk_imp (rhs, lhs))], 215 fn [th1, th2] => IMP_ANTISYM_RULE th1 th2 | _ => raise Match) 216 end 217 handle HOL_ERR _ => raise ERR "EQ_TAC" "" 218val eq_tac = EQ_TAC 219 220(*---------------------------------------------------------------------------* 221 * Universal quantifier * 222 * * 223 * !x.A(x) * 224 * ============== * 225 * A(x') * 226 * * 227 * Explicit version for tactic programming; proof fails if x' is free in * 228 * hyps. * 229 * * 230 * fun X_GEN_TAC x' :tactic (asl,w) = * 231 * (let val x,body = dest_forall w in * 232 * [ (asl, subst[x',x]body) ], (\[th]. GEN x' th) * 233 * ) ? failwith X_GEN_TAC; * 234 * * 235 * T. Melham. X_GEN_TAC rewritten 88.09.17 * 236 * * 237 * 1) X_GEN_TAC x' now fails if x' is not a variable. * 238 * * 239 * 2) rewritten so that the proof yields the same quantified var as the * 240 * goal. * 241 * * 242 * fun X_GEN_TAC x' :tactic = * 243 * if not(is_var x') then failwith X_GEN_TAC else * 244 * \(asl,w).((let val x,body = dest_forall w in * 245 * [(asl,subst[x',x]body)], * 246 * (\[th]. GEN x (INST [(x,x')] th))) * 247 * ? failwith X_GEN_TAC); * 248 * Bugfix for HOL88.1.05, MJCG, 4 April 1989 * 249 * Instantiation before GEN replaced by alpha-conversion after it to * 250 * prevent spurious failures due to bound variable problems when * 251 * quantified variable is free in assumptions. * 252 * Optimization for the x=x' case added. * 253 *---------------------------------------------------------------------------*) 254 255fun X_GEN_TAC x1 : tactic = 256 fn (asl, w) => 257 if is_var x1 258 then let 259 val (Bvar, Body) = dest_forall w 260 in 261 if aconv Bvar x1 then ([(asl, Body)], sing (GEN x1)) 262 else ([(asl, subst [Bvar |-> x1] Body)], 263 sing (fn th => 264 let 265 val th' = GEN x1 th 266 in 267 EQ_MP (GEN_ALPHA_CONV Bvar (concl th')) th' 268 end)) 269 end 270 handle HOL_ERR _ => raise ERR "X_GEN_TAC" "" 271 else raise ERR "X_GEN_TAC" "need a variable" 272 273(*---------------------------------------------------------------------------* 274 * GEN_TAC - Chooses a variant for the user; for interactive proof * 275 *---------------------------------------------------------------------------*) 276 277val GEN_TAC: tactic = 278 fn (asl, w) => 279 let 280 val (Bvar, _) = with_exn dest_forall w (ERR "GEN_TAC" "not a forall") 281 in 282 X_GEN_TAC 283 (gen_variant Parse.is_constname "" (free_varsl (w :: asl)) Bvar) 284 (asl, w) 285 end 286val gen_tac = GEN_TAC 287 288(*---------------------------------------------------------------------------* 289 * Specialization * 290 * A(t) * 291 * ============ t,x * 292 * !x.A(x) * 293 * * 294 * Example of use: generalizing a goal before attempting an inductive proof * 295 * as with Boyer and Moore. * 296 *---------------------------------------------------------------------------*) 297 298fun SPEC_TAC (t, x) : tactic = 299 fn (asl, w) => 300 ([(asl, mk_forall (x, subst [t |-> x] w))], sing (SPEC t)) 301 handle HOL_ERR _ => raise ERR "SPEC_TAC" "" 302 303fun ID_SPEC_TAC x : tactic = 304 fn (asl, w) => 305 ([(asl, mk_forall (x, w))], sing (SPEC x)) 306 handle HOL_ERR _ => raise ERR "SPEC_TAC" "" 307 308(*---------------------------------------------------------------------------* 309 * Existential introduction * 310 * * 311 * ?x.A(x) * 312 * ============== t * 313 * A(t) * 314 *---------------------------------------------------------------------------*) 315 316fun EXISTS_TAC t : tactic = 317 fn (asl, w) => 318 let 319 val (Bvar, Body) = dest_exists w 320 in 321 ([(asl, subst [Bvar |-> t] Body)], sing (EXISTS (w, t))) 322 end 323 handle HOL_ERR _ => raise ERR "EXISTS_TAC" "" 324val exists_tac = EXISTS_TAC 325 326fun ID_EX_TAC(g as (_,w)) = 327 EXISTS_TAC (fst(dest_exists w) 328 handle HOL_ERR _ => raise ERR "ID_EX_TAC" "goal not an exists") g; 329 330 331 332(*---------------------------------------------------------------------------* 333 * Substitution * 334 * * 335 * These substitute in the goal; thus they DO NOT invert the rules SUBS and * 336 * SUBS_OCCS, despite superficial similarities. In fact, SUBS and SUBS_OCCS * 337 * are not invertible; only SUBST is. * 338 *---------------------------------------------------------------------------*) 339 340fun GSUBST_TAC substfn ths (asl, w) = 341 let 342 val (theta1, theta2, theta3) = 343 itlist (fn th => fn (theta1, theta2, theta3) => 344 let 345 val (lhs, rhs) = dest_eq (concl th) 346 val v = Term.genvar (type_of lhs) 347 in 348 ((lhs |-> v) :: theta1, 349 (v |-> rhs) :: theta2, 350 (v |-> SYM th) :: theta3) 351 end) ths ([], [], []) 352 val base = substfn theta1 w 353 in 354 ([(asl, subst theta2 base)], sing (SUBST theta3 base)) 355 end 356 handle HOL_ERR _ => raise ERR "GSUBST_TAC" "" 357 358(*---------------------------------------------------------------------------* 359 * A(ti) * 360 * ============== |- ti == ui * 361 * A(ui) * 362 *---------------------------------------------------------------------------*) 363 364fun SUBST_TAC ths = 365 GSUBST_TAC subst ths handle HOL_ERR _ => raise ERR "SUBST_TAC" "" 366 367fun SUBST_OCCS_TAC nlths = 368 let 369 val (nll, ths) = unzip nlths 370 in 371 GSUBST_TAC (subst_occs nll) ths 372 end 373 handle HOL_ERR _ => raise ERR "SUBST_OCCS_TAC" "" 374 375(*---------------------------------------------------------------------------* 376 * A(t) * 377 * =============== |- t==u * 378 * A(u) * 379 * * 380 * Works nicely with tacticals. * 381 *---------------------------------------------------------------------------*) 382 383fun SUBST1_TAC rthm = SUBST_TAC [rthm] 384 385(*---------------------------------------------------------------------------* 386 * Map an inference rule over the assumptions, replacing them. * 387 *---------------------------------------------------------------------------*) 388 389fun RULE_ASSUM_TAC rule : tactic = 390 POP_ASSUM_LIST 391 (fn asl => MAP_EVERY ASSUME_TAC (rev_itlist (cons o rule) asl [])) 392val rule_assum_tac = RULE_ASSUM_TAC 393 394fun RULE_L_ASSUM_TAC rule : tactic = 395 POP_ASSUM_LIST 396 (fn asl => MAP_EVERY ASSUME_TAC (rev_itlist (append o rule) asl [])) 397 398(*---------------------------------------------------------------------------* 399 * Substitute throughout the goal and its assumptions. * 400 *---------------------------------------------------------------------------*) 401 402fun SUBST_ALL_TAC rth = SUBST1_TAC rth THEN RULE_ASSUM_TAC (SUBS [rth]) 403 404val CHECK_ASSUME_TAC: thm_tactic = 405 fn gth => 406 FIRST [CONTR_TAC gth, ACCEPT_TAC gth, OPPOSITE_TAC gth, 407 DISCARD_TAC gth, ASSUME_TAC gth] 408 409val STRIP_ASSUME_TAC = REPEAT_TCL STRIP_THM_THEN CHECK_ASSUME_TAC 410val strip_assume_tac = STRIP_ASSUME_TAC 411 412(*---------------------------------------------------------------------------* 413 * given a theorem: * 414 * * 415 * |- (?y1. (x=t1(y1)) /\ B1(x,y1)) \/...\/ (?yn. (x=tn(yn)) /\ Bn(x,yn)) * 416 * * 417 * where each y is a vector of zero or more variables and each Bi is a * 418 * conjunction (Ci1 /\ ... /\ Cin) * 419 * * 420 * A(x) * 421 * =============================================== * 422 * [Ci1(tm,y1')] A(t1) . . . [Cin(tm,yn')] A(tn) * 423 * * 424 * such definitions specify a structure as having n different possible * 425 * constructions (the ti) from subcomponents (the yi) that satisfy various * 426 * constraints (the Cij). * 427 *---------------------------------------------------------------------------*) 428 429val STRUCT_CASES_TAC = 430 REPEAT_TCL STRIP_THM_THEN (fn th => SUBST1_TAC th ORELSE ASSUME_TAC th) 431 432val FULL_STRUCT_CASES_TAC = 433 REPEAT_TCL STRIP_THM_THEN (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th) 434 435(*---------------------------------------------------------------------------* 436 * COND_CASES_TAC: tactic for doing a case split on the condition p * 437 * in a conditional (p => u | v). * 438 * * 439 * Find a conditional "p => u | v" that is free in the goal and whose * 440 * condition p is not a constant. Perform a case split on the condition. * 441 * * 442 * t[p=>u|v] * 443 * ================= COND_CASES_TAC * 444 * {p} t[u] * 445 * {~p} t[v] * 446 * * 447 * [Revised: TFM 90.05.11] * 448 *---------------------------------------------------------------------------*) 449 450fun GEN_COND_CASES_TAC P (asl, w) = 451 let 452 val cond = find_term (fn tm => P tm andalso free_in tm w) w 453 handle HOL_ERR _ => raise ERR "GEN_COND_CASES_TAC" "" 454 val (cond, larm, rarm) = dest_cond cond 455 val inst = INST_TYPE [Type.alpha |-> type_of larm] COND_CLAUSES 456 val (ct, cf) = CONJ_PAIR (SPEC rarm (SPEC larm inst)) 457 fun subst_tac th c = SUBST1_TAC th THEN SUBST1_TAC (SUBS [th] c) 458 in 459 DISJ_CASES_THEN2 460 (fn th => 461 subst_tac (EQT_INTRO th) ct THEN ASSUME_TAC th) 462 (fn th => 463 subst_tac (EQF_INTRO th) cf THEN ASSUME_TAC th) 464 (SPEC cond EXCLUDED_MIDDLE) 465 (asl, w) 466 end 467 468local 469 fun bool_can P x = P x handle HOL_ERR _ => false 470in 471 val COND_CASES_TAC = 472 GEN_COND_CASES_TAC (bool_can (not o is_const o #1 o dest_cond)) 473end 474 475(*--------------------------------------------------------------------------- 476 Version of COND_CASES_TAC that handles nested conditionals 477 in the test of a conditional nicely (by not putting them onto 478 the assumptions). 479 ---------------------------------------------------------------------------*) 480 481val IF_CASES_TAC = 482 let 483 fun test tm = 484 let 485 val (b,_,_) = dest_cond tm 486 in 487 not (is_const b orelse is_cond b) 488 end 489 handle HOL_ERR _ => false 490 in 491 GEN_COND_CASES_TAC test 492 end 493 494(*---------------------------------------------------------------------------* 495 * Cases on |- p=T \/ p=F * 496 *---------------------------------------------------------------------------*) 497 498fun BOOL_CASES_TAC p = STRUCT_CASES_TAC (SPEC p BOOL_CASES_AX) 499 500(*---------------------------------------------------------------------------* 501 * Strip one outer !, /\, ==> from the goal. * 502 *---------------------------------------------------------------------------*) 503 504fun STRIP_GOAL_THEN ttac = FIRST [GEN_TAC, CONJ_TAC, DISCH_THEN ttac] 505 506(*---------------------------------------------------------------------------* 507 * Like GEN_TAC but fails if the term equals the quantified variable. * 508 *---------------------------------------------------------------------------*) 509 510fun FILTER_GEN_TAC tm : tactic = 511 fn (asl, w) => 512 if is_forall w andalso not (aconv tm (fst (dest_forall w))) 513 then GEN_TAC (asl, w) 514 else raise ERR "FILTER_GEN_TAC" "" 515 516(*---------------------------------------------------------------------------* 517 * Like DISCH_THEN but fails if the antecedent mentions the given term. * 518 *---------------------------------------------------------------------------*) 519 520fun FILTER_DISCH_THEN ttac tm = fn (asl, w) => 521 if is_imp w andalso not (free_in tm (fst (dest_imp w))) 522 then DISCH_THEN ttac (asl, w) 523 else raise ERR "FILTER_DISCH_THEN" "" 524 525(*---------------------------------------------------------------------------* 526 * Like STRIP_THEN but preserves any part of the goal mentioning the term. * 527 *---------------------------------------------------------------------------*) 528 529fun FILTER_STRIP_THEN ttac tm = 530 FIRST [FILTER_GEN_TAC tm, FILTER_DISCH_THEN ttac tm, CONJ_TAC] 531 532fun DISCH_TAC g = 533 DISCH_THEN ASSUME_TAC g handle HOL_ERR _ => raise ERR "DISCH_TAC" "" 534 535val disch_tac = DISCH_TAC 536 537val FILTER_DISCH_TAC = FILTER_DISCH_THEN STRIP_ASSUME_TAC 538 539val DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC 540 541val CHOOSE_TAC = CHOOSE_THEN ASSUME_TAC 542 543fun X_CHOOSE_TAC x = X_CHOOSE_THEN x ASSUME_TAC 544 545fun STRIP_TAC g = 546 STRIP_GOAL_THEN STRIP_ASSUME_TAC g 547 handle HOL_ERR _ => raise ERR "STRIP_TAC" "" 548val strip_tac = STRIP_TAC 549 550val FILTER_STRIP_TAC = FILTER_STRIP_THEN STRIP_ASSUME_TAC 551 552(*---------------------------------------------------------------------------* 553 * Cases on |- t \/ ~t * 554 *---------------------------------------------------------------------------*) 555 556fun ASM_CASES_TAC t = DISJ_CASES_TAC (SPEC t EXCLUDED_MIDDLE) 557 558(*---------------------------------------------------------------------------* 559 * A tactic inverting REFL (from tfm). * 560 * * 561 * A = A * 562 * ============== * 563 * * 564 * Revised to work if lhs is alpha-equivalent to rhs [TFM 91.02.02] * 565 * Also revised to retain assumptions. * 566 *---------------------------------------------------------------------------*) 567 568fun REFL_TAC (asl, g) = 569 let 570 val (lhs, rhs) = with_exn dest_eq g (ERR "REFL_TAC" "not an equation") 571 val asms = itlist ADD_ASSUM asl 572 in 573 if aconv lhs rhs then ([], K (asms (REFL lhs))) 574 else raise ERR "REFL_TAC" "lhs and rhs not alpha-equivalent" 575 end 576 577(*---------------------------------------------------------------------------* 578 * UNDISCH_TAC - moves one of the assumptions as LHS of an implication * 579 * to the goal (fails if named assumption not in assumptions) * 580 * * 581 * UNDISCH_TAC: term -> tactic * 582 * tm * 583 * * 584 * [ t1;t2;...;tm;tn;...tz ] t * 585 * ====================================== * 586 * [ t1;t2;...;tn;...tz ] tm ==> t * 587 *---------------------------------------------------------------------------*) 588 589fun UNDISCH_TAC wf (asl, w) = 590 if op_mem term_eq wf asl 591 then ([(op_set_diff term_eq asl [wf], mk_imp (wf, w))], 592 UNDISCH o Lib.trye hd) 593 else raise ERR "UNDISCH_TAC" "Specified term not in assumption list" 594 595(*---------------------------------------------------------------------------* 596 * AP_TERM_TAC: Strips a function application off the lhs and rhs of an * 597 * equation. If the function is not one-to-one, does not preserve * 598 * equivalence of the goal and subgoal. * 599 * * 600 * f x = f y * 601 * ============= * 602 * x = y * 603 * * 604 * Added: TFM 88.03.31 * 605 * Revised: TFM 91.02.02 * 606 *---------------------------------------------------------------------------*) 607 608local 609 fun ER s = ERR "AP_TERM_TAC" s 610in 611 fun AP_TERM_TAC (asl, gl) = 612 let 613 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") 614 val (g, x) = with_exn dest_comb lhs (ER "lhs not a comb") 615 val (f, y) = with_exn dest_comb rhs (ER "rhs not a comb") 616 in 617 if not (term_eq f g) 618 then raise ER "functions on lhs and rhs differ" 619 else ([(asl, mk_eq (x, y))], AP_TERM f o Lib.trye hd) 620 end 621end 622 623(*---------------------------------------------------------------------------* 624 * AP_THM_TAC: inverts the AP_THM inference rule. * 625 * * 626 * f x = g x * 627 * ============= * 628 * f = g * 629 * * 630 * Added: TFM 91.02.02 * 631 *---------------------------------------------------------------------------*) 632 633local 634 fun ER s = ERR "AP_THM_TAC" s 635in 636 fun AP_THM_TAC (asl, gl) = 637 let 638 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") 639 val (g, x) = with_exn dest_comb lhs (ER "lhs not a comb") 640 val (f, y) = with_exn dest_comb rhs (ER "rhs not a comb") 641 in 642 if not (term_eq x y) 643 then raise ER "arguments on lhs and rhs differ" 644 else ([(asl, mk_eq (g, f))], C AP_THM x o Lib.trye hd) 645 end 646end 647 648(*---------------------------------------------------------------------------* 649 * MK_COMB_TAC - reduces ?- f x = g y to ?- f = g and ?- x = y (JRH) * 650 *---------------------------------------------------------------------------*) 651 652local 653 fun ER s = ERR "MK_COMB_TAC" s 654in 655 fun MK_COMB_TAC (asl, w) = 656 let 657 val (lhs, rhs) = with_exn dest_eq w (ER "not an equation") 658 val (l1, l2) = with_exn dest_comb lhs (ER "lhs not a comb") 659 val (r1, r2) = with_exn dest_comb rhs (ER "rhs not a comb") 660 in 661 ([(asl, mk_eq (l1, r1)), (asl, mk_eq (l2, r2))], 662 end_itlist (curry MK_COMB)) 663 end 664end 665 666(*---------------------------------------------------------------------------* 667 * BINOP_TAC - reduces "$op x y = $op u v" to "x = u" and "y = v" (JRH) * 668 *---------------------------------------------------------------------------*) 669 670val BINOP_TAC = MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC] 671 672(*---------------------------------------------------------------------------* 673 * ABS_TAC: inverts the ABS inference rule. * 674 * * 675 * \x. f x = \x. g x * 676 * ===================== * 677 * f x = g x * 678 * * 679 * Added: TT 2009.12.23 * 680 *---------------------------------------------------------------------------*) 681 682local 683 fun ER s = ERR "ABS_TAC" s 684in 685 fun ABS_TAC (asl: term list, gl) = 686 let 687 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") 688 val (x, g) = with_exn dest_abs lhs (ER "lhs not an abstraction") 689 val (y, f) = with_exn dest_abs rhs (ER "rhs not an abstraction") 690 val f_thm = if aconv x y then REFL rhs else ALPHA_CONV x rhs 691 val (_, f') = dest_abs (rand (concl f_thm)) 692 in 693 ([(asl, mk_eq (g, f'))], 694 CONV_RULE (RHS_CONV (K (GSYM f_thm))) o ABS x o Lib.trye hd) 695 end 696end 697 698(*---------------------------------------------------------------------------* 699 * NTAC n tac - Applies the tactic the given number of times. * 700 *---------------------------------------------------------------------------*) 701 702fun NTAC n tac = funpow n (curry op THEN tac) ALL_TAC 703val ntac = NTAC 704 705(*---------------------------------------------------------------------------* 706 * WEAKEN_TAC tm - Removes the first term meeting P from the hypotheses * 707 * of the goal. * 708 *---------------------------------------------------------------------------*) 709 710fun WEAKEN_TAC P : tactic = 711 fn (asl, w) => 712 let 713 fun robustP x = Lib.trye P x handle HOL_ERR _ => false 714 val (tm, rst) = 715 Lib.pluck robustP asl 716 handle HOL_ERR _ => 717 raise ERR "WEAKEN_TAC" "no matching item found in hypotheses" 718 in 719 ([(rst, w)], sing (ADD_ASSUM tm)) 720 end 721 722(* ---------------------------------------------------------------------* 723 * Accept a theorem that, properly instantiated, satisfies the goal * 724 * ---------------------------------------------------------------------*) 725 726fun MATCH_ACCEPT_TAC thm : tactic = 727 let 728 val fmatch = PART_MATCH Lib.I thm 729 fun atac (asl, w) = ([], Lib.K (fmatch w)) 730 in 731 REPEAT GEN_TAC THEN atac 732 end 733 handle HOL_ERR _ => raise ERR "MATCH_ACCEPT_TAC" "" 734 735(* ---------------------------------------------------------------------* 736 * prim_irule : Similar to MATCH_ACCEPT_TAC but * 737 * (1) allows substitution in hypotheses of the supplied theorem * 738 * (2) adds new subgoals for those hypotheses * 739 * ---------------------------------------------------------------------*) 740 741fun prim_irule thm (asl, w) = 742 let val matchsub = match_term (concl thm) w ; 743 val (subthm, subhyps) = INST_TT_HYPS matchsub thm ; 744 in ADD_SGS_TAC subhyps (ACCEPT_TAC subthm) (asl, w) end ; 745 746(* --------------------------------------------------------------------------* 747 * MATCH_MP_TAC: Takes a theorem of the form * 748 * * 749 * |- !x1..xn. A ==> !y1 ... ym. B * 750 * * 751 * and matches B to the goal, reducing it to the subgoal consisting of * 752 * some existentially-quantified instance of A: * 753 * * 754 * !v1...vi. B * 755 * ======================= MATCH_MP_TAC |- !x1...1n. A ==> !y1...ym. B * 756 * ?z1...zp. A * 757 * * 758 * where {z1,...,zn} is the subset of {x1,...,xn} whose elements do not * 759 * appear free in B. * 760 * * 761 * Added: TFM 88.03.31 * 762 * Revised: TFM 91.04.20 * 763 * * 764 * Old version: * 765 * * 766 * let MATCH_MP_TAC thm:tactic (gl,g) = * 767 * let imp = ((PART_MATCH (snd o dest_imp) thm) g) ? * 768 * failwith `MATCH_MP_TAC` in * 769 * ([gl,(fst(dest_imp(concl imp)))], \thl. MP imp (hd thl)); * 770 * --------------------------------------------------------------------------*) 771 772local 773 fun efn v (tm, th) = 774 let val ntm = mk_exists (v, tm) in (ntm, CHOOSE (v, ASSUME ntm) th) end 775in 776 fun MATCH_MP_TAC thm : tactic = 777 let 778 val lconsts = 779 HOLset.intersection (FVL [concl thm] empty_tmset, hyp_frees thm) 780 val hyptyvars = HOLset.listItems (hyp_tyvars thm) 781 val (gvs, imp) = strip_forall (concl thm) 782 in 783 fn (A,g) => 784 let 785 val (ant, conseq) = 786 with_exn dest_imp imp (ERR "MATCH_MP_TAC" "Not an implication") 787 val (cvs, con) = strip_forall conseq 788 val th1 = SPECL cvs (UNDISCH (SPECL gvs thm)) 789 val (vs, evs) = partition (C Term.free_in con) gvs 790 val th2 = uncurry DISCH (itlist efn evs (ant, th1)) 791 val (vs, gl) = strip_forall g 792 val ins = match_terml hyptyvars lconsts con gl 793 handle HOL_ERR _ => raise ERR "MATCH_MP_TAC" "No match" 794 val ith = INST_TY_TERM ins th2 795 val gth = GENL vs (UNDISCH ith) 796 handle HOL_ERR _ => raise ERR "MATCH_MP_TAC" 797 "Generalized var(s)." 798 val ant = fst (dest_imp (concl ith)) 799 in 800 ([(A, ant)], fn thl => MP (DISCH ant gth) (hd thl)) 801 end 802 end 803 val match_mp_tac = MATCH_MP_TAC 804end 805 806(* --------------------------------------------------------------------------* 807 * irule: similar to MATCH_MP_TAC, but * 808 * (1) uses conclusion following more than one ==> * 809 * (2) where multiple assumptions involve the same variable that is not in * 810 * the conclusion (as y in x = y ==> y = z ==> x = z), collects them * 811 * and existentially quantifies * 812 * (3) hypotheses of the theorem provided also become new subgoals * 813 * --------------------------------------------------------------------------*) 814 815fun irule thm = let 816 val th' = IRULE_CANON thm 817in 818 if th' |> concl |> strip_forall |> #2 |> is_imp then 819 MATCH_MP_TAC th' 820 else MATCH_ACCEPT_TAC th' 821end 822fun irule_at pos thm = 823 let 824 open resolve_then 825 in 826 case pos of 827 Concl => irule thm 828 | Any => irule thm ORELSE goal_assum (resolve_then Any mp_tac thm) 829 | _ => goal_assum (resolve_then pos mp_tac thm) 830 end 831val IRULE_TAC = irule 832 833 834(* ----------------------------------------------------------------------* 835 * Definition of the standard resolution tactics IMP_RES_TAC and RES_TAC * 836 * * 837 * The function SA is like STRIP_ASSUME_TAC, except that it does not * 838 * strip off existential quantifiers. And ST is like STRIP_THM_THEN, * 839 * except that it also does not strip existential quantifiers. * 840 * * 841 * Old version: deleted for HOL version 1.12 [TFM 91.01.17] * 842 * * 843 * let (IMP_RES_TAC,RES_TAC) = * 844 * let ST = FIRST_TCL [CONJUNCTS_THEN; DISJ_CASES_THEN] in * 845 * let SA = (REPEAT_TCL ST) CHECK_ASSUME_TAC in * 846 * (IMP_RES_THEN SA, RES_THEN SA); * 847 * * 848 * The "new" versions of IMP_RES_TAC and RES_TAC: repeatedly resolve, * 849 * and then add FULLY stripped, final, result(s) to the assumptions. * 850 * ----------------------------------------------------------------------*) 851 852local 853 open Thm_cont 854in 855 fun IMP_RES_TAC th g = 856 IMP_RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) th g 857 handle HOL_ERR _ => ALL_TAC g 858 859 fun RES_TAC g = 860 RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) g 861 handle HOL_ERR _ => ALL_TAC g 862 863 val res_tac = RES_TAC 864 val imp_res_tac = IMP_RES_TAC 865end 866 867(*--------------------------------------------------------------------------* 868 * Assertional style reasoning * 869 *--------------------------------------------------------------------------*) 870 871(* First we need a variant on THEN. *) 872 873fun THENF (tac1: tactic, tac2: tactic, tac3: tactic) g = 874 case tac1 g of 875 (h::rst, p) => 876 let 877 val (gl0, p0) = tac2 h 878 val (gln, pn) = unzip (map tac3 rst) 879 val gll = gl0 @ flatten gln 880 in 881 (gll, p o mapshape (length gl0 :: map length gln) (p0 :: pn)) 882 end 883 | x => x 884 885infix 8 via; 886 887fun (tm via tac) = 888 THENF (SUBGOAL_THEN tm STRIP_ASSUME_TAC, tac, ALL_TAC) 889 handle e as HOL_ERR _ => raise ERR "via" "" 890 891(*--------------------------------------------------------------------------* 892 * Tactic for beta-reducing a goal. * 893 *--------------------------------------------------------------------------*) 894 895val BETA_TAC = CONV_TAC (DEPTH_CONV BETA_CONV) 896 897(* ---------------------------------------------------------------------* 898 * Accept a theorem that, properly instantiated, satisfies the goal * 899 * ---------------------------------------------------------------------*) 900 901fun HO_MATCH_ACCEPT_TAC thm = 902 let 903 val fmatch = HO_PART_MATCH I thm 904 fun atac (asl, w) = ([], K (fmatch w)) 905 in 906 REPEAT GEN_TAC THEN atac 907 end 908 handle HOL_ERR _ => raise ERR "HO_MATCH_ACCEPT_TAC" "" 909 910(*-------------------------------------------------------------------------* 911 * Simplified version of HO_MATCH_MP_TAC to avoid quantifier troubles. * 912 *-------------------------------------------------------------------------*) 913 914fun HO_BACKCHAIN_TAC th = 915 let 916 val match_fn = HO_PART_MATCH (snd o dest_imp_only) th 917 in 918 fn (asl, w) => 919 let 920 val th1 = match_fn w 921 val (ant, _) = dest_imp_only (concl th1) 922 in 923 ([(asl, ant)], sing (HO_MATCH_MP th1)) 924 end 925 end 926 927fun HO_MATCH_MP_TAC th = 928 let 929 val sth = 930 let 931 val tm = concl th 932 val (avs, bod) = strip_forall tm 933 val (ant, conseq) = dest_imp_only bod 934 val th1 = SPECL avs (ASSUME tm) 935 val th2 = UNDISCH th1 936 val evs = 937 filter (fn v => free_in v ant andalso not (free_in v conseq)) avs 938 val th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2) 939 val tm3 = Lib.trye hd (hyp th3) 940 in 941 MP (DISCH tm (GEN_ALL (DISCH tm3 (UNDISCH th3)))) th 942 end 943 handle HOL_ERR _ => raise ERR "HO_MATCH_MP_TAC" "Bad theorem" 944 val match_fun = HO_PART_MATCH (snd o dest_imp_only) sth 945 in 946 fn (asl, w) => 947 let 948 val xth = match_fun w 949 val lant = fst (dest_imp_only (concl xth)) 950 in 951 ([(asl, lant)], MP xth o Lib.trye hd) 952 end 953 handle e => raise (wrap_exn "Tactic" "HO_MATCH_MP_TAC" e) 954 end 955 956val ho_match_mp_tac = HO_MATCH_MP_TAC 957 958(*----------------------------------------------------------------------* 959 * Tactics explicitly declaring subgoals. * 960 *----------------------------------------------------------------------*) 961 962fun SUFF_TAC tm (al, c) = 963 ([(al, mk_imp (tm, c)), (al, tm)], 964 fn [th1, th2] => MP th1 th2 965 | _ => raise ERR "SUFF_TAC" "panic") 966val suff_tac = SUFF_TAC 967 968fun KNOW_TAC tm = REVERSE (SUFF_TAC tm) 969 970(* ---------------------------------------------------------------------- 971 Eliminate an equation on a variable (as well as t = t instances) 972 ---------------------------------------------------------------------- *) 973 974fun eliminable tm = 975 let val (lhs,rhs) = dest_eq tm 976 in 977 aconv lhs rhs orelse 978 (is_var lhs andalso not (free_in lhs rhs)) orelse 979 (is_var rhs andalso not (free_in rhs lhs)) 980 end handle HOL_ERR _ => is_bool_atom tm 981 982fun orient th = 983 let 984 val c = concl th 985 in 986 if is_bool_atom c then 987 if is_neg c then EQF_INTRO th else EQT_INTRO th 988 else 989 let 990 val (lhs,rhs) = dest_eq c 991 in 992 if is_var lhs then 993 if is_var rhs then 994 case Term.compare (lhs, rhs) of LESS => SYM th | other => th 995 else th 996 else SYM th 997 end 998 end; 999 1000fun eliminable_eqvar t = 1001 is_bool_atom t orelse (let val (l,r) = dest_eq t in l !~ r end) 1002 1003fun VSUBST_TAC thm = 1004 if eliminable_eqvar (concl thm) then 1005 SUBST_ALL_TAC (orient thm) 1006 else (* do nothing as it's of form t = t *) 1007 ALL_TAC 1008 1009 1010(*----------------------------------------------------------------------* 1011 * DEEP_INTROk_TAC : thm -> tactic -> tactic * 1012 *----------------------------------------------------------------------*) 1013 1014fun gvarify th = 1015 let 1016 val th = SPEC_ALL th 1017 val fvs = FVL [concl th] empty_tmset 1018 val hfvs = hyp_frees th 1019 val true_frees = HOLset.difference (fvs, hfvs) 1020 fun foldthis (fv, acc) = (fv |-> genvar (type_of fv)) :: acc 1021 in 1022 INST (HOLset.foldl foldthis [] true_frees) th 1023 end 1024 1025fun IMP2AND_CONV t = 1026 if is_imp t 1027 then (RAND_CONV IMP2AND_CONV THENC TRY_CONV (REWR_CONV AND_IMP_INTRO)) t 1028 else ALL_CONV t 1029 1030fun DEEP_INTROk_TAC th tac (asl, g) = 1031 let 1032 val th = th |> CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV THENC 1033 STRIP_QUANT_CONV IMP2AND_CONV) 1034 |> GEN_ALL 1035 val hyfrees = hyp_frees th 1036 val hytyvars = hyp_tyvars th 1037 val (_, Ppattern) = th |> concl |> strip_forall |> #2 |> dest_imp 1038 val (Pvar, pattern) = dest_comb Ppattern 1039 val _ = is_var Pvar 1040 orelse raise ERR "DEEP_INTROk_TAC" 1041 "Conclusion not of form ``var (pattern)``" 1042 fun test (bvs, t) = 1043 let 1044 val ((theta_tms, tmids), _) = 1045 raw_match (HOLset.listItems hytyvars) hyfrees pattern t ([], []) 1046 val bv_set = HOLset.fromList Term.compare bvs 1047 fun testtheta {redex, residue} = 1048 let 1049 val rfrees = FVL [residue] empty_tmset 1050 in 1051 HOLset.isEmpty (HOLset.intersection (rfrees, bv_set)) 1052 end 1053 in 1054 List.all testtheta theta_tms 1055 andalso HOLset.isEmpty (HOLset.intersection (bv_set, tmids)) 1056 end 1057 handle HOL_ERR _ (* if match fails *) => false 1058 fun continuation subt = 1059 (CONV_TAC (UNBETA_CONV subt) THEN 1060 MATCH_MP_TAC th THEN BETA_TAC THEN tac) (asl, g) 1061 in 1062 case bvk_find_term test continuation g of 1063 SOME result => result 1064 | NONE => raise ERR "DEEP_INTROk_TAC" "No matching sub-terms" 1065 end 1066 1067fun DEEP_INTRO_TAC th = DEEP_INTROk_TAC th ALL_TAC 1068 1069(*----------------------------------------------------------------------* 1070 * SELECT_ELIM_TAC * 1071 * eliminates a select term from the goal. * 1072 *----------------------------------------------------------------------*) 1073 1074val SELECT_ELIM_TAC = DEEP_INTRO_TAC SELECT_ELIM_THM 1075 1076 1077(*----------------------------------------------------------------------* 1078 * HINT_EXISTS_TAC * 1079 * instantiates an existential by using hints from the assumptions. * 1080 *----------------------------------------------------------------------*) 1081 1082fun HINT_EXISTS_TAC g = 1083 let 1084 val (hs,c) = g 1085 val (v,c') = dest_exists c 1086 val (vs,c') = strip_exists c' 1087 fun hyp_match c h = 1088 if exists (C (op_mem aconv) vs) (free_vars c) then fail () 1089 else match_term c h 1090 val (subs,_) = tryfind (C tryfind hs o hyp_match) (strip_conj c') 1091 val witness = 1092 case subs of 1093 [] => v 1094 |[{redex = u, residue = t}] => 1095 if aconv u v then t else failwith "HINT_EXISTS_TAC not applicable" 1096 |_ => failwith "HINT_EXISTS_TAC not applicable" 1097 in 1098 EXISTS_TAC witness g 1099 end; 1100 1101(* ---------------------------------------------------------------------- 1102 part_match_exists_tac : (term -> term) -> term -> tactic 1103 1104 part_match_exists_tac selfn tm (asl,w) 1105 1106 w must be of shape ?v1 .. vn. body. 1107 1108 Apply selfn to body extracting a term that is then matched against 1109 tm. Instantiate the existential variables according to this match. 1110 1111 ---------------------------------------------------------------------- *) 1112 1113fun part_match_exists_tac selfn tm (g as (_,w)) = 1114 let 1115 val (vs,b) = strip_exists w 1116 val c = selfn b 1117 val cfvs = FVL [c] empty_tmset 1118 val constvars = HOLset.difference(cfvs, HOLset.fromList Term.compare vs) 1119 val ((tms0,tmfixed),_) = raw_match [] constvars c tm ([], []) 1120 val tms = 1121 tms0 @ HOLset.foldl 1122 (fn (v,acc) => 1123 if op_mem aconv v vs then {redex=v,residue=v}::acc 1124 else acc) 1125 [] tmfixed 1126 val xs = map #redex tms 1127 val ys = map #residue tms 1128 fun sorter ls = xs@(List.filter(not o Lib.C (op_mem aconv) xs)ls) 1129 in 1130 CONV_TAC(RESORT_EXISTS_CONV sorter) >> map_every exists_tac ys 1131 end g 1132 1133val provehyp = provehyp_then (K mp_tac) 1134val impl_tac = disch_then provehyp 1135val impl_keep_tac = 1136 disch_then (provehyp_then (fn lth => fn rth => assume_tac lth >> mp_tac rth)) 1137 1138 1139open mp_then 1140fun dGEN sel pos k = sel o mp_then pos k 1141val drule = dGEN first_assum (Pos hd) mp_tac 1142val rev_drule = dGEN last_assum (Pos hd) mp_tac 1143val dxrule = dGEN first_x_assum (Pos hd) mp_tac 1144val rev_dxrule = dGEN last_x_assum (Pos hd) mp_tac 1145 1146fun drule_then k = dGEN first_assum (Pos hd) k 1147fun dxrule_then k = dGEN first_x_assum (Pos hd) k 1148fun rev_drule_then k = dGEN last_assum (Pos hd) k 1149fun rev_dxrule_then k = dGEN last_x_assum (Pos hd) k 1150 1151fun drule_at p = dGEN first_assum p mp_tac 1152fun dxrule_at p = dGEN first_x_assum p mp_tac 1153fun rev_drule_at p = dGEN last_assum p mp_tac 1154fun rev_dxrule_at p = dGEN last_x_assum p mp_tac 1155 1156fun drule_at_then p k = dGEN first_assum p k 1157fun dxrule_at_then p k = dGEN first_x_assum p k 1158fun rev_drule_at_then p k = dGEN last_assum p k 1159fun rev_dxrule_at_then p k = dGEN last_x_assum p k 1160 1161fun isfa_imp th = th |> concl |> strip_forall |> #2 |> is_imp 1162fun dall_prim k fa ith0 g = 1163 REPEAT_GTCL (fn ttcl => fn th => fa (mp_then (Pos hd) ttcl th)) 1164 (k o assert (not o isfa_imp)) 1165 (assert isfa_imp ith0) 1166 g 1167val drule_all = dall_prim mp_tac first_assum 1168val dxrule_all = dall_prim mp_tac first_x_assum 1169fun drule_all_then k = dall_prim k first_assum 1170fun dxrule_all_then k = dall_prim k first_x_assum 1171 1172val rev_drule_all = dall_prim mp_tac last_assum 1173val rev_dxrule_all = dall_prim mp_tac last_x_assum 1174fun rev_drule_all_then k = dall_prim k last_assum 1175fun rev_dxrule_all_then k = dall_prim k last_x_assum 1176 1177open resolve_then 1178 1179end (* structure Tactic *) 1180