author  wenzelm 
Wed, 15 Oct 1997 15:12:59 +0200  
changeset 3872  a5839ecee7b8 
parent 3533  b976967a92fc 
child 3917  6ea5f9101c3e 
permissions  rwrr 
2894  1 
(* Title: Provers/blast 
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 

63 
val claset : claset ref 

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 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

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

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

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

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

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

89 
val Blast_tac : int > tactic 

90 
val declConsts : string list * thm list > unit 

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

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

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

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

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

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

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

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

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

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

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

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

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

107 

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

111 
type claset = Data.claset; 

112 

113 
val trace = ref false; 

114 

115 
datatype term = 

116 
Const of string 

117 
 OConst of string * int 

118 
 Skolem of string * term option ref list 

119 
 Free of string 

120 
 Var of term option ref 

121 
 Bound of int 

122 
 Abs of string*term 

123 
 op $ of term*term; 

124 

125 

126 
(** Basic syntactic operations **) 

127 

128 
fun is_Var (Var _) = true 

129 
 is_Var _ = false; 

130 

131 
fun dest_Var (Var x) = x; 

132 

133 

134 
fun rand (f$x) = x; 

135 

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

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

138 

139 

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

141 
fun strip_comb u : term * term list = 

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

143 
 stripc x = x 

144 
in stripc(u,[]) end; 

145 

146 

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

148 
fun head_of (f$t) = head_of f 

149 
 head_of u = u; 

150 

151 

152 
(** Particular constants **) 

153 

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

155 

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

157 

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

159 
 isGoal _ = false; 

160 

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

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

163 

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

165 
 isTrueprop _ = false; 

166 

167 

168 
(** Dealing with overloaded constants **) 

169 

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

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

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

173 
*) 

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

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

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

177 
 Some patList => 

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

179 
None => Symtab.update 

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

181 
tab) 

182 
 _ => tab)) 

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

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

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

186 

187 

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

189 

2883  190 
fun declConst (a,tab) = 
191 
case Symtab.lookup (tab,a) of 

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

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

2854  194 

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

196 
which may be polymorphic.*) 

197 
local 

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

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

200 
in 

201 

202 
fun declConsts (names, rls) = 

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

204 

205 

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

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

208 
let fun find [] = Const a 

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

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

211 
else find patList 

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

213 
None => Const a 

214 
 Some patList => find patList 

215 
end; 

216 
end; 

217 

218 

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

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

221 
 (OConst ai) aconv (OConst bj) = ai=bj 

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

223 
 (Free a) aconv (Free b) = a=b 

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

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

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

227 
 (Bound i) aconv (Bound j) = i=j 

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

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

230 
 _ aconv _ = false; 

231 

232 

233 
fun mem_term (_, []) = false 

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

235 

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

237 

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

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

240 

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

242 

243 

244 
(** Vars **) 

245 

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

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

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

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

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

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

252 
 add_term_vars (_, vars) = vars 

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

254 
and add_terms_vars ([], vars) = vars 

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

256 
(*Var list version.*) 

257 
and add_vars_vars ([], vars) = vars 

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

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

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

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

262 

263 

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

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

266 

267 

268 

269 
(*increment a term's nonlocal bound variables 

270 
inc is increment for bound variables 

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

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

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

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

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

276 

277 
fun incr_boundvars 0 t = t 

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

279 

280 

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

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

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

284 
else (ilev) ins_int js 

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

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

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

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

289 

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

291 

292 
fun subst_bound (arg, t) : term = 

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

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

295 
else if i=lev then incr_boundvars lev arg 

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

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

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

299 
 subst (t,lev) = t 

300 
in subst (t,0) end; 

301 

302 

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

303 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  304 
fun norm t = case t of 
2952  305 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
2854  306 
 (Var (ref None)) => t 
307 
 (Var (ref (Some u))) => norm u 

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

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

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

310 
 nf => nf $ norm u) 
2854  311 
 _ => t; 
312 

313 

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

315 
fun wkNormAux t = case t of 

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

317 
Some u => wkNorm u 

318 
 None => t) 

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

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

321 
 nf => nf $ u) 

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

324 
nb as (f $ t) => 

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

326 
then Abs(a,nb) 

327 
else wkNorm (incr_boundvars ~1 f) 

3092  328 
 nb => Abs (a,nb)) 
2854  329 
 _ => t 
330 
and wkNorm t = case head_of t of 

331 
Const _ => t 

332 
 OConst _ => t 

333 
 Skolem(a,args) => t 

334 
 Free _ => t 

335 
 _ => wkNormAux t; 

336 

337 

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

339 
fun varOccur v = 

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

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

342 
and occ (Var w) = 

343 
v=w orelse 

344 
(case !w of None => false 

345 
 Some u => occ u) 

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

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

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

349 
 occ (_) = false; 

350 
in occ end; 

351 

352 
exception UNIFY; 

353 

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

355 
val ntrail = ref 0; 

356 

357 

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

359 
fun clearTo n = 

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

363 
ntrail := !ntrail  1); 

364 

365 

366 
(*Firstorder unification with bound variables. 

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

368 
on the trail (no point in doing so) 

369 
*) 

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

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

373 
if t aconv u then () 

374 
else if varOccur v u then raise UNIFY 

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

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

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

378 
then dest_Var u := Some t 

379 
else (v := Some u; 

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

381 
fun unifyAux (t,u) = 

382 
case (wkNorm t, wkNorm u) of 

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

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

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

385 
 (Const a, OConst(b,_)) => if allowClash andalso a=b then () 
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

386 
else raise UNIFY 
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

387 
 (OConst(a,_), Const b) => if allowClash andalso a=b then () 
fad7cc426242
Penalty for branching instantiations reduced from log3 to log4.
paulson
parents:
2952
diff
changeset

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

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

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

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

396 

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

398 
fun fromTerm tsig t = 

399 
let val alist = ref [] 

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

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

402 
 from (Term.Bound i) = Bound i 

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

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

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

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

407 
end 

408 
 Some (v,_) => v) 

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

410 
(case from u of 

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

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

413 
else incr_boundvars ~1 f 

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

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

416 
in from t end; 

417 

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

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

420 
A :: strip_imp_prems B 

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

422 
 strip_imp_prems _ = []; 

423 

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

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

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

427 
 strip_imp_concl A = A : term; 

428 

429 

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

431 

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

433 
fun squash_nots [] = [] 

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

435 
squash_nots Ps 

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

437 
squash_nots Ps 

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

439 

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

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

442 
 skoPrem vars P = P; 

443 

444 
fun convertPrem t = 

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

446 

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

448 
fun convertRule vars t = 

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

450 
val Var v = strip_imp_concl t 

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

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

453 
end; 

454 

455 

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

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

458 

459 

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

461 
fun nNewHyps [] = 0 

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

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

464 

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

466 
 rot_subgoals_tac (k::ks) i st = 

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

468 
handle OPTION _ => Sequence.null; 

469 

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

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

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

473 
affected formula.*) 

474 
fun fromRule vars rl = 

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

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

477 
fun tac dup i = 

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

478 
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i 
2854  479 
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i 
480 

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

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

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

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

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

486 
Option.NONE); 
2854  487 

488 

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

489 
(*** Conversion of Introduction Rules ***) 
2854  490 

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

492 

493 
fun convertIntrRule vars t = 

494 
let val Ps = strip_imp_prems t 

495 
val P = strip_imp_concl t 

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

497 
end; 

498 

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

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

501 
fun fromIntrRule vars rl = 

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

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

504 
fun tac dup i = 

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

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

508 

509 

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

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

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

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

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

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

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

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

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

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

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

522 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  523 

524 

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

526 
case P of 

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

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

528 
let val pG = mk_tprop (toTerm 2 G) 
2854  529 
val intrs = List.concat 
530 
(map (fn (inet,_) => Net.unify_term inet pG) 

531 
nps) 

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

533 
 _ => 

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

534 
let val pP = mk_tprop (toTerm 3 P) 
2854  535 
val elims = List.concat 
536 
(map (fn (_,enet) => Net.unify_term enet pP) 

537 
nps) 

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

539 

540 
(** 

541 
end; 

542 
**) 

543 

3092  544 

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

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

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

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

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

550 
int; (*resource limit*) 

551 

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

553 

554 
(*Normalize a branchfor tracing*) 

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

556 

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

558 

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

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

561 

562 

563 
val dummyVar2 = Term.Var(("var",0), dummyT); 

564 

565 
(*Convert from prototerms to ordinary terms with dummy types for tracing*) 

566 
fun showTerm d (Const a) = Term.Const (a,dummyT) 

567 
 showTerm d (OConst(a,_)) = Term.Const (a,dummyT) 

568 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 

569 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

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

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

572 
 showTerm d (Var(ref None)) = dummyVar2 
3092  573 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
574 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

577 

578 

579 
fun traceTerm sign t = Sign.string_of_term sign (showTerm 8 (norm t)); 

580 

581 

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

583 
fun tracing sign brs = 

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

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

586 
 printPairs _ = () 

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

588 
(fullTrace := brs0 :: !fullTrace; 

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

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

591 
printPairs pairs; 

592 
writeln"") 

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

594 
end; 

595 

596 
(*Tracing: variables updated in the last branch operation?*) 

597 
fun traceVars ntrl = 

598 
if !trace then 

599 
(case !ntrailntrl of 

600 
0 => writeln"" 

601 
 1 => writeln"\t1 variable updated" 

602 
 n => writeln("\t" ^ Int.toString n ^ " variables updated")) 

603 
else (); 

604 

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

606 
fun traceNew prems = 

607 
if !trace then 

608 
case length prems of 

609 
0 => prs"branch closed by rule" 

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

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

612 
else (); 

613 

614 

615 

2854  616 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
617 

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

619 
fun subst_atomic (old,new) t = 

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

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

622 
 subst (f$t) = subst f $ subst t 

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

624 
in subst t end; 

625 

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

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

628 
(case eta_contract2 body of 

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

630 
else eta_contract_atom (incr_boundvars ~1 f) 

631 
 _ => t0) 

632 
 eta_contract_atom t = t 

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

634 
 eta_contract2 t = eta_contract_atom t; 

635 

636 

637 
(*When can we safely delete the equality? 

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

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

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

641 
Prefer to eliminate Bound variables if possible. 

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

643 

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

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

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

647 
fun substOccur t = 

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

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

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

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

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

653 
 occ (_) = false; 

654 
in occEq end; 

655 

3092  656 
exception DEST_EQ; 
657 

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

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

660 
(eta_contract_atom t, eta_contract_atom u) 

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

662 
(eta_contract_atom t, eta_contract_atom u) 

663 
 dest_eq _ = raise DEST_EQ; 

664 

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

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

668 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  669 
fun orientGoal (t,u) = case (t,u) of 
2854  670 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
671 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

674 
 _ => raise DEST_EQ; 

675 

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

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

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

681 
val subst = subst_atomic (t,u) 

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

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

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

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

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

687 
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

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

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

690 
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

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

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

2854  695 
let val nlit = subst lit 
2894  696 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
697 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  698 
end 
3092  699 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
700 
" for " ^ traceTerm sign t ^ " in branch" ) 

701 
else (); 

3083  702 
subLits (rev lits, [], []) 
2854  703 
end; 
704 

705 

706 
exception NEWBRANCHES and CLOSEF; 

707 

708 
exception PROVE; 

709 

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

711 

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

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

714 

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

3083  716 
fun tryClose (Const"*Goal*" $ G, L) = 
717 
if unify(true,[],G,L) then Some eAssume_tac else None 

718 
 tryClose (G, Const"*Goal*" $ L) = 

719 
if unify(true,[],G,L) then Some eAssume_tac else None 

720 
 tryClose (Const"Not" $ G, L) = 

721 
if unify(true,[],G,L) then Some eContr_tac else None 

722 
 tryClose (G, Const"Not" $ L) = 

723 
if unify(true,[],G,L) then Some eContr_tac else None 

724 
 tryClose _ = None; 

2854  725 

726 

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

728 
fun hasSkolem (Skolem _) = true 

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

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

731 
 hasSkolem _ = false; 

732 

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

734 
Skolem terms then allow duplication.*) 

735 
fun joinMd md [] = [] 

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

737 

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

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

741 
 negOfGoal G = G; 

742 

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

744 

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

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

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

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

749 

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

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

752 

2854  753 

754 
(** Backtracking and Pruning **) 

755 

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

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

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

759 
 clashVar vars = 

760 
let fun clash (0, _) = false 

761 
 clash (_, []) = false 

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

763 
in clash end; 

764 

765 

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

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

768 
next branch have been updated.*) 

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

770 
backtracking over bad proofs*) 

771 
 prune (nbrs, nxtVars, choices) = 

772 
let fun traceIt last = 

773 
let val ll = length last 

774 
and lc = length choices 

775 
in if !trace andalso ll<lc then 

3083  776 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  777 
last) 
778 
else last 

779 
end 

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

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

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

785 
else (* nbrs'=nbrs *) 

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

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

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

789 
choices) 

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

791 

2894  792 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  793 
 nextVars [] = []; 
2854  794 

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

797 
Int.toString nbrs ^ " branches")) 

798 
else (); 

799 
raise exn) 

800 
 backtrack _ = raise PROVE; 

2854  801 

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

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

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

807 
 bad _ = false; 

808 
fun change [] = [] 

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

810 
if G aconv G' then change lits 

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

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

813 
if G aconv G' then change lits 

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

815 
 change (lit::lits) = lit :: change lits 

816 
in 

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

818 
end 

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

820 

821 

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

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

825 

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

826 

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

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

828 
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

829 
fun match (Var _) u = true 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

830 
 match (Const"*Goal*") (Const"Not") = true 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

831 
 match (Const"Not") (Const"*Goal*") = true 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

832 
 match (Const a) (Const b) = (a=b) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

833 
 match (OConst ai) (OConst bj) = (ai=bj) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

834 
 match (Free a) (Free b) = (a=b) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

835 
 match (Bound i) (Bound j) = (i=j) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

836 
 match (Abs(_,t)) (Abs(_,u)) = match t u 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

837 
 match (f$t) (g$u) = match f g andalso match t u 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

838 
 match t u = false; 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

839 

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

840 

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

843 
bound on unsafe expansions.*) 

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

847 
and hazList = [haz_netpair] 

3083  848 
fun prv (tacs, trs, choices, []) = cont (tacs, trs, choices) 
2854  849 
 prv (tacs, trs, choices, 
2894  850 
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = 
2854  851 
let exception PRV (*backtrack to precisely this recursion!*) 
852 
val ntrl = !ntrail 

853 
val nbrs = length brs0 

854 
val nxtVars = nextVars brs 

855 
val G = norm G 

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

856 
val rules = netMkRules G vars safeList 
2854  857 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  858 
fun newBr (vars',lim') prems = 
859 
map (fn prem => 

860 
if (exists isGoal prem) 

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

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

863 
map negOfGoal lits, 

864 
vars', lim') 

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

866 
lits, vars', lim')) 

2854  867 
prems @ 
868 
brs 

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

870 
to branch.*) 

871 
fun deeper [] = raise NEWBRANCHES 

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

3083  873 
if unify(false, add_term_vars(P,[]), P, G) 
874 
then (*P comes from the rule; G comes from the branch.*) 

875 
let val ntrl' = !ntrail 

876 
val lim' = if ntrl < !ntrail 

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

878 
else lim (*discourage branching updates*) 

879 
val vars = vars_in_vars vars 

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

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

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

883 
(*no duplication*) 

884 
in 

3092  885 
traceNew prems; traceVars ntrl; 
3083  886 
(if null prems then (*closed the branch: prune!*) 
887 
prv(tacs', brs0::trs, 

888 
prune (nbrs, nxtVars, choices'), 

889 
brs) 

890 
else 

891 
if lim'<0 (*faster to kill ALL the alternatives*) 

892 
then raise NEWBRANCHES 

893 
else 

894 
prv(tacs', brs0::trs, choices', 

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

896 
handle PRV => 

897 
if ntrl < ntrl' (*Vars have been updated*) 

898 
then 

899 
(*Backtrack at this level. 

900 
Reset Vars and try another rule*) 

901 
(clearTo ntrl; deeper grls) 

902 
else (*backtrack to previous level*) 

903 
backtrack choices 

904 
end 

905 
else deeper grls 

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

908 
 closeF (L::Ls) = 

3083  909 
case tryClose(G,L) of 
910 
None => closeF Ls 

911 
 Some tac => 

912 
let val choices' = 

3092  913 
(if !trace then (prs"branch closed"; 
914 
traceVars ntrl) 

3083  915 
else (); 
916 
prune (nbrs, nxtVars, 

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

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

919 
handle PRV => 

920 
(*reset Vars and try another literal 

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

922 
(clearTo ntrl; closeF Ls) 

923 
end 

2894  924 
fun closeFl [] = raise CLOSEF 
925 
 closeFl ((br, haz)::pairs) = 

926 
closeF (map fst br) 

927 
handle CLOSEF => closeF (map fst haz) 

928 
handle CLOSEF => closeFl pairs 

3083  929 
in tracing sign brs0; 
2854  930 
if lim<0 then backtrack choices 
931 
else 

3092  932 
prv ((TRY o Data.vars_gen_hyp_subst_tac false) :: tacs, 
933 
(*The TRY above allows the substitution to fail, e.g. if 

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

935 
still succeed!*) 

2854  936 
brs0::trs, choices, 
3092  937 
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
2854  938 
handle DEST_EQ => closeF lits 
2894  939 
handle CLOSEF => closeFl ((br,haz)::pairs) 
2854  940 
handle CLOSEF => 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

941 
deeper rules 
2894  942 
handle NEWBRANCHES => 
943 
(case netMkRules G vars hazList of 

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

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

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

947 
::brs) 

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

949 
prv (if isGoal G then negOfGoal_tac :: tacs 

950 
else tacs, 

951 
brs0::trs, choices, 

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

953 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

966 
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

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

968 
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

969 
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

970 
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

971 
in (if recur then [(Gs',Hs')] else [(Gs',[]), ([],Hs')], 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

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

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

976 
to branch.*) 

977 
fun deeper [] = raise NEWBRANCHES 

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

3083  979 
if unify(false, add_term_vars(P,[]), P, H) 
980 
then 

981 
let val ntrl' = !ntrail 

982 
val vars = vars_in_vars vars 

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

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

985 
val dup = md andalso vars' <> vars 

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

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

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

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

990 
else lim1 

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

992 
both dup and recur are false. Proofs are 

993 
found at shallower depths, but looping 

994 
occurs too often...*) 

995 
val mayUndo = not(null grls) (*other rules to try?*) 

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

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

998 
val tac' = if mayUndo then tac dup 

999 
else DETERM o (tac dup) 

1000 
in 

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

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

1003 
raise NEWBRANCHES 

1004 
else 

3092  1005 
traceNew prems; traceVars ntrl; 
3083  1006 
prv(tac dup :: tacs, 
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

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

1008 
call rotate_tac: new formulae should be last*) 
3083  1009 
brs0::trs, 
1010 
(ntrl, length brs0, PRV) :: choices, 

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

1012 
handle PRV => 

1013 
if mayUndo 

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

1015 
(clearTo ntrl; deeper grls) 

1016 
else (*backtrack to previous level*) 

1017 
backtrack choices 

1018 
end 

1019 
else deeper grls 

1020 
in tracing sign brs0; 

2854  1021 
if lim<1 then backtrack choices 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1022 
else deeper rules 
2854  1023 
handle NEWBRANCHES => 
2894  1024 
(*cannot close branch: move H to literals*) 
2854  1025 
prv (tacs, brs0::trs, choices, 
2894  1026 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1027 
end 
1028 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

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

1030 

1031 

2883  1032 
(*Construct an initial branch.*) 
2854  1033 
fun initBranch (ts,lim) = 
2894  1034 
([(map (fn t => (t,true)) ts, [])], 
1035 
[], add_terms_vars (ts,[]), lim); 

2854  1036 

1037 

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

1039 

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

1041 
local open Term 

1042 
in 

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

1044 
 discard_foralls t = t; 

1045 
end; 

1046 

1047 

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

1049 
fun getVars [] i = [] 

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

1051 
if i mem is then getVars alist i 

1052 
else v :: getVars alist i; 

1053 

1054 

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

1056 
fun fromSubgoal tsig t = 

1057 
let val alist = ref [] 

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

1059 
fun from lev t = 

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

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

1062 
fun bounds [] = [] 

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

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

1065 
else ilev :: bounds ts 

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

1067 
in 

1068 
case ht of 

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

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

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

1072 
 Term.Var (ix,_) => 

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

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

1075 
:: !alist; 

1076 
Var (hdvar(!alist))) 

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

1078 
else error("Discrepancy among occurrences of ?" 

1079 
^ Syntax.string_of_vname ix)) 

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

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

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

1083 
end 

1084 

1085 
val npars = length (Logic.strip_params t) 

1086 

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

1088 
fun skoSubgoal i t = 

1089 
if i<npars then 

1090 
skoSubgoal (i+1) 

3092  1091 
(subst_bound (Skolem (gensym "T_", getVars (!alist) i), 
2854  1092 
t)) 
1093 
else t 

1094 

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

1096 

1097 

1098 
(*Tactic using tableau engine and proof reconstruction. 

1099 
"lim" is depth limit.*) 

1100 
fun depth_tac cs lim i st = 

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

3030  1102 
let val {sign,...} = rep_thm st 
1103 
val {tsig,...} = Sign.rep_sg sign 

2854  1104 
val skoprem = fromSubgoal tsig (List.nth(prems_of st, i1)) 
1105 
val hyps = strip_imp_prems skoprem 

1106 
and concl = strip_imp_concl skoprem 

3083  1107 
fun cont (tacs,_,choices) = 
2854  1108 
(case Sequence.pull(EVERY' (rev tacs) i st) of 
1109 
None => (writeln ("PROOF FAILED for depth " ^ 

1110 
Int.toString lim); 

1111 
backtrack choices) 

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

3030  1113 
in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
2854  1114 
end 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3244
diff
changeset

1115 
handle PROVE => Sequence.null); 
2854  1116 

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

1118 

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

1120 

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

1121 

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

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

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

1124 

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

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

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

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

1128 
let val st = topthm() 
3030  1129 
val {sign,...} = rep_thm st 
1130 
val {tsig,...} = Sign.rep_sg sign 

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

1131 
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

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

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

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

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

1137 
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

1138 

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

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

1140 

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

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

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

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

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

1145 

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

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

1147 
(fullTrace:=[]; trail := []; ntrail := 0; 
3030  1148 
timeap prove (sign_of thy, 
1149 
!Data.claset, 

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

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

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

1152 

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

1153 

2854  1154 
end; 
1155 