author  paulson 
Wed, 26 Nov 1997 16:49:54 +0100  
changeset 4300  451ae21dca28 
parent 4271  3a82492e70c5 
child 4323  561242f8606b 
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*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

97 
val fromSubgoal : Term.term > term 

98 
val instVars : term > (unit > unit) 

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

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

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

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

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

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

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

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

110 

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

114 
type claset = Data.claset; 

115 

116 
val trace = ref false; 

117 

118 
datatype term = 

119 
Const of string 

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

123 
 Var of term option ref 

124 
 Bound of int 

125 
 Abs of string*term 

126 
 op $ of term*term; 

127 

128 

129 
(** Basic syntactic operations **) 

130 

131 
fun is_Var (Var _) = true 

132 
 is_Var _ = false; 

133 

134 
fun dest_Var (Var x) = x; 

135 

136 

137 
fun rand (f$x) = x; 

138 

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

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

141 

142 

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

144 
fun strip_comb u : term * term list = 

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

146 
 stripc x = x 

147 
in stripc(u,[]) end; 

148 

149 

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

151 
fun head_of (f$t) = head_of f 

152 
 head_of u = u; 

153 

154 

155 
(** Particular constants **) 

156 

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

158 

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

160 

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

162 
 isGoal _ = false; 

163 

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

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

166 

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

168 
 isTrueprop _ = false; 

169 

170 

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

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

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

176 
map (fromType alist) Ts) 

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

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

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

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

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

182 
end 

183 
 Some v => v) 

2854  184 

185 
local 

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

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

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

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

193 
fun fromConst alist (a,T) = 

194 
case assoc_string (!overloads, a) of 

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

196 
 Some f => 

197 
let val T' = f T 

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

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

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

2854  202 
end; 
203 

204 

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

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

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

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

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

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

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

216 
 _ aconv _ = false; 

217 

218 

219 
fun mem_term (_, []) = false 

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

221 

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

223 

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

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

226 

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

228 

229 

230 
(** Vars **) 

231 

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

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

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

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

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

239 
 add_term_vars (_, vars) = vars 

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

241 
and add_terms_vars ([], vars) = vars 

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

243 
(*Var list version.*) 

244 
and add_vars_vars ([], vars) = vars 

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

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

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

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

249 

250 

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

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

253 

254 

255 

256 
(*increment a term's nonlocal bound variables 

257 
inc is increment for bound variables 

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

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

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

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

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

263 

264 
fun incr_boundvars 0 t = t 

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

266 

267 

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

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

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

271 
else (ilev) ins_int js 

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

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

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

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

276 

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

278 

279 
fun subst_bound (arg, t) : term = 

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

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

282 
else if i=lev then incr_boundvars lev arg 

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

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

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

286 
 subst (t,lev) = t 

287 
in subst (t,0) end; 

288 

289 

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

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

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

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

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

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

301 

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

303 
fun wkNormAux t = case t of 

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

305 
Some u => wkNorm u 

306 
 None => t) 

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

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

309 
 nf => nf $ u) 

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

312 
nb as (f $ t) => 

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

314 
then Abs(a,nb) 

315 
else wkNorm (incr_boundvars ~1 f) 

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

319 
Const _ => t 

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

323 
 _ => wkNormAux t; 

324 

325 

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

327 
fun varOccur v = 

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

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

330 
and occ (Var w) = 

331 
v=w orelse 

332 
(case !w of None => false 

333 
 Some u => occ u) 

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

4065  335 
 occ (TConst(_,u)) = occ u 
2854  336 
 occ (Abs(_,u)) = occ u 
337 
 occ (f$u) = occ u orelse occ f 

338 
 occ (_) = false; 

339 
in occ end; 

340 

341 
exception UNIFY; 

342 

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

344 
val ntrail = ref 0; 

345 

346 

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

348 
fun clearTo n = 

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

352 
ntrail := !ntrail  1); 

353 

354 

355 
(*Firstorder unification with bound variables. 

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

357 
on the trail (no point in doing so) 

358 
*) 

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

362 
if t aconv u then () 

363 
else if varOccur v u then raise UNIFY 

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

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

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

367 
then dest_Var u := Some t 

368 
else (v := Some u; 

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

370 
fun unifyAux (t,u) = 

371 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

383 

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

386 
fun fromTerm t = 

387 
let val alistVar = ref [] 

388 
and alistTVar = ref [] 

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

2854  390 
 from (Term.Free (a,_)) = Free a 
391 
 from (Term.Bound i) = Bound i 

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

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

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

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

402 
else incr_boundvars ~1 f 

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

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

405 
in from t end; 

406 

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

409 
fun instVars t = 

410 
let val name = ref "A" 

411 
val updated = ref [] 

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

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

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

415 
name := bump_string (!name)) 

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

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

418 
 inst _ = () 

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

420 
in inst t; revert end; 

421 

422 

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

425 
A :: strip_imp_prems B 

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

427 
 strip_imp_prems _ = []; 

428 

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

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

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

432 
 strip_imp_concl A = A : term; 

433 

434 

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

436 

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

438 
fun squash_nots [] = [] 

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

440 
squash_nots Ps 

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

442 
squash_nots Ps 

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

444 

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

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

447 
 skoPrem vars P = P; 

448 

449 
fun convertPrem t = 

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

451 

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

453 
fun convertRule vars t = 

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

455 
val Var v = strip_imp_concl t 

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

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

458 
end; 

459 

460 

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

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

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

464 

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

466 
fun nNewHyps [] = 0 

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

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

469 

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

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

472 
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

473 
handle OPTION => Seq.empty; 
2854  474 

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

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

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

478 
affected formula.*) 

479 
fun fromRule vars rl = 

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

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

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

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

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

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

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

490 
Option.NONE); 
2854  491 

492 

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

493 
(*** Conversion of Introduction Rules ***) 
2854  494 

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

496 

497 
fun convertIntrRule vars t = 

498 
let val Ps = strip_imp_prems t 

499 
val P = strip_imp_concl t 

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

501 
end; 

502 

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

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

505 
fun fromIntrRule vars rl = 

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

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

511 

512 

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

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

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

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

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

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

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

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

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

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

525 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  526 

527 

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

529 
case P of 

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

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

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

534 
nps) 

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

536 
 _ => 

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

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

540 
nps) 

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

542 

543 
(** 

544 
end; 

545 
**) 

546 

3092  547 

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

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

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

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

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

553 
int; (*resource limit*) 

554 

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

556 

557 
(*Normalize a branchfor tracing*) 

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

559 

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

561 

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

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

564 

565 

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

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

571 
 showType (Var _) = dummyTVar 

572 
 showType t = 

573 
(case strip_comb t of 

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

575 
 _ => dummyT); 

576 

577 
(*Display toplevel overloading if any*) 

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

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

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

581 
None => topType u 

582 
 some => some) 

583 
 topType _ = None; 

584 

585 

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

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

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

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

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

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

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

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

598 

4065  599 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  600 

4065  601 
fun traceTerm sign t = 
602 
let val t' = norm t 

603 
val stm = string_of sign 8 t' 

604 
in 

605 
case topType t' of 

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

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

608 
end; 

3092  609 

610 

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

612 
fun tracing sign brs = 

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

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

615 
 printPairs _ = () 

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

617 
(fullTrace := brs0 :: !fullTrace; 

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

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

620 
printPairs pairs; 

621 
writeln"") 

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

623 
end; 

624 

4065  625 
fun traceMsg s = if !trace then prs s else (); 
626 

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

630 
(case !ntrailntrl of 

631 
0 => () 

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

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

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

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

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

637 
writeln"") 

3092  638 
else (); 
639 

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

641 
fun traceNew prems = 

642 
if !trace then 

643 
case length prems of 

644 
0 => prs"branch closed by rule" 

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

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

647 
else (); 

648 

649 

650 

2854  651 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
652 

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

654 
fun subst_atomic (old,new) t = 

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

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

657 
 subst (f$t) = subst f $ subst t 

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

659 
in subst t end; 

660 

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

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

663 
(case eta_contract2 body of 

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

665 
else eta_contract_atom (incr_boundvars ~1 f) 

666 
 _ => t0) 

667 
 eta_contract_atom t = t 

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

669 
 eta_contract2 t = eta_contract_atom t; 

670 

671 

672 
(*When can we safely delete the equality? 

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

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

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

676 
Prefer to eliminate Bound variables if possible. 

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

678 

679 
(*Does t occur in u? For substitution. 

680 
Does NOT check 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

681 
REFLEXIVE because hyp_subst_tac fails on x=x.*) 
2854  682 
fun substOccur t = 
683 
let fun occEq u = (t aconv u) orelse occ u 

684 
and occ (Var(ref None)) = false 

685 
 occ (Var(ref(Some u))) = occEq u 

686 
 occ (Abs(_,u)) = occEq u 

687 
 occ (f$u) = occEq u orelse occEq f 

688 
 occ (_) = false; 

689 
in occEq end; 

690 

3092  691 
exception DEST_EQ; 
692 

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

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

695 
(eta_contract_atom t, eta_contract_atom u) 

4065  696 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  697 
(eta_contract_atom t, eta_contract_atom u) 
698 
 dest_eq _ = raise DEST_EQ; 

699 

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

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

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

704 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  705 
fun orientGoal (t,u) = case (t,u) of 
2854  706 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
707 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

710 
 _ => raise DEST_EQ; 

711 

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

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

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

717 
val subst = subst_atomic (t,u) 

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

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

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

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

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

723 
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

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

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

726 
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

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

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

2854  731 
let val nlit = subst lit 
2894  732 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
733 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  734 
end 
3092  735 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
736 
" for " ^ traceTerm sign t ^ " in branch" ) 

737 
else (); 

3083  738 
subLits (rev lits, [], []) 
2854  739 
end; 
740 

741 

742 
exception NEWBRANCHES and CLOSEF; 

743 

744 
exception PROVE; 

745 

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

747 

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

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

750 

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

3083  752 
fun tryClose (Const"*Goal*" $ G, L) = 
4065  753 
if unify([],G,L) then Some eAssume_tac else None 
3083  754 
 tryClose (G, Const"*Goal*" $ L) = 
4065  755 
if unify([],G,L) then Some eAssume_tac else None 
3083  756 
 tryClose (Const"Not" $ G, L) = 
4065  757 
if unify([],G,L) then Some eContr_tac else None 
3083  758 
 tryClose (G, Const"Not" $ L) = 
4065  759 
if unify([],G,L) then Some eContr_tac else None 
3083  760 
 tryClose _ = None; 
2854  761 

762 

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

764 
fun hasSkolem (Skolem _) = true 

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

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

767 
 hasSkolem _ = false; 

768 

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

770 
Skolem terms then allow duplication.*) 

771 
fun joinMd md [] = [] 

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

773 

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

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

777 
 negOfGoal G = G; 

778 

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

780 

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

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

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

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

785 

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

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

788 

2854  789 

790 
(** Backtracking and Pruning **) 

791 

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

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

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

795 
 clashVar vars = 

796 
let fun clash (0, _) = false 

797 
 clash (_, []) = false 

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

799 
in clash end; 

800 

801 

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

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

804 
next branch have been updated.*) 

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

806 
backtracking over bad proofs*) 

807 
 prune (nbrs, nxtVars, choices) = 

808 
let fun traceIt last = 

809 
let val ll = length last 

810 
and lc = length choices 

811 
in if !trace andalso ll<lc then 

3083  812 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  813 
last) 
814 
else last 

815 
end 

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

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

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

821 
else (* nbrs'=nbrs *) 

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

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

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

825 
choices) 

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

827 

2894  828 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  829 
 nextVars [] = []; 
2854  830 

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

833 
Int.toString nbrs ^ " branches")) 

834 
else (); 

835 
raise exn) 

836 
 backtrack _ = raise PROVE; 

2854  837 

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

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

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

843 
 bad _ = false; 

844 
fun change [] = [] 

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

846 
if G aconv G' then change lits 

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

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

849 
if G aconv G' then change lits 

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

851 
 change (lit::lits) = lit :: change lits 

852 
in 

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

854 
end 

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

856 

857 

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

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

861 

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

862 

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

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

864 
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

865 
fun match (Var _) u = true 
4065  866 
 match (Const"*Goal*") (Const"Not") = true 
867 
 match (Const"Not") (Const"*Goal*") = true 

868 
 match (Const a) (Const b) = (a=b) 

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

870 
 match (Free a) (Free b) = (a=b) 

871 
 match (Bound i) (Bound j) = (i=j) 

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

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

874 
 match t u = false; 

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

875 

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

876 

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

879 
val nclosed = ref 0 

880 
and ntried = ref 1; 

881 

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

884 
bound on unsafe expansions.*) 

3030  885 
fun prove (sign, cs, brs, cont) = 
2854  886 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs 
887 
val safeList = [safe0_netpair, safep_netpair] 

888 
and hazList = [haz_netpair] 

4065  889 
fun prv (tacs, trs, choices, []) = 
890 
cont (tacs, trs, choices) (*all branches closed!*) 

2854  891 
 prv (tacs, trs, choices, 
2894  892 
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = 
3917  893 
(*apply a safe rule only (possibly allowing instantiation); 
894 
defer any haz formulae*) 

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

897 
val nbrs = length brs0 

898 
val nxtVars = nextVars brs 

899 
val G = norm G 

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

900 
val rules = netMkRules G vars safeList 
2854  901 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  902 
fun newBr (vars',lim') prems = 
903 
map (fn prem => 

904 
if (exists isGoal prem) 

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

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

907 
map negOfGoal lits, 

908 
vars', lim') 

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

910 
lits, vars', lim')) 

2854  911 
prems @ 
912 
brs 

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

914 
to branch.*) 

915 
fun deeper [] = raise NEWBRANCHES 

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

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

920 
val lim' = if ntrl < !ntrail 

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

922 
else lim (*discourage branching updates*) 

923 
val vars = vars_in_vars vars 

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

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

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

927 
(*no duplication*) 

928 
in 

4065  929 
traceNew prems; traceVars sign ntrl; 
3083  930 
(if null prems then (*closed the branch: prune!*) 
4300  931 
(nclosed := !nclosed + 1; 
932 
prv(tacs', brs0::trs, 

933 
prune (nbrs, nxtVars, choices'), 

934 
brs)) 

935 
else (*prems nonnull*) 

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

3083  939 
else 
4300  940 
(ntried := !ntried + length prems  1; 
941 
prv(tacs', brs0::trs, choices', 

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

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

4065  945 
then 
3083  946 
(*Backtrack at this level. 
947 
Reset Vars and try another rule*) 

948 
(clearTo ntrl; deeper grls) 

949 
else (*backtrack to previous level*) 

950 
backtrack choices 

951 
end 

952 
else deeper grls 

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

955 
 closeF (L::Ls) = 

3083  956 
case tryClose(G,L) of 
957 
None => closeF Ls 

958 
 Some tac => 

959 
let val choices' = 

3092  960 
(if !trace then (prs"branch closed"; 
4065  961 
traceVars sign ntrl) 
3083  962 
else (); 
963 
prune (nbrs, nxtVars, 

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

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

3083  967 
handle PRV => 
968 
(*reset Vars and try another literal 

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

970 
(clearTo ntrl; closeF Ls) 

971 
end 

2894  972 
fun closeFl [] = raise CLOSEF 
973 
 closeFl ((br, haz)::pairs) = 

974 
closeF (map fst br) 

975 
handle CLOSEF => closeF (map fst haz) 

976 
handle CLOSEF => closeFl pairs 

3083  977 
in tracing sign brs0; 
4065  978 
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) 
2854  979 
else 
3092  980 
prv ((TRY o Data.vars_gen_hyp_subst_tac false) :: tacs, 
981 
(*The TRY above allows the substitution to fail, e.g. if 

982 
the real version is z = f(?x z). Rest of proof might 

983 
still succeed!*) 

2854  984 
brs0::trs, choices, 
3092  985 
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
4065  986 
handle DEST_EQ => closeF lits 
987 
handle CLOSEF => closeFl ((br,haz)::pairs) 

988 
handle CLOSEF => deeper rules 

2894  989 
handle NEWBRANCHES => 
990 
(case netMkRules G vars hazList of 

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

994 
::brs) 

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

996 
prv (if isGoal G then negOfGoal_tac :: tacs 

997 
else tacs, 

998 
brs0::trs, choices, 

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

1000 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

1013 
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

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

1015 
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

1016 
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

1017 
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

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

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

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

1021 
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

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

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

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

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

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

1029 
to branch.*) 

1030 
fun deeper [] = raise NEWBRANCHES 

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

4065  1032 
if unify(add_term_vars(P,[]), P, H) 
3083  1033 
then 
1034 
let val ntrl' = !ntrail 

1035 
val vars = vars_in_vars vars 

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

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

1038 
val dup = md andalso vars' <> vars 

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

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

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

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

1043 
else lim1 

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

1045 
both dup and recur are false. Proofs are 

1046 
found at shallower depths, but looping 

1047 
occurs too often...*) 

3917  1048 
val mayUndo = 
1049 
(*Allowing backtracking from a rule application 

1050 
if other matching rules exist, if the rule 

1051 
updated variables, or if the rule did not 

1052 
introduce new variables. This latter condition 

1053 
means it is not a standard "gammarule" but 

1054 
some other form of unsafe rule. Aim is to 

1055 
emulate Fast_tac, which allows all unsafe steps 

1056 
to be undone.*) 

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

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

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

3083  1060 
val tac' = if mayUndo then tac dup 
1061 
else DETERM o (tac dup) 

1062 
in 

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

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

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

3083  1067 
else 
4065  1068 
traceNew prems; traceVars sign ntrl; 
4300  1069 
if null prems then nclosed := !nclosed + 1 
1070 
else ntried := !ntried + length prems  1; 

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

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

1073 
call rotate_tac: new formulae should be last*) 
3083  1074 
brs0::trs, 
1075 
(ntrl, length brs0, PRV) :: choices, 

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

1077 
handle PRV => 

1078 
if mayUndo 

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

1080 
(clearTo ntrl; deeper grls) 

1081 
else (*backtrack to previous level*) 

1082 
backtrack choices 

1083 
end 

1084 
else deeper grls 

1085 
in tracing sign brs0; 

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

1087 
else deeper rules 
2854  1088 
handle NEWBRANCHES => 
2894  1089 
(*cannot close branch: move H to literals*) 
2854  1090 
prv (tacs, brs0::trs, choices, 
2894  1091 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1092 
end 
1093 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1094 
in init_gensym(); 
1095 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1096 
end; 

2854  1097 

1098 

2883  1099 
(*Construct an initial branch.*) 
2854  1100 
fun initBranch (ts,lim) = 
2894  1101 
([(map (fn t => (t,true)) ts, [])], 
1102 
[], add_terms_vars (ts,[]), lim); 

2854  1103 

1104 

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

1106 

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

1108 
local open Term 

1109 
in 

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

1111 
 discard_foralls t = t; 

1112 
end; 

1113 

1114 

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

1116 
fun getVars [] i = [] 

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

1118 
if i mem is then getVars alist i 

1119 
else v :: getVars alist i; 

1120 

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

1121 
exception TRANS of string; 
2854  1122 

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

1123 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1124 
fun fromSubgoal t = 
1125 
let val alistVar = ref [] 

1126 
and alistTVar = ref [] 

2854  1127 
fun hdvar ((ix,(v,is))::_) = v 
1128 
fun from lev t = 

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

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

1131 
fun bounds [] = [] 

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

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

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

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

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

1137 
"Function unknown's argument not a bound variable" 
2854  1138 
in 
1139 
case ht of 

4065  1140 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1141 
 Term.Free (a,_) => apply (Free a) 
1142 
 Term.Bound i => apply (Bound i) 

1143 
 Term.Var (ix,_) => 

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

1146 
:: !alistVar; 

1147 
Var (hdvar(!alistVar))) 

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

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

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

1151 
^ Syntax.string_of_vname ix)) 
2854  1152 
 Term.Abs (a,_,body) => 
1153 
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

1154 
else raise TRANS "argument not in normal form" 
2854  1155 
end 
1156 

1157 
val npars = length (Logic.strip_params t) 

1158 

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

1160 
fun skoSubgoal i t = 

1161 
if i<npars then 

1162 
skoSubgoal (i+1) 

4065  1163 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1164 
t)) 
1165 
else t 

1166 

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

1168 

1169 

4300  1170 
fun initialize() = 
1171 
(fullTrace:=[]; trail := []; ntrail := 0; 

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

1173 

1174 

1175 
fun printStats b = 

1176 
if b then 

1177 
(writeln ("Branches closed: " ^ Int.toString (!nclosed)); 

1178 
writeln ("Branches tried: " ^ Int.toString (!ntried))) 

1179 
else (); 

1180 

1181 

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

1184 
fun depth_tac cs lim i st = 

4300  1185 
(initialize(); 
3030  1186 
let val {sign,...} = rep_thm st 
4065  1187 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
2854  1188 
val hyps = strip_imp_prems skoprem 
1189 
and concl = strip_imp_concl skoprem 

3083  1190 
fun cont (tacs,_,choices) = 
4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

1191 
(case Seq.pull(EVERY' (rev tacs) i st) of 
2854  1192 
None => (writeln ("PROOF FAILED for depth " ^ 
1193 
Int.toString lim); 

1194 
backtrack choices) 

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

1195 
 cell => Seq.make(fn()=> cell)) 
4300  1196 
in #1 (prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont), 
1197 
printStats (!trace)) 

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

1199 
handle PROVE => Seq.empty); 
2854  1200 

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

1201 
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

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

4078  1204 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1205 

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

1206 

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

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

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

1209 

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

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

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

1213 
let val st = topthm() 
3030  1214 
val {sign,...} = rep_thm st 
4065  1215 
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

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

1217 
and concl = strip_imp_concl skoprem 
4300  1218 
in #1 (timeap prove 
1219 
(sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I), 

1220 
printStats true) 

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

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

1222 
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

1223 

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

1225 

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

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

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

1229 

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

1230 
fun tryInThy thy lim s = 
4300  1231 
(initialize(); 
1232 
#1 (timeap prove (sign_of thy, 

1233 
Data.claset(), 

1234 
[initBranch ([readGoal (sign_of thy) s], lim)], 

1235 
I), 

1236 
printStats true)); 

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 

2854  1239 
end; 
1240 