2894
|
1 |
(* Title: Provers/blast
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
Generic tableau prover with proof reconstruction
|
|
7 |
|
2854
|
8 |
SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
|
2894
|
9 |
Needs explicit instantiation of assumptions?
|
|
10 |
|
|
11 |
|
|
12 |
Limitations compared with fast_tac:
|
|
13 |
* ignores addss, addbefore, addafter; this restriction is intrinsic
|
|
14 |
* seems to loop given transitivity and similar rules
|
|
15 |
* ignores elimination rules that don't have the correct format
|
|
16 |
(conclusion must be a formula variable)
|
|
17 |
* ignores types, which can make HOL proofs fail
|
|
18 |
|
|
19 |
Known problems:
|
|
20 |
With hyp_subst_tac:
|
|
21 |
1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter
|
|
22 |
as the argument of a function variable
|
|
23 |
2. When a literal is affected, it is moved back to the active formulae.
|
|
24 |
But there's no way of putting it in the right place.
|
|
25 |
3. Affected haz formulae should also be moved, but they are not.
|
2854
|
26 |
|
|
27 |
*)
|
|
28 |
|
|
29 |
|
|
30 |
(*Should be a type abbreviation?*)
|
|
31 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
|
|
32 |
|
|
33 |
|
|
34 |
(*Assumptions about constants:
|
|
35 |
--The negation symbol is "Not"
|
|
36 |
--The equality symbol is "op ="
|
|
37 |
--The is-true judgement symbol is "Trueprop"
|
|
38 |
--There are no constants named "*Goal* or "*False*"
|
|
39 |
*)
|
|
40 |
signature BLAST_DATA =
|
|
41 |
sig
|
|
42 |
type claset
|
|
43 |
val notE : thm (* [| ~P; P |] ==> R *)
|
|
44 |
val ccontr : thm
|
|
45 |
val contr_tac : int -> tactic
|
|
46 |
val dup_intr : thm -> thm
|
|
47 |
val vars_gen_hyp_subst_tac : bool -> int -> tactic
|
|
48 |
val claset : claset ref
|
|
49 |
val rep_claset :
|
|
50 |
claset -> {safeIs: thm list, safeEs: thm list,
|
|
51 |
hazIs: thm list, hazEs: thm list,
|
|
52 |
uwrapper: (int -> tactic) -> (int -> tactic),
|
|
53 |
swrapper: (int -> tactic) -> (int -> tactic),
|
|
54 |
safe0_netpair: netpair, safep_netpair: netpair,
|
|
55 |
haz_netpair: netpair, dup_netpair: netpair}
|
|
56 |
end;
|
|
57 |
|
|
58 |
|
|
59 |
signature BLAST =
|
|
60 |
sig
|
|
61 |
type claset
|
2883
|
62 |
val depth_tac : claset -> int -> int -> tactic
|
|
63 |
val blast_tac : claset -> int -> tactic
|
|
64 |
val Blast_tac : int -> tactic
|
|
65 |
val declConsts : string list * thm list -> unit
|
2854
|
66 |
end;
|
|
67 |
|
|
68 |
|
2883
|
69 |
functor BlastFun(Data: BLAST_DATA) =
|
2854
|
70 |
struct
|
|
71 |
|
|
72 |
type claset = Data.claset;
|
|
73 |
|
|
74 |
val trace = ref false;
|
|
75 |
|
|
76 |
datatype term =
|
|
77 |
Const of string
|
|
78 |
| OConst of string * int
|
|
79 |
| Skolem of string * term option ref list
|
|
80 |
| Free of string
|
|
81 |
| Var of term option ref
|
|
82 |
| Bound of int
|
|
83 |
| Abs of string*term
|
|
84 |
| op $ of term*term;
|
|
85 |
|
|
86 |
|
|
87 |
exception DEST_EQ;
|
|
88 |
|
|
89 |
(*Take apart an equality (plain or overloaded). NO constant Trueprop*)
|
|
90 |
fun dest_eq (Const "op =" $ t $ u) = (t,u)
|
|
91 |
| dest_eq (OConst("op =",_) $ t $ u) = (t,u)
|
|
92 |
| dest_eq _ = raise DEST_EQ;
|
|
93 |
|
|
94 |
(** Basic syntactic operations **)
|
|
95 |
|
|
96 |
fun is_Var (Var _) = true
|
|
97 |
| is_Var _ = false;
|
|
98 |
|
|
99 |
fun dest_Var (Var x) = x;
|
|
100 |
|
|
101 |
|
|
102 |
fun rand (f$x) = x;
|
|
103 |
|
|
104 |
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
|
|
105 |
val list_comb : term * term list -> term = foldl (op $);
|
|
106 |
|
|
107 |
|
|
108 |
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
|
|
109 |
fun strip_comb u : term * term list =
|
|
110 |
let fun stripc (f$t, ts) = stripc (f, t::ts)
|
|
111 |
| stripc x = x
|
|
112 |
in stripc(u,[]) end;
|
|
113 |
|
|
114 |
|
|
115 |
(* maps f(t1,...,tn) to f , which is never a combination *)
|
|
116 |
fun head_of (f$t) = head_of f
|
|
117 |
| head_of u = u;
|
|
118 |
|
|
119 |
|
|
120 |
(** Particular constants **)
|
|
121 |
|
|
122 |
fun negate P = Const"Not" $ P;
|
|
123 |
|
|
124 |
fun mkGoal P = Const"*Goal*" $ P;
|
|
125 |
|
|
126 |
fun isGoal (Const"*Goal*" $ _) = true
|
|
127 |
| isGoal _ = false;
|
|
128 |
|
|
129 |
val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT);
|
|
130 |
fun mk_tprop P = Term.$ (Trueprop, P);
|
|
131 |
|
|
132 |
fun isTrueprop (Term.Const("Trueprop",_)) = true
|
|
133 |
| isTrueprop _ = false;
|
|
134 |
|
|
135 |
|
|
136 |
(** Dealing with overloaded constants **)
|
|
137 |
|
|
138 |
(*Result is a symbol table, indexed by names of overloaded constants.
|
|
139 |
Each constant maps to a list of (pattern,Blast.Const) pairs.
|
|
140 |
Any Term.Const that matches a pattern gets replaced by the Blast.Const.
|
|
141 |
*)
|
|
142 |
fun addConsts (t as Term.Const(a,_), tab) =
|
|
143 |
(case Symtab.lookup (tab,a) of
|
|
144 |
None => tab (*ignore: not a constant that we are looking for*)
|
|
145 |
| Some patList =>
|
|
146 |
(case gen_assoc (op aconv) (patList, t) of
|
|
147 |
None => Symtab.update
|
|
148 |
((a, (t, OConst (a, length patList)) :: patList),
|
|
149 |
tab)
|
|
150 |
| _ => tab))
|
|
151 |
| addConsts (Term.Abs(_,_,body), tab) = addConsts (body, tab)
|
|
152 |
| addConsts (Term.$ (t,u), tab) = addConsts (t, addConsts (u, tab))
|
|
153 |
| addConsts (_, tab) = tab (*ignore others*);
|
|
154 |
|
|
155 |
|
|
156 |
fun addRules (rls,tab) = foldr addConsts (map (#prop o rep_thm) rls, tab);
|
|
157 |
|
2883
|
158 |
fun declConst (a,tab) =
|
|
159 |
case Symtab.lookup (tab,a) of
|
|
160 |
None => Symtab.update((a,[]), tab) (*create a brand new entry*)
|
|
161 |
| Some _ => tab (*preserve old entry*);
|
2854
|
162 |
|
|
163 |
(*maps the name of each overloaded constant to a list of archetypal constants,
|
|
164 |
which may be polymorphic.*)
|
|
165 |
local
|
|
166 |
val overLoadTab = ref (Symtab.null : (Term.term * term) list Symtab.table)
|
|
167 |
(*The alists in this table should only be increased*)
|
|
168 |
in
|
|
169 |
|
|
170 |
fun declConsts (names, rls) =
|
|
171 |
overLoadTab := addRules (rls, foldr declConst (names, !overLoadTab));
|
|
172 |
|
|
173 |
|
|
174 |
(*Convert a possibly overloaded Term.Const to a Blast.Const*)
|
|
175 |
fun fromConst tsig (t as Term.Const (a,_)) =
|
|
176 |
let fun find [] = Const a
|
|
177 |
| find ((pat,t')::patList) =
|
|
178 |
if Pattern.matches tsig (pat,t) then t'
|
|
179 |
else find patList
|
|
180 |
in case Symtab.lookup(!overLoadTab, a) of
|
|
181 |
None => Const a
|
|
182 |
| Some patList => find patList
|
|
183 |
end;
|
|
184 |
end;
|
|
185 |
|
|
186 |
|
|
187 |
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
|
|
188 |
fun (Const a) aconv (Const b) = a=b
|
|
189 |
| (OConst ai) aconv (OConst bj) = ai=bj
|
|
190 |
| (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*)
|
|
191 |
| (Free a) aconv (Free b) = a=b
|
|
192 |
| (Var(ref(Some t))) aconv u = t aconv u
|
|
193 |
| t aconv (Var(ref(Some u))) = t aconv u
|
|
194 |
| (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*)
|
|
195 |
| (Bound i) aconv (Bound j) = i=j
|
|
196 |
| (Abs(_,t)) aconv (Abs(_,u)) = t aconv u
|
|
197 |
| (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
|
|
198 |
| _ aconv _ = false;
|
|
199 |
|
|
200 |
|
|
201 |
fun mem_term (_, []) = false
|
|
202 |
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
|
|
203 |
|
|
204 |
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
|
|
205 |
|
|
206 |
fun mem_var (v: term option ref, []) = false
|
|
207 |
| mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs);
|
|
208 |
|
|
209 |
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
|
|
210 |
|
|
211 |
|
|
212 |
(** Vars **)
|
|
213 |
|
|
214 |
(*Accumulates the Vars in the term, suppressing duplicates*)
|
|
215 |
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
|
|
216 |
| add_term_vars (Var (v as ref None), vars) = ins_var (v, vars)
|
|
217 |
| add_term_vars (Var (ref (Some u)), vars) = add_term_vars(u,vars)
|
|
218 |
| add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars)
|
|
219 |
| add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars))
|
|
220 |
| add_term_vars (_, vars) = vars
|
|
221 |
(*Term list version. [The fold functionals are slow]*)
|
|
222 |
and add_terms_vars ([], vars) = vars
|
|
223 |
| add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
|
|
224 |
(*Var list version.*)
|
|
225 |
and add_vars_vars ([], vars) = vars
|
|
226 |
| add_vars_vars (ref (Some u) :: vs, vars) =
|
|
227 |
add_vars_vars (vs, add_term_vars(u,vars))
|
|
228 |
| add_vars_vars (v::vs, vars) = (*v must be a ref None*)
|
|
229 |
add_vars_vars (vs, ins_var (v, vars));
|
|
230 |
|
|
231 |
|
|
232 |
(*Chase assignments in "vars"; return a list of unassigned variables*)
|
|
233 |
fun vars_in_vars vars = add_vars_vars(vars,[]);
|
|
234 |
|
|
235 |
|
|
236 |
|
|
237 |
(*increment a term's non-local bound variables
|
|
238 |
inc is increment for bound variables
|
|
239 |
lev is level at which a bound variable is considered 'loose'*)
|
|
240 |
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
|
|
241 |
| incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
|
|
242 |
| incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
|
|
243 |
| incr_bv (inc, lev, u) = u;
|
|
244 |
|
|
245 |
fun incr_boundvars 0 t = t
|
|
246 |
| incr_boundvars inc t = incr_bv(inc,0,t);
|
|
247 |
|
|
248 |
|
|
249 |
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
|
|
250 |
(Bound 0) is loose at level 0 *)
|
|
251 |
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js
|
|
252 |
else (i-lev) ins_int js
|
|
253 |
| add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
|
|
254 |
| add_loose_bnos (f$t, lev, js) =
|
|
255 |
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
|
|
256 |
| add_loose_bnos (_, _, js) = js;
|
|
257 |
|
|
258 |
fun loose_bnos t = add_loose_bnos (t, 0, []);
|
|
259 |
|
|
260 |
fun subst_bound (arg, t) : term =
|
|
261 |
let fun subst (t as Bound i, lev) =
|
|
262 |
if i<lev then t (*var is locally bound*)
|
|
263 |
else if i=lev then incr_boundvars lev arg
|
|
264 |
else Bound(i-1) (*loose: change it*)
|
|
265 |
| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
|
|
266 |
| subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
|
|
267 |
| subst (t,lev) = t
|
|
268 |
in subst (t,0) end;
|
|
269 |
|
|
270 |
|
|
271 |
(*Normalize...but not the bodies of ABSTRACTIONS*)
|
|
272 |
fun norm t = case t of
|
|
273 |
Skolem(a,args) => Skolem(a, vars_in_vars args)
|
|
274 |
| (Var (ref None)) => t
|
|
275 |
| (Var (ref (Some u))) => norm u
|
|
276 |
| (f $ u) => (case norm f of
|
|
277 |
Abs(_,body) => norm (subst_bound (u, body))
|
|
278 |
| nf => nf $ norm u)
|
|
279 |
| _ => t;
|
|
280 |
|
|
281 |
|
|
282 |
(*Weak (one-level) normalize for use in unification*)
|
|
283 |
fun wkNormAux t = case t of
|
|
284 |
(Var v) => (case !v of
|
|
285 |
Some u => wkNorm u
|
|
286 |
| None => t)
|
|
287 |
| (f $ u) => (case wkNormAux f of
|
|
288 |
Abs(_,body) => wkNorm (subst_bound (u, body))
|
|
289 |
| nf => nf $ u)
|
|
290 |
| _ => t
|
|
291 |
and wkNorm t = case head_of t of
|
|
292 |
Const _ => t
|
|
293 |
| OConst _ => t
|
|
294 |
| Skolem(a,args) => t
|
|
295 |
| Free _ => t
|
|
296 |
| _ => wkNormAux t;
|
|
297 |
|
|
298 |
|
|
299 |
(*Does variable v occur in u? For unification.*)
|
|
300 |
fun varOccur v =
|
|
301 |
let fun occL [] = false (*same as (exists occ), but faster*)
|
|
302 |
| occL (u::us) = occ u orelse occL us
|
|
303 |
and occ (Var w) =
|
|
304 |
v=w orelse
|
|
305 |
(case !w of None => false
|
|
306 |
| Some u => occ u)
|
|
307 |
| occ (Skolem(_,args)) = occL (map Var args)
|
|
308 |
| occ (Abs(_,u)) = occ u
|
|
309 |
| occ (f$u) = occ u orelse occ f
|
|
310 |
| occ (_) = false;
|
|
311 |
in occ end;
|
|
312 |
|
|
313 |
exception UNIFY;
|
|
314 |
|
|
315 |
val trail = ref [] : term option ref list ref;
|
|
316 |
val ntrail = ref 0;
|
|
317 |
|
|
318 |
|
|
319 |
(*Restore the trail to some previous state: for backtracking*)
|
|
320 |
fun clearTo n =
|
|
321 |
while !ntrail>n do
|
|
322 |
(hd(!trail) := None;
|
|
323 |
trail := tl (!trail);
|
|
324 |
ntrail := !ntrail - 1);
|
|
325 |
|
|
326 |
|
|
327 |
(*First-order unification with bound variables.
|
|
328 |
"vars" is a list of variables local to the rule and NOT to be put
|
|
329 |
on the trail (no point in doing so)
|
|
330 |
*)
|
|
331 |
fun unify(vars,t,u) =
|
|
332 |
let val n = !ntrail
|
|
333 |
fun update (t as Var v, u) =
|
|
334 |
if t aconv u then ()
|
|
335 |
else if varOccur v u then raise UNIFY
|
|
336 |
else if mem_var(v, vars) then v := Some u
|
|
337 |
else (*avoid updating Vars in the branch if possible!*)
|
|
338 |
if is_Var u andalso mem_var(dest_Var u, vars)
|
|
339 |
then dest_Var u := Some t
|
|
340 |
else (v := Some u;
|
|
341 |
trail := v :: !trail; ntrail := !ntrail + 1)
|
|
342 |
fun unifyAux (t,u) =
|
|
343 |
case (wkNorm t, wkNorm u) of
|
|
344 |
(nt as Var v, nu) => update(nt,nu)
|
|
345 |
| (nu, nt as Var v) => update(nt,nu)
|
|
346 |
| (Abs(_,t'), Abs(_,u')) => unifyAux(t',u')
|
|
347 |
(*NB: can yield unifiers having dangling Bound vars!*)
|
|
348 |
| (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u'))
|
|
349 |
| (nt, nu) => if nt aconv nu then () else raise UNIFY
|
|
350 |
in unifyAux(t,u) handle UNIFY => (clearTo n; raise UNIFY)
|
|
351 |
end;
|
|
352 |
|
|
353 |
|
|
354 |
(*Convert from "real" terms to prototerms; eta-contract*)
|
|
355 |
fun fromTerm tsig t =
|
|
356 |
let val alist = ref []
|
|
357 |
fun from (t as Term.Const _) = fromConst tsig t
|
|
358 |
| from (Term.Free (a,_)) = Free a
|
|
359 |
| from (Term.Bound i) = Bound i
|
|
360 |
| from (Term.Var (ixn,T)) =
|
|
361 |
(case (assoc_string_int(!alist,ixn)) of
|
|
362 |
None => let val t' = Var(ref None)
|
|
363 |
in alist := (ixn, (t', T)) :: !alist; t'
|
|
364 |
end
|
|
365 |
| Some (v,_) => v)
|
|
366 |
| from (Term.Abs (a,_,u)) =
|
|
367 |
(case from u of
|
|
368 |
u' as (f $ Bound 0) =>
|
|
369 |
if (0 mem_int loose_bnos f) then Abs(a,u')
|
|
370 |
else incr_boundvars ~1 f
|
|
371 |
| u' => Abs(a,u'))
|
|
372 |
| from (Term.$ (f,u)) = from f $ from u
|
|
373 |
in from t end;
|
|
374 |
|
|
375 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
|
|
376 |
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) =
|
|
377 |
A :: strip_imp_prems B
|
|
378 |
| strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B
|
|
379 |
| strip_imp_prems _ = [];
|
|
380 |
|
|
381 |
(* A1==>...An==>B goes to B, where B is not an implication *)
|
|
382 |
fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B
|
|
383 |
| strip_imp_concl (Const"Trueprop" $ A) = A
|
|
384 |
| strip_imp_concl A = A : term;
|
|
385 |
|
|
386 |
|
|
387 |
(*** Conversion of Elimination Rules to Tableau Operations ***)
|
|
388 |
|
|
389 |
(*The conclusion becomes the goal/negated assumption *False*: delete it!*)
|
|
390 |
fun squash_nots [] = []
|
|
391 |
| squash_nots (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
|
|
392 |
squash_nots Ps
|
|
393 |
| squash_nots (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
|
|
394 |
squash_nots Ps
|
|
395 |
| squash_nots (P::Ps) = P :: squash_nots Ps;
|
|
396 |
|
|
397 |
fun skoPrem vars (Const "all" $ Abs (_, P)) =
|
|
398 |
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
|
|
399 |
| skoPrem vars P = P;
|
|
400 |
|
|
401 |
fun convertPrem t =
|
|
402 |
squash_nots (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
|
|
403 |
|
|
404 |
(*Expects elimination rules to have a formula variable as conclusion*)
|
|
405 |
fun convertRule vars t =
|
|
406 |
let val (P::Ps) = strip_imp_prems t
|
|
407 |
val Var v = strip_imp_concl t
|
|
408 |
in v := Some (Const"*False*");
|
|
409 |
(P, map (convertPrem o skoPrem vars) Ps)
|
|
410 |
end;
|
|
411 |
|
|
412 |
|
|
413 |
(*Like dup_elim, but puts the duplicated major premise FIRST*)
|
|
414 |
fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd;
|
|
415 |
|
|
416 |
|
|
417 |
(*Count new hyps so that they can be rotated*)
|
|
418 |
fun nNewHyps [] = 0
|
|
419 |
| nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
|
|
420 |
| nNewHyps (P::Ps) = 1 + nNewHyps Ps;
|
|
421 |
|
|
422 |
fun rot_subgoals_tac [] i st = Sequence.single st
|
|
423 |
| rot_subgoals_tac (k::ks) i st =
|
|
424 |
rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
|
|
425 |
handle OPTION _ => Sequence.null;
|
|
426 |
|
|
427 |
fun TRACE rl tac st = if !trace then (prth rl; tac st) else tac st;
|
|
428 |
|
|
429 |
(*Tableau rule from elimination rule. Flag "dup" requests duplication of the
|
|
430 |
affected formula.*)
|
|
431 |
fun fromRule vars rl =
|
|
432 |
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
|
|
433 |
val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertRule vars
|
|
434 |
fun tac dup i =
|
|
435 |
TRACE rl
|
|
436 |
(DETERM (etac (if dup then rev_dup_elim rl else rl) i))
|
|
437 |
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
|
|
438 |
|
|
439 |
in General.SOME (trl, tac) end
|
|
440 |
handle Bind => General.NONE (*reject: conclusion is not just a variable*);
|
|
441 |
|
|
442 |
|
|
443 |
(*** Conversion of Introduction Rules (needed for efficiency in
|
|
444 |
proof reconstruction) ***)
|
|
445 |
|
|
446 |
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
|
|
447 |
|
|
448 |
fun convertIntrRule vars t =
|
|
449 |
let val Ps = strip_imp_prems t
|
|
450 |
val P = strip_imp_concl t
|
|
451 |
in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
|
|
452 |
end;
|
|
453 |
|
|
454 |
(*Tableau rule from introduction rule. Since haz rules are now delayed,
|
|
455 |
"dup" is always FALSE for introduction rules.*)
|
|
456 |
fun fromIntrRule vars rl =
|
|
457 |
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
|
|
458 |
val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertIntrRule vars
|
|
459 |
fun tac dup i =
|
|
460 |
TRACE rl (DETERM (rtac (if dup then Data.dup_intr rl else rl) i))
|
|
461 |
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
|
|
462 |
in (trl, tac) end;
|
|
463 |
|
|
464 |
|
|
465 |
val dummyVar = Term.Var (("Doom",666), dummyT);
|
|
466 |
|
|
467 |
(*Convert from prototerms to ordinary terms with dummy types
|
|
468 |
Ignore abstractions; identify all Vars*)
|
|
469 |
fun dummyTerm 0 _ = dummyVar
|
|
470 |
| dummyTerm d (Const a) = Term.Const (a,dummyT)
|
|
471 |
| dummyTerm d (OConst(a,_)) = Term.Const (a,dummyT)
|
|
472 |
| dummyTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
|
|
473 |
| dummyTerm d (Free a) = Term.Free (a,dummyT)
|
|
474 |
| dummyTerm d (Bound i) = Term.Bound i
|
|
475 |
| dummyTerm d (Var _) = dummyVar
|
|
476 |
| dummyTerm d (Abs(a,_)) = dummyVar
|
|
477 |
| dummyTerm d (f $ u) = Term.$ (dummyTerm d f, dummyTerm (d-1) u);
|
|
478 |
|
|
479 |
|
|
480 |
fun netMkRules P vars (nps: netpair list) =
|
|
481 |
case P of
|
|
482 |
(Const "*Goal*" $ G) =>
|
|
483 |
let val pG = mk_tprop (dummyTerm 2 G)
|
|
484 |
val intrs = List.concat
|
|
485 |
(map (fn (inet,_) => Net.unify_term inet pG)
|
|
486 |
nps)
|
|
487 |
in map (fromIntrRule vars o #2) (orderlist intrs) end
|
|
488 |
| _ =>
|
|
489 |
let val pP = mk_tprop (dummyTerm 3 P)
|
|
490 |
val elims = List.concat
|
|
491 |
(map (fn (_,enet) => Net.unify_term enet pP)
|
|
492 |
nps)
|
|
493 |
in List.mapPartial (fromRule vars o #2) (orderlist elims) end;
|
|
494 |
|
|
495 |
(**
|
|
496 |
end;
|
|
497 |
**)
|
|
498 |
|
|
499 |
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
|
|
500 |
|
|
501 |
(*Replace the ATOMIC term "old" by "new" in t*)
|
|
502 |
fun subst_atomic (old,new) t =
|
|
503 |
let fun subst (Var(ref(Some u))) = subst u
|
|
504 |
| subst (Abs(a,body)) = Abs(a, subst body)
|
|
505 |
| subst (f$t) = subst f $ subst t
|
|
506 |
| subst t = if t aconv old then new else t
|
|
507 |
in subst t end;
|
|
508 |
|
|
509 |
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
|
|
510 |
fun eta_contract_atom (t0 as Abs(a, body)) =
|
|
511 |
(case eta_contract2 body of
|
|
512 |
f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
|
|
513 |
else eta_contract_atom (incr_boundvars ~1 f)
|
|
514 |
| _ => t0)
|
|
515 |
| eta_contract_atom t = t
|
|
516 |
and eta_contract2 (f$t) = f $ eta_contract_atom t
|
|
517 |
| eta_contract2 t = eta_contract_atom t;
|
|
518 |
|
|
519 |
|
|
520 |
(*When can we safely delete the equality?
|
|
521 |
Not if it equates two constants; consider 0=1.
|
|
522 |
Not if it resembles x=t[x], since substitution does not eliminate x.
|
|
523 |
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
|
|
524 |
Prefer to eliminate Bound variables if possible.
|
|
525 |
Result: true = use as is, false = reorient first *)
|
|
526 |
|
|
527 |
(*Does t occur in u? For substitution.
|
|
528 |
Does NOT check args of Skolem terms: substitution does not affect them.
|
|
529 |
NOT reflexive since hyp_subst_tac fails on x=x.*)
|
|
530 |
fun substOccur t =
|
|
531 |
let fun occEq u = (t aconv u) orelse occ u
|
|
532 |
and occ (Var(ref None)) = false
|
|
533 |
| occ (Var(ref(Some u))) = occEq u
|
|
534 |
| occ (Abs(_,u)) = occEq u
|
|
535 |
| occ (f$u) = occEq u orelse occEq f
|
|
536 |
| occ (_) = false;
|
|
537 |
in occEq end;
|
|
538 |
|
|
539 |
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
|
|
540 |
|
|
541 |
(*IF the goal is an equality with a substitutable variable
|
|
542 |
THEN orient that equality ELSE raise exception DEST_EQ*)
|
|
543 |
fun orientGoal (t,u) =
|
|
544 |
case (eta_contract_atom t, eta_contract_atom u) of
|
|
545 |
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*)
|
|
546 |
| (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*)
|
|
547 |
| (Free _, _) => check(t,u,(t,u)) (*eliminates t*)
|
|
548 |
| (_, Free _) => check(u,t,(u,t)) (*eliminates u*)
|
|
549 |
| _ => raise DEST_EQ;
|
|
550 |
|
|
551 |
|
2894
|
552 |
(*Substitute through the branch if an equality goal (else raise DEST_EQ).
|
|
553 |
Moves affected literals back into the branch, but it is not clear where
|
|
554 |
they should go: this could make proofs fail. ??? *)
|
|
555 |
fun equalSubst (G, pairs, lits, vars, lim) =
|
2854
|
556 |
let val subst = subst_atomic (orientGoal(dest_eq G))
|
|
557 |
fun subst2(G,md) = (subst G, md)
|
2894
|
558 |
val pairs' = map (fn(Gs,Hs) => (map subst2 Gs, map subst2 Hs)) pairs
|
|
559 |
(*substitute throughout literals and note those affected*)
|
|
560 |
fun subLits ([], [], nlits) = (pairs', nlits, vars, lim)
|
|
561 |
| subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim)
|
|
562 |
| subLits (lit::lits, Gs, nlits) =
|
2854
|
563 |
let val nlit = subst lit
|
2894
|
564 |
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits)
|
|
565 |
else subLits (lits, (nlit,true)::Gs, nlits)
|
2854
|
566 |
end
|
2894
|
567 |
in subLits (rev lits, [], [])
|
2854
|
568 |
end;
|
|
569 |
|
|
570 |
|
|
571 |
exception NEWBRANCHES and CLOSEF;
|
|
572 |
|
2894
|
573 |
(*Pending formulae carry md (may duplicate) flags*)
|
|
574 |
type branch = ((term*bool) list * (*safe formulae on this level*)
|
|
575 |
(term*bool) list) list * (*haz formulae on this level*)
|
2854
|
576 |
term list * (*literals: irreducible formulae*)
|
|
577 |
term option ref list * (*variables occurring in branch*)
|
|
578 |
int; (*resource limit*)
|
|
579 |
|
|
580 |
val fullTrace = ref[] : branch list list ref;
|
|
581 |
|
|
582 |
exception PROVE;
|
|
583 |
|
|
584 |
val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac;
|
|
585 |
|
|
586 |
val eContr_tac = TRACE Data.notE (eq_contr_tac ORELSE' Data.contr_tac);
|
|
587 |
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
|
|
588 |
|
|
589 |
(*Try to unify complementary literals and return the corresponding tactic. *)
|
|
590 |
fun tryClose (Const"*Goal*" $ G, L) = (unify([],G,L); eAssume_tac)
|
|
591 |
| tryClose (G, Const"*Goal*" $ L) = (unify([],G,L); eAssume_tac)
|
|
592 |
| tryClose (Const"Not" $ G, L) = (unify([],G,L); eContr_tac)
|
|
593 |
| tryClose (G, Const"Not" $ L) = (unify([],G,L); eContr_tac)
|
|
594 |
| tryClose _ = raise UNIFY;
|
|
595 |
|
|
596 |
|
|
597 |
(*Were there Skolem terms in the premise? Must NOT chase Vars*)
|
|
598 |
fun hasSkolem (Skolem _) = true
|
|
599 |
| hasSkolem (Abs (_,body)) = hasSkolem body
|
|
600 |
| hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
|
|
601 |
| hasSkolem _ = false;
|
|
602 |
|
|
603 |
(*Attach the right "may duplicate" flag to new formulae: if they contain
|
|
604 |
Skolem terms then allow duplication.*)
|
|
605 |
fun joinMd md [] = []
|
|
606 |
| joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
|
|
607 |
|
2894
|
608 |
(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like
|
|
609 |
Ex(P) is duplicated as the assumption ~Ex(P). *)
|
|
610 |
fun negOfGoal (Const"*Goal*" $ G) = negate G
|
|
611 |
| negOfGoal G = G;
|
|
612 |
|
|
613 |
fun negOfGoal2 (G,md) = (negOfGoal G, md);
|
|
614 |
|
|
615 |
(*Converts all Goals to Nots in the safe parts of a branch. They could
|
|
616 |
have been moved there from the literals list after substitution (equalSubst).
|
|
617 |
There can be at most one--this function could be made more efficient.*)
|
|
618 |
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
|
|
619 |
|
|
620 |
(*Tactic. Convert *Goal* to negated assumption in FIRST position*)
|
|
621 |
val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1;
|
|
622 |
|
2854
|
623 |
|
|
624 |
(** Backtracking and Pruning **)
|
|
625 |
|
|
626 |
(*clashVar vars (n,trail) determines whether any of the last n elements
|
|
627 |
of "trail" occur in "vars" OR in their instantiations*)
|
|
628 |
fun clashVar [] = (fn _ => false)
|
|
629 |
| clashVar vars =
|
|
630 |
let fun clash (0, _) = false
|
|
631 |
| clash (_, []) = false
|
|
632 |
| clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
|
|
633 |
in clash end;
|
|
634 |
|
|
635 |
|
|
636 |
(*nbrs = # of branches just prior to closing this one. Delete choice points
|
|
637 |
for goals proved by the latest inference, provided NO variables in the
|
|
638 |
next branch have been updated.*)
|
|
639 |
fun prune (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
|
|
640 |
backtracking over bad proofs*)
|
|
641 |
| prune (nbrs, nxtVars, choices) =
|
|
642 |
let fun traceIt last =
|
|
643 |
let val ll = length last
|
|
644 |
and lc = length choices
|
|
645 |
in if !trace andalso ll<lc then
|
|
646 |
(writeln("PRUNING " ^ Int.toString(lc-ll) ^ " LEVELS");
|
|
647 |
last)
|
|
648 |
else last
|
|
649 |
end
|
|
650 |
fun pruneAux (last, _, _, []) = last
|
|
651 |
| pruneAux (last, ntrl, trl, ch' as (ntrl',nbrs',exn) :: choices) =
|
|
652 |
if nbrs' < nbrs
|
|
653 |
then last (*don't backtrack beyond first solution of goal*)
|
|
654 |
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
|
|
655 |
else (* nbrs'=nbrs *)
|
|
656 |
if clashVar nxtVars (ntrl-ntrl', trl) then last
|
|
657 |
else (*no clashes: can go back at least this far!*)
|
|
658 |
pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
|
|
659 |
choices)
|
|
660 |
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end;
|
|
661 |
|
2894
|
662 |
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars
|
2854
|
663 |
| nextVars [] = [];
|
|
664 |
|
|
665 |
fun backtrack ((_, _, exn)::_) = raise exn
|
|
666 |
| backtrack _ = raise PROVE;
|
|
667 |
|
2894
|
668 |
(*Add the literal G, handling *Goal* and detecting duplicates.*)
|
|
669 |
fun addLit (Const "*Goal*" $ G, lits) =
|
|
670 |
(*New literal is a *Goal*, so change all other Goals to Nots*)
|
2854
|
671 |
let fun bad (Const"*Goal*" $ _) = true
|
|
672 |
| bad (Const"Not" $ G') = G aconv G'
|
|
673 |
| bad _ = false;
|
|
674 |
fun change [] = []
|
|
675 |
| change (Const"*Goal*" $ G' :: lits) =
|
|
676 |
if G aconv G' then change lits
|
|
677 |
else Const"Not" $ G' :: change lits
|
|
678 |
| change (Const"Not" $ G' :: lits) =
|
|
679 |
if G aconv G' then change lits
|
|
680 |
else Const"Not" $ G' :: change lits
|
|
681 |
| change (lit::lits) = lit :: change lits
|
|
682 |
in
|
|
683 |
Const "*Goal*" $ G :: (if exists bad lits then change lits else lits)
|
|
684 |
end
|
|
685 |
| addLit (G,lits) = ins_term(G, lits)
|
|
686 |
|
|
687 |
|
|
688 |
(*Tableau prover based on leanTaP. Argument is a list of branches. Each
|
|
689 |
branch contains a list of unexpanded formulae, a list of literals, and a
|
|
690 |
bound on unsafe expansions.*)
|
|
691 |
fun prove (cs, brs, cont) =
|
|
692 |
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
|
|
693 |
val safeList = [safe0_netpair, safep_netpair]
|
|
694 |
and hazList = [haz_netpair]
|
|
695 |
fun prv (tacs, trs, choices, []) = (cont (trs,choices,tacs))
|
|
696 |
| prv (tacs, trs, choices,
|
2894
|
697 |
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) =
|
2854
|
698 |
let exception PRV (*backtrack to precisely this recursion!*)
|
|
699 |
val ntrl = !ntrail
|
|
700 |
val nbrs = length brs0
|
|
701 |
val nxtVars = nextVars brs
|
|
702 |
val G = norm G
|
|
703 |
(*Make a new branch, decrementing "lim" if instantiations occur*)
|
2894
|
704 |
fun newBr (vars',lim') prems =
|
|
705 |
map (fn prem =>
|
|
706 |
if (exists isGoal prem)
|
|
707 |
then (((joinMd md prem, []) ::
|
|
708 |
negOfGoals ((br, haz)::pairs)),
|
|
709 |
map negOfGoal lits,
|
|
710 |
vars', lim')
|
|
711 |
else (((joinMd md prem, []) :: (br, haz) :: pairs),
|
|
712 |
lits, vars', lim'))
|
2854
|
713 |
prems @
|
|
714 |
brs
|
|
715 |
(*Seek a matching rule. If unifiable then add new premises
|
|
716 |
to branch.*)
|
|
717 |
fun deeper [] = raise NEWBRANCHES
|
|
718 |
| deeper (((P,prems),tac)::grls) =
|
|
719 |
let val dummy = unify(add_term_vars(P,[]), P, G)
|
|
720 |
(*P comes from the rule; G comes from the branch.*)
|
|
721 |
val ntrl' = !ntrail
|
2894
|
722 |
val lim' = if ntrl < !ntrail then lim-3 else lim
|
|
723 |
val vars = vars_in_vars vars
|
|
724 |
val vars' = foldr add_terms_vars (prems, vars)
|
2854
|
725 |
val choices' = (ntrl, nbrs, PRV) :: choices
|
|
726 |
in
|
|
727 |
if null prems then (*closed the branch: prune!*)
|
|
728 |
prv(tac false :: tacs, (*no duplication*)
|
|
729 |
brs0::trs,
|
|
730 |
prune (nbrs, nxtVars, choices'),
|
|
731 |
brs)
|
|
732 |
handle PRV =>
|
|
733 |
(*reset Vars and try another rule*)
|
|
734 |
(clearTo ntrl; deeper grls)
|
|
735 |
else
|
|
736 |
prv(tac false :: tacs, (*no duplication*)
|
|
737 |
brs0::trs, choices',
|
2894
|
738 |
newBr (vars',lim') prems)
|
2854
|
739 |
handle PRV =>
|
|
740 |
if ntrl < ntrl' then
|
|
741 |
(*Vars have been updated: must backtrack
|
|
742 |
even if not mentioned in other goals!
|
|
743 |
Reset Vars and try another rule*)
|
|
744 |
(clearTo ntrl; deeper grls)
|
|
745 |
else (*backtrack to previous level*)
|
|
746 |
backtrack choices
|
|
747 |
end
|
|
748 |
handle UNIFY => deeper grls
|
|
749 |
(*Try to close branch by unifying with head goal*)
|
|
750 |
fun closeF [] = raise CLOSEF
|
|
751 |
| closeF (L::Ls) =
|
|
752 |
let val tacs' = tryClose(G,L)::tacs
|
|
753 |
val choices' = prune (nbrs, nxtVars,
|
|
754 |
(ntrl, nbrs, PRV) :: choices)
|
|
755 |
in prv (tacs', brs0::trs, choices', brs)
|
|
756 |
handle PRV =>
|
|
757 |
(*reset Vars and try another literal
|
|
758 |
[this handler is pruned if possible!]*)
|
|
759 |
(clearTo ntrl; closeF Ls)
|
|
760 |
end
|
|
761 |
handle UNIFY => closeF Ls
|
2894
|
762 |
fun closeFl [] = raise CLOSEF
|
|
763 |
| closeFl ((br, haz)::pairs) =
|
|
764 |
closeF (map fst br)
|
|
765 |
handle CLOSEF => closeF (map fst haz)
|
|
766 |
handle CLOSEF => closeFl pairs
|
2854
|
767 |
in if !trace then fullTrace := brs0 :: !fullTrace else ();
|
|
768 |
if lim<0 then backtrack choices
|
|
769 |
else
|
|
770 |
prv (Data.vars_gen_hyp_subst_tac false :: tacs,
|
|
771 |
brs0::trs, choices,
|
2894
|
772 |
equalSubst (G, (br,haz)::pairs, lits, vars, lim) :: brs)
|
2854
|
773 |
handle DEST_EQ => closeF lits
|
2894
|
774 |
handle CLOSEF => closeFl ((br,haz)::pairs)
|
2854
|
775 |
handle CLOSEF =>
|
2894
|
776 |
deeper (netMkRules G vars safeList)
|
|
777 |
handle NEWBRANCHES =>
|
|
778 |
(case netMkRules G vars hazList of
|
|
779 |
[] => (*no plausible rules: move G to literals*)
|
|
780 |
prv (tacs, brs0::trs, choices,
|
|
781 |
((br,haz)::pairs, addLit(G,lits), vars, lim)
|
|
782 |
::brs)
|
|
783 |
| _ => (*G admits some haz rules: try later*)
|
|
784 |
prv (if isGoal G then negOfGoal_tac :: tacs
|
|
785 |
else tacs,
|
|
786 |
brs0::trs, choices,
|
|
787 |
((br, haz@[(negOfGoal G, md)])::pairs,
|
|
788 |
lits, vars, lim) :: brs))
|
2854
|
789 |
end
|
2894
|
790 |
| prv (tacs, trs, choices, (([],haz)::(Gs,haz')::pairs,
|
|
791 |
lits, vars, lim) :: brs) =
|
|
792 |
(*no more "safe" formulae: transfer haz down a level*)
|
|
793 |
prv (tacs, trs, choices, ((Gs,haz@haz')::pairs, lits, vars, lim)
|
|
794 |
:: brs)
|
2854
|
795 |
| prv (tacs, trs, choices,
|
2894
|
796 |
brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) =
|
|
797 |
(*no safe steps possible at any level: apply a haz rule*)
|
2854
|
798 |
let exception PRV (*backtrack to precisely this recursion!*)
|
2894
|
799 |
val H = norm H
|
2854
|
800 |
val ntrl = !ntrail
|
|
801 |
fun newPrem (vars,dup) prem =
|
2894
|
802 |
([(map (fn P => (P,false)) prem, []), (*may NOT duplicate*)
|
|
803 |
([], if dup then Hs @ [(negOfGoal H, md)] else Hs)],
|
2854
|
804 |
lits,
|
|
805 |
vars,
|
|
806 |
(*Decrement "lim" if instantiations occur or the
|
|
807 |
formula is duplicated*)
|
|
808 |
if ntrl < !ntrail then lim-3
|
|
809 |
else if dup then lim-1 else lim)
|
|
810 |
fun newBr x prems = map (newPrem x) prems @ brs
|
|
811 |
(*Seek a matching rule. If unifiable then add new premises
|
|
812 |
to branch.*)
|
|
813 |
fun deeper [] = raise NEWBRANCHES
|
|
814 |
| deeper (((P,prems),tac)::grls) =
|
2894
|
815 |
let val dummy = unify(add_term_vars(P,[]), P, H)
|
2854
|
816 |
val ntrl' = !ntrail
|
|
817 |
val vars = vars_in_vars vars
|
|
818 |
val vars' = foldr add_terms_vars (prems, vars)
|
|
819 |
val dup = md andalso vars' <> vars
|
2894
|
820 |
(*duplicate H only if md and the premise has new vars*)
|
2854
|
821 |
in
|
|
822 |
prv(tac dup :: tacs,
|
|
823 |
brs0::trs,
|
|
824 |
(ntrl, length brs0, PRV) :: choices,
|
|
825 |
newBr (vars', dup) prems)
|
|
826 |
handle PRV =>
|
|
827 |
if ntrl < ntrl' (*variables updated?*)
|
2883
|
828 |
orelse vars=vars' (*pseudo-unsafe: no new Vars?*)
|
2854
|
829 |
then (*reset Vars and try another rule*)
|
|
830 |
(clearTo ntrl; deeper grls)
|
|
831 |
else (*backtrack to previous level*)
|
|
832 |
backtrack choices
|
|
833 |
end
|
|
834 |
handle UNIFY => deeper grls
|
|
835 |
in if !trace then fullTrace := brs0 :: !fullTrace else ();
|
|
836 |
if lim<1 then backtrack choices
|
|
837 |
else
|
2894
|
838 |
deeper (netMkRules H vars hazList)
|
2854
|
839 |
handle NEWBRANCHES =>
|
2894
|
840 |
(*cannot close branch: move H to literals*)
|
2854
|
841 |
prv (tacs, brs0::trs, choices,
|
2894
|
842 |
([([], Hs)], H::lits, vars, lim)::brs)
|
2854
|
843 |
end
|
|
844 |
| prv (tacs, trs, choices, _ :: brs) = backtrack choices
|
|
845 |
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
|
|
846 |
|
|
847 |
|
2883
|
848 |
(*Construct an initial branch.*)
|
2854
|
849 |
fun initBranch (ts,lim) =
|
2894
|
850 |
([(map (fn t => (t,true)) ts, [])],
|
|
851 |
[], add_terms_vars (ts,[]), lim);
|
2854
|
852 |
|
|
853 |
|
|
854 |
(*** Conversion & Skolemization of the Isabelle proof state ***)
|
|
855 |
|
|
856 |
(*Make a list of all the parameters in a subgoal, even if nested*)
|
|
857 |
local open Term
|
|
858 |
in
|
|
859 |
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
|
|
860 |
| discard_foralls t = t;
|
|
861 |
end;
|
|
862 |
|
|
863 |
|
|
864 |
(*List of variables not appearing as arguments to the given parameter*)
|
|
865 |
fun getVars [] i = []
|
|
866 |
| getVars ((_,(v,is))::alist) i =
|
|
867 |
if i mem is then getVars alist i
|
|
868 |
else v :: getVars alist i;
|
|
869 |
|
|
870 |
|
|
871 |
(*Conversion of a subgoal: Skolemize all parameters*)
|
|
872 |
fun fromSubgoal tsig t =
|
|
873 |
let val alist = ref []
|
|
874 |
fun hdvar ((ix,(v,is))::_) = v
|
|
875 |
fun from lev t =
|
|
876 |
let val (ht,ts) = Term.strip_comb t
|
|
877 |
fun apply u = list_comb (u, map (from lev) ts)
|
|
878 |
fun bounds [] = []
|
|
879 |
| bounds (Term.Bound i::ts) =
|
|
880 |
if i<lev then error"Function Var's argument not a parameter"
|
|
881 |
else i-lev :: bounds ts
|
|
882 |
| bounds ts = error"Function Var's argument not a bound variable"
|
|
883 |
in
|
|
884 |
case ht of
|
|
885 |
t as Term.Const _ => apply (fromConst tsig t)
|
|
886 |
| Term.Free (a,_) => apply (Free a)
|
|
887 |
| Term.Bound i => apply (Bound i)
|
|
888 |
| Term.Var (ix,_) =>
|
|
889 |
(case (assoc_string_int(!alist,ix)) of
|
|
890 |
None => (alist := (ix, (ref None, bounds ts))
|
|
891 |
:: !alist;
|
|
892 |
Var (hdvar(!alist)))
|
|
893 |
| Some(v,is) => if is=bounds ts then Var v
|
|
894 |
else error("Discrepancy among occurrences of ?"
|
|
895 |
^ Syntax.string_of_vname ix))
|
|
896 |
| Term.Abs (a,_,body) =>
|
|
897 |
if null ts then Abs(a, from (lev+1) body)
|
|
898 |
else error "fromSubgoal: argument not in normal form"
|
|
899 |
end
|
|
900 |
|
|
901 |
val npars = length (Logic.strip_params t)
|
|
902 |
|
|
903 |
(*Skolemize a subgoal from a proof state*)
|
|
904 |
fun skoSubgoal i t =
|
|
905 |
if i<npars then
|
|
906 |
skoSubgoal (i+1)
|
|
907 |
(subst_bound (Skolem (gensym "SG_", getVars (!alist) i),
|
|
908 |
t))
|
|
909 |
else t
|
|
910 |
|
|
911 |
in skoSubgoal 0 (from 0 (discard_foralls t)) end;
|
|
912 |
|
|
913 |
|
|
914 |
(*Tactic using tableau engine and proof reconstruction.
|
|
915 |
"lim" is depth limit.*)
|
|
916 |
fun depth_tac cs lim i st =
|
|
917 |
(fullTrace:=[]; trail := []; ntrail := 0;
|
|
918 |
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm st))
|
|
919 |
val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1))
|
|
920 |
val hyps = strip_imp_prems skoprem
|
|
921 |
and concl = strip_imp_concl skoprem
|
|
922 |
fun cont (_,choices,tacs) =
|
|
923 |
(case Sequence.pull(EVERY' (rev tacs) i st) of
|
|
924 |
None => (writeln ("PROOF FAILED for depth " ^
|
|
925 |
Int.toString lim);
|
|
926 |
backtrack choices)
|
|
927 |
| cell => Sequence.seqof(fn()=> cell))
|
|
928 |
in prove (cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
|
|
929 |
end
|
|
930 |
handle Subscript => Sequence.null
|
|
931 |
| PROVE => Sequence.null);
|
|
932 |
|
|
933 |
fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);
|
|
934 |
|
|
935 |
fun Blast_tac i = blast_tac (!Data.claset) i;
|
|
936 |
|
|
937 |
end;
|
|
938 |
|