author  paulson 
Mon, 06 Aug 2001 12:42:43 +0200  
changeset 11461  ffeac9aa1967 
parent 11152  32d002362005 
child 11754  3928d990c22f 
permissions  rwrr 
4078  1 
(* Title: Provers/blast.ML 
2894  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3083  4 
Copyright 1997 University of Cambridge 
2894  5 

6 
Generic tableau prover with proof reconstruction 

7 

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

11 

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

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

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

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

18 
* ignores types, which can make HOL proofs fail 

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

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

20 
+ message "Function Var's argument not a bound variable" relates to this 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

23 
Known problems: 

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

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

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

28 
the formulae get into the wrong order (see WRONG below). 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

29 

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

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

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

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

34 
"Relation.op ^^". 
2952  35 

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

36 
With substition for equalities (hyp_subst_tac): 
3092  37 
When substitution affects a haz formula or literal, it is moved 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

39 
But there's no way of putting it in the right place. A "moved" or 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

43 
(*Should be a type abbreviation?*) 

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

45 

46 

47 
(*Assumptions about constants: 

48 
The negation symbol is "Not" 

49 
The equality symbol is "op =" 

50 
The istrue judgement symbol is "Trueprop" 

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

52 
*) 

53 
signature BLAST_DATA = 

54 
sig 

55 
type claset 

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

57 
val ccontr : thm 

58 
val contr_tac : int > tactic 

59 
val dup_intr : thm > thm 

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

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

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

2854  68 
safe0_netpair: netpair, safep_netpair: netpair, 
6955  69 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

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

75 

76 
signature BLAST = 

77 
sig 

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

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

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

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

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

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

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

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

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

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

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

92 
val Blast_tac : int > tactic 

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

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

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

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

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

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

102 
val fromSubgoal : Term.term > term 

103 
val instVars : term > (unit > unit) 

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

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

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

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

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

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

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

115 

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

119 
type claset = Data.claset; 

10400  120 
val atomize_goal = Method.atomize_goal Data.atomize; 
2854  121 

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

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

123 
and stats = ref false; (*for runtime and search statistics*) 
2854  124 

125 
datatype term = 

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

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

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

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

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

132 
 Abs of string*term 
5613  133 
 op $ of term*term; 
2854  134 

135 

136 
(** Basic syntactic operations **) 

137 

138 
fun is_Var (Var _) = true 

139 
 is_Var _ = false; 

140 

141 
fun dest_Var (Var x) = x; 

142 

143 

144 
fun rand (f$x) = x; 

145 

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

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

148 

149 

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

151 
fun strip_comb u : term * term list = 

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

153 
 stripc x = x 

154 
in stripc(u,[]) end; 

155 

156 

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

158 
fun head_of (f$t) = head_of f 

159 
 head_of u = u; 

160 

161 

162 
(** Particular constants **) 

163 

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

165 

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

167 

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

169 
 isGoal _ = false; 

170 

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

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

173 

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

175 
 isTrueprop _ = false; 

176 

177 

4065  178 
(*** Dealing with overloaded constants ***) 
2854  179 

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

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

183 
map (fromType alist) Ts) 

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

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

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

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

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

189 
end 

190 
 Some v => v) 

2854  191 

192 
local 

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

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

196 
fun overloaded arg = (overloads := arg :: (!overloads)); 
2854  197 

11119  198 
fun get_overloads() = !overloads; 
199 

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

202 
fun fromConst alist (a,T) = 

203 
case assoc_string (!overloads, a) of 

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

205 
 Some f => 

206 
let val T' = f T 

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

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

208 
("Blast_tac: unexpected type for overloaded constant " ^ a) 
4065  209 
in TConst(a, fromType alist T') end; 
210 

2854  211 
end; 
212 

213 

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

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

4065  216 
 (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb 
2854  217 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
218 
 (Free a) aconv (Free b) = a=b 

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

4065  220 
 t aconv (Var(ref(Some u))) = t aconv u 
2854  221 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
222 
 (Bound i) aconv (Bound j) = i=j 

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

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

225 
 _ aconv _ = false; 

226 

227 

228 
fun mem_term (_, []) = false 

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

230 

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

232 

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

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

235 

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

237 

238 

239 
(** Vars **) 

240 

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

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

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

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

4065  245 
 add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) 
2854  246 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
247 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

248 
 add_term_vars (_, vars) = vars 

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

250 
and add_terms_vars ([], vars) = vars 

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

252 
(*Var list version.*) 

253 
and add_vars_vars ([], vars) = vars 

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

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

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

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

258 

259 

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

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

262 

263 

264 

265 
(*increment a term's nonlocal bound variables 

266 
inc is increment for bound variables 

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

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

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

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

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

272 

273 
fun incr_boundvars 0 t = t 

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

275 

276 

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

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

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

280 
else (ilev) ins_int js 

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

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

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

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

285 

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

287 

288 
fun subst_bound (arg, t) : term = 

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

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

291 
else if i=lev then incr_boundvars lev arg 

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

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

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

295 
 subst (t,lev) = t 

296 
in subst (t,0) end; 

297 

298 

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

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

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

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

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

307 
 nf => nf $ norm u) 
2854  308 
 _ => t; 
309 

310 

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

312 
fun wkNormAux t = case t of 

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

314 
Some u => wkNorm u 

315 
 None => t) 

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

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

318 
 nf => nf $ u) 

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

321 
nb as (f $ t) => 

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

323 
then Abs(a,nb) 

324 
else wkNorm (incr_boundvars ~1 f) 

3092  325 
 nb => Abs (a,nb)) 
2854  326 
 _ => t 
327 
and wkNorm t = case head_of t of 

328 
Const _ => t 

4065  329 
 TConst _ => t 
2854  330 
 Skolem(a,args) => t 
331 
 Free _ => t 

332 
 _ => wkNormAux t; 

333 

334 

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

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

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

338 
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

339 
 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

340 
and occ lev (Var w) = 
2854  341 
v=w orelse 
342 
(case !w of None => false 

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

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

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

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

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

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

348 
 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

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

350 
in occ 0 end; 
2854  351 

352 
exception UNIFY; 

353 

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

355 
val ntrail = ref 0; 

356 

357 

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

359 
fun clearTo n = 

3083  360 
while !ntrail<>n do 
2854  361 
(hd(!trail) := None; 
362 
trail := tl (!trail); 

363 
ntrail := !ntrail  1); 

364 

365 

366 
(*Firstorder unification with bound variables. 

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

368 
on the trail (no point in doing so) 

369 
*) 

4065  370 
fun unify(vars,t,u) = 
2854  371 
let val n = !ntrail 
372 
fun update (t as Var v, u) = 

373 
if t aconv u then () 

374 
else if varOccur v u then raise UNIFY 

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

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

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

378 
then dest_Var u := Some t 

379 
else (v := Some u; 

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

381 
fun unifyAux (t,u) = 

382 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

3083  391 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  392 
end; 
393 

394 

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

397 
fun fromTerm t = 

398 
let val alistVar = ref [] 

399 
and alistTVar = ref [] 

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

2854  401 
 from (Term.Free (a,_)) = Free a 
402 
 from (Term.Bound i) = Bound i 

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

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

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

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

413 
else incr_boundvars ~1 f 

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

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

416 
in from t end; 

417 

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

420 
fun instVars t = 

421 
let val name = ref "A" 

422 
val updated = ref [] 

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

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

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

426 
name := bump_string (!name)) 

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

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

429 
 inst _ = () 

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

431 
in inst t; revert end; 

432 

433 

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

436 
A :: strip_imp_prems B 

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

438 
 strip_imp_prems _ = []; 

439 

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

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

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

443 
 strip_imp_concl A = A : term; 

444 

445 

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

447 

9170  448 
exception ElimBadConcl and ElimBadPrem; 
449 

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

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

452 
PROOF FAILED*) 

453 
fun delete_concl [] = raise ElimBadPrem 

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

455 
Ps 

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

457 
Ps 

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

2854  459 

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

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

462 
 skoPrem vars P = P; 

463 

464 
fun convertPrem t = 

9170  465 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  466 

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

468 
fun convertRule vars t = 

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

470 
val Var v = strip_imp_concl t 

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

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

9170  473 
end 
474 
handle Bind => raise ElimBadConcl; 

2854  475 

476 

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

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

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

480 

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

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

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

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

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

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

486 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  487 

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

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

489 
 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

490 
 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

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

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

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

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

495 

2854  496 

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

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

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

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

500 
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

501 
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

502 
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

503 

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

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

505 
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

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

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

510 
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

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

512 
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

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

516 
Option.NONE) 

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

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

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

520 
else (); 

521 
Option.NONE); 

2854  522 

523 

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

524 
(*** Conversion of Introduction Rules ***) 
2854  525 

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

527 

528 
fun convertIntrRule vars t = 

529 
let val Ps = strip_imp_prems t 

530 
val P = strip_imp_concl t 

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

532 
end; 

533 

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

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

535 
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

536 
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

537 
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

538 
introduction rules.*) 
2854  539 
fun fromIntrRule vars rl = 
4065  540 
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

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

542 
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

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

544 
rot_subgoals_tac (rot, #2 trl) i 
2854  545 
in (trl, tac) end; 
546 

547 

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

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

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

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

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

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

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

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

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

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

560 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  561 

562 

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

564 
case P of 

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

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

566 
let val pG = mk_tprop (toTerm 2 G) 
2854  567 
val intrs = List.concat 
568 
(map (fn (inet,_) => Net.unify_term inet pG) 

569 
nps) 

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

571 
 _ => 

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

572 
let val pP = mk_tprop (toTerm 3 P) 
2854  573 
val elims = List.concat 
574 
(map (fn (_,enet) => Net.unify_term enet pP) 

575 
nps) 

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

577 

3092  578 

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

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

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

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

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

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

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

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

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

588 

589 
(*Normalize a branchfor tracing*) 

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

591 

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

593 

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

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

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

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

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

598 
lim = lim}; 
3092  599 

600 

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

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

606 
 showType (Var _) = dummyTVar 

607 
 showType t = 

608 
(case strip_comb t of 

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

610 
 _ => dummyT); 

611 

612 
(*Display toplevel overloading if any*) 

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

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

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

616 
None => topType u 

617 
 some => some) 

618 
 topType _ = None; 

619 

620 

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

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

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

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

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

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

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

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

633 

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

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

638 
val stm = string_of sign 8 t' 

639 
in 

640 
case topType t' of 

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

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

643 
end; 

3092  644 

645 

5961  646 
val prs = std_output; 
647 

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

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

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

652 
 printPairs _ = () 

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

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

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

657 
printPairs pairs; 

658 
writeln"") 

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

660 
end; 

661 

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

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

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

667 
(case !ntrailntrl of 

668 
0 => () 

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

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

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

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

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

674 
writeln"") 

3092  675 
else (); 
676 

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

678 
fun traceNew prems = 

679 
if !trace then 

680 
case length prems of 

681 
0 => prs"branch closed by rule" 

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

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

684 
else (); 

685 

686 

687 

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

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

691 
fun subst_atomic (old,new) t = 

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

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

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

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

696 
in subst t end; 

697 

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

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

700 
(case eta_contract2 body of 

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

702 
else eta_contract_atom (incr_boundvars ~1 f) 

703 
 _ => t0) 

704 
 eta_contract_atom t = t 

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

706 
 eta_contract2 t = eta_contract_atom t; 

707 

708 

709 
(*When can we safely delete the equality? 

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

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

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

713 
Prefer to eliminate Bound variables if possible. 

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

715 

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

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

717 
Does NOT examine the args of Skolem terms: substitution does not affect them. 
4196
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

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

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

721 
a Skolem term. This ensures that no equations are deleted that could 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

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

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

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

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

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

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

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

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

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

733 
in occEq end; 

734 

3092  735 
exception DEST_EQ; 
736 

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

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

739 
(eta_contract_atom t, eta_contract_atom u) 

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

743 

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

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

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

748 
THEN orient that equality ELSE raise exception DEST_EQ*) 

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

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

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

754 
 _ => raise DEST_EQ; 

755 

2894  756 
(*Substitute through the branch if an equality goal (else raise DEST_EQ). 
757 
Moves affected literals back into the branch, but it is not clear where 

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

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

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

2854  762 
fun subst2(G,md) = (subst G, md) 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

763 
(*substitute throughout list; extract affected formulae*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

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

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

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

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

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

769 
(*substitute throughout "stack frame"; extract affected formulae*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

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

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

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

773 
in (changed'', (Gs',Hs')::frames) end 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

774 
(*substitute throughout literals; extract affected ones*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

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

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

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

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

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

784 
else (); 

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

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

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

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

788 
lim = lim} 
2854  789 
end; 
790 

791 

792 
exception NEWBRANCHES and CLOSEF; 

793 

794 
exception PROVE; 

795 

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

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

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

798 
(eq_assume_tac ORELSE' assume_tac); 
2854  799 

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

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

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

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

814 

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

816 
fun hasSkolem (Skolem _) = true 

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

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

819 
 hasSkolem _ = false; 

820 

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

822 
Skolem terms then allow duplication.*) 

823 
fun joinMd md [] = [] 

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

825 

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

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

829 
 negOfGoal G = G; 

830 

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

832 

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

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

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

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

837 

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

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

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

840 
rotate_tac ~1 i; 
2894  841 

2854  842 

843 
(** Backtracking and Pruning **) 

844 

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

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

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

848 
 clashVar vars = 

849 
let fun clash (0, _) = false 

850 
 clash (_, []) = false 

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

852 
in clash end; 

853 

854 

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

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

857 
next branch have been updated.*) 

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

859 
backtracking over bad proofs*) 

860 
 prune (nbrs, nxtVars, choices) = 

861 
let fun traceIt last = 

862 
let val ll = length last 

863 
and lc = length choices 

864 
in if !trace andalso ll<lc then 

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

868 
end 

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

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

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

874 
else (* nbrs'=nbrs *) 

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

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

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

878 
choices) 

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

880 

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

881 
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

882 
 nextVars [] = []; 
2854  883 

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

886 
Int.toString nbrs ^ " branches")) 

887 
else (); 

888 
raise exn) 

889 
 backtrack _ = raise PROVE; 

2854  890 

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

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

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

896 
 bad _ = false; 

897 
fun change [] = [] 

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

899 
if G aconv G' then change lits 

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

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

902 
if G aconv G' then change lits 

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

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

905 
in 

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

907 
end 

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

909 

910 

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

3083  913 
fun log n = if n<4 then 0 else 1 + log(n div 4); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

914 

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

915 

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

916 
(*match(t,u) says whether the term u might be an instance of the pattern t 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

917 
Used to detect "recursive" rules such as transitivity*) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

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

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

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

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

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

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

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

927 
 match t u = false; 

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

928 

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

929 

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

932 
val nclosed = ref 0 

933 
and ntried = ref 1; 

934 

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

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

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

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

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

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

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

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

942 

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

943 

2854  944 
(*Tableau prover based on leanTaP. Argument is a list of branches. Each 
945 
branch contains a list of unexpanded formulae, a list of literals, and a 

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

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

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

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

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

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

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

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

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

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

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

963 
val nbrs = length brs0 

964 
val nxtVars = nextVars brs 

965 
val G = norm G 

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

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

970 
if (exists isGoal prem) 

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

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

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

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

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

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

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

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

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

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

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

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

984 
to branch.*) 

985 
fun deeper [] = raise NEWBRANCHES 

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

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

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

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

993 
val vars = vars_in_vars vars 

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

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

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

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

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

1003 
prune (nbrs, nxtVars, choices'), 

1004 
brs)) 

1005 
else (*prems nonnull*) 

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

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

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

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

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

1017 
(clearTo ntrl; deeper grls) 

1018 
else (*backtrack to previous level*) 

1019 
backtrack choices 

1020 
end 

1021 
else deeper grls 

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

1024 
 closeF (L::Ls) = 

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

1027 
 Some tac => 

1028 
let val choices' = 

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

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

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

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

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

1039 
(clearTo ntrl; closeF Ls) 

1040 
end 

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

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

1044 
closeF (map fst br) 

1045 
handle CLOSEF => closeF (map fst haz) 

1046 
handle CLOSEF => closeFl pairs 

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

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

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

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

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

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

1058 
handle CLOSEF => deeper rules 

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

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

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

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

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

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

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

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

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

1070 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1094 
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

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

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

1097 
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

1098 
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

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

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

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

1102 
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

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

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

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

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

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

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

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

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

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

1114 
to branch.*) 

1115 
fun deeper [] = raise NEWBRANCHES 

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

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

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

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

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

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

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

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

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

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

1132 
both dup and recur are false. Proofs are 

1133 
found at shallower depths, but looping 

1134 
occurs too often...*) 

3917  1135 
val mayUndo = 
1136 
(*Allowing backtracking from a rule application 

1137 
if other matching rules exist, if the rule 

1138 
updated variables, or if the rule did not 

1139 
introduce new variables. This latter condition 

1140 
means it is not a standard "gammarule" but 

1141 
some other form of unsafe rule. Aim is to 

1142 
emulate Fast_tac, which allows all unsafe steps 

1143 
to be undone.*) 

1144 
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

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

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

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

1149 
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

1150 
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

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

1152 

3083  1153 
in 
1154 
if lim'<0 andalso not (null prems) 

1155 
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

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

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

1160 
if !trace andalso dup then prs" (duplicating)" 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

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

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

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

1164 
traceVars sign ntrl; 
4300  1165 
if null prems then nclosed := !nclosed + 1 
1166 
else ntried := !ntried + length prems  1; 

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

1167 
prv(tac' :: tacs, 
3083  1168 
brs0::trs, 
1169 
(ntrl, length brs0, PRV) :: choices, 

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

1170 
newBr (vars', P, dup, lim') prems) 
3083  1171 
handle PRV => 
1172 
if mayUndo 

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

1174 
(clearTo ntrl; deeper grls) 

1175 
else (*backtrack to previous level*) 

1176 
backtrack choices 

1177 
end 

1178 
else deeper grls 

1179 
in tracing sign brs0; 

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

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

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

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

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

1188 
lim = lim} :: brs) 
2854  1189 
end 
1190 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1191 
in init_gensym(); 
1192 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1193 
end; 

2854  1194 

1195 

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

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

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

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

1201 
lim = lim}; 
2854  1202 

1203 

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

1205 

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

1207 
local open Term 

1208 
in 

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

1210 
 discard_foralls t = t; 

1211 
end; 

1212 

1213 

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

1215 
fun getVars [] i = [] 

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

1217 
if i mem is then getVars alist i 

1218 
else v :: getVars alist i; 

1219 

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

1220 
exception TRANS of string; 
2854  1221 

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

1222 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1223 
fun fromSubgoal t = 
1224 
let val alistVar = ref [] 

1225 
and alistTVar = ref [] 

2854  1226 
fun hdvar ((ix,(v,is))::_) = v 
1227 
fun from lev t = 

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

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

1230 
fun bounds [] = [] 

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

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

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

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

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

1236 
"Function unknown's argument not a bound variable" 
2854  1237 
in 
1238 
case ht of 

4065  1239 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1240 
 Term.Free (a,_) => apply (Free a) 
1241 
 Term.Bound i => apply (Bound i) 

1242 
 Term.Var (ix,_) => 

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

1245 
:: !alistVar; 

1246 
Var (hdvar(!alistVar))) 

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

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

1250 
^ Syntax.string_of_vname ix)) 
2854  1251 
 Term.Abs (a,_,body) => 
1252 
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

1253 
else raise TRANS "argument not in normal form" 
2854  1254 
end 
1255 

1256 
val npars = length (Logic.strip_params t) 

1257 

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

1259 
fun skoSubgoal i t = 

1260 
if i<npars then 

1261 
skoSubgoal (i+1) 

4065  1262 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1263 
t)) 
1264 
else t 

1265 

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

1267 

1268 

4300  1269 
fun initialize() = 
1270 
(fullTrace:=[]; trail := []; ntrail := 0; 

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

1272 

1273 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1299 
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

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

1301 
handle PROVE => Seq.empty); 
2854  1302 

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

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

1304 
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

1305 

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

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

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

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

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

4078  1311 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1312 

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

1313 

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

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

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

1316 

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

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

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

1320 
let val st = topthm() 
3030  1321 
val {sign,...} = rep_thm st 
4065  1322 
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

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

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

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

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

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

1328 
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

1329 

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

1331 

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

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

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

1335 

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

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

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

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

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

1343 

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

1344 

5926  1345 
(** method setup **) 
1346 

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

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

1349 
Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; 
7155  1350 

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

7155  1353 

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

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

1355 
"tableau prover")]]; 
5926  1356 

1357 

2854  1358 
end; 