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