1(* ===================================================================== *) 2(* FILE : Thm_cont.sml *) 3(* DESCRIPTION : Larry Paulson's theorem continuations for HOL. *) 4(* Translated from hol88. *) 5(* *) 6(* "Theorem continuations" *) 7(* *) 8(* Many inference rules, particularly those involving disjunction and *) 9(* existential quantifiers, produce intermediate results that are needed *) 10(* only briefly. One approach is to treat the assumption list like a *) 11(* stack, pushing and popping theorems from it. However, it is *) 12(* traditional to regard the assumptions as unordered; also, stack *) 13(* operations are crude. *) 14(* *) 15(* Instead, we adopt a continuation approach: a continuation is a *) 16(* function that maps theorems to tactics. It can put the theorem on *) 17(* the assumption list, produce a case split, throw it away, etc. The *) 18(* text of a large theorem continuation should be a readable description *) 19(* of the flow of inference. *) 20(* *) 21(* AUTHORS : (c) Larry Paulson and others, *) 22(* University of Cambridge, for hol88 *) 23(* TRANSLATOR : Konrad Slind, University of Calgary *) 24(* DATE : September 11, 1991 *) 25(* ===================================================================== *) 26 27structure Thm_cont :> Thm_cont = 28struct 29 30open Feedback HolKernel Drule boolSyntax Abbrev Conv; 31 32val ERR = mk_HOL_ERR "Thm_cont" 33 34fun (ttcl1: thm_tactical) THEN_TCL (ttcl2: thm_tactical) = 35 fn ttac => ttcl1 (ttcl2 ttac) 36 37fun (ttcl1: thm_tactical) ORELSE_TCL (ttcl2: thm_tactical) = 38 fn ttac => fn th => ttcl1 ttac th handle HOL_ERR _ => ttcl2 ttac th 39 40fun REPEAT_TCL ttcl ttac th = 41 ((ttcl THEN_TCL (REPEAT_TCL ttcl)) ORELSE_TCL I) ttac th 42 43(* --------------------------------------------------------------------- *) 44(* New version of REPEAT for ttcl's. Designed for use with IMP_RES_THEN.*) 45(* TFM 91.01.20. *) 46(* --------------------------------------------------------------------- *) 47 48fun REPEAT_GTCL (ttcl: thm_tactical) ttac th (A,g) = 49 ttcl (REPEAT_GTCL ttcl ttac) th (A,g) 50 handle HOL_ERR _ => ttac th (A,g) 51 52val ALL_THEN: thm_tactical = I 53val NO_THEN: thm_tactical = fn ttac => fn th => raise ERR "NO_THEN" "" 54 55(*--------------------------------------------------------------------------- 56 * Uses every theorem tactical. 57 * 58 * EVERY_TCL [ttcl1;...;ttcln] = ttcl1 THEN_TCL ... THEN_TCL ttcln 59 *---------------------------------------------------------------------------*) 60 61val EVERY_TCL = List.foldr (op THEN_TCL) ALL_THEN 62 63(*--------------------------------------------------------------------------- 64 * Uses first successful theorem tactical. 65 * 66 * FIRST_TCL [ttcl1;...;ttcln] = ttcl1 ORELSE_TCL ... ORELSE_TCL ttcln 67 *---------------------------------------------------------------------------*) 68 69val FIRST_TCL = List.foldr (op ORELSE_TCL) NO_THEN 70 71(*--------------------------------------------------------------------------- 72 * Conjunction elimination 73 * 74 * C 75 * ============== |- A1 /\ A2 76 * C 77 * ===== ttac1 |-A1 78 * ... 79 * ===== ttac2 |-A2 80 * ... 81 *---------------------------------------------------------------------------*) 82 83fun CONJUNCTS_THEN2 ttac1 ttac2 = 84 fn cth => 85 let 86 val (th1,th2) = CONJ_PAIR cth 87 in 88 Tactical.THEN (ttac1 th1, ttac2 th2) 89 end 90 handle HOL_ERR _ => raise ERR "CONJUNCTS_THEN2" "" 91 92val CONJUNCTS_THEN: thm_tactical = fn ttac => CONJUNCTS_THEN2 ttac ttac 93 94(*--------------------------------------------------------------------------- 95 * Disjunction elimination 96 * 97 * C 98 * ============================= |- A1 \/ A2 99 * C C 100 * ===== ttac1 A1|-A1 ===== ttac2 A2|-A2 101 * ... ... 102 *---------------------------------------------------------------------------*) 103 104(* -------------------------------------------------------------------------*) 105(* REVISED 22 Oct 1992 by TFM. Bugfix. *) 106(* *) 107(* The problem was, for example: *) 108(* *) 109(* th = |- ?n. ((?n. n = SUC 0) \/ F) /\ (n = 0) *) 110(* set_goal ([], "F");; *) 111(* expandf (STRIP_ASSUME_TAC th);; *) 112(* OK.. *) 113(* "F" *) 114(* [ "n = SUC 0" ] (n.b. should be n') *) 115(* [ "n = 0" ] *) 116(* *) 117(* let DISJ_CASES_THEN2 ttac1 ttac2 disth :tactic = *) 118(* let a1,a2 = dest_disj (concl disth) ? failwith `DISJ_CASES_THEN2` in *) 119(* \(asl,w). *) 120(* let gl1,prf1 = ttac1 (ASSUME a1) (asl,w) *) 121(* and gl2,prf2 = ttac2 (ASSUME a2) (asl,w) *) 122(* in *) 123(* gl1 @ gl2, *) 124(* \thl. let thl1,thl2 = chop_list (length gl1) thl in *) 125(* DISJ_CASES disth (prf1 thl1) (prf2 thl2);; *) 126(* -------------------------------------------------------------------------*) 127 128(*--------------------------------------------------------------------------- 129 foo needs to return a theorem with M as conclusion, and M as one 130 of the assumptions, and all of the assumptions of th as well: 131 132 foo th M = mk_thm(M::Thm.hyp th, M) 133 ---------------------------------------------------------------------------*) 134 135fun foo th M = MP (DISCH (concl th) (ASSUME M)) th 136 137fun DISJ_CASES_THEN2 ttac1 ttac2 = 138 fn disth => 139 let 140 val (disj1, disj2) = dest_disj (Thm.concl disth) 141 in 142 fn g as (asl, w) => 143 let 144 val (gl1, prf1) = ttac1 (foo disth disj1) g 145(* ttac1 (itlist ADD_ASSUM (Thm.hyp disth) (ASSUME disj1)) g *) 146 and (gl2, prf2) = ttac2 (foo disth disj2) g 147(* ttac2 (itlist ADD_ASSUM (Thm.hyp disth) (ASSUME disj2)) g *) 148 in 149 (gl1 @ gl2, 150 fn thl => 151 let 152 val (thl1, thl2) = split_after (length gl1) thl 153 in 154 DISJ_CASES disth (prf1 thl1) (prf2 thl2) 155 end) 156 end 157 end 158 handle HOL_ERR _ => raise ERR "DISJ_CASES_THEN2" "" 159 160(*---------------------------------------------------------------------------* 161 * Single-, multi-tactic versions * 162 *---------------------------------------------------------------------------*) 163 164val DISJ_CASES_THEN: thm_tactical = fn ttac => DISJ_CASES_THEN2 ttac ttac 165 166val DISJ_CASES_THENL: thm_tactic list -> thm_tactic = 167 end_itlist DISJ_CASES_THEN2 168 169(*--------------------------------------------------------------------------- 170 * Implication introduction 171 * 172 * A ==> B 173 * ============== 174 * B 175 * ============== ttac |-A 176 * . . . 177 * 178 * DISCH changed to NEG_DISCH for HOL 179 * 180 * Deleted: TFM 88.03.31 181 * 182 * let DISCH_THEN ttac :tactic (asl,w) = 183 * let ante,conc = dest_imp w ? failwith `DISCH_THEN` in 184 * let gl,prf = ttac (ASSUME ante) (asl,conc) in 185 * gl, (NEG_DISCH ante) o prf;; 186 * Added: TFM 88.03.31 (bug fix) 187 *---------------------------------------------------------------------------*) 188 189fun DISCH_THEN ttac (asl,w) = 190 let 191 val (ant, conseq) = dest_imp w 192 val (gl, prf) = ttac (ASSUME ant) (asl, conseq) 193 in 194 (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf) 195 end 196 handle HOL_ERR _ => raise ERR "DISCH_THEN" "" 197val disch_then = DISCH_THEN 198 199(*---------------------------------------------------------------------------* 200 * DISCH_THEN's "dual" * 201 * * 202 * ported from John Harrison's HOL Light * 203 * -- Michael Norrish 30 June 1999 * 204 *---------------------------------------------------------------------------*) 205 206fun UNDISCH_THEN tm ttac (asl, w) = 207 let 208 val (_, asl') = 209 with_exn (Lib.pluck (aconv tm)) asl 210 (ERR "UNDISCH_THEN" "Term given not an assumption") 211 in 212 ttac (ASSUME tm) (asl', w) 213 end 214 215(*--------------------------------------------------------------------------- 216 * Existential elimination 217 * 218 * B 219 * ================== |- ?x. A(x) 220 * B 221 * ================== ttac A(y) 222 * ... 223 * explicit version for tactic programming 224 *---------------------------------------------------------------------------*) 225 226fun X_CHOOSE_THEN y (ttac: thm_tactic) : thm_tactic = 227 fn xth => 228 let 229 val (Bvar,Body) = dest_exists (Thm.concl xth) 230 in 231 fn (asl,w) => 232 let 233 val th = foo xth (subst[Bvar |-> y] Body) 234 (* itlist ADD_ASSUM (hyp xth) (ASSUME (subst[Bvar |-> y] Body)) *) 235 val (gl,prf) = ttac th (asl,w) 236 in 237 (gl, (CHOOSE (y,xth)) o prf) 238 end 239 end 240 handle HOL_ERR _ => raise ERR "X_CHOOSE_THEN" "" 241 242(*--------------------------------------------------------------------------- 243 * Chooses a variant for the user. 244 *---------------------------------------------------------------------------*) 245 246val CHOOSE_THEN: thm_tactical = 247 fn ttac => fn xth => 248 let 249 val (hyp,conc) = dest_thm xth 250 val (Bvar,_) = dest_exists conc 251 in 252 fn (asl,w) => 253 let 254 val y = gen_variant Parse.is_constname "" 255 (free_varsl ((conc::hyp)@(w::asl))) 256 Bvar 257 in 258 X_CHOOSE_THEN y ttac xth (asl,w) 259 end 260 end 261 handle HOL_ERR _ => raise ERR "CHOOSE_THEN" "" 262 263(*---------- Cases tactics -------------*) 264 265(*--------------------------------------------------------------------------- 266 * For a generalized disjunction |-(?xl1.B1(xl1)) \/...\/ (?xln.Bn(xln)) 267 * where the xl1...xln are vectors of zero or more variables, and the 268 * variables in each of yl1...yln have the same types as the 269 * corresponding xli do 270 * 271 * A 272 * ============================================= 273 * A A 274 * ======= ttac1 |-B1(yl1) ... ======= ttacn |-Bn(yln) 275 * ... ... 276 * 277 *---------------------------------------------------------------------------*) 278 279fun X_CASES_THENL varsl (ttacl: thm_tactic list) = 280 DISJ_CASES_THENL 281 (map (fn (vars,ttac) => EVERY_TCL (map X_CHOOSE_THEN vars) ttac) 282 (varsl zip ttacl)) 283 284fun X_CASES_THEN varsl ttac = 285 DISJ_CASES_THENL 286 (map (fn vars => EVERY_TCL (map X_CHOOSE_THEN vars) ttac) varsl) 287 288(*---------------------------------------------------------------------------* 289 * Version that chooses the y's as variants of the x's. * 290 *---------------------------------------------------------------------------*) 291 292fun CASES_THENL ttacl = DISJ_CASES_THENL (map (REPEAT_TCL CHOOSE_THEN) ttacl) 293 294(*---------------------------------------------------------------------------* 295 * Tactical to strip off ONE disjunction, conjunction, or existential. * 296 *---------------------------------------------------------------------------*) 297 298val STRIP_THM_THEN = FIRST_TCL [CONJUNCTS_THEN, DISJ_CASES_THEN, CHOOSE_THEN] 299 300 301(* ---------------------------------------------------------------------*) 302(* Resolve implicative assumptions with an antecedent *) 303(* ---------------------------------------------------------------------*) 304 305fun ANTE_RES_THEN ttac ante : tactic = 306 Tactical.ASSUM_LIST 307 (Tactical.EVERY o (mapfilter (fn imp => ttac (MATCH_MP imp ante)))) 308 309(* ---------------------------------------------------------------------*) 310(* Old versions of RESOLVE_THEN etc. [TFM 90.04.24] *) 311(* *) 312(* letrec RESOLVE_THEN antel ttac impth : tactic = *) 313(* let answers = mapfilter (MATCH_MP impth) antel in *) 314(* EVERY (mapfilter ttac answers) *) 315(* THEN *) 316(* (EVERY (mapfilter (RESOLVE_THEN antel ttac) answers)); *) 317(* *) 318(* let OLD_IMP_RES_THEN ttac impth = *) 319(* ASSUM_LIST *) 320(* (\asl. EVERY (mapfilter (RESOLVE_THEN asl ttac) *) 321(* (IMP_CANON impth))); *) 322(* *) 323(* let OLD_RES_THEN ttac = *) 324(* ASSUM_LIST (EVERY o (mapfilter (OLD_IMP_RES_THEN ttac))); *) 325(* ---------------------------------------------------------------------*) 326 327 328(* --------------------------------------------------------------------- *) 329(* Definitions of the primitive: *) 330(* *) 331(* IMP_RES_THEN: Resolve all assumptions against an implication. *) 332(* *) 333(* The definition uses two auxiliary (local) functions: *) 334(* *) 335(* MATCH_MP : like the built-in version, but doesn't use GSPEC. *) 336(* RESOLVE_THEN : repeatedly resolve an implication *) 337(* *) 338(* This version deleted for HOL version 1.12 [TFM 91.01.17] *) 339(* *) 340(* begin_section IMP_RES_THEN; *) 341(* *) 342(* let MATCH_MP impth = *) 343(* let sth = SPEC_ALL impth in *) 344(* let pat = fst(dest_imp(concl sth)) in *) 345(* let matchfn = match pat in *) 346(* (\th. MP (INST_TY_TERM (matchfn (concl th)) sth) th); *) 347(* *) 348(* letrec RESOLVE_THEN antel ttac impth : tactic = *) 349(* let answers = mapfilter (MATCH_MP impth) antel in *) 350(* EVERY (mapfilter ttac answers) THEN *) 351(* (EVERY (mapfilter (RESOLVE_THEN antel ttac) answers)); *) 352(* *) 353(* let IMP_RES_THEN ttac impth = *) 354(* ASSUM_LIST (\asl. *) 355(* EVERY (mapfilter (RESOLVE_THEN asl ttac) (RES_CANON impth))) ? *) 356(* failwith `IMP_RES_THEN`; *) 357(* *) 358(* IMP_RES_THEN; *) 359(* *) 360(* end_section IMP_RES_THEN; *) 361(* *) 362(* let IMP_RES_THEN = it; *) 363(* ---------------------------------------------------------------------*) 364 365(* ---------------------------------------------------------------------*) 366(* Definition of the primitive: *) 367(* *) 368(* IMP_RES_THEN: Resolve all assumptions against an implication. *) 369(* *) 370(* The definition uses an auxiliary (local) function, MATCH_MP, which is*) 371(* just like the built-in version, but doesn't use GSPEC. *) 372(* *) 373(* New implementation for version 1.12: fails if no MP-consequences can *) 374(* be drawn, and does only one-step resolution. [TFM 90.12.07] *) 375(* ---------------------------------------------------------------------*) 376 377local 378 fun MATCH_MP impth = 379 let 380 val sth = SPEC_ALL impth 381 val hyptyvars = HOLset.listItems (hyp_tyvars sth) 382 val lconstants = HOLset.intersection 383 (FVL [concl sth] empty_tmset, hyp_frees sth) 384 val matchfn = 385 match_terml hyptyvars lconstants (fst (dest_imp (concl sth))) 386 in 387 fn th => MP (INST_TY_TERM (matchfn (concl th)) sth) th 388 end 389 390(* ---------------------------------------------------------------------*) 391(* check ex l : Fail with ex if l is empty, otherwise return l. *) 392(* ---------------------------------------------------------------------*) 393 394 fun check ex [] = raise ex 395 | check ex l = l 396 397(* ---------------------------------------------------------------------*) 398(* IMP_RES_THEN : Resolve an implication against the assumptions. *) 399(* ---------------------------------------------------------------------*) 400in 401 fun IMP_RES_THEN ttac impth = 402 let 403 val ths = 404 RES_CANON impth 405 handle HOL_ERR _ => raise ERR "IMP_RES_THEN" "No implication" 406 in 407 Tactical.ASSUM_LIST 408 (fn asl => 409 let 410 val l = 411 itlist 412 (fn th => append (mapfilter (MATCH_MP th) asl)) ths [] 413 val res = check (ERR "IMP_RES_THEN" "No resolvents") l 414 val tacs = check (ERR "IMP_RES_THEN" "No tactics") 415 (Lib.mapfilter ttac res) 416 in 417 Tactical.EVERY tacs 418 end) 419 end 420 421(* ---------------------------------------------------------------------*) 422(* RES_THEN : Resolve all implicative assumptions against the rest. *) 423(* ---------------------------------------------------------------------*) 424 425 fun RES_THEN ttac (asl,g) = 426 let 427 val aas = map ASSUME asl 428 val ths = itlist append (mapfilter RES_CANON aas) [] 429 val imps = check (ERR "RES_THEN" "No implication") ths 430 val l = itlist (fn th => append (mapfilter (MATCH_MP th) aas)) imps [] 431 val res = check (ERR "RES_THEN" "No resolvents") l 432 val tacs = check (ERR "RES_THEN" "No tactics") (Lib.mapfilter ttac res) 433 in 434 Tactical.EVERY tacs (asl,g) 435 end 436end 437 438(* ---------------------------------------------------------------------- 439 PROVEHYP_THEN ttac th 440 441 th must be of form |- !x1..xn. l ==> r x1..xn 442 443 Application of tactic sets up l as a subgoal, and in the second 444 branch applies ttac to |- !x1..xn. r x1..xn 445 ---------------------------------------------------------------------- *) 446 447local 448 fun occurs_check [] tm = () 449 | occurs_check (v::vs) tm = if free_in v tm then raise (ERR "PROVEHYP_THEN" "") else occurs_check vs tm 450 val IMP_CLAUSES1 = boolTheory.IMP_CLAUSES |> SPEC_ALL |> CONJUNCT1 |> GEN_ALL 451 fun lth_mp th lth = CONV_RULE (STRIP_QUANT_CONV (LAND_CONV (K (EQT_INTRO lth)) THENC 452 REWR_CONV IMP_CLAUSES1)) th 453in 454 fun PROVEHYP_THEN t2tac th g = let 455 val (vs, tm) = strip_forall (concl th) 456 val (l, _) = dest_imp tm 457 val () = occurs_check vs l 458 in 459 Tactical.SUBGOAL_THEN l (fn lth => t2tac lth (lth_mp th lth)) 460 end g 461end 462 463val provehyp_then = PROVEHYP_THEN 464 465 466end 467