author  paulson 
Mon, 05 May 1997 12:15:20 +0200  
changeset 3101  e8a92f497295 
parent 3092  b92a1b50b16b 
child 3244  71b760618f30 
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 

3083  472 
local open General in (*make available the Basis type "option"*) 
473 

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

476 
fun fromRule vars rl = 

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

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

479 
fun tac dup i = 

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

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

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

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

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

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

487 
else (); 
3049  488 
NONE); 
3083  489 
end; 
2854  490 

491 

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

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

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

495 

496 
fun convertIntrRule vars t = 

497 
let val Ps = strip_imp_prems t 

498 
val P = strip_imp_concl t 

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

500 
end; 

501 

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

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

504 
fun fromIntrRule vars rl = 

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

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

507 
fun tac dup i = 

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

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

511 

512 

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

515 
(*Convert from prototerms to ordinary terms with dummy types 

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

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

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

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

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

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

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

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

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

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

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

527 

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

529 
case P of 

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

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

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

534 
nps) 

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

536 
 _ => 

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

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

540 
nps) 

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

542 

543 
(** 

544 
end; 

545 
**) 

546 

3092  547 

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

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

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

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

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

553 
int; (*resource limit*) 

554 

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

556 

557 
(*Normalize a branchfor tracing*) 

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

559 

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

561 

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

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

564 

565 

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

567 

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

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

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

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

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

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

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

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

575 
 showTerm d (Var(ref None)) = dummyVar2 
3092  576 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
577 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

580 

581 

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

583 

584 

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

586 
fun tracing sign brs = 

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

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

589 
 printPairs _ = () 

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

591 
(fullTrace := brs0 :: !fullTrace; 

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

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

594 
printPairs pairs; 

595 
writeln"") 

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

597 
end; 

598 

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

600 
fun traceVars ntrl = 

601 
if !trace then 

602 
(case !ntrailntrl of 

603 
0 => writeln"" 

604 
 1 => writeln"\t1 variable updated" 

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

606 
else (); 

607 

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

609 
fun traceNew prems = 

610 
if !trace then 

611 
case length prems of 

612 
0 => prs"branch closed by rule" 

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

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

615 
else (); 

616 

617 

618 

2854  619 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
620 

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

622 
fun subst_atomic (old,new) t = 

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

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

625 
 subst (f$t) = subst f $ subst t 

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

627 
in subst t end; 

628 

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

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

631 
(case eta_contract2 body of 

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

633 
else eta_contract_atom (incr_boundvars ~1 f) 

634 
 _ => t0) 

635 
 eta_contract_atom t = t 

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

637 
 eta_contract2 t = eta_contract_atom t; 

638 

639 

640 
(*When can we safely delete the equality? 

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

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

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

644 
Prefer to eliminate Bound variables if possible. 

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

646 

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

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

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

650 
fun substOccur t = 

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

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

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

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

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

656 
 occ (_) = false; 

657 
in occEq end; 

658 

3092  659 
exception DEST_EQ; 
660 

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

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

663 
(eta_contract_atom t, eta_contract_atom u) 

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

665 
(eta_contract_atom t, eta_contract_atom u) 

666 
 dest_eq _ = raise DEST_EQ; 

667 

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

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

671 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  672 
fun orientGoal (t,u) = case (t,u) of 
2854  673 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
674 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

677 
 _ => raise DEST_EQ; 

678 

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

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

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

684 
val subst = subst_atomic (t,u) 

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

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

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

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

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

690 
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

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

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

693 
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

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

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

2854  698 
let val nlit = subst lit 
2894  699 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
700 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  701 
end 
3092  702 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
703 
" for " ^ traceTerm sign t ^ " in branch" ) 

704 
else (); 

3083  705 
subLits (rev lits, [], []) 
2854  706 
end; 
707 

708 

709 
exception NEWBRANCHES and CLOSEF; 

710 

711 
exception PROVE; 

712 

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

714 

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

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

717 

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

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

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

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

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

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

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

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

727 
 tryClose _ = None; 

2854  728 

729 

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

731 
fun hasSkolem (Skolem _) = true 

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

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

734 
 hasSkolem _ = false; 

735 

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

737 
Skolem terms then allow duplication.*) 

738 
fun joinMd md [] = [] 

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

740 

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

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

744 
 negOfGoal G = G; 

745 

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

747 

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

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

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

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

752 

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

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

755 

2854  756 

757 
(** Backtracking and Pruning **) 

758 

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

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

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

762 
 clashVar vars = 

763 
let fun clash (0, _) = false 

764 
 clash (_, []) = false 

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

766 
in clash end; 

767 

768 

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

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

771 
next branch have been updated.*) 

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

773 
backtracking over bad proofs*) 

774 
 prune (nbrs, nxtVars, choices) = 

775 
let fun traceIt last = 

776 
let val ll = length last 

777 
and lc = length choices 

778 
in if !trace andalso ll<lc then 

3083  779 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  780 
last) 
781 
else last 

782 
end 

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

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

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

788 
else (* nbrs'=nbrs *) 

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

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

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

792 
choices) 

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

794 

2894  795 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  796 
 nextVars [] = []; 
2854  797 

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

800 
Int.toString nbrs ^ " branches")) 

801 
else (); 

802 
raise exn) 

803 
 backtrack _ = raise PROVE; 

2854  804 

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

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

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

810 
 bad _ = false; 

811 
fun change [] = [] 

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

813 
if G aconv G' then change lits 

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

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

816 
if G aconv G' then change lits 

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

818 
 change (lit::lits) = lit :: change lits 

819 
in 

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

821 
end 

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

823 

824 

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

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

828 

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

829 

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

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

831 
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

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

833 
 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

834 
 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

835 
 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

836 
 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

837 
 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

838 
 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

839 
 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

840 
 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

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

842 

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

843 

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

846 
bound on unsafe expansions.*) 

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

850 
and hazList = [haz_netpair] 

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

856 
val nbrs = length brs0 

857 
val nxtVars = nextVars brs 

858 
val G = norm G 

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

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

863 
if (exists isGoal prem) 

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

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

866 
map negOfGoal lits, 

867 
vars', lim') 

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

869 
lits, vars', lim')) 

2854  870 
prems @ 
871 
brs 

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

873 
to branch.*) 

874 
fun deeper [] = raise NEWBRANCHES 

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

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

878 
let val ntrl' = !ntrail 

879 
val lim' = if ntrl < !ntrail 

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

881 
else lim (*discourage branching updates*) 

882 
val vars = vars_in_vars vars 

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

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

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

886 
(*no duplication*) 

887 
in 

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

891 
prune (nbrs, nxtVars, choices'), 

892 
brs) 

893 
else 

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

895 
then raise NEWBRANCHES 

896 
else 

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

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

899 
handle PRV => 

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

901 
then 

902 
(*Backtrack at this level. 

903 
Reset Vars and try another rule*) 

904 
(clearTo ntrl; deeper grls) 

905 
else (*backtrack to previous level*) 

906 
backtrack choices 

907 
end 

908 
else deeper grls 

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

911 
 closeF (L::Ls) = 

3083  912 
case tryClose(G,L) of 
913 
None => closeF Ls 

914 
 Some tac => 

915 
let val choices' = 

3092  916 
(if !trace then (prs"branch closed"; 
917 
traceVars ntrl) 

3083  918 
else (); 
919 
prune (nbrs, nxtVars, 

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

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

922 
handle PRV => 

923 
(*reset Vars and try another literal 

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

925 
(clearTo ntrl; closeF Ls) 

926 
end 

2894  927 
fun closeFl [] = raise CLOSEF 
928 
 closeFl ((br, haz)::pairs) = 

929 
closeF (map fst br) 

930 
handle CLOSEF => closeF (map fst haz) 

931 
handle CLOSEF => closeFl pairs 

3083  932 
in tracing sign brs0; 
2854  933 
if lim<0 then backtrack choices 
934 
else 

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

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

938 
still succeed!*) 

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

944 
deeper rules 
2894  945 
handle NEWBRANCHES => 
946 
(case netMkRules G vars hazList of 

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

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

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

950 
::brs) 

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

952 
prv (if isGoal G then negOfGoal_tac :: tacs 

953 
else tacs, 

954 
brs0::trs, choices, 

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

956 
lits, vars, lim) :: brs)) 

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

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

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

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

969 
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

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

971 
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

972 
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

973 
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

974 
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

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

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

979 
to branch.*) 

980 
fun deeper [] = raise NEWBRANCHES 

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

3083  982 
if unify(false, add_term_vars(P,[]), P, H) 
983 
then 

984 
let val ntrl' = !ntrail 

985 
val vars = vars_in_vars vars 

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

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

988 
val dup = md andalso vars' <> vars 

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

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

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

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

993 
else lim1 

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

995 
both dup and recur are false. Proofs are 

996 
found at shallower depths, but looping 

997 
occurs too often...*) 

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

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

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

1001 
val tac' = if mayUndo then tac dup 

1002 
else DETERM o (tac dup) 

1003 
in 

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

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

1006 
raise NEWBRANCHES 

1007 
else 

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

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

1011 
call rotate_tac: new formulae should be last*) 
3083  1012 
brs0::trs, 
1013 
(ntrl, length brs0, PRV) :: choices, 

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

1015 
handle PRV => 

1016 
if mayUndo 

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

1018 
(clearTo ntrl; deeper grls) 

1019 
else (*backtrack to previous level*) 

1020 
backtrack choices 

1021 
end 

1022 
else deeper grls 

1023 
in tracing sign brs0; 

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

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

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

1033 

1034 

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

2854  1039 

1040 

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

1042 

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

1044 
local open Term 

1045 
in 

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

1047 
 discard_foralls t = t; 

1048 
end; 

1049 

1050 

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

1052 
fun getVars [] i = [] 

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

1054 
if i mem is then getVars alist i 

1055 
else v :: getVars alist i; 

1056 

1057 

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

1059 
fun fromSubgoal tsig t = 

1060 
let val alist = ref [] 

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

1062 
fun from lev t = 

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

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

1065 
fun bounds [] = [] 

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

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

1068 
else ilev :: bounds ts 

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

1070 
in 

1071 
case ht of 

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

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

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

1075 
 Term.Var (ix,_) => 

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

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

1078 
:: !alist; 

1079 
Var (hdvar(!alist))) 

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

1081 
else error("Discrepancy among occurrences of ?" 

1082 
^ Syntax.string_of_vname ix)) 

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

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

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

1086 
end 

1087 

1088 
val npars = length (Logic.strip_params t) 

1089 

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

1091 
fun skoSubgoal i t = 

1092 
if i<npars then 

1093 
skoSubgoal (i+1) 

3092  1094 
(subst_bound (Skolem (gensym "T_", getVars (!alist) i), 
2854  1095 
t)) 
1096 
else t 

1097 

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

1099 

1100 

1101 
(*Tactic using tableau engine and proof reconstruction. 

1102 
"lim" is depth limit.*) 

1103 
fun depth_tac cs lim i st = 

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

3030  1105 
let val {sign,...} = rep_thm st 
1106 
val {tsig,...} = Sign.rep_sg sign 

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

1109 
and concl = strip_imp_concl skoprem 

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

1113 
Int.toString lim); 

1114 
backtrack choices) 

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

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

1119 
 PROVE => Sequence.null); 

1120 

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

1122 

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

1124 

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

1125 

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

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

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

1128 

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

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

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

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

1132 
let val st = topthm() 
3030  1133 
val {sign,...} = rep_thm st 
1134 
val {tsig,...} = Sign.rep_sg sign 

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

1135 
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

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

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

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

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

1141 
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

1142 

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

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

1144 

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

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

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

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

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

1149 

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

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

1151 
(fullTrace:=[]; trail := []; ntrail := 0; 
3030  1152 
timeap prove (sign_of thy, 
1153 
!Data.claset, 

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

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

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

1156 

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

1157 

2854  1158 
end; 
1159 