author  paulson 
Mon, 14 Nov 2005 18:25:34 +0100  
changeset 18171  c4f873d65603 
parent 18146  47463b1825c6 
child 18177  7041d038acb0 
permissions  rwrr 
4078  1 
(* Title: Provers/blast.ML 
2894  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3083  4 
Copyright 1997 University of Cambridge 
2894  5 

6 
Generic tableau prover with proof reconstruction 

7 

2854  8 
SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? 
2894  9 
Needs explicit instantiation of assumptions? 
10 

18171  11 
Given the typeargs system, constructor Const could be eliminated, with 
12 
TConst replaced by a constructor that takes the typargs list as an argument. 

13 
However, Const is heavily used for logical connectives. 

2894  14 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

15 
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

16 
Blast_tac... 
4651  17 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
18 
this restriction is intrinsic 

2894  19 
* ignores elimination rules that don't have the correct format 
20 
(conclusion must be a formula variable) 

21 
* ignores types, which can make HOL proofs fail 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

22 
* rules must not require higherorder unification, e.g. apply_type in ZF 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

23 
+ 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

24 
* its proof strategy is more general but can actually be slower 
2894  25 

26 
Known problems: 

3092  27 
"Recursive" chains of rules can sometimes exclude other unsafe formulae 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

28 
from expansion. This happens because newlycreated formulae always 
3092  29 
have priority over existing ones. But obviously recursive rules 
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset

30 
such as transitivity are treated specially to prevent this. Sometimes 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

31 
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

32 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

33 
With substition for equalities (hyp_subst_tac): 
3092  34 
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

35 
back to the list of safe formulae. 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

36 
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

37 
"no DETERM" flag would prevent proofs failing here. 
2854  38 
*) 
39 

40 
(*Should be a type abbreviation?*) 

41 
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; 

42 

43 

44 
(*Assumptions about constants: 

45 
The negation symbol is "Not" 

46 
The equality symbol is "op =" 

47 
The istrue judgement symbol is "Trueprop" 

48 
There are no constants named "*Goal* or "*False*" 

49 
*) 

50 
signature BLAST_DATA = 

51 
sig 

52 
type claset 

53 
val notE : thm (* [ ~P; P ] ==> R *) 

54 
val ccontr : thm 

55 
val contr_tac : int > tactic 

56 
val dup_intr : thm > thm 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

57 
val hyp_subst_tac : bool ref > int > tactic 
4078  58 
val claset : unit > claset 
4653  59 
val rep_cs : (* dependent on classical.ML *) 
2854  60 
claset > {safeIs: thm list, safeEs: thm list, 
61 
hazIs: thm list, hazEs: thm list, 

4651  62 
swrappers: (string * wrapper) list, 
63 
uwrappers: (string * wrapper) list, 

2854  64 
safe0_netpair: netpair, safep_netpair: netpair, 
12403  65 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} 
7272  66 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  67 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 
2854  68 
end; 
69 

70 

71 
signature BLAST = 

72 
sig 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

73 
type claset 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

74 
exception TRANS of string (*reports translation errors*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

75 
datatype term = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

76 
Const of string 
4065  77 
 TConst of string * term 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

78 
 Skolem of string * term option ref list 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

79 
 Free of string 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

80 
 Var of term option ref 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

81 
 Bound of int 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

82 
 Abs of string*term 
17795  83 
 $ of term*term; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

84 
type branch 
2883  85 
val depth_tac : claset > int > int > tactic 
15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

86 
val depth_limit : int ref 
2883  87 
val blast_tac : claset > int > tactic 
88 
val Blast_tac : int > tactic 

5926  89 
val setup : (theory > theory) list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

90 
(*debugging tools*) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

91 
val stats : bool ref 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

92 
val trace : bool ref 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

93 
val fullTrace : branch list list ref 
4065  94 
val fromType : (indexname * term) list ref > Term.typ > term 
95 
val fromTerm : Term.term > term 

96 
val fromSubgoal : Term.term > term 

97 
val instVars : term > (unit > unit) 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

98 
val toTerm : int > term > Term.term 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

99 
val readGoal : Sign.sg > string > term 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

100 
val tryInThy : theory > int > string > 
3083  101 
(int>tactic) list * branch list list * (int*int*exn) list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

102 
val trygl : claset > int > int > 
3083  103 
(int>tactic) list * branch list list * (int*int*exn) list 
104 
val Trygl : int > int > 

105 
(int>tactic) list * branch list list * (int*int*exn) list 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

106 
val normBr : branch > branch 
2854  107 
end; 
108 

109 

3092  110 
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854  111 
struct 
112 

113 
type claset = Data.claset; 

114 

4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

115 
val trace = ref false 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

116 
and stats = ref false; (*for runtime and search statistics*) 
2854  117 

118 
datatype term = 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

119 
Const of string 
4065  120 
 TConst of string * term (*type of overloaded constantas a term!*) 
2854  121 
 Skolem of string * term option ref list 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

122 
 Free of string 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

123 
 Var of term option ref 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

124 
 Bound of int 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

125 
 Abs of string*term 
5613  126 
 op $ of term*term; 
2854  127 

128 

129 
(** Basic syntactic operations **) 

130 

131 
fun is_Var (Var _) = true 

132 
 is_Var _ = false; 

133 

134 
fun dest_Var (Var x) = x; 

135 

136 
fun rand (f$x) = x; 

137 

138 
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *) 

15570  139 
val list_comb : term * term list > term = Library.foldl (op $); 
2854  140 

141 
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tailrecursive*) 

142 
fun strip_comb u : term * term list = 

143 
let fun stripc (f$t, ts) = stripc (f, t::ts) 

144 
 stripc x = x 

145 
in stripc(u,[]) end; 

146 

147 
(* maps f(t1,...,tn) to f , which is never a combination *) 

148 
fun head_of (f$t) = head_of f 

149 
 head_of u = u; 

150 

151 

152 
(** Particular constants **) 

153 

154 
fun negate P = Const"Not" $ P; 

155 

156 
fun mkGoal P = Const"*Goal*" $ P; 

157 

158 
fun isGoal (Const"*Goal*" $ _) = true 

159 
 isGoal _ = false; 

160 

18171  161 
val boolT = 
162 
case term_vars (hd (prems_of Data.notE)) of 

163 
[Term.Var(_, Type(s, []))] => s 

164 
 _ => error ("Theorem notE is illformed: " ^ string_of_thm Data.notE); 

165 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

166 
val Trueprop = Term.Const("Trueprop", Type(boolT,[])>propT); 
2854  167 
fun mk_tprop P = Term.$ (Trueprop, P); 
168 

169 
fun isTrueprop (Term.Const("Trueprop",_)) = true 

170 
 isTrueprop _ = false; 

171 

172 

4065  173 
(*** Dealing with overloaded constants ***) 
2854  174 

4065  175 
(*alist is a map from TVar names to Vars. We need to unify the TVars 
176 
faithfully in order to track overloading*) 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

177 
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts) 
4065  178 
 fromType alist (Term.TFree(a,_)) = Free a 
179 
 fromType alist (Term.TVar (ixn,_)) = 

17271  180 
(case (AList.lookup (op =) (!alist) ixn) of 
15531  181 
NONE => let val t' = Var(ref NONE) 
4065  182 
in alist := (ixn, t') :: !alist; t' 
183 
end 

15531  184 
 SOME v => v) 
2854  185 

17993  186 
(*refer to the theory in which blast is initialized*) 
18146  187 
val typargs = ref (fn ((_, T): string * typ) => [T]); 
2854  188 

13550  189 
(*Convert a Term.Const to a Blast.Const or Blast.TConst, 
18058
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

190 
converting its type to a Blast.term in the latter case.*) 
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

191 
fun fromConst alist (a as "all", _) = Const a 
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

192 
 fromConst alist (a, T) = 
18146  193 
(case ! typargs (a, T) of 
18058
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

194 
[] => Const a 
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

195 
 [T] => TConst (a, fromType alist T) 
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

196 
 Ts => TConst (a, list_comb (Const "*typargs*", map (fromType alist) Ts))); 
2854  197 

198 

199 
(*Tests whether 2 terms are alphaconvertible; chases instantiations*) 

200 
fun (Const a) aconv (Const b) = a=b 

4065  201 
 (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb 
2854  202 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
203 
 (Free a) aconv (Free b) = a=b 

15531  204 
 (Var(ref(SOME t))) aconv u = t aconv u 
205 
 t aconv (Var(ref(SOME u))) = t aconv u 

2854  206 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
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) 

210 
 _ aconv _ = false; 

211 

212 

213 
fun mem_term (_, []) = false 

214 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts); 

215 

216 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 

217 

218 
fun mem_var (v: term option ref, []) = false 

219 
 mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); 

220 

221 
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; 

222 

223 

224 
(** Vars **) 

225 

226 
(*Accumulates the Vars in the term, suppressing duplicates*) 

227 
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) 

15531  228 
 add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) 
229 
 add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) 

4065  230 
 add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) 
2854  231 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
232 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

233 
 add_term_vars (_, vars) = vars 

234 
(*Term list version. [The fold functionals are slow]*) 

235 
and add_terms_vars ([], vars) = vars 

236 
 add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) 

237 
(*Var list version.*) 

238 
and add_vars_vars ([], vars) = vars 

15531  239 
 add_vars_vars (ref (SOME u) :: vs, vars) = 
2854  240 
add_vars_vars (vs, add_term_vars(u,vars)) 
15531  241 
 add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) 
2854  242 
add_vars_vars (vs, ins_var (v, vars)); 
243 

244 

245 
(*Chase assignments in "vars"; return a list of unassigned variables*) 

246 
fun vars_in_vars vars = add_vars_vars(vars,[]); 

247 

248 

249 

250 
(*increment a term's nonlocal bound variables 

251 
inc is increment for bound variables 

252 
lev is level at which a bound variable is considered 'loose'*) 

253 
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 

254 
 incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body)) 

255 
 incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

256 
 incr_bv (inc, lev, u) = u; 

257 

258 
fun incr_boundvars 0 t = t 

259 
 incr_boundvars inc t = incr_bv(inc,0,t); 

260 

261 

262 
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. 

263 
(Bound 0) is loose at level 0 *) 

264 
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js 

265 
else (ilev) ins_int js 

266 
 add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js) 

267 
 add_loose_bnos (f$t, lev, js) = 

268 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 

269 
 add_loose_bnos (_, _, js) = js; 

270 

271 
fun loose_bnos t = add_loose_bnos (t, 0, []); 

272 

273 
fun subst_bound (arg, t) : term = 

274 
let fun subst (t as Bound i, lev) = 

275 
if i<lev then t (*var is locally bound*) 

276 
else if i=lev then incr_boundvars lev arg 

277 
else Bound(i1) (*loose: change it*) 

278 
 subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1)) 

279 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 

280 
 subst (t,lev) = t 

281 
in subst (t,0) end; 

282 

283 

3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

284 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  285 
fun norm t = case t of 
2952  286 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
4065  287 
 TConst(a,aT) => TConst(a, norm aT) 
15531  288 
 (Var (ref NONE)) => t 
289 
 (Var (ref (SOME u))) => norm u 

2854  290 
 (f $ u) => (case norm f of 
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

291 
Abs(_,body) => norm (subst_bound (u, body)) 
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

292 
 nf => nf $ norm u) 
2854  293 
 _ => t; 
294 

295 

296 
(*Weak (onelevel) normalize for use in unification*) 

297 
fun wkNormAux t = case t of 

298 
(Var v) => (case !v of 

15531  299 
SOME u => wkNorm u 
300 
 NONE => t) 

2854  301 
 (f $ u) => (case wkNormAux f of 
302 
Abs(_,body) => wkNorm (subst_bound (u, body)) 

303 
 nf => nf $ u) 

2952  304 
 Abs (a,body) => (*etacontract if possible*) 
305 
(case wkNormAux body of 

306 
nb as (f $ t) => 

307 
if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0 

308 
then Abs(a,nb) 

309 
else wkNorm (incr_boundvars ~1 f) 

3092  310 
 nb => Abs (a,nb)) 
2854  311 
 _ => t 
312 
and wkNorm t = case head_of t of 

313 
Const _ => t 

4065  314 
 TConst _ => t 
2854  315 
 Skolem(a,args) => t 
316 
 Free _ => t 

317 
 _ => wkNormAux t; 

318 

319 

5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

320 
(*Does variable v occur in u? For unification. 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

321 
Dangling bound vars are also forbidden.*) 
2854  322 
fun varOccur v = 
5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

323 
let fun occL lev [] = false (*same as (exists occ), but faster*) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

324 
 occL lev (u::us) = occ lev u orelse occL lev us 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

325 
and occ lev (Var w) = 
2854  326 
v=w orelse 
15531  327 
(case !w of NONE => false 
328 
 SOME u => occ lev u) 

5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

329 
 occ lev (Skolem(_,args)) = occL lev (map Var args) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

330 
(*ignore TConst, since term variables can't occur in types (?) *) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

331 
 occ lev (Bound i) = lev <= i 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

332 
 occ lev (Abs(_,u)) = occ (lev+1) u 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

333 
 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

334 
 occ lev _ = false; 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

335 
in occ 0 end; 
2854  336 

337 
exception UNIFY; 

338 

339 
val trail = ref [] : term option ref list ref; 

340 
val ntrail = ref 0; 

341 

342 

343 
(*Restore the trail to some previous state: for backtracking*) 

344 
fun clearTo n = 

3083  345 
while !ntrail<>n do 
15531  346 
(hd(!trail) := NONE; 
2854  347 
trail := tl (!trail); 
348 
ntrail := !ntrail  1); 

349 

350 

351 
(*Firstorder unification with bound variables. 

352 
"vars" is a list of variables local to the rule and NOT to be put 

353 
on the trail (no point in doing so) 

354 
*) 

4065  355 
fun unify(vars,t,u) = 
2854  356 
let val n = !ntrail 
357 
fun update (t as Var v, u) = 

358 
if t aconv u then () 

359 
else if varOccur v u then raise UNIFY 

15531  360 
else if mem_var(v, vars) then v := SOME u 
2854  361 
else (*avoid updating Vars in the branch if possible!*) 
362 
if is_Var u andalso mem_var(dest_Var u, vars) 

15531  363 
then dest_Var u := SOME t 
364 
else (v := SOME u; 

2854  365 
trail := v :: !trail; ntrail := !ntrail + 1) 
366 
fun unifyAux (t,u) = 

367 
case (wkNorm t, wkNorm u) of 

368 
(nt as Var v, nu) => update(nt,nu) 

369 
 (nu, nt as Var v) => update(nt,nu) 

4065  370 
 (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt) 
371 
else raise UNIFY 

2854  372 
 (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') 
373 
(*NB: can yield unifiers having dangling Bound vars!*) 

374 
 (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) 

375 
 (nt, nu) => if nt aconv nu then () else raise UNIFY 

3083  376 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  377 
end; 
378 

379 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

380 
(*Convert from "real" terms to prototerms; etacontract. 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

381 
Code is similar to fromSubgoal.*) 
4065  382 
fun fromTerm t = 
383 
let val alistVar = ref [] 

384 
and alistTVar = ref [] 

385 
fun from (Term.Const aT) = fromConst alistTVar aT 

2854  386 
 from (Term.Free (a,_)) = Free a 
387 
 from (Term.Bound i) = Bound i 

388 
 from (Term.Var (ixn,T)) = 

17271  389 
(case (AList.lookup (op =) (!alistVar) ixn) of 
15531  390 
NONE => let val t' = Var(ref NONE) 
4065  391 
in alistVar := (ixn, t') :: !alistVar; t' 
2854  392 
end 
15531  393 
 SOME v => v) 
2854  394 
 from (Term.Abs (a,_,u)) = 
395 
(case from u of 

396 
u' as (f $ Bound 0) => 

397 
if (0 mem_int loose_bnos f) then Abs(a,u') 

398 
else incr_boundvars ~1 f 

399 
 u' => Abs(a,u')) 

400 
 from (Term.$ (f,u)) = from f $ from u 

401 
in from t end; 

402 

4065  403 
(*A debugging function: replaces all Vars by dummy Frees for visual inspection 
404 
of whether they are distinct. Function revert undoes the assignments.*) 

405 
fun instVars t = 

12902  406 
let val name = ref "a" 
4065  407 
val updated = ref [] 
408 
fun inst (TConst(a,t)) = inst t 

15531  409 
 inst (Var(v as ref NONE)) = (updated := v :: (!updated); 
410 
v := SOME (Free ("?" ^ !name)); 

12902  411 
name := Symbol.bump_string (!name)) 
4065  412 
 inst (Abs(a,t)) = inst t 
413 
 inst (f $ u) = (inst f; inst u) 

414 
 inst _ = () 

15570  415 
fun revert() = List.app (fn v => v:=NONE) (!updated) 
4065  416 
in inst t; revert end; 
417 

418 

2854  419 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
420 
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 

421 
A :: strip_imp_prems B 

422 
 strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B 

423 
 strip_imp_prems _ = []; 

424 

425 
(* A1==>...An==>B goes to B, where B is not an implication *) 

426 
fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B 

427 
 strip_imp_concl (Const"Trueprop" $ A) = A 

428 
 strip_imp_concl A = A : term; 

429 

430 

431 
(*** Conversion of Elimination Rules to Tableau Operations ***) 

432 

9170  433 
exception ElimBadConcl and ElimBadPrem; 
434 

435 
(*The conclusion becomes the goal/negated assumption *False*: delete it! 

436 
If we don't find it then the premise is illformed and could cause 

437 
PROOF FAILED*) 

438 
fun delete_concl [] = raise ElimBadPrem 

15531  439 
 delete_concl (Const "*Goal*" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = 
9170  440 
Ps 
15531  441 
 delete_concl (Const "Not" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = 
9170  442 
Ps 
443 
 delete_concl (P::Ps) = P :: delete_concl Ps; 

2854  444 

445 
fun skoPrem vars (Const "all" $ Abs (_, P)) = 

446 
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) 

447 
 skoPrem vars P = P; 

448 

449 
fun convertPrem t = 

9170  450 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  451 

452 
(*Expects elimination rules to have a formula variable as conclusion*) 

453 
fun convertRule vars t = 

454 
let val (P::Ps) = strip_imp_prems t 

455 
val Var v = strip_imp_concl t 

15531  456 
in v := SOME (Const"*False*"); 
2854  457 
(P, map (convertPrem o skoPrem vars) Ps) 
9170  458 
end 
459 
handle Bind => raise ElimBadConcl; 

2854  460 

461 

462 
(*Like dup_elim, but puts the duplicated major premise FIRST*) 

17257
0ab67cb765da
introduced binding priority 1 for linear combinators etc.
haftmann
parents:
16976
diff
changeset

463 
fun rev_dup_elim th = (th RSN (2, revcut_rl)) > assumption 2 > Seq.hd; 
2854  464 

465 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

466 
(*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

467 
local 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

468 
(*Count new hyps so that they can be rotated*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

469 
fun nNewHyps [] = 0 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

470 
 nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

471 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  472 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

473 
fun rot_tac [] i st = Seq.single st 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

474 
 rot_tac (0::ks) i st = rot_tac ks (i+1) st 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

475 
 rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st); 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

476 
in 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

477 
fun rot_subgoals_tac (rot, rl) = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

478 
rot_tac (if rot then map nNewHyps rl else []) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

479 
end; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

480 

2854  481 

2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

482 
fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i; 
2854  483 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

484 
(*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

485 
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

486 
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

487 
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

488 

871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

489 
(*Tableau rule from elimination rule. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

490 
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

491 
Flag "dup" requests duplication of the affected formula.*) 
2854  492 
fun fromRule vars rl = 
4065  493 
let val trl = rl > rep_thm > #prop > fromTerm > convertRule vars 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

494 
fun tac (upd, dup,rot) i = 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

495 
emtac upd (if dup then rev_dup_elim rl else rl) i 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

496 
THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

497 
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

498 
in Option.SOME (trl, tac) end 
9170  499 
handle ElimBadPrem => (*reject: prems don't preserve conclusion*) 
500 
(warning("Ignoring weak elimination rule\n" ^ string_of_thm rl); 

501 
Option.NONE) 

502 
 ElimBadConcl => (*ignore: conclusion is not just a variable*) 

503 
(if !trace then (warning("Ignoring illformed elimination rule:\n" ^ 

504 
"conclusion should be a variable\n" ^ string_of_thm rl)) 

505 
else (); 

506 
Option.NONE); 

2854  507 

508 

3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

509 
(*** Conversion of Introduction Rules ***) 
2854  510 

511 
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; 

512 

513 
fun convertIntrRule vars t = 

514 
let val Ps = strip_imp_prems t 

515 
val P = strip_imp_concl t 

516 
in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 

517 
end; 

518 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

519 
(*Tableau rule from introduction rule. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

520 
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

521 
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

522 
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

523 
introduction rules.*) 
2854  524 
fun fromIntrRule vars rl = 
4065  525 
let val trl = rl > rep_thm > #prop > fromTerm > convertIntrRule vars 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

526 
fun tac (upd,dup,rot) i = 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

527 
rmtac upd (if dup then Data.dup_intr rl else rl) i 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

528 
THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

529 
rot_subgoals_tac (rot, #2 trl) i 
2854  530 
in (trl, tac) end; 
531 

532 

3030  533 
val dummyVar = Term.Var (("etc",0), dummyT); 
2854  534 

535 
(*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

536 
Ignore abstractions; identify all Vars; STOP at given depth*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

537 
fun toTerm 0 _ = dummyVar 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

538 
 toTerm d (Const a) = Term.Const (a,dummyT) 
4065  539 
 toTerm d (TConst(a,_)) = Term.Const (a,dummyT) (*no need to convert type*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

540 
 toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

541 
 toTerm d (Free a) = Term.Free (a,dummyT) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

542 
 toTerm d (Bound i) = Term.Bound i 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

543 
 toTerm d (Var _) = dummyVar 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

544 
 toTerm d (Abs(a,_)) = dummyVar 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

545 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  546 

547 

548 
fun netMkRules P vars (nps: netpair list) = 

549 
case P of 

550 
(Const "*Goal*" $ G) => 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

551 
let val pG = mk_tprop (toTerm 2 G) 
2854  552 
val intrs = List.concat 
553 
(map (fn (inet,_) => Net.unify_term inet pG) 

554 
nps) 

11783  555 
in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end 
2854  556 
 _ => 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

557 
let val pP = mk_tprop (toTerm 3 P) 
2854  558 
val elims = List.concat 
559 
(map (fn (_,enet) => Net.unify_term enet pP) 

560 
nps) 

11783  561 
in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end; 
2854  562 

3092  563 

564 
(*Pending formulae carry md (may duplicate) flags*) 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

565 
type branch = 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

566 
{pairs: ((term*bool) list * (*safe formulae on this level*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

567 
(term*bool) list) list, (*haz formulae on this level*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

568 
lits: term list, (*literals: irreducible formulae*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

569 
vars: term option ref list, (*variables occurring in branch*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

570 
lim: int}; (*resource limit*) 
3092  571 

572 
val fullTrace = ref[] : branch list list ref; 

573 

574 
(*Normalize a branchfor tracing*) 

575 
fun norm2 (G,md) = (norm G, md); 

576 

577 
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); 

578 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

579 
fun normBr {pairs, lits, vars, lim} = 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

580 
{pairs = map normLev pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

581 
lits = map norm lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

582 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

583 
lim = lim}; 
3092  584 

585 

4065  586 
val dummyTVar = Term.TVar(("a",0), []); 
3092  587 
val dummyVar2 = Term.Var(("var",0), dummyT); 
588 

4065  589 
(*convert Blast_tac's type representation to real types for tracing*) 
590 
fun showType (Free a) = Term.TFree (a,[]) 

591 
 showType (Var _) = dummyTVar 

592 
 showType t = 

593 
(case strip_comb t of 

594 
(Const a, us) => Term.Type(a, map showType us) 

595 
 _ => dummyT); 

596 

597 
(*Display toplevel overloading if any*) 

15531  598 
fun topType (TConst(a,t)) = SOME (showType t) 
4065  599 
 topType (Abs(a,t)) = topType t 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

600 
 topType (f $ u) = (case topType f of NONE => topType u  some => some) 
15531  601 
 topType _ = NONE; 
4065  602 

603 

3092  604 
(*Convert from prototerms to ordinary terms with dummy types for tracing*) 
605 
fun showTerm d (Const a) = Term.Const (a,dummyT) 

4065  606 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  607 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
608 
 showTerm d (Free a) = Term.Free (a,dummyT) 

609 
 showTerm d (Bound i) = Term.Bound i 

15531  610 
 showTerm d (Var(ref(SOME u))) = showTerm d u 
611 
 showTerm d (Var(ref NONE)) = dummyVar2 

3092  612 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
613 
else Term.Abs(a, dummyT, showTerm (d1) t) 

614 
 showTerm d (f $ u) = if d=0 then dummyVar 

615 
else Term.$ (showTerm d f, showTerm (d1) u); 

616 

4065  617 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  618 

4065  619 
fun traceTerm sign t = 
620 
let val t' = norm t 

621 
val stm = string_of sign 8 t' 

622 
in 

623 
case topType t' of 

15531  624 
NONE => stm (*no type to attach*) 
625 
 SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T 

4065  626 
end; 
3092  627 

628 

629 
(*Print tracing information at each iteration of prover*) 

630 
fun tracing sign brs = 

14984  631 
let fun printPairs (((G,_)::_,_)::_) = immediate_output(traceTerm sign G) 
632 
 printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)") 

3092  633 
 printPairs _ = () 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

634 
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 
3092  635 
(fullTrace := brs0 :: !fullTrace; 
15570  636 
List.app (fn _ => immediate_output "+") brs; 
14984  637 
immediate_output (" [" ^ Int.toString lim ^ "] "); 
3092  638 
printPairs pairs; 
639 
writeln"") 

640 
in if !trace then printBrs (map normBr brs) else () 

641 
end; 

642 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

643 
fun traceMsg s = if !trace then writeln s else (); 
4065  644 

3092  645 
(*Tracing: variables updated in the last branch operation?*) 
4065  646 
fun traceVars sign ntrl = 
647 
if !trace then 

648 
(case !ntrailntrl of 

649 
0 => () 

14984  650 
 1 => immediate_output"\t1 variable UPDATED:" 
651 
 n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); 

4065  652 
(*display the instantiations themselves, though no variable names*) 
15570  653 
List.app (fn v => immediate_output(" " ^ string_of sign 4 (valOf (!v)))) 
4065  654 
(List.take(!trail, !ntrailntrl)); 
655 
writeln"") 

3092  656 
else (); 
657 

658 
(*Tracing: how many new branches are created?*) 

659 
fun traceNew prems = 

660 
if !trace then 

661 
case length prems of 

14984  662 
0 => immediate_output"branch closed by rule" 
663 
 1 => immediate_output"branch extended (1 new subgoal)" 

664 
 n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals") 

3092  665 
else (); 
666 

667 

668 

2854  669 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
670 

671 
(*Replace the ATOMIC term "old" by "new" in t*) 

672 
fun subst_atomic (old,new) t = 

15531  673 
let fun subst (Var(ref(SOME u))) = subst u 
2854  674 
 subst (Abs(a,body)) = Abs(a, subst body) 
675 
 subst (f$t) = subst f $ subst t 

676 
 subst t = if t aconv old then new else t 

677 
in subst t end; 

678 

679 
(*Etacontract a term from outside: just enough to reduce it to an atom*) 

680 
fun eta_contract_atom (t0 as Abs(a, body)) = 

681 
(case eta_contract2 body of 

682 
f $ Bound 0 => if (0 mem_int loose_bnos f) then t0 

683 
else eta_contract_atom (incr_boundvars ~1 f) 

684 
 _ => t0) 

685 
 eta_contract_atom t = t 

686 
and eta_contract2 (f$t) = f $ eta_contract_atom t 

687 
 eta_contract2 t = eta_contract_atom t; 

688 

689 

690 
(*When can we safely delete the equality? 

691 
Not if it equates two constants; consider 0=1. 

692 
Not if it resembles x=t[x], since substitution does not eliminate x. 

693 
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) 

694 
Prefer to eliminate Bound variables if possible. 

695 
Result: true = use as is, false = reorient first *) 

696 

4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

697 
(*Can t occur in u? For substitution. 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

698 
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

699 
REFLEXIVE because hyp_subst_tac fails on x=x.*) 
2854  700 
fun substOccur t = 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

701 
let (*NO vars are permitted in u except the arguments of t, if it is 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

702 
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

703 
be instantiated to a cycle. For example, x=?a is rejected because ?a 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

704 
could be instantiated to Suc(x).*) 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

705 
val vars = case t of 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

706 
Skolem(_,vars) => vars 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

707 
 _ => [] 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

708 
fun occEq u = (t aconv u) orelse occ u 
15531  709 
and occ (Var(ref(SOME u))) = occEq u 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

710 
 occ (Var v) = not (mem_var (v, vars)) 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

711 
 occ (Abs(_,u)) = occEq u 
2854  712 
 occ (f$u) = occEq u orelse occEq f 
713 
 occ (_) = false; 

714 
in occEq end; 

715 

3092  716 
exception DEST_EQ; 
717 

718 
(*Take apart an equality (plain or overloaded). NO constant Trueprop*) 

719 
fun dest_eq (Const "op =" $ t $ u) = 

720 
(eta_contract_atom t, eta_contract_atom u) 

4065  721 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  722 
(eta_contract_atom t, eta_contract_atom u) 
723 
 dest_eq _ = raise DEST_EQ; 

724 

4196
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

725 
(*Reject the equality if u occurs in (or equals!) t*) 
2854  726 
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; 
727 

728 
(*IF the goal is an equality with a substitutable variable 

729 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  730 
fun orientGoal (t,u) = case (t,u) of 
2854  731 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
732 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

733 
 (Free _, _) => check(t,u,(t,u)) (*eliminates t*) 

734 
 (_, Free _) => check(u,t,(u,t)) (*eliminates u*) 

735 
 _ => raise DEST_EQ; 

736 

2894  737 
(*Substitute through the branch if an equality goal (else raise DEST_EQ). 
738 
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

739 
they should go: this could make proofs fail.*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

740 
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092  741 
let val (t,u) = orientGoal(dest_eq G) 
742 
val subst = subst_atomic (t,u) 

2854  743 
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

744 
(*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

745 
fun subForm ((G,md), (changed, pairs)) = 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

746 
let val nG = subst G 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

747 
in if nG aconv G then (changed, (G,md)::pairs) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

748 
else ((nG,md)::changed, pairs) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

749 
end 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

750 
(*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

751 
fun subFrame ((Gs,Hs), (changed, frames)) = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

752 
let val (changed', Gs') = foldr subForm (changed, []) Gs 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

753 
val (changed'', Hs') = 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

754 
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

755 
(*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

756 
fun subLit (lit, (changed, nlits)) = 
2854  757 
let val nlit = subst lit 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

758 
in if nlit aconv lit then (changed, nlit::nlits) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

759 
else ((nlit,true)::changed, nlits) 
2854  760 
end 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

761 
val (changed, lits') = foldr subLit ([], []) lits 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

762 
val (changed', pairs') = foldr subFrame (changed, []) pairs 
3092  763 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
764 
" for " ^ traceTerm sign t ^ " in branch" ) 

765 
else (); 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

766 
{pairs = (changed',[])::pairs', (*affected formulas, and others*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

767 
lits = lits', (*unaffected literals*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

768 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

769 
lim = lim} 
2854  770 
end; 
771 

772 

773 
exception NEWBRANCHES and CLOSEF; 

774 

775 
exception PROVE; 

776 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

777 
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

778 
val contr_tac = ematch_tac [Data.notE] THEN' 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

779 
(eq_assume_tac ORELSE' assume_tac); 
2854  780 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

781 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  782 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
783 

784 
(*Try to unify complementary literals and return the corresponding tactic. *) 

3083  785 
fun tryClose (Const"*Goal*" $ G, L) = 
15531  786 
if unify([],G,L) then SOME eAssume_tac else NONE 
3083  787 
 tryClose (G, Const"*Goal*" $ L) = 
15531  788 
if unify([],G,L) then SOME eAssume_tac else NONE 
3083  789 
 tryClose (Const"Not" $ G, L) = 
15531  790 
if unify([],G,L) then SOME eContr_tac else NONE 
3083  791 
 tryClose (G, Const"Not" $ L) = 
15531  792 
if unify([],G,L) then SOME eContr_tac else NONE 
793 
 tryClose _ = NONE; 

2854  794 

795 

796 
(*Were there Skolem terms in the premise? Must NOT chase Vars*) 

797 
fun hasSkolem (Skolem _) = true 

798 
 hasSkolem (Abs (_,body)) = hasSkolem body 

799 
 hasSkolem (f$t) = hasSkolem f orelse hasSkolem t 

800 
 hasSkolem _ = false; 

801 

802 
(*Attach the right "may duplicate" flag to new formulae: if they contain 

803 
Skolem terms then allow duplication.*) 

804 
fun joinMd md [] = [] 

805 
 joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; 

806 

2894  807 
(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like 
808 
Ex(P) is duplicated as the assumption ~Ex(P). *) 

809 
fun negOfGoal (Const"*Goal*" $ G) = negate G 

810 
 negOfGoal G = G; 

811 

812 
fun negOfGoal2 (G,md) = (negOfGoal G, md); 

813 

814 
(*Converts all Goals to Nots in the safe parts of a branch. They could 

815 
have been moved there from the literals list after substitution (equalSubst). 

816 
There can be at most onethis function could be made more efficient.*) 

817 
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; 

818 

819 
(*Tactic. Convert *Goal* to negated assumption in FIRST position*) 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

820 
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

821 
rotate_tac ~1 i; 
2894  822 

2854  823 

824 
(** Backtracking and Pruning **) 

825 

826 
(*clashVar vars (n,trail) determines whether any of the last n elements 

827 
of "trail" occur in "vars" OR in their instantiations*) 

828 
fun clashVar [] = (fn _ => false) 

829 
 clashVar vars = 

830 
let fun clash (0, _) = false 

831 
 clash (_, []) = false 

832 
 clash (n, v::vs) = exists (varOccur v) vars orelse clash(n1,vs) 

833 
in clash end; 

834 

835 

836 
(*nbrs = # of branches just prior to closing this one. Delete choice points 

837 
for goals proved by the latest inference, provided NO variables in the 

838 
next branch have been updated.*) 

839 
fun prune (1, nxtVars, choices) = choices (*DON'T prune at very end: allow 

840 
backtracking over bad proofs*) 

17795  841 
 prune (nbrs: int, nxtVars, choices) = 
2854  842 
let fun traceIt last = 
843 
let val ll = length last 

844 
and lc = length choices 

845 
in if !trace andalso ll<lc then 

3083  846 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  847 
last) 
848 
else last 

849 
end 

850 
fun pruneAux (last, _, _, []) = last 

3083  851 
 pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) = 
2854  852 
if nbrs' < nbrs 
853 
then last (*don't backtrack beyond first solution of goal*) 

854 
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices) 

855 
else (* nbrs'=nbrs *) 

856 
if clashVar nxtVars (ntrlntrl', trl) then last 

857 
else (*no clashes: can go back at least this far!*) 

858 
pruneAux(choices, ntrl', List.drop(trl, ntrlntrl'), 

859 
choices) 

860 
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; 

861 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

862 
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

863 
 nextVars [] = []; 
2854  864 

3083  865 
fun backtrack (choices as (ntrl, nbrs, exn)::_) = 
866 
(if !trace then (writeln ("Backtracking; now there are " ^ 

867 
Int.toString nbrs ^ " branches")) 

868 
else (); 

869 
raise exn) 

870 
 backtrack _ = raise PROVE; 

2854  871 

2894  872 
(*Add the literal G, handling *Goal* and detecting duplicates.*) 
873 
fun addLit (Const "*Goal*" $ G, lits) = 

874 
(*New literal is a *Goal*, so change all other Goals to Nots*) 

2854  875 
let fun bad (Const"*Goal*" $ _) = true 
876 
 bad (Const"Not" $ G') = G aconv G' 

877 
 bad _ = false; 

878 
fun change [] = [] 

879 
 change (Const"*Goal*" $ G' :: lits) = 

880 
if G aconv G' then change lits 

881 
else Const"Not" $ G' :: change lits 

882 
 change (Const"Not" $ G' :: lits) = 

883 
if G aconv G' then change lits 

884 
else Const"Not" $ G' :: change lits 

885 
 change (lit::lits) = lit :: change lits 

886 
in 

887 
Const "*Goal*" $ G :: (if exists bad lits then change lits else lits) 

888 
end 

889 
 addLit (G,lits) = ins_term(G, lits) 

890 

891 

2952  892 
(*For calculating the "penalty" to assess on a branching factor of n 
893 
log2 seems a little too severe*) 

3083  894 
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

895 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

896 

3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

897 
(*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

898 
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

899 
fun match (Var _) u = true 
4065  900 
 match (Const"*Goal*") (Const"Not") = true 
901 
 match (Const"Not") (Const"*Goal*") = true 

902 
 match (Const a) (Const b) = (a=b) 

903 
 match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb 

904 
 match (Free a) (Free b) = (a=b) 

905 
 match (Bound i) (Bound j) = (i=j) 

906 
 match (Abs(_,t)) (Abs(_,u)) = match t u 

907 
 match (f$t) (g$u) = match f g andalso match t u 

908 
 match t u = false; 

3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

909 

39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

910 

4300  911 
(*Branches closed: number of branches closed during the search 
912 
Branches tried: number of branches created by splitting (counting from 1)*) 

913 
val nclosed = ref 0 

914 
and ntried = ref 1; 

915 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

916 
fun printStats (b, start, tacs) = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

917 
if b then 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

918 
writeln (endTiming start ^ " for search. Closed: " 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

919 
^ Int.toString (!nclosed) ^ 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

920 
" tried: " ^ Int.toString (!ntried) ^ 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

921 
" tactics: " ^ Int.toString (length tacs)) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

922 
else (); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

923 

561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

924 

2854  925 
(*Tableau prover based on leanTaP. Argument is a list of branches. Each 
926 
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

927 
bound on unsafe expansions. 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

928 
"start" is CPU time at start, for printing search time 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

929 
*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

930 
fun prove (sign, start, cs, brs, cont) = 
4653  931 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  932 
val safeList = [safe0_netpair, safep_netpair] 
933 
and hazList = [haz_netpair] 

4065  934 
fun prv (tacs, trs, choices, []) = 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

935 
(printStats (!trace orelse !stats, start, tacs); 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

936 
cont (tacs, trs, choices)) (*all branches closed!*) 
2854  937 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

938 
brs0 as {pairs = ((G,md)::br, haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

939 
lits, vars, lim} :: brs) = 
3917  940 
(*apply a safe rule only (possibly allowing instantiation); 
941 
defer any haz formulae*) 

2854  942 
let exception PRV (*backtrack to precisely this recursion!*) 
943 
val ntrl = !ntrail 

944 
val nbrs = length brs0 

945 
val nxtVars = nextVars brs 

946 
val G = norm G 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

947 
val rules = netMkRules G vars safeList 
2854  948 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  949 
fun newBr (vars',lim') prems = 
950 
map (fn prem => 

951 
if (exists isGoal prem) 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

952 
then {pairs = ((joinMd md prem, []) :: 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

953 
negOfGoals ((br, haz)::pairs)), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

954 
lits = map negOfGoal lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

955 
vars = vars', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

956 
lim = lim'} 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

957 
else {pairs = ((joinMd md prem, []) :: 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

958 
(br, haz) :: pairs), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

959 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

960 
vars = vars', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

961 
lim = lim'}) 
2854  962 
prems @ 
963 
brs 

964 
(*Seek a matching rule. If unifiable then add new premises 

965 
to branch.*) 

966 
fun deeper [] = raise NEWBRANCHES 

967 
 deeper (((P,prems),tac)::grls) = 

4065  968 
if unify(add_term_vars(P,[]), P, G) 
3083  969 
then (*P comes from the rule; G comes from the branch.*) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

970 
let val updated = ntrl < !ntrail (*branch updated*) 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

971 
val lim' = if updated 
3083  972 
then lim  (1+log(length rules)) 
973 
else lim (*discourage branching updates*) 

974 
val vars = vars_in_vars vars 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

975 
val vars' = foldr add_terms_vars vars prems 
3083  976 
val choices' = (ntrl, nbrs, PRV) :: choices 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

977 
val tacs' = (tac(updated,false,true)) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

978 
:: tacs (*no duplication; rotate*) 
3083  979 
in 
4065  980 
traceNew prems; traceVars sign ntrl; 
3083  981 
(if null prems then (*closed the branch: prune!*) 
4300  982 
(nclosed := !nclosed + 1; 
983 
prv(tacs', brs0::trs, 

984 
prune (nbrs, nxtVars, choices'), 

985 
brs)) 

986 
else (*prems nonnull*) 

3083  987 
if lim'<0 (*faster to kill ALL the alternatives*) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

988 
then (traceMsg"Excessive branching: KILLED"; 
4065  989 
clearTo ntrl; raise NEWBRANCHES) 
3083  990 
else 
4300  991 
(ntried := !ntried + length prems  1; 
992 
prv(tacs', brs0::trs, choices', 

993 
newBr (vars',lim') prems))) 

3083  994 
handle PRV => 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

995 
if updated then 
3083  996 
(*Backtrack at this level. 
997 
Reset Vars and try another rule*) 

998 
(clearTo ntrl; deeper grls) 

999 
else (*backtrack to previous level*) 

1000 
backtrack choices 

1001 
end 

1002 
else deeper grls 

2854  1003 
(*Try to close branch by unifying with head goal*) 
1004 
fun closeF [] = raise CLOSEF 

1005 
 closeF (L::Ls) = 

3083  1006 
case tryClose(G,L) of 
15531  1007 
NONE => closeF Ls 
1008 
 SOME tac => 

3083  1009 
let val choices' = 
14984  1010 
(if !trace then (immediate_output"branch closed"; 
4065  1011 
traceVars sign ntrl) 
3083  1012 
else (); 
1013 
prune (nbrs, nxtVars, 

1014 
(ntrl, nbrs, PRV) :: choices)) 

4300  1015 
in nclosed := !nclosed + 1; 
1016 
prv (tac::tacs, brs0::trs, choices', brs) 

3083  1017 
handle PRV => 
1018 
(*reset Vars and try another literal 

1019 
[this handler is pruned if possible!]*) 

1020 
(clearTo ntrl; closeF Ls) 

1021 
end 

11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1022 
(*Try to unify a queued formula (safe or haz) with head goal*) 
2894  1023 
fun closeFl [] = raise CLOSEF 
1024 
 closeFl ((br, haz)::pairs) = 

1025 
closeF (map fst br) 

1026 
handle CLOSEF => closeF (map fst haz) 

1027 
handle CLOSEF => closeFl pairs 

3083  1028 
in tracing sign brs0; 
4065  1029 
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) 
2854  1030 
else 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1031 
prv (Data.hyp_subst_tac trace :: tacs, 
2854  1032 
brs0::trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1033 
equalSubst sign 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1034 
(G, {pairs = (br,haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1035 
lits = lits, vars = vars, lim = lim}) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1036 
:: brs) 
4065  1037 
handle DEST_EQ => closeF lits 
1038 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1039 
handle CLOSEF => deeper rules 

2894  1040 
handle NEWBRANCHES => 
1041 
(case netMkRules G vars hazList of 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1042 
[] => (*there are no plausible haz rules*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1043 
(traceMsg "moving formula to literals"; 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1044 
prv (tacs, brs0::trs, choices, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1045 
{pairs = (br,haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1046 
lits = addLit(G,lits), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1047 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1048 
lim = lim} :: brs)) 
2894  1049 
 _ => (*G admits some haz rules: try later*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1050 
(traceMsg "moving formula to haz list"; 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1051 
prv (if isGoal G then negOfGoal_tac :: tacs 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1052 
else tacs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1053 
brs0::trs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1054 
choices, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1055 
{pairs = (br, haz@[(negOfGoal G, md)])::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1056 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1057 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1058 
lim = lim} :: brs))) 
2854  1059 
end 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1060 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1061 
{pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = 
2894  1062 
(*no more "safe" formulae: transfer haz down a level*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1063 
prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1064 
{pairs = (Gs,haz@haz')::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1065 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1066 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1067 
lim = lim} :: brs) 
2854  1068 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1069 
brs0 as {pairs = [([], (H,md)::Hs)], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1070 
lits, vars, lim} :: brs) = 
2894  1071 
(*no safe steps possible at any level: apply a haz rule*) 
2854  1072 
let exception PRV (*backtrack to precisely this recursion!*) 
2894  1073 
val H = norm H 
2854  1074 
val ntrl = !ntrail 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1075 
val rules = netMkRules H vars hazList 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

1076 
(*new premises of haz rules may NOT be duplicated*) 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1077 
fun newPrem (vars,P,dup,lim') prem = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1078 
let val Gs' = map (fn Q => (Q,false)) prem 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

1079 
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs 
4196
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1080 
and lits' = if (exists isGoal prem) 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1081 
then map negOfGoal lits 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1082 
else lits 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1083 
in {pairs = if exists (match P) prem then [(Gs',Hs')] 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1084 
(*Recursive in this premise. Don't make new 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1085 
"stack frame". New haz premises will end up 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1086 
at the BACK of the queue, preventing 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1087 
exclusion of others*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1088 
else [(Gs',[]), ([],Hs')], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1089 
lits = lits', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1090 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1091 
lim = lim'} 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

1092 
end 
2854  1093 
fun newBr x prems = map (newPrem x) prems @ brs 
1094 
(*Seek a matching rule. If unifiable then add new premises 

1095 
to branch.*) 

1096 
fun deeper [] = raise NEWBRANCHES 

1097 
 deeper (((P,prems),tac)::grls) = 

4065  1098 
if unify(add_term_vars(P,[]), P, H) 
3083  1099 
then 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1100 
let val updated = ntrl < !ntrail (*branch updated*) 
3083  1101 
val vars = vars_in_vars vars 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1102 
val vars' = foldr add_terms_vars vars prems 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1103 
(*duplicate H if md permits*) 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1104 
val dup = md (*earlier had "andalso vars' <> vars": 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1105 
duplicate only if the subgoal has new vars*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1106 
(*any instances of P in the subgoals? 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1107 
NB: boolean "recur" affects tracing only!*) 
3083  1108 
and recur = exists (exists (match P)) prems 
1109 
val lim' = (*Decrement "lim" extra if updates occur*) 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1110 
if updated then lim  (1+log(length rules)) 
3083  1111 
else lim1 
1112 
(*It is tempting to leave "lim" UNCHANGED if 

1113 
both dup and recur are false. Proofs are 

1114 
found at shallower depths, but looping 

1115 
occurs too often...*) 

3917  1116 
val mayUndo = 
1117 
(*Allowing backtracking from a rule application 

1118 
if other matching rules exist, if the rule 

1119 
updated variables, or if the rule did not 

1120 
introduce new variables. This latter condition 

1121 
means it is not a standard "gammarule" but 

1122 
some other form of unsafe rule. Aim is to 

1123 
emulate Fast_tac, which allows all unsafe steps 

1124 
to be undone.*) 

1125 
not(null grls) (*other rules to try?*) 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1126 
orelse updated 
3917  1127 
orelse vars=vars' (*no new Vars?*) 
5481
c41956742c2e
Less deterministic reconstruction: now more robust but perhaps slower
paulson
parents:
5463
diff
changeset

1128 
val tac' = tac(updated, dup, true) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1129 
(*if recur then perhaps shouldn't call rotate_tac: new 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1130 
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

1131 
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

1132 
position*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1133 

3083  1134 
in 
1135 
if lim'<0 andalso not (null prems) 

1136 
then (*it's faster to kill ALL the alternatives*) 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1137 
(traceMsg"Excessive branching: KILLED"; 
4065  1138 
clearTo ntrl; raise NEWBRANCHES) 
3083  1139 
else 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1140 
traceNew prems; 
14984  1141 
if !trace andalso dup then immediate_output" (duplicating)" 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1142 
else (); 
14984  1143 
if !trace andalso recur then immediate_output" (recursive)" 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1144 
else (); 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1145 
traceVars sign ntrl; 
4300  1146 
if null prems then nclosed := !nclosed + 1 
1147 
else ntried := !ntried + length prems  1; 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1148 
prv(tac' :: tacs, 
3083  1149 
brs0::trs, 
1150 
(ntrl, length brs0, PRV) :: choices, 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1151 
newBr (vars', P, dup, lim') prems) 
3083  1152 
handle PRV => 
1153 
if mayUndo 

1154 
then (*reset Vars and try another rule*) 

1155 
(clearTo ntrl; deeper grls) 

1156 
else (*backtrack to previous level*) 

1157 
backtrack choices 

1158 
end 

1159 
else deeper grls 

1160 
in tracing sign brs0; 

4065  1161 
if lim<1 then (traceMsg "Limit reached. "; backtrack choices) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1162 
else deeper rules 
2854  1163 
handle NEWBRANCHES => 
2894  1164 
(*cannot close branch: move H to literals*) 
2854  1165 
prv (tacs, brs0::trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1166 
{pairs = [([], Hs)], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1167 
lits = H::lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1168 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1169 
lim = lim} :: brs) 
2854  1170 
end 
1171 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

12346  1172 
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 
2854  1173 

1174 

2883  1175 
(*Construct an initial branch.*) 
2854  1176 
fun initBranch (ts,lim) = 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1177 
{pairs = [(map (fn t => (t,true)) ts, [])], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1178 
lits = [], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1179 
vars = add_terms_vars (ts,[]), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1180 
lim = lim}; 
2854  1181 

1182 

1183 
(*** Conversion & Skolemization of the Isabelle proof state ***) 

1184 

1185 
(*Make a list of all the parameters in a subgoal, even if nested*) 

1186 
local open Term 

1187 
in 

1188 
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t 

1189 
 discard_foralls t = t; 

1190 
end; 

1191 

1192 

1193 
(*List of variables not appearing as arguments to the given parameter*) 

1194 
fun getVars [] i = [] 

1195 
 getVars ((_,(v,is))::alist) i = 

1196 
if i mem is then getVars alist i 

1197 
else v :: getVars alist i; 

1198 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1199 
exception TRANS of string; 
2854  1200 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1201 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1202 
fun fromSubgoal t = 
1203 
let val alistVar = ref [] 

1204 
and alistTVar = ref [] 

2854  1205 
fun hdvar ((ix,(v,is))::_) = v 
1206 
fun from lev t = 

1207 
let val (ht,ts) = Term.strip_comb t 

1208 
fun apply u = list_comb (u, map (from lev) ts) 

1209 
fun bounds [] = [] 

1210 
 bounds (Term.Bound i::ts) = 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1211 
if i<lev then raise TRANS 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1212 
"Function unknown's argument not a parameter" 
2854  1213 
else ilev :: bounds ts 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1214 
 bounds ts = raise TRANS 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1215 
"Function unknown's argument not a bound variable" 
2854  1216 
in 
1217 
case ht of 

4065  1218 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1219 
 Term.Free (a,_) => apply (Free a) 
1220 
 Term.Bound i => apply (Bound i) 

1221 
 Term.Var (ix,_) => 

17271  1222 
(case (AList.lookup (op =) (!alistVar) ix) of 
15531  1223 
NONE => (alistVar := (ix, (ref NONE, bounds ts)) 
4065  1224 
:: !alistVar; 
1225 
Var (hdvar(!alistVar))) 

15531  1226 
 SOME(v,is) => if is=bounds ts then Var v 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1227 
else raise TRANS 
5411  1228 
("Discrepancy among occurrences of " 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1229 
^ Syntax.string_of_vname ix)) 
2854  1230 
 Term.Abs (a,_,body) => 
1231 
if null ts then Abs(a, from (lev+1) body) 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1232 
else raise TRANS "argument not in normal form" 
2854  1233 
end 
1234 

1235 
val npars = length (Logic.strip_params t) 

1236 

1237 
(*Skolemize a subgoal from a proof state*) 

1238 
fun skoSubgoal i t = 

1239 
if i<npars then 

1240 
skoSubgoal (i+1) 

4065  1241 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1242 
t)) 
1243 
else t 

1244 

1245 
in skoSubgoal 0 (from 0 (discard_foralls t)) end; 

1246 

1247 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1248 
fun initialize thy = 
4300  1249 
(fullTrace:=[]; trail := []; ntrail := 0; 
18058
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

1250 
nclosed := 0; ntried := 1; typargs := Sign.const_typargs thy); 
4300  1251 

1252 

2854  1253 
(*Tactic using tableau engine and proof reconstruction. 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1254 
"start" is CPU time at start, for printing SEARCH time 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1255 
(also prints reconstruction time) 
2854  1256 
"lim" is depth limit.*) 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

1257 
fun timing_depth_tac start cs lim i st0 = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1258 
let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0); 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

1259 
val {sign,...} = rep_thm st 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1260 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1261 
val hyps = strip_imp_prems skoprem 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1262 
and concl = strip_imp_concl skoprem 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1263 
fun cont (tacs,_,choices) = 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1264 
let val start = startTiming() 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1265 
in 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1266 
case Seq.pull(EVERY' (rev tacs) i st) of 
15531  1267 
NONE => (writeln ("PROOF FAILED for depth " ^ 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1268 
Int.toString lim); 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1269 
if !trace then error "************************\n" 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1270 
else (); 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1271 
backtrack choices) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1272 
 cell => (if (!trace orelse !stats) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1273 
then writeln (endTiming start ^ " for reconstruction") 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1274 
else (); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1275 
Seq.make(fn()=> cell)) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1276 
end 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1277 
in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1278 
end 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1279 
handle PROVE => Seq.empty; 
2854  1280 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1281 
(*Public version with fixed depth*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1282 
fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1283 

15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1284 
val depth_limit = ref 20; 
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1285 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1286 
fun blast_tac cs i st = 
15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1287 
((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1288 
THEN flexflex_tac) st 
14466  1289 
handle TRANS s => 
1290 
((if !trace then warning ("blast: " ^ s) else ()); 

1291 
Seq.empty); 

2854  1292 

4078  1293 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1294 

2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1295 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1296 
(*** For debugging: these apply the prover to a subgoal and return 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1297 
the resulting tactics, trace, etc. ***) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1298 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1299 
(*Translate subgoal i from a proof state*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1300 
fun trygl cs lim i = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1301 
let val st = topthm() 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1302 
val {sign,...} = rep_thm st 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1303 
val skoprem = (initialize (theory_of_thm st); 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1304 
fromSubgoal (List.nth(prems_of st, i1))) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1305 
val hyps = strip_imp_prems skoprem 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1306 
and concl = strip_imp_concl skoprem 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1307 
in timeap prove (sign, startTiming(), cs, 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1308 
[initBranch (mkGoal concl :: hyps, lim)], I) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1309 
end 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1310 
handle Subscript => error("There is no subgoal " ^ Int.toString i); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1311 

4078  1312 
fun Trygl lim i = trygl (Data.claset()) lim i; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1313 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1314 
(*Read a string to make an initial, singleton branch*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1315 
fun readGoal sign s = read_cterm sign (s,propT) > 
4065  1316 
term_of > fromTerm > rand > mkGoal; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1317 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1318 
fun tryInThy thy lim s = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1319 
(initialize thy; 
6391  1320 
timeap prove (Theory.sign_of thy, 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1321 
startTiming(), 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1322 
Data.claset(), 
6391  1323 
[initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1324 
I)); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1325 

af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1326 

5926  1327 
(** method setup **) 
1328 

7559  1329 
fun blast_args m = 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1330 
Method.bang_sectioned_args' 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1331 
Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; 
7155  1332 

15531  1333 
fun blast_meth NONE = Data.cla_meth' blast_tac 
1334 
 blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim); 

7155  1335 

11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1336 
val setup = [Method.add_methods [("blast", blast_args blast_meth, 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1337 
"tableau prover")]]; 
5926  1338 

1339 

2854  1340 
end; 