author  paulson 
Wed, 30 Apr 1997 12:59:24 +0200  
changeset 3083  1a7edbd7f55a 
parent 3049  79c1ba7effb2 
child 3092  b92a1b50b16b 
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: 

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

23 
"Recursive" rules such as transitivity can exclude other unsafe formulae 
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 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

25 
have priority over existing ones. 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

26 

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

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

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

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

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

34 
type ... set) 

35 

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

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

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

39 
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

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

41 
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

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

45 

46 
(*Should be a type abbreviation?*) 

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

48 

49 

50 
(*Assumptions about constants: 

51 
The negation symbol is "Not" 

52 
The equality symbol is "op =" 

53 
The istrue judgement symbol is "Trueprop" 

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

55 
*) 

56 
signature BLAST_DATA = 

57 
sig 

58 
type claset 

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

60 
val ccontr : thm 

61 
val contr_tac : int > tactic 

62 
val dup_intr : thm > thm 

63 
val vars_gen_hyp_subst_tac : bool > int > tactic 

64 
val claset : claset ref 

65 
val rep_claset : 

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

67 
hazIs: thm list, hazEs: thm list, 

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

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

70 
safe0_netpair: netpair, safep_netpair: netpair, 

71 
haz_netpair: netpair, dup_netpair: netpair} 

72 
end; 

73 

74 

75 
signature BLAST = 

76 
sig 

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

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

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

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

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

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

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

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

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

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

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

90 
val Blast_tac : int > tactic 

91 
val declConsts : string list * thm list > unit 

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

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

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

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

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

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

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

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

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

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

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

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

108 

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

109 
functor BlastFun(Data: BLAST_DATA)(**********: BLAST*******) = 
2854  110 
struct 
111 

112 
type claset = Data.claset; 

113 

114 
val trace = ref false; 

115 

116 
datatype term = 

117 
Const of string 

118 
 OConst of string * int 

119 
 Skolem of string * term option ref list 

120 
 Free of string 

121 
 Var of term option ref 

122 
 Bound of int 

123 
 Abs of string*term 

124 
 op $ of term*term; 

125 

126 

127 
exception DEST_EQ; 

128 

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

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

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

132 
 dest_eq _ = raise DEST_EQ; 

133 

134 
(** Basic syntactic operations **) 

135 

136 
fun is_Var (Var _) = true 

137 
 is_Var _ = false; 

138 

139 
fun dest_Var (Var x) = x; 

140 

141 

142 
fun rand (f$x) = x; 

143 

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

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

146 

147 

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

149 
fun strip_comb u : term * term list = 

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

151 
 stripc x = x 

152 
in stripc(u,[]) end; 

153 

154 

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

156 
fun head_of (f$t) = head_of f 

157 
 head_of u = u; 

158 

159 

160 
(** Particular constants **) 

161 

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

163 

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

165 

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

167 
 isGoal _ = false; 

168 

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

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

171 

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

173 
 isTrueprop _ = false; 

174 

175 

176 
(** Dealing with overloaded constants **) 

177 

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

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

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

181 
*) 

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

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

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

185 
 Some patList => 

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

187 
None => Symtab.update 

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

189 
tab) 

190 
 _ => tab)) 

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

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

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

194 

195 

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

197 

2883  198 
fun declConst (a,tab) = 
199 
case Symtab.lookup (tab,a) of 

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

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

2854  202 

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

204 
which may be polymorphic.*) 

205 
local 

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

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

208 
in 

209 

210 
fun declConsts (names, rls) = 

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

212 

213 

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

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

216 
let fun find [] = Const a 

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

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

219 
else find patList 

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

221 
None => Const a 

222 
 Some patList => find patList 

223 
end; 

224 
end; 

225 

226 

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

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

229 
 (OConst ai) aconv (OConst bj) = ai=bj 

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

231 
 (Free a) aconv (Free b) = a=b 

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

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

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

235 
 (Bound i) aconv (Bound j) = i=j 

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

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

238 
 _ aconv _ = false; 

239 

240 

241 
fun mem_term (_, []) = false 

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

243 

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

245 

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

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

248 

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

250 

251 

252 
(** Vars **) 

253 

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

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

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

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

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

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

260 
 add_term_vars (_, vars) = vars 

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

262 
and add_terms_vars ([], vars) = vars 

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

264 
(*Var list version.*) 

265 
and add_vars_vars ([], vars) = vars 

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

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

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

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

270 

271 

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

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

274 

275 

276 

277 
(*increment a term's nonlocal bound variables 

278 
inc is increment for bound variables 

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

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

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

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

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

284 

285 
fun incr_boundvars 0 t = t 

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

287 

288 

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

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

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

292 
else (ilev) ins_int js 

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

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

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

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

297 

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

299 

300 
fun subst_bound (arg, t) : term = 

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

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

303 
else if i=lev then incr_boundvars lev arg 

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

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

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

307 
 subst (t,lev) = t 

308 
in subst (t,0) end; 

309 

310 

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

312 
fun norm t = case t of 

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

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

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

318 
 nf => nf $ norm u) 

319 
 _ => t; 

320 

321 

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

323 
fun wkNormAux t = case t of 

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

325 
Some u => wkNorm u 

326 
 None => t) 

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

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

329 
 nf => nf $ u) 

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

332 
nb as (f $ t) => 

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

334 
then Abs(a,nb) 

335 
else wkNorm (incr_boundvars ~1 f) 

336 
 nb => Abs (a,nb)) 

2854  337 
 _ => t 
338 
and wkNorm t = case head_of t of 

339 
Const _ => t 

340 
 OConst _ => t 

341 
 Skolem(a,args) => t 

342 
 Free _ => t 

343 
 _ => wkNormAux t; 

344 

345 

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

347 
fun varOccur v = 

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

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

350 
and occ (Var w) = 

351 
v=w orelse 

352 
(case !w of None => false 

353 
 Some u => occ u) 

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

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

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

357 
 occ (_) = false; 

358 
in occ end; 

359 

360 
exception UNIFY; 

361 

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

363 
val ntrail = ref 0; 

364 

365 

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

367 
fun clearTo n = 

3083  368 
while !ntrail<>n do 
2854  369 
(hd(!trail) := None; 
370 
trail := tl (!trail); 

371 
ntrail := !ntrail  1); 

372 

373 

374 
(*Firstorder unification with bound variables. 

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

376 
on the trail (no point in doing so) 

377 
*) 

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

378 
fun unify(allowClash,vars,t,u) = 
2854  379 
let val n = !ntrail 
380 
fun update (t as Var v, u) = 

381 
if t aconv u then () 

382 
else if varOccur v u then raise UNIFY 

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

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

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

386 
then dest_Var u := Some t 

387 
else (v := Some u; 

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

389 
fun unifyAux (t,u) = 

390 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

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

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

3083  401 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  402 
end; 
403 

404 

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

406 
fun fromTerm tsig t = 

407 
let val alist = ref [] 

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

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

410 
 from (Term.Bound i) = Bound i 

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

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

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

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

415 
end 

416 
 Some (v,_) => v) 

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

418 
(case from u of 

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

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

421 
else incr_boundvars ~1 f 

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

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

424 
in from t end; 

425 

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

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

428 
A :: strip_imp_prems B 

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

430 
 strip_imp_prems _ = []; 

431 

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

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

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

435 
 strip_imp_concl A = A : term; 

436 

437 

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

439 

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

441 
fun squash_nots [] = [] 

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

443 
squash_nots Ps 

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

445 
squash_nots Ps 

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

447 

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

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

450 
 skoPrem vars P = P; 

451 

452 
fun convertPrem t = 

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

454 

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

456 
fun convertRule vars t = 

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

458 
val Var v = strip_imp_concl t 

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

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

461 
end; 

462 

463 

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

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

466 

467 

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

469 
fun nNewHyps [] = 0 

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

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

472 

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

474 
 rot_subgoals_tac (k::ks) i st = 

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

476 
handle OPTION _ => Sequence.null; 

477 

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

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

3083  480 
local open General in (*make available the Basis type "option"*) 
481 

2854  482 
(*Tableau rule from elimination rule. Flag "dup" requests duplication of the 
483 
affected formula.*) 

484 
fun fromRule vars rl = 

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

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

487 
fun tac dup i = 

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

488 
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i 
2854  489 
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i 
490 

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

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

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

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

495 
else (); 
3049  496 
NONE); 
3083  497 
end; 
2854  498 

499 

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

501 
proof reconstruction) ***) 

502 

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

504 

505 
fun convertIntrRule vars t = 

506 
let val Ps = strip_imp_prems t 

507 
val P = strip_imp_concl t 

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

509 
end; 

510 

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

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

513 
fun fromIntrRule vars rl = 

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

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

516 
fun tac dup i = 

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

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

520 

521 

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

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

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

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

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

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

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

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

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

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

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

534 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  535 

536 

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

538 
case P of 

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

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

540 
let val pG = mk_tprop (toTerm 2 G) 
2854  541 
val intrs = List.concat 
542 
(map (fn (inet,_) => Net.unify_term inet pG) 

543 
nps) 

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

545 
 _ => 

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

546 
let val pP = mk_tprop (toTerm 3 P) 
2854  547 
val elims = List.concat 
548 
(map (fn (_,enet) => Net.unify_term enet pP) 

549 
nps) 

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

551 

552 
(** 

553 
end; 

554 
**) 

555 

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

557 

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

559 
fun subst_atomic (old,new) t = 

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

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

562 
 subst (f$t) = subst f $ subst t 

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

564 
in subst t end; 

565 

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

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

568 
(case eta_contract2 body of 

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

570 
else eta_contract_atom (incr_boundvars ~1 f) 

571 
 _ => t0) 

572 
 eta_contract_atom t = t 

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

574 
 eta_contract2 t = eta_contract_atom t; 

575 

576 

577 
(*When can we safely delete the equality? 

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

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

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

581 
Prefer to eliminate Bound variables if possible. 

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

583 

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

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

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

587 
fun substOccur t = 

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

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

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

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

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

593 
 occ (_) = false; 

594 
in occEq end; 

595 

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

597 

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

599 
THEN orient that equality ELSE raise exception DEST_EQ*) 

600 
fun orientGoal (t,u) = 

601 
case (eta_contract_atom t, eta_contract_atom u) of 

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

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

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

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

606 
 _ => raise DEST_EQ; 

607 

608 

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

609 

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

610 

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

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

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

2854  615 
let val subst = subst_atomic (orientGoal(dest_eq G)) 
616 
fun subst2(G,md) = (subst G, md) 

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

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

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

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

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

621 
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

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

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

624 
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

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

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

2854  629 
let val nlit = subst lit 
2894  630 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
631 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  632 
end 
3083  633 
in if !trace then writeln "substitution in branch" else (); 
634 
subLits (rev lits, [], []) 

2854  635 
end; 
636 

637 

638 
exception NEWBRANCHES and CLOSEF; 

639 

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

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

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

645 
int; (*resource limit*) 

646 

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

648 

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

649 
(*Normalize a branchfor tracing*) 
3083  650 
fun norm2 (G,md) = (norm G, md); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

651 

3083  652 
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); 
2924
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 
fun normBr (br, lits, vars, lim) = 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

656 

3030  657 

3083  658 
val dummyVar2 = Term.Var(("var",0), dummyT); 
659 

3030  660 
(*Convert from prototerms to ordinary terms with dummy types for tracing*) 
3083  661 
fun showTerm d (Const a) = Term.Const (a,dummyT) 
3030  662 
 showTerm d (OConst(a,_)) = Term.Const (a,dummyT) 
663 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 

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

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

3083  666 
 showTerm d (Var _) = dummyVar2 
667 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 

668 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

3030  671 

672 

3083  673 
(*Print tracing information at each iteration of prover*) 
3030  674 
fun tracing sign brs = 
3083  675 
let fun pr t = prs (Sign.string_of_term sign (showTerm 8 t)) 
3030  676 
fun printPairs (((G,_)::_,_)::_) = pr G 
3083  677 
 printPairs (([],(H,_)::_)::_) = (pr H; prs"\t (Unsafe)") 
3030  678 
 printPairs _ = () 
679 
fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) = 

680 
(fullTrace := brs0 :: !fullTrace; 

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

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

683 
printPairs pairs; 

684 
writeln"") 

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

686 
end; 

687 

3083  688 
fun traceNew prems = 
689 
if !trace then 

690 
case length prems of 

691 
0 => writeln"branch closed by rule" 

692 
 1 => writeln"branch extended (1 new subgoal)" 

693 
 n => writeln("branch split: "^ Int.toString n ^ 

694 
" new subgoals") 

695 
else (); 

696 

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

697 

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

698 

2854  699 
exception PROVE; 
700 

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

702 

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

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

705 

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

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

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

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

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

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

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

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

715 
 tryClose _ = None; 

2854  716 

717 

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

719 
fun hasSkolem (Skolem _) = true 

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

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

722 
 hasSkolem _ = false; 

723 

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

725 
Skolem terms then allow duplication.*) 

726 
fun joinMd md [] = [] 

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

728 

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

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

732 
 negOfGoal G = G; 

733 

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

735 

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

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

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

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

740 

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

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

743 

2854  744 

745 
(** Backtracking and Pruning **) 

746 

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

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

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

750 
 clashVar vars = 

751 
let fun clash (0, _) = false 

752 
 clash (_, []) = false 

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

754 
in clash end; 

755 

756 

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

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

759 
next branch have been updated.*) 

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

761 
backtracking over bad proofs*) 

762 
 prune (nbrs, nxtVars, choices) = 

763 
let fun traceIt last = 

764 
let val ll = length last 

765 
and lc = length choices 

766 
in if !trace andalso ll<lc then 

3083  767 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  768 
last) 
769 
else last 

770 
end 

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

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

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

776 
else (* nbrs'=nbrs *) 

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

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

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

780 
choices) 

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

782 

2894  783 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  784 
 nextVars [] = []; 
2854  785 

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

788 
Int.toString nbrs ^ " branches")) 

789 
else (); 

790 
raise exn) 

791 
 backtrack _ = raise PROVE; 

2854  792 

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

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

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

798 
 bad _ = false; 

799 
fun change [] = [] 

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

801 
if G aconv G' then change lits 

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

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

804 
if G aconv G' then change lits 

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

806 
 change (lit::lits) = lit :: change lits 

807 
in 

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

809 
end 

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

811 

812 

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

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

816 

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

817 

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

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

819 
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

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

821 
 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

822 
 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

823 
 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

824 
 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

825 
 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

826 
 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

827 
 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

828 
 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

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

830 

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

831 

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

834 
bound on unsafe expansions.*) 

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

838 
and hazList = [haz_netpair] 

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

844 
val nbrs = length brs0 

845 
val nxtVars = nextVars brs 

846 
val G = norm G 

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

847 
val rules = netMkRules G vars safeList 
2854  848 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  849 
fun newBr (vars',lim') prems = 
850 
map (fn prem => 

851 
if (exists isGoal prem) 

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

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

854 
map negOfGoal lits, 

855 
vars', lim') 

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

857 
lits, vars', lim')) 

2854  858 
prems @ 
859 
brs 

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

861 
to branch.*) 

862 
fun deeper [] = raise NEWBRANCHES 

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

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

866 
let val ntrl' = !ntrail 

867 
val lim' = if ntrl < !ntrail 

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

869 
else lim (*discourage branching updates*) 

870 
val vars = vars_in_vars vars 

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

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

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

874 
(*no duplication*) 

875 
in 

876 
traceNew prems; 

877 
(if null prems then (*closed the branch: prune!*) 

878 
prv(tacs', brs0::trs, 

879 
prune (nbrs, nxtVars, choices'), 

880 
brs) 

881 
else 

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

883 
then raise NEWBRANCHES 

884 
else 

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

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

887 
handle PRV => 

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

889 
then 

890 
(*Backtrack at this level. 

891 
Reset Vars and try another rule*) 

892 
(clearTo ntrl; deeper grls) 

893 
else (*backtrack to previous level*) 

894 
backtrack choices 

895 
end 

896 
else deeper grls 

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

899 
 closeF (L::Ls) = 

3083  900 
case tryClose(G,L) of 
901 
None => closeF Ls 

902 
 Some tac => 

903 
let val choices' = 

904 
(if !trace then writeln"branch closed" 

905 
else (); 

906 
prune (nbrs, nxtVars, 

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

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

909 
handle PRV => 

910 
(*reset Vars and try another literal 

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

912 
(clearTo ntrl; closeF Ls) 

913 
end 

2894  914 
fun closeFl [] = raise CLOSEF 
915 
 closeFl ((br, haz)::pairs) = 

916 
closeF (map fst br) 

917 
handle CLOSEF => closeF (map fst haz) 

918 
handle CLOSEF => closeFl pairs 

3083  919 
in tracing sign brs0; 
2854  920 
if lim<0 then backtrack choices 
921 
else 

922 
prv (Data.vars_gen_hyp_subst_tac false :: tacs, 

923 
brs0::trs, choices, 

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

928 
deeper rules 
2894  929 
handle NEWBRANCHES => 
930 
(case netMkRules G vars hazList of 

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

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

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

934 
::brs) 

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

936 
prv (if isGoal G then negOfGoal_tac :: tacs 

937 
else tacs, 

938 
brs0::trs, choices, 

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

940 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

953 
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

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

955 
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

956 
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

957 
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

958 
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

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

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

963 
to branch.*) 

964 
fun deeper [] = raise NEWBRANCHES 

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

3083  966 
if unify(false, add_term_vars(P,[]), P, H) 
967 
then 

968 
let val ntrl' = !ntrail 

969 
val vars = vars_in_vars vars 

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

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

972 
val dup = md andalso vars' <> vars 

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

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

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

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

977 
else lim1 

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

979 
both dup and recur are false. Proofs are 

980 
found at shallower depths, but looping 

981 
occurs too often...*) 

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

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

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

985 
val tac' = if mayUndo then tac dup 

986 
else DETERM o (tac dup) 

987 
in 

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

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

990 
raise NEWBRANCHES 

991 
else 

992 
traceNew prems; 

993 
prv(tac dup :: tacs, 

994 
brs0::trs, 

995 
(ntrl, length brs0, PRV) :: choices, 

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

997 
handle PRV => 

998 
if mayUndo 

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

1000 
(clearTo ntrl; deeper grls) 

1001 
else (*backtrack to previous level*) 

1002 
backtrack choices 

1003 
end 

1004 
else deeper grls 

1005 
in tracing sign brs0; 

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

1007 
else deeper rules 
2854  1008 
handle NEWBRANCHES => 
2894  1009 
(*cannot close branch: move H to literals*) 
2854  1010 
prv (tacs, brs0::trs, choices, 
2894  1011 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1012 
end 
1013 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

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

1015 

1016 

2883  1017 
(*Construct an initial branch.*) 
2854  1018 
fun initBranch (ts,lim) = 
2894  1019 
([(map (fn t => (t,true)) ts, [])], 
1020 
[], add_terms_vars (ts,[]), lim); 

2854  1021 

1022 

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

1024 

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

1026 
local open Term 

1027 
in 

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

1029 
 discard_foralls t = t; 

1030 
end; 

1031 

1032 

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

1034 
fun getVars [] i = [] 

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

1036 
if i mem is then getVars alist i 

1037 
else v :: getVars alist i; 

1038 

1039 

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

1041 
fun fromSubgoal tsig t = 

1042 
let val alist = ref [] 

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

1044 
fun from lev t = 

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

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

1047 
fun bounds [] = [] 

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

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

1050 
else ilev :: bounds ts 

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

1052 
in 

1053 
case ht of 

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

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

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

1057 
 Term.Var (ix,_) => 

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

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

1060 
:: !alist; 

1061 
Var (hdvar(!alist))) 

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

1063 
else error("Discrepancy among occurrences of ?" 

1064 
^ Syntax.string_of_vname ix)) 

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

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

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

1068 
end 

1069 

1070 
val npars = length (Logic.strip_params t) 

1071 

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

1073 
fun skoSubgoal i t = 

1074 
if i<npars then 

1075 
skoSubgoal (i+1) 

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

1077 
t)) 

1078 
else t 

1079 

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

1081 

1082 

1083 
(*Tactic using tableau engine and proof reconstruction. 

1084 
"lim" is depth limit.*) 

1085 
fun depth_tac cs lim i st = 

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

3030  1087 
let val {sign,...} = rep_thm st 
1088 
val {tsig,...} = Sign.rep_sg sign 

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

1091 
and concl = strip_imp_concl skoprem 

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

1095 
Int.toString lim); 

1096 
backtrack choices) 

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

3030  1098 
in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
2854  1099 
end 
1100 
handle Subscript => Sequence.null 

1101 
 PROVE => Sequence.null); 

1102 

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

1104 

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

1106 

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

1107 

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

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

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

1110 

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

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

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

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

1114 
let val st = topthm() 
3030  1115 
val {sign,...} = rep_thm st 
1116 
val {tsig,...} = Sign.rep_sg sign 

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

1117 
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

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

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

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

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

1123 
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

1124 

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

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

1126 

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

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

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

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

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

1131 

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

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

1133 
(fullTrace:=[]; trail := []; ntrail := 0; 
3030  1134 
timeap prove (sign_of thy, 
1135 
!Data.claset, 

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

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

1137 
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 

2854  1140 
end; 
1141 