author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9779  c71a1acffc27 
child 10400  8621cb0021a6 
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} 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

70 
val atomize: thm list 
7272  71 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  72 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 
2854  73 
end; 
74 

75 

76 
signature BLAST = 

77 
sig 

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

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

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

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

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

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

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

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

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

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

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

92 
val Blast_tac : int > tactic 

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

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

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

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

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

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

101 
val fromSubgoal : Term.term > term 

102 
val instVars : term > (unit > unit) 

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

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

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

105 
val tryInThy : theory > int > string > 
3083  106 
(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

107 
val trygl : claset > int > int > 
3083  108 
(int>tactic) list * branch list list * (int*int*exn) list 
109 
val Trygl : int > int > 

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

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

114 

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

118 
type claset = Data.claset; 

119 

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

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

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

123 
datatype term = 

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

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

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

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

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

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

133 

134 
(** Basic syntactic operations **) 

135 

136 
fun is_Var (Var _) = true 

137 
 is_Var _ = false; 

138 

139 
fun dest_Var (Var x) = x; 

140 

141 

142 
fun rand (f$x) = x; 

143 

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

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

146 

147 

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

149 
fun strip_comb u : term * term list = 

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

151 
 stripc x = x 

152 
in stripc(u,[]) end; 

153 

154 

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

156 
fun head_of (f$t) = head_of f 

157 
 head_of u = u; 

158 

159 

160 
(** Particular constants **) 

161 

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

163 

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

165 

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

167 
 isGoal _ = false; 

168 

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

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

171 

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

173 
 isTrueprop _ = false; 

174 

175 

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

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

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

181 
map (fromType alist) Ts) 

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

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

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

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

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

187 
end 

188 
 Some v => v) 

2854  189 

190 
local 

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

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

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

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

198 
fun fromConst alist (a,T) = 

199 
case assoc_string (!overloads, a) of 

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

201 
 Some f => 

202 
let val T' = f T 

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

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

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

2854  207 
end; 
208 

209 

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

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

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

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

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

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

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

221 
 _ aconv _ = false; 

222 

223 

224 
fun mem_term (_, []) = false 

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

226 

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

228 

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

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

231 

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

233 

234 

235 
(** Vars **) 

236 

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

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

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

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

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

244 
 add_term_vars (_, vars) = vars 

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

246 
and add_terms_vars ([], vars) = vars 

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

248 
(*Var list version.*) 

249 
and add_vars_vars ([], vars) = vars 

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

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

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

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

254 

255 

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

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

258 

259 

260 

261 
(*increment a term's nonlocal bound variables 

262 
inc is increment for bound variables 

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

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

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

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

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

268 

269 
fun incr_boundvars 0 t = t 

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

271 

272 

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

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

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

276 
else (ilev) ins_int js 

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

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

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

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

281 

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

283 

284 
fun subst_bound (arg, t) : term = 

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

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

287 
else if i=lev then incr_boundvars lev arg 

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

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

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

291 
 subst (t,lev) = t 

292 
in subst (t,0) end; 

293 

294 

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

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

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

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

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

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

306 

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

308 
fun wkNormAux t = case t of 

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

310 
Some u => wkNorm u 

311 
 None => t) 

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

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

314 
 nf => nf $ u) 

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

317 
nb as (f $ t) => 

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

319 
then Abs(a,nb) 

320 
else wkNorm (incr_boundvars ~1 f) 

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

324 
Const _ => t 

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

328 
 _ => wkNormAux t; 

329 

330 

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

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

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

334 
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

335 
 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

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

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

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

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

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

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

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

344 
 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

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

346 
in occ 0 end; 
2854  347 

348 
exception UNIFY; 

349 

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

351 
val ntrail = ref 0; 

352 

353 

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

355 
fun clearTo n = 

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

359 
ntrail := !ntrail  1); 

360 

361 

362 
(*Firstorder unification with bound variables. 

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

364 
on the trail (no point in doing so) 

365 
*) 

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

369 
if t aconv u then () 

370 
else if varOccur v u then raise UNIFY 

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

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

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

374 
then dest_Var u := Some t 

375 
else (v := Some u; 

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

377 
fun unifyAux (t,u) = 

378 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

390 

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

393 
fun fromTerm t = 

394 
let val alistVar = ref [] 

395 
and alistTVar = ref [] 

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

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

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

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

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

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

409 
else incr_boundvars ~1 f 

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

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

412 
in from t end; 

413 

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

416 
fun instVars t = 

417 
let val name = ref "A" 

418 
val updated = ref [] 

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

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

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

422 
name := bump_string (!name)) 

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

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

425 
 inst _ = () 

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

427 
in inst t; revert end; 

428 

429 

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

432 
A :: strip_imp_prems B 

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

434 
 strip_imp_prems _ = []; 

435 

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

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

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

439 
 strip_imp_concl A = A : term; 

440 

441 

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

443 

9170  444 
exception ElimBadConcl and ElimBadPrem; 
445 

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

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

448 
PROOF FAILED*) 

449 
fun delete_concl [] = raise ElimBadPrem 

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

451 
Ps 

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

453 
Ps 

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

2854  455 

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

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

458 
 skoPrem vars P = P; 

459 

460 
fun convertPrem t = 

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

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

464 
fun convertRule vars t = 

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

466 
val Var v = strip_imp_concl t 

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

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

9170  469 
end 
470 
handle Bind => raise ElimBadConcl; 

2854  471 

472 

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

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

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

476 

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

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

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

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

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

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

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

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

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

485 
 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

486 
 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

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

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

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

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

491 

2854  492 

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

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

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

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

496 
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

497 
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

498 
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

499 

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

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

501 
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

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

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

506 
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

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

508 
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

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

512 
Option.NONE) 

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

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

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

516 
else (); 

517 
Option.NONE); 

2854  518 

519 

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

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

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

523 

524 
fun convertIntrRule vars t = 

525 
let val Ps = strip_imp_prems t 

526 
val P = strip_imp_concl t 

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

528 
end; 

529 

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

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

531 
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

532 
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

533 
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

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

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

538 
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

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

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

543 

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

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

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

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

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

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

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

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

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

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

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

558 

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

560 
case P of 

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

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

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

565 
nps) 

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

567 
 _ => 

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

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

571 
nps) 

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

573 

574 
(** 

575 
end; 

576 
**) 

577 

3092  578 

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

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

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

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

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

584 
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

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

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

588 

589 
(*Normalize a branchfor tracing*) 

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

591 

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

593 

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

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

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

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

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

598 
lim = lim}; 
3092  599 

600 

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

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

606 
 showType (Var _) = dummyTVar 

607 
 showType t = 

608 
(case strip_comb t of 

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

610 
 _ => dummyT); 

611 

612 
(*Display toplevel overloading if any*) 

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

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

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

616 
None => topType u 

617 
 some => some) 

618 
 topType _ = None; 

619 

620 

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

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

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

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

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

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

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

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

633 

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

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

638 
val stm = string_of sign 8 t' 

639 
in 

640 
case topType t' of 

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

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

643 
end; 

3092  644 

645 

5961  646 
val prs = std_output; 
647 

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

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

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

652 
 printPairs _ = () 

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

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

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

657 
printPairs pairs; 

658 
writeln"") 

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

660 
end; 

661 

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

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

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

667 
(case !ntrailntrl of 

668 
0 => () 

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

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

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

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

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

674 
writeln"") 

3092  675 
else (); 
676 

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

678 
fun traceNew prems = 

679 
if !trace then 

680 
case length prems of 

681 
0 => prs"branch closed by rule" 

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

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

684 
else (); 

685 

686 

687 

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

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

691 
fun subst_atomic (old,new) t = 

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

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

694 
 subst (f$t) = subst f $ subst t 

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

696 
in subst t end; 

697 

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

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

700 
(case eta_contract2 body of 

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

702 
else eta_contract_atom (incr_boundvars ~1 f) 

703 
 _ => t0) 

704 
 eta_contract_atom t = t 

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

706 
 eta_contract2 t = eta_contract_atom t; 

707 

708 

709 
(*When can we safely delete the equality? 

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

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

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

713 
Prefer to eliminate Bound variables if possible. 

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

715 

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

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

717 
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

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

720 
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

721 
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

722 
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

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

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

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

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

727 
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

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

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

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

733 
in occEq end; 

734 

3092  735 
exception DEST_EQ; 
736 

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

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

739 
(eta_contract_atom t, eta_contract_atom u) 

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

743 

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

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

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

748 
THEN orient that equality ELSE raise exception DEST_EQ*) 

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

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

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

754 
 _ => raise DEST_EQ; 

755 

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

758 
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

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

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

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

764 
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

765 
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

766 
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

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

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

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

770 
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

771 
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

772 
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

773 
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

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

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

777 
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

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

780 
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

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

784 
else (); 

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

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

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

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

788 
lim = lim} 
2854  789 
end; 
790 

791 

792 
exception NEWBRANCHES and CLOSEF; 

793 

794 
exception PROVE; 

795 

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

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

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

798 
(eq_assume_tac ORELSE' assume_tac); 
2854  799 

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

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

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

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

814 

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

816 
fun hasSkolem (Skolem _) = true 

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

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

819 
 hasSkolem _ = false; 

820 

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

822 
Skolem terms then allow duplication.*) 

823 
fun joinMd md [] = [] 

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

825 

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

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

829 
 negOfGoal G = G; 

830 

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

832 

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

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

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

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

837 

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

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

839 
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

840 
rotate_tac ~1 i; 
2894  841 

2854  842 

843 
(** Backtracking and Pruning **) 

844 

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

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

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

848 
 clashVar vars = 

849 
let fun clash (0, _) = false 

850 
 clash (_, []) = false 

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

852 
in clash end; 

853 

854 

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

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

857 
next branch have been updated.*) 

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

859 
backtracking over bad proofs*) 

860 
 prune (nbrs, nxtVars, choices) = 

861 
let fun traceIt last = 

862 
let val ll = length last 

863 
and lc = length choices 

864 
in if !trace andalso ll<lc then 

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

868 
end 

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

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

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

874 
else (* nbrs'=nbrs *) 

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

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

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

878 
choices) 

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

880 

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

881 
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

882 
 nextVars [] = []; 
2854  883 

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

886 
Int.toString nbrs ^ " branches")) 

887 
else (); 

888 
raise exn) 

889 
 backtrack _ = raise PROVE; 

2854  890 

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

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

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

896 
 bad _ = false; 

897 
fun change [] = [] 

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

899 
if G aconv G' then change lits 

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

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

902 
if G aconv G' then change lits 

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

904 
 change (lit::lits) = lit :: change lits 

905 
in 

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

907 
end 

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

909 

910 

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

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

914 

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

915 

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

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

917 
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

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

921 
 match (Const a) (Const b) = (a=b) 

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

923 
 match (Free a) (Free b) = (a=b) 

924 
 match (Bound i) (Bound j) = (i=j) 

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

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

927 
 match t u = false; 

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

928 

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

929 

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

932 
val nclosed = ref 0 

933 
and ntried = ref 1; 

934 

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

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

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

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

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

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

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

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

942 

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

943 

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

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

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

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

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

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

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

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

957 
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

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

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

963 
val nbrs = length brs0 

964 
val nxtVars = nextVars brs 

965 
val G = norm G 

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

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

970 
if (exists isGoal prem) 

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

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

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

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

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

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

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

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

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

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

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

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

984 
to branch.*) 

985 
fun deeper [] = raise NEWBRANCHES 

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

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

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

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

993 
val vars = vars_in_vars vars 

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

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

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

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

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

1003 
prune (nbrs, nxtVars, choices'), 

1004 
brs)) 

1005 
else (*prems nonnull*) 

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

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

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

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

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

1017 
(clearTo ntrl; deeper grls) 

1018 
else (*backtrack to previous level*) 

1019 
backtrack choices 

1020 
end 

1021 
else deeper grls 

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

1024 
 closeF (L::Ls) = 

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

1027 
 Some tac => 

1028 
let val choices' = 

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

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

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

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

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

1039 
(clearTo ntrl; closeF Ls) 

1040 
end 

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

1043 
closeF (map fst br) 

1044 
handle CLOSEF => closeF (map fst haz) 

1045 
handle CLOSEF => closeFl pairs 

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

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

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

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

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

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

1057 
handle CLOSEF => deeper rules 

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

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

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

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

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

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

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

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

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

1069 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1093 
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

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

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

1096 
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

1097 
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

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

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

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

1101 
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

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

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

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

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

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

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

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

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

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

1113 
to branch.*) 

1114 
fun deeper [] = raise NEWBRANCHES 

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

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

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

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

1122 
val dup = md andalso vars' <> vars 

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

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

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

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

1130 
both dup and recur are false. Proofs are 

1131 
found at shallower depths, but looping 

1132 
occurs too often...*) 

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

1135 
if other matching rules exist, if the rule 

1136 
updated variables, or if the rule did not 

1137 
introduce new variables. This latter condition 

1138 
means it is not a standard "gammarule" but 

1139 
some other form of unsafe rule. Aim is to 

1140 
emulate Fast_tac, which allows all unsafe steps 

1141 
to be undone.*) 

1142 
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

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

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

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

1147 
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

1148 
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

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

1150 

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

1153 
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

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

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

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

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

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

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

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

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

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

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

1170 
(clearTo ntrl; deeper grls) 

1171 
else (*backtrack to previous level*) 

1172 
backtrack choices 

1173 
end 

1174 
else deeper grls 

1175 
in tracing sign brs0; 

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

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

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

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

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

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

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

1189 
end; 

2854  1190 

1191 

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

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

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

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

1197 
lim = lim}; 
2854  1198 

1199 

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

1201 

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

1203 
local open Term 

1204 
in 

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

1206 
 discard_foralls t = t; 

1207 
end; 

1208 

1209 

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

1211 
fun getVars [] i = [] 

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

1213 
if i mem is then getVars alist i 

1214 
else v :: getVars alist i; 

1215 

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

1216 
exception TRANS of string; 
2854  1217 

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

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

1221 
and alistTVar = ref [] 

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

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

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

1226 
fun bounds [] = [] 

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

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

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

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

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

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

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

1238 
 Term.Var (ix,_) => 

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

1241 
:: !alistVar; 

1242 
Var (hdvar(!alistVar))) 

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

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

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

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

1252 
val npars = length (Logic.strip_params t) 

1253 

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

1255 
fun skoSubgoal i t = 

1256 
if i<npars then 

1257 
skoSubgoal (i+1) 

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

1261 

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

1263 

1264 

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

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

1268 

1269 

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

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

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

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

1275 
(initialize(); 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

1276 
let val st = Method.atomize_goal Data.atomize i st0; 
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1295 
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

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

1297 
handle PROVE => Seq.empty); 
2854  1298 

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

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

1300 
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

1301 

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

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

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

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

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

4078  1307 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1308 

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

1309 

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

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

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

1312 

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

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

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

1316 
let val st = topthm() 
3030  1317 
val {sign,...} = rep_thm st 
4065  1318 
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

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

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

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

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

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

1324 
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

1325 

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

1327 

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

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

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

1331 

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

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

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

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

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

1339 

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

1340 

5926  1341 
(** method setup **) 
1342 

7559  1343 
fun blast_args m = 
9779  1344 
Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; 
7155  1345 

9779  1346 
fun blast_meth None = Data.cla_meth' blast_tac 
1347 
 blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim); 

7155  1348 

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

5926  1350 

1351 

2854  1352 
end; 