1(* ===================================================================== *) 2(* FILE : Tactical.sml *) 3(* DESCRIPTION : Functions that glue tactics together. From LCF, and *) 4(* added to through the years. Translated from hol88. *) 5(* *) 6(* AUTHORS : (c) University of Edinburgh and *) 7(* University of Cambridge, for hol88 *) 8(* TRANSLATOR : Konrad Slind, University of Calgary *) 9(* DATE : September 11, 1991 *) 10(* Updated : 1997 (to treat validity checking as an oracle) (KLS) *) 11(* ===================================================================== *) 12 13structure Tactical :> Tactical = 14struct 15 16open Feedback HolKernel Drule Conv boolSyntax Abbrev 17 18val ERR = mk_HOL_ERR "Tactical" 19 20fun empty th [] = th 21 | empty th _ = raise ERR "empty" "Bind Error" 22 23(*--------------------------------------------------------------------------- 24 * tac1 THEN_LT ltac2: 25 * A tactical that applies ltac2 to the list of subgoals resulting from tac1 26 * tac1 may be a tactic or a list_tactic 27 *---------------------------------------------------------------------------*) 28fun op THEN_LT (tac1, ltac2 : list_tactic) = 29 fn g => 30 let 31 val (gl1, vf1) = tac1 g 32 val (gl2, vf2) = ltac2 gl1 ; 33 in 34 (gl2, vf1 o vf2) 35 end 36 37val op >>> = op THEN_LT 38 39(* first argument can be a tactic or a list-tactic *) 40val _ = op THEN_LT : tactic * list_tactic -> tactic ; 41val _ = op THEN_LT : list_tactic * list_tactic -> list_tactic ; 42 43(*--------------------------------------------------------------------------- 44 * fun ALLGOALS (tac2:tactic) : list_tactic = fn gl => 45 * let 46 * val (gll,pl) = unzip(map tac2 gl) 47 * in 48 * (flatten gll, mapshape(map length gll)pl) 49 * end; 50 * A list_tactic which applies a given tactic to all goals 51 *---------------------------------------------------------------------------*) 52 53fun ALLGOALS tac2 gl = 54 case itlist 55 (fn goal => fn (G, V, lengths) => 56 case tac2 goal of 57 ([], vfun) => let 58 val th = vfun [] 59 in 60 (G, empty th :: V, 0 :: lengths) 61 end 62 | (goals, vfun) => 63 (goals @ G, vfun :: V, length goals :: lengths)) 64 gl ([], [], []) of 65 ([], V, _) => 66 ([], let val ths = map (fn f => f []) V in empty ths end) 67 | (G, V, lengths) => (G, mapshape lengths V) 68 69(*--------------------------------------------------------------------------- 70 * fun (tac1:tactic) THEN (tac2:tactic) : tactic = fn g => 71 * let val (gl,p) = tac1 g 72 * val (gll,pl) = unzip(map tac2 gl) 73 * in 74 * (flatten gll, (p o mapshape(map length gll)pl)) 75 * end; 76 *---------------------------------------------------------------------------*) 77 78fun tac1 THEN tac2 = tac1 THEN_LT ALLGOALS tac2 ; 79val op >> = op THEN 80val op \\ = op THEN 81 82(* first argument can be a tactic or a list-tactic *) 83val _ = op THEN : tactic * tactic -> tactic ; 84val _ = op THEN : list_tactic * tactic -> list_tactic ; 85 86(*--------------------------------------------------------------------------- 87 * fun TACS_TO_LT (tac2l: tactic list) : list_tactic = fn gl => 88 * let 89 * val tac2gl = zip tac2l gl 90 * val (gll,pl) = unzip (map (fn (tac2,g) => tac2 g) tac2gl) 91 * in 92 * (flatten gll, mapshape(map length gll) pl) 93 * end 94 * Converts a list of tactics to a single list_tactic 95 *---------------------------------------------------------------------------*) 96 97fun TACS_TO_LT (tacl: tactic list) : list_tactic = 98 fn gl => 99 let 100 val (G, V, lengths) = 101 itlist2 102 (fn goal => fn tac => fn (G, V, lengths) => 103 case tac goal of 104 ([], vfun) => let 105 val th = vfun [] 106 in 107 (G, (empty th) :: V, 0 :: lengths) 108 end 109 | (goals, vfun) => 110 (goals @ G, vfun :: V, length goals :: lengths)) 111 gl tacl ([], [], []) 112 in 113 case G of 114 [] => ([], let val ths = map (fn f => f []) V in empty ths end) 115 | _ => (G, mapshape lengths V) 116 end 117 118(*--------------------------------------------------------------------------- 119 * NULL_OK_LT ltac: A list-tactical like ltac but succeeds with no effect 120 * when applied to an empty goal list 121 *---------------------------------------------------------------------------*) 122 123fun NULL_OK_LT ltac [] = ([], Lib.I) 124 | NULL_OK_LT ltac gl = ltac gl ; 125 126(*--------------------------------------------------------------------------- 127 * fun (tac1:tactic) THENL (tac2l: tactic list) : tactic = fn g => 128 * let val (gl,p) = tac1 g 129 * val tac2gl = zip tac2l gl 130 * val (gll,pl) = unzip (map (fn (tac2,g) => tac2 g) tac2gl) 131 * in 132 * (flatten gll, p o mapshape(map length gll) pl) 133 * end 134 * BUT - if gl is empty, just return (gl, p) 135 *---------------------------------------------------------------------------*) 136 137fun tac1 THENL tacs2 = tac1 THEN_LT NULL_OK_LT (TACS_TO_LT tacs2) ; 138val op >| = op THENL 139 140(* first argument can be a tactic or a list-tactic *) 141val _ = op THENL : tactic * tactic list -> tactic ; 142val _ = op THENL : list_tactic * tactic list -> list_tactic ; 143 144fun (tac1 ORELSE tac2) g = tac1 g handle HOL_ERR _ => tac2 g 145fun (ltac1 ORELSE_LT ltac2) gl = ltac1 gl handle HOL_ERR _ => ltac2 gl 146 147(*--------------------------------------------------------------------------- 148 * tac1 THEN1 tac2: A tactical like THEN that applies tac2 only to the 149 * first subgoal of tac1 150 *---------------------------------------------------------------------------*) 151 152fun op THEN1 (tac1: tactic, tac2: tactic) : tactic = 153 fn g => 154 let 155 val (gl, jf) = tac1 g 156 val (h_g, t_gl) = 157 case gl of 158 [] => raise ERR "THEN1" "goal completely solved by first tactic" 159 | h :: t => (h, t) 160 val (h_gl, h_jf) = tac2 h_g 161 val _ = 162 if null h_gl then () 163 else raise ERR "THEN1" "first subgoal not solved by second tactic" 164 in 165 (t_gl, fn thl => jf (h_jf [] :: thl)) 166 end 167 168val op >- = op THEN1 169fun op>>-(tac1, n) tac2 g = 170 op>- (tac1, tac2) g 171 handle e as HOL_ERR {message,origin_structure,origin_function} => 172 raise HOL_ERR {message = message ^ " (THEN1 on line "^Int.toString n^")", 173 origin_function = origin_function, 174 origin_structure = origin_structure} 175fun (f ?? x) = f x 176 177 178(*--------------------------------------------------------------------------- 179 * NTH_GOAL tac n: A list_tactic that applies tac to the nth goal 180 (counting goals from 1) 181 *---------------------------------------------------------------------------*) 182fun NTH_GOAL tac n gl1 = 183 let 184 val (gl_before, ggl_after) = Lib.split_after (n-1) gl1 185 handle _ => raise ERR "NTH_GOAL" "no nth subgoal in list" ; 186 val (g, gl_after) = valOf (List.getItem ggl_after) 187 handle _ => raise ERR "NTH_GOAL" "no nth subgoal in list" ; 188 val (gl2, vf2) = tac g ; 189 val gl_result = gl_before @ gl2 @ gl_after ; 190 fun vf thl = 191 let val (th_before, th_rest) = Lib.split_after (n-1) thl ; 192 val (th2, th_after) = Lib.split_after (length gl2) th_rest ; 193 val th_result = th_before @ vf2 th2 :: th_after ; 194 in th_result end ; 195 in (gl_result, vf) end ; 196 197fun LASTGOAL tac gl1 = NTH_GOAL tac (length gl1) gl1 ; 198fun HEADGOAL tac gl1 = NTH_GOAL tac 1 gl1 ; 199 200(*--------------------------------------------------------------------------- 201 * SPLIT_LT n (ltaca, ltacb) : A list_tactic that applies ltaca to the 202 first n goals, and ltacb to the rest 203 *---------------------------------------------------------------------------*) 204fun SPLIT_LT n (ltaca, ltacb) gl = 205 let val fixn = if n >= 0 then n else length gl + n ; 206 val (gla, glb) = Lib.split_after fixn gl ; 207 val (glra, vfa) = ltaca gla ; 208 val (glrb, vfb) = ltacb glb ; 209 fun vf ths = 210 let val (thsa, thsb) = Lib.split_after (length glra) ths ; 211 in vfa thsa @ vfb thsb end ; 212 in (glra @ glrb, vf) end ; 213 214(*--------------------------------------------------------------------------- 215 * ROTATE_LT n : 216 * A list_tactic that moves the first n goals to the end of the goal list 217 * first n goals 218 *---------------------------------------------------------------------------*) 219fun ROTATE_LT n [] = ([], Lib.I) 220 | ROTATE_LT n gl = 221 let val lgl = length gl ; 222 val fixn = Int.mod (n, lgl) ; 223 val (gla, glb) = Lib.split_after fixn gl ; 224 fun vf ths = 225 let val (thsb, thsa) = Lib.split_after (lgl - fixn) ths ; 226 in thsa @ thsb end ; 227 in (glb @ gla, vf) end ; 228 229(*--------------------------------------------------------------------------- 230 * REVERSE tac: A tactical that reverses the list of subgoals of tac. 231 * Intended for use with THEN1 to pick the `easy' subgoal, e.g.: 232 * - CONJ_TAC THEN1 SIMP_TAC 233 * if the first conjunct is easily dispatched 234 * - REVERSE CONJ_TAC THEN1 SIMP_TAC 235 * if it is the second conjunct that yields. 236 *---------------------------------------------------------------------------*) 237 238fun REVERSE tac g = 239 let 240 val (gl, jf) = tac g 241 in 242 (rev gl, jf o rev) 243 end 244val reverse = REVERSE 245 246(*--------------------------------------------------------------------------- 247 * REVERSE_LT: A list_tactic that reverses a list of subgoals 248 *---------------------------------------------------------------------------*) 249 250fun REVERSE_LT gl = (rev gl, rev) ; 251 252(* for testing, redefine REVERSE 253fun REVERSE tac = tac THEN_LT REVERSE_LT ; 254*) 255 256(*--------------------------------------------------------------------------- 257 * Fail with the given token. Useful in tactic programs to check that a 258 * tactic produces no subgoals. Write 259 * 260 * TAC THEN FAIL_TAC "TAC did not solve the goal" 261 *---------------------------------------------------------------------------*) 262 263fun FAIL_TAC tok (g: goal) = raise ERR "FAIL_TAC" tok 264fun FAIL_LT tok (gl: goal list) = raise ERR "FAIL_LT" tok 265 266(*--------------------------------------------------------------------------- 267 * Tactic that succeeds on no goals; identity for ORELSE. 268 *---------------------------------------------------------------------------*) 269 270fun NO_TAC g = FAIL_TAC "NO_TAC" g 271fun NO_LT gl = FAIL_LT "NO_LT" gl 272 273(* for testing, redefine THEN1 274fun tac1 THEN1 tac2 = tac1 THEN_LT NTH_GOAL (tac2 THEN NO_TAC) 1 ; 275fun tac1 THEN1 tac2 = tac1 THEN_LT REVERSE_LT THEN_LT 276 LASTGOAL (tac2 THEN NO_TAC) THEN_LT REVERSE_LT ; 277*) 278 279(*--------------------------------------------------------------------------- 280 * Tactic that succeeds on all goals; identity for THEN 281 *---------------------------------------------------------------------------*) 282 283val ALL_TAC: tactic = fn (g: goal) => ([g], hd) 284val ALL_LT: list_tactic = fn (gl: goal list) => (gl, Lib.I) 285val all_tac = ALL_TAC 286 287fun TRY tac = tac ORELSE ALL_TAC 288fun TRY_LT ltac = ltac ORELSE_LT ALL_LT 289fun TRYALL tac = ALLGOALS (TRY tac) ; 290 291(*--------------------------------------------------------------------------- 292 * The abstraction around g is essential to avoid looping, due to applicative 293 * order semantics. 294 *---------------------------------------------------------------------------*) 295 296fun REPEAT tac g = ((tac THEN REPEAT tac) ORELSE ALL_TAC) g 297fun REPEAT_LT ltac gl = ((ltac THEN_LT REPEAT_LT ltac) ORELSE_LT ALL_LT) gl 298val rpt = REPEAT 299 300(*--------------------------------------------------------------------------- 301 * Add extra subgoals, which may be needed to make a tactic valid; 302 * similar to VALIDATE, but you can control the order of the extra goals 303 *---------------------------------------------------------------------------*) 304fun ADD_SGS_TAC (tms : term list) (tac : tactic) (g as (asl, w) : goal) = 305 let val (glist, prf) = tac g ; 306 val extra_goals = map (fn tm => (asl, tm)) tms ; 307 val nextra = length extra_goals ; 308 (* new validation: apply the theorems proving the additional goals to 309 eliminate the extra hyps in the theorem proved by the given validation *) 310 fun eprf ethlist = 311 let val (extra_thms, thlist) = split_after nextra ethlist ; 312 in itlist PROVE_HYP extra_thms (prf thlist) end ; 313 in (extra_goals @ glist, eprf) end ; 314 315(*--------------------------------------------------------------------------- 316 * Tacticals to make any tactic or list_tactic valid. 317 * 318 * VALID tac 319 * 320 * is the same as "tac", except it will fail in the cases where "tac" 321 * returns an invalid proof. 322 * 323 * VALID_LT ltac 324 * 325 * is the same as "ltac", except it will fail in the cases where "ltac" 326 * returns an invalid proof. 327 *---------------------------------------------------------------------------*) 328 329local 330 val validity_tag = "ValidityCheck" 331 fun masquerade goal = Thm.mk_oracle_thm validity_tag goal 332 datatype validity_failure = Concl of term | Hyp of term 333 fun bad_prf th (asl, w) = 334 if concl th !~ w then SOME (Concl (concl th)) 335 else 336 case List.find (fn h => List.all (not o aconv h) asl) (hyp th) of 337 NONE => NONE 338 | SOME h => SOME (Hyp h) 339 fun error f t e = 340 let 341 val pfx = "Invalid " ^ t ^ ": theorem has " 342 val (desc, t) = 343 case e of 344 Hyp h => ("bad hypothesis", h) 345 | Concl c => ("wrong conclusion", c) 346 in 347 raise ERR f (pfx ^ desc ^ " " ^ Parse.term_to_string t) 348 end 349in 350 fun VALID (tac: tactic) : tactic = 351 fn g: goal => 352 let 353 val (result as (glist, prf)) = tac g 354 in 355 case bad_prf (prf (map masquerade glist)) g of 356 NONE => result 357 | SOME e => error "VALID" "tactic" e 358 end 359 360 fun VALID_LT (ltac: list_tactic) : list_tactic = 361 fn gl: goal list => 362 let 363 val (result as (glist, prf)) = ltac gl 364 val wrongnum_msg = "Invalid list-tactic: wrong number of results\ 365 \ from justification" 366 fun check ths gls = 367 case (ths, gls) of 368 ([], []) => result 369 | (_, []) => raise ERR "VALID_LT" wrongnum_msg 370 | ([], _) => raise ERR "VALID_LT" wrongnum_msg 371 | (th::ths0,gl::gls0) => 372 (case bad_prf th gl of 373 NONE => check ths0 gls0 374 | SOME e => error "VALID_LT" "list-tactic" e) 375 in 376 check (prf (map masquerade glist)) gl 377 end 378end 379 380(*--------------------------------------------------------------------------- 381 * Tacticals to include proofs of necessary hypotheses for an invalid 382 * tactic or list_tactic valid. 383 * 384 * VALIDATE tac 385 * GEN_VALIDATE true tac 386 * 387 * is the same as "tac", except that where "tac" returns a proof which is 388 * invalid because it proves a theorem with extra hypotheses, 389 * it returns those hypotheses as extra goals 390 * 391 * VALIDATE_LT ltac 392 * GEN_VALIDATE_LT true ltac 393 * 394 * is the same as "ltac", except it will return extra goals where this is 395 * necessary to make a valid list-tactic 396 * 397 * GEN_VALIDATE(_LT) false always returns extra goals corresponding 398 * to the hypotheses of the theorem proved 399 * 400 *---------------------------------------------------------------------------*) 401local val validity_tag = "ValidityCheck" 402 fun masquerade goal = Thm.mk_oracle_thm validity_tag goal ; 403 fun achieves_concl th (asl, w) = Term.aconv (concl th) w ; 404 fun hyps_not_in_goal th (asl, w) = 405 Lib.filter (fn h => not (Lib.exists (aconv h) asl)) (hyp th) ; 406 fun extra_goals_tbp flag th (asl, w) = 407 List.map (fn eg => (asl, eg)) 408 (case flag of true => hyps_not_in_goal th (asl, w) 409 | false => hyp th) ; 410in 411(* GEN_VALIDATE : bool -> tactic -> tactic *) 412fun GEN_VALIDATE (flag : bool) (tac : tactic) (g as (asl, w) : goal) = 413 let val (glist, prf) = tac g ; 414 (* pretend new goals are theorems, and apply validation to them *) 415 val thprf = (prf (map masquerade glist)) ; 416 val _ = if achieves_concl thprf g then () 417 else raise ERR "GEN_VALIDATE" "Invalid tactic - wrong conclusion" ; 418 val extra_goals = extra_goals_tbp flag thprf g ; 419 val nextra = length extra_goals ; 420 (* new validation: apply the theorems proving the additional goals to 421 eliminate the extra hyps in the theorem proved by the given validation *) 422 fun eprf ethlist = 423 let val (extra_thms, thlist) = split_after nextra ethlist ; 424 in itlist PROVE_HYP extra_thms (prf thlist) end ; 425 in (extra_goals @ glist, eprf) end ; 426 427(* split_lists : int list -> 'a list -> 'a list list * 'a list *) 428fun split_lists (n :: ns) ths = 429 let val (nths, rest) = split_after n ths ; 430 val (nsths, left) = split_lists ns rest ; 431 in (nths :: nsths, left) end 432 | split_lists [] ths = ([], ths) ; 433 434(* GEN_VALIDATE_LT : bool -> list_tactic -> list_tactic *) 435fun GEN_VALIDATE_LT (flag : bool) (ltac : list_tactic) (gl : goal list) = 436 let val (glist, prf) = ltac gl ; 437 (* pretend new goals are theorems, and apply validation to them *) 438 val thsprf = (prf (map masquerade glist)) ; 439 val _ = if Lib.all2 achieves_concl thsprf gl then () 440 else raise ERR "GEN_VALIDATE_LT" 441 "Invalid list-tactic - some wrong conclusion" ; 442 val extra_goal_lists = Lib.map2 (extra_goals_tbp flag) thsprf gl ; 443 val nextras = map length extra_goal_lists ; 444 (* new validation: apply the theorems proving the additional goals to 445 eliminate the extra hyps in the theorems proved by the given validation *) 446 fun eprf ethlist = 447 let val (extra_thm_lists, thlist) = split_lists nextras ethlist ; 448 in Lib.map2 (itlist PROVE_HYP) extra_thm_lists (prf thlist) end ; 449 in (List.concat extra_goal_lists @ glist, eprf) end ; 450 451end; 452 453val VALIDATE = GEN_VALIDATE true ; 454val VALIDATE_LT = GEN_VALIDATE_LT true ; 455 456(* could avoid duplication of code in the above by the following 457fun GEN_VALIDATE flag tac = 458 ALL_TAC THEN_LT GEN_VALIDATE_LT flag (TACS_TO_LT [tac]) ; 459*) 460 461(*--------------------------------------------------------------------------- 462 * Provide a function (tactic) with the current assumption list. 463 *---------------------------------------------------------------------------*) 464 465fun ASSUM_LIST aslfun (g as (asl, _)) = aslfun (map ASSUME asl) g 466 467(*--------------------------------------------------------------------------- 468 * Pop the first assumption and give it to a function (tactic) 469 *---------------------------------------------------------------------------*) 470 471fun POP_ASSUM thfun (a :: asl, w) = thfun (ASSUME a) (asl, w) 472 | POP_ASSUM _ ([], _) = raise ERR "POP_ASSUM" "no assum" 473val pop_assum = POP_ASSUM 474 475(*--------------------------------------------------------------------------- 476 * Pop off the entire assumption list and give it to a function (tactic) 477 *---------------------------------------------------------------------------*) 478 479fun POP_ASSUM_LIST asltac (asl, w) = asltac (map ASSUME asl) ([], w) 480 481(*--------------------------------------------------------------------------- 482 * Pop the first assumption satisying the given predictae and give it to 483 * a function (tactic). 484 *---------------------------------------------------------------------------*) 485 486fun PRED_ASSUM pred thfun (asl, w) = 487 case Lib.total (Lib.pluck pred) asl of 488 SOME (ob, asl') => thfun (ASSUME ob) (asl', w) 489 | NONE => raise ERR "PRED_ASSUM" "No suitable assumption found." 490 491 492(*-- Tactical quantifiers -- Apply a list of tactics in succession. -------*) 493 494(*--------------------------------------------------------------------------- 495 * Uses every tactic (similarly EVERY_LT for list_tactics) 496 * EVERY [TAC1;...;TACn] = TAC1 THEN ... THEN TACn 497 *---------------------------------------------------------------------------*) 498 499fun EVERY tacl = List.foldr (op THEN) ALL_TAC tacl 500fun EVERY_LT ltacl = List.foldr (op THEN_LT) ALL_LT ltacl 501 502(*--------------------------------------------------------------------------- 503 * Uses first tactic that succeeds. 504 * FIRST [TAC1;...;TACn] = TAC1 ORELSE ... ORELSE TACn 505 *---------------------------------------------------------------------------*) 506 507fun FIRST [] g = NO_TAC g 508 | FIRST (tac :: rst) g = tac g handle HOL_ERR _ => FIRST rst g 509 510fun MAP_EVERY tacf lst = EVERY (map tacf lst) 511val map_every = MAP_EVERY 512fun MAP_FIRST tacf lst = FIRST (map tacf lst) 513 514(*--------------------------------------------------------------------------- 515 * Uses first tactic that proves the goal. 516 * FIRST_PROVE [TAC1;...;TACn] = 517 * (TAC1 THEN NO_TAC) ORELSE ... ORELSE (TACn THEN NO_TAC) 518 * Fails if no tactic proves the goal. 519 *---------------------------------------------------------------------------*) 520 521fun FIRST_PROVE tacl = 522 itlist (fn a => fn b => (a THEN NO_TAC) ORELSE b) tacl NO_TAC 523 524(*--------------------------------------------------------------------------- 525 * Call a thm-tactic for every assumption. 526 *---------------------------------------------------------------------------*) 527 528val EVERY_ASSUM = ASSUM_LIST o MAP_EVERY 529 530(*--------------------------------------------------------------------------- 531 * Call a thm-tactic for the first assumption at which it succeeds. 532 *---------------------------------------------------------------------------*) 533 534val shut_parser_up = 535 trace ("notify type variable guesses", 0) o 536 trace ("syntax_error", 0) o 537 trace ("show_typecheck_errors", 0) 538 539local 540 fun find ttac name goal [] = raise ERR name "" 541 | find ttac name goal (a :: L) = 542 ttac (ASSUME a) goal handle HOL_ERR _ => find ttac name goal L 543in 544 fun FIRST_ASSUM ttac (A, g) = 545 shut_parser_up (find ttac "FIRST_ASSUM" (A, g)) A 546 fun LAST_ASSUM ttac (A, g) = 547 shut_parser_up (find ttac "LAST_ASSUM" (A, g)) (List.rev A) 548 val first_assum = FIRST_ASSUM 549 val last_assum = LAST_ASSUM 550end 551 552 553(*--------------------------------------------------------------------------- 554 * Call a thm-tactic for the first assumption at which it succeeds and 555 * remove that assumption from the list. 556 * Note that UNDISCH_THEN is actually defined for public consumption 557 * in Thm_cont.sml, but we can't use that here because Thm_cont builds 558 * on this module. Arguably all of the ASSUM tactics are not tacticals 559 * at all, and shouldn't be here along with THEN etc. 560 *---------------------------------------------------------------------------*) 561 562local 563 fun UNDISCH_THEN tm ttac (asl, w) = 564 let val (_, A) = Lib.pluck (equal tm) asl in ttac (ASSUME tm) (A, w) end 565 fun f ttac th = UNDISCH_THEN (concl th) ttac 566in 567 val FIRST_X_ASSUM = FIRST_ASSUM o f 568 val LAST_X_ASSUM = LAST_ASSUM o f 569 val first_x_assum = FIRST_X_ASSUM 570 val last_x_assum = LAST_X_ASSUM 571end 572 573(*--------------------------------------------------------------------------- 574 * Pop the first assumption matching (higher-order match) the given term 575 * and give it to a function (tactic). 576 *---------------------------------------------------------------------------*) 577 578local 579 fun can_match_with_constants constants pat ob = 580 let 581 val (tm_inst, _) = ho_match_term [] empty_tmset pat ob 582 val bound_vars = map #redex tm_inst 583 in 584 null (intersect constants bound_vars) 585 end handle HOL_ERR _ => false 586 587 (* you might think that one could simply pass the free variable set 588 to ho_match_term, and do without this bogus looking 589 can_match_with_constants function. Unfortunately, this doesn't 590 quite work because the match is higher-order, meaning that a 591 pattern like ``_ x``, where x is a "constant" will match something 592 like ``f y``, where y is of the right type, but manifestly not x. 593 This is because 594 595 ho_match_term [] (some set including x) ``_ x`` ``f y`` 596 597 will return an instantiation where _ maps to (\x. y). This 598 respects the request not to bind x, but the intention is bypassed. 599 *) 600 601 fun gen tcl pat thfun (g as (asl,w)) = 602 let 603 val fvs = free_varsl (w::asl) 604 in 605 tcl (thfun o assert (can_match_with_constants fvs pat o concl)) 606 end g 607in 608 val PAT_X_ASSUM = gen FIRST_X_ASSUM 609 val PAT_ASSUM = gen FIRST_ASSUM 610end 611 612 613local 614fun hdsym t = (t |> lhs |> strip_comb |> #1) 615 handle HOL_ERR _ => t |> strip_comb |> #1 616fun hdsym_check tm ttac = ttac o assert (same_const tm o hdsym o concl) 617in 618fun hdtm_assum tm ttac = first_assum (hdsym_check tm ttac) 619fun hdtm_x_assum tm ttac = first_x_assum (hdsym_check tm ttac) 620end 621 622fun sing f [x] = f x 623 | sing f _ = raise ERR "sing" "Bind Error" 624 625fun CONV_TAC (conv: conv) : tactic = 626 fn (asl, w) => 627 let 628 val th = conv w 629 val (_, rhs) = dest_eq (concl th) 630 in 631 if rhs = T 632 then ([], empty (EQ_MP (SYM th) boolTheory.TRUTH)) 633 else ([(asl, rhs)], sing (EQ_MP (SYM th))) 634 end 635 handle UNCHANGED => 636 if w = T (* special case, can happen! *) 637 then ([], empty boolTheory.TRUTH) 638 else ALL_TAC (asl, w) 639 640(*--------------------------------------------------------------------------- 641 * Call a thm-tactic on the "assumption" obtained by negating the goal, i.e., 642 turn an existential goal into a universal assumption. Fix up the resulting 643 new goal if necessary. 644 *---------------------------------------------------------------------------*) 645 646local 647 fun DISCH_THEN ttac (asl,w) = 648 let 649 val (ant, conseq) = dest_imp w 650 val (gl, prf) = ttac (ASSUME ant) (asl, conseq) 651 in 652 (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf) 653 end 654 handle HOL_ERR _ => raise ERR "DISCH_THEN" "" 655 val NOT_NOT_E = boolTheory.NOT_CLAUSES |> CONJUNCT1 656 val NOT_NOT_I = NOT_NOT_E |> GSYM 657 val NOT_IMP_F = IMP_ANTISYM_RULE (SPEC_ALL boolTheory.F_IMP) 658 (SPEC_ALL boolTheory.IMP_F) 659 val IMP_F_NOT = NOT_IMP_F |> GSYM 660 val P_IMP_P = boolTheory.IMP_CLAUSES |> SPEC_ALL |> CONJUNCTS |> el 4 661 val NOT_IMP_F_elim = 662 TRANS (AP_TERM boolSyntax.negation (SYM NOT_IMP_F)) 663 (boolTheory.NOT_CLAUSES |> CONJUNCT1 |> SPEC_ALL) 664 fun EX_IMP_F_CONV tm = 665 (IFC NOT_EXISTS_CONV (BINDER_CONV EX_IMP_F_CONV) (REWR_CONV NOT_IMP_F)) tm 666 fun undo_conv tm = 667 (IFC NOT_FORALL_CONV 668 (BINDER_CONV undo_conv) 669 (REWR_CONV NOT_IMP_F_elim ORELSEC TRY_CONV (REWR_CONV NOT_NOT_E))) tm 670in 671 fun goal_assum ttac : tactic = 672 CONV_TAC (REWR_CONV NOT_NOT_I THENC RAND_CONV EX_IMP_F_CONV) THEN 673 DISCH_THEN ttac THEN 674 (CONV_TAC (REWR_CONV P_IMP_P) ORELSE 675 TRY (CONV_TAC (REWR_CONV IMP_F_NOT THENC undo_conv))) 676end 677 678(*--------------------------------------------------------------------------- 679 * Split off a new subgoal and provide it as a theorem to a tactic 680 * 681 * SUBGOAL_THEN wa (\tha. tac) 682 * 683 * makes a subgoal of wa, and also assumes wa for proving the original goal. 684 * Most convenient when the tactic solves the original goal, leaving only the 685 * new subgoal wa. 686 *---------------------------------------------------------------------------*) 687 688fun SUBGOAL_THEN wa ttac (asl, w) = 689 let 690 val (gl, p) = ttac (ASSUME wa) (asl, w) 691 in 692 ((asl, wa) :: gl, 693 (fn (tha :: thl) => PROVE_HYP tha (p thl) | _ => raise Match)) 694 end 695 696(*--------------------------------------------------------------------------- 697 * Use another subgoal, providing it as a theorem to a tactic 698 * 699 * USE_SG_THEN ttac nu np 700 * 701 * assumes subgoal number nu for proving subgoal number np 702 *---------------------------------------------------------------------------*) 703 704(* USE_SG_VAL : int -> int -> list_validation *) 705fun USE_SG_VAL nu np thl = 706 let val thu = List.nth (thl, nu - 1) ; 707 in apnth (PROVE_HYP thu) (np - 1) thl end ; 708 709(* USE_SG_THEN : thm_tactic -> int -> int -> list_tactic *) 710fun USE_SG_THEN ttac nu np gl = 711 let 712 val (_, wu) = List.nth (gl, nu - 1) ; 713 val ltac = NTH_GOAL (ttac (ASSUME wu)) np ; 714 val (glr, v) = ltac gl ; 715 val vp = USE_SG_VAL nu np ; 716 in (glr, vp o v) end ; 717 718(* USE_SG_TAC : int -> int -> list_tactic 719val USE_SG_TAC = USE_SG_THEN ASSUME_TAC ; 720*) 721 722(*--------------------------------------------------------------------------- 723 * A tactical that makes a tactic fail if it has no effect. 724 *---------------------------------------------------------------------------*) 725 726fun CHANGED_TAC tac g = 727 let 728 val (gl, p) = tac g 729 in 730 if set_eq gl [g] then raise ERR "CHANGED_TAC" "no change" else (gl, p) 731 end 732 733(*--------------------------------------------------------------------------- 734 * A tactical that parses in the context of a goal, a la the Q library. 735 *---------------------------------------------------------------------------*) 736 737fun parse_with_goal t (asms, g) = 738 let 739 val ctxt = free_varsl (g :: asms) 740 in 741 Parse.parse_in_context ctxt t 742 end 743 744fun Q_TAC0 {traces} tyopt (tac : term -> tactic) q (g as (asl,w)) = 745 let 746 open Parse 747 val ctxt = free_varsl (w::asl) 748 val ab = 749 case tyopt of 750 NONE => Absyn 751 | SOME ty => 752 fn q => Absyn.TYPED(locn.Loc_None, Absyn q, Pretype.fromType ty) 753 val s = TermParse.prim_ctxt_termS ab (term_grammar()) ctxt q 754 fun cases s = List.foldl 755 (fn (trpair,f) => Feedback.trace trpair f) 756 seq.cases 757 traces 758 s 759 in 760 case cases s of 761 NONE => raise ERR "Q_TAC" "No parse for quotation" 762 | SOME _ => 763 (case cases (seq.mapPartial (fn t => total (tac t) g) s) of 764 NONE => raise ERR "Q_TAC" "No parse of quotation leads to success" 765 | SOME (res,_) => res) 766 end 767 768val Q_TAC = Q_TAC0 {traces = []} NONE 769fun QTY_TAC ty = Q_TAC0 {traces = []} (SOME ty) 770 771(*--------------------------------------------------------------------------- 772 * TAC_PROOF (g,tac) uses tac to prove the goal g. An alpha conversion 773 * step needs to be done if the proof returns a theorem that is 774 * alpha-equivalent but not equal to the goal. To be really precise, 775 * we should do this check in the hypotheses of the goal as well. 776 *---------------------------------------------------------------------------*) 777 778local 779 val unsolved_list = ref ([]: goal list) 780in 781 fun unsolved () = !unsolved_list 782 fun TAC_PROOF (g, tac) = 783 case tac g of 784 ([], p) => 785 (let 786 val thm = p [] 787 val c = concl thm 788 val () = unsolved_list := [] 789 in 790 if c = snd g then thm else EQ_MP (ALPHA c (snd g)) thm 791 end 792 handle e => raise ERR "TAC_PROOF" "Can't alpha convert") 793 | (l, _) => (unsolved_list := l; raise ERR "TAC_PROOF" "unsolved goals") 794end 795 796fun default_prover (t, tac) = TAC_PROOF (([], t), VALID tac) 797 798local 799 val mesg = Lib.with_flag (Feedback.MESG_to_string, Lib.I) Feedback.HOL_MESG 800 fun provide_feedback f (t, tac: tactic) = 801 f (t, tac) 802 handle (e as HOL_ERR {message = m, origin_function = f, ...}) => 803 (mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n") 804 ; (case (m, f, unsolved ()) of 805 ("unsolved goals", "TAC_PROOF", (_, u)::_) => 806 if Term.term_eq u t 807 then () 808 else mesg ("First unsolved sub-goal is\n\n" ^ 809 Parse.term_to_string u ^ "\n\n") 810 | _ => ()) 811 ; raise e) 812 val internal_prover = 813 ref (provide_feedback default_prover: Term.term * tactic -> Thm.thm) 814in 815 fun set_prover f = internal_prover := provide_feedback f 816 fun restore_prover () = set_prover default_prover 817 fun prove (t, tac) = !internal_prover (t, tac) 818end 819 820fun store_thm (name, tm, tac) = 821 Theory.save_thm (name, prove (tm, tac)) 822 handle e => 823 (print ("Failed to prove theorem " ^ name ^ ".\n"); 824 Raise e) 825 826end (* Tactical *) 827