author  wenzelm 
Sat, 01 Jul 2000 19:55:22 +0200  
changeset 9230  17ae63f82ad8 
parent 9170  0bfe5354d5e7 
child 9486  2df511ebb956 
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 

11 

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

12 
Blast_tac is often more powerful than fast_tac, but has some limitations. 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

13 
Blast_tac... 
4651  14 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
15 
this restriction is intrinsic 

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

18 
* ignores types, which can make HOL proofs fail 

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

19 
* 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

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

21 
* its proof strategy is more general but can actually be slower 
2894  22 

23 
Known problems: 

3092  24 
"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

25 
from expansion. This happens because newlycreated formulae always 
3092  26 
have priority over existing ones. But obviously recursive rules 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

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

28 
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

29 

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

31 
Calls to Blast.overloaded (see HOL/Set.ML for examples) are needed 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

32 
to tell Blast_tac when to retain some type information. Make sure 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

33 
you know the constant's internal name, which might be "op <=" or 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

34 
"Relation.op ^^". 
2952  35 

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

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

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

39 
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

40 
"no DETERM" flag would prevent proofs failing here. 
2854  41 
*) 
42 

43 
(*Should be a type abbreviation?*) 

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

45 

46 

47 
(*Assumptions about constants: 

48 
The negation symbol is "Not" 

49 
The equality symbol is "op =" 

50 
The istrue judgement symbol is "Trueprop" 

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

52 
*) 

53 
signature BLAST_DATA = 

54 
sig 

55 
type claset 

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

57 
val ccontr : thm 

58 
val contr_tac : int > tactic 

59 
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

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

6955  65 
xtraIs: thm list, xtraEs: thm list, 
4651  66 
swrappers: (string * wrapper) list, 
67 
uwrappers: (string * wrapper) list, 

2854  68 
safe0_netpair: netpair, safep_netpair: netpair, 
6955  69 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 
7272  70 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  71 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 
2854  72 
end; 
73 

74 

75 
signature BLAST = 

76 
sig 

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

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

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

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

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

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

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

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

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

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

88 
type branch 
2883  89 
val depth_tac : claset > int > int > tactic 
90 
val blast_tac : claset > int > tactic 

91 
val Blast_tac : int > tactic 

4240
8ba60a4cd380
Renamed "overload" to "overloaded" for sml/nj compatibility
paulson
parents:
4233
diff
changeset

92 
val overloaded : string * (Term.typ > Term.typ) > unit 
5926  93 
val setup : (theory > theory) list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

97 
val fullTrace : branch list list ref 
4065  98 
val fromType : (indexname * term) list ref > Term.typ > term 
99 
val fromTerm : Term.term > term 

100 
val fromSubgoal : Term.term > term 

101 
val instVars : term > (unit > unit) 

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

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

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

104 
val tryInThy : theory > int > string > 
3083  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 trygl : claset > int > int > 
3083  107 
(int>tactic) list * branch list list * (int*int*exn) list 
108 
val Trygl : int > int > 

109 
(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

110 
val normBr : branch > branch 
2854  111 
end; 
112 

113 

3092  114 
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854  115 
struct 
116 

117 
type claset = Data.claset; 

118 

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

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

120 
and stats = ref false; (*for runtime and search statistics*) 
2854  121 

122 
datatype term = 

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

123 
Const of string 
4065  124 
 TConst of string * term (*type of overloaded constantas a term!*) 
2854  125 
 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

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

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

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

129 
 Abs of string*term 
5613  130 
 op $ of term*term; 
2854  131 

132 

133 
(** Basic syntactic operations **) 

134 

135 
fun is_Var (Var _) = true 

136 
 is_Var _ = false; 

137 

138 
fun dest_Var (Var x) = x; 

139 

140 

141 
fun rand (f$x) = x; 

142 

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

144 
val list_comb : term * term list > term = foldl (op $); 

145 

146 

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

148 
fun strip_comb u : term * term list = 

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

150 
 stripc x = x 

151 
in stripc(u,[]) end; 

152 

153 

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

155 
fun head_of (f$t) = head_of f 

156 
 head_of u = u; 

157 

158 

159 
(** Particular constants **) 

160 

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

162 

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

164 

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

166 
 isGoal _ = false; 

167 

168 
val Trueprop = Term.Const("Trueprop", Type("o",[])>propT); 

169 
fun mk_tprop P = Term.$ (Trueprop, P); 

170 

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

172 
 isTrueprop _ = false; 

173 

174 

4065  175 
(*** Dealing with overloaded constants ***) 
2854  176 

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

179 
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, 

180 
map (fromType alist) Ts) 

181 
 fromType alist (Term.TFree(a,_)) = Free a 

182 
 fromType alist (Term.TVar (ixn,_)) = 

183 
(case (assoc_string_int(!alist,ixn)) of 

184 
None => let val t' = Var(ref None) 

185 
in alist := (ixn, t') :: !alist; t' 

186 
end 

187 
 Some v => v) 

2854  188 

189 
local 

4065  190 
val overloads = ref ([]: (string * (Term.typ > Term.typ)) list) 
2854  191 
in 
192 

4240
8ba60a4cd380
Renamed "overload" to "overloaded" for sml/nj compatibility
paulson
parents:
4233
diff
changeset

193 
fun overloaded arg = (overloads := arg :: (!overloads)); 
2854  194 

4065  195 
(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst, 
196 
converting its type to a Blast.term in the latter case.*) 

197 
fun fromConst alist (a,T) = 

198 
case assoc_string (!overloads, a) of 

199 
None => Const a (*not overloaded*) 

200 
 Some f => 

201 
let val T' = f T 

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

202 
handle Match => error 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

203 
("Blast_tac: unexpected type for overloaded constant " ^ a) 
4065  204 
in TConst(a, fromType alist T') end; 
205 

2854  206 
end; 
207 

208 

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

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

4065  211 
 (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb 
2854  212 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
213 
 (Free a) aconv (Free b) = a=b 

214 
 (Var(ref(Some t))) aconv u = t aconv u 

4065  215 
 t aconv (Var(ref(Some u))) = t aconv u 
2854  216 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
217 
 (Bound i) aconv (Bound j) = i=j 

218 
 (Abs(_,t)) aconv (Abs(_,u)) = t aconv u 

219 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 

220 
 _ aconv _ = false; 

221 

222 

223 
fun mem_term (_, []) = false 

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

225 

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

227 

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

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

230 

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

232 

233 

234 
(** Vars **) 

235 

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

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

238 
 add_term_vars (Var (v as ref None), vars) = ins_var (v, vars) 

239 
 add_term_vars (Var (ref (Some u)), vars) = add_term_vars(u,vars) 

4065  240 
 add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) 
2854  241 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
242 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

243 
 add_term_vars (_, vars) = vars 

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

245 
and add_terms_vars ([], vars) = vars 

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

247 
(*Var list version.*) 

248 
and add_vars_vars ([], vars) = vars 

249 
 add_vars_vars (ref (Some u) :: vs, vars) = 

250 
add_vars_vars (vs, add_term_vars(u,vars)) 

251 
 add_vars_vars (v::vs, vars) = (*v must be a ref None*) 

252 
add_vars_vars (vs, ins_var (v, vars)); 

253 

254 

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

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

257 

258 

259 

260 
(*increment a term's nonlocal bound variables 

261 
inc is increment for bound variables 

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

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

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

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

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

267 

268 
fun incr_boundvars 0 t = t 

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

270 

271 

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

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

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

275 
else (ilev) ins_int js 

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

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

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

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

280 

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

282 

283 
fun subst_bound (arg, t) : term = 

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

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

286 
else if i=lev then incr_boundvars lev arg 

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

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

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

290 
 subst (t,lev) = t 

291 
in subst (t,0) end; 

292 

293 

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

294 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  295 
fun norm t = case t of 
2952  296 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
4065  297 
 TConst(a,aT) => TConst(a, norm aT) 
2854  298 
 (Var (ref None)) => t 
299 
 (Var (ref (Some u))) => norm u 

300 
 (f $ u) => (case norm f of 

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

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

302 
 nf => nf $ norm u) 
2854  303 
 _ => t; 
304 

305 

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

307 
fun wkNormAux t = case t of 

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

309 
Some u => wkNorm u 

310 
 None => t) 

311 
 (f $ u) => (case wkNormAux f of 

312 
Abs(_,body) => wkNorm (subst_bound (u, body)) 

313 
 nf => nf $ u) 

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

316 
nb as (f $ t) => 

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

318 
then Abs(a,nb) 

319 
else wkNorm (incr_boundvars ~1 f) 

3092  320 
 nb => Abs (a,nb)) 
2854  321 
 _ => t 
322 
and wkNorm t = case head_of t of 

323 
Const _ => t 

4065  324 
 TConst _ => t 
2854  325 
 Skolem(a,args) => t 
326 
 Free _ => t 

327 
 _ => wkNormAux t; 

328 

329 

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

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

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

333 
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

334 
 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

335 
and occ lev (Var w) = 
2854  336 
v=w orelse 
337 
(case !w of None => false 

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

338 
 Some u => occ lev u) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

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

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

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

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

343 
 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

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

345 
in occ 0 end; 
2854  346 

347 
exception UNIFY; 

348 

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

350 
val ntrail = ref 0; 

351 

352 

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

354 
fun clearTo n = 

3083  355 
while !ntrail<>n do 
2854  356 
(hd(!trail) := None; 
357 
trail := tl (!trail); 

358 
ntrail := !ntrail  1); 

359 

360 

361 
(*Firstorder unification with bound variables. 

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

363 
on the trail (no point in doing so) 

364 
*) 

4065  365 
fun unify(vars,t,u) = 
2854  366 
let val n = !ntrail 
367 
fun update (t as Var v, u) = 

368 
if t aconv u then () 

369 
else if varOccur v u then raise UNIFY 

370 
else if mem_var(v, vars) then v := Some u 

371 
else (*avoid updating Vars in the branch if possible!*) 

372 
if is_Var u andalso mem_var(dest_Var u, vars) 

373 
then dest_Var u := Some t 

374 
else (v := Some u; 

375 
trail := v :: !trail; ntrail := !ntrail + 1) 

376 
fun unifyAux (t,u) = 

377 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

3083  386 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  387 
end; 
388 

389 

4065  390 
(*Convert from "real" terms to prototerms; etacontract 
391 
Code is duplicated with fromSubgoal. Correct this?*) 

392 
fun fromTerm t = 

393 
let val alistVar = ref [] 

394 
and alistTVar = ref [] 

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

2854  396 
 from (Term.Free (a,_)) = Free a 
397 
 from (Term.Bound i) = Bound i 

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

4065  399 
(case (assoc_string_int(!alistVar,ixn)) of 
2854  400 
None => let val t' = Var(ref None) 
4065  401 
in alistVar := (ixn, t') :: !alistVar; t' 
2854  402 
end 
4065  403 
 Some v => v) 
2854  404 
 from (Term.Abs (a,_,u)) = 
405 
(case from u of 

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

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

408 
else incr_boundvars ~1 f 

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

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

411 
in from t end; 

412 

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

415 
fun instVars t = 

416 
let val name = ref "A" 

417 
val updated = ref [] 

418 
fun inst (TConst(a,t)) = inst t 

419 
 inst (Var(v as ref None)) = (updated := v :: (!updated); 

420 
v := Some (Free ("?" ^ !name)); 

421 
name := bump_string (!name)) 

422 
 inst (Abs(a,t)) = inst t 

423 
 inst (f $ u) = (inst f; inst u) 

424 
 inst _ = () 

425 
fun revert() = seq (fn v => v:=None) (!updated) 

426 
in inst t; revert end; 

427 

428 

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

431 
A :: strip_imp_prems B 

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

433 
 strip_imp_prems _ = []; 

434 

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

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

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

438 
 strip_imp_concl A = A : term; 

439 

440 

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

442 

9170  443 
exception ElimBadConcl and ElimBadPrem; 
444 

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

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

447 
PROOF FAILED*) 

448 
fun delete_concl [] = raise ElimBadPrem 

449 
 delete_concl (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) = 

450 
Ps 

451 
 delete_concl (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) = 

452 
Ps 

453 
 delete_concl (P::Ps) = P :: delete_concl Ps; 

2854  454 

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

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

457 
 skoPrem vars P = P; 

458 

459 
fun convertPrem t = 

9170  460 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  461 

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

463 
fun convertRule vars t = 

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

465 
val Var v = strip_imp_concl t 

466 
in v := Some (Const"*False*"); 

467 
(P, map (convertPrem o skoPrem vars) Ps) 

9170  468 
end 
469 
handle Bind => raise ElimBadConcl; 

2854  470 

471 

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

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

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

475 

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

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

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

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

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

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

481 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  482 

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

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

484 
 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

485 
 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

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

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

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

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

490 

2854  491 

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

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

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

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

495 
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

496 
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

497 
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

498 

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

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

500 
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

501 
Flag "dup" requests duplication of the affected formula.*) 
2854  502 
fun fromRule vars rl = 
4065  503 
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

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

505 
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

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

507 
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

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

511 
Option.NONE) 

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

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

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

515 
else (); 

516 
Option.NONE); 

2854  517 

518 

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

519 
(*** Conversion of Introduction Rules ***) 
2854  520 

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

522 

523 
fun convertIntrRule vars t = 

524 
let val Ps = strip_imp_prems t 

525 
val P = strip_imp_concl t 

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

527 
end; 

528 

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

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

530 
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

531 
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

532 
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

533 
introduction rules.*) 
2854  534 
fun fromIntrRule vars rl = 
4065  535 
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

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

537 
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

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

539 
rot_subgoals_tac (rot, #2 trl) i 
2854  540 
in (trl, tac) end; 
541 

542 

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

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

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

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

548 
 toTerm d (Const a) = Term.Const (a,dummyT) 
4065  549 
 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

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

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

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

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

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

555 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  556 

557 

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

559 
case P of 

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

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

561 
let val pG = mk_tprop (toTerm 2 G) 
2854  562 
val intrs = List.concat 
563 
(map (fn (inet,_) => Net.unify_term inet pG) 

564 
nps) 

565 
in map (fromIntrRule vars o #2) (orderlist intrs) end 

566 
 _ => 

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

567 
let val pP = mk_tprop (toTerm 3 P) 
2854  568 
val elims = List.concat 
569 
(map (fn (_,enet) => Net.unify_term enet pP) 

570 
nps) 

571 
in List.mapPartial (fromRule vars o #2) (orderlist elims) end; 

572 

573 
(** 

574 
end; 

575 
**) 

576 

3092  577 

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

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

580 
{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

581 
(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

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

583 
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

584 
lim: int}; (*resource limit*) 
3092  585 

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

587 

588 
(*Normalize a branchfor tracing*) 

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

590 

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

592 

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

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

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

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

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

597 
lim = lim}; 
3092  598 

599 

4065  600 
val dummyTVar = Term.TVar(("a",0), []); 
3092  601 
val dummyVar2 = Term.Var(("var",0), dummyT); 
602 

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

605 
 showType (Var _) = dummyTVar 

606 
 showType t = 

607 
(case strip_comb t of 

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

609 
 _ => dummyT); 

610 

611 
(*Display toplevel overloading if any*) 

612 
fun topType (TConst(a,t)) = Some (showType t) 

613 
 topType (Abs(a,t)) = topType t 

614 
 topType (f $ u) = (case topType f of 

615 
None => topType u 

616 
 some => some) 

617 
 topType _ = None; 

618 

619 

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

4065  622 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  623 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
624 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

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

626 
 showTerm d (Var(ref(Some u))) = showTerm d u 
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

627 
 showTerm d (Var(ref None)) = dummyVar2 
3092  628 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
629 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

632 

4065  633 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  634 

4065  635 
fun traceTerm sign t = 
636 
let val t' = norm t 

637 
val stm = string_of sign 8 t' 

638 
in 

639 
case topType t' of 

640 
None => stm (*no type to attach*) 

641 
 Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T 

642 
end; 

3092  643 

644 

5961  645 
val prs = std_output; 
646 

3092  647 
(*Print tracing information at each iteration of prover*) 
648 
fun tracing sign brs = 

649 
let fun printPairs (((G,_)::_,_)::_) = prs(traceTerm sign G) 

650 
 printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)") 

651 
 printPairs _ = () 

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

652 
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 
3092  653 
(fullTrace := brs0 :: !fullTrace; 
654 
seq (fn _ => prs "+") brs; 

655 
prs (" [" ^ Int.toString lim ^ "] "); 

656 
printPairs pairs; 

657 
writeln"") 

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

659 
end; 

660 

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

661 
fun traceMsg s = if !trace then writeln s else (); 
4065  662 

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

666 
(case !ntrailntrl of 

667 
0 => () 

668 
 1 => prs"\t1 variable UPDATED:" 

669 
 n => prs("\t" ^ Int.toString n ^ " variables UPDATED:"); 

670 
(*display the instantiations themselves, though no variable names*) 

671 
seq (fn v => prs(" " ^ string_of sign 4 (the (!v)))) 

672 
(List.take(!trail, !ntrailntrl)); 

673 
writeln"") 

3092  674 
else (); 
675 

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

677 
fun traceNew prems = 

678 
if !trace then 

679 
case length prems of 

680 
0 => prs"branch closed by rule" 

681 
 1 => prs"branch extended (1 new subgoal)" 

682 
 n => prs("branch split: "^ Int.toString n ^ " new subgoals") 

683 
else (); 

684 

685 

686 

2854  687 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
688 

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

690 
fun subst_atomic (old,new) t = 

691 
let fun subst (Var(ref(Some u))) = subst u 

692 
 subst (Abs(a,body)) = Abs(a, subst body) 

693 
 subst (f$t) = subst f $ subst t 

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

695 
in subst t end; 

696 

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

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

699 
(case eta_contract2 body of 

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

701 
else eta_contract_atom (incr_boundvars ~1 f) 

702 
 _ => t0) 

703 
 eta_contract_atom t = t 

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

705 
 eta_contract2 t = eta_contract_atom t; 

706 

707 

708 
(*When can we safely delete the equality? 

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

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

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

712 
Prefer to eliminate Bound variables if possible. 

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

714 

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

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

716 
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

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

719 
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

720 
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

721 
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

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

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

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

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

726 
fun occEq u = (t aconv u) orelse occ u 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

727 
and occ (Var(ref(Some u))) = occEq u 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

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

729 
 occ (Abs(_,u)) = occEq u 
2854  730 
 occ (f$u) = occEq u orelse occEq f 
731 
 occ (_) = false; 

732 
in occEq end; 

733 

3092  734 
exception DEST_EQ; 
735 

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

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

738 
(eta_contract_atom t, eta_contract_atom u) 

4065  739 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  740 
(eta_contract_atom t, eta_contract_atom u) 
741 
 dest_eq _ = raise DEST_EQ; 

742 

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

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

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

747 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  748 
fun orientGoal (t,u) = case (t,u) of 
2854  749 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
750 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

753 
 _ => raise DEST_EQ; 

754 

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

757 
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

758 
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092  759 
let val (t,u) = orientGoal(dest_eq G) 
760 
val subst = subst_atomic (t,u) 

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

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

763 
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

764 
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

765 
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

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

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

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

769 
fun subFrame ((Gs,Hs), (changed, frames)) = 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

770 
let val (changed', Gs') = foldr subForm (Gs, (changed, [])) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

771 
val (changed'', Hs') = foldr subForm (Hs, (changed', [])) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

772 
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

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

774 
fun subLit (lit, (changed, nlits)) = 
2854  775 
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

776 
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

777 
else ((nlit,true)::changed, nlits) 
2854  778 
end 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

779 
val (changed, lits') = foldr subLit (lits, ([], [])) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

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

783 
else (); 

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

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

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

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

787 
lim = lim} 
2854  788 
end; 
789 

790 

791 
exception NEWBRANCHES and CLOSEF; 

792 

793 
exception PROVE; 

794 

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

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

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

797 
(eq_assume_tac ORELSE' assume_tac); 
2854  798 

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

799 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  800 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
801 

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

3083  803 
fun tryClose (Const"*Goal*" $ G, L) = 
4065  804 
if unify([],G,L) then Some eAssume_tac else None 
3083  805 
 tryClose (G, Const"*Goal*" $ L) = 
4065  806 
if unify([],G,L) then Some eAssume_tac else None 
3083  807 
 tryClose (Const"Not" $ G, L) = 
4065  808 
if unify([],G,L) then Some eContr_tac else None 
3083  809 
 tryClose (G, Const"Not" $ L) = 
4065  810 
if unify([],G,L) then Some eContr_tac else None 
3083  811 
 tryClose _ = None; 
2854  812 

813 

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

815 
fun hasSkolem (Skolem _) = true 

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

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

818 
 hasSkolem _ = false; 

819 

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

821 
Skolem terms then allow duplication.*) 

822 
fun joinMd md [] = [] 

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

824 

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

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

828 
 negOfGoal G = G; 

829 

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

831 

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

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

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

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

836 

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

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

838 
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

839 
rotate_tac ~1 i; 
2894  840 

2854  841 

842 
(** Backtracking and Pruning **) 

843 

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

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

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

847 
 clashVar vars = 

848 
let fun clash (0, _) = false 

849 
 clash (_, []) = false 

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

851 
in clash end; 

852 

853 

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

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

856 
next branch have been updated.*) 

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

858 
backtracking over bad proofs*) 

859 
 prune (nbrs, nxtVars, choices) = 

860 
let fun traceIt last = 

861 
let val ll = length last 

862 
and lc = length choices 

863 
in if !trace andalso ll<lc then 

3083  864 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  865 
last) 
866 
else last 

867 
end 

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

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

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

873 
else (* nbrs'=nbrs *) 

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

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

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

877 
choices) 

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

879 

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

880 
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

881 
 nextVars [] = []; 
2854  882 

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

885 
Int.toString nbrs ^ " branches")) 

886 
else (); 

887 
raise exn) 

888 
 backtrack _ = raise PROVE; 

2854  889 

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

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

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

895 
 bad _ = false; 

896 
fun change [] = [] 

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

898 
if G aconv G' then change lits 

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

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

901 
if G aconv G' then change lits 

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

903 
 change (lit::lits) = lit :: change lits 

904 
in 

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

906 
end 

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

908 

909 

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

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

913 

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

914 

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

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

916 
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

917 
fun match (Var _) u = true 
4065  918 
 match (Const"*Goal*") (Const"Not") = true 
919 
 match (Const"Not") (Const"*Goal*") = true 

920 
 match (Const a) (Const b) = (a=b) 

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

922 
 match (Free a) (Free b) = (a=b) 

923 
 match (Bound i) (Bound j) = (i=j) 

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

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

926 
 match t u = false; 

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

927 

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

928 

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

931 
val nclosed = ref 0 

932 
and ntried = ref 1; 

933 

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

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

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

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

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

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

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

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

941 

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

942 

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

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

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

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

948 
fun prove (sign, start, cs, brs, cont) = 
4653  949 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  950 
val safeList = [safe0_netpair, safep_netpair] 
951 
and hazList = [haz_netpair] 

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

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

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

956 
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

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

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

962 
val nbrs = length brs0 

963 
val nxtVars = nextVars brs 

964 
val G = norm G 

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

965 
val rules = netMkRules G vars safeList 
2854  966 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  967 
fun newBr (vars',lim') prems = 
968 
map (fn prem => 

969 
if (exists isGoal prem) 

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

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

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

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

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

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

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

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

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

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

979 
lim = lim'}) 
2854  980 
prems @ 
981 
brs 

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

983 
to branch.*) 

984 
fun deeper [] = raise NEWBRANCHES 

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

4065  986 
if unify(add_term_vars(P,[]), P, G) 
3083  987 
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

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

989 
val lim' = if updated 
3083  990 
then lim  (1+log(length rules)) 
991 
else lim (*discourage branching updates*) 

992 
val vars = vars_in_vars vars 

993 
val vars' = foldr add_terms_vars (prems, vars) 

994 
val choices' = (ntrl, nbrs, PRV) :: choices 

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

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

996 
:: tacs (*no duplication; rotate*) 
3083  997 
in 
4065  998 
traceNew prems; traceVars sign ntrl; 
3083  999 
(if null prems then (*closed the branch: prune!*) 
4300  1000 
(nclosed := !nclosed + 1; 
1001 
prv(tacs', brs0::trs, 

1002 
prune (nbrs, nxtVars, choices'), 

1003 
brs)) 

1004 
else (*prems nonnull*) 

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

1006 
then (traceMsg"Excessive branching: KILLED"; 
4065  1007 
clearTo ntrl; raise NEWBRANCHES) 
3083  1008 
else 
4300  1009 
(ntried := !ntried + length prems  1; 
1010 
prv(tacs', brs0::trs, choices', 

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

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

1013 
if updated then 
3083  1014 
(*Backtrack at this level. 
1015 
Reset Vars and try another rule*) 

1016 
(clearTo ntrl; deeper grls) 

1017 
else (*backtrack to previous level*) 

1018 
backtrack choices 

1019 
end 

1020 
else deeper grls 

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

1023 
 closeF (L::Ls) = 

3083  1024 
case tryClose(G,L) of 
1025 
None => closeF Ls 

1026 
 Some tac => 

1027 
let val choices' = 

3092  1028 
(if !trace then (prs"branch closed"; 
4065  1029 
traceVars sign ntrl) 
3083  1030 
else (); 
1031 
prune (nbrs, nxtVars, 

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

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

3083  1035 
handle PRV => 
1036 
(*reset Vars and try another literal 

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

1038 
(clearTo ntrl; closeF Ls) 

1039 
end 

2894  1040 
fun closeFl [] = raise CLOSEF 
1041 
 closeFl ((br, haz)::pairs) = 

1042 
closeF (map fst br) 

1043 
handle CLOSEF => closeF (map fst haz) 

1044 
handle CLOSEF => closeFl pairs 

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

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

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

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

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

1053 
:: brs) 
4065  1054 
handle DEST_EQ => closeF lits 
1055 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1056 
handle CLOSEF => deeper rules 

2894  1057 
handle NEWBRANCHES => 
1058 
(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

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

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

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

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

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

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

1065 
lim = lim} :: brs)) 
2894  1066 
 _ => (*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

1067 
(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

1068 
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

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

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

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

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

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

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

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

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

1078 
{pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = 
2894  1079 
(*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

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

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

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

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

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

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

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

1092 
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

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

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

1095 
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

1096 
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

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

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

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

1100 
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

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

1102 
"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

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

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

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

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

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

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

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

1112 
to branch.*) 

1113 
fun deeper [] = raise NEWBRANCHES 

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

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

1117 
let val updated = ntrl < !ntrail (*branch updated*) 
3083  1118 
val vars = vars_in_vars vars 
1119 
val vars' = foldr add_terms_vars (prems, vars) 

1120 
(*duplicate H if md and the subgoal has new vars*) 

1121 
val dup = md andalso vars' <> vars 

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

1122 
(*any instances of P in the subgoals? 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1123 
NB: this boolean affects tracing only!*) 
3083  1124 
and recur = exists (exists (match P)) prems 
1125 
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

1126 
if updated then lim  (1+log(length rules)) 
3083  1127 
else lim1 
1128 
(*It is tempting to leave "lim" UNCHANGED if 

1129 
both dup and recur are false. Proofs are 

1130 
found at shallower depths, but looping 

1131 
occurs too often...*) 

3917  1132 
val mayUndo = 
1133 
(*Allowing backtracking from a rule application 

1134 
if other matching rules exist, if the rule 

1135 
updated variables, or if the rule did not 

1136 
introduce new variables. This latter condition 

1137 
means it is not a standard "gammarule" but 

1138 
some other form of unsafe rule. Aim is to 

1139 
emulate Fast_tac, which allows all unsafe steps 

1140 
to be undone.*) 

1141 
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

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

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

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

1146 
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

1147 
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

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

1149 

3083  1150 
in 
1151 
if lim'<0 andalso not (null prems) 

1152 
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

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

1156 
traceNew prems; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1157 
if !trace andalso recur then prs" (recursive)" 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

1159 
traceVars sign ntrl; 
4300  1160 
if null prems then nclosed := !nclosed + 1 
1161 
else ntried := !ntried + length prems  1; 

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

1162 
prv(tac' :: tacs, 
3083  1163 
brs0::trs, 
1164 
(ntrl, length brs0, PRV) :: choices, 

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

1165 
newBr (vars', P, dup, lim') prems) 
3083  1166 
handle PRV => 
1167 
if mayUndo 

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

1169 
(clearTo ntrl; deeper grls) 

1170 
else (*backtrack to previous level*) 

1171 
backtrack choices 

1172 
end 

1173 
else deeper grls 

1174 
in tracing sign brs0; 

4065  1175 
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

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

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

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

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

1183 
lim = lim} :: brs) 
2854  1184 
end 
1185 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1186 
in init_gensym(); 
1187 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1188 
end; 

2854  1189 

1190 

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

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

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

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

1196 
lim = lim}; 
2854  1197 

1198 

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

1200 

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

1202 
local open Term 

1203 
in 

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

1205 
 discard_foralls t = t; 

1206 
end; 

1207 

1208 

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

1210 
fun getVars [] i = [] 

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

1212 
if i mem is then getVars alist i 

1213 
else v :: getVars alist i; 

1214 

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

1215 
exception TRANS of string; 
2854  1216 

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

1217 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1218 
fun fromSubgoal t = 
1219 
let val alistVar = ref [] 

1220 
and alistTVar = ref [] 

2854  1221 
fun hdvar ((ix,(v,is))::_) = v 
1222 
fun from lev t = 

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

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

1225 
fun bounds [] = [] 

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

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

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

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

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

1231 
"Function unknown's argument not a bound variable" 
2854  1232 
in 
1233 
case ht of 

4065  1234 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1235 
 Term.Free (a,_) => apply (Free a) 
1236 
 Term.Bound i => apply (Bound i) 

1237 
 Term.Var (ix,_) => 

4065  1238 
(case (assoc_string_int(!alistVar,ix)) of 
1239 
None => (alistVar := (ix, (ref None, bounds ts)) 

1240 
:: !alistVar; 

1241 
Var (hdvar(!alistVar))) 

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

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

1245 
^ Syntax.string_of_vname ix)) 
2854  1246 
 Term.Abs (a,_,body) => 
1247 
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

1248 
else raise TRANS "argument not in normal form" 
2854  1249 
end 
1250 

1251 
val npars = length (Logic.strip_params t) 

1252 

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

1254 
fun skoSubgoal i t = 

1255 
if i<npars then 

1256 
skoSubgoal (i+1) 

4065  1257 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1258 
t)) 
1259 
else t 

1260 

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

1262 

1263 

4300  1264 
fun initialize() = 
1265 
(fullTrace:=[]; trail := []; ntrail := 0; 

1266 
nclosed := 0; ntried := 1); 

1267 

1268 

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

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

1271 
(also prints reconstruction time) 
2854  1272 
"lim" is depth limit.*) 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1273 
fun timing_depth_tac start cs lim i st = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

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

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

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

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

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

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

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

1282 
case Seq.pull(EVERY' (rev tacs) i st) of 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1283 
None => (writeln ("PROOF FAILED for depth " ^ 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1284 
Int.toString lim); 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

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

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

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

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

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

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

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

1293 
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

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

1295 
handle PROVE => Seq.empty); 
2854  1296 

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

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

1298 
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

1299 

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

1300 
fun blast_tac cs i st = 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

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

1303 
handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); 
2854  1304 

4078  1305 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1306 

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

1307 

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

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

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

1310 

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

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

1312 
fun trygl cs lim i = 
4300  1313 
(initialize(); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1314 
let val st = topthm() 
3030  1315 
val {sign,...} = rep_thm st 
4065  1316 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1317 
val hyps = strip_imp_prems skoprem 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1318 
and concl = strip_imp_concl skoprem 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1319 
in timeap prove (sign, startTiming(), cs, 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1320 
[initBranch (mkGoal concl :: hyps, lim)], I) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

1323 

4078  1324 
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

1325 

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

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

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

1329 

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

1330 
fun tryInThy thy lim s = 
4300  1331 
(initialize(); 
6391  1332 
timeap prove (Theory.sign_of thy, 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

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

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

1337 

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

1338 

5926  1339 
(** method setup **) 
1340 

7559  1341 
fun blast_args m = 
7607  1342 
Method.sectioned_args (Args.bang_facts  Scan.lift (Scan.option Args.nat)) Data.cla_modifiers m; 
7155  1343 

7559  1344 
fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems 
1345 
 blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems; 

7155  1346 

1347 
val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]]; 

5926  1348 

1349 

2854  1350 
end; 