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