author  paulson 
Wed, 03 Dec 1997 11:42:45 +0100  
changeset 4354  7f4da01bdf0e 
parent 4323  561242f8606b 
child 4391  cc3e8453d7f0 
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... 
2894  14 
* ignores addss, addbefore, addafter; this restriction is intrinsic 
15 
* ignores elimination rules that don't have the correct format 

16 
(conclusion must be a formula variable) 

17 
* ignores types, which can make HOL proofs fail 

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

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

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

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

22 
Known problems: 

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

24 
from expansion. This happens because newlycreated formulae always 
3092  25 
have priority over existing ones. But obviously recursive rules 
26 
such as transitivity are treated specially to prevent this. 

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

27 

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

29 
Overloading can't follow all chains of type dependencies. Cannot 
2952  30 
prove "In1 x ~: Part A In0" because PartE introducees the polymorphic 
31 
equality In1 x = In0 y, when the corresponding rule uses the (distinct) 

32 
set equality. Workaround: supply a type instance of the rule that 

33 
creates new equalities (e.g. PartE in HOL/ex/Simult) 

34 
==> affects freeness reasoning about Sexp constants (since they have 

35 
type ... set) 

36 

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

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

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

40 
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

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

44 

45 
(*Should be a type abbreviation?*) 

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

47 

48 

49 
(*Assumptions about constants: 

50 
The negation symbol is "Not" 

51 
The equality symbol is "op =" 

52 
The istrue judgement symbol is "Trueprop" 

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

54 
*) 

55 
signature BLAST_DATA = 

56 
sig 

57 
type claset 

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

59 
val ccontr : thm 

60 
val contr_tac : int > tactic 

61 
val dup_intr : thm > thm 

62 
val vars_gen_hyp_subst_tac : bool > int > tactic 

4078  63 
val claset : unit > claset 
2854  64 
val rep_claset : 
65 
claset > {safeIs: thm list, safeEs: thm list, 

66 
hazIs: thm list, hazEs: thm list, 

67 
uwrapper: (int > tactic) > (int > tactic), 

68 
swrapper: (int > tactic) > (int > tactic), 

69 
safe0_netpair: netpair, safep_netpair: netpair, 

70 
haz_netpair: netpair, dup_netpair: netpair} 

71 
end; 

72 

73 

74 
signature BLAST = 

75 
sig 

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

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

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

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

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

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

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

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

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

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

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

90 
val Blast_tac : int > tactic 

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

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

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

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

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

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

98 
val fromSubgoal : Term.term > term 

99 
val instVars : term > (unit > unit) 

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

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

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

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

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

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 normBr : branch > branch 
2854  109 
end; 
110 

111 

3092  112 
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854  113 
struct 
114 

115 
type claset = Data.claset; 

116 

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

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

118 
and stats = ref false; (*for runtime and search statistics*) 
2854  119 

120 
datatype term = 

121 
Const of string 

4065  122 
 TConst of string * term (*type of overloaded constantas a term!*) 
2854  123 
 Skolem of string * term option ref list 
124 
 Free of string 

125 
 Var of term option ref 

126 
 Bound of int 

127 
 Abs of string*term 

128 
 op $ of term*term; 

129 

130 

131 
(** Basic syntactic operations **) 

132 

133 
fun is_Var (Var _) = true 

134 
 is_Var _ = false; 

135 

136 
fun dest_Var (Var x) = x; 

137 

138 

139 
fun rand (f$x) = x; 

140 

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

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

143 

144 

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

146 
fun strip_comb u : term * term list = 

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

148 
 stripc x = x 

149 
in stripc(u,[]) end; 

150 

151 

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

153 
fun head_of (f$t) = head_of f 

154 
 head_of u = u; 

155 

156 

157 
(** Particular constants **) 

158 

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

160 

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

162 

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

164 
 isGoal _ = false; 

165 

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

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

168 

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

170 
 isTrueprop _ = false; 

171 

172 

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

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

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

178 
map (fromType alist) Ts) 

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

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

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

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

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

184 
end 

185 
 Some v => v) 

2854  186 

187 
local 

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

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

191 
fun overloaded arg = (overloads := arg :: (!overloads)); 
2854  192 

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

195 
fun fromConst alist (a,T) = 

196 
case assoc_string (!overloads, a) of 

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

198 
 Some f => 

199 
let val T' = f T 

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

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

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

2854  204 
end; 
205 

206 

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

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

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

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

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

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

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

218 
 _ aconv _ = false; 

219 

220 

221 
fun mem_term (_, []) = false 

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

223 

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

225 

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

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

228 

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

230 

231 

232 
(** Vars **) 

233 

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

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

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

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

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

241 
 add_term_vars (_, vars) = vars 

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

243 
and add_terms_vars ([], vars) = vars 

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

245 
(*Var list version.*) 

246 
and add_vars_vars ([], vars) = vars 

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

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

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

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

251 

252 

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

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

255 

256 

257 

258 
(*increment a term's nonlocal bound variables 

259 
inc is increment for bound variables 

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

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

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

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

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

265 

266 
fun incr_boundvars 0 t = t 

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

268 

269 

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

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

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

273 
else (ilev) ins_int js 

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

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

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

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

278 

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

280 

281 
fun subst_bound (arg, t) : term = 

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

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

284 
else if i=lev then incr_boundvars lev arg 

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

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

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

288 
 subst (t,lev) = t 

289 
in subst (t,0) end; 

290 

291 

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

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

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

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

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

300 
 nf => nf $ norm u) 
2854  301 
 _ => t; 
302 

303 

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

305 
fun wkNormAux t = case t of 

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

307 
Some u => wkNorm u 

308 
 None => t) 

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

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

311 
 nf => nf $ u) 

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

314 
nb as (f $ t) => 

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

316 
then Abs(a,nb) 

317 
else wkNorm (incr_boundvars ~1 f) 

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

321 
Const _ => t 

4065  322 
 TConst _ => t 
2854  323 
 Skolem(a,args) => t 
324 
 Free _ => t 

325 
 _ => wkNormAux t; 

326 

327 

328 
(*Does variable v occur in u? For unification.*) 

329 
fun varOccur v = 

330 
let fun occL [] = false (*same as (exists occ), but faster*) 

331 
 occL (u::us) = occ u orelse occL us 

332 
and occ (Var w) = 

333 
v=w orelse 

334 
(case !w of None => false 

335 
 Some u => occ u) 

336 
 occ (Skolem(_,args)) = occL (map Var args) 

4065  337 
 occ (TConst(_,u)) = occ u 
2854  338 
 occ (Abs(_,u)) = occ u 
339 
 occ (f$u) = occ u orelse occ f 

340 
 occ (_) = false; 

341 
in occ end; 

342 

343 
exception UNIFY; 

344 

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

346 
val ntrail = ref 0; 

347 

348 

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

350 
fun clearTo n = 

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

354 
ntrail := !ntrail  1); 

355 

356 

357 
(*Firstorder unification with bound variables. 

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

359 
on the trail (no point in doing so) 

360 
*) 

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

364 
if t aconv u then () 

365 
else if varOccur v u then raise UNIFY 

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

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

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

369 
then dest_Var u := Some t 

370 
else (v := Some u; 

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

372 
fun unifyAux (t,u) = 

373 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

385 

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

388 
fun fromTerm t = 

389 
let val alistVar = ref [] 

390 
and alistTVar = ref [] 

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

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

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

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

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

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

404 
else incr_boundvars ~1 f 

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

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

407 
in from t end; 

408 

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

411 
fun instVars t = 

412 
let val name = ref "A" 

413 
val updated = ref [] 

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

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

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

417 
name := bump_string (!name)) 

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

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

420 
 inst _ = () 

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

422 
in inst t; revert end; 

423 

424 

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

427 
A :: strip_imp_prems B 

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

429 
 strip_imp_prems _ = []; 

430 

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

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

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

434 
 strip_imp_concl A = A : term; 

435 

436 

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

438 

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

440 
fun squash_nots [] = [] 

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

442 
squash_nots Ps 

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

444 
squash_nots Ps 

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

446 

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

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

449 
 skoPrem vars P = P; 

450 

451 
fun convertPrem t = 

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

453 

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

455 
fun convertRule vars t = 

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

457 
val Var v = strip_imp_concl t 

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

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

460 
end; 

461 

462 

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

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

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

466 

467 
(*Count new hyps so that they can be rotated*) 

468 
fun nNewHyps [] = 0 

469 
 nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps 

470 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 

471 

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

472 
fun rot_subgoals_tac [] i st = Seq.single st 
2854  473 
 rot_subgoals_tac (k::ks) i st = 
4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

474 
rot_subgoals_tac ks (i+1) (Seq.hd (rotate_tac (~k) i st)) 
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

475 
handle OPTION => Seq.empty; 
2854  476 

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

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

479 
(*Tableau rule from elimination rule. Flag "dup" requests duplication of the 

480 
affected formula.*) 

481 
fun fromRule vars rl = 

4065  482 
let val trl = rl > rep_thm > #prop > fromTerm > convertRule vars 
2854  483 
fun tac dup i = 
2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

484 
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i 
2854  485 
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i 
486 

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

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

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

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

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

492 
Option.NONE); 
2854  493 

494 

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

495 
(*** Conversion of Introduction Rules ***) 
2854  496 

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

498 

499 
fun convertIntrRule vars t = 

500 
let val Ps = strip_imp_prems t 

501 
val P = strip_imp_concl t 

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

503 
end; 

504 

505 
(*Tableau rule from introduction rule. Since haz rules are now delayed, 

506 
"dup" is always FALSE for introduction rules.*) 

507 
fun fromIntrRule vars rl = 

4065  508 
let val trl = rl > rep_thm > #prop > fromTerm > convertIntrRule vars 
2854  509 
fun tac dup i = 
2999
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

510 
TRACE rl (DETERM o (rtac (if dup then Data.dup_intr rl else rl))) i 
2854  511 
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i 
512 
in (trl, tac) end; 

513 

514 

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

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

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

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

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

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

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

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

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

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

527 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  528 

529 

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

531 
case P of 

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

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

533 
let val pG = mk_tprop (toTerm 2 G) 
2854  534 
val intrs = List.concat 
535 
(map (fn (inet,_) => Net.unify_term inet pG) 

536 
nps) 

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

538 
 _ => 

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

539 
let val pP = mk_tprop (toTerm 3 P) 
2854  540 
val elims = List.concat 
541 
(map (fn (_,enet) => Net.unify_term enet pP) 

542 
nps) 

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

544 

545 
(** 

546 
end; 

547 
**) 

548 

3092  549 

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

551 
type branch = ((term*bool) list * (*safe formulae on this level*) 

552 
(term*bool) list) list * (*haz formulae on this level*) 

553 
term list * (*literals: irreducible formulae*) 

554 
term option ref list * (*variables occurring in branch*) 

555 
int; (*resource limit*) 

556 

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

558 

559 
(*Normalize a branchfor tracing*) 

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

561 

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

563 

564 
fun normBr (br, lits, vars, lim) = 

565 
(map normLev br, map norm lits, vars, lim); 

566 

567 

4065  568 
val dummyTVar = Term.TVar(("a",0), []); 
3092  569 
val dummyVar2 = Term.Var(("var",0), dummyT); 
570 

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

573 
 showType (Var _) = dummyTVar 

574 
 showType t = 

575 
(case strip_comb t of 

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

577 
 _ => dummyT); 

578 

579 
(*Display toplevel overloading if any*) 

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

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

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

583 
None => topType u 

584 
 some => some) 

585 
 topType _ = None; 

586 

587 

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

4065  590 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  591 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
592 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

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

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

595 
 showTerm d (Var(ref None)) = dummyVar2 
3092  596 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
597 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

600 

4065  601 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  602 

4065  603 
fun traceTerm sign t = 
604 
let val t' = norm t 

605 
val stm = string_of sign 8 t' 

606 
in 

607 
case topType t' of 

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

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

610 
end; 

3092  611 

612 

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

614 
fun tracing sign brs = 

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

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

617 
 printPairs _ = () 

618 
fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = 

619 
(fullTrace := brs0 :: !fullTrace; 

620 
seq (fn _ => prs "+") brs; 

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

622 
printPairs pairs; 

623 
writeln"") 

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

625 
end; 

626 

4065  627 
fun traceMsg s = if !trace then prs s else (); 
628 

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

632 
(case !ntrailntrl of 

633 
0 => () 

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

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

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

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

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

639 
writeln"") 

3092  640 
else (); 
641 

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

643 
fun traceNew prems = 

644 
if !trace then 

645 
case length prems of 

646 
0 => prs"branch closed by rule" 

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

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

649 
else (); 

650 

651 

652 

2854  653 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
654 

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

656 
fun subst_atomic (old,new) t = 

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

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

659 
 subst (f$t) = subst f $ subst t 

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

661 
in subst t end; 

662 

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

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

665 
(case eta_contract2 body of 

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

667 
else eta_contract_atom (incr_boundvars ~1 f) 

668 
 _ => t0) 

669 
 eta_contract_atom t = t 

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

671 
 eta_contract2 t = eta_contract_atom t; 

672 

673 

674 
(*When can we safely delete the equality? 

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

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

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

678 
Prefer to eliminate Bound variables if possible. 

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

680 

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

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

682 
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

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

685 
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

686 
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

687 
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

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

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

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

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

692 
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

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

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

695 
 occ (Abs(_,u)) = occEq u 
2854  696 
 occ (f$u) = occEq u orelse occEq f 
697 
 occ (_) = false; 

698 
in occEq end; 

699 

3092  700 
exception DEST_EQ; 
701 

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

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

704 
(eta_contract_atom t, eta_contract_atom u) 

4065  705 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  706 
(eta_contract_atom t, eta_contract_atom u) 
707 
 dest_eq _ = raise DEST_EQ; 

708 

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

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

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

713 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  714 
fun orientGoal (t,u) = case (t,u) of 
2854  715 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
716 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

719 
 _ => raise DEST_EQ; 

720 

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

723 
they should go: this could make proofs fail. ??? *) 

3092  724 
fun equalSubst sign (G, pairs, lits, vars, lim) = 
725 
let val (t,u) = orientGoal(dest_eq G) 

726 
val subst = subst_atomic (t,u) 

2854  727 
fun subst2(G,md) = (subst G, md) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

728 
(*substitute throughout Haz list; move affected ones to Safe part*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

729 
fun subHazs ([], Gs, nHs) = (Gs,nHs) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

730 
 subHazs ((H,md)::Hs, Gs, nHs) = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

731 
let val nH = subst H 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

732 
in if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

733 
else subHazs (Hs, (nH,md)::Gs, nHs) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

735 
val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

736 
(*substitute throughout literals; move affected ones to Safe part*) 
2894  737 
fun subLits ([], [], nlits) = (pairs', nlits, vars, lim) 
738 
 subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim) 

739 
 subLits (lit::lits, Gs, nlits) = 

2854  740 
let val nlit = subst lit 
2894  741 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
742 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  743 
end 
3092  744 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
745 
" for " ^ traceTerm sign t ^ " in branch" ) 

746 
else (); 

3083  747 
subLits (rev lits, [], []) 
2854  748 
end; 
749 

750 

751 
exception NEWBRANCHES and CLOSEF; 

752 

753 
exception PROVE; 

754 

755 
val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac; 

756 

757 
val eContr_tac = TRACE Data.notE (eq_contr_tac ORELSE' Data.contr_tac); 

758 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 

759 

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

3083  761 
fun tryClose (Const"*Goal*" $ G, L) = 
4065  762 
if unify([],G,L) then Some eAssume_tac else None 
3083  763 
 tryClose (G, Const"*Goal*" $ L) = 
4065  764 
if unify([],G,L) then Some eAssume_tac else None 
3083  765 
 tryClose (Const"Not" $ G, L) = 
4065  766 
if unify([],G,L) then Some eContr_tac else None 
3083  767 
 tryClose (G, Const"Not" $ L) = 
4065  768 
if unify([],G,L) then Some eContr_tac else None 
3083  769 
 tryClose _ = None; 
2854  770 

771 

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

773 
fun hasSkolem (Skolem _) = true 

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

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

776 
 hasSkolem _ = false; 

777 

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

779 
Skolem terms then allow duplication.*) 

780 
fun joinMd md [] = [] 

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

782 

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

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

786 
 negOfGoal G = G; 

787 

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

789 

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

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

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

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

794 

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

796 
val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1; 

797 

2854  798 

799 
(** Backtracking and Pruning **) 

800 

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

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

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

804 
 clashVar vars = 

805 
let fun clash (0, _) = false 

806 
 clash (_, []) = false 

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

808 
in clash end; 

809 

810 

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

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

813 
next branch have been updated.*) 

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

815 
backtracking over bad proofs*) 

816 
 prune (nbrs, nxtVars, choices) = 

817 
let fun traceIt last = 

818 
let val ll = length last 

819 
and lc = length choices 

820 
in if !trace andalso ll<lc then 

3083  821 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  822 
last) 
823 
else last 

824 
end 

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

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

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

830 
else (* nbrs'=nbrs *) 

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

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

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

834 
choices) 

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

836 

2894  837 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  838 
 nextVars [] = []; 
2854  839 

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

842 
Int.toString nbrs ^ " branches")) 

843 
else (); 

844 
raise exn) 

845 
 backtrack _ = raise PROVE; 

2854  846 

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

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

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

852 
 bad _ = false; 

853 
fun change [] = [] 

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

855 
if G aconv G' then change lits 

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

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

858 
if G aconv G' then change lits 

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

860 
 change (lit::lits) = lit :: change lits 

861 
in 

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

863 
end 

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

865 

866 

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

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

870 

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

871 

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

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

873 
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

874 
fun match (Var _) u = true 
4065  875 
 match (Const"*Goal*") (Const"Not") = true 
876 
 match (Const"Not") (Const"*Goal*") = true 

877 
 match (Const a) (Const b) = (a=b) 

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

879 
 match (Free a) (Free b) = (a=b) 

880 
 match (Bound i) (Bound j) = (i=j) 

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

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

883 
 match t u = false; 

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

884 

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

885 

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

888 
val nclosed = ref 0 

889 
and ntried = ref 1; 

890 

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

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

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

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

894 
^ Int.toString (!nclosed) ^ 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

895 
" tried: " ^ Int.toString (!ntried)) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

897 

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

898 

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

901 
bound on unsafe expansions.*) 

3030  902 
fun prove (sign, cs, brs, cont) = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

904 
val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs 
2854  905 
val safeList = [safe0_netpair, safep_netpair] 
906 
and hazList = [haz_netpair] 

4065  907 
fun prv (tacs, trs, choices, []) = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

909 
cont (tacs, trs, choices)) (*all branches closed!*) 
2854  910 
 prv (tacs, trs, choices, 
2894  911 
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = 
3917  912 
(*apply a safe rule only (possibly allowing instantiation); 
913 
defer any haz formulae*) 

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

916 
val nbrs = length brs0 

917 
val nxtVars = nextVars brs 

918 
val G = norm G 

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

919 
val rules = netMkRules G vars safeList 
2854  920 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  921 
fun newBr (vars',lim') prems = 
922 
map (fn prem => 

923 
if (exists isGoal prem) 

924 
then (((joinMd md prem, []) :: 

925 
negOfGoals ((br, haz)::pairs)), 

926 
map negOfGoal lits, 

927 
vars', lim') 

928 
else (((joinMd md prem, []) :: (br, haz) :: pairs), 

929 
lits, vars', lim')) 

2854  930 
prems @ 
931 
brs 

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

933 
to branch.*) 

934 
fun deeper [] = raise NEWBRANCHES 

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

4065  936 
if unify(add_term_vars(P,[]), P, G) 
3083  937 
then (*P comes from the rule; G comes from the branch.*) 
938 
let val ntrl' = !ntrail 

939 
val lim' = if ntrl < !ntrail 

940 
then lim  (1+log(length rules)) 

941 
else lim (*discourage branching updates*) 

942 
val vars = vars_in_vars vars 

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

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

945 
val tacs' = (DETERM o (tac false)) :: tacs 

946 
(*no duplication*) 

947 
in 

4065  948 
traceNew prems; traceVars sign ntrl; 
3083  949 
(if null prems then (*closed the branch: prune!*) 
4300  950 
(nclosed := !nclosed + 1; 
951 
prv(tacs', brs0::trs, 

952 
prune (nbrs, nxtVars, choices'), 

953 
brs)) 

954 
else (*prems nonnull*) 

3083  955 
if lim'<0 (*faster to kill ALL the alternatives*) 
4065  956 
then (traceMsg"Excessive branching: KILLED\n"; 
957 
clearTo ntrl; raise NEWBRANCHES) 

3083  958 
else 
4300  959 
(ntried := !ntried + length prems  1; 
960 
prv(tacs', brs0::trs, choices', 

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

3083  962 
handle PRV => 
963 
if ntrl < ntrl' (*Vars have been updated*) 

4065  964 
then 
3083  965 
(*Backtrack at this level. 
966 
Reset Vars and try another rule*) 

967 
(clearTo ntrl; deeper grls) 

968 
else (*backtrack to previous level*) 

969 
backtrack choices 

970 
end 

971 
else deeper grls 

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

974 
 closeF (L::Ls) = 

3083  975 
case tryClose(G,L) of 
976 
None => closeF Ls 

977 
 Some tac => 

978 
let val choices' = 

3092  979 
(if !trace then (prs"branch closed"; 
4065  980 
traceVars sign ntrl) 
3083  981 
else (); 
982 
prune (nbrs, nxtVars, 

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

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

3083  986 
handle PRV => 
987 
(*reset Vars and try another literal 

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

989 
(clearTo ntrl; closeF Ls) 

990 
end 

2894  991 
fun closeFl [] = raise CLOSEF 
992 
 closeFl ((br, haz)::pairs) = 

993 
closeF (map fst br) 

994 
handle CLOSEF => closeF (map fst haz) 

995 
handle CLOSEF => closeFl pairs 

3083  996 
in tracing sign brs0; 
4065  997 
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) 
2854  998 
else 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

999 
prv (Data.vars_gen_hyp_subst_tac false :: tacs, 
2854  1000 
brs0::trs, choices, 
3092  1001 
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
4065  1002 
handle DEST_EQ => closeF lits 
1003 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1004 
handle CLOSEF => deeper rules 

2894  1005 
handle NEWBRANCHES => 
1006 
(case netMkRules G vars hazList of 

3917  1007 
[] => (*no plausible haz rules: move G to literals*) 
2894  1008 
prv (tacs, brs0::trs, choices, 
1009 
((br,haz)::pairs, addLit(G,lits), vars, lim) 

1010 
::brs) 

1011 
 _ => (*G admits some haz rules: try later*) 

1012 
prv (if isGoal G then negOfGoal_tac :: tacs 

1013 
else tacs, 

1014 
brs0::trs, choices, 

1015 
((br, haz@[(negOfGoal G, md)])::pairs, 

1016 
lits, vars, lim) :: brs)) 

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

1018 
 prv (tacs, trs, choices, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

1021 
prv (tacs, trs, choices, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1022 
((Gs,haz@haz')::pairs, lits, vars, lim) :: brs) 
2854  1023 
 prv (tacs, trs, choices, 
2894  1024 
brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) = 
1025 
(*no safe steps possible at any level: apply a haz rule*) 

2854  1026 
let exception PRV (*backtrack to precisely this recursion!*) 
2894  1027 
val H = norm H 
2854  1028 
val ntrl = !ntrail 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1029 
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

1030 
(*new premises of haz rules may NOT be duplicated*) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

1031 
fun newPrem (vars,recur,dup,lim') prem = 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

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

1033 
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

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

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

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

1037 
in (if recur (*send new haz premises to the BACK of the 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1038 
queue to prevent exclusion of others*) 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1039 
then [(Gs',Hs')] 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1040 
else [(Gs',[]), ([],Hs')], 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

1041 
lits', vars, lim') 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

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

1045 
to branch.*) 

1046 
fun deeper [] = raise NEWBRANCHES 

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

4065  1048 
if unify(add_term_vars(P,[]), P, H) 
3083  1049 
then 
1050 
let val ntrl' = !ntrail 

1051 
val vars = vars_in_vars vars 

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

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

1054 
val dup = md andalso vars' <> vars 

1055 
(*any instances of P in the subgoals?*) 

1056 
and recur = exists (exists (match P)) prems 

1057 
val lim' = (*Decrement "lim" extra if updates occur*) 

1058 
if ntrl < !ntrail then lim  (1+log(length rules)) 

1059 
else lim1 

1060 
(*It is tempting to leave "lim" UNCHANGED if 

1061 
both dup and recur are false. Proofs are 

1062 
found at shallower depths, but looping 

1063 
occurs too often...*) 

3917  1064 
val mayUndo = 
1065 
(*Allowing backtracking from a rule application 

1066 
if other matching rules exist, if the rule 

1067 
updated variables, or if the rule did not 

1068 
introduce new variables. This latter condition 

1069 
means it is not a standard "gammarule" but 

1070 
some other form of unsafe rule. Aim is to 

1071 
emulate Fast_tac, which allows all unsafe steps 

1072 
to be undone.*) 

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

1074 
orelse ntrl < ntrl' (*variables updated?*) 

1075 
orelse vars=vars' (*no new Vars?*) 

3083  1076 
val tac' = if mayUndo then tac dup 
1077 
else DETERM o (tac dup) 

1078 
in 

1079 
if lim'<0 andalso not (null prems) 

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

4065  1081 
(traceMsg"Excessive branching: KILLED\n"; 
1082 
clearTo ntrl; raise NEWBRANCHES) 

3083  1083 
else 
4065  1084 
traceNew prems; traceVars sign ntrl; 
4300  1085 
if null prems then nclosed := !nclosed + 1 
1086 
else ntried := !ntried + length prems  1; 

3083  1087 
prv(tac dup :: tacs, 
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

1088 
(*FIXME: if recur then the tactic should not 
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

1089 
call rotate_tac: new formulae should be last*) 
3083  1090 
brs0::trs, 
1091 
(ntrl, length brs0, PRV) :: choices, 

1092 
newBr (vars', recur, dup, lim') prems) 

1093 
handle PRV => 

1094 
if mayUndo 

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

1096 
(clearTo ntrl; deeper grls) 

1097 
else (*backtrack to previous level*) 

1098 
backtrack choices 

1099 
end 

1100 
else deeper grls 

1101 
in tracing sign brs0; 

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

1103 
else deeper rules 
2854  1104 
handle NEWBRANCHES => 
2894  1105 
(*cannot close branch: move H to literals*) 
2854  1106 
prv (tacs, brs0::trs, choices, 
2894  1107 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1108 
end 
1109 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1110 
in init_gensym(); 
1111 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1112 
end; 

2854  1113 

1114 

2883  1115 
(*Construct an initial branch.*) 
2854  1116 
fun initBranch (ts,lim) = 
2894  1117 
([(map (fn t => (t,true)) ts, [])], 
1118 
[], add_terms_vars (ts,[]), lim); 

2854  1119 

1120 

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

1122 

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

1124 
local open Term 

1125 
in 

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

1127 
 discard_foralls t = t; 

1128 
end; 

1129 

1130 

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

1132 
fun getVars [] i = [] 

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

1134 
if i mem is then getVars alist i 

1135 
else v :: getVars alist i; 

1136 

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

1137 
exception TRANS of string; 
2854  1138 

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

1139 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1140 
fun fromSubgoal t = 
1141 
let val alistVar = ref [] 

1142 
and alistTVar = ref [] 

2854  1143 
fun hdvar ((ix,(v,is))::_) = v 
1144 
fun from lev t = 

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

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

1147 
fun bounds [] = [] 

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

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

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

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

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

1153 
"Function unknown's argument not a bound variable" 
2854  1154 
in 
1155 
case ht of 

4065  1156 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1157 
 Term.Free (a,_) => apply (Free a) 
1158 
 Term.Bound i => apply (Bound i) 

1159 
 Term.Var (ix,_) => 

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

1162 
:: !alistVar; 

1163 
Var (hdvar(!alistVar))) 

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

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

1166 
("Discrepancy among occurrences of ?" 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1167 
^ Syntax.string_of_vname ix)) 
2854  1168 
 Term.Abs (a,_,body) => 
1169 
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

1170 
else raise TRANS "argument not in normal form" 
2854  1171 
end 
1172 

1173 
val npars = length (Logic.strip_params t) 

1174 

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

1176 
fun skoSubgoal i t = 

1177 
if i<npars then 

1178 
skoSubgoal (i+1) 

4065  1179 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1180 
t)) 
1181 
else t 

1182 

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

1184 

1185 

4300  1186 
fun initialize() = 
1187 
(fullTrace:=[]; trail := []; ntrail := 0; 

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

1189 

1190 

2854  1191 
(*Tactic using tableau engine and proof reconstruction. 
1192 
"lim" is depth limit.*) 

1193 
fun depth_tac cs lim i st = 

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

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

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

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

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

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

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

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

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

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

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

1204 
Int.toString lim); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

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

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

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

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

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

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

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

1213 
handle PROVE => Seq.empty); 
2854  1214 

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

1215 
fun blast_tac cs i st = (DEEPEN (1,20) (depth_tac cs) 0) i st 
4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

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

4078  1218 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1219 

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

1220 

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

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

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

1223 

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

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

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

1227 
let val st = topthm() 
3030  1228 
val {sign,...} = rep_thm st 
4065  1229 
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

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

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

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

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

1234 
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

1235 

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

1237 

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

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

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

1241 

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

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

1244 
timeap prove (sign_of thy, 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

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

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

1248 

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

1249 

2854  1250 
end; 
1251 