author | wenzelm |
Mon, 03 Nov 1997 11:56:17 +0100 | |
changeset 4078 | c107ab1c7626 |
parent 4065 | 8862fcb5d44a |
child 4149 | a6ccec4fd0c3 |
permissions | -rw-r--r-- |
4078 | 1 |
(* Title: Provers/blast.ML |
2894 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3083 | 4 |
Copyright 1997 University of Cambridge |
2894 | 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 |
||
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
12 |
Blast_tac is often more powerful than fast_tac, but has some limitations. |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
13 |
Blast_tac... |
2894 | 14 |
* ignores addss, addbefore, addafter; this restriction is intrinsic |
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 |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
18 |
* rules must not require higher-order unification, e.g. apply_type in ZF |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
19 |
+ message "Function Var's argument not a bound variable" relates to this |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
20 |
* its proof strategy is more general but can actually be slower |
2894 | 21 |
|
22 |
Known problems: |
|
3092 | 23 |
"Recursive" chains of rules can sometimes exclude other unsafe formulae |
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
24 |
from expansion. This happens because newly-created formulae always |
3092 | 25 |
have priority over existing ones. But obviously recursive rules |
26 |
such as transitivity are treated specially to prevent this. |
|
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
27 |
|
2952 | 28 |
With overloading: |
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
29 |
Overloading can't follow all chains of type dependencies. Cannot |
2952 | 30 |
prove "In1 x ~: Part A In0" because PartE introducees the polymorphic |
31 |
equality In1 x = In0 y, when the corresponding rule uses the (distinct) |
|
32 |
set equality. Workaround: supply a type instance of the rule that |
|
33 |
creates new equalities (e.g. PartE in HOL/ex/Simult) |
|
34 |
==> affects freeness reasoning about Sexp constants (since they have |
|
35 |
type ... set) |
|
36 |
||
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
37 |
With substition for equalities (hyp_subst_tac): |
3092 | 38 |
When substitution affects a haz formula or literal, it is moved |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
39 |
back to the list of safe formulae. |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
40 |
But there's no way of putting it in the right place. A "moved" or |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
41 |
"no DETERM" flag would prevent proofs failing here. |
2854 | 42 |
*) |
43 |
||
44 |
||
45 |
(*Should be a type abbreviation?*) |
|
46 |
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; |
|
47 |
||
48 |
||
49 |
(*Assumptions about constants: |
|
50 |
--The negation symbol is "Not" |
|
51 |
--The equality symbol is "op =" |
|
52 |
--The is-true judgement symbol is "Trueprop" |
|
53 |
--There are no constants named "*Goal* or "*False*" |
|
54 |
*) |
|
55 |
signature BLAST_DATA = |
|
56 |
sig |
|
57 |
type claset |
|
58 |
val notE : thm (* [| ~P; P |] ==> R *) |
|
59 |
val ccontr : thm |
|
60 |
val contr_tac : int -> tactic |
|
61 |
val dup_intr : thm -> thm |
|
62 |
val vars_gen_hyp_subst_tac : bool -> int -> tactic |
|
4078 | 63 |
val claset : unit -> claset |
2854 | 64 |
val rep_claset : |
65 |
claset -> {safeIs: thm list, safeEs: thm list, |
|
66 |
hazIs: thm list, hazEs: thm list, |
|
67 |
uwrapper: (int -> tactic) -> (int -> tactic), |
|
68 |
swrapper: (int -> tactic) -> (int -> tactic), |
|
69 |
safe0_netpair: netpair, safep_netpair: netpair, |
|
70 |
haz_netpair: netpair, dup_netpair: netpair} |
|
71 |
end; |
|
72 |
||
73 |
||
74 |
signature BLAST = |
|
75 |
sig |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
76 |
type claset |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
77 |
datatype term = |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
78 |
Const of string |
4065 | 79 |
| TConst of string * term |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
80 |
| Skolem of string * term option ref list |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
81 |
| Free of string |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
82 |
| Var of term option ref |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
83 |
| Bound of int |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
84 |
| Abs of string*term |
3030 | 85 |
| $ of term*term; |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
86 |
type branch |
2883 | 87 |
val depth_tac : claset -> int -> int -> tactic |
88 |
val blast_tac : claset -> int -> tactic |
|
89 |
val Blast_tac : int -> tactic |
|
4065 | 90 |
val overload : string * (Term.typ -> Term.typ) -> unit |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
91 |
(*debugging tools*) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
92 |
val trace : bool ref |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
93 |
val fullTrace : branch list list ref |
4065 | 94 |
val fromType : (indexname * term) list ref -> Term.typ -> term |
95 |
val fromTerm : Term.term -> term |
|
96 |
val fromSubgoal : Term.term -> term |
|
97 |
val instVars : term -> (unit -> unit) |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
98 |
val toTerm : int -> term -> Term.term |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
99 |
val readGoal : Sign.sg -> string -> term |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
100 |
val tryInThy : theory -> int -> string -> |
3083 | 101 |
(int->tactic) list * branch list list * (int*int*exn) list |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
102 |
val trygl : claset -> int -> int -> |
3083 | 103 |
(int->tactic) list * branch list list * (int*int*exn) list |
104 |
val Trygl : int -> int -> |
|
105 |
(int->tactic) list * branch list list * (int*int*exn) list |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
106 |
val normBr : branch -> branch |
2854 | 107 |
end; |
108 |
||
109 |
||
3092 | 110 |
functor BlastFun(Data: BLAST_DATA) : BLAST = |
2854 | 111 |
struct |
112 |
||
113 |
type claset = Data.claset; |
|
114 |
||
115 |
val trace = ref false; |
|
116 |
||
117 |
datatype term = |
|
118 |
Const of string |
|
4065 | 119 |
| TConst of string * term (*type of overloaded constant--as a term!*) |
2854 | 120 |
| Skolem of string * term option ref list |
121 |
| Free of string |
|
122 |
| Var of term option ref |
|
123 |
| Bound of int |
|
124 |
| Abs of string*term |
|
125 |
| op $ of term*term; |
|
126 |
||
127 |
||
128 |
(** Basic syntactic operations **) |
|
129 |
||
130 |
fun is_Var (Var _) = true |
|
131 |
| is_Var _ = false; |
|
132 |
||
133 |
fun dest_Var (Var x) = x; |
|
134 |
||
135 |
||
136 |
fun rand (f$x) = x; |
|
137 |
||
138 |
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *) |
|
139 |
val list_comb : term * term list -> term = foldl (op $); |
|
140 |
||
141 |
||
142 |
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) |
|
143 |
fun strip_comb u : term * term list = |
|
144 |
let fun stripc (f$t, ts) = stripc (f, t::ts) |
|
145 |
| stripc x = x |
|
146 |
in stripc(u,[]) end; |
|
147 |
||
148 |
||
149 |
(* maps f(t1,...,tn) to f , which is never a combination *) |
|
150 |
fun head_of (f$t) = head_of f |
|
151 |
| head_of u = u; |
|
152 |
||
153 |
||
154 |
(** Particular constants **) |
|
155 |
||
156 |
fun negate P = Const"Not" $ P; |
|
157 |
||
158 |
fun mkGoal P = Const"*Goal*" $ P; |
|
159 |
||
160 |
fun isGoal (Const"*Goal*" $ _) = true |
|
161 |
| isGoal _ = false; |
|
162 |
||
163 |
val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT); |
|
164 |
fun mk_tprop P = Term.$ (Trueprop, P); |
|
165 |
||
166 |
fun isTrueprop (Term.Const("Trueprop",_)) = true |
|
167 |
| isTrueprop _ = false; |
|
168 |
||
169 |
||
4065 | 170 |
(*** Dealing with overloaded constants ***) |
2854 | 171 |
|
4065 | 172 |
(*alist is a map from TVar names to Vars. We need to unify the TVars |
173 |
faithfully in order to track overloading*) |
|
174 |
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, |
|
175 |
map (fromType alist) Ts) |
|
176 |
| fromType alist (Term.TFree(a,_)) = Free a |
|
177 |
| fromType alist (Term.TVar (ixn,_)) = |
|
178 |
(case (assoc_string_int(!alist,ixn)) of |
|
179 |
None => let val t' = Var(ref None) |
|
180 |
in alist := (ixn, t') :: !alist; t' |
|
181 |
end |
|
182 |
| Some v => v) |
|
2854 | 183 |
|
184 |
local |
|
4065 | 185 |
val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list) |
2854 | 186 |
in |
187 |
||
4065 | 188 |
fun overload arg = (overloads := arg :: (!overloads)); |
2854 | 189 |
|
4065 | 190 |
(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst, |
191 |
converting its type to a Blast.term in the latter case.*) |
|
192 |
fun fromConst alist (a,T) = |
|
193 |
case assoc_string (!overloads, a) of |
|
194 |
None => Const a (*not overloaded*) |
|
195 |
| Some f => |
|
196 |
let val T' = f T |
|
197 |
handle Match => |
|
198 |
error ("Blast_tac: unexpected type for overloaded constant " ^ a) |
|
199 |
in TConst(a, fromType alist T') end; |
|
200 |
||
2854 | 201 |
end; |
202 |
||
203 |
||
204 |
(*Tests whether 2 terms are alpha-convertible; chases instantiations*) |
|
205 |
fun (Const a) aconv (Const b) = a=b |
|
4065 | 206 |
| (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb |
2854 | 207 |
| (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) |
208 |
| (Free a) aconv (Free b) = a=b |
|
209 |
| (Var(ref(Some t))) aconv u = t aconv u |
|
4065 | 210 |
| t aconv (Var(ref(Some u))) = t aconv u |
2854 | 211 |
| (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*) |
212 |
| (Bound i) aconv (Bound j) = i=j |
|
213 |
| (Abs(_,t)) aconv (Abs(_,u)) = t aconv u |
|
214 |
| (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) |
|
215 |
| _ aconv _ = false; |
|
216 |
||
217 |
||
218 |
fun mem_term (_, []) = false |
|
219 |
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts); |
|
220 |
||
221 |
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; |
|
222 |
||
223 |
fun mem_var (v: term option ref, []) = false |
|
224 |
| mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); |
|
225 |
||
226 |
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; |
|
227 |
||
228 |
||
229 |
(** Vars **) |
|
230 |
||
231 |
(*Accumulates the Vars in the term, suppressing duplicates*) |
|
232 |
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) |
|
233 |
| add_term_vars (Var (v as ref None), vars) = ins_var (v, vars) |
|
234 |
| add_term_vars (Var (ref (Some u)), vars) = add_term_vars(u,vars) |
|
4065 | 235 |
| add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) |
2854 | 236 |
| add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) |
237 |
| add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) |
|
238 |
| add_term_vars (_, vars) = vars |
|
239 |
(*Term list version. [The fold functionals are slow]*) |
|
240 |
and add_terms_vars ([], vars) = vars |
|
241 |
| add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) |
|
242 |
(*Var list version.*) |
|
243 |
and add_vars_vars ([], vars) = vars |
|
244 |
| add_vars_vars (ref (Some u) :: vs, vars) = |
|
245 |
add_vars_vars (vs, add_term_vars(u,vars)) |
|
246 |
| add_vars_vars (v::vs, vars) = (*v must be a ref None*) |
|
247 |
add_vars_vars (vs, ins_var (v, vars)); |
|
248 |
||
249 |
||
250 |
(*Chase assignments in "vars"; return a list of unassigned variables*) |
|
251 |
fun vars_in_vars vars = add_vars_vars(vars,[]); |
|
252 |
||
253 |
||
254 |
||
255 |
(*increment a term's non-local bound variables |
|
256 |
inc is increment for bound variables |
|
257 |
lev is level at which a bound variable is considered 'loose'*) |
|
258 |
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u |
|
259 |
| incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body)) |
|
260 |
| incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) |
|
261 |
| incr_bv (inc, lev, u) = u; |
|
262 |
||
263 |
fun incr_boundvars 0 t = t |
|
264 |
| incr_boundvars inc t = incr_bv(inc,0,t); |
|
265 |
||
266 |
||
267 |
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. |
|
268 |
(Bound 0) is loose at level 0 *) |
|
269 |
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js |
|
270 |
else (i-lev) ins_int js |
|
271 |
| add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js) |
|
272 |
| add_loose_bnos (f$t, lev, js) = |
|
273 |
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) |
|
274 |
| add_loose_bnos (_, _, js) = js; |
|
275 |
||
276 |
fun loose_bnos t = add_loose_bnos (t, 0, []); |
|
277 |
||
278 |
fun subst_bound (arg, t) : term = |
|
279 |
let fun subst (t as Bound i, lev) = |
|
280 |
if i<lev then t (*var is locally bound*) |
|
281 |
else if i=lev then incr_boundvars lev arg |
|
282 |
else Bound(i-1) (*loose: change it*) |
|
283 |
| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1)) |
|
284 |
| subst (f$t, lev) = subst(f,lev) $ subst(t,lev) |
|
285 |
| subst (t,lev) = t |
|
286 |
in subst (t,0) end; |
|
287 |
||
288 |
||
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
289 |
(*Normalize...but not the bodies of ABSTRACTIONS*) |
2854 | 290 |
fun norm t = case t of |
2952 | 291 |
Skolem (a,args) => Skolem(a, vars_in_vars args) |
4065 | 292 |
| TConst(a,aT) => TConst(a, norm aT) |
2854 | 293 |
| (Var (ref None)) => t |
294 |
| (Var (ref (Some u))) => norm u |
|
295 |
| (f $ u) => (case norm f of |
|
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
296 |
Abs(_,body) => norm (subst_bound (u, body)) |
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
297 |
| nf => nf $ norm u) |
2854 | 298 |
| _ => t; |
299 |
||
300 |
||
301 |
(*Weak (one-level) normalize for use in unification*) |
|
302 |
fun wkNormAux t = case t of |
|
303 |
(Var v) => (case !v of |
|
304 |
Some u => wkNorm u |
|
305 |
| None => t) |
|
306 |
| (f $ u) => (case wkNormAux f of |
|
307 |
Abs(_,body) => wkNorm (subst_bound (u, body)) |
|
308 |
| nf => nf $ u) |
|
2952 | 309 |
| Abs (a,body) => (*eta-contract if possible*) |
310 |
(case wkNormAux body of |
|
311 |
nb as (f $ t) => |
|
312 |
if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0 |
|
313 |
then Abs(a,nb) |
|
314 |
else wkNorm (incr_boundvars ~1 f) |
|
3092 | 315 |
| nb => Abs (a,nb)) |
2854 | 316 |
| _ => t |
317 |
and wkNorm t = case head_of t of |
|
318 |
Const _ => t |
|
4065 | 319 |
| TConst _ => t |
2854 | 320 |
| Skolem(a,args) => t |
321 |
| Free _ => t |
|
322 |
| _ => wkNormAux t; |
|
323 |
||
324 |
||
325 |
(*Does variable v occur in u? For unification.*) |
|
326 |
fun varOccur v = |
|
327 |
let fun occL [] = false (*same as (exists occ), but faster*) |
|
328 |
| occL (u::us) = occ u orelse occL us |
|
329 |
and occ (Var w) = |
|
330 |
v=w orelse |
|
331 |
(case !w of None => false |
|
332 |
| Some u => occ u) |
|
333 |
| occ (Skolem(_,args)) = occL (map Var args) |
|
4065 | 334 |
| occ (TConst(_,u)) = occ u |
2854 | 335 |
| occ (Abs(_,u)) = occ u |
336 |
| occ (f$u) = occ u orelse occ f |
|
337 |
| occ (_) = false; |
|
338 |
in occ end; |
|
339 |
||
340 |
exception UNIFY; |
|
341 |
||
342 |
val trail = ref [] : term option ref list ref; |
|
343 |
val ntrail = ref 0; |
|
344 |
||
345 |
||
346 |
(*Restore the trail to some previous state: for backtracking*) |
|
347 |
fun clearTo n = |
|
3083 | 348 |
while !ntrail<>n do |
2854 | 349 |
(hd(!trail) := None; |
350 |
trail := tl (!trail); |
|
351 |
ntrail := !ntrail - 1); |
|
352 |
||
353 |
||
354 |
(*First-order unification with bound variables. |
|
355 |
"vars" is a list of variables local to the rule and NOT to be put |
|
356 |
on the trail (no point in doing so) |
|
357 |
*) |
|
4065 | 358 |
fun unify(vars,t,u) = |
2854 | 359 |
let val n = !ntrail |
360 |
fun update (t as Var v, u) = |
|
361 |
if t aconv u then () |
|
362 |
else if varOccur v u then raise UNIFY |
|
363 |
else if mem_var(v, vars) then v := Some u |
|
364 |
else (*avoid updating Vars in the branch if possible!*) |
|
365 |
if is_Var u andalso mem_var(dest_Var u, vars) |
|
366 |
then dest_Var u := Some t |
|
367 |
else (v := Some u; |
|
368 |
trail := v :: !trail; ntrail := !ntrail + 1) |
|
369 |
fun unifyAux (t,u) = |
|
370 |
case (wkNorm t, wkNorm u) of |
|
371 |
(nt as Var v, nu) => update(nt,nu) |
|
372 |
| (nu, nt as Var v) => update(nt,nu) |
|
4065 | 373 |
| (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt) |
374 |
else raise UNIFY |
|
2854 | 375 |
| (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') |
376 |
(*NB: can yield unifiers having dangling Bound vars!*) |
|
377 |
| (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) |
|
378 |
| (nt, nu) => if nt aconv nu then () else raise UNIFY |
|
3083 | 379 |
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) |
2854 | 380 |
end; |
381 |
||
382 |
||
4065 | 383 |
(*Convert from "real" terms to prototerms; eta-contract |
384 |
Code is duplicated with fromSubgoal. Correct this?*) |
|
385 |
fun fromTerm t = |
|
386 |
let val alistVar = ref [] |
|
387 |
and alistTVar = ref [] |
|
388 |
fun from (Term.Const aT) = fromConst alistTVar aT |
|
2854 | 389 |
| from (Term.Free (a,_)) = Free a |
390 |
| from (Term.Bound i) = Bound i |
|
391 |
| from (Term.Var (ixn,T)) = |
|
4065 | 392 |
(case (assoc_string_int(!alistVar,ixn)) of |
2854 | 393 |
None => let val t' = Var(ref None) |
4065 | 394 |
in alistVar := (ixn, t') :: !alistVar; t' |
2854 | 395 |
end |
4065 | 396 |
| Some v => v) |
2854 | 397 |
| from (Term.Abs (a,_,u)) = |
398 |
(case from u of |
|
399 |
u' as (f $ Bound 0) => |
|
400 |
if (0 mem_int loose_bnos f) then Abs(a,u') |
|
401 |
else incr_boundvars ~1 f |
|
402 |
| u' => Abs(a,u')) |
|
403 |
| from (Term.$ (f,u)) = from f $ from u |
|
404 |
in from t end; |
|
405 |
||
4065 | 406 |
(*A debugging function: replaces all Vars by dummy Frees for visual inspection |
407 |
of whether they are distinct. Function revert undoes the assignments.*) |
|
408 |
fun instVars t = |
|
409 |
let val name = ref "A" |
|
410 |
val updated = ref [] |
|
411 |
fun inst (TConst(a,t)) = inst t |
|
412 |
| inst (Var(v as ref None)) = (updated := v :: (!updated); |
|
413 |
v := Some (Free ("?" ^ !name)); |
|
414 |
name := bump_string (!name)) |
|
415 |
| inst (Abs(a,t)) = inst t |
|
416 |
| inst (f $ u) = (inst f; inst u) |
|
417 |
| inst _ = () |
|
418 |
fun revert() = seq (fn v => v:=None) (!updated) |
|
419 |
in inst t; revert end; |
|
420 |
||
421 |
||
2854 | 422 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) |
423 |
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = |
|
424 |
A :: strip_imp_prems B |
|
425 |
| strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B |
|
426 |
| strip_imp_prems _ = []; |
|
427 |
||
428 |
(* A1==>...An==>B goes to B, where B is not an implication *) |
|
429 |
fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B |
|
430 |
| strip_imp_concl (Const"Trueprop" $ A) = A |
|
431 |
| strip_imp_concl A = A : term; |
|
432 |
||
433 |
||
434 |
(*** Conversion of Elimination Rules to Tableau Operations ***) |
|
435 |
||
436 |
(*The conclusion becomes the goal/negated assumption *False*: delete it!*) |
|
437 |
fun squash_nots [] = [] |
|
438 |
| squash_nots (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) = |
|
439 |
squash_nots Ps |
|
440 |
| squash_nots (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) = |
|
441 |
squash_nots Ps |
|
442 |
| squash_nots (P::Ps) = P :: squash_nots Ps; |
|
443 |
||
444 |
fun skoPrem vars (Const "all" $ Abs (_, P)) = |
|
445 |
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) |
|
446 |
| skoPrem vars P = P; |
|
447 |
||
448 |
fun convertPrem t = |
|
449 |
squash_nots (mkGoal (strip_imp_concl t) :: strip_imp_prems t); |
|
450 |
||
451 |
(*Expects elimination rules to have a formula variable as conclusion*) |
|
452 |
fun convertRule vars t = |
|
453 |
let val (P::Ps) = strip_imp_prems t |
|
454 |
val Var v = strip_imp_concl t |
|
455 |
in v := Some (Const"*False*"); |
|
456 |
(P, map (convertPrem o skoPrem vars) Ps) |
|
457 |
end; |
|
458 |
||
459 |
||
460 |
(*Like dup_elim, but puts the duplicated major premise FIRST*) |
|
461 |
fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd; |
|
462 |
||
463 |
||
464 |
(*Count new hyps so that they can be rotated*) |
|
465 |
fun nNewHyps [] = 0 |
|
466 |
| nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps |
|
467 |
| nNewHyps (P::Ps) = 1 + nNewHyps Ps; |
|
468 |
||
469 |
fun rot_subgoals_tac [] i st = Sequence.single st |
|
470 |
| rot_subgoals_tac (k::ks) i st = |
|
471 |
rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st)) |
|
472 |
handle OPTION _ => Sequence.null; |
|
473 |
||
2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset
|
474 |
fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i; |
2854 | 475 |
|
476 |
(*Tableau rule from elimination rule. Flag "dup" requests duplication of the |
|
477 |
affected formula.*) |
|
478 |
fun fromRule vars rl = |
|
4065 | 479 |
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars |
2854 | 480 |
fun tac dup i = |
2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset
|
481 |
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i |
2854 | 482 |
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i |
483 |
||
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3101
diff
changeset
|
484 |
in Option.SOME (trl, tac) end |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
485 |
handle Bind => (*reject: conclusion is not just a variable*) |
3533 | 486 |
(if !trace then (warning ("ignoring ill-formed elimination rule\n" ^ |
487 |
string_of_thm rl)) |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
488 |
else (); |
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3101
diff
changeset
|
489 |
Option.NONE); |
2854 | 490 |
|
491 |
||
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
492 |
(*** Conversion of Introduction Rules ***) |
2854 | 493 |
|
494 |
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; |
|
495 |
||
496 |
fun convertIntrRule vars t = |
|
497 |
let val Ps = strip_imp_prems t |
|
498 |
val P = strip_imp_concl t |
|
499 |
in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) |
|
500 |
end; |
|
501 |
||
502 |
(*Tableau rule from introduction rule. Since haz rules are now delayed, |
|
503 |
"dup" is always FALSE for introduction rules.*) |
|
504 |
fun fromIntrRule vars rl = |
|
4065 | 505 |
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars |
2854 | 506 |
fun tac dup i = |
2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset
|
507 |
TRACE rl (DETERM o (rtac (if dup then Data.dup_intr rl else rl))) i |
2854 | 508 |
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i |
509 |
in (trl, tac) end; |
|
510 |
||
511 |
||
3030 | 512 |
val dummyVar = Term.Var (("etc",0), dummyT); |
2854 | 513 |
|
514 |
(*Convert from prototerms to ordinary terms with dummy types |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
515 |
Ignore abstractions; identify all Vars; STOP at given depth*) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
516 |
fun toTerm 0 _ = dummyVar |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
517 |
| toTerm d (Const a) = Term.Const (a,dummyT) |
4065 | 518 |
| toTerm d (TConst(a,_)) = Term.Const (a,dummyT) (*no need to convert type*) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
519 |
| toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
520 |
| toTerm d (Free a) = Term.Free (a,dummyT) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
521 |
| toTerm d (Bound i) = Term.Bound i |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
522 |
| toTerm d (Var _) = dummyVar |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
523 |
| toTerm d (Abs(a,_)) = dummyVar |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
524 |
| toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); |
2854 | 525 |
|
526 |
||
527 |
fun netMkRules P vars (nps: netpair list) = |
|
528 |
case P of |
|
529 |
(Const "*Goal*" $ G) => |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
530 |
let val pG = mk_tprop (toTerm 2 G) |
2854 | 531 |
val intrs = List.concat |
532 |
(map (fn (inet,_) => Net.unify_term inet pG) |
|
533 |
nps) |
|
534 |
in map (fromIntrRule vars o #2) (orderlist intrs) end |
|
535 |
| _ => |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
536 |
let val pP = mk_tprop (toTerm 3 P) |
2854 | 537 |
val elims = List.concat |
538 |
(map (fn (_,enet) => Net.unify_term enet pP) |
|
539 |
nps) |
|
540 |
in List.mapPartial (fromRule vars o #2) (orderlist elims) end; |
|
541 |
||
542 |
(** |
|
543 |
end; |
|
544 |
**) |
|
545 |
||
3092 | 546 |
|
547 |
(*Pending formulae carry md (may duplicate) flags*) |
|
548 |
type branch = ((term*bool) list * (*safe formulae on this level*) |
|
549 |
(term*bool) list) list * (*haz formulae on this level*) |
|
550 |
term list * (*literals: irreducible formulae*) |
|
551 |
term option ref list * (*variables occurring in branch*) |
|
552 |
int; (*resource limit*) |
|
553 |
||
554 |
val fullTrace = ref[] : branch list list ref; |
|
555 |
||
556 |
(*Normalize a branch--for tracing*) |
|
557 |
fun norm2 (G,md) = (norm G, md); |
|
558 |
||
559 |
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); |
|
560 |
||
561 |
fun normBr (br, lits, vars, lim) = |
|
562 |
(map normLev br, map norm lits, vars, lim); |
|
563 |
||
564 |
||
4065 | 565 |
val dummyTVar = Term.TVar(("a",0), []); |
3092 | 566 |
val dummyVar2 = Term.Var(("var",0), dummyT); |
567 |
||
4065 | 568 |
(*convert Blast_tac's type representation to real types for tracing*) |
569 |
fun showType (Free a) = Term.TFree (a,[]) |
|
570 |
| showType (Var _) = dummyTVar |
|
571 |
| showType t = |
|
572 |
(case strip_comb t of |
|
573 |
(Const a, us) => Term.Type(a, map showType us) |
|
574 |
| _ => dummyT); |
|
575 |
||
576 |
(*Display top-level overloading if any*) |
|
577 |
fun topType (TConst(a,t)) = Some (showType t) |
|
578 |
| topType (Abs(a,t)) = topType t |
|
579 |
| topType (f $ u) = (case topType f of |
|
580 |
None => topType u |
|
581 |
| some => some) |
|
582 |
| topType _ = None; |
|
583 |
||
584 |
||
3092 | 585 |
(*Convert from prototerms to ordinary terms with dummy types for tracing*) |
586 |
fun showTerm d (Const a) = Term.Const (a,dummyT) |
|
4065 | 587 |
| showTerm d (TConst(a,_)) = Term.Const (a,dummyT) |
3092 | 588 |
| showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) |
589 |
| showTerm d (Free a) = Term.Free (a,dummyT) |
|
590 |
| showTerm d (Bound i) = Term.Bound i |
|
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
591 |
| showTerm d (Var(ref(Some u))) = showTerm d u |
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
592 |
| showTerm d (Var(ref None)) = dummyVar2 |
3092 | 593 |
| showTerm d (Abs(a,t)) = if d=0 then dummyVar |
594 |
else Term.Abs(a, dummyT, showTerm (d-1) t) |
|
595 |
| showTerm d (f $ u) = if d=0 then dummyVar |
|
596 |
else Term.$ (showTerm d f, showTerm (d-1) u); |
|
597 |
||
4065 | 598 |
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); |
3092 | 599 |
|
4065 | 600 |
fun traceTerm sign t = |
601 |
let val t' = norm t |
|
602 |
val stm = string_of sign 8 t' |
|
603 |
in |
|
604 |
case topType t' of |
|
605 |
None => stm (*no type to attach*) |
|
606 |
| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T |
|
607 |
end; |
|
3092 | 608 |
|
609 |
||
610 |
(*Print tracing information at each iteration of prover*) |
|
611 |
fun tracing sign brs = |
|
612 |
let fun printPairs (((G,_)::_,_)::_) = prs(traceTerm sign G) |
|
613 |
| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)") |
|
614 |
| printPairs _ = () |
|
615 |
fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = |
|
616 |
(fullTrace := brs0 :: !fullTrace; |
|
617 |
seq (fn _ => prs "+") brs; |
|
618 |
prs (" [" ^ Int.toString lim ^ "] "); |
|
619 |
printPairs pairs; |
|
620 |
writeln"") |
|
621 |
in if !trace then printBrs (map normBr brs) else () |
|
622 |
end; |
|
623 |
||
4065 | 624 |
fun traceMsg s = if !trace then prs s else (); |
625 |
||
3092 | 626 |
(*Tracing: variables updated in the last branch operation?*) |
4065 | 627 |
fun traceVars sign ntrl = |
628 |
if !trace then |
|
629 |
(case !ntrail-ntrl of |
|
630 |
0 => () |
|
631 |
| 1 => prs"\t1 variable UPDATED:" |
|
632 |
| n => prs("\t" ^ Int.toString n ^ " variables UPDATED:"); |
|
633 |
(*display the instantiations themselves, though no variable names*) |
|
634 |
seq (fn v => prs(" " ^ string_of sign 4 (the (!v)))) |
|
635 |
(List.take(!trail, !ntrail-ntrl)); |
|
636 |
writeln"") |
|
3092 | 637 |
else (); |
638 |
||
639 |
(*Tracing: how many new branches are created?*) |
|
640 |
fun traceNew prems = |
|
641 |
if !trace then |
|
642 |
case length prems of |
|
643 |
0 => prs"branch closed by rule" |
|
644 |
| 1 => prs"branch extended (1 new subgoal)" |
|
645 |
| n => prs("branch split: "^ Int.toString n ^ " new subgoals") |
|
646 |
else (); |
|
647 |
||
648 |
||
649 |
||
2854 | 650 |
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) |
651 |
||
652 |
(*Replace the ATOMIC term "old" by "new" in t*) |
|
653 |
fun subst_atomic (old,new) t = |
|
654 |
let fun subst (Var(ref(Some u))) = subst u |
|
655 |
| subst (Abs(a,body)) = Abs(a, subst body) |
|
656 |
| subst (f$t) = subst f $ subst t |
|
657 |
| subst t = if t aconv old then new else t |
|
658 |
in subst t end; |
|
659 |
||
660 |
(*Eta-contract a term from outside: just enough to reduce it to an atom*) |
|
661 |
fun eta_contract_atom (t0 as Abs(a, body)) = |
|
662 |
(case eta_contract2 body of |
|
663 |
f $ Bound 0 => if (0 mem_int loose_bnos f) then t0 |
|
664 |
else eta_contract_atom (incr_boundvars ~1 f) |
|
665 |
| _ => t0) |
|
666 |
| eta_contract_atom t = t |
|
667 |
and eta_contract2 (f$t) = f $ eta_contract_atom t |
|
668 |
| eta_contract2 t = eta_contract_atom t; |
|
669 |
||
670 |
||
671 |
(*When can we safely delete the equality? |
|
672 |
Not if it equates two constants; consider 0=1. |
|
673 |
Not if it resembles x=t[x], since substitution does not eliminate x. |
|
674 |
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) |
|
675 |
Prefer to eliminate Bound variables if possible. |
|
676 |
Result: true = use as is, false = reorient first *) |
|
677 |
||
678 |
(*Does t occur in u? For substitution. |
|
679 |
Does NOT check args of Skolem terms: substitution does not affect them. |
|
680 |
NOT reflexive since hyp_subst_tac fails on x=x.*) |
|
681 |
fun substOccur t = |
|
682 |
let fun occEq u = (t aconv u) orelse occ u |
|
683 |
and occ (Var(ref None)) = false |
|
684 |
| occ (Var(ref(Some u))) = occEq u |
|
685 |
| occ (Abs(_,u)) = occEq u |
|
686 |
| occ (f$u) = occEq u orelse occEq f |
|
687 |
| occ (_) = false; |
|
688 |
in occEq end; |
|
689 |
||
3092 | 690 |
exception DEST_EQ; |
691 |
||
692 |
(*Take apart an equality (plain or overloaded). NO constant Trueprop*) |
|
693 |
fun dest_eq (Const "op =" $ t $ u) = |
|
694 |
(eta_contract_atom t, eta_contract_atom u) |
|
4065 | 695 |
| dest_eq (TConst("op =",_) $ t $ u) = |
3092 | 696 |
(eta_contract_atom t, eta_contract_atom u) |
697 |
| dest_eq _ = raise DEST_EQ; |
|
698 |
||
2854 | 699 |
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; |
700 |
||
701 |
(*IF the goal is an equality with a substitutable variable |
|
702 |
THEN orient that equality ELSE raise exception DEST_EQ*) |
|
3092 | 703 |
fun orientGoal (t,u) = case (t,u) of |
2854 | 704 |
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) |
705 |
| (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) |
|
706 |
| (Free _, _) => check(t,u,(t,u)) (*eliminates t*) |
|
707 |
| (_, Free _) => check(u,t,(u,t)) (*eliminates u*) |
|
708 |
| _ => raise DEST_EQ; |
|
709 |
||
2894 | 710 |
(*Substitute through the branch if an equality goal (else raise DEST_EQ). |
711 |
Moves affected literals back into the branch, but it is not clear where |
|
712 |
they should go: this could make proofs fail. ??? *) |
|
3092 | 713 |
fun equalSubst sign (G, pairs, lits, vars, lim) = |
714 |
let val (t,u) = orientGoal(dest_eq G) |
|
715 |
val subst = subst_atomic (t,u) |
|
2854 | 716 |
fun subst2(G,md) = (subst G, md) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
717 |
(*substitute throughout Haz list; move affected ones to Safe part*) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
718 |
fun subHazs ([], Gs, nHs) = (Gs,nHs) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
719 |
| subHazs ((H,md)::Hs, Gs, nHs) = |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
720 |
let val nH = subst H |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
721 |
in if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
722 |
else subHazs (Hs, (nH,md)::Gs, nHs) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
723 |
end |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
724 |
val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
725 |
(*substitute throughout literals; move affected ones to Safe part*) |
2894 | 726 |
fun subLits ([], [], nlits) = (pairs', nlits, vars, lim) |
727 |
| subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim) |
|
728 |
| subLits (lit::lits, Gs, nlits) = |
|
2854 | 729 |
let val nlit = subst lit |
2894 | 730 |
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) |
731 |
else subLits (lits, (nlit,true)::Gs, nlits) |
|
2854 | 732 |
end |
3092 | 733 |
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ |
734 |
" for " ^ traceTerm sign t ^ " in branch" ) |
|
735 |
else (); |
|
3083 | 736 |
subLits (rev lits, [], []) |
2854 | 737 |
end; |
738 |
||
739 |
||
740 |
exception NEWBRANCHES and CLOSEF; |
|
741 |
||
742 |
exception PROVE; |
|
743 |
||
744 |
val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac; |
|
745 |
||
746 |
val eContr_tac = TRACE Data.notE (eq_contr_tac ORELSE' Data.contr_tac); |
|
747 |
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); |
|
748 |
||
749 |
(*Try to unify complementary literals and return the corresponding tactic. *) |
|
3083 | 750 |
fun tryClose (Const"*Goal*" $ G, L) = |
4065 | 751 |
if unify([],G,L) then Some eAssume_tac else None |
3083 | 752 |
| tryClose (G, Const"*Goal*" $ L) = |
4065 | 753 |
if unify([],G,L) then Some eAssume_tac else None |
3083 | 754 |
| tryClose (Const"Not" $ G, L) = |
4065 | 755 |
if unify([],G,L) then Some eContr_tac else None |
3083 | 756 |
| tryClose (G, Const"Not" $ L) = |
4065 | 757 |
if unify([],G,L) then Some eContr_tac else None |
3083 | 758 |
| tryClose _ = None; |
2854 | 759 |
|
760 |
||
761 |
(*Were there Skolem terms in the premise? Must NOT chase Vars*) |
|
762 |
fun hasSkolem (Skolem _) = true |
|
763 |
| hasSkolem (Abs (_,body)) = hasSkolem body |
|
764 |
| hasSkolem (f$t) = hasSkolem f orelse hasSkolem t |
|
765 |
| hasSkolem _ = false; |
|
766 |
||
767 |
(*Attach the right "may duplicate" flag to new formulae: if they contain |
|
768 |
Skolem terms then allow duplication.*) |
|
769 |
fun joinMd md [] = [] |
|
770 |
| joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; |
|
771 |
||
2894 | 772 |
(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like |
773 |
Ex(P) is duplicated as the assumption ~Ex(P). *) |
|
774 |
fun negOfGoal (Const"*Goal*" $ G) = negate G |
|
775 |
| negOfGoal G = G; |
|
776 |
||
777 |
fun negOfGoal2 (G,md) = (negOfGoal G, md); |
|
778 |
||
779 |
(*Converts all Goals to Nots in the safe parts of a branch. They could |
|
780 |
have been moved there from the literals list after substitution (equalSubst). |
|
781 |
There can be at most one--this function could be made more efficient.*) |
|
782 |
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; |
|
783 |
||
784 |
(*Tactic. Convert *Goal* to negated assumption in FIRST position*) |
|
785 |
val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1; |
|
786 |
||
2854 | 787 |
|
788 |
(** Backtracking and Pruning **) |
|
789 |
||
790 |
(*clashVar vars (n,trail) determines whether any of the last n elements |
|
791 |
of "trail" occur in "vars" OR in their instantiations*) |
|
792 |
fun clashVar [] = (fn _ => false) |
|
793 |
| clashVar vars = |
|
794 |
let fun clash (0, _) = false |
|
795 |
| clash (_, []) = false |
|
796 |
| clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs) |
|
797 |
in clash end; |
|
798 |
||
799 |
||
800 |
(*nbrs = # of branches just prior to closing this one. Delete choice points |
|
801 |
for goals proved by the latest inference, provided NO variables in the |
|
802 |
next branch have been updated.*) |
|
803 |
fun prune (1, nxtVars, choices) = choices (*DON'T prune at very end: allow |
|
804 |
backtracking over bad proofs*) |
|
805 |
| prune (nbrs, nxtVars, choices) = |
|
806 |
let fun traceIt last = |
|
807 |
let val ll = length last |
|
808 |
and lc = length choices |
|
809 |
in if !trace andalso ll<lc then |
|
3083 | 810 |
(writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels"); |
2854 | 811 |
last) |
812 |
else last |
|
813 |
end |
|
814 |
fun pruneAux (last, _, _, []) = last |
|
3083 | 815 |
| pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) = |
2854 | 816 |
if nbrs' < nbrs |
817 |
then last (*don't backtrack beyond first solution of goal*) |
|
818 |
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices) |
|
819 |
else (* nbrs'=nbrs *) |
|
820 |
if clashVar nxtVars (ntrl-ntrl', trl) then last |
|
821 |
else (*no clashes: can go back at least this far!*) |
|
822 |
pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), |
|
823 |
choices) |
|
824 |
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; |
|
825 |
||
2894 | 826 |
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars |
3083 | 827 |
| nextVars [] = []; |
2854 | 828 |
|
3083 | 829 |
fun backtrack (choices as (ntrl, nbrs, exn)::_) = |
830 |
(if !trace then (writeln ("Backtracking; now there are " ^ |
|
831 |
Int.toString nbrs ^ " branches")) |
|
832 |
else (); |
|
833 |
raise exn) |
|
834 |
| backtrack _ = raise PROVE; |
|
2854 | 835 |
|
2894 | 836 |
(*Add the literal G, handling *Goal* and detecting duplicates.*) |
837 |
fun addLit (Const "*Goal*" $ G, lits) = |
|
838 |
(*New literal is a *Goal*, so change all other Goals to Nots*) |
|
2854 | 839 |
let fun bad (Const"*Goal*" $ _) = true |
840 |
| bad (Const"Not" $ G') = G aconv G' |
|
841 |
| bad _ = false; |
|
842 |
fun change [] = [] |
|
843 |
| change (Const"*Goal*" $ G' :: lits) = |
|
844 |
if G aconv G' then change lits |
|
845 |
else Const"Not" $ G' :: change lits |
|
846 |
| change (Const"Not" $ G' :: lits) = |
|
847 |
if G aconv G' then change lits |
|
848 |
else Const"Not" $ G' :: change lits |
|
849 |
| change (lit::lits) = lit :: change lits |
|
850 |
in |
|
851 |
Const "*Goal*" $ G :: (if exists bad lits then change lits else lits) |
|
852 |
end |
|
853 |
| addLit (G,lits) = ins_term(G, lits) |
|
854 |
||
855 |
||
2952 | 856 |
(*For calculating the "penalty" to assess on a branching factor of n |
857 |
log2 seems a little too severe*) |
|
3083 | 858 |
fun log n = if n<4 then 0 else 1 + log(n div 4); |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
859 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
860 |
|
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
861 |
(*match(t,u) says whether the term u might be an instance of the pattern t |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
862 |
Used to detect "recursive" rules such as transitivity*) |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
863 |
fun match (Var _) u = true |
4065 | 864 |
| match (Const"*Goal*") (Const"Not") = true |
865 |
| match (Const"Not") (Const"*Goal*") = true |
|
866 |
| match (Const a) (Const b) = (a=b) |
|
867 |
| match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb |
|
868 |
| match (Free a) (Free b) = (a=b) |
|
869 |
| match (Bound i) (Bound j) = (i=j) |
|
870 |
| match (Abs(_,t)) (Abs(_,u)) = match t u |
|
871 |
| match (f$t) (g$u) = match f g andalso match t u |
|
872 |
| match t u = false; |
|
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
873 |
|
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
874 |
|
2854 | 875 |
(*Tableau prover based on leanTaP. Argument is a list of branches. Each |
876 |
branch contains a list of unexpanded formulae, a list of literals, and a |
|
877 |
bound on unsafe expansions.*) |
|
3030 | 878 |
fun prove (sign, cs, brs, cont) = |
2854 | 879 |
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs |
880 |
val safeList = [safe0_netpair, safep_netpair] |
|
881 |
and hazList = [haz_netpair] |
|
4065 | 882 |
fun prv (tacs, trs, choices, []) = |
883 |
cont (tacs, trs, choices) (*all branches closed!*) |
|
2854 | 884 |
| prv (tacs, trs, choices, |
2894 | 885 |
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = |
3917 | 886 |
(*apply a safe rule only (possibly allowing instantiation); |
887 |
defer any haz formulae*) |
|
2854 | 888 |
let exception PRV (*backtrack to precisely this recursion!*) |
889 |
val ntrl = !ntrail |
|
890 |
val nbrs = length brs0 |
|
891 |
val nxtVars = nextVars brs |
|
892 |
val G = norm G |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
893 |
val rules = netMkRules G vars safeList |
2854 | 894 |
(*Make a new branch, decrementing "lim" if instantiations occur*) |
2894 | 895 |
fun newBr (vars',lim') prems = |
896 |
map (fn prem => |
|
897 |
if (exists isGoal prem) |
|
898 |
then (((joinMd md prem, []) :: |
|
899 |
negOfGoals ((br, haz)::pairs)), |
|
900 |
map negOfGoal lits, |
|
901 |
vars', lim') |
|
902 |
else (((joinMd md prem, []) :: (br, haz) :: pairs), |
|
903 |
lits, vars', lim')) |
|
2854 | 904 |
prems @ |
905 |
brs |
|
906 |
(*Seek a matching rule. If unifiable then add new premises |
|
907 |
to branch.*) |
|
908 |
fun deeper [] = raise NEWBRANCHES |
|
909 |
| deeper (((P,prems),tac)::grls) = |
|
4065 | 910 |
if unify(add_term_vars(P,[]), P, G) |
3083 | 911 |
then (*P comes from the rule; G comes from the branch.*) |
912 |
let val ntrl' = !ntrail |
|
913 |
val lim' = if ntrl < !ntrail |
|
914 |
then lim - (1+log(length rules)) |
|
915 |
else lim (*discourage branching updates*) |
|
916 |
val vars = vars_in_vars vars |
|
917 |
val vars' = foldr add_terms_vars (prems, vars) |
|
918 |
val choices' = (ntrl, nbrs, PRV) :: choices |
|
919 |
val tacs' = (DETERM o (tac false)) :: tacs |
|
920 |
(*no duplication*) |
|
921 |
in |
|
4065 | 922 |
traceNew prems; traceVars sign ntrl; |
3083 | 923 |
(if null prems then (*closed the branch: prune!*) |
924 |
prv(tacs', brs0::trs, |
|
925 |
prune (nbrs, nxtVars, choices'), |
|
926 |
brs) |
|
927 |
else |
|
928 |
if lim'<0 (*faster to kill ALL the alternatives*) |
|
4065 | 929 |
then (traceMsg"Excessive branching: KILLED\n"; |
930 |
clearTo ntrl; raise NEWBRANCHES) |
|
3083 | 931 |
else |
932 |
prv(tacs', brs0::trs, choices', |
|
933 |
newBr (vars',lim') prems)) |
|
934 |
handle PRV => |
|
935 |
if ntrl < ntrl' (*Vars have been updated*) |
|
4065 | 936 |
then |
3083 | 937 |
(*Backtrack at this level. |
938 |
Reset Vars and try another rule*) |
|
939 |
(clearTo ntrl; deeper grls) |
|
940 |
else (*backtrack to previous level*) |
|
941 |
backtrack choices |
|
942 |
end |
|
943 |
else deeper grls |
|
2854 | 944 |
(*Try to close branch by unifying with head goal*) |
945 |
fun closeF [] = raise CLOSEF |
|
946 |
| closeF (L::Ls) = |
|
3083 | 947 |
case tryClose(G,L) of |
948 |
None => closeF Ls |
|
949 |
| Some tac => |
|
950 |
let val choices' = |
|
3092 | 951 |
(if !trace then (prs"branch closed"; |
4065 | 952 |
traceVars sign ntrl) |
3083 | 953 |
else (); |
954 |
prune (nbrs, nxtVars, |
|
955 |
(ntrl, nbrs, PRV) :: choices)) |
|
956 |
in prv (tac::tacs, brs0::trs, choices', brs) |
|
957 |
handle PRV => |
|
958 |
(*reset Vars and try another literal |
|
959 |
[this handler is pruned if possible!]*) |
|
960 |
(clearTo ntrl; closeF Ls) |
|
961 |
end |
|
2894 | 962 |
fun closeFl [] = raise CLOSEF |
963 |
| closeFl ((br, haz)::pairs) = |
|
964 |
closeF (map fst br) |
|
965 |
handle CLOSEF => closeF (map fst haz) |
|
966 |
handle CLOSEF => closeFl pairs |
|
3083 | 967 |
in tracing sign brs0; |
4065 | 968 |
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) |
2854 | 969 |
else |
3092 | 970 |
prv ((TRY o Data.vars_gen_hyp_subst_tac false) :: tacs, |
971 |
(*The TRY above allows the substitution to fail, e.g. if |
|
972 |
the real version is z = f(?x z). Rest of proof might |
|
973 |
still succeed!*) |
|
2854 | 974 |
brs0::trs, choices, |
3092 | 975 |
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) |
4065 | 976 |
handle DEST_EQ => closeF lits |
977 |
handle CLOSEF => closeFl ((br,haz)::pairs) |
|
978 |
handle CLOSEF => deeper rules |
|
2894 | 979 |
handle NEWBRANCHES => |
980 |
(case netMkRules G vars hazList of |
|
3917 | 981 |
[] => (*no plausible haz rules: move G to literals*) |
2894 | 982 |
prv (tacs, brs0::trs, choices, |
983 |
((br,haz)::pairs, addLit(G,lits), vars, lim) |
|
984 |
::brs) |
|
985 |
| _ => (*G admits some haz rules: try later*) |
|
986 |
prv (if isGoal G then negOfGoal_tac :: tacs |
|
987 |
else tacs, |
|
988 |
brs0::trs, choices, |
|
989 |
((br, haz@[(negOfGoal G, md)])::pairs, |
|
990 |
lits, vars, lim) :: brs)) |
|
2854 | 991 |
end |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
992 |
| prv (tacs, trs, choices, |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
993 |
(([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) = |
2894 | 994 |
(*no more "safe" formulae: transfer haz down a level*) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
995 |
prv (tacs, trs, choices, |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
996 |
((Gs,haz@haz')::pairs, lits, vars, lim) :: brs) |
2854 | 997 |
| prv (tacs, trs, choices, |
2894 | 998 |
brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) = |
999 |
(*no safe steps possible at any level: apply a haz rule*) |
|
2854 | 1000 |
let exception PRV (*backtrack to precisely this recursion!*) |
2894 | 1001 |
val H = norm H |
2854 | 1002 |
val ntrl = !ntrail |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1003 |
val rules = netMkRules H vars hazList |
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1004 |
(*new premises of haz rules may NOT be duplicated*) |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1005 |
fun newPrem (vars,recur,dup,lim') prem = |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1006 |
let val Gs' = map (fn P => (P,false)) prem |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1007 |
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1008 |
in (if recur then [(Gs',Hs')] else [(Gs',[]), ([],Hs')], |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1009 |
lits, vars, lim') |
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset
|
1010 |
end |
2854 | 1011 |
fun newBr x prems = map (newPrem x) prems @ brs |
1012 |
(*Seek a matching rule. If unifiable then add new premises |
|
1013 |
to branch.*) |
|
1014 |
fun deeper [] = raise NEWBRANCHES |
|
1015 |
| deeper (((P,prems),tac)::grls) = |
|
4065 | 1016 |
if unify(add_term_vars(P,[]), P, H) |
3083 | 1017 |
then |
1018 |
let val ntrl' = !ntrail |
|
1019 |
val vars = vars_in_vars vars |
|
1020 |
val vars' = foldr add_terms_vars (prems, vars) |
|
1021 |
(*duplicate H if md and the subgoal has new vars*) |
|
1022 |
val dup = md andalso vars' <> vars |
|
1023 |
(*any instances of P in the subgoals?*) |
|
1024 |
and recur = exists (exists (match P)) prems |
|
1025 |
val lim' = (*Decrement "lim" extra if updates occur*) |
|
1026 |
if ntrl < !ntrail then lim - (1+log(length rules)) |
|
1027 |
else lim-1 |
|
1028 |
(*It is tempting to leave "lim" UNCHANGED if |
|
1029 |
both dup and recur are false. Proofs are |
|
1030 |
found at shallower depths, but looping |
|
1031 |
occurs too often...*) |
|
3917 | 1032 |
val mayUndo = |
1033 |
(*Allowing backtracking from a rule application |
|
1034 |
if other matching rules exist, if the rule |
|
1035 |
updated variables, or if the rule did not |
|
1036 |
introduce new variables. This latter condition |
|
1037 |
means it is not a standard "gamma-rule" but |
|
1038 |
some other form of unsafe rule. Aim is to |
|
1039 |
emulate Fast_tac, which allows all unsafe steps |
|
1040 |
to be undone.*) |
|
1041 |
not(null grls) (*other rules to try?*) |
|
1042 |
orelse ntrl < ntrl' (*variables updated?*) |
|
1043 |
orelse vars=vars' (*no new Vars?*) |
|
3083 | 1044 |
val tac' = if mayUndo then tac dup |
1045 |
else DETERM o (tac dup) |
|
1046 |
in |
|
1047 |
if lim'<0 andalso not (null prems) |
|
1048 |
then (*it's faster to kill ALL the alternatives*) |
|
4065 | 1049 |
(traceMsg"Excessive branching: KILLED\n"; |
1050 |
clearTo ntrl; raise NEWBRANCHES) |
|
3083 | 1051 |
else |
4065 | 1052 |
traceNew prems; traceVars sign ntrl; |
3083 | 1053 |
prv(tac dup :: tacs, |
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
1054 |
(*FIXME: if recur then the tactic should not |
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset
|
1055 |
call rotate_tac: new formulae should be last*) |
3083 | 1056 |
brs0::trs, |
1057 |
(ntrl, length brs0, PRV) :: choices, |
|
1058 |
newBr (vars', recur, dup, lim') prems) |
|
1059 |
handle PRV => |
|
1060 |
if mayUndo |
|
1061 |
then (*reset Vars and try another rule*) |
|
1062 |
(clearTo ntrl; deeper grls) |
|
1063 |
else (*backtrack to previous level*) |
|
1064 |
backtrack choices |
|
1065 |
end |
|
1066 |
else deeper grls |
|
1067 |
in tracing sign brs0; |
|
4065 | 1068 |
if lim<1 then (traceMsg "Limit reached. "; backtrack choices) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1069 |
else deeper rules |
2854 | 1070 |
handle NEWBRANCHES => |
2894 | 1071 |
(*cannot close branch: move H to literals*) |
2854 | 1072 |
prv (tacs, brs0::trs, choices, |
2894 | 1073 |
([([], Hs)], H::lits, vars, lim)::brs) |
2854 | 1074 |
end |
1075 |
| prv (tacs, trs, choices, _ :: brs) = backtrack choices |
|
4065 | 1076 |
in init_gensym(); |
1077 |
prv ([], [], [(!ntrail, length brs, PROVE)], brs) |
|
1078 |
end; |
|
2854 | 1079 |
|
1080 |
||
2883 | 1081 |
(*Construct an initial branch.*) |
2854 | 1082 |
fun initBranch (ts,lim) = |
2894 | 1083 |
([(map (fn t => (t,true)) ts, [])], |
1084 |
[], add_terms_vars (ts,[]), lim); |
|
2854 | 1085 |
|
1086 |
||
1087 |
(*** Conversion & Skolemization of the Isabelle proof state ***) |
|
1088 |
||
1089 |
(*Make a list of all the parameters in a subgoal, even if nested*) |
|
1090 |
local open Term |
|
1091 |
in |
|
1092 |
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t |
|
1093 |
| discard_foralls t = t; |
|
1094 |
end; |
|
1095 |
||
1096 |
||
1097 |
(*List of variables not appearing as arguments to the given parameter*) |
|
1098 |
fun getVars [] i = [] |
|
1099 |
| getVars ((_,(v,is))::alist) i = |
|
1100 |
if i mem is then getVars alist i |
|
1101 |
else v :: getVars alist i; |
|
1102 |
||
1103 |
||
1104 |
(*Conversion of a subgoal: Skolemize all parameters*) |
|
4065 | 1105 |
fun fromSubgoal t = |
1106 |
let val alistVar = ref [] |
|
1107 |
and alistTVar = ref [] |
|
2854 | 1108 |
fun hdvar ((ix,(v,is))::_) = v |
1109 |
fun from lev t = |
|
1110 |
let val (ht,ts) = Term.strip_comb t |
|
1111 |
fun apply u = list_comb (u, map (from lev) ts) |
|
1112 |
fun bounds [] = [] |
|
1113 |
| bounds (Term.Bound i::ts) = |
|
1114 |
if i<lev then error"Function Var's argument not a parameter" |
|
1115 |
else i-lev :: bounds ts |
|
1116 |
| bounds ts = error"Function Var's argument not a bound variable" |
|
1117 |
in |
|
1118 |
case ht of |
|
4065 | 1119 |
Term.Const aT => apply (fromConst alistTVar aT) |
2854 | 1120 |
| Term.Free (a,_) => apply (Free a) |
1121 |
| Term.Bound i => apply (Bound i) |
|
1122 |
| Term.Var (ix,_) => |
|
4065 | 1123 |
(case (assoc_string_int(!alistVar,ix)) of |
1124 |
None => (alistVar := (ix, (ref None, bounds ts)) |
|
1125 |
:: !alistVar; |
|
1126 |
Var (hdvar(!alistVar))) |
|
2854 | 1127 |
| Some(v,is) => if is=bounds ts then Var v |
1128 |
else error("Discrepancy among occurrences of ?" |
|
1129 |
^ Syntax.string_of_vname ix)) |
|
1130 |
| Term.Abs (a,_,body) => |
|
1131 |
if null ts then Abs(a, from (lev+1) body) |
|
1132 |
else error "fromSubgoal: argument not in normal form" |
|
1133 |
end |
|
1134 |
||
1135 |
val npars = length (Logic.strip_params t) |
|
1136 |
||
1137 |
(*Skolemize a subgoal from a proof state*) |
|
1138 |
fun skoSubgoal i t = |
|
1139 |
if i<npars then |
|
1140 |
skoSubgoal (i+1) |
|
4065 | 1141 |
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), |
2854 | 1142 |
t)) |
1143 |
else t |
|
1144 |
||
1145 |
in skoSubgoal 0 (from 0 (discard_foralls t)) end; |
|
1146 |
||
1147 |
||
1148 |
(*Tactic using tableau engine and proof reconstruction. |
|
1149 |
"lim" is depth limit.*) |
|
1150 |
fun depth_tac cs lim i st = |
|
1151 |
(fullTrace:=[]; trail := []; ntrail := 0; |
|
3030 | 1152 |
let val {sign,...} = rep_thm st |
4065 | 1153 |
val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) |
2854 | 1154 |
val hyps = strip_imp_prems skoprem |
1155 |
and concl = strip_imp_concl skoprem |
|
3083 | 1156 |
fun cont (tacs,_,choices) = |
2854 | 1157 |
(case Sequence.pull(EVERY' (rev tacs) i st) of |
1158 |
None => (writeln ("PROOF FAILED for depth " ^ |
|
1159 |
Int.toString lim); |
|
1160 |
backtrack choices) |
|
1161 |
| cell => Sequence.seqof(fn()=> cell)) |
|
3030 | 1162 |
in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) |
2854 | 1163 |
end |
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3244
diff
changeset
|
1164 |
handle PROVE => Sequence.null); |
2854 | 1165 |
|
1166 |
fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0); |
|
1167 |
||
4078 | 1168 |
fun Blast_tac i = blast_tac (Data.claset()) i; |
2854 | 1169 |
|
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1170 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1171 |
(*** For debugging: these apply the prover to a subgoal and return |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1172 |
the resulting tactics, trace, etc. ***) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1173 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1174 |
(*Translate subgoal i from a proof state*) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1175 |
fun trygl cs lim i = |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1176 |
(fullTrace:=[]; trail := []; ntrail := 0; |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1177 |
let val st = topthm() |
3030 | 1178 |
val {sign,...} = rep_thm st |
4065 | 1179 |
val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1180 |
val hyps = strip_imp_prems skoprem |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1181 |
and concl = strip_imp_concl skoprem |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1182 |
in timeap prove |
3030 | 1183 |
(sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I) |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1184 |
end |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1185 |
handle Subscript => error("There is no subgoal " ^ Int.toString i)); |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1186 |
|
4078 | 1187 |
fun Trygl lim i = trygl (Data.claset()) lim i; |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1188 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1189 |
(*Read a string to make an initial, singleton branch*) |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1190 |
fun readGoal sign s = read_cterm sign (s,propT) |> |
4065 | 1191 |
term_of |> fromTerm |> rand |> mkGoal; |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1192 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1193 |
fun tryInThy thy lim s = |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1194 |
(fullTrace:=[]; trail := []; ntrail := 0; |
3030 | 1195 |
timeap prove (sign_of thy, |
4078 | 1196 |
Data.claset(), |
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1197 |
[initBranch ([readGoal (sign_of thy) s], lim)], |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1198 |
I)); |
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1199 |
|
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset
|
1200 |
|
2854 | 1201 |
end; |
1202 |