author  paulson 
Tue, 15 Apr 1997 10:22:50 +0200  
changeset 2952  ea834e8fac1b 
parent 2924  af506c35b4ed 
child 2999  fad7cc426242 
permissions  rwrr 
2894  1 
(* Title: Provers/blast 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Generic tableau prover with proof reconstruction 

7 

2952  8 
Why does Abs take a string argument? 
9 

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

13 

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

14 
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

15 
Blast_tac... 
2894  16 
* ignores addss, addbefore, addafter; this restriction is intrinsic 
17 
* ignores elimination rules that don't have the correct format 

18 
(conclusion must be a formula variable) 

19 
* ignores types, which can make HOL proofs fail 

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

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

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

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

24 
Known problems: 

2952  25 
With overloading: 
26 
1. Overloading can't follow all chains of type dependencies. Cannot 

27 
prove "In1 x ~: Part A In0" because PartE introducees the polymorphic 

28 
equality In1 x = In0 y, when the corresponding rule uses the (distinct) 

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

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

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

32 
type ... set) 

33 

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

34 
With substition for equalities (hyp_subst_tac): 
2894  35 
1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter 
36 
as the argument of a function variable 

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

37 
2. When substitution affects a haz formula or literal, it is moved 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

43 

44 
(*Should be a type abbreviation?*) 

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

46 

47 

48 
(*Assumptions about constants: 

49 
The negation symbol is "Not" 

50 
The equality symbol is "op =" 

51 
The istrue judgement symbol is "Trueprop" 

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

53 
*) 

54 
signature BLAST_DATA = 

55 
sig 

56 
type claset 

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

58 
val ccontr : thm 

59 
val contr_tac : int > tactic 

60 
val dup_intr : thm > thm 

61 
val vars_gen_hyp_subst_tac : bool > int > tactic 

62 
val claset : claset ref 

63 
val rep_claset : 

64 
claset > {safeIs: thm list, safeEs: thm list, 

65 
hazIs: thm list, hazEs: thm list, 

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

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

68 
safe0_netpair: netpair, safep_netpair: netpair, 

69 
haz_netpair: netpair, dup_netpair: netpair} 

70 
end; 

71 

72 

73 
signature BLAST = 

74 
sig 

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

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

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

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

78 
 OConst of string * int 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

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

84 
 op $ of term*term; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

88 
val Blast_tac : int > tactic 

89 
val declConsts : string list * thm list > unit 

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

90 
(*debugging tools*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

92 
val fullTrace : branch list list ref 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

93 
val fromTerm : Type.type_sig > Term.term > term 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

94 
val fromSubgoal : Type.type_sig > Term.term > term 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

97 
val tryInThy : theory > int > string > 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

98 
branch list list * (int*int*exn) list * (int > tactic) list 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

99 
val trygl : claset > int > int > 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

100 
branch list list * (int*int*exn) list * (int > tactic) list 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

101 
val Trygl : int > int > 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

102 
branch list list * (int*int*exn) list * (int > tactic) list 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

103 
val normBr : branch > branch 
2854  104 
end; 
105 

106 

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

107 
functor BlastFun(Data: BLAST_DATA): BLAST = 
2854  108 
struct 
109 

110 
type claset = Data.claset; 

111 

112 
val trace = ref false; 

113 

114 
datatype term = 

115 
Const of string 

116 
 OConst of string * int 

117 
 Skolem of string * term option ref list 

118 
 Free of string 

119 
 Var of term option ref 

120 
 Bound of int 

121 
 Abs of string*term 

122 
 op $ of term*term; 

123 

124 

125 
exception DEST_EQ; 

126 

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

128 
fun dest_eq (Const "op =" $ t $ u) = (t,u) 

129 
 dest_eq (OConst("op =",_) $ t $ u) = (t,u) 

130 
 dest_eq _ = raise DEST_EQ; 

131 

132 
(** Basic syntactic operations **) 

133 

134 
fun is_Var (Var _) = true 

135 
 is_Var _ = false; 

136 

137 
fun dest_Var (Var x) = x; 

138 

139 

140 
fun rand (f$x) = x; 

141 

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

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

144 

145 

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

147 
fun strip_comb u : term * term list = 

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

149 
 stripc x = x 

150 
in stripc(u,[]) end; 

151 

152 

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

154 
fun head_of (f$t) = head_of f 

155 
 head_of u = u; 

156 

157 

158 
(** Particular constants **) 

159 

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

161 

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

163 

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

165 
 isGoal _ = false; 

166 

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

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

169 

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

171 
 isTrueprop _ = false; 

172 

173 

174 
(** Dealing with overloaded constants **) 

175 

176 
(*Result is a symbol table, indexed by names of overloaded constants. 

177 
Each constant maps to a list of (pattern,Blast.Const) pairs. 

178 
Any Term.Const that matches a pattern gets replaced by the Blast.Const. 

179 
*) 

180 
fun addConsts (t as Term.Const(a,_), tab) = 

181 
(case Symtab.lookup (tab,a) of 

182 
None => tab (*ignore: not a constant that we are looking for*) 

183 
 Some patList => 

184 
(case gen_assoc (op aconv) (patList, t) of 

185 
None => Symtab.update 

186 
((a, (t, OConst (a, length patList)) :: patList), 

187 
tab) 

188 
 _ => tab)) 

189 
 addConsts (Term.Abs(_,_,body), tab) = addConsts (body, tab) 

190 
 addConsts (Term.$ (t,u), tab) = addConsts (t, addConsts (u, tab)) 

191 
 addConsts (_, tab) = tab (*ignore others*); 

192 

193 

194 
fun addRules (rls,tab) = foldr addConsts (map (#prop o rep_thm) rls, tab); 

195 

2883  196 
fun declConst (a,tab) = 
197 
case Symtab.lookup (tab,a) of 

198 
None => Symtab.update((a,[]), tab) (*create a brand new entry*) 

199 
 Some _ => tab (*preserve old entry*); 

2854  200 

201 
(*maps the name of each overloaded constant to a list of archetypal constants, 

202 
which may be polymorphic.*) 

203 
local 

204 
val overLoadTab = ref (Symtab.null : (Term.term * term) list Symtab.table) 

205 
(*The alists in this table should only be increased*) 

206 
in 

207 

208 
fun declConsts (names, rls) = 

209 
overLoadTab := addRules (rls, foldr declConst (names, !overLoadTab)); 

210 

211 

212 
(*Convert a possibly overloaded Term.Const to a Blast.Const*) 

213 
fun fromConst tsig (t as Term.Const (a,_)) = 

214 
let fun find [] = Const a 

215 
 find ((pat,t')::patList) = 

216 
if Pattern.matches tsig (pat,t) then t' 

217 
else find patList 

218 
in case Symtab.lookup(!overLoadTab, a) of 

219 
None => Const a 

220 
 Some patList => find patList 

221 
end; 

222 
end; 

223 

224 

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

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

227 
 (OConst ai) aconv (OConst bj) = ai=bj 

228 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 

229 
 (Free a) aconv (Free b) = a=b 

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

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

232 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 

233 
 (Bound i) aconv (Bound j) = i=j 

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

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

236 
 _ aconv _ = false; 

237 

238 

239 
fun mem_term (_, []) = false 

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

241 

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

243 

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

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

246 

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

248 

249 

250 
(** Vars **) 

251 

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

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

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

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

256 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 

257 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

258 
 add_term_vars (_, vars) = vars 

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

260 
and add_terms_vars ([], vars) = vars 

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

262 
(*Var list version.*) 

263 
and add_vars_vars ([], vars) = vars 

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

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

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

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

268 

269 

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

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

272 

273 

274 

275 
(*increment a term's nonlocal bound variables 

276 
inc is increment for bound variables 

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

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

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

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

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

282 

283 
fun incr_boundvars 0 t = t 

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

285 

286 

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

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

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

290 
else (ilev) ins_int js 

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

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

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

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

295 

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

297 

298 
fun subst_bound (arg, t) : term = 

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

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

301 
else if i=lev then incr_boundvars lev arg 

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

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

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

305 
 subst (t,lev) = t 

306 
in subst (t,0) end; 

307 

308 

309 
(*Normalize...but not the bodies of ABSTRACTIONS*) 

310 
fun norm t = case t of 

2952  311 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
2854  312 
 (Var (ref None)) => t 
313 
 (Var (ref (Some u))) => norm u 

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

315 
Abs(_,body) => norm (subst_bound (u, body)) 

316 
 nf => nf $ norm u) 

317 
 _ => t; 

318 

319 

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

321 
fun wkNormAux t = case t of 

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

323 
Some u => wkNorm u 

324 
 None => t) 

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

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

327 
 nf => nf $ u) 

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

330 
nb as (f $ t) => 

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

332 
then Abs(a,nb) 

333 
else wkNorm (incr_boundvars ~1 f) 

334 
 nb => Abs (a,nb)) 

2854  335 
 _ => t 
336 
and wkNorm t = case head_of t of 

337 
Const _ => t 

338 
 OConst _ => t 

339 
 Skolem(a,args) => t 

340 
 Free _ => t 

341 
 _ => wkNormAux t; 

342 

343 

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

345 
fun varOccur v = 

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

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

348 
and occ (Var w) = 

349 
v=w orelse 

350 
(case !w of None => false 

351 
 Some u => occ u) 

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

353 
 occ (Abs(_,u)) = occ u 

354 
 occ (f$u) = occ u orelse occ f 

355 
 occ (_) = false; 

356 
in occ end; 

357 

358 
exception UNIFY; 

359 

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

361 
val ntrail = ref 0; 

362 

363 

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

365 
fun clearTo n = 

366 
while !ntrail>n do 

367 
(hd(!trail) := None; 

368 
trail := tl (!trail); 

369 
ntrail := !ntrail  1); 

370 

371 

372 
(*Firstorder unification with bound variables. 

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

374 
on the trail (no point in doing so) 

375 
*) 

376 
fun unify(vars,t,u) = 

377 
let val n = !ntrail 

378 
fun update (t as Var v, u) = 

379 
if t aconv u then () 

380 
else if varOccur v u then raise UNIFY 

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

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

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

384 
then dest_Var u := Some t 

385 
else (v := Some u; 

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

387 
fun unifyAux (t,u) = 

388 
case (wkNorm t, wkNorm u) of 

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

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

391 
 (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') 

392 
(*NB: can yield unifiers having dangling Bound vars!*) 

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

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

395 
in unifyAux(t,u) handle UNIFY => (clearTo n; raise UNIFY) 

396 
end; 

397 

398 

399 
(*Convert from "real" terms to prototerms; etacontract*) 

400 
fun fromTerm tsig t = 

401 
let val alist = ref [] 

402 
fun from (t as Term.Const _) = fromConst tsig t 

403 
 from (Term.Free (a,_)) = Free a 

404 
 from (Term.Bound i) = Bound i 

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

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

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

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

409 
end 

410 
 Some (v,_) => v) 

411 
 from (Term.Abs (a,_,u)) = 

412 
(case from u of 

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

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

415 
else incr_boundvars ~1 f 

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

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

418 
in from t end; 

419 

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

421 
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 

422 
A :: strip_imp_prems B 

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

424 
 strip_imp_prems _ = []; 

425 

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

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

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

429 
 strip_imp_concl A = A : term; 

430 

431 

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

433 

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

435 
fun squash_nots [] = [] 

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

437 
squash_nots Ps 

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

439 
squash_nots Ps 

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

441 

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

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

444 
 skoPrem vars P = P; 

445 

446 
fun convertPrem t = 

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

448 

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

450 
fun convertRule vars t = 

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

452 
val Var v = strip_imp_concl t 

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

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

455 
end; 

456 

457 

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

459 
fun rev_dup_elim th = th RSN (2, revcut_rl) > assumption 2 > Sequence.hd; 

460 

461 

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

463 
fun nNewHyps [] = 0 

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

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

466 

467 
fun rot_subgoals_tac [] i st = Sequence.single st 

468 
 rot_subgoals_tac (k::ks) i st = 

469 
rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st)) 

470 
handle OPTION _ => Sequence.null; 

471 

472 
fun TRACE rl tac st = if !trace then (prth rl; tac st) else tac st; 

473 

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

475 
affected formula.*) 

476 
fun fromRule vars rl = 

477 
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl)) 

478 
val trl = rl > rep_thm > #prop > fromTerm tsig > convertRule vars 

479 
fun tac dup i = 

480 
TRACE rl 

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

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

484 
in General.SOME (trl, tac) end 

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

485 
handle Bind => (*reject: conclusion is not just a variable*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

486 
(if !trace then (writeln"Warning: ignoring illformed elimination rule"; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

488 
else (); 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

489 
General.NONE); 
2854  490 

491 

492 
(*** Conversion of Introduction Rules (needed for efficiency in 

493 
proof reconstruction) ***) 

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 = 

506 
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl)) 

507 
val trl = rl > rep_thm > #prop > fromTerm tsig > convertIntrRule vars 

508 
fun tac dup i = 

509 
TRACE rl (DETERM (rtac (if dup then Data.dup_intr rl else rl) i)) 

510 
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i 

511 
in (trl, tac) end; 

512 

513 

514 
val dummyVar = Term.Var (("Doom",666), dummyT); 

515 

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

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

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

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

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

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

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

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

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

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

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

528 

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

530 
case P of 

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

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

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

535 
nps) 

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

537 
 _ => 

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

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

541 
nps) 

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

543 

544 
(** 

545 
end; 

546 
**) 

547 

548 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 

549 

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

551 
fun subst_atomic (old,new) t = 

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

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

554 
 subst (f$t) = subst f $ subst t 

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

556 
in subst t end; 

557 

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

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

560 
(case eta_contract2 body of 

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

562 
else eta_contract_atom (incr_boundvars ~1 f) 

563 
 _ => t0) 

564 
 eta_contract_atom t = t 

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

566 
 eta_contract2 t = eta_contract_atom t; 

567 

568 

569 
(*When can we safely delete the equality? 

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

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

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

573 
Prefer to eliminate Bound variables if possible. 

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

575 

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

577 
Does NOT check args of Skolem terms: substitution does not affect them. 

578 
NOT reflexive since hyp_subst_tac fails on x=x.*) 

579 
fun substOccur t = 

580 
let fun occEq u = (t aconv u) orelse occ u 

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

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

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

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

585 
 occ (_) = false; 

586 
in occEq end; 

587 

588 
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; 

589 

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

591 
THEN orient that equality ELSE raise exception DEST_EQ*) 

592 
fun orientGoal (t,u) = 

593 
case (eta_contract_atom t, eta_contract_atom u) of 

594 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 

595 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

598 
 _ => raise DEST_EQ; 

599 

600 

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

601 

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

602 

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

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

606 
fun equalSubst (G, pairs, lits, vars, lim) = 

2854  607 
let val subst = subst_atomic (orientGoal(dest_eq G)) 
608 
fun subst2(G,md) = (subst G, md) 

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

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

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

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

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

613 
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

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

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

616 
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

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

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

2854  621 
let val nlit = subst lit 
2894  622 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
623 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  624 
end 
2894  625 
in subLits (rev lits, [], []) 
2854  626 
end; 
627 

628 

629 
exception NEWBRANCHES and CLOSEF; 

630 

2894  631 
(*Pending formulae carry md (may duplicate) flags*) 
632 
type branch = ((term*bool) list * (*safe formulae on this level*) 

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

2854  634 
term list * (*literals: irreducible formulae*) 
635 
term option ref list * (*variables occurring in branch*) 

636 
int; (*resource limit*) 

637 

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

639 

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

640 
(*Normalize a branchfor tracing*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

642 
fun norm2 (G,md) = (norm G, md); 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

643 

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

644 
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

645 

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

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

647 
fun normBr (br, lits, vars, lim) = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

648 
(map normLev br, map norm lits, vars, lim); 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

649 

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

650 
fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace 
2952  651 
else () 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

653 

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

654 

2854  655 
exception PROVE; 
656 

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

658 

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

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

661 

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

663 
fun tryClose (Const"*Goal*" $ G, L) = (unify([],G,L); eAssume_tac) 

664 
 tryClose (G, Const"*Goal*" $ L) = (unify([],G,L); eAssume_tac) 

665 
 tryClose (Const"Not" $ G, L) = (unify([],G,L); eContr_tac) 

666 
 tryClose (G, Const"Not" $ L) = (unify([],G,L); eContr_tac) 

667 
 tryClose _ = raise UNIFY; 

668 

669 

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

671 
fun hasSkolem (Skolem _) = true 

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

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

674 
 hasSkolem _ = false; 

675 

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

677 
Skolem terms then allow duplication.*) 

678 
fun joinMd md [] = [] 

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

680 

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

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

684 
 negOfGoal G = G; 

685 

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

687 

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

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

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

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

692 

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

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

695 

2854  696 

697 
(** Backtracking and Pruning **) 

698 

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

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

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

702 
 clashVar vars = 

703 
let fun clash (0, _) = false 

704 
 clash (_, []) = false 

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

706 
in clash end; 

707 

708 

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

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

711 
next branch have been updated.*) 

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

713 
backtracking over bad proofs*) 

714 
 prune (nbrs, nxtVars, choices) = 

715 
let fun traceIt last = 

716 
let val ll = length last 

717 
and lc = length choices 

718 
in if !trace andalso ll<lc then 

719 
(writeln("PRUNING " ^ Int.toString(lcll) ^ " LEVELS"); 

720 
last) 

721 
else last 

722 
end 

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

724 
 pruneAux (last, ntrl, trl, ch' as (ntrl',nbrs',exn) :: choices) = 

725 
if nbrs' < nbrs 

726 
then last (*don't backtrack beyond first solution of goal*) 

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

728 
else (* nbrs'=nbrs *) 

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

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

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

732 
choices) 

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

734 

2894  735 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
2854  736 
 nextVars [] = []; 
737 

738 
fun backtrack ((_, _, exn)::_) = raise exn 

739 
 backtrack _ = raise PROVE; 

740 

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

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

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

746 
 bad _ = false; 

747 
fun change [] = [] 

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

749 
if G aconv G' then change lits 

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

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

752 
if G aconv G' then change lits 

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

754 
 change (lit::lits) = lit :: change lits 

755 
in 

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

757 
end 

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

759 

760 

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

763 
fun log3 n = if n<3 then 0 else 1 + log3(n div 3); 

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

764 

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

765 

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

768 
bound on unsafe expansions.*) 

769 
fun prove (cs, brs, cont) = 

770 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs 

771 
val safeList = [safe0_netpair, safep_netpair] 

772 
and hazList = [haz_netpair] 

773 
fun prv (tacs, trs, choices, []) = (cont (trs,choices,tacs)) 

774 
 prv (tacs, trs, choices, 

2894  775 
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = 
2854  776 
let exception PRV (*backtrack to precisely this recursion!*) 
777 
val ntrl = !ntrail 

778 
val nbrs = length brs0 

779 
val nxtVars = nextVars brs 

780 
val G = norm G 

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

781 
val rules = netMkRules G vars safeList 
2854  782 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  783 
fun newBr (vars',lim') prems = 
784 
map (fn prem => 

785 
if (exists isGoal prem) 

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

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

788 
map negOfGoal lits, 

789 
vars', lim') 

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

791 
lits, vars', lim')) 

2854  792 
prems @ 
793 
brs 

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

795 
to branch.*) 

796 
fun deeper [] = raise NEWBRANCHES 

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

798 
let val dummy = unify(add_term_vars(P,[]), P, G) 

799 
(*P comes from the rule; G comes from the branch.*) 

800 
val ntrl' = !ntrail 

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

801 
val lim' = if ntrl < !ntrail 
2952  802 
then lim  (1+log3(length rules)) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

803 
else lim (*discourage branching updates*) 
2894  804 
val vars = vars_in_vars vars 
805 
val vars' = foldr add_terms_vars (prems, vars) 

2854  806 
val choices' = (ntrl, nbrs, PRV) :: choices 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

807 
val tacs' = (DETERM o (tac false)) :: tacs 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

808 
(*no duplication*) 
2854  809 
in 
810 
if null prems then (*closed the branch: prune!*) 

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

811 
prv(tacs', brs0::trs, 
2854  812 
prune (nbrs, nxtVars, choices'), 
813 
brs) 

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

814 
handle PRV => (*reset Vars and try another rule*) 
2854  815 
(clearTo ntrl; deeper grls) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

816 
else (*can we kill all the alternatives??*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

817 
if lim'<0 then raise NEWBRANCHES 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

819 
prv(tacs', brs0::trs, choices', 
2894  820 
newBr (vars',lim') prems) 
2854  821 
handle PRV => 
822 
if ntrl < ntrl' then 

823 
(*Vars have been updated: must backtrack 

824 
even if not mentioned in other goals! 

825 
Reset Vars and try another rule*) 

826 
(clearTo ntrl; deeper grls) 

827 
else (*backtrack to previous level*) 

828 
backtrack choices 

829 
end 

830 
handle UNIFY => deeper grls 

831 
(*Try to close branch by unifying with head goal*) 

832 
fun closeF [] = raise CLOSEF 

833 
 closeF (L::Ls) = 

834 
let val tacs' = tryClose(G,L)::tacs 

835 
val choices' = prune (nbrs, nxtVars, 

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

837 
in prv (tacs', brs0::trs, choices', brs) 

838 
handle PRV => 

839 
(*reset Vars and try another literal 

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

841 
(clearTo ntrl; closeF Ls) 

842 
end 

843 
handle UNIFY => closeF Ls 

2894  844 
fun closeFl [] = raise CLOSEF 
845 
 closeFl ((br, haz)::pairs) = 

846 
closeF (map fst br) 

847 
handle CLOSEF => closeF (map fst haz) 

848 
handle CLOSEF => closeFl pairs 

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

849 
in tracing brs0; 
2854  850 
if lim<0 then backtrack choices 
851 
else 

852 
prv (Data.vars_gen_hyp_subst_tac false :: tacs, 

853 
brs0::trs, choices, 

2894  854 
equalSubst (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
2854  855 
handle DEST_EQ => closeF lits 
2894  856 
handle CLOSEF => closeFl ((br,haz)::pairs) 
2854  857 
handle CLOSEF => 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

858 
deeper rules 
2894  859 
handle NEWBRANCHES => 
860 
(case netMkRules G vars hazList of 

861 
[] => (*no plausible rules: move G to literals*) 

862 
prv (tacs, brs0::trs, choices, 

863 
((br,haz)::pairs, addLit(G,lits), vars, lim) 

864 
::brs) 

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

866 
prv (if isGoal G then negOfGoal_tac :: tacs 

867 
else tacs, 

868 
brs0::trs, choices, 

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

870 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

883 
val rules = netMkRules H vars hazList 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

884 
fun newPrem (vars,dup,lim') prem = 
2894  885 
([(map (fn P => (P,false)) prem, []), (*may NOT duplicate*) 
886 
([], if dup then Hs @ [(negOfGoal H, md)] else Hs)], 

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

887 
lits, vars, lim') 
2854  888 
fun newBr x prems = map (newPrem x) prems @ brs 
889 
(*Seek a matching rule. If unifiable then add new premises 

890 
to branch.*) 

891 
fun deeper [] = raise NEWBRANCHES 

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

2894  893 
let val dummy = unify(add_term_vars(P,[]), P, H) 
2854  894 
val ntrl' = !ntrail 
895 
val vars = vars_in_vars vars 

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

897 
val dup = md andalso vars' <> vars 

2894  898 
(*duplicate H only if md and the premise has new vars*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

899 
val lim' = (*Decrement "lim" extra if updates occur*) 
2952  900 
if ntrl < !ntrail then lim  (1+log3(length rules)) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

902 
(*NB: if the formula is duplicated, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

903 
then it seems plausible to leave lim alone. 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

904 
But then transitivity laws loop.*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

905 
val mayUndo = not (null grls) (*other rules to try?*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

906 
orelse ntrl < ntrl' (*variables updated?*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

907 
orelse vars=vars' (*no new Vars?*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

908 
val tac' = if mayUndo then tac dup 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

909 
else DETERM o (tac dup) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

911 
(*can we kill all the alternatives??*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

912 
if lim'<0 andalso not (null prems) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

915 
prv(tac dup :: tacs, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

917 
(ntrl, length brs0, PRV) :: choices, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

918 
newBr (vars', dup, lim') prems) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

919 
handle PRV => 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

921 
then (*reset Vars and try another rule*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

922 
(clearTo ntrl; deeper grls) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

923 
else (*backtrack to previous level*) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

924 
backtrack choices 
2854  925 
end 
926 
handle UNIFY => deeper grls 

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

927 
in tracing brs0; 
2854  928 
if lim<1 then backtrack choices 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

929 
else deeper rules 
2854  930 
handle NEWBRANCHES => 
2894  931 
(*cannot close branch: move H to literals*) 
2854  932 
prv (tacs, brs0::trs, choices, 
2894  933 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  934 
end 
935 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

936 
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 

937 

938 

2883  939 
(*Construct an initial branch.*) 
2854  940 
fun initBranch (ts,lim) = 
2894  941 
([(map (fn t => (t,true)) ts, [])], 
942 
[], add_terms_vars (ts,[]), lim); 

2854  943 

944 

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

946 

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

948 
local open Term 

949 
in 

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

951 
 discard_foralls t = t; 

952 
end; 

953 

954 

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

956 
fun getVars [] i = [] 

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

958 
if i mem is then getVars alist i 

959 
else v :: getVars alist i; 

960 

961 

962 
(*Conversion of a subgoal: Skolemize all parameters*) 

963 
fun fromSubgoal tsig t = 

964 
let val alist = ref [] 

965 
fun hdvar ((ix,(v,is))::_) = v 

966 
fun from lev t = 

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

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

969 
fun bounds [] = [] 

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

971 
if i<lev then error"Function Var's argument not a parameter" 

972 
else ilev :: bounds ts 

973 
 bounds ts = error"Function Var's argument not a bound variable" 

974 
in 

975 
case ht of 

976 
t as Term.Const _ => apply (fromConst tsig t) 

977 
 Term.Free (a,_) => apply (Free a) 

978 
 Term.Bound i => apply (Bound i) 

979 
 Term.Var (ix,_) => 

980 
(case (assoc_string_int(!alist,ix)) of 

981 
None => (alist := (ix, (ref None, bounds ts)) 

982 
:: !alist; 

983 
Var (hdvar(!alist))) 

984 
 Some(v,is) => if is=bounds ts then Var v 

985 
else error("Discrepancy among occurrences of ?" 

986 
^ Syntax.string_of_vname ix)) 

987 
 Term.Abs (a,_,body) => 

988 
if null ts then Abs(a, from (lev+1) body) 

989 
else error "fromSubgoal: argument not in normal form" 

990 
end 

991 

992 
val npars = length (Logic.strip_params t) 

993 

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

995 
fun skoSubgoal i t = 

996 
if i<npars then 

997 
skoSubgoal (i+1) 

998 
(subst_bound (Skolem (gensym "SG_", getVars (!alist) i), 

999 
t)) 

1000 
else t 

1001 

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

1003 

1004 

1005 
(*Tactic using tableau engine and proof reconstruction. 

1006 
"lim" is depth limit.*) 

1007 
fun depth_tac cs lim i st = 

1008 
(fullTrace:=[]; trail := []; ntrail := 0; 

1009 
let val {tsig,...} = Sign.rep_sg (#sign (rep_thm st)) 

1010 
val skoprem = fromSubgoal tsig (List.nth(prems_of st, i1)) 

1011 
val hyps = strip_imp_prems skoprem 

1012 
and concl = strip_imp_concl skoprem 

1013 
fun cont (_,choices,tacs) = 

1014 
(case Sequence.pull(EVERY' (rev tacs) i st) of 

1015 
None => (writeln ("PROOF FAILED for depth " ^ 

1016 
Int.toString lim); 

1017 
backtrack choices) 

1018 
 cell => Sequence.seqof(fn()=> cell)) 

1019 
in prove (cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 

1020 
end 

1021 
handle Subscript => Sequence.null 

1022 
 PROVE => Sequence.null); 

1023 

1024 
fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0); 

1025 

1026 
fun Blast_tac i = blast_tac (!Data.claset) i; 

1027 

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

1028 

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

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

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

1031 

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

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

1033 
fun trygl cs lim i = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1034 
(fullTrace:=[]; trail := []; ntrail := 0; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1035 
let val st = topthm() 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1036 
val {tsig,...} = Sign.rep_sg (#sign (rep_thm st)) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1037 
val skoprem = fromSubgoal tsig (List.nth(prems_of st, i1)) 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

1039 
and concl = strip_imp_concl skoprem 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

1043 
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

1044 

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

1045 
fun Trygl lim i = trygl (!Data.claset) lim i; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1046 

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

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

1048 
fun readGoal sign s = read_cterm sign (s,propT) > 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1049 
term_of > fromTerm (#tsig(Sign.rep_sg sign)) > 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1050 
rand > mkGoal; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1051 

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

1052 
fun tryInThy thy lim s = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1053 
(fullTrace:=[]; trail := []; ntrail := 0; 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1054 
timeap prove (!Data.claset, 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1055 
[initBranch ([readGoal (sign_of thy) s], lim)], 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

1057 

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

1058 

2854  1059 
end; 
1060 