wenzelm@18525
|
1 |
(* Title: Provers/blast.ML
|
wenzelm@18525
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@3083
|
3 |
Copyright 1997 University of Cambridge
|
paulson@2894
|
4 |
|
paulson@2894
|
5 |
Generic tableau prover with proof reconstruction
|
paulson@2894
|
6 |
|
paulson@2854
|
7 |
SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
|
paulson@2894
|
8 |
Needs explicit instantiation of assumptions?
|
paulson@2894
|
9 |
|
paulson@18171
|
10 |
Given the typeargs system, constructor Const could be eliminated, with
|
paulson@18171
|
11 |
TConst replaced by a constructor that takes the typargs list as an argument.
|
paulson@18171
|
12 |
However, Const is heavily used for logical connectives.
|
paulson@2894
|
13 |
|
paulson@2924
|
14 |
Blast_tac is often more powerful than fast_tac, but has some limitations.
|
paulson@2924
|
15 |
Blast_tac...
|
wenzelm@18525
|
16 |
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...);
|
oheimb@4651
|
17 |
this restriction is intrinsic
|
paulson@2894
|
18 |
* ignores elimination rules that don't have the correct format
|
wenzelm@18525
|
19 |
(conclusion must be a formula variable)
|
paulson@2924
|
20 |
* rules must not require higher-order unification, e.g. apply_type in ZF
|
paulson@2924
|
21 |
+ message "Function Var's argument not a bound variable" relates to this
|
paulson@2924
|
22 |
* its proof strategy is more general but can actually be slower
|
paulson@2894
|
23 |
|
paulson@2894
|
24 |
Known problems:
|
paulson@3092
|
25 |
"Recursive" chains of rules can sometimes exclude other unsafe formulae
|
wenzelm@18525
|
26 |
from expansion. This happens because newly-created formulae always
|
wenzelm@18525
|
27 |
have priority over existing ones. But obviously recursive rules
|
wenzelm@18525
|
28 |
such as transitivity are treated specially to prevent this. Sometimes
|
wenzelm@18525
|
29 |
the formulae get into the wrong order (see WRONG below).
|
paulson@3021
|
30 |
|
paulson@2924
|
31 |
With substition for equalities (hyp_subst_tac):
|
paulson@3092
|
32 |
When substitution affects a haz formula or literal, it is moved
|
paulson@2924
|
33 |
back to the list of safe formulae.
|
paulson@2924
|
34 |
But there's no way of putting it in the right place. A "moved" or
|
paulson@2924
|
35 |
"no DETERM" flag would prevent proofs failing here.
|
paulson@2854
|
36 |
*)
|
paulson@2854
|
37 |
|
paulson@2854
|
38 |
(*Should be a type abbreviation?*)
|
paulson@2854
|
39 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
|
paulson@2854
|
40 |
|
paulson@2854
|
41 |
signature BLAST_DATA =
|
paulson@2854
|
42 |
sig
|
paulson@2854
|
43 |
type claset
|
wenzelm@18525
|
44 |
val equality_name: string
|
wenzelm@18525
|
45 |
val not_name: string
|
wenzelm@18525
|
46 |
val notE : thm (* [| ~P; P |] ==> R *)
|
wenzelm@18525
|
47 |
val ccontr : thm
|
wenzelm@18525
|
48 |
val contr_tac : int -> tactic
|
wenzelm@18525
|
49 |
val dup_intr : thm -> thm
|
wenzelm@23908
|
50 |
val hyp_subst_tac : bool -> int -> tactic
|
wenzelm@18525
|
51 |
val claset : unit -> claset
|
wenzelm@18525
|
52 |
val rep_cs : (* dependent on classical.ML *)
|
wenzelm@18525
|
53 |
claset -> {safeIs: thm list, safeEs: thm list,
|
wenzelm@18525
|
54 |
hazIs: thm list, hazEs: thm list,
|
wenzelm@18525
|
55 |
swrappers: (string * wrapper) list,
|
wenzelm@18525
|
56 |
uwrappers: (string * wrapper) list,
|
wenzelm@18525
|
57 |
safe0_netpair: netpair, safep_netpair: netpair,
|
wenzelm@18525
|
58 |
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
|
wenzelm@7272
|
59 |
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
|
wenzelm@7559
|
60 |
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
|
paulson@2854
|
61 |
end;
|
paulson@2854
|
62 |
|
paulson@2854
|
63 |
|
paulson@2854
|
64 |
signature BLAST =
|
paulson@2854
|
65 |
sig
|
wenzelm@18525
|
66 |
type claset
|
paulson@4233
|
67 |
exception TRANS of string (*reports translation errors*)
|
wenzelm@18525
|
68 |
datatype term =
|
wenzelm@18177
|
69 |
Const of string * term list
|
paulson@2924
|
70 |
| Skolem of string * term option ref list
|
paulson@2924
|
71 |
| Free of string
|
paulson@2924
|
72 |
| Var of term option ref
|
paulson@2924
|
73 |
| Bound of int
|
paulson@2924
|
74 |
| Abs of string*term
|
wenzelm@17795
|
75 |
| $ of term*term;
|
paulson@2924
|
76 |
type branch
|
wenzelm@18525
|
77 |
val depth_tac : claset -> int -> int -> tactic
|
wenzelm@24112
|
78 |
val depth_limit : int Config.T
|
wenzelm@18525
|
79 |
val blast_tac : claset -> int -> tactic
|
wenzelm@18525
|
80 |
val Blast_tac : int -> tactic
|
wenzelm@18708
|
81 |
val setup : theory -> theory
|
paulson@2924
|
82 |
(*debugging tools*)
|
wenzelm@18525
|
83 |
val stats : bool ref
|
wenzelm@18525
|
84 |
val trace : bool ref
|
wenzelm@18525
|
85 |
val fullTrace : branch list list ref
|
wenzelm@18525
|
86 |
val fromType : (indexname * term) list ref -> Term.typ -> term
|
wenzelm@24062
|
87 |
val fromTerm : theory -> Term.term -> term
|
wenzelm@24062
|
88 |
val fromSubgoal : theory -> Term.term -> term
|
paulson@4065
|
89 |
val instVars : term -> (unit -> unit)
|
wenzelm@18525
|
90 |
val toTerm : int -> term -> Term.term
|
wenzelm@18525
|
91 |
val readGoal : theory -> string -> term
|
wenzelm@18525
|
92 |
val tryInThy : theory -> int -> string ->
|
paulson@3083
|
93 |
(int->tactic) list * branch list list * (int*int*exn) list
|
wenzelm@18525
|
94 |
val normBr : branch -> branch
|
paulson@2854
|
95 |
end;
|
paulson@2854
|
96 |
|
paulson@2854
|
97 |
|
wenzelm@18525
|
98 |
functor BlastFun(Data: BLAST_DATA) : BLAST =
|
paulson@2854
|
99 |
struct
|
paulson@2854
|
100 |
|
paulson@2854
|
101 |
type claset = Data.claset;
|
paulson@2854
|
102 |
|
paulson@4323
|
103 |
val trace = ref false
|
paulson@4323
|
104 |
and stats = ref false; (*for runtime and search statistics*)
|
paulson@2854
|
105 |
|
wenzelm@18525
|
106 |
datatype term =
|
wenzelm@18177
|
107 |
Const of string * term list (*typargs constant--as a terms!*)
|
paulson@2854
|
108 |
| Skolem of string * term option ref list
|
paulson@5343
|
109 |
| Free of string
|
paulson@5343
|
110 |
| Var of term option ref
|
paulson@5343
|
111 |
| Bound of int
|
paulson@5343
|
112 |
| Abs of string*term
|
paulson@5613
|
113 |
| op $ of term*term;
|
paulson@2854
|
114 |
|
wenzelm@24062
|
115 |
(*Pending formulae carry md (may duplicate) flags*)
|
wenzelm@24062
|
116 |
type branch =
|
wenzelm@24062
|
117 |
{pairs: ((term*bool) list * (*safe formulae on this level*)
|
wenzelm@24062
|
118 |
(term*bool) list) list, (*haz formulae on this level*)
|
wenzelm@24062
|
119 |
lits: term list, (*literals: irreducible formulae*)
|
wenzelm@24062
|
120 |
vars: term option ref list, (*variables occurring in branch*)
|
wenzelm@24062
|
121 |
lim: int}; (*resource limit*)
|
wenzelm@24062
|
122 |
|
wenzelm@24062
|
123 |
|
wenzelm@24062
|
124 |
(* global state information *)
|
wenzelm@24062
|
125 |
|
wenzelm@24062
|
126 |
datatype state = State of
|
wenzelm@24062
|
127 |
{thy: theory,
|
wenzelm@24062
|
128 |
fullTrace: branch list list ref,
|
wenzelm@24062
|
129 |
trail: term option ref list ref,
|
wenzelm@24062
|
130 |
ntrail: int ref,
|
wenzelm@24062
|
131 |
nclosed: int ref,
|
wenzelm@24062
|
132 |
ntried: int ref}
|
wenzelm@24062
|
133 |
|
wenzelm@24062
|
134 |
fun reject_const thy c =
|
wenzelm@24062
|
135 |
is_some (Sign.const_type thy c) andalso
|
wenzelm@24062
|
136 |
error ("blast: theory contains illegal constant " ^ quote c);
|
wenzelm@24062
|
137 |
|
wenzelm@24062
|
138 |
fun initialize thy =
|
wenzelm@24062
|
139 |
(reject_const thy "*Goal*";
|
wenzelm@24062
|
140 |
reject_const thy "*False*";
|
wenzelm@24062
|
141 |
State
|
wenzelm@24062
|
142 |
{thy = thy,
|
wenzelm@24062
|
143 |
fullTrace = ref [],
|
wenzelm@24062
|
144 |
trail = ref [],
|
wenzelm@24062
|
145 |
ntrail = ref 0,
|
wenzelm@24062
|
146 |
nclosed = ref 0, (*branches closed: number of branches closed during the search*)
|
wenzelm@24062
|
147 |
ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
|
wenzelm@24062
|
148 |
|
wenzelm@24062
|
149 |
|
paulson@2854
|
150 |
|
paulson@2854
|
151 |
(** Basic syntactic operations **)
|
paulson@2854
|
152 |
|
paulson@2854
|
153 |
fun is_Var (Var _) = true
|
paulson@2854
|
154 |
| is_Var _ = false;
|
paulson@2854
|
155 |
|
paulson@2854
|
156 |
fun dest_Var (Var x) = x;
|
paulson@2854
|
157 |
|
paulson@2854
|
158 |
fun rand (f$x) = x;
|
paulson@2854
|
159 |
|
paulson@2854
|
160 |
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
|
skalberg@15570
|
161 |
val list_comb : term * term list -> term = Library.foldl (op $);
|
paulson@2854
|
162 |
|
paulson@2854
|
163 |
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
|
wenzelm@18525
|
164 |
fun strip_comb u : term * term list =
|
paulson@2854
|
165 |
let fun stripc (f$t, ts) = stripc (f, t::ts)
|
wenzelm@18525
|
166 |
| stripc x = x
|
paulson@2854
|
167 |
in stripc(u,[]) end;
|
paulson@2854
|
168 |
|
paulson@2854
|
169 |
(* maps f(t1,...,tn) to f , which is never a combination *)
|
paulson@2854
|
170 |
fun head_of (f$t) = head_of f
|
paulson@2854
|
171 |
| head_of u = u;
|
paulson@2854
|
172 |
|
paulson@2854
|
173 |
|
paulson@2854
|
174 |
(** Particular constants **)
|
paulson@2854
|
175 |
|
wenzelm@18525
|
176 |
fun negate P = Const (Data.not_name, []) $ P;
|
wenzelm@18525
|
177 |
|
wenzelm@18525
|
178 |
fun isNot (Const (c, _) $ _) = c = Data.not_name
|
wenzelm@18525
|
179 |
| isNot _ = false;
|
paulson@2854
|
180 |
|
wenzelm@18177
|
181 |
fun mkGoal P = Const ("*Goal*", []) $ P;
|
paulson@2854
|
182 |
|
wenzelm@18177
|
183 |
fun isGoal (Const ("*Goal*", _) $ _) = true
|
wenzelm@18525
|
184 |
| isGoal _ = false;
|
paulson@2854
|
185 |
|
wenzelm@18177
|
186 |
val TruepropC = ObjectLogic.judgment_name (the_context ());
|
wenzelm@18177
|
187 |
val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
|
paulson@18171
|
188 |
|
wenzelm@18177
|
189 |
fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
|
paulson@2854
|
190 |
|
wenzelm@18177
|
191 |
fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm
|
wenzelm@18177
|
192 |
| strip_Trueprop tm = tm;
|
wenzelm@18177
|
193 |
|
paulson@2854
|
194 |
|
paulson@2854
|
195 |
|
paulson@4065
|
196 |
(*** Dealing with overloaded constants ***)
|
paulson@2854
|
197 |
|
paulson@4065
|
198 |
(*alist is a map from TVar names to Vars. We need to unify the TVars
|
paulson@4065
|
199 |
faithfully in order to track overloading*)
|
wenzelm@18177
|
200 |
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts)
|
paulson@4065
|
201 |
| fromType alist (Term.TFree(a,_)) = Free a
|
paulson@4065
|
202 |
| fromType alist (Term.TVar (ixn,_)) =
|
wenzelm@18525
|
203 |
(case (AList.lookup (op =) (!alist) ixn) of
|
wenzelm@18525
|
204 |
NONE => let val t' = Var(ref NONE)
|
wenzelm@18525
|
205 |
in alist := (ixn, t') :: !alist; t'
|
wenzelm@18525
|
206 |
end
|
wenzelm@18525
|
207 |
| SOME v => v)
|
paulson@2854
|
208 |
|
wenzelm@24062
|
209 |
fun fromConst thy alist (a, T) =
|
wenzelm@24062
|
210 |
Const (a, map (fromType alist) (Sign.const_typargs thy (a, T)));
|
paulson@2854
|
211 |
|
paulson@2854
|
212 |
|
paulson@2854
|
213 |
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
|
wenzelm@18177
|
214 |
fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us)
|
paulson@2854
|
215 |
| (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*)
|
paulson@2854
|
216 |
| (Free a) aconv (Free b) = a=b
|
skalberg@15531
|
217 |
| (Var(ref(SOME t))) aconv u = t aconv u
|
skalberg@15531
|
218 |
| t aconv (Var(ref(SOME u))) = t aconv u
|
wenzelm@18525
|
219 |
| (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*)
|
paulson@2854
|
220 |
| (Bound i) aconv (Bound j) = i=j
|
paulson@2854
|
221 |
| (Abs(_,t)) aconv (Abs(_,u)) = t aconv u
|
paulson@2854
|
222 |
| (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
|
wenzelm@18177
|
223 |
| _ aconv _ = false
|
wenzelm@18177
|
224 |
and aconvs ([], []) = true
|
wenzelm@18177
|
225 |
| aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us)
|
wenzelm@18177
|
226 |
| aconvs _ = false;
|
paulson@2854
|
227 |
|
paulson@2854
|
228 |
|
paulson@2854
|
229 |
fun mem_term (_, []) = false
|
paulson@2854
|
230 |
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
|
paulson@2854
|
231 |
|
paulson@2854
|
232 |
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
|
paulson@2854
|
233 |
|
paulson@2854
|
234 |
fun mem_var (v: term option ref, []) = false
|
paulson@2854
|
235 |
| mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs);
|
paulson@2854
|
236 |
|
paulson@2854
|
237 |
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
|
paulson@2854
|
238 |
|
paulson@2854
|
239 |
|
paulson@2854
|
240 |
(** Vars **)
|
paulson@2854
|
241 |
|
paulson@2854
|
242 |
(*Accumulates the Vars in the term, suppressing duplicates*)
|
wenzelm@18525
|
243 |
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
|
wenzelm@18525
|
244 |
| add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars)
|
skalberg@15531
|
245 |
| add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars)
|
wenzelm@18525
|
246 |
| add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars)
|
wenzelm@18525
|
247 |
| add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars)
|
wenzelm@18525
|
248 |
| add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars))
|
wenzelm@18525
|
249 |
| add_term_vars (_, vars) = vars
|
paulson@2854
|
250 |
(*Term list version. [The fold functionals are slow]*)
|
paulson@2854
|
251 |
and add_terms_vars ([], vars) = vars
|
paulson@2854
|
252 |
| add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
|
paulson@2854
|
253 |
(*Var list version.*)
|
paulson@2854
|
254 |
and add_vars_vars ([], vars) = vars
|
wenzelm@18525
|
255 |
| add_vars_vars (ref (SOME u) :: vs, vars) =
|
wenzelm@18525
|
256 |
add_vars_vars (vs, add_term_vars(u,vars))
|
skalberg@15531
|
257 |
| add_vars_vars (v::vs, vars) = (*v must be a ref NONE*)
|
wenzelm@18525
|
258 |
add_vars_vars (vs, ins_var (v, vars));
|
paulson@2854
|
259 |
|
paulson@2854
|
260 |
|
paulson@2854
|
261 |
(*Chase assignments in "vars"; return a list of unassigned variables*)
|
paulson@2854
|
262 |
fun vars_in_vars vars = add_vars_vars(vars,[]);
|
paulson@2854
|
263 |
|
paulson@2854
|
264 |
|
paulson@2854
|
265 |
|
paulson@2854
|
266 |
(*increment a term's non-local bound variables
|
paulson@2854
|
267 |
inc is increment for bound variables
|
paulson@2854
|
268 |
lev is level at which a bound variable is considered 'loose'*)
|
wenzelm@18525
|
269 |
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
|
paulson@2854
|
270 |
| incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
|
paulson@2854
|
271 |
| incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
|
paulson@2854
|
272 |
| incr_bv (inc, lev, u) = u;
|
paulson@2854
|
273 |
|
paulson@2854
|
274 |
fun incr_boundvars 0 t = t
|
paulson@2854
|
275 |
| incr_boundvars inc t = incr_bv(inc,0,t);
|
paulson@2854
|
276 |
|
paulson@2854
|
277 |
|
paulson@2854
|
278 |
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
|
paulson@2854
|
279 |
(Bound 0) is loose at level 0 *)
|
wenzelm@18525
|
280 |
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js
|
haftmann@20854
|
281 |
else insert (op =) (i - lev) js
|
paulson@2854
|
282 |
| add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
|
paulson@2854
|
283 |
| add_loose_bnos (f$t, lev, js) =
|
wenzelm@18525
|
284 |
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
|
paulson@2854
|
285 |
| add_loose_bnos (_, _, js) = js;
|
paulson@2854
|
286 |
|
paulson@2854
|
287 |
fun loose_bnos t = add_loose_bnos (t, 0, []);
|
paulson@2854
|
288 |
|
wenzelm@18525
|
289 |
fun subst_bound (arg, t) : term =
|
paulson@2854
|
290 |
let fun subst (t as Bound i, lev) =
|
wenzelm@18525
|
291 |
if i<lev then t (*var is locally bound*)
|
wenzelm@18525
|
292 |
else if i=lev then incr_boundvars lev arg
|
wenzelm@18525
|
293 |
else Bound(i-1) (*loose: change it*)
|
wenzelm@18525
|
294 |
| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
|
wenzelm@18525
|
295 |
| subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
|
wenzelm@18525
|
296 |
| subst (t,lev) = t
|
paulson@2854
|
297 |
in subst (t,0) end;
|
paulson@2854
|
298 |
|
paulson@2854
|
299 |
|
paulson@3101
|
300 |
(*Normalize...but not the bodies of ABSTRACTIONS*)
|
paulson@2854
|
301 |
fun norm t = case t of
|
paulson@2952
|
302 |
Skolem (a,args) => Skolem(a, vars_in_vars args)
|
wenzelm@18177
|
303 |
| Const(a,ts) => Const(a, map norm ts)
|
skalberg@15531
|
304 |
| (Var (ref NONE)) => t
|
skalberg@15531
|
305 |
| (Var (ref (SOME u))) => norm u
|
paulson@2854
|
306 |
| (f $ u) => (case norm f of
|
paulson@3101
|
307 |
Abs(_,body) => norm (subst_bound (u, body))
|
paulson@3101
|
308 |
| nf => nf $ norm u)
|
paulson@2854
|
309 |
| _ => t;
|
paulson@2854
|
310 |
|
paulson@2854
|
311 |
|
paulson@2854
|
312 |
(*Weak (one-level) normalize for use in unification*)
|
paulson@2854
|
313 |
fun wkNormAux t = case t of
|
paulson@2854
|
314 |
(Var v) => (case !v of
|
wenzelm@18525
|
315 |
SOME u => wkNorm u
|
wenzelm@18525
|
316 |
| NONE => t)
|
paulson@2854
|
317 |
| (f $ u) => (case wkNormAux f of
|
wenzelm@18525
|
318 |
Abs(_,body) => wkNorm (subst_bound (u, body))
|
wenzelm@18525
|
319 |
| nf => nf $ u)
|
wenzelm@18525
|
320 |
| Abs (a,body) => (*eta-contract if possible*)
|
wenzelm@18525
|
321 |
(case wkNormAux body of
|
wenzelm@18525
|
322 |
nb as (f $ t) =>
|
wenzelm@20664
|
323 |
if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0
|
wenzelm@18525
|
324 |
then Abs(a,nb)
|
wenzelm@18525
|
325 |
else wkNorm (incr_boundvars ~1 f)
|
wenzelm@18525
|
326 |
| nb => Abs (a,nb))
|
paulson@2854
|
327 |
| _ => t
|
paulson@2854
|
328 |
and wkNorm t = case head_of t of
|
paulson@2854
|
329 |
Const _ => t
|
paulson@2854
|
330 |
| Skolem(a,args) => t
|
paulson@2854
|
331 |
| Free _ => t
|
paulson@2854
|
332 |
| _ => wkNormAux t;
|
paulson@2854
|
333 |
|
paulson@2854
|
334 |
|
wenzelm@18525
|
335 |
(*Does variable v occur in u? For unification.
|
paulson@5734
|
336 |
Dangling bound vars are also forbidden.*)
|
wenzelm@18525
|
337 |
fun varOccur v =
|
wenzelm@18525
|
338 |
let fun occL lev [] = false (*same as (exists occ), but faster*)
|
wenzelm@18525
|
339 |
| occL lev (u::us) = occ lev u orelse occL lev us
|
wenzelm@18525
|
340 |
and occ lev (Var w) =
|
wenzelm@18525
|
341 |
v=w orelse
|
skalberg@15531
|
342 |
(case !w of NONE => false
|
wenzelm@18525
|
343 |
| SOME u => occ lev u)
|
paulson@5734
|
344 |
| occ lev (Skolem(_,args)) = occL lev (map Var args)
|
wenzelm@18177
|
345 |
(*ignore Const, since term variables can't occur in types (?) *)
|
paulson@5734
|
346 |
| occ lev (Bound i) = lev <= i
|
paulson@5734
|
347 |
| occ lev (Abs(_,u)) = occ (lev+1) u
|
paulson@5734
|
348 |
| occ lev (f$u) = occ lev u orelse occ lev f
|
paulson@5734
|
349 |
| occ lev _ = false;
|
paulson@5734
|
350 |
in occ 0 end;
|
paulson@2854
|
351 |
|
paulson@2854
|
352 |
exception UNIFY;
|
paulson@2854
|
353 |
|
paulson@2854
|
354 |
|
paulson@2854
|
355 |
(*Restore the trail to some previous state: for backtracking*)
|
wenzelm@24062
|
356 |
fun clearTo (State {ntrail, trail, ...}) n =
|
paulson@3083
|
357 |
while !ntrail<>n do
|
wenzelm@18525
|
358 |
(hd(!trail) := NONE;
|
wenzelm@18525
|
359 |
trail := tl (!trail);
|
wenzelm@18525
|
360 |
ntrail := !ntrail - 1);
|
paulson@2854
|
361 |
|
paulson@2854
|
362 |
|
wenzelm@18525
|
363 |
(*First-order unification with bound variables.
|
paulson@2854
|
364 |
"vars" is a list of variables local to the rule and NOT to be put
|
wenzelm@18525
|
365 |
on the trail (no point in doing so)
|
paulson@2854
|
366 |
*)
|
wenzelm@24062
|
367 |
fun unify state (vars,t,u) =
|
wenzelm@24062
|
368 |
let val State {ntrail, trail, ...} = state
|
wenzelm@24062
|
369 |
val n = !ntrail
|
wenzelm@18525
|
370 |
fun update (t as Var v, u) =
|
wenzelm@18525
|
371 |
if t aconv u then ()
|
wenzelm@18525
|
372 |
else if varOccur v u then raise UNIFY
|
wenzelm@18525
|
373 |
else if mem_var(v, vars) then v := SOME u
|
wenzelm@18525
|
374 |
else (*avoid updating Vars in the branch if possible!*)
|
wenzelm@18525
|
375 |
if is_Var u andalso mem_var(dest_Var u, vars)
|
wenzelm@18525
|
376 |
then dest_Var u := SOME t
|
wenzelm@18525
|
377 |
else (v := SOME u;
|
wenzelm@18525
|
378 |
trail := v :: !trail; ntrail := !ntrail + 1)
|
wenzelm@18525
|
379 |
fun unifyAux (t,u) =
|
wenzelm@18525
|
380 |
case (wkNorm t, wkNorm u) of
|
wenzelm@18525
|
381 |
(nt as Var v, nu) => update(nt,nu)
|
wenzelm@18525
|
382 |
| (nu, nt as Var v) => update(nt,nu)
|
wenzelm@18525
|
383 |
| (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts)
|
wenzelm@18525
|
384 |
else raise UNIFY
|
wenzelm@18525
|
385 |
| (Abs(_,t'), Abs(_,u')) => unifyAux(t',u')
|
wenzelm@18525
|
386 |
(*NB: can yield unifiers having dangling Bound vars!*)
|
wenzelm@18525
|
387 |
| (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u'))
|
wenzelm@18525
|
388 |
| (nt, nu) => if nt aconv nu then () else raise UNIFY
|
wenzelm@18177
|
389 |
and unifysAux ([], []) = ()
|
wenzelm@18177
|
390 |
| unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us))
|
wenzelm@18177
|
391 |
| unifysAux _ = raise UNIFY;
|
wenzelm@24062
|
392 |
in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false)
|
paulson@2854
|
393 |
end;
|
paulson@2854
|
394 |
|
paulson@2854
|
395 |
|
paulson@16774
|
396 |
(*Convert from "real" terms to prototerms; eta-contract.
|
paulson@16774
|
397 |
Code is similar to fromSubgoal.*)
|
wenzelm@24062
|
398 |
fun fromTerm thy t =
|
paulson@4065
|
399 |
let val alistVar = ref []
|
paulson@4065
|
400 |
and alistTVar = ref []
|
wenzelm@24062
|
401 |
fun from (Term.Const aT) = fromConst thy alistTVar aT
|
wenzelm@18525
|
402 |
| from (Term.Free (a,_)) = Free a
|
wenzelm@18525
|
403 |
| from (Term.Bound i) = Bound i
|
wenzelm@18525
|
404 |
| from (Term.Var (ixn,T)) =
|
wenzelm@18525
|
405 |
(case (AList.lookup (op =) (!alistVar) ixn) of
|
wenzelm@18525
|
406 |
NONE => let val t' = Var(ref NONE)
|
wenzelm@18525
|
407 |
in alistVar := (ixn, t') :: !alistVar; t'
|
wenzelm@18525
|
408 |
end
|
wenzelm@18525
|
409 |
| SOME v => v)
|
wenzelm@18525
|
410 |
| from (Term.Abs (a,_,u)) =
|
wenzelm@18525
|
411 |
(case from u of
|
wenzelm@18525
|
412 |
u' as (f $ Bound 0) =>
|
wenzelm@20664
|
413 |
if member (op =) (loose_bnos f) 0 then Abs(a,u')
|
wenzelm@18525
|
414 |
else incr_boundvars ~1 f
|
wenzelm@18525
|
415 |
| u' => Abs(a,u'))
|
wenzelm@18525
|
416 |
| from (Term.$ (f,u)) = from f $ from u
|
paulson@2854
|
417 |
in from t end;
|
paulson@2854
|
418 |
|
paulson@4065
|
419 |
(*A debugging function: replaces all Vars by dummy Frees for visual inspection
|
paulson@4065
|
420 |
of whether they are distinct. Function revert undoes the assignments.*)
|
paulson@4065
|
421 |
fun instVars t =
|
wenzelm@12902
|
422 |
let val name = ref "a"
|
paulson@4065
|
423 |
val updated = ref []
|
wenzelm@18177
|
424 |
fun inst (Const(a,ts)) = List.app inst ts
|
wenzelm@18525
|
425 |
| inst (Var(v as ref NONE)) = (updated := v :: (!updated);
|
wenzelm@18525
|
426 |
v := SOME (Free ("?" ^ !name));
|
wenzelm@18525
|
427 |
name := Symbol.bump_string (!name))
|
wenzelm@18525
|
428 |
| inst (Abs(a,t)) = inst t
|
wenzelm@18525
|
429 |
| inst (f $ u) = (inst f; inst u)
|
wenzelm@18525
|
430 |
| inst _ = ()
|
skalberg@15570
|
431 |
fun revert() = List.app (fn v => v:=NONE) (!updated)
|
paulson@4065
|
432 |
in inst t; revert end;
|
paulson@4065
|
433 |
|
paulson@4065
|
434 |
|
paulson@2854
|
435 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
|
wenzelm@18177
|
436 |
fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
|
paulson@2854
|
437 |
| strip_imp_prems _ = [];
|
paulson@2854
|
438 |
|
paulson@2854
|
439 |
(* A1==>...An==>B goes to B, where B is not an implication *)
|
wenzelm@18177
|
440 |
fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
|
wenzelm@18177
|
441 |
| strip_imp_concl A = strip_Trueprop A;
|
wenzelm@18177
|
442 |
|
paulson@2854
|
443 |
|
paulson@2854
|
444 |
|
paulson@2854
|
445 |
(*** Conversion of Elimination Rules to Tableau Operations ***)
|
paulson@2854
|
446 |
|
paulson@9170
|
447 |
exception ElimBadConcl and ElimBadPrem;
|
paulson@9170
|
448 |
|
paulson@9170
|
449 |
(*The conclusion becomes the goal/negated assumption *False*: delete it!
|
wenzelm@18525
|
450 |
If we don't find it then the premise is ill-formed and could cause
|
paulson@9170
|
451 |
PROOF FAILED*)
|
paulson@9170
|
452 |
fun delete_concl [] = raise ElimBadPrem
|
wenzelm@18525
|
453 |
| delete_concl (P :: Ps) =
|
wenzelm@18525
|
454 |
(case P of
|
wenzelm@18525
|
455 |
Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) =>
|
wenzelm@18525
|
456 |
if c = "*Goal*" orelse c = Data.not_name then Ps
|
wenzelm@18525
|
457 |
else P :: delete_concl Ps
|
wenzelm@18525
|
458 |
| _ => P :: delete_concl Ps);
|
paulson@2854
|
459 |
|
wenzelm@18177
|
460 |
fun skoPrem vars (Const ("all", _) $ Abs (_, P)) =
|
paulson@2854
|
461 |
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
|
paulson@2854
|
462 |
| skoPrem vars P = P;
|
paulson@2854
|
463 |
|
wenzelm@18525
|
464 |
fun convertPrem t =
|
paulson@9170
|
465 |
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
|
paulson@2854
|
466 |
|
paulson@2854
|
467 |
(*Expects elimination rules to have a formula variable as conclusion*)
|
paulson@2854
|
468 |
fun convertRule vars t =
|
paulson@2854
|
469 |
let val (P::Ps) = strip_imp_prems t
|
paulson@2854
|
470 |
val Var v = strip_imp_concl t
|
wenzelm@18177
|
471 |
in v := SOME (Const ("*False*", []));
|
wenzelm@18525
|
472 |
(P, map (convertPrem o skoPrem vars) Ps)
|
paulson@9170
|
473 |
end
|
paulson@9170
|
474 |
handle Bind => raise ElimBadConcl;
|
paulson@2854
|
475 |
|
paulson@2854
|
476 |
|
paulson@2854
|
477 |
(*Like dup_elim, but puts the duplicated major premise FIRST*)
|
haftmann@17257
|
478 |
fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
|
paulson@2854
|
479 |
|
paulson@2854
|
480 |
|
paulson@4391
|
481 |
(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
|
paulson@4391
|
482 |
local
|
paulson@4391
|
483 |
(*Count new hyps so that they can be rotated*)
|
paulson@4391
|
484 |
fun nNewHyps [] = 0
|
wenzelm@18177
|
485 |
| nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps
|
paulson@4391
|
486 |
| nNewHyps (P::Ps) = 1 + nNewHyps Ps;
|
paulson@2854
|
487 |
|
paulson@5463
|
488 |
fun rot_tac [] i st = Seq.single st
|
paulson@4391
|
489 |
| rot_tac (0::ks) i st = rot_tac ks (i+1) st
|
paulson@4391
|
490 |
| rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
|
paulson@4391
|
491 |
in
|
paulson@4391
|
492 |
fun rot_subgoals_tac (rot, rl) =
|
wenzelm@18525
|
493 |
rot_tac (if rot then map nNewHyps rl else [])
|
paulson@4391
|
494 |
end;
|
paulson@4391
|
495 |
|
paulson@2854
|
496 |
|
wenzelm@26928
|
497 |
fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
|
paulson@2854
|
498 |
|
paulson@5343
|
499 |
(*Resolution/matching tactics: if upd then the proof state may be updated.
|
paulson@5343
|
500 |
Matching makes the tactics more deterministic in the presence of Vars.*)
|
paulson@5343
|
501 |
fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
|
paulson@5343
|
502 |
fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
|
paulson@5343
|
503 |
|
wenzelm@18525
|
504 |
(*Tableau rule from elimination rule.
|
paulson@5343
|
505 |
Flag "upd" says that the inference updated the branch.
|
paulson@5343
|
506 |
Flag "dup" requests duplication of the affected formula.*)
|
wenzelm@24062
|
507 |
fun fromRule thy vars rl =
|
wenzelm@24062
|
508 |
let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
|
wenzelm@18525
|
509 |
fun tac (upd, dup,rot) i =
|
wenzelm@18525
|
510 |
emtac upd (if dup then rev_dup_elim rl else rl) i
|
wenzelm@18525
|
511 |
THEN
|
wenzelm@18525
|
512 |
rot_subgoals_tac (rot, #2 trl) i
|
paulson@3244
|
513 |
in Option.SOME (trl, tac) end
|
paulson@9170
|
514 |
handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
|
wenzelm@26928
|
515 |
(warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
|
wenzelm@18525
|
516 |
Option.NONE)
|
paulson@9170
|
517 |
| ElimBadConcl => (*ignore: conclusion is not just a variable*)
|
wenzelm@18525
|
518 |
(if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
|
wenzelm@26928
|
519 |
"conclusion should be a variable\n" ^ Display.string_of_thm rl))
|
wenzelm@18525
|
520 |
else ();
|
wenzelm@18525
|
521 |
Option.NONE);
|
paulson@2854
|
522 |
|
paulson@2854
|
523 |
|
paulson@3101
|
524 |
(*** Conversion of Introduction Rules ***)
|
paulson@2854
|
525 |
|
paulson@2854
|
526 |
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
|
paulson@2854
|
527 |
|
paulson@2854
|
528 |
fun convertIntrRule vars t =
|
paulson@2854
|
529 |
let val Ps = strip_imp_prems t
|
paulson@2854
|
530 |
val P = strip_imp_concl t
|
wenzelm@18525
|
531 |
in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
|
paulson@2854
|
532 |
end;
|
paulson@2854
|
533 |
|
wenzelm@18525
|
534 |
(*Tableau rule from introduction rule.
|
paulson@5343
|
535 |
Flag "upd" says that the inference updated the branch.
|
paulson@5343
|
536 |
Flag "dup" requests duplication of the affected formula.
|
paulson@5343
|
537 |
Since haz rules are now delayed, "dup" is always FALSE for
|
paulson@5343
|
538 |
introduction rules.*)
|
wenzelm@24062
|
539 |
fun fromIntrRule thy vars rl =
|
wenzelm@24062
|
540 |
let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
|
wenzelm@18525
|
541 |
fun tac (upd,dup,rot) i =
|
wenzelm@18525
|
542 |
rmtac upd (if dup then Data.dup_intr rl else rl) i
|
wenzelm@18525
|
543 |
THEN
|
wenzelm@18525
|
544 |
rot_subgoals_tac (rot, #2 trl) i
|
paulson@2854
|
545 |
in (trl, tac) end;
|
paulson@2854
|
546 |
|
paulson@2854
|
547 |
|
paulson@3030
|
548 |
val dummyVar = Term.Var (("etc",0), dummyT);
|
paulson@2854
|
549 |
|
paulson@2854
|
550 |
(*Convert from prototerms to ordinary terms with dummy types
|
paulson@2924
|
551 |
Ignore abstractions; identify all Vars; STOP at given depth*)
|
paulson@2924
|
552 |
fun toTerm 0 _ = dummyVar
|
wenzelm@18177
|
553 |
| toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*)
|
paulson@2924
|
554 |
| toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
|
paulson@2924
|
555 |
| toTerm d (Free a) = Term.Free (a,dummyT)
|
paulson@2924
|
556 |
| toTerm d (Bound i) = Term.Bound i
|
paulson@2924
|
557 |
| toTerm d (Var _) = dummyVar
|
paulson@2924
|
558 |
| toTerm d (Abs(a,_)) = dummyVar
|
paulson@2924
|
559 |
| toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
|
paulson@2854
|
560 |
|
paulson@2854
|
561 |
|
wenzelm@24062
|
562 |
fun netMkRules thy P vars (nps: netpair list) =
|
paulson@2854
|
563 |
case P of
|
wenzelm@18177
|
564 |
(Const ("*Goal*", _) $ G) =>
|
wenzelm@18525
|
565 |
let val pG = mk_Trueprop (toTerm 2 G)
|
wenzelm@19482
|
566 |
val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
|
wenzelm@24062
|
567 |
in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end
|
paulson@2854
|
568 |
| _ =>
|
wenzelm@18525
|
569 |
let val pP = mk_Trueprop (toTerm 3 P)
|
wenzelm@19482
|
570 |
val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
|
wenzelm@24062
|
571 |
in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end;
|
paulson@2854
|
572 |
|
paulson@3092
|
573 |
|
paulson@3092
|
574 |
(*Normalize a branch--for tracing*)
|
paulson@3092
|
575 |
fun norm2 (G,md) = (norm G, md);
|
paulson@3092
|
576 |
|
paulson@3092
|
577 |
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
|
paulson@3092
|
578 |
|
paulson@5463
|
579 |
fun normBr {pairs, lits, vars, lim} =
|
wenzelm@18525
|
580 |
{pairs = map normLev pairs,
|
wenzelm@18525
|
581 |
lits = map norm lits,
|
wenzelm@18525
|
582 |
vars = vars,
|
paulson@5463
|
583 |
lim = lim};
|
paulson@3092
|
584 |
|
paulson@3092
|
585 |
|
paulson@4065
|
586 |
val dummyTVar = Term.TVar(("a",0), []);
|
paulson@3092
|
587 |
val dummyVar2 = Term.Var(("var",0), dummyT);
|
paulson@3092
|
588 |
|
wenzelm@26938
|
589 |
(*convert blast_tac's type representation to real types for tracing*)
|
paulson@4065
|
590 |
fun showType (Free a) = Term.TFree (a,[])
|
paulson@4065
|
591 |
| showType (Var _) = dummyTVar
|
paulson@4065
|
592 |
| showType t =
|
paulson@4065
|
593 |
(case strip_comb t of
|
wenzelm@18525
|
594 |
(Const (a, _), us) => Term.Type(a, map showType us)
|
wenzelm@18525
|
595 |
| _ => dummyT);
|
paulson@4065
|
596 |
|
paulson@4065
|
597 |
(*Display top-level overloading if any*)
|
wenzelm@18177
|
598 |
fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts))
|
wenzelm@18177
|
599 |
| topType thy (Abs(a,t)) = topType thy t
|
wenzelm@18177
|
600 |
| topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some)
|
wenzelm@18177
|
601 |
| topType _ _ = NONE;
|
paulson@4065
|
602 |
|
paulson@4065
|
603 |
|
paulson@3092
|
604 |
(*Convert from prototerms to ordinary terms with dummy types for tracing*)
|
wenzelm@18177
|
605 |
fun showTerm d (Const (a,_)) = Term.Const (a,dummyT)
|
paulson@3092
|
606 |
| showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
|
paulson@3092
|
607 |
| showTerm d (Free a) = Term.Free (a,dummyT)
|
paulson@3092
|
608 |
| showTerm d (Bound i) = Term.Bound i
|
skalberg@15531
|
609 |
| showTerm d (Var(ref(SOME u))) = showTerm d u
|
skalberg@15531
|
610 |
| showTerm d (Var(ref NONE)) = dummyVar2
|
paulson@3092
|
611 |
| showTerm d (Abs(a,t)) = if d=0 then dummyVar
|
wenzelm@18525
|
612 |
else Term.Abs(a, dummyT, showTerm (d-1) t)
|
paulson@3092
|
613 |
| showTerm d (f $ u) = if d=0 then dummyVar
|
wenzelm@18525
|
614 |
else Term.$ (showTerm d f, showTerm (d-1) u);
|
paulson@3092
|
615 |
|
wenzelm@26939
|
616 |
fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
|
paulson@3092
|
617 |
|
paulson@19037
|
618 |
(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like
|
paulson@19037
|
619 |
Ex(P) is duplicated as the assumption ~Ex(P). *)
|
paulson@19037
|
620 |
fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
|
paulson@19037
|
621 |
| negOfGoal G = G;
|
paulson@19037
|
622 |
|
paulson@19037
|
623 |
fun negOfGoal2 (G,md) = (negOfGoal G, md);
|
paulson@19037
|
624 |
|
paulson@19037
|
625 |
(*Converts all Goals to Nots in the safe parts of a branch. They could
|
paulson@19037
|
626 |
have been moved there from the literals list after substitution (equalSubst).
|
paulson@19037
|
627 |
There can be at most one--this function could be made more efficient.*)
|
paulson@19037
|
628 |
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
|
paulson@19037
|
629 |
|
paulson@19037
|
630 |
(*Tactic. Convert *Goal* to negated assumption in FIRST position*)
|
paulson@19037
|
631 |
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
|
paulson@19037
|
632 |
rotate_tac ~1 i;
|
paulson@19037
|
633 |
|
wenzelm@24062
|
634 |
fun traceTerm thy t =
|
paulson@19037
|
635 |
let val t' = norm (negOfGoal t)
|
wenzelm@24062
|
636 |
val stm = string_of thy 8 t'
|
wenzelm@18525
|
637 |
in
|
wenzelm@24062
|
638 |
case topType thy t' of
|
wenzelm@18525
|
639 |
NONE => stm (*no type to attach*)
|
wenzelm@26939
|
640 |
| SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
|
paulson@4065
|
641 |
end;
|
paulson@3092
|
642 |
|
paulson@3092
|
643 |
|
paulson@3092
|
644 |
(*Print tracing information at each iteration of prover*)
|
wenzelm@24062
|
645 |
fun tracing (State {thy, fullTrace, ...}) brs =
|
wenzelm@24062
|
646 |
let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G)
|
wenzelm@24062
|
647 |
| printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)")
|
wenzelm@18525
|
648 |
| printPairs _ = ()
|
paulson@5463
|
649 |
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
|
wenzelm@18525
|
650 |
(fullTrace := brs0 :: !fullTrace;
|
wenzelm@22580
|
651 |
List.app (fn _ => Output.immediate_output "+") brs;
|
wenzelm@22580
|
652 |
Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
|
wenzelm@18525
|
653 |
printPairs pairs;
|
wenzelm@18525
|
654 |
writeln"")
|
paulson@3092
|
655 |
in if !trace then printBrs (map normBr brs) else ()
|
paulson@3092
|
656 |
end;
|
paulson@3092
|
657 |
|
paulson@5343
|
658 |
fun traceMsg s = if !trace then writeln s else ();
|
paulson@4065
|
659 |
|
paulson@3092
|
660 |
(*Tracing: variables updated in the last branch operation?*)
|
wenzelm@24062
|
661 |
fun traceVars (State {thy, ntrail, trail, ...}) ntrl =
|
wenzelm@18525
|
662 |
if !trace then
|
paulson@4065
|
663 |
(case !ntrail-ntrl of
|
wenzelm@18525
|
664 |
0 => ()
|
wenzelm@22580
|
665 |
| 1 => Output.immediate_output"\t1 variable UPDATED:"
|
wenzelm@22580
|
666 |
| n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
|
paulson@4065
|
667 |
(*display the instantiations themselves, though no variable names*)
|
wenzelm@24062
|
668 |
List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v))))
|
paulson@4065
|
669 |
(List.take(!trail, !ntrail-ntrl));
|
paulson@4065
|
670 |
writeln"")
|
paulson@3092
|
671 |
else ();
|
paulson@3092
|
672 |
|
paulson@3092
|
673 |
(*Tracing: how many new branches are created?*)
|
paulson@3092
|
674 |
fun traceNew prems =
|
wenzelm@18525
|
675 |
if !trace then
|
paulson@3092
|
676 |
case length prems of
|
wenzelm@22580
|
677 |
0 => Output.immediate_output"branch closed by rule"
|
wenzelm@22580
|
678 |
| 1 => Output.immediate_output"branch extended (1 new subgoal)"
|
wenzelm@22580
|
679 |
| n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
|
paulson@3092
|
680 |
else ();
|
paulson@3092
|
681 |
|
paulson@3092
|
682 |
|
paulson@3092
|
683 |
|
paulson@2854
|
684 |
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
|
paulson@2854
|
685 |
|
wenzelm@18525
|
686 |
(*Replace the ATOMIC term "old" by "new" in t*)
|
paulson@2854
|
687 |
fun subst_atomic (old,new) t =
|
skalberg@15531
|
688 |
let fun subst (Var(ref(SOME u))) = subst u
|
wenzelm@18525
|
689 |
| subst (Abs(a,body)) = Abs(a, subst body)
|
wenzelm@18525
|
690 |
| subst (f$t) = subst f $ subst t
|
wenzelm@18525
|
691 |
| subst t = if t aconv old then new else t
|
paulson@2854
|
692 |
in subst t end;
|
paulson@2854
|
693 |
|
paulson@2854
|
694 |
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
|
wenzelm@18525
|
695 |
fun eta_contract_atom (t0 as Abs(a, body)) =
|
paulson@2854
|
696 |
(case eta_contract2 body of
|
wenzelm@20664
|
697 |
f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0
|
wenzelm@18525
|
698 |
else eta_contract_atom (incr_boundvars ~1 f)
|
paulson@2854
|
699 |
| _ => t0)
|
paulson@2854
|
700 |
| eta_contract_atom t = t
|
paulson@2854
|
701 |
and eta_contract2 (f$t) = f $ eta_contract_atom t
|
paulson@2854
|
702 |
| eta_contract2 t = eta_contract_atom t;
|
paulson@2854
|
703 |
|
paulson@2854
|
704 |
|
paulson@2854
|
705 |
(*When can we safely delete the equality?
|
paulson@2854
|
706 |
Not if it equates two constants; consider 0=1.
|
paulson@2854
|
707 |
Not if it resembles x=t[x], since substitution does not eliminate x.
|
paulson@2854
|
708 |
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
|
paulson@2854
|
709 |
Prefer to eliminate Bound variables if possible.
|
paulson@2854
|
710 |
Result: true = use as is, false = reorient first *)
|
paulson@2854
|
711 |
|
wenzelm@18525
|
712 |
(*Can t occur in u? For substitution.
|
paulson@4354
|
713 |
Does NOT examine the args of Skolem terms: substitution does not affect them.
|
paulson@4196
|
714 |
REFLEXIVE because hyp_subst_tac fails on x=x.*)
|
wenzelm@18525
|
715 |
fun substOccur t =
|
wenzelm@18525
|
716 |
let (*NO vars are permitted in u except the arguments of t, if it is
|
paulson@4354
|
717 |
a Skolem term. This ensures that no equations are deleted that could
|
paulson@4354
|
718 |
be instantiated to a cycle. For example, x=?a is rejected because ?a
|
wenzelm@18525
|
719 |
could be instantiated to Suc(x).*)
|
paulson@4354
|
720 |
val vars = case t of
|
paulson@4354
|
721 |
Skolem(_,vars) => vars
|
wenzelm@18525
|
722 |
| _ => []
|
paulson@4354
|
723 |
fun occEq u = (t aconv u) orelse occ u
|
skalberg@15531
|
724 |
and occ (Var(ref(SOME u))) = occEq u
|
paulson@4354
|
725 |
| occ (Var v) = not (mem_var (v, vars))
|
wenzelm@18525
|
726 |
| occ (Abs(_,u)) = occEq u
|
paulson@2854
|
727 |
| occ (f$u) = occEq u orelse occEq f
|
paulson@2854
|
728 |
| occ (_) = false;
|
paulson@2854
|
729 |
in occEq end;
|
paulson@2854
|
730 |
|
paulson@3092
|
731 |
exception DEST_EQ;
|
paulson@3092
|
732 |
|
wenzelm@18177
|
733 |
(*Take apart an equality. NO constant Trueprop*)
|
wenzelm@18525
|
734 |
fun dest_eq (Const (c, _) $ t $ u) =
|
wenzelm@18525
|
735 |
if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u)
|
wenzelm@18525
|
736 |
else raise DEST_EQ
|
wenzelm@18525
|
737 |
| dest_eq _ = raise DEST_EQ;
|
paulson@3092
|
738 |
|
paulson@4196
|
739 |
(*Reject the equality if u occurs in (or equals!) t*)
|
paulson@2854
|
740 |
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
|
paulson@2854
|
741 |
|
wenzelm@18525
|
742 |
(*IF the goal is an equality with a substitutable variable
|
paulson@2854
|
743 |
THEN orient that equality ELSE raise exception DEST_EQ*)
|
paulson@3092
|
744 |
fun orientGoal (t,u) = case (t,u) of
|
wenzelm@18525
|
745 |
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*)
|
wenzelm@18525
|
746 |
| (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*)
|
wenzelm@18525
|
747 |
| (Free _, _) => check(t,u,(t,u)) (*eliminates t*)
|
wenzelm@18525
|
748 |
| (_, Free _) => check(u,t,(u,t)) (*eliminates u*)
|
paulson@2854
|
749 |
| _ => raise DEST_EQ;
|
paulson@2854
|
750 |
|
paulson@2894
|
751 |
(*Substitute through the branch if an equality goal (else raise DEST_EQ).
|
paulson@2894
|
752 |
Moves affected literals back into the branch, but it is not clear where
|
paulson@4391
|
753 |
they should go: this could make proofs fail.*)
|
wenzelm@24062
|
754 |
fun equalSubst thy (G, {pairs, lits, vars, lim}) =
|
paulson@3092
|
755 |
let val (t,u) = orientGoal(dest_eq G)
|
paulson@3092
|
756 |
val subst = subst_atomic (t,u)
|
paulson@2854
|
757 |
fun subst2(G,md) = (subst G, md)
|
paulson@4466
|
758 |
(*substitute throughout list; extract affected formulae*)
|
paulson@4466
|
759 |
fun subForm ((G,md), (changed, pairs)) =
|
wenzelm@18525
|
760 |
let val nG = subst G
|
wenzelm@18525
|
761 |
in if nG aconv G then (changed, (G,md)::pairs)
|
wenzelm@18525
|
762 |
else ((nG,md)::changed, pairs)
|
paulson@2924
|
763 |
end
|
paulson@4466
|
764 |
(*substitute throughout "stack frame"; extract affected formulae*)
|
paulson@4466
|
765 |
fun subFrame ((Gs,Hs), (changed, frames)) =
|
wenzelm@30193
|
766 |
let val (changed', Gs') = List.foldr subForm (changed, []) Gs
|
wenzelm@30193
|
767 |
val (changed'', Hs') = List.foldr subForm (changed', []) Hs
|
paulson@4466
|
768 |
in (changed'', (Gs',Hs')::frames) end
|
paulson@4466
|
769 |
(*substitute throughout literals; extract affected ones*)
|
paulson@4466
|
770 |
fun subLit (lit, (changed, nlits)) =
|
wenzelm@18525
|
771 |
let val nlit = subst lit
|
wenzelm@18525
|
772 |
in if nlit aconv lit then (changed, nlit::nlits)
|
wenzelm@18525
|
773 |
else ((nlit,true)::changed, nlits)
|
paulson@2854
|
774 |
end
|
wenzelm@30193
|
775 |
val (changed, lits') = List.foldr subLit ([], []) lits
|
wenzelm@30193
|
776 |
val (changed', pairs') = List.foldr subFrame (changed, []) pairs
|
wenzelm@24062
|
777 |
in if !trace then writeln ("Substituting " ^ traceTerm thy u ^
|
wenzelm@24062
|
778 |
" for " ^ traceTerm thy t ^ " in branch" )
|
paulson@3092
|
779 |
else ();
|
wenzelm@18525
|
780 |
{pairs = (changed',[])::pairs', (*affected formulas, and others*)
|
wenzelm@18525
|
781 |
lits = lits', (*unaffected literals*)
|
wenzelm@18525
|
782 |
vars = vars,
|
paulson@5463
|
783 |
lim = lim}
|
paulson@2854
|
784 |
end;
|
paulson@2854
|
785 |
|
paulson@2854
|
786 |
|
paulson@2854
|
787 |
exception NEWBRANCHES and CLOSEF;
|
paulson@2854
|
788 |
|
paulson@2854
|
789 |
exception PROVE;
|
paulson@2854
|
790 |
|
paulson@4391
|
791 |
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
|
wenzelm@18525
|
792 |
val contr_tac = ematch_tac [Data.notE] THEN'
|
paulson@4391
|
793 |
(eq_assume_tac ORELSE' assume_tac);
|
paulson@2854
|
794 |
|
paulson@4391
|
795 |
val eContr_tac = TRACE Data.notE contr_tac;
|
paulson@2854
|
796 |
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
|
paulson@2854
|
797 |
|
wenzelm@18525
|
798 |
(*Try to unify complementary literals and return the corresponding tactic. *)
|
wenzelm@24062
|
799 |
fun tryClose state (G, L) =
|
wenzelm@18525
|
800 |
let
|
wenzelm@24062
|
801 |
fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
|
wenzelm@18525
|
802 |
fun arg (_ $ t) = t;
|
wenzelm@18525
|
803 |
in
|
wenzelm@18525
|
804 |
if isGoal G then close (arg G) L eAssume_tac
|
wenzelm@18525
|
805 |
else if isGoal L then close G (arg L) eAssume_tac
|
wenzelm@18525
|
806 |
else if isNot G then close (arg G) L eContr_tac
|
wenzelm@18525
|
807 |
else if isNot L then close G (arg L) eContr_tac
|
wenzelm@18525
|
808 |
else NONE
|
wenzelm@18525
|
809 |
end;
|
paulson@2854
|
810 |
|
paulson@2854
|
811 |
(*Were there Skolem terms in the premise? Must NOT chase Vars*)
|
paulson@2854
|
812 |
fun hasSkolem (Skolem _) = true
|
wenzelm@18525
|
813 |
| hasSkolem (Abs (_,body)) = hasSkolem body
|
paulson@2854
|
814 |
| hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
|
paulson@2854
|
815 |
| hasSkolem _ = false;
|
paulson@2854
|
816 |
|
paulson@2854
|
817 |
(*Attach the right "may duplicate" flag to new formulae: if they contain
|
paulson@2854
|
818 |
Skolem terms then allow duplication.*)
|
paulson@2854
|
819 |
fun joinMd md [] = []
|
paulson@2854
|
820 |
| joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
|
paulson@2854
|
821 |
|
paulson@2854
|
822 |
|
paulson@2854
|
823 |
(** Backtracking and Pruning **)
|
paulson@2854
|
824 |
|
paulson@2854
|
825 |
(*clashVar vars (n,trail) determines whether any of the last n elements
|
paulson@2854
|
826 |
of "trail" occur in "vars" OR in their instantiations*)
|
paulson@2854
|
827 |
fun clashVar [] = (fn _ => false)
|
paulson@2854
|
828 |
| clashVar vars =
|
paulson@2854
|
829 |
let fun clash (0, _) = false
|
wenzelm@18525
|
830 |
| clash (_, []) = false
|
wenzelm@18525
|
831 |
| clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
|
paulson@2854
|
832 |
in clash end;
|
paulson@2854
|
833 |
|
paulson@2854
|
834 |
|
paulson@2854
|
835 |
(*nbrs = # of branches just prior to closing this one. Delete choice points
|
paulson@2854
|
836 |
for goals proved by the latest inference, provided NO variables in the
|
paulson@2854
|
837 |
next branch have been updated.*)
|
wenzelm@24062
|
838 |
fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
|
wenzelm@18525
|
839 |
backtracking over bad proofs*)
|
wenzelm@24062
|
840 |
| prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) =
|
paulson@2854
|
841 |
let fun traceIt last =
|
wenzelm@18525
|
842 |
let val ll = length last
|
wenzelm@18525
|
843 |
and lc = length choices
|
wenzelm@18525
|
844 |
in if !trace andalso ll<lc then
|
wenzelm@18525
|
845 |
(writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
|
wenzelm@18525
|
846 |
last)
|
wenzelm@18525
|
847 |
else last
|
wenzelm@18525
|
848 |
end
|
wenzelm@18525
|
849 |
fun pruneAux (last, _, _, []) = last
|
wenzelm@18525
|
850 |
| pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
|
wenzelm@18525
|
851 |
if nbrs' < nbrs
|
wenzelm@18525
|
852 |
then last (*don't backtrack beyond first solution of goal*)
|
wenzelm@18525
|
853 |
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
|
wenzelm@18525
|
854 |
else (* nbrs'=nbrs *)
|
wenzelm@18525
|
855 |
if clashVar nxtVars (ntrl-ntrl', trl) then last
|
wenzelm@18525
|
856 |
else (*no clashes: can go back at least this far!*)
|
wenzelm@18525
|
857 |
pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
|
wenzelm@18525
|
858 |
choices)
|
paulson@2854
|
859 |
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end;
|
paulson@2854
|
860 |
|
paulson@5463
|
861 |
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
|
paulson@5463
|
862 |
| nextVars [] = [];
|
paulson@2854
|
863 |
|
wenzelm@18525
|
864 |
fun backtrack (choices as (ntrl, nbrs, exn)::_) =
|
wenzelm@18525
|
865 |
(if !trace then (writeln ("Backtracking; now there are " ^
|
wenzelm@18525
|
866 |
Int.toString nbrs ^ " branches"))
|
wenzelm@18525
|
867 |
else ();
|
paulson@3083
|
868 |
raise exn)
|
paulson@3083
|
869 |
| backtrack _ = raise PROVE;
|
paulson@2854
|
870 |
|
paulson@2894
|
871 |
(*Add the literal G, handling *Goal* and detecting duplicates.*)
|
wenzelm@18525
|
872 |
fun addLit (Const ("*Goal*", _) $ G, lits) =
|
paulson@2894
|
873 |
(*New literal is a *Goal*, so change all other Goals to Nots*)
|
wenzelm@18177
|
874 |
let fun bad (Const ("*Goal*", _) $ _) = true
|
wenzelm@18525
|
875 |
| bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G'
|
wenzelm@18525
|
876 |
| bad _ = false;
|
wenzelm@18525
|
877 |
fun change [] = []
|
wenzelm@18525
|
878 |
| change (lit :: lits) =
|
wenzelm@18525
|
879 |
(case lit of
|
wenzelm@18525
|
880 |
Const (c, _) $ G' =>
|
wenzelm@18525
|
881 |
if c = "*Goal*" orelse c = Data.not_name then
|
wenzelm@18525
|
882 |
if G aconv G' then change lits
|
wenzelm@18525
|
883 |
else negate G' :: change lits
|
wenzelm@18525
|
884 |
else lit :: change lits
|
wenzelm@18525
|
885 |
| _ => lit :: change lits)
|
paulson@2854
|
886 |
in
|
wenzelm@18525
|
887 |
Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits)
|
paulson@2854
|
888 |
end
|
paulson@2854
|
889 |
| addLit (G,lits) = ins_term(G, lits)
|
paulson@2854
|
890 |
|
paulson@2854
|
891 |
|
paulson@2952
|
892 |
(*For calculating the "penalty" to assess on a branching factor of n
|
paulson@2952
|
893 |
log2 seems a little too severe*)
|
paulson@3083
|
894 |
fun log n = if n<4 then 0 else 1 + log(n div 4);
|
paulson@2924
|
895 |
|
paulson@2924
|
896 |
|
paulson@3021
|
897 |
(*match(t,u) says whether the term u might be an instance of the pattern t
|
paulson@3021
|
898 |
Used to detect "recursive" rules such as transitivity*)
|
paulson@3021
|
899 |
fun match (Var _) u = true
|
wenzelm@18525
|
900 |
| match (Const (a,tas)) (Const (b,tbs)) =
|
wenzelm@18525
|
901 |
a = "*Goal*" andalso b = Data.not_name orelse
|
wenzelm@18525
|
902 |
a = Data.not_name andalso b = "*Goal*" orelse
|
wenzelm@18525
|
903 |
a = b andalso matchs tas tbs
|
paulson@4065
|
904 |
| match (Free a) (Free b) = (a=b)
|
paulson@4065
|
905 |
| match (Bound i) (Bound j) = (i=j)
|
paulson@4065
|
906 |
| match (Abs(_,t)) (Abs(_,u)) = match t u
|
paulson@4065
|
907 |
| match (f$t) (g$u) = match f g andalso match t u
|
wenzelm@18177
|
908 |
| match t u = false
|
wenzelm@18177
|
909 |
and matchs [] [] = true
|
wenzelm@18177
|
910 |
| matchs (t :: ts) (u :: us) = match t u andalso matchs ts us;
|
paulson@3021
|
911 |
|
paulson@3021
|
912 |
|
wenzelm@24062
|
913 |
fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
|
paulson@4323
|
914 |
if b then
|
wenzelm@30187
|
915 |
writeln (#message (end_timing start) ^ " for search. Closed: "
|
wenzelm@18525
|
916 |
^ Int.toString (!nclosed) ^
|
paulson@4391
|
917 |
" tried: " ^ Int.toString (!ntried) ^
|
paulson@4391
|
918 |
" tactics: " ^ Int.toString (length tacs))
|
paulson@4323
|
919 |
else ();
|
paulson@4323
|
920 |
|
paulson@4323
|
921 |
|
wenzelm@18525
|
922 |
(*Tableau prover based on leanTaP. Argument is a list of branches. Each
|
wenzelm@18525
|
923 |
branch contains a list of unexpanded formulae, a list of literals, and a
|
paulson@4391
|
924 |
bound on unsafe expansions.
|
paulson@4391
|
925 |
"start" is CPU time at start, for printing search time
|
paulson@4391
|
926 |
*)
|
wenzelm@24062
|
927 |
fun prove (state, start, cs, brs, cont) =
|
wenzelm@24062
|
928 |
let val State {thy, ntrail, nclosed, ntried, ...} = state;
|
wenzelm@24062
|
929 |
val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
|
paulson@2854
|
930 |
val safeList = [safe0_netpair, safep_netpair]
|
paulson@2854
|
931 |
and hazList = [haz_netpair]
|
wenzelm@18525
|
932 |
fun prv (tacs, trs, choices, []) =
|
wenzelm@24062
|
933 |
(printStats state (!trace orelse !stats, start, tacs);
|
wenzelm@18525
|
934 |
cont (tacs, trs, choices)) (*all branches closed!*)
|
wenzelm@18525
|
935 |
| prv (tacs, trs, choices,
|
wenzelm@18525
|
936 |
brs0 as {pairs = ((G,md)::br, haz)::pairs,
|
wenzelm@18525
|
937 |
lits, vars, lim} :: brs) =
|
wenzelm@18525
|
938 |
(*apply a safe rule only (possibly allowing instantiation);
|
paulson@3917
|
939 |
defer any haz formulae*)
|
wenzelm@18525
|
940 |
let exception PRV (*backtrack to precisely this recursion!*)
|
wenzelm@18525
|
941 |
val ntrl = !ntrail
|
wenzelm@18525
|
942 |
val nbrs = length brs0
|
paulson@2854
|
943 |
val nxtVars = nextVars brs
|
wenzelm@18525
|
944 |
val G = norm G
|
wenzelm@24062
|
945 |
val rules = netMkRules thy G vars safeList
|
wenzelm@18525
|
946 |
(*Make a new branch, decrementing "lim" if instantiations occur*)
|
wenzelm@18525
|
947 |
fun newBr (vars',lim') prems =
|
wenzelm@18525
|
948 |
map (fn prem =>
|
wenzelm@18525
|
949 |
if (exists isGoal prem)
|
wenzelm@18525
|
950 |
then {pairs = ((joinMd md prem, []) ::
|
wenzelm@18525
|
951 |
negOfGoals ((br, haz)::pairs)),
|
wenzelm@18525
|
952 |
lits = map negOfGoal lits,
|
wenzelm@18525
|
953 |
vars = vars',
|
wenzelm@18525
|
954 |
lim = lim'}
|
wenzelm@18525
|
955 |
else {pairs = ((joinMd md prem, []) ::
|
wenzelm@18525
|
956 |
(br, haz) :: pairs),
|
wenzelm@18525
|
957 |
lits = lits,
|
wenzelm@18525
|
958 |
vars = vars',
|
wenzelm@18525
|
959 |
lim = lim'})
|
wenzelm@18525
|
960 |
prems @
|
wenzelm@18525
|
961 |
brs
|
wenzelm@18525
|
962 |
(*Seek a matching rule. If unifiable then add new premises
|
paulson@2854
|
963 |
to branch.*)
|
wenzelm@18525
|
964 |
fun deeper [] = raise NEWBRANCHES
|
wenzelm@18525
|
965 |
| deeper (((P,prems),tac)::grls) =
|
wenzelm@24062
|
966 |
if unify state (add_term_vars(P,[]), P, G)
|
wenzelm@18525
|
967 |
then (*P comes from the rule; G comes from the branch.*)
|
wenzelm@18525
|
968 |
let val updated = ntrl < !ntrail (*branch updated*)
|
wenzelm@18525
|
969 |
val lim' = if updated
|
wenzelm@18525
|
970 |
then lim - (1+log(length rules))
|
wenzelm@18525
|
971 |
else lim (*discourage branching updates*)
|
wenzelm@18525
|
972 |
val vars = vars_in_vars vars
|
wenzelm@30193
|
973 |
val vars' = List.foldr add_terms_vars vars prems
|
wenzelm@18525
|
974 |
val choices' = (ntrl, nbrs, PRV) :: choices
|
wenzelm@18525
|
975 |
val tacs' = (tac(updated,false,true))
|
paulson@5343
|
976 |
:: tacs (*no duplication; rotate*)
|
wenzelm@18525
|
977 |
in
|
wenzelm@24062
|
978 |
traceNew prems; traceVars state ntrl;
|
wenzelm@18525
|
979 |
(if null prems then (*closed the branch: prune!*)
|
wenzelm@18525
|
980 |
(nclosed := !nclosed + 1;
|
wenzelm@18525
|
981 |
prv(tacs', brs0::trs,
|
wenzelm@24062
|
982 |
prune state (nbrs, nxtVars, choices'),
|
wenzelm@18525
|
983 |
brs))
|
wenzelm@18525
|
984 |
else (*prems non-null*)
|
wenzelm@18525
|
985 |
if lim'<0 (*faster to kill ALL the alternatives*)
|
wenzelm@18525
|
986 |
then (traceMsg"Excessive branching: KILLED";
|
wenzelm@24062
|
987 |
clearTo state ntrl; raise NEWBRANCHES)
|
wenzelm@18525
|
988 |
else
|
wenzelm@18525
|
989 |
(ntried := !ntried + length prems - 1;
|
wenzelm@18525
|
990 |
prv(tacs', brs0::trs, choices',
|
wenzelm@18525
|
991 |
newBr (vars',lim') prems)))
|
wenzelm@18525
|
992 |
handle PRV =>
|
wenzelm@18525
|
993 |
if updated then
|
wenzelm@18525
|
994 |
(*Backtrack at this level.
|
wenzelm@18525
|
995 |
Reset Vars and try another rule*)
|
wenzelm@24062
|
996 |
(clearTo state ntrl; deeper grls)
|
wenzelm@18525
|
997 |
else (*backtrack to previous level*)
|
wenzelm@18525
|
998 |
backtrack choices
|
wenzelm@18525
|
999 |
end
|
wenzelm@18525
|
1000 |
else deeper grls
|
wenzelm@18525
|
1001 |
(*Try to close branch by unifying with head goal*)
|
wenzelm@18525
|
1002 |
fun closeF [] = raise CLOSEF
|
wenzelm@18525
|
1003 |
| closeF (L::Ls) =
|
wenzelm@24062
|
1004 |
case tryClose state (G,L) of
|
wenzelm@18525
|
1005 |
NONE => closeF Ls
|
wenzelm@18525
|
1006 |
| SOME tac =>
|
wenzelm@18525
|
1007 |
let val choices' =
|
wenzelm@22580
|
1008 |
(if !trace then (Output.immediate_output"branch closed";
|
wenzelm@24062
|
1009 |
traceVars state ntrl)
|
wenzelm@18525
|
1010 |
else ();
|
wenzelm@24062
|
1011 |
prune state (nbrs, nxtVars,
|
wenzelm@18525
|
1012 |
(ntrl, nbrs, PRV) :: choices))
|
wenzelm@18525
|
1013 |
in nclosed := !nclosed + 1;
|
wenzelm@18525
|
1014 |
prv (tac::tacs, brs0::trs, choices', brs)
|
wenzelm@18525
|
1015 |
handle PRV =>
|
wenzelm@18525
|
1016 |
(*reset Vars and try another literal
|
wenzelm@18525
|
1017 |
[this handler is pruned if possible!]*)
|
wenzelm@24062
|
1018 |
(clearTo state ntrl; closeF Ls)
|
wenzelm@18525
|
1019 |
end
|
wenzelm@18525
|
1020 |
(*Try to unify a queued formula (safe or haz) with head goal*)
|
wenzelm@18525
|
1021 |
fun closeFl [] = raise CLOSEF
|
wenzelm@18525
|
1022 |
| closeFl ((br, haz)::pairs) =
|
wenzelm@18525
|
1023 |
closeF (map fst br)
|
wenzelm@18525
|
1024 |
handle CLOSEF => closeF (map fst haz)
|
wenzelm@18525
|
1025 |
handle CLOSEF => closeFl pairs
|
wenzelm@24062
|
1026 |
in tracing state brs0;
|
wenzelm@18525
|
1027 |
if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
|
wenzelm@18525
|
1028 |
else
|
wenzelm@23908
|
1029 |
prv (Data.hyp_subst_tac (!trace) :: tacs,
|
wenzelm@18525
|
1030 |
brs0::trs, choices,
|
wenzelm@24062
|
1031 |
equalSubst thy
|
wenzelm@18525
|
1032 |
(G, {pairs = (br,haz)::pairs,
|
wenzelm@18525
|
1033 |
lits = lits, vars = vars, lim = lim})
|
wenzelm@18525
|
1034 |
:: brs)
|
wenzelm@18525
|
1035 |
handle DEST_EQ => closeF lits
|
wenzelm@18525
|
1036 |
handle CLOSEF => closeFl ((br,haz)::pairs)
|
wenzelm@18525
|
1037 |
handle CLOSEF => deeper rules
|
wenzelm@18525
|
1038 |
handle NEWBRANCHES =>
|
wenzelm@24062
|
1039 |
(case netMkRules thy G vars hazList of
|
wenzelm@18525
|
1040 |
[] => (*there are no plausible haz rules*)
|
wenzelm@18525
|
1041 |
(traceMsg "moving formula to literals";
|
wenzelm@18525
|
1042 |
prv (tacs, brs0::trs, choices,
|
wenzelm@18525
|
1043 |
{pairs = (br,haz)::pairs,
|
wenzelm@18525
|
1044 |
lits = addLit(G,lits),
|
wenzelm@18525
|
1045 |
vars = vars,
|
wenzelm@18525
|
1046 |
lim = lim} :: brs))
|
wenzelm@18525
|
1047 |
| _ => (*G admits some haz rules: try later*)
|
wenzelm@18525
|
1048 |
(traceMsg "moving formula to haz list";
|
wenzelm@18525
|
1049 |
prv (if isGoal G then negOfGoal_tac :: tacs
|
wenzelm@18525
|
1050 |
else tacs,
|
wenzelm@18525
|
1051 |
brs0::trs,
|
wenzelm@18525
|
1052 |
choices,
|
wenzelm@18525
|
1053 |
{pairs = (br, haz@[(negOfGoal G, md)])::pairs,
|
wenzelm@18525
|
1054 |
lits = lits,
|
wenzelm@18525
|
1055 |
vars = vars,
|
wenzelm@18525
|
1056 |
lim = lim} :: brs)))
|
wenzelm@18525
|
1057 |
end
|
wenzelm@18525
|
1058 |
| prv (tacs, trs, choices,
|
wenzelm@18525
|
1059 |
{pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
|
wenzelm@18525
|
1060 |
(*no more "safe" formulae: transfer haz down a level*)
|
wenzelm@18525
|
1061 |
prv (tacs, trs, choices,
|
wenzelm@18525
|
1062 |
{pairs = (Gs,haz@haz')::pairs,
|
wenzelm@18525
|
1063 |
lits = lits,
|
wenzelm@18525
|
1064 |
vars = vars,
|
wenzelm@18525
|
1065 |
lim = lim} :: brs)
|
wenzelm@18525
|
1066 |
| prv (tacs, trs, choices,
|
wenzelm@18525
|
1067 |
brs0 as {pairs = [([], (H,md)::Hs)],
|
wenzelm@18525
|
1068 |
lits, vars, lim} :: brs) =
|
wenzelm@18525
|
1069 |
(*no safe steps possible at any level: apply a haz rule*)
|
wenzelm@18525
|
1070 |
let exception PRV (*backtrack to precisely this recursion!*)
|
wenzelm@18525
|
1071 |
val H = norm H
|
wenzelm@18525
|
1072 |
val ntrl = !ntrail
|
wenzelm@24062
|
1073 |
val rules = netMkRules thy H vars hazList
|
wenzelm@18525
|
1074 |
(*new premises of haz rules may NOT be duplicated*)
|
wenzelm@18525
|
1075 |
fun newPrem (vars,P,dup,lim') prem =
|
wenzelm@18525
|
1076 |
let val Gs' = map (fn Q => (Q,false)) prem
|
wenzelm@18525
|
1077 |
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
|
wenzelm@18525
|
1078 |
and lits' = if (exists isGoal prem)
|
wenzelm@18525
|
1079 |
then map negOfGoal lits
|
wenzelm@18525
|
1080 |
else lits
|
wenzelm@18525
|
1081 |
in {pairs = if exists (match P) prem then [(Gs',Hs')]
|
wenzelm@18525
|
1082 |
(*Recursive in this premise. Don't make new
|
wenzelm@18525
|
1083 |
"stack frame". New haz premises will end up
|
wenzelm@18525
|
1084 |
at the BACK of the queue, preventing
|
wenzelm@18525
|
1085 |
exclusion of others*)
|
wenzelm@18525
|
1086 |
else [(Gs',[]), ([],Hs')],
|
wenzelm@18525
|
1087 |
lits = lits',
|
wenzelm@18525
|
1088 |
vars = vars,
|
wenzelm@18525
|
1089 |
lim = lim'}
|
wenzelm@18525
|
1090 |
end
|
wenzelm@18525
|
1091 |
fun newBr x prems = map (newPrem x) prems @ brs
|
wenzelm@18525
|
1092 |
(*Seek a matching rule. If unifiable then add new premises
|
paulson@2854
|
1093 |
to branch.*)
|
wenzelm@18525
|
1094 |
fun deeper [] = raise NEWBRANCHES
|
wenzelm@18525
|
1095 |
| deeper (((P,prems),tac)::grls) =
|
wenzelm@24062
|
1096 |
if unify state (add_term_vars(P,[]), P, H)
|
wenzelm@18525
|
1097 |
then
|
wenzelm@18525
|
1098 |
let val updated = ntrl < !ntrail (*branch updated*)
|
wenzelm@18525
|
1099 |
val vars = vars_in_vars vars
|
wenzelm@30193
|
1100 |
val vars' = List.foldr add_terms_vars vars prems
|
wenzelm@18525
|
1101 |
(*duplicate H if md permits*)
|
wenzelm@18525
|
1102 |
val dup = md (*earlier had "andalso vars' <> vars":
|
paulson@11152
|
1103 |
duplicate only if the subgoal has new vars*)
|
wenzelm@18525
|
1104 |
(*any instances of P in the subgoals?
|
wenzelm@18525
|
1105 |
NB: boolean "recur" affects tracing only!*)
|
wenzelm@18525
|
1106 |
and recur = exists (exists (match P)) prems
|
wenzelm@18525
|
1107 |
val lim' = (*Decrement "lim" extra if updates occur*)
|
wenzelm@18525
|
1108 |
if updated then lim - (1+log(length rules))
|
wenzelm@18525
|
1109 |
else lim-1
|
wenzelm@18525
|
1110 |
(*It is tempting to leave "lim" UNCHANGED if
|
wenzelm@18525
|
1111 |
both dup and recur are false. Proofs are
|
wenzelm@18525
|
1112 |
found at shallower depths, but looping
|
wenzelm@18525
|
1113 |
occurs too often...*)
|
wenzelm@18525
|
1114 |
val mayUndo =
|
wenzelm@18525
|
1115 |
(*Allowing backtracking from a rule application
|
wenzelm@18525
|
1116 |
if other matching rules exist, if the rule
|
wenzelm@18525
|
1117 |
updated variables, or if the rule did not
|
wenzelm@18525
|
1118 |
introduce new variables. This latter condition
|
wenzelm@18525
|
1119 |
means it is not a standard "gamma-rule" but
|
wenzelm@18525
|
1120 |
some other form of unsafe rule. Aim is to
|
wenzelm@18525
|
1121 |
emulate Fast_tac, which allows all unsafe steps
|
wenzelm@18525
|
1122 |
to be undone.*)
|
wenzelm@18525
|
1123 |
not(null grls) (*other rules to try?*)
|
wenzelm@18525
|
1124 |
orelse updated
|
wenzelm@18525
|
1125 |
orelse vars=vars' (*no new Vars?*)
|
wenzelm@18525
|
1126 |
val tac' = tac(updated, dup, true)
|
wenzelm@18525
|
1127 |
(*if recur then perhaps shouldn't call rotate_tac: new
|
paulson@5463
|
1128 |
formulae should be last, but that's WRONG if the new
|
paulson@5463
|
1129 |
formulae are Goals, since they remain in the first
|
paulson@5463
|
1130 |
position*)
|
paulson@5463
|
1131 |
|
wenzelm@18525
|
1132 |
in
|
wenzelm@18525
|
1133 |
if lim'<0 andalso not (null prems)
|
wenzelm@18525
|
1134 |
then (*it's faster to kill ALL the alternatives*)
|
wenzelm@18525
|
1135 |
(traceMsg"Excessive branching: KILLED";
|
wenzelm@24062
|
1136 |
clearTo state ntrl; raise NEWBRANCHES)
|
wenzelm@18525
|
1137 |
else
|
wenzelm@18525
|
1138 |
traceNew prems;
|
wenzelm@22580
|
1139 |
if !trace andalso dup then Output.immediate_output" (duplicating)"
|
wenzelm@18525
|
1140 |
else ();
|
wenzelm@22580
|
1141 |
if !trace andalso recur then Output.immediate_output" (recursive)"
|
wenzelm@18525
|
1142 |
else ();
|
wenzelm@24062
|
1143 |
traceVars state ntrl;
|
wenzelm@18525
|
1144 |
if null prems then nclosed := !nclosed + 1
|
wenzelm@18525
|
1145 |
else ntried := !ntried + length prems - 1;
|
wenzelm@18525
|
1146 |
prv(tac' :: tacs,
|
wenzelm@18525
|
1147 |
brs0::trs,
|
wenzelm@18525
|
1148 |
(ntrl, length brs0, PRV) :: choices,
|
wenzelm@18525
|
1149 |
newBr (vars', P, dup, lim') prems)
|
wenzelm@18525
|
1150 |
handle PRV =>
|
wenzelm@18525
|
1151 |
if mayUndo
|
wenzelm@18525
|
1152 |
then (*reset Vars and try another rule*)
|
wenzelm@24062
|
1153 |
(clearTo state ntrl; deeper grls)
|
wenzelm@18525
|
1154 |
else (*backtrack to previous level*)
|
wenzelm@18525
|
1155 |
backtrack choices
|
wenzelm@18525
|
1156 |
end
|
wenzelm@18525
|
1157 |
else deeper grls
|
wenzelm@24062
|
1158 |
in tracing state brs0;
|
wenzelm@18525
|
1159 |
if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
|
wenzelm@18525
|
1160 |
else deeper rules
|
wenzelm@18525
|
1161 |
handle NEWBRANCHES =>
|
wenzelm@18525
|
1162 |
(*cannot close branch: move H to literals*)
|
wenzelm@18525
|
1163 |
prv (tacs, brs0::trs, choices,
|
wenzelm@18525
|
1164 |
{pairs = [([], Hs)],
|
wenzelm@18525
|
1165 |
lits = H::lits,
|
wenzelm@18525
|
1166 |
vars = vars,
|
wenzelm@18525
|
1167 |
lim = lim} :: brs)
|
wenzelm@18525
|
1168 |
end
|
paulson@2854
|
1169 |
| prv (tacs, trs, choices, _ :: brs) = backtrack choices
|
wenzelm@12346
|
1170 |
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
|
paulson@2854
|
1171 |
|
paulson@2854
|
1172 |
|
paulson@2883
|
1173 |
(*Construct an initial branch.*)
|
wenzelm@18525
|
1174 |
fun initBranch (ts,lim) =
|
paulson@5463
|
1175 |
{pairs = [(map (fn t => (t,true)) ts, [])],
|
wenzelm@18525
|
1176 |
lits = [],
|
wenzelm@18525
|
1177 |
vars = add_terms_vars (ts,[]),
|
paulson@5463
|
1178 |
lim = lim};
|
paulson@2854
|
1179 |
|
paulson@2854
|
1180 |
|
paulson@2854
|
1181 |
(*** Conversion & Skolemization of the Isabelle proof state ***)
|
paulson@2854
|
1182 |
|
paulson@2854
|
1183 |
(*Make a list of all the parameters in a subgoal, even if nested*)
|
wenzelm@18525
|
1184 |
local open Term
|
paulson@2854
|
1185 |
in
|
paulson@2854
|
1186 |
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
|
paulson@2854
|
1187 |
| discard_foralls t = t;
|
paulson@2854
|
1188 |
end;
|
paulson@2854
|
1189 |
|
paulson@2854
|
1190 |
(*List of variables not appearing as arguments to the given parameter*)
|
paulson@2854
|
1191 |
fun getVars [] i = []
|
wenzelm@20664
|
1192 |
| getVars ((_,(v,is))::alist) (i: int) =
|
wenzelm@20664
|
1193 |
if member (op =) is i then getVars alist i
|
wenzelm@18525
|
1194 |
else v :: getVars alist i;
|
paulson@2854
|
1195 |
|
paulson@4233
|
1196 |
exception TRANS of string;
|
paulson@2854
|
1197 |
|
paulson@4233
|
1198 |
(*Translation of a subgoal: Skolemize all parameters*)
|
wenzelm@24062
|
1199 |
fun fromSubgoal thy t =
|
paulson@4065
|
1200 |
let val alistVar = ref []
|
paulson@4065
|
1201 |
and alistTVar = ref []
|
paulson@2854
|
1202 |
fun hdvar ((ix,(v,is))::_) = v
|
paulson@2854
|
1203 |
fun from lev t =
|
wenzelm@18525
|
1204 |
let val (ht,ts) = Term.strip_comb t
|
wenzelm@18525
|
1205 |
fun apply u = list_comb (u, map (from lev) ts)
|
wenzelm@18525
|
1206 |
fun bounds [] = []
|
wenzelm@18525
|
1207 |
| bounds (Term.Bound i::ts) =
|
wenzelm@18525
|
1208 |
if i<lev then raise TRANS
|
wenzelm@18525
|
1209 |
"Function unknown's argument not a parameter"
|
wenzelm@18525
|
1210 |
else i-lev :: bounds ts
|
wenzelm@18525
|
1211 |
| bounds ts = raise TRANS
|
wenzelm@18525
|
1212 |
"Function unknown's argument not a bound variable"
|
paulson@2854
|
1213 |
in
|
wenzelm@18525
|
1214 |
case ht of
|
wenzelm@24062
|
1215 |
Term.Const aT => apply (fromConst thy alistTVar aT)
|
wenzelm@18525
|
1216 |
| Term.Free (a,_) => apply (Free a)
|
wenzelm@18525
|
1217 |
| Term.Bound i => apply (Bound i)
|
wenzelm@18525
|
1218 |
| Term.Var (ix,_) =>
|
wenzelm@18525
|
1219 |
(case (AList.lookup (op =) (!alistVar) ix) of
|
wenzelm@18525
|
1220 |
NONE => (alistVar := (ix, (ref NONE, bounds ts))
|
wenzelm@18525
|
1221 |
:: !alistVar;
|
wenzelm@18525
|
1222 |
Var (hdvar(!alistVar)))
|
wenzelm@18525
|
1223 |
| SOME(v,is) => if is=bounds ts then Var v
|
wenzelm@18525
|
1224 |
else raise TRANS
|
wenzelm@18525
|
1225 |
("Discrepancy among occurrences of "
|
wenzelm@22678
|
1226 |
^ Term.string_of_vname ix))
|
wenzelm@18525
|
1227 |
| Term.Abs (a,_,body) =>
|
wenzelm@18525
|
1228 |
if null ts then Abs(a, from (lev+1) body)
|
wenzelm@18525
|
1229 |
else raise TRANS "argument not in normal form"
|
paulson@2854
|
1230 |
end
|
paulson@2854
|
1231 |
|
paulson@2854
|
1232 |
val npars = length (Logic.strip_params t)
|
paulson@2854
|
1233 |
|
paulson@2854
|
1234 |
(*Skolemize a subgoal from a proof state*)
|
paulson@2854
|
1235 |
fun skoSubgoal i t =
|
wenzelm@18525
|
1236 |
if i<npars then
|
wenzelm@18525
|
1237 |
skoSubgoal (i+1)
|
wenzelm@18525
|
1238 |
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
|
wenzelm@18525
|
1239 |
t))
|
wenzelm@18525
|
1240 |
else t
|
paulson@2854
|
1241 |
|
paulson@2854
|
1242 |
in skoSubgoal 0 (from 0 (discard_foralls t)) end;
|
paulson@2854
|
1243 |
|
paulson@2854
|
1244 |
|
wenzelm@18525
|
1245 |
(*Tactic using tableau engine and proof reconstruction.
|
paulson@4391
|
1246 |
"start" is CPU time at start, for printing SEARCH time
|
wenzelm@18525
|
1247 |
(also prints reconstruction time)
|
paulson@2854
|
1248 |
"lim" is depth limit.*)
|
wenzelm@24062
|
1249 |
fun timing_depth_tac start cs lim i st0 =
|
wenzelm@24062
|
1250 |
let val thy = Thm.theory_of_thm st0
|
wenzelm@24062
|
1251 |
val state = initialize thy
|
wenzelm@24062
|
1252 |
val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
|
wenzelm@24062
|
1253 |
val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
|
paulson@4323
|
1254 |
val hyps = strip_imp_prems skoprem
|
paulson@4323
|
1255 |
and concl = strip_imp_concl skoprem
|
wenzelm@18525
|
1256 |
fun cont (tacs,_,choices) =
|
wenzelm@21295
|
1257 |
let val start = start_timing ()
|
wenzelm@18525
|
1258 |
in
|
wenzelm@18525
|
1259 |
case Seq.pull(EVERY' (rev tacs) i st) of
|
wenzelm@18525
|
1260 |
NONE => (writeln ("PROOF FAILED for depth " ^
|
wenzelm@18525
|
1261 |
Int.toString lim);
|
wenzelm@18525
|
1262 |
if !trace then error "************************\n"
|
wenzelm@18525
|
1263 |
else ();
|
wenzelm@18525
|
1264 |
backtrack choices)
|
wenzelm@18525
|
1265 |
| cell => (if (!trace orelse !stats)
|
wenzelm@30187
|
1266 |
then writeln (#message (end_timing start) ^ " for reconstruction")
|
wenzelm@18525
|
1267 |
else ();
|
wenzelm@18525
|
1268 |
Seq.make(fn()=> cell))
|
paulson@4323
|
1269 |
end
|
wenzelm@24062
|
1270 |
in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end
|
wenzelm@24062
|
1271 |
handle PROVE => Seq.empty
|
paulson@2854
|
1272 |
|
paulson@4391
|
1273 |
(*Public version with fixed depth*)
|
wenzelm@21295
|
1274 |
fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
|
paulson@4391
|
1275 |
|
wenzelm@24112
|
1276 |
val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
|
webertj@15162
|
1277 |
|
wenzelm@18525
|
1278 |
fun blast_tac cs i st =
|
wenzelm@24112
|
1279 |
((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
|
wenzelm@24099
|
1280 |
(timing_depth_tac (start_timing ()) cs) 0) i
|
paulson@5463
|
1281 |
THEN flexflex_tac) st
|
paulson@14466
|
1282 |
handle TRANS s =>
|
wenzelm@18525
|
1283 |
((if !trace then warning ("blast: " ^ s) else ());
|
paulson@14466
|
1284 |
Seq.empty);
|
paulson@2854
|
1285 |
|
wenzelm@4078
|
1286 |
fun Blast_tac i = blast_tac (Data.claset()) i;
|
paulson@2854
|
1287 |
|
paulson@2924
|
1288 |
|
wenzelm@18525
|
1289 |
(*** For debugging: these apply the prover to a subgoal and return
|
paulson@2924
|
1290 |
the resulting tactics, trace, etc. ***)
|
paulson@2924
|
1291 |
|
wenzelm@24062
|
1292 |
val fullTrace = ref ([]: branch list list);
|
paulson@2924
|
1293 |
|
paulson@2924
|
1294 |
(*Read a string to make an initial, singleton branch*)
|
wenzelm@25365
|
1295 |
fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
|
paulson@2924
|
1296 |
|
wenzelm@18525
|
1297 |
fun tryInThy thy lim s =
|
wenzelm@24062
|
1298 |
let
|
wenzelm@24062
|
1299 |
val state as State {fullTrace = ft, ...} = initialize thy;
|
wenzelm@24062
|
1300 |
val res = timeap prove
|
wenzelm@24062
|
1301 |
(state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
|
wenzelm@24062
|
1302 |
val _ = fullTrace := !ft;
|
wenzelm@24062
|
1303 |
in res end;
|
paulson@2924
|
1304 |
|
paulson@2924
|
1305 |
|
wenzelm@5926
|
1306 |
(** method setup **)
|
wenzelm@5926
|
1307 |
|
wenzelm@24099
|
1308 |
val blast_method =
|
wenzelm@27809
|
1309 |
Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
|
wenzelm@24099
|
1310 |
(fn NONE => Data.cla_meth' blast_tac
|
wenzelm@24099
|
1311 |
| SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
|
wenzelm@7155
|
1312 |
|
wenzelm@18525
|
1313 |
val setup =
|
wenzelm@24099
|
1314 |
setup_depth_limit #>
|
wenzelm@24099
|
1315 |
Method.add_methods [("blast", blast_method, "tableau prover")];
|
wenzelm@5926
|
1316 |
|
paulson@2854
|
1317 |
end;
|