author  paulson 
Fri, 23 Oct 1998 11:03:35 +0200  
changeset 5734  bebd10cb7a8d 
parent 5613  5cb6129566e7 
child 5926  58f9ca06b76b 
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, 

4651  65 
swrappers: (string * wrapper) list, 
66 
uwrappers: (string * wrapper) list, 

2854  67 
safe0_netpair: netpair, safep_netpair: netpair, 
68 
haz_netpair: netpair, dup_netpair: netpair} 

69 
end; 

70 

71 

72 
signature BLAST = 

73 
sig 

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

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

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

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

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

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

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

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

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

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

85 
type branch 
2883  86 
val depth_tac : claset > int > int > tactic 
87 
val blast_tac : claset > int > tactic 

88 
val Blast_tac : int > tactic 

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

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

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

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

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

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

96 
val fromSubgoal : Term.term > term 

97 
val instVars : term > (unit > unit) 

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

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

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

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

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

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

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

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

109 

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

113 
type claset = Data.claset; 

114 

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

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

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

118 
datatype term = 

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

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

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

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

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

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

128 

129 
(** Basic syntactic operations **) 

130 

131 
fun is_Var (Var _) = true 

132 
 is_Var _ = false; 

133 

134 
fun dest_Var (Var x) = x; 

135 

136 

137 
fun rand (f$x) = x; 

138 

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

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

141 

142 

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

144 
fun strip_comb u : term * term list = 

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

146 
 stripc x = x 

147 
in stripc(u,[]) end; 

148 

149 

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

151 
fun head_of (f$t) = head_of f 

152 
 head_of u = u; 

153 

154 

155 
(** Particular constants **) 

156 

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

158 

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

160 

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

162 
 isGoal _ = false; 

163 

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

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

166 

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

168 
 isTrueprop _ = false; 

169 

170 

4065  171 
(*** Dealing with overloaded constants ***) 
2854  172 

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

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

176 
map (fromType alist) Ts) 

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

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

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

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

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

182 
end 

183 
 Some v => v) 

2854  184 

185 
local 

4065  186 
val overloads = ref ([]: (string * (Term.typ > Term.typ)) list) 
2854  187 
in 
188 

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

189 
fun overloaded arg = (overloads := arg :: (!overloads)); 
2854  190 

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

193 
fun fromConst alist (a,T) = 

194 
case assoc_string (!overloads, a) of 

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

196 
 Some f => 

197 
let val T' = f T 

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

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

199 
("Blast_tac: unexpected type for overloaded constant " ^ a) 
4065  200 
in TConst(a, fromType alist T') end; 
201 

2854  202 
end; 
203 

204 

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

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

4065  207 
 (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb 
2854  208 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
209 
 (Free a) aconv (Free b) = a=b 

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

4065  211 
 t aconv (Var(ref(Some u))) = t aconv u 
2854  212 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
213 
 (Bound i) aconv (Bound j) = i=j 

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

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

216 
 _ aconv _ = false; 

217 

218 

219 
fun mem_term (_, []) = false 

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

221 

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

223 

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

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

226 

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

228 

229 

230 
(** Vars **) 

231 

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

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

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

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

4065  236 
 add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) 
2854  237 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
238 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

239 
 add_term_vars (_, vars) = vars 

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

241 
and add_terms_vars ([], vars) = vars 

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

243 
(*Var list version.*) 

244 
and add_vars_vars ([], vars) = vars 

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

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

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

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

249 

250 

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

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

253 

254 

255 

256 
(*increment a term's nonlocal bound variables 

257 
inc is increment for bound variables 

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

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

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

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

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

263 

264 
fun incr_boundvars 0 t = t 

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

266 

267 

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

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

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

271 
else (ilev) ins_int js 

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

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

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

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

276 

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

278 

279 
fun subst_bound (arg, t) : term = 

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

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

282 
else if i=lev then incr_boundvars lev arg 

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

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

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

286 
 subst (t,lev) = t 

287 
in subst (t,0) end; 

288 

289 

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

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

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

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

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

298 
 nf => nf $ norm u) 
2854  299 
 _ => t; 
300 

301 

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

303 
fun wkNormAux t = case t of 

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

305 
Some u => wkNorm u 

306 
 None => t) 

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

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

309 
 nf => nf $ u) 

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

312 
nb as (f $ t) => 

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

314 
then Abs(a,nb) 

315 
else wkNorm (incr_boundvars ~1 f) 

3092  316 
 nb => Abs (a,nb)) 
2854  317 
 _ => t 
318 
and wkNorm t = case head_of t of 

319 
Const _ => t 

4065  320 
 TConst _ => t 
2854  321 
 Skolem(a,args) => t 
322 
 Free _ => t 

323 
 _ => wkNormAux t; 

324 

325 

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

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

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

329 
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

330 
 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

331 
and occ lev (Var w) = 
2854  332 
v=w orelse 
333 
(case !w of None => false 

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

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

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

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

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

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

339 
 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

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

341 
in occ 0 end; 
2854  342 

343 
exception UNIFY; 

344 

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

346 
val ntrail = ref 0; 

347 

348 

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

350 
fun clearTo n = 

3083  351 
while !ntrail<>n do 
2854  352 
(hd(!trail) := None; 
353 
trail := tl (!trail); 

354 
ntrail := !ntrail  1); 

355 

356 

357 
(*Firstorder unification with bound variables. 

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

359 
on the trail (no point in doing so) 

360 
*) 

4065  361 
fun unify(vars,t,u) = 
2854  362 
let val n = !ntrail 
363 
fun update (t as Var v, u) = 

364 
if t aconv u then () 

365 
else if varOccur v u then raise UNIFY 

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

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

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

369 
then dest_Var u := Some t 

370 
else (v := Some u; 

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

372 
fun unifyAux (t,u) = 

373 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

3083  382 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  383 
end; 
384 

385 

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

388 
fun fromTerm t = 

389 
let val alistVar = ref [] 

390 
and alistTVar = ref [] 

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

2854  392 
 from (Term.Free (a,_)) = Free a 
393 
 from (Term.Bound i) = Bound i 

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

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

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

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

404 
else incr_boundvars ~1 f 

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

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

407 
in from t end; 

408 

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

411 
fun instVars t = 

412 
let val name = ref "A" 

413 
val updated = ref [] 

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

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

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

417 
name := bump_string (!name)) 

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

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

420 
 inst _ = () 

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

422 
in inst t; revert end; 

423 

424 

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

427 
A :: strip_imp_prems B 

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

429 
 strip_imp_prems _ = []; 

430 

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

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

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

434 
 strip_imp_concl A = A : term; 

435 

436 

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

438 

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

440 
fun squash_nots [] = [] 

441 
 squash_nots (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) = 

442 
squash_nots Ps 

443 
 squash_nots (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) = 

444 
squash_nots Ps 

445 
 squash_nots (P::Ps) = P :: squash_nots Ps; 

446 

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

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

449 
 skoPrem vars P = P; 

450 

451 
fun convertPrem t = 

452 
squash_nots (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 

453 

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

455 
fun convertRule vars t = 

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

457 
val Var v = strip_imp_concl t 

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

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

460 
end; 

461 

462 

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

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

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

466 

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

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

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

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

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

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

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

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

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

475 
 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

476 
 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

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

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

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

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

481 

2854  482 

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

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

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

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

486 
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

487 
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

488 
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

489 

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

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

491 
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

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

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

496 
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

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

498 
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

499 
in Option.SOME (trl, tac) end 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

500 
handle Bind => (*reject: conclusion is not just a variable*) 
3533  501 
(if !trace then (warning ("ignoring illformed elimination rule\n" ^ 
502 
string_of_thm rl)) 

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

503 
else (); 
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3101
diff
changeset

504 
Option.NONE); 
2854  505 

506 

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

507 
(*** Conversion of Introduction Rules ***) 
2854  508 

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

510 

511 
fun convertIntrRule vars t = 

512 
let val Ps = strip_imp_prems t 

513 
val P = strip_imp_concl t 

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

515 
end; 

516 

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

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

518 
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

519 
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

520 
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

521 
introduction rules.*) 
2854  522 
fun fromIntrRule vars rl = 
4065  523 
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

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

525 
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

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

527 
rot_subgoals_tac (rot, #2 trl) i 
2854  528 
in (trl, tac) end; 
529 

530 

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

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

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

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

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

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

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

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

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

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

543 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  544 

545 

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

547 
case P of 

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

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

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

552 
nps) 

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

554 
 _ => 

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

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

558 
nps) 

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

560 

561 
(** 

562 
end; 

563 
**) 

564 

3092  565 

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

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

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

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

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

571 
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

572 
lim: int}; (*resource limit*) 
3092  573 

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

575 

576 
(*Normalize a branchfor tracing*) 

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

578 

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

580 

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

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

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

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

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

585 
lim = lim}; 
3092  586 

587 

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

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

593 
 showType (Var _) = dummyTVar 

594 
 showType t = 

595 
(case strip_comb t of 

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

597 
 _ => dummyT); 

598 

599 
(*Display toplevel overloading if any*) 

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

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

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

603 
None => topType u 

604 
 some => some) 

605 
 topType _ = None; 

606 

607 

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

4065  610 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  611 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
612 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

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

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

615 
 showTerm d (Var(ref None)) = dummyVar2 
3092  616 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
617 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

620 

4065  621 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  622 

4065  623 
fun traceTerm sign t = 
624 
let val t' = norm t 

625 
val stm = string_of sign 8 t' 

626 
in 

627 
case topType t' of 

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

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

630 
end; 

3092  631 

632 

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

634 
fun tracing sign brs = 

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

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

637 
 printPairs _ = () 

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

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

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

642 
printPairs pairs; 

643 
writeln"") 

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

645 
end; 

646 

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

647 
fun traceMsg s = if !trace then writeln s else (); 
4065  648 

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

652 
(case !ntrailntrl of 

653 
0 => () 

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

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

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

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

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

659 
writeln"") 

3092  660 
else (); 
661 

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

663 
fun traceNew prems = 

664 
if !trace then 

665 
case length prems of 

666 
0 => prs"branch closed by rule" 

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

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

669 
else (); 

670 

671 

672 

2854  673 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
674 

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

676 
fun subst_atomic (old,new) t = 

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

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

679 
 subst (f$t) = subst f $ subst t 

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

681 
in subst t end; 

682 

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

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

685 
(case eta_contract2 body of 

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

687 
else eta_contract_atom (incr_boundvars ~1 f) 

688 
 _ => t0) 

689 
 eta_contract_atom t = t 

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

691 
 eta_contract2 t = eta_contract_atom t; 

692 

693 

694 
(*When can we safely delete the equality? 

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

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

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

698 
Prefer to eliminate Bound variables if possible. 

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

700 

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

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

702 
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

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

705 
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

706 
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

707 
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

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

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

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

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

712 
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

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

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

715 
 occ (Abs(_,u)) = occEq u 
2854  716 
 occ (f$u) = occEq u orelse occEq f 
717 
 occ (_) = false; 

718 
in occEq end; 

719 

3092  720 
exception DEST_EQ; 
721 

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

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

724 
(eta_contract_atom t, eta_contract_atom u) 

4065  725 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  726 
(eta_contract_atom t, eta_contract_atom u) 
727 
 dest_eq _ = raise DEST_EQ; 

728 

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

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

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

733 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  734 
fun orientGoal (t,u) = case (t,u) of 
2854  735 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
736 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

739 
 _ => raise DEST_EQ; 

740 

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

743 
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

744 
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092  745 
let val (t,u) = orientGoal(dest_eq G) 
746 
val subst = subst_atomic (t,u) 

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

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

749 
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

750 
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

751 
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

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

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

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

755 
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

756 
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

757 
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

758 
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

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

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

762 
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

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

765 
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

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

769 
else (); 

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

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

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

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

773 
lim = lim} 
2854  774 
end; 
775 

776 

777 
exception NEWBRANCHES and CLOSEF; 

778 

779 
exception PROVE; 

780 

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

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

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

783 
(eq_assume_tac ORELSE' assume_tac); 
2854  784 

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

785 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  786 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
787 

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

3083  789 
fun tryClose (Const"*Goal*" $ G, L) = 
4065  790 
if unify([],G,L) then Some eAssume_tac else None 
3083  791 
 tryClose (G, Const"*Goal*" $ L) = 
4065  792 
if unify([],G,L) then Some eAssume_tac else None 
3083  793 
 tryClose (Const"Not" $ G, L) = 
4065  794 
if unify([],G,L) then Some eContr_tac else None 
3083  795 
 tryClose (G, Const"Not" $ L) = 
4065  796 
if unify([],G,L) then Some eContr_tac else None 
3083  797 
 tryClose _ = None; 
2854  798 

799 

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

801 
fun hasSkolem (Skolem _) = true 

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

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

804 
 hasSkolem _ = false; 

805 

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

807 
Skolem terms then allow duplication.*) 

808 
fun joinMd md [] = [] 

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

810 

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

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

814 
 negOfGoal G = G; 

815 

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

817 

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

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

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

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

822 

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

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

824 
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

825 
rotate_tac ~1 i; 
2894  826 

2854  827 

828 
(** Backtracking and Pruning **) 

829 

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

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

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

833 
 clashVar vars = 

834 
let fun clash (0, _) = false 

835 
 clash (_, []) = false 

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

837 
in clash end; 

838 

839 

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

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

842 
next branch have been updated.*) 

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

844 
backtracking over bad proofs*) 

845 
 prune (nbrs, nxtVars, choices) = 

846 
let fun traceIt last = 

847 
let val ll = length last 

848 
and lc = length choices 

849 
in if !trace andalso ll<lc then 

3083  850 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  851 
last) 
852 
else last 

853 
end 

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

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

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

859 
else (* nbrs'=nbrs *) 

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

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

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

863 
choices) 

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

865 

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

866 
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

867 
 nextVars [] = []; 
2854  868 

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

871 
Int.toString nbrs ^ " branches")) 

872 
else (); 

873 
raise exn) 

874 
 backtrack _ = raise PROVE; 

2854  875 

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

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

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

881 
 bad _ = false; 

882 
fun change [] = [] 

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

884 
if G aconv G' then change lits 

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

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

887 
if G aconv G' then change lits 

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

889 
 change (lit::lits) = lit :: change lits 

890 
in 

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

892 
end 

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

894 

895 

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

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

899 

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

900 

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

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

902 
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

903 
fun match (Var _) u = true 
4065  904 
 match (Const"*Goal*") (Const"Not") = true 
905 
 match (Const"Not") (Const"*Goal*") = true 

906 
 match (Const a) (Const b) = (a=b) 

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

908 
 match (Free a) (Free b) = (a=b) 

909 
 match (Bound i) (Bound j) = (i=j) 

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

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

912 
 match t u = false; 

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

913 

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

914 

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

917 
val nclosed = ref 0 

918 
and ntried = ref 1; 

919 

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

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

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

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

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

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

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

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

927 

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

928 

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

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

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

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

934 
fun prove (sign, start, cs, brs, cont) = 
4653  935 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  936 
val safeList = [safe0_netpair, safep_netpair] 
937 
and hazList = [haz_netpair] 

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

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

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

942 
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

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

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

948 
val nbrs = length brs0 

949 
val nxtVars = nextVars brs 

950 
val G = norm G 

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

951 
val rules = netMkRules G vars safeList 
2854  952 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  953 
fun newBr (vars',lim') prems = 
954 
map (fn prem => 

955 
if (exists isGoal prem) 

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

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

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

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

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

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

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

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

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

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

965 
lim = lim'}) 
2854  966 
prems @ 
967 
brs 

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

969 
to branch.*) 

970 
fun deeper [] = raise NEWBRANCHES 

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

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

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

975 
val lim' = if updated 
3083  976 
then lim  (1+log(length rules)) 
977 
else lim (*discourage branching updates*) 

978 
val vars = vars_in_vars vars 

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

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

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

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

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

988 
prune (nbrs, nxtVars, choices'), 

989 
brs)) 

990 
else (*prems nonnull*) 

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

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

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

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

999 
if updated then 
3083  1000 
(*Backtrack at this level. 
1001 
Reset Vars and try another rule*) 

1002 
(clearTo ntrl; deeper grls) 

1003 
else (*backtrack to previous level*) 

1004 
backtrack choices 

1005 
end 

1006 
else deeper grls 

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

1009 
 closeF (L::Ls) = 

3083  1010 
case tryClose(G,L) of 
1011 
None => closeF Ls 

1012 
 Some tac => 

1013 
let val choices' = 

3092  1014 
(if !trace then (prs"branch closed"; 
4065  1015 
traceVars sign ntrl) 
3083  1016 
else (); 
1017 
prune (nbrs, nxtVars, 

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

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

3083  1021 
handle PRV => 
1022 
(*reset Vars and try another literal 

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

1024 
(clearTo ntrl; closeF Ls) 

1025 
end 

2894  1026 
fun closeFl [] = raise CLOSEF 
1027 
 closeFl ((br, haz)::pairs) = 

1028 
closeF (map fst br) 

1029 
handle CLOSEF => closeF (map fst haz) 

1030 
handle CLOSEF => closeFl pairs 

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

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

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

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

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

1039 
:: brs) 
4065  1040 
handle DEST_EQ => closeF lits 
1041 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1042 
handle CLOSEF => deeper rules 

2894  1043 
handle NEWBRANCHES => 
1044 
(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

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

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

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

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

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

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

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

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

1054 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1078 
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

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

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

1081 
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

1082 
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

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

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

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

1086 
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

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

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

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

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

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

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

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

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

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

1098 
to branch.*) 

1099 
fun deeper [] = raise NEWBRANCHES 

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

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

1103 
let val updated = ntrl < !ntrail (*branch updated*) 
3083  1104 
val vars = vars_in_vars vars 
1105 
val vars' = foldr add_terms_vars (prems, vars) 

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

1107 
val dup = md andalso vars' <> vars 

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

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

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

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

1115 
both dup and recur are false. Proofs are 

1116 
found at shallower depths, but looping 

1117 
occurs too often...*) 

3917  1118 
val mayUndo = 
1119 
(*Allowing backtracking from a rule application 

1120 
if other matching rules exist, if the rule 

1121 
updated variables, or if the rule did not 

1122 
introduce new variables. This latter condition 

1123 
means it is not a standard "gammarule" but 

1124 
some other form of unsafe rule. Aim is to 

1125 
emulate Fast_tac, which allows all unsafe steps 

1126 
to be undone.*) 

1127 
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

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

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

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

1132 
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

1133 
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

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

1135 

3083  1136 
in 
1137 
if lim'<0 andalso not (null prems) 

1138 
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

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

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

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

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

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

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

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

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

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

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

1155 
(clearTo ntrl; deeper grls) 

1156 
else (*backtrack to previous level*) 

1157 
backtrack choices 

1158 
end 

1159 
else deeper grls 

1160 
in tracing sign brs0; 

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

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

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

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

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

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

4065  1172 
in init_gensym(); 
1173 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1174 
end; 

2854  1175 

1176 

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

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

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

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

1182 
lim = lim}; 
2854  1183 

1184 

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

1186 

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

1188 
local open Term 

1189 
in 

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

1191 
 discard_foralls t = t; 

1192 
end; 

1193 

1194 

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

1196 
fun getVars [] i = [] 

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

1198 
if i mem is then getVars alist i 

1199 
else v :: getVars alist i; 

1200 

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

1201 
exception TRANS of string; 
2854  1202 

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

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

1206 
and alistTVar = ref [] 

2854  1207 
fun hdvar ((ix,(v,is))::_) = v 
1208 
fun from lev t = 

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

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

1211 
fun bounds [] = [] 

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

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

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

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

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

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

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

1223 
 Term.Var (ix,_) => 

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

1226 
:: !alistVar; 

1227 
Var (hdvar(!alistVar))) 

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

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

1231 
^ Syntax.string_of_vname ix)) 
2854  1232 
 Term.Abs (a,_,body) => 
1233 
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

1234 
else raise TRANS "argument not in normal form" 
2854  1235 
end 
1236 

1237 
val npars = length (Logic.strip_params t) 

1238 

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

1240 
fun skoSubgoal i t = 

1241 
if i<npars then 

1242 
skoSubgoal (i+1) 

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

1246 

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

1248 

1249 

4300  1250 
fun initialize() = 
1251 
(fullTrace:=[]; trail := []; ntrail := 0; 

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

1253 

1254 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1279 
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

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

1281 
handle PROVE => Seq.empty); 
2854  1282 

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

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

1284 
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

1285 

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

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

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

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

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

4078  1291 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1292 

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

1293 

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

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

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

1296 

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

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

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

1300 
let val st = topthm() 
3030  1301 
val {sign,...} = rep_thm st 
4065  1302 
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

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

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

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

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

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

1308 
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

1309 

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

1311 

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

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

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

1315 

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

1316 
fun tryInThy thy lim s = 
4300  1317 
(initialize(); 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1318 
timeap prove (sign_of thy, 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

1320 
Data.claset(), 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1321 
[initBranch ([readGoal (sign_of thy) s], lim)], 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

1323 

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

1324 

2854  1325 
end; 