1 (* Title: Provers/blast.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1997 University of Cambridge
6 Generic tableau prover with proof reconstruction
8 SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
9 Needs explicit instantiation of assumptions?
11 Given the typeargs system, constructor Const could be eliminated, with
12 TConst replaced by a constructor that takes the typargs list as an argument.
13 However, Const is heavily used for logical connectives.
15 Blast_tac is often more powerful than fast_tac, but has some limitations.
17 * ignores wrappers (addss, addbefore, addafter, addWrapper, ...);
18 this restriction is intrinsic
19 * ignores elimination rules that don't have the correct format
20 (conclusion must be a formula variable)
21 * rules must not require higher-order unification, e.g. apply_type in ZF
22 + message "Function Var's argument not a bound variable" relates to this
23 * its proof strategy is more general but can actually be slower
26 "Recursive" chains of rules can sometimes exclude other unsafe formulae
27 from expansion. This happens because newly-created formulae always
28 have priority over existing ones. But obviously recursive rules
29 such as transitivity are treated specially to prevent this. Sometimes
30 the formulae get into the wrong order (see WRONG below).
32 With substition for equalities (hyp_subst_tac):
33 When substitution affects a haz formula or literal, it is moved
34 back to the list of safe formulae.
35 But there's no way of putting it in the right place. A "moved" or
36 "no DETERM" flag would prevent proofs failing here.
39 (*Should be a type abbreviation?*)
40 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
42 signature BLAST_DATA =
45 val equality_name: string
47 val notE : thm (* [| ~P; P |] ==> R *)
49 val contr_tac : int -> tactic
50 val dup_intr : thm -> thm
51 val hyp_subst_tac : bool -> int -> tactic
52 val claset : unit -> claset
53 val rep_cs : (* dependent on classical.ML *)
54 claset -> {safeIs: thm list, safeEs: thm list,
55 hazIs: thm list, hazEs: thm list,
56 swrappers: (string * wrapper) list,
57 uwrappers: (string * wrapper) list,
58 safe0_netpair: netpair, safep_netpair: netpair,
59 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
60 val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
61 val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
68 exception TRANS of string (*reports translation errors*)
70 Const of string * term list
71 | Skolem of string * term option ref list
73 | Var of term option ref
78 val depth_tac : claset -> int -> int -> tactic
79 val depth_limit : int Config.T
80 val blast_tac : claset -> int -> tactic
81 val Blast_tac : int -> tactic
82 val setup : theory -> theory
86 val fullTrace : branch list list ref
87 val fromType : (indexname * term) list ref -> Term.typ -> term
88 val fromTerm : theory -> Term.term -> term
89 val fromSubgoal : theory -> Term.term -> term
90 val instVars : term -> (unit -> unit)
91 val toTerm : int -> term -> Term.term
92 val readGoal : theory -> string -> term
93 val tryInThy : theory -> int -> string ->
94 (int->tactic) list * branch list list * (int*int*exn) list
95 val normBr : branch -> branch
99 functor BlastFun(Data: BLAST_DATA) : BLAST =
102 type claset = Data.claset;
104 val trace = ref false
105 and stats = ref false; (*for runtime and search statistics*)
108 Const of string * term list (*typargs constant--as a terms!*)
109 | Skolem of string * term option ref list
111 | Var of term option ref
116 (*Pending formulae carry md (may duplicate) flags*)
118 {pairs: ((term*bool) list * (*safe formulae on this level*)
119 (term*bool) list) list, (*haz formulae on this level*)
120 lits: term list, (*literals: irreducible formulae*)
121 vars: term option ref list, (*variables occurring in branch*)
122 lim: int}; (*resource limit*)
125 (* global state information *)
127 datatype state = State of
129 fullTrace: branch list list ref,
130 trail: term option ref list ref,
135 fun reject_const thy c =
136 is_some (Sign.const_type thy c) andalso
137 error ("blast: theory contains illegal constant " ^ quote c);
140 (reject_const thy "*Goal*";
141 reject_const thy "*False*";
147 nclosed = ref 0, (*branches closed: number of branches closed during the search*)
148 ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
152 (** Basic syntactic operations **)
154 fun is_Var (Var _) = true
157 fun dest_Var (Var x) = x;
161 (* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
162 val list_comb : term * term list -> term = Library.foldl (op $);
164 (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
165 fun strip_comb u : term * term list =
166 let fun stripc (f$t, ts) = stripc (f, t::ts)
170 (* maps f(t1,...,tn) to f , which is never a combination *)
171 fun head_of (f$t) = head_of f
175 (** Particular constants **)
177 fun negate P = Const (Data.not_name, []) $ P;
179 fun isNot (Const (c, _) $ _) = c = Data.not_name
182 fun mkGoal P = Const ("*Goal*", []) $ P;
184 fun isGoal (Const ("*Goal*", _) $ _) = true
187 val TruepropC = ObjectLogic.judgment_name (the_context ());
188 val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
190 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
192 fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm
193 | strip_Trueprop tm = tm;
197 (*** Dealing with overloaded constants ***)
199 (*alist is a map from TVar names to Vars. We need to unify the TVars
200 faithfully in order to track overloading*)
201 fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts)
202 | fromType alist (Term.TFree(a,_)) = Free a
203 | fromType alist (Term.TVar (ixn,_)) =
204 (case (AList.lookup (op =) (!alist) ixn) of
205 NONE => let val t' = Var(ref NONE)
206 in alist := (ixn, t') :: !alist; t'
210 fun fromConst thy alist (a, T) =
211 Const (a, map (fromType alist) (Sign.const_typargs thy (a, T)));
214 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
215 fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us)
216 | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*)
217 | (Free a) aconv (Free b) = a=b
218 | (Var(ref(SOME t))) aconv u = t aconv u
219 | t aconv (Var(ref(SOME u))) = t aconv u
220 | (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*)
221 | (Bound i) aconv (Bound j) = i=j
222 | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u
223 | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
225 and aconvs ([], []) = true
226 | aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us)
230 fun mem_term (_, []) = false
231 | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
233 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
235 fun mem_var (v: term option ref, []) = false
236 | mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs);
238 fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
243 (*Accumulates the Vars in the term, suppressing duplicates*)
244 fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
245 | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars)
246 | add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars)
247 | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars)
248 | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars)
249 | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars))
250 | add_term_vars (_, vars) = vars
251 (*Term list version. [The fold functionals are slow]*)
252 and add_terms_vars ([], vars) = vars
253 | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
254 (*Var list version.*)
255 and add_vars_vars ([], vars) = vars
256 | add_vars_vars (ref (SOME u) :: vs, vars) =
257 add_vars_vars (vs, add_term_vars(u,vars))
258 | add_vars_vars (v::vs, vars) = (*v must be a ref NONE*)
259 add_vars_vars (vs, ins_var (v, vars));
262 (*Chase assignments in "vars"; return a list of unassigned variables*)
263 fun vars_in_vars vars = add_vars_vars(vars,[]);
267 (*increment a term's non-local bound variables
268 inc is increment for bound variables
269 lev is level at which a bound variable is considered 'loose'*)
270 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
271 | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
272 | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
273 | incr_bv (inc, lev, u) = u;
275 fun incr_boundvars 0 t = t
276 | incr_boundvars inc t = incr_bv(inc,0,t);
279 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
280 (Bound 0) is loose at level 0 *)
281 fun add_loose_bnos (Bound i, lev, js) = if i<lev then js
282 else insert (op =) (i - lev) js
283 | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
284 | add_loose_bnos (f$t, lev, js) =
285 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
286 | add_loose_bnos (_, _, js) = js;
288 fun loose_bnos t = add_loose_bnos (t, 0, []);
290 fun subst_bound (arg, t) : term =
291 let fun subst (t as Bound i, lev) =
292 if i<lev then t (*var is locally bound*)
293 else if i=lev then incr_boundvars lev arg
294 else Bound(i-1) (*loose: change it*)
295 | subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
296 | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
301 (*Normalize...but not the bodies of ABSTRACTIONS*)
302 fun norm t = case t of
303 Skolem (a,args) => Skolem(a, vars_in_vars args)
304 | Const(a,ts) => Const(a, map norm ts)
305 | (Var (ref NONE)) => t
306 | (Var (ref (SOME u))) => norm u
307 | (f $ u) => (case norm f of
308 Abs(_,body) => norm (subst_bound (u, body))
313 (*Weak (one-level) normalize for use in unification*)
314 fun wkNormAux t = case t of
315 (Var v) => (case !v of
318 | (f $ u) => (case wkNormAux f of
319 Abs(_,body) => wkNorm (subst_bound (u, body))
321 | Abs (a,body) => (*eta-contract if possible*)
322 (case wkNormAux body of
324 if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0
326 else wkNorm (incr_boundvars ~1 f)
329 and wkNorm t = case head_of t of
331 | Skolem(a,args) => t
336 (*Does variable v occur in u? For unification.
337 Dangling bound vars are also forbidden.*)
339 let fun occL lev [] = false (*same as (exists occ), but faster*)
340 | occL lev (u::us) = occ lev u orelse occL lev us
341 and occ lev (Var w) =
343 (case !w of NONE => false
344 | SOME u => occ lev u)
345 | occ lev (Skolem(_,args)) = occL lev (map Var args)
346 (*ignore Const, since term variables can't occur in types (?) *)
347 | occ lev (Bound i) = lev <= i
348 | occ lev (Abs(_,u)) = occ (lev+1) u
349 | occ lev (f$u) = occ lev u orelse occ lev f
356 (*Restore the trail to some previous state: for backtracking*)
357 fun clearTo (State {ntrail, trail, ...}) n =
360 trail := tl (!trail);
361 ntrail := !ntrail - 1);
364 (*First-order unification with bound variables.
365 "vars" is a list of variables local to the rule and NOT to be put
366 on the trail (no point in doing so)
368 fun unify state (vars,t,u) =
369 let val State {ntrail, trail, ...} = state
371 fun update (t as Var v, u) =
373 else if varOccur v u then raise UNIFY
374 else if mem_var(v, vars) then v := SOME u
375 else (*avoid updating Vars in the branch if possible!*)
376 if is_Var u andalso mem_var(dest_Var u, vars)
377 then dest_Var u := SOME t
379 trail := v :: !trail; ntrail := !ntrail + 1)
381 case (wkNorm t, wkNorm u) of
382 (nt as Var v, nu) => update(nt,nu)
383 | (nu, nt as Var v) => update(nt,nu)
384 | (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts)
386 | (Abs(_,t'), Abs(_,u')) => unifyAux(t',u')
387 (*NB: can yield unifiers having dangling Bound vars!*)
388 | (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u'))
389 | (nt, nu) => if nt aconv nu then () else raise UNIFY
390 and unifysAux ([], []) = ()
391 | unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us))
392 | unifysAux _ = raise UNIFY;
393 in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false)
397 (*Convert from "real" terms to prototerms; eta-contract.
398 Code is similar to fromSubgoal.*)
400 let val alistVar = ref []
401 and alistTVar = ref []
402 fun from (Term.Const aT) = fromConst thy alistTVar aT
403 | from (Term.Free (a,_)) = Free a
404 | from (Term.Bound i) = Bound i
405 | from (Term.Var (ixn,T)) =
406 (case (AList.lookup (op =) (!alistVar) ixn) of
407 NONE => let val t' = Var(ref NONE)
408 in alistVar := (ixn, t') :: !alistVar; t'
411 | from (Term.Abs (a,_,u)) =
413 u' as (f $ Bound 0) =>
414 if member (op =) (loose_bnos f) 0 then Abs(a,u')
415 else incr_boundvars ~1 f
417 | from (Term.$ (f,u)) = from f $ from u
420 (*A debugging function: replaces all Vars by dummy Frees for visual inspection
421 of whether they are distinct. Function revert undoes the assignments.*)
423 let val name = ref "a"
425 fun inst (Const(a,ts)) = List.app inst ts
426 | inst (Var(v as ref NONE)) = (updated := v :: (!updated);
427 v := SOME (Free ("?" ^ !name));
428 name := Symbol.bump_string (!name))
429 | inst (Abs(a,t)) = inst t
430 | inst (f $ u) = (inst f; inst u)
432 fun revert() = List.app (fn v => v:=NONE) (!updated)
433 in inst t; revert end;
436 (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
437 fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
438 | strip_imp_prems _ = [];
440 (* A1==>...An==>B goes to B, where B is not an implication *)
441 fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
442 | strip_imp_concl A = strip_Trueprop A;
446 (*** Conversion of Elimination Rules to Tableau Operations ***)
448 exception ElimBadConcl and ElimBadPrem;
450 (*The conclusion becomes the goal/negated assumption *False*: delete it!
451 If we don't find it then the premise is ill-formed and could cause
453 fun delete_concl [] = raise ElimBadPrem
454 | delete_concl (P :: Ps) =
456 Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) =>
457 if c = "*Goal*" orelse c = Data.not_name then Ps
458 else P :: delete_concl Ps
459 | _ => P :: delete_concl Ps);
461 fun skoPrem vars (Const ("all", _) $ Abs (_, P)) =
462 skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
463 | skoPrem vars P = P;
466 delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
468 (*Expects elimination rules to have a formula variable as conclusion*)
469 fun convertRule vars t =
470 let val (P::Ps) = strip_imp_prems t
471 val Var v = strip_imp_concl t
472 in v := SOME (Const ("*False*", []));
473 (P, map (convertPrem o skoPrem vars) Ps)
475 handle Bind => raise ElimBadConcl;
478 (*Like dup_elim, but puts the duplicated major premise FIRST*)
479 fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
482 (*Rotate the assumptions in all new subgoals for the LIFO discipline*)
484 (*Count new hyps so that they can be rotated*)
486 | nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps
487 | nNewHyps (P::Ps) = 1 + nNewHyps Ps;
489 fun rot_tac [] i st = Seq.single st
490 | rot_tac (0::ks) i st = rot_tac ks (i+1) st
491 | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
493 fun rot_subgoals_tac (rot, rl) =
494 rot_tac (if rot then map nNewHyps rl else [])
498 fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
500 (*Resolution/matching tactics: if upd then the proof state may be updated.
501 Matching makes the tactics more deterministic in the presence of Vars.*)
502 fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
503 fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
505 (*Tableau rule from elimination rule.
506 Flag "upd" says that the inference updated the branch.
507 Flag "dup" requests duplication of the affected formula.*)
508 fun fromRule thy vars rl =
509 let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
510 fun tac (upd, dup,rot) i =
511 emtac upd (if dup then rev_dup_elim rl else rl) i
513 rot_subgoals_tac (rot, #2 trl) i
514 in Option.SOME (trl, tac) end
515 handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
516 (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
518 | ElimBadConcl => (*ignore: conclusion is not just a variable*)
519 (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
520 "conclusion should be a variable\n" ^ Display.string_of_thm rl))
525 (*** Conversion of Introduction Rules ***)
527 fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
529 fun convertIntrRule vars t =
530 let val Ps = strip_imp_prems t
531 val P = strip_imp_concl t
532 in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
535 (*Tableau rule from introduction rule.
536 Flag "upd" says that the inference updated the branch.
537 Flag "dup" requests duplication of the affected formula.
538 Since haz rules are now delayed, "dup" is always FALSE for
539 introduction rules.*)
540 fun fromIntrRule thy vars rl =
541 let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
542 fun tac (upd,dup,rot) i =
543 rmtac upd (if dup then Data.dup_intr rl else rl) i
545 rot_subgoals_tac (rot, #2 trl) i
549 val dummyVar = Term.Var (("etc",0), dummyT);
551 (*Convert from prototerms to ordinary terms with dummy types
552 Ignore abstractions; identify all Vars; STOP at given depth*)
553 fun toTerm 0 _ = dummyVar
554 | toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*)
555 | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
556 | toTerm d (Free a) = Term.Free (a,dummyT)
557 | toTerm d (Bound i) = Term.Bound i
558 | toTerm d (Var _) = dummyVar
559 | toTerm d (Abs(a,_)) = dummyVar
560 | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
563 fun netMkRules thy P vars (nps: netpair list) =
565 (Const ("*Goal*", _) $ G) =>
566 let val pG = mk_Trueprop (toTerm 2 G)
567 val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
568 in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end
570 let val pP = mk_Trueprop (toTerm 3 P)
571 val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
572 in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end;
575 (*Normalize a branch--for tracing*)
576 fun norm2 (G,md) = (norm G, md);
578 fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
580 fun normBr {pairs, lits, vars, lim} =
581 {pairs = map normLev pairs,
582 lits = map norm lits,
587 val dummyTVar = Term.TVar(("a",0), []);
588 val dummyVar2 = Term.Var(("var",0), dummyT);
590 (*convert blast_tac's type representation to real types for tracing*)
591 fun showType (Free a) = Term.TFree (a,[])
592 | showType (Var _) = dummyTVar
594 (case strip_comb t of
595 (Const (a, _), us) => Term.Type(a, map showType us)
598 (*Display top-level overloading if any*)
599 fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts))
600 | topType thy (Abs(a,t)) = topType thy t
601 | topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some)
602 | topType _ _ = NONE;
605 (*Convert from prototerms to ordinary terms with dummy types for tracing*)
606 fun showTerm d (Const (a,_)) = Term.Const (a,dummyT)
607 | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
608 | showTerm d (Free a) = Term.Free (a,dummyT)
609 | showTerm d (Bound i) = Term.Bound i
610 | showTerm d (Var(ref(SOME u))) = showTerm d u
611 | showTerm d (Var(ref NONE)) = dummyVar2
612 | showTerm d (Abs(a,t)) = if d=0 then dummyVar
613 else Term.Abs(a, dummyT, showTerm (d-1) t)
614 | showTerm d (f $ u) = if d=0 then dummyVar
615 else Term.$ (showTerm d f, showTerm (d-1) u);
617 fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
619 (*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like
620 Ex(P) is duplicated as the assumption ~Ex(P). *)
621 fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
624 fun negOfGoal2 (G,md) = (negOfGoal G, md);
626 (*Converts all Goals to Nots in the safe parts of a branch. They could
627 have been moved there from the literals list after substitution (equalSubst).
628 There can be at most one--this function could be made more efficient.*)
629 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
631 (*Tactic. Convert *Goal* to negated assumption in FIRST position*)
632 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
635 fun traceTerm thy t =
636 let val t' = norm (negOfGoal t)
637 val stm = string_of thy 8 t'
639 case topType thy t' of
640 NONE => stm (*no type to attach*)
641 | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
645 (*Print tracing information at each iteration of prover*)
646 fun tracing (State {thy, fullTrace, ...}) brs =
647 let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G)
648 | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)")
650 fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
651 (fullTrace := brs0 :: !fullTrace;
652 List.app (fn _ => Output.immediate_output "+") brs;
653 Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
656 in if !trace then printBrs (map normBr brs) else ()
659 fun traceMsg s = if !trace then writeln s else ();
661 (*Tracing: variables updated in the last branch operation?*)
662 fun traceVars (State {thy, ntrail, trail, ...}) ntrl =
664 (case !ntrail-ntrl of
666 | 1 => Output.immediate_output"\t1 variable UPDATED:"
667 | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
668 (*display the instantiations themselves, though no variable names*)
669 List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v))))
670 (List.take(!trail, !ntrail-ntrl));
674 (*Tracing: how many new branches are created?*)
678 0 => Output.immediate_output"branch closed by rule"
679 | 1 => Output.immediate_output"branch extended (1 new subgoal)"
680 | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
685 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
687 (*Replace the ATOMIC term "old" by "new" in t*)
688 fun subst_atomic (old,new) t =
689 let fun subst (Var(ref(SOME u))) = subst u
690 | subst (Abs(a,body)) = Abs(a, subst body)
691 | subst (f$t) = subst f $ subst t
692 | subst t = if t aconv old then new else t
695 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
696 fun eta_contract_atom (t0 as Abs(a, body)) =
697 (case eta_contract2 body of
698 f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0
699 else eta_contract_atom (incr_boundvars ~1 f)
701 | eta_contract_atom t = t
702 and eta_contract2 (f$t) = f $ eta_contract_atom t
703 | eta_contract2 t = eta_contract_atom t;
706 (*When can we safely delete the equality?
707 Not if it equates two constants; consider 0=1.
708 Not if it resembles x=t[x], since substitution does not eliminate x.
709 Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
710 Prefer to eliminate Bound variables if possible.
711 Result: true = use as is, false = reorient first *)
713 (*Can t occur in u? For substitution.
714 Does NOT examine the args of Skolem terms: substitution does not affect them.
715 REFLEXIVE because hyp_subst_tac fails on x=x.*)
717 let (*NO vars are permitted in u except the arguments of t, if it is
718 a Skolem term. This ensures that no equations are deleted that could
719 be instantiated to a cycle. For example, x=?a is rejected because ?a
720 could be instantiated to Suc(x).*)
722 Skolem(_,vars) => vars
724 fun occEq u = (t aconv u) orelse occ u
725 and occ (Var(ref(SOME u))) = occEq u
726 | occ (Var v) = not (mem_var (v, vars))
727 | occ (Abs(_,u)) = occEq u
728 | occ (f$u) = occEq u orelse occEq f
734 (*Take apart an equality. NO constant Trueprop*)
735 fun dest_eq (Const (c, _) $ t $ u) =
736 if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u)
738 | dest_eq _ = raise DEST_EQ;
740 (*Reject the equality if u occurs in (or equals!) t*)
741 fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
743 (*IF the goal is an equality with a substitutable variable
744 THEN orient that equality ELSE raise exception DEST_EQ*)
745 fun orientGoal (t,u) = case (t,u) of
746 (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*)
747 | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*)
748 | (Free _, _) => check(t,u,(t,u)) (*eliminates t*)
749 | (_, Free _) => check(u,t,(u,t)) (*eliminates u*)
750 | _ => raise DEST_EQ;
752 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
753 Moves affected literals back into the branch, but it is not clear where
754 they should go: this could make proofs fail.*)
755 fun equalSubst thy (G, {pairs, lits, vars, lim}) =
756 let val (t,u) = orientGoal(dest_eq G)
757 val subst = subst_atomic (t,u)
758 fun subst2(G,md) = (subst G, md)
759 (*substitute throughout list; extract affected formulae*)
760 fun subForm ((G,md), (changed, pairs)) =
762 in if nG aconv G then (changed, (G,md)::pairs)
763 else ((nG,md)::changed, pairs)
765 (*substitute throughout "stack frame"; extract affected formulae*)
766 fun subFrame ((Gs,Hs), (changed, frames)) =
767 let val (changed', Gs') = foldr subForm (changed, []) Gs
768 val (changed'', Hs') = foldr subForm (changed', []) Hs
769 in (changed'', (Gs',Hs')::frames) end
770 (*substitute throughout literals; extract affected ones*)
771 fun subLit (lit, (changed, nlits)) =
772 let val nlit = subst lit
773 in if nlit aconv lit then (changed, nlit::nlits)
774 else ((nlit,true)::changed, nlits)
776 val (changed, lits') = foldr subLit ([], []) lits
777 val (changed', pairs') = foldr subFrame (changed, []) pairs
778 in if !trace then writeln ("Substituting " ^ traceTerm thy u ^
779 " for " ^ traceTerm thy t ^ " in branch" )
781 {pairs = (changed',[])::pairs', (*affected formulas, and others*)
782 lits = lits', (*unaffected literals*)
788 exception NEWBRANCHES and CLOSEF;
792 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
793 val contr_tac = ematch_tac [Data.notE] THEN'
794 (eq_assume_tac ORELSE' assume_tac);
796 val eContr_tac = TRACE Data.notE contr_tac;
797 val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
799 (*Try to unify complementary literals and return the corresponding tactic. *)
800 fun tryClose state (G, L) =
802 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
805 if isGoal G then close (arg G) L eAssume_tac
806 else if isGoal L then close G (arg L) eAssume_tac
807 else if isNot G then close (arg G) L eContr_tac
808 else if isNot L then close G (arg L) eContr_tac
812 (*Were there Skolem terms in the premise? Must NOT chase Vars*)
813 fun hasSkolem (Skolem _) = true
814 | hasSkolem (Abs (_,body)) = hasSkolem body
815 | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
816 | hasSkolem _ = false;
818 (*Attach the right "may duplicate" flag to new formulae: if they contain
819 Skolem terms then allow duplication.*)
820 fun joinMd md [] = []
821 | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
824 (** Backtracking and Pruning **)
826 (*clashVar vars (n,trail) determines whether any of the last n elements
827 of "trail" occur in "vars" OR in their instantiations*)
828 fun clashVar [] = (fn _ => false)
830 let fun clash (0, _) = false
831 | clash (_, []) = false
832 | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
836 (*nbrs = # of branches just prior to closing this one. Delete choice points
837 for goals proved by the latest inference, provided NO variables in the
838 next branch have been updated.*)
839 fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
840 backtracking over bad proofs*)
841 | prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) =
842 let fun traceIt last =
843 let val ll = length last
844 and lc = length choices
845 in if !trace andalso ll<lc then
846 (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
850 fun pruneAux (last, _, _, []) = last
851 | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
853 then last (*don't backtrack beyond first solution of goal*)
854 else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
855 else (* nbrs'=nbrs *)
856 if clashVar nxtVars (ntrl-ntrl', trl) then last
857 else (*no clashes: can go back at least this far!*)
858 pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
860 in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end;
862 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
865 fun backtrack (choices as (ntrl, nbrs, exn)::_) =
866 (if !trace then (writeln ("Backtracking; now there are " ^
867 Int.toString nbrs ^ " branches"))
870 | backtrack _ = raise PROVE;
872 (*Add the literal G, handling *Goal* and detecting duplicates.*)
873 fun addLit (Const ("*Goal*", _) $ G, lits) =
874 (*New literal is a *Goal*, so change all other Goals to Nots*)
875 let fun bad (Const ("*Goal*", _) $ _) = true
876 | bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G'
879 | change (lit :: lits) =
882 if c = "*Goal*" orelse c = Data.not_name then
883 if G aconv G' then change lits
884 else negate G' :: change lits
885 else lit :: change lits
886 | _ => lit :: change lits)
888 Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits)
890 | addLit (G,lits) = ins_term(G, lits)
893 (*For calculating the "penalty" to assess on a branching factor of n
894 log2 seems a little too severe*)
895 fun log n = if n<4 then 0 else 1 + log(n div 4);
898 (*match(t,u) says whether the term u might be an instance of the pattern t
899 Used to detect "recursive" rules such as transitivity*)
900 fun match (Var _) u = true
901 | match (Const (a,tas)) (Const (b,tbs)) =
902 a = "*Goal*" andalso b = Data.not_name orelse
903 a = Data.not_name andalso b = "*Goal*" orelse
904 a = b andalso matchs tas tbs
905 | match (Free a) (Free b) = (a=b)
906 | match (Bound i) (Bound j) = (i=j)
907 | match (Abs(_,t)) (Abs(_,u)) = match t u
908 | match (f$t) (g$u) = match f g andalso match t u
910 and matchs [] [] = true
911 | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us;
914 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
916 writeln (end_timing start ^ " for search. Closed: "
917 ^ Int.toString (!nclosed) ^
918 " tried: " ^ Int.toString (!ntried) ^
919 " tactics: " ^ Int.toString (length tacs))
923 (*Tableau prover based on leanTaP. Argument is a list of branches. Each
924 branch contains a list of unexpanded formulae, a list of literals, and a
925 bound on unsafe expansions.
926 "start" is CPU time at start, for printing search time
928 fun prove (state, start, cs, brs, cont) =
929 let val State {thy, ntrail, nclosed, ntried, ...} = state;
930 val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
931 val safeList = [safe0_netpair, safep_netpair]
932 and hazList = [haz_netpair]
933 fun prv (tacs, trs, choices, []) =
934 (printStats state (!trace orelse !stats, start, tacs);
935 cont (tacs, trs, choices)) (*all branches closed!*)
936 | prv (tacs, trs, choices,
937 brs0 as {pairs = ((G,md)::br, haz)::pairs,
938 lits, vars, lim} :: brs) =
939 (*apply a safe rule only (possibly allowing instantiation);
940 defer any haz formulae*)
941 let exception PRV (*backtrack to precisely this recursion!*)
943 val nbrs = length brs0
944 val nxtVars = nextVars brs
946 val rules = netMkRules thy G vars safeList
947 (*Make a new branch, decrementing "lim" if instantiations occur*)
948 fun newBr (vars',lim') prems =
950 if (exists isGoal prem)
951 then {pairs = ((joinMd md prem, []) ::
952 negOfGoals ((br, haz)::pairs)),
953 lits = map negOfGoal lits,
956 else {pairs = ((joinMd md prem, []) ::
963 (*Seek a matching rule. If unifiable then add new premises
965 fun deeper [] = raise NEWBRANCHES
966 | deeper (((P,prems),tac)::grls) =
967 if unify state (add_term_vars(P,[]), P, G)
968 then (*P comes from the rule; G comes from the branch.*)
969 let val updated = ntrl < !ntrail (*branch updated*)
970 val lim' = if updated
971 then lim - (1+log(length rules))
972 else lim (*discourage branching updates*)
973 val vars = vars_in_vars vars
974 val vars' = foldr add_terms_vars vars prems
975 val choices' = (ntrl, nbrs, PRV) :: choices
976 val tacs' = (tac(updated,false,true))
977 :: tacs (*no duplication; rotate*)
979 traceNew prems; traceVars state ntrl;
980 (if null prems then (*closed the branch: prune!*)
981 (nclosed := !nclosed + 1;
982 prv(tacs', brs0::trs,
983 prune state (nbrs, nxtVars, choices'),
985 else (*prems non-null*)
986 if lim'<0 (*faster to kill ALL the alternatives*)
987 then (traceMsg"Excessive branching: KILLED";
988 clearTo state ntrl; raise NEWBRANCHES)
990 (ntried := !ntried + length prems - 1;
991 prv(tacs', brs0::trs, choices',
992 newBr (vars',lim') prems)))
995 (*Backtrack at this level.
996 Reset Vars and try another rule*)
997 (clearTo state ntrl; deeper grls)
998 else (*backtrack to previous level*)
1002 (*Try to close branch by unifying with head goal*)
1003 fun closeF [] = raise CLOSEF
1005 case tryClose state (G,L) of
1009 (if !trace then (Output.immediate_output"branch closed";
1010 traceVars state ntrl)
1012 prune state (nbrs, nxtVars,
1013 (ntrl, nbrs, PRV) :: choices))
1014 in nclosed := !nclosed + 1;
1015 prv (tac::tacs, brs0::trs, choices', brs)
1017 (*reset Vars and try another literal
1018 [this handler is pruned if possible!]*)
1019 (clearTo state ntrl; closeF Ls)
1021 (*Try to unify a queued formula (safe or haz) with head goal*)
1022 fun closeFl [] = raise CLOSEF
1023 | closeFl ((br, haz)::pairs) =
1025 handle CLOSEF => closeF (map fst haz)
1026 handle CLOSEF => closeFl pairs
1027 in tracing state brs0;
1028 if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
1030 prv (Data.hyp_subst_tac (!trace) :: tacs,
1033 (G, {pairs = (br,haz)::pairs,
1034 lits = lits, vars = vars, lim = lim})
1036 handle DEST_EQ => closeF lits
1037 handle CLOSEF => closeFl ((br,haz)::pairs)
1038 handle CLOSEF => deeper rules
1039 handle NEWBRANCHES =>
1040 (case netMkRules thy G vars hazList of
1041 [] => (*there are no plausible haz rules*)
1042 (traceMsg "moving formula to literals";
1043 prv (tacs, brs0::trs, choices,
1044 {pairs = (br,haz)::pairs,
1045 lits = addLit(G,lits),
1048 | _ => (*G admits some haz rules: try later*)
1049 (traceMsg "moving formula to haz list";
1050 prv (if isGoal G then negOfGoal_tac :: tacs
1054 {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
1057 lim = lim} :: brs)))
1059 | prv (tacs, trs, choices,
1060 {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
1061 (*no more "safe" formulae: transfer haz down a level*)
1062 prv (tacs, trs, choices,
1063 {pairs = (Gs,haz@haz')::pairs,
1067 | prv (tacs, trs, choices,
1068 brs0 as {pairs = [([], (H,md)::Hs)],
1069 lits, vars, lim} :: brs) =
1070 (*no safe steps possible at any level: apply a haz rule*)
1071 let exception PRV (*backtrack to precisely this recursion!*)
1074 val rules = netMkRules thy H vars hazList
1075 (*new premises of haz rules may NOT be duplicated*)
1076 fun newPrem (vars,P,dup,lim') prem =
1077 let val Gs' = map (fn Q => (Q,false)) prem
1078 and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
1079 and lits' = if (exists isGoal prem)
1080 then map negOfGoal lits
1082 in {pairs = if exists (match P) prem then [(Gs',Hs')]
1083 (*Recursive in this premise. Don't make new
1084 "stack frame". New haz premises will end up
1085 at the BACK of the queue, preventing
1086 exclusion of others*)
1087 else [(Gs',[]), ([],Hs')],
1092 fun newBr x prems = map (newPrem x) prems @ brs
1093 (*Seek a matching rule. If unifiable then add new premises
1095 fun deeper [] = raise NEWBRANCHES
1096 | deeper (((P,prems),tac)::grls) =
1097 if unify state (add_term_vars(P,[]), P, H)
1099 let val updated = ntrl < !ntrail (*branch updated*)
1100 val vars = vars_in_vars vars
1101 val vars' = foldr add_terms_vars vars prems
1102 (*duplicate H if md permits*)
1103 val dup = md (*earlier had "andalso vars' <> vars":
1104 duplicate only if the subgoal has new vars*)
1105 (*any instances of P in the subgoals?
1106 NB: boolean "recur" affects tracing only!*)
1107 and recur = exists (exists (match P)) prems
1108 val lim' = (*Decrement "lim" extra if updates occur*)
1109 if updated then lim - (1+log(length rules))
1111 (*It is tempting to leave "lim" UNCHANGED if
1112 both dup and recur are false. Proofs are
1113 found at shallower depths, but looping
1114 occurs too often...*)
1116 (*Allowing backtracking from a rule application
1117 if other matching rules exist, if the rule
1118 updated variables, or if the rule did not
1119 introduce new variables. This latter condition
1120 means it is not a standard "gamma-rule" but
1121 some other form of unsafe rule. Aim is to
1122 emulate Fast_tac, which allows all unsafe steps
1124 not(null grls) (*other rules to try?*)
1126 orelse vars=vars' (*no new Vars?*)
1127 val tac' = tac(updated, dup, true)
1128 (*if recur then perhaps shouldn't call rotate_tac: new
1129 formulae should be last, but that's WRONG if the new
1130 formulae are Goals, since they remain in the first
1134 if lim'<0 andalso not (null prems)
1135 then (*it's faster to kill ALL the alternatives*)
1136 (traceMsg"Excessive branching: KILLED";
1137 clearTo state ntrl; raise NEWBRANCHES)
1140 if !trace andalso dup then Output.immediate_output" (duplicating)"
1142 if !trace andalso recur then Output.immediate_output" (recursive)"
1144 traceVars state ntrl;
1145 if null prems then nclosed := !nclosed + 1
1146 else ntried := !ntried + length prems - 1;
1149 (ntrl, length brs0, PRV) :: choices,
1150 newBr (vars', P, dup, lim') prems)
1153 then (*reset Vars and try another rule*)
1154 (clearTo state ntrl; deeper grls)
1155 else (*backtrack to previous level*)
1159 in tracing state brs0;
1160 if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
1162 handle NEWBRANCHES =>
1163 (*cannot close branch: move H to literals*)
1164 prv (tacs, brs0::trs, choices,
1165 {pairs = [([], Hs)],
1170 | prv (tacs, trs, choices, _ :: brs) = backtrack choices
1171 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
1174 (*Construct an initial branch.*)
1175 fun initBranch (ts,lim) =
1176 {pairs = [(map (fn t => (t,true)) ts, [])],
1178 vars = add_terms_vars (ts,[]),
1182 (*** Conversion & Skolemization of the Isabelle proof state ***)
1184 (*Make a list of all the parameters in a subgoal, even if nested*)
1187 fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
1188 | discard_foralls t = t;
1191 (*List of variables not appearing as arguments to the given parameter*)
1192 fun getVars [] i = []
1193 | getVars ((_,(v,is))::alist) (i: int) =
1194 if member (op =) is i then getVars alist i
1195 else v :: getVars alist i;
1197 exception TRANS of string;
1199 (*Translation of a subgoal: Skolemize all parameters*)
1200 fun fromSubgoal thy t =
1201 let val alistVar = ref []
1202 and alistTVar = ref []
1203 fun hdvar ((ix,(v,is))::_) = v
1205 let val (ht,ts) = Term.strip_comb t
1206 fun apply u = list_comb (u, map (from lev) ts)
1208 | bounds (Term.Bound i::ts) =
1209 if i<lev then raise TRANS
1210 "Function unknown's argument not a parameter"
1211 else i-lev :: bounds ts
1212 | bounds ts = raise TRANS
1213 "Function unknown's argument not a bound variable"
1216 Term.Const aT => apply (fromConst thy alistTVar aT)
1217 | Term.Free (a,_) => apply (Free a)
1218 | Term.Bound i => apply (Bound i)
1219 | Term.Var (ix,_) =>
1220 (case (AList.lookup (op =) (!alistVar) ix) of
1221 NONE => (alistVar := (ix, (ref NONE, bounds ts))
1223 Var (hdvar(!alistVar)))
1224 | SOME(v,is) => if is=bounds ts then Var v
1226 ("Discrepancy among occurrences of "
1227 ^ Term.string_of_vname ix))
1228 | Term.Abs (a,_,body) =>
1229 if null ts then Abs(a, from (lev+1) body)
1230 else raise TRANS "argument not in normal form"
1233 val npars = length (Logic.strip_params t)
1235 (*Skolemize a subgoal from a proof state*)
1236 fun skoSubgoal i t =
1239 (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
1243 in skoSubgoal 0 (from 0 (discard_foralls t)) end;
1246 (*Tactic using tableau engine and proof reconstruction.
1247 "start" is CPU time at start, for printing SEARCH time
1248 (also prints reconstruction time)
1249 "lim" is depth limit.*)
1250 fun timing_depth_tac start cs lim i st0 =
1251 let val thy = Thm.theory_of_thm st0
1252 val state = initialize thy
1253 val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
1254 val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
1255 val hyps = strip_imp_prems skoprem
1256 and concl = strip_imp_concl skoprem
1257 fun cont (tacs,_,choices) =
1258 let val start = start_timing ()
1260 case Seq.pull(EVERY' (rev tacs) i st) of
1261 NONE => (writeln ("PROOF FAILED for depth " ^
1263 if !trace then error "************************\n"
1266 | cell => (if (!trace orelse !stats)
1267 then writeln (end_timing start ^ " for reconstruction")
1269 Seq.make(fn()=> cell))
1271 in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end
1272 handle PROVE => Seq.empty
1274 (*Public version with fixed depth*)
1275 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
1277 val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
1279 fun blast_tac cs i st =
1280 ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
1281 (timing_depth_tac (start_timing ()) cs) 0) i
1282 THEN flexflex_tac) st
1284 ((if !trace then warning ("blast: " ^ s) else ());
1287 fun Blast_tac i = blast_tac (Data.claset()) i;
1290 (*** For debugging: these apply the prover to a subgoal and return
1291 the resulting tactics, trace, etc. ***)
1293 val fullTrace = ref ([]: branch list list);
1295 (*Read a string to make an initial, singleton branch*)
1296 fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
1298 fun tryInThy thy lim s =
1300 val state as State {fullTrace = ft, ...} = initialize thy;
1301 val res = timeap prove
1302 (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
1303 val _ = fullTrace := !ft;
1307 (** method setup **)
1310 Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
1311 (fn NONE => Data.cla_meth' blast_tac
1312 | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
1315 setup_depth_limit #>
1316 Method.add_methods [("blast", blast_method, "tableau prover")];