author  paulson 
Tue, 11 Nov 1997 11:12:37 +0100  
changeset 4196  9953c0995b79 
parent 4149  a6ccec4fd0c3 
child 4233  85d004a96b98 
permissions  rwrr 
4078  1 
(* Title: Provers/blast.ML 
2894  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3083  4 
Copyright 1997 University of Cambridge 
2894  5 

6 
Generic tableau prover with proof reconstruction 

7 

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

11 

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

12 
Blast_tac is often more powerful than fast_tac, but has some limitations. 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

16 
(conclusion must be a formula variable) 

17 
* ignores types, which can make HOL proofs fail 

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

18 
* rules must not require higherorder unification, e.g. apply_type in ZF 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

19 
+ message "Function Var's argument not a bound variable" relates to this 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

20 
* its proof strategy is more general but can actually be slower 
2894  21 

22 
Known problems: 

3092  23 
"Recursive" chains of rules can sometimes exclude other unsafe formulae 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

24 
from expansion. This happens because newlycreated formulae always 
3092  25 
have priority over existing ones. But obviously recursive rules 
26 
such as transitivity are treated specially to prevent this. 

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

27 

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

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

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

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

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

35 
type ... set) 

36 

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

37 
With substition for equalities (hyp_subst_tac): 
3092  38 
When substitution affects a haz formula or literal, it is moved 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

44 

45 
(*Should be a type abbreviation?*) 

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

47 

48 

49 
(*Assumptions about constants: 

50 
The negation symbol is "Not" 

51 
The equality symbol is "op =" 

52 
The istrue judgement symbol is "Trueprop" 

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

54 
*) 

55 
signature BLAST_DATA = 

56 
sig 

57 
type claset 

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

59 
val ccontr : thm 

60 
val contr_tac : int > tactic 

61 
val dup_intr : thm > thm 

62 
val vars_gen_hyp_subst_tac : bool > int > tactic 

4078  63 
val claset : unit > claset 
2854  64 
val rep_claset : 
65 
claset > {safeIs: thm list, safeEs: thm list, 

66 
hazIs: thm list, hazEs: thm list, 

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

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

69 
safe0_netpair: netpair, safep_netpair: netpair, 

70 
haz_netpair: netpair, dup_netpair: netpair} 

71 
end; 

72 

73 

74 
signature BLAST = 

75 
sig 

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

76 
type claset 
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 
4065  79 
 TConst of string * term 
2924
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 

4065  90 
val overload : string * (Term.typ > Term.typ) > 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 
4065  94 
val fromType : (indexname * term) list ref > Term.typ > term 
95 
val fromTerm : Term.term > term 

96 
val fromSubgoal : Term.term > term 

97 
val instVars : term > (unit > unit) 

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

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

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

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

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

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

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

109 

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

113 
type claset = Data.claset; 

114 

115 
val trace = ref false; 

116 

117 
datatype term = 

118 
Const of string 

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

122 
 Var of term option ref 

123 
 Bound of int 

124 
 Abs of string*term 

125 
 op $ of term*term; 

126 

127 

128 
(** Basic syntactic operations **) 

129 

130 
fun is_Var (Var _) = true 

131 
 is_Var _ = false; 

132 

133 
fun dest_Var (Var x) = x; 

134 

135 

136 
fun rand (f$x) = x; 

137 

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

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

140 

141 

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

143 
fun strip_comb u : term * term list = 

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

145 
 stripc x = x 

146 
in stripc(u,[]) end; 

147 

148 

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

150 
fun head_of (f$t) = head_of f 

151 
 head_of u = u; 

152 

153 

154 
(** Particular constants **) 

155 

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

157 

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

159 

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

161 
 isGoal _ = false; 

162 

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

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

165 

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

167 
 isTrueprop _ = false; 

168 

169 

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

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

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

175 
map (fromType alist) Ts) 

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

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

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

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

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

181 
end 

182 
 Some v => v) 

2854  183 

184 
local 

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

4065  188 
fun overload arg = (overloads := arg :: (!overloads)); 
2854  189 

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

192 
fun fromConst alist (a,T) = 

193 
case assoc_string (!overloads, a) of 

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

195 
 Some f => 

196 
let val T' = f T 

197 
handle Match => 

198 
error ("Blast_tac: unexpected type for overloaded constant " ^ a) 

199 
in TConst(a, fromType alist T') end; 

200 

2854  201 
end; 
202 

203 

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

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

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

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

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

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

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

215 
 _ aconv _ = false; 

216 

217 

218 
fun mem_term (_, []) = false 

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

220 

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

222 

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

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

225 

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

227 

228 

229 
(** Vars **) 

230 

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

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

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

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

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

238 
 add_term_vars (_, vars) = vars 

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

240 
and add_terms_vars ([], vars) = vars 

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

242 
(*Var list version.*) 

243 
and add_vars_vars ([], vars) = vars 

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

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

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

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

248 

249 

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

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

252 

253 

254 

255 
(*increment a term's nonlocal bound variables 

256 
inc is increment for bound variables 

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

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

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

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

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

262 

263 
fun incr_boundvars 0 t = t 

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

265 

266 

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

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

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

270 
else (ilev) ins_int js 

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

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

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

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

275 

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

277 

278 
fun subst_bound (arg, t) : term = 

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

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

281 
else if i=lev then incr_boundvars lev arg 

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

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

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

285 
 subst (t,lev) = t 

286 
in subst (t,0) end; 

287 

288 

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

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

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

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

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

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

300 

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

302 
fun wkNormAux t = case t of 

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

304 
Some u => wkNorm u 

305 
 None => t) 

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

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

308 
 nf => nf $ u) 

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

311 
nb as (f $ t) => 

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

313 
then Abs(a,nb) 

314 
else wkNorm (incr_boundvars ~1 f) 

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

318 
Const _ => t 

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

322 
 _ => wkNormAux t; 

323 

324 

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

326 
fun varOccur v = 

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

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

329 
and occ (Var w) = 

330 
v=w orelse 

331 
(case !w of None => false 

332 
 Some u => occ u) 

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

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

337 
 occ (_) = false; 

338 
in occ end; 

339 

340 
exception UNIFY; 

341 

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

343 
val ntrail = ref 0; 

344 

345 

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

347 
fun clearTo n = 

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

351 
ntrail := !ntrail  1); 

352 

353 

354 
(*Firstorder unification with bound variables. 

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

356 
on the trail (no point in doing so) 

357 
*) 

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

361 
if t aconv u then () 

362 
else if varOccur v u then raise UNIFY 

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

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

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

366 
then dest_Var u := Some t 

367 
else (v := Some u; 

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

369 
fun unifyAux (t,u) = 

370 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

382 

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

385 
fun fromTerm t = 

386 
let val alistVar = ref [] 

387 
and alistTVar = ref [] 

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

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

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

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

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

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

401 
else incr_boundvars ~1 f 

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

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

404 
in from t end; 

405 

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

408 
fun instVars t = 

409 
let val name = ref "A" 

410 
val updated = ref [] 

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

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

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

414 
name := bump_string (!name)) 

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

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

417 
 inst _ = () 

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

419 
in inst t; revert end; 

420 

421 

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

424 
A :: strip_imp_prems B 

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

426 
 strip_imp_prems _ = []; 

427 

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

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

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

431 
 strip_imp_concl A = A : term; 

432 

433 

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

435 

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

437 
fun squash_nots [] = [] 

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

439 
squash_nots Ps 

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

441 
squash_nots Ps 

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

443 

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

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

446 
 skoPrem vars P = P; 

447 

448 
fun convertPrem t = 

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

450 

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

452 
fun convertRule vars t = 

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

454 
val Var v = strip_imp_concl t 

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

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

457 
end; 

458 

459 

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

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

462 

463 

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

465 
fun nNewHyps [] = 0 

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

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

468 

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

470 
 rot_subgoals_tac (k::ks) i st = 

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

4149  472 
handle OPTION => Sequence.null; 
2854  473 

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

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

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

477 
affected formula.*) 

478 
fun fromRule vars rl = 

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

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

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

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

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

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

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

489 
Option.NONE); 
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 = 

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

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

510 

511 

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

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

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

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

517 
 toTerm d (Const a) = Term.Const (a,dummyT) 
4065  518 
 toTerm d (TConst(a,_)) = Term.Const (a,dummyT) (*no need to convert type*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

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

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

526 

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

528 
case P of 

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

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

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

533 
nps) 

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

535 
 _ => 

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

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

539 
nps) 

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

541 

542 
(** 

543 
end; 

544 
**) 

545 

3092  546 

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

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

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

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

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

552 
int; (*resource limit*) 

553 

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

555 

556 
(*Normalize a branchfor tracing*) 

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

558 

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

560 

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

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

563 

564 

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

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

570 
 showType (Var _) = dummyTVar 

571 
 showType t = 

572 
(case strip_comb t of 

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

574 
 _ => dummyT); 

575 

576 
(*Display toplevel overloading if any*) 

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

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

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

580 
None => topType u 

581 
 some => some) 

582 
 topType _ = None; 

583 

584 

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

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

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

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

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

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

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

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

597 

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

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

602 
val stm = string_of sign 8 t' 

603 
in 

604 
case topType t' of 

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

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

607 
end; 

3092  608 

609 

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

611 
fun tracing sign brs = 

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

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

614 
 printPairs _ = () 

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

616 
(fullTrace := brs0 :: !fullTrace; 

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

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

619 
printPairs pairs; 

620 
writeln"") 

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

622 
end; 

623 

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

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

629 
(case !ntrailntrl of 

630 
0 => () 

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

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

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

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

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

636 
writeln"") 

3092  637 
else (); 
638 

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

640 
fun traceNew prems = 

641 
if !trace then 

642 
case length prems of 

643 
0 => prs"branch closed by rule" 

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

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

646 
else (); 

647 

648 

649 

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

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

653 
fun subst_atomic (old,new) t = 

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

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

656 
 subst (f$t) = subst f $ subst t 

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

658 
in subst t end; 

659 

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

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

662 
(case eta_contract2 body of 

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

664 
else eta_contract_atom (incr_boundvars ~1 f) 

665 
 _ => t0) 

666 
 eta_contract_atom t = t 

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

668 
 eta_contract2 t = eta_contract_atom t; 

669 

670 

671 
(*When can we safely delete the equality? 

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

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

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

675 
Prefer to eliminate Bound variables if possible. 

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

677 

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

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

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

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

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

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

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

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

687 
 occ (_) = false; 

688 
in occEq end; 

689 

3092  690 
exception DEST_EQ; 
691 

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

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

694 
(eta_contract_atom t, eta_contract_atom u) 

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

698 

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

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

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

703 
THEN orient that equality ELSE raise exception DEST_EQ*) 

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

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

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

709 
 _ => raise DEST_EQ; 

710 

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

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

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

716 
val subst = subst_atomic (t,u) 

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

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

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

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

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

722 
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

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

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

725 
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

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

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

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

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

736 
else (); 

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

740 

741 
exception NEWBRANCHES and CLOSEF; 

742 

743 
exception PROVE; 

744 

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

746 

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

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

749 

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

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

761 

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

763 
fun hasSkolem (Skolem _) = true 

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

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

766 
 hasSkolem _ = false; 

767 

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

769 
Skolem terms then allow duplication.*) 

770 
fun joinMd md [] = [] 

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

772 

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

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

776 
 negOfGoal G = G; 

777 

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

779 

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

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

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

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

784 

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

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

787 

2854  788 

789 
(** Backtracking and Pruning **) 

790 

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

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

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

794 
 clashVar vars = 

795 
let fun clash (0, _) = false 

796 
 clash (_, []) = false 

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

798 
in clash end; 

799 

800 

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

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

803 
next branch have been updated.*) 

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

805 
backtracking over bad proofs*) 

806 
 prune (nbrs, nxtVars, choices) = 

807 
let fun traceIt last = 

808 
let val ll = length last 

809 
and lc = length choices 

810 
in if !trace andalso ll<lc then 

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

814 
end 

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

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

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

820 
else (* nbrs'=nbrs *) 

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

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

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

824 
choices) 

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

826 

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

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

832 
Int.toString nbrs ^ " branches")) 

833 
else (); 

834 
raise exn) 

835 
 backtrack _ = raise PROVE; 

2854  836 

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

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

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

842 
 bad _ = false; 

843 
fun change [] = [] 

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

845 
if G aconv G' then change lits 

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

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

848 
if G aconv G' then change lits 

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

850 
 change (lit::lits) = lit :: change lits 

851 
in 

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

853 
end 

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

855 

856 

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

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

860 

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

861 

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

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

863 
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

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

867 
 match (Const a) (Const b) = (a=b) 

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

869 
 match (Free a) (Free b) = (a=b) 

870 
 match (Bound i) (Bound j) = (i=j) 

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

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

873 
 match t u = false; 

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

874 

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

875 

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

878 
bound on unsafe expansions.*) 

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

882 
and hazList = [haz_netpair] 

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

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

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

891 
val nbrs = length brs0 

892 
val nxtVars = nextVars brs 

893 
val G = norm G 

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

894 
val rules = netMkRules G vars safeList 
2854  895 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  896 
fun newBr (vars',lim') prems = 
897 
map (fn prem => 

898 
if (exists isGoal prem) 

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

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

901 
map negOfGoal lits, 

902 
vars', lim') 

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

904 
lits, vars', lim')) 

2854  905 
prems @ 
906 
brs 

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

908 
to branch.*) 

909 
fun deeper [] = raise NEWBRANCHES 

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

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

914 
val lim' = if ntrl < !ntrail 

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

916 
else lim (*discourage branching updates*) 

917 
val vars = vars_in_vars vars 

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

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

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

921 
(*no duplication*) 

922 
in 

4065  923 
traceNew prems; traceVars sign ntrl; 
3083  924 
(if null prems then (*closed the branch: prune!*) 
925 
prv(tacs', brs0::trs, 

926 
prune (nbrs, nxtVars, choices'), 

927 
brs) 

928 
else 

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

4065  930 
then (traceMsg"Excessive branching: KILLED\n"; 
931 
clearTo ntrl; raise NEWBRANCHES) 

3083  932 
else 
933 
prv(tacs', brs0::trs, choices', 

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

935 
handle PRV => 

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

4065  937 
then 
3083  938 
(*Backtrack at this level. 
939 
Reset Vars and try another rule*) 

940 
(clearTo ntrl; deeper grls) 

941 
else (*backtrack to previous level*) 

942 
backtrack choices 

943 
end 

944 
else deeper grls 

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

947 
 closeF (L::Ls) = 

3083  948 
case tryClose(G,L) of 
949 
None => closeF Ls 

950 
 Some tac => 

951 
let val choices' = 

3092  952 
(if !trace then (prs"branch closed"; 
4065  953 
traceVars sign ntrl) 
3083  954 
else (); 
955 
prune (nbrs, nxtVars, 

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

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

958 
handle PRV => 

959 
(*reset Vars and try another literal 

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

961 
(clearTo ntrl; closeF Ls) 

962 
end 

2894  963 
fun closeFl [] = raise CLOSEF 
964 
 closeFl ((br, haz)::pairs) = 

965 
closeF (map fst br) 

966 
handle CLOSEF => closeF (map fst haz) 

967 
handle CLOSEF => closeFl pairs 

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

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

974 
still succeed!*) 

2854  975 
brs0::trs, choices, 
3092  976 
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
4065  977 
handle DEST_EQ => closeF lits 
978 
handle CLOSEF => closeFl ((br,haz)::pairs) 

979 
handle CLOSEF => deeper rules 

2894  980 
handle NEWBRANCHES => 
981 
(case netMkRules G vars hazList of 

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

985 
::brs) 

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

987 
prv (if isGoal G then negOfGoal_tac :: tacs 

988 
else tacs, 

989 
brs0::trs, choices, 

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

991 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

1004 
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

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

1006 
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

1007 
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

1008 
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs 
4196
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

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

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

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

1012 
in (if recur (*send new haz premises to the BACK of the 
9953c0995b79
Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents:
4149
diff
changeset

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

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

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

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

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

1020 
to branch.*) 

1021 
fun deeper [] = raise NEWBRANCHES 

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

4065  1023 
if unify(add_term_vars(P,[]), P, H) 
3083  1024 
then 
1025 
let val ntrl' = !ntrail 

1026 
val vars = vars_in_vars vars 

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

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

1029 
val dup = md andalso vars' <> vars 

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

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

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

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

1034 
else lim1 

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

1036 
both dup and recur are false. Proofs are 

1037 
found at shallower depths, but looping 

1038 
occurs too often...*) 

3917  1039 
val mayUndo = 
1040 
(*Allowing backtracking from a rule application 

1041 
if other matching rules exist, if the rule 

1042 
updated variables, or if the rule did not 

1043 
introduce new variables. This latter condition 

1044 
means it is not a standard "gammarule" but 

1045 
some other form of unsafe rule. Aim is to 

1046 
emulate Fast_tac, which allows all unsafe steps 

1047 
to be undone.*) 

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

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

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

3083  1051 
val tac' = if mayUndo then tac dup 
1052 
else DETERM o (tac dup) 

1053 
in 

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

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

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

3083  1058 
else 
4065  1059 
traceNew prems; traceVars sign ntrl; 
3083  1060 
prv(tac dup :: tacs, 
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

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

1062 
call rotate_tac: new formulae should be last*) 
3083  1063 
brs0::trs, 
1064 
(ntrl, length brs0, PRV) :: choices, 

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

1066 
handle PRV => 

1067 
if mayUndo 

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

1069 
(clearTo ntrl; deeper grls) 

1070 
else (*backtrack to previous level*) 

1071 
backtrack choices 

1072 
end 

1073 
else deeper grls 

1074 
in tracing sign brs0; 

4065  1075 
if lim<1 then (traceMsg "Limit reached. "; backtrack choices) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1076 
else deeper rules 
2854  1077 
handle NEWBRANCHES => 
2894  1078 
(*cannot close branch: move H to literals*) 
2854  1079 
prv (tacs, brs0::trs, choices, 
2894  1080 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1081 
end 
1082 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1083 
in init_gensym(); 
1084 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1085 
end; 

2854  1086 

1087 

2883  1088 
(*Construct an initial branch.*) 
2854  1089 
fun initBranch (ts,lim) = 
2894  1090 
([(map (fn t => (t,true)) ts, [])], 
1091 
[], add_terms_vars (ts,[]), lim); 

2854  1092 

1093 

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

1095 

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

1097 
local open Term 

1098 
in 

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

1100 
 discard_foralls t = t; 

1101 
end; 

1102 

1103 

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

1105 
fun getVars [] i = [] 

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

1107 
if i mem is then getVars alist i 

1108 
else v :: getVars alist i; 

1109 

1110 

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

4065  1112 
fun fromSubgoal t = 
1113 
let val alistVar = ref [] 

1114 
and alistTVar = ref [] 

2854  1115 
fun hdvar ((ix,(v,is))::_) = v 
1116 
fun from lev t = 

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

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

1119 
fun bounds [] = [] 

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

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

1122 
else ilev :: bounds ts 

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

1124 
in 

1125 
case ht of 

4065  1126 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1127 
 Term.Free (a,_) => apply (Free a) 
1128 
 Term.Bound i => apply (Bound i) 

1129 
 Term.Var (ix,_) => 

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

1132 
:: !alistVar; 

1133 
Var (hdvar(!alistVar))) 

2854  1134 
 Some(v,is) => if is=bounds ts then Var v 
1135 
else error("Discrepancy among occurrences of ?" 

1136 
^ Syntax.string_of_vname ix)) 

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

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

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

1140 
end 

1141 

1142 
val npars = length (Logic.strip_params t) 

1143 

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

1145 
fun skoSubgoal i t = 

1146 
if i<npars then 

1147 
skoSubgoal (i+1) 

4065  1148 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1149 
t)) 
1150 
else t 

1151 

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

1153 

1154 

1155 
(*Tactic using tableau engine and proof reconstruction. 

1156 
"lim" is depth limit.*) 

1157 
fun depth_tac cs lim i st = 

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

3030  1159 
let val {sign,...} = rep_thm st 
4065  1160 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
2854  1161 
val hyps = strip_imp_prems skoprem 
1162 
and concl = strip_imp_concl skoprem 

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

1166 
Int.toString lim); 

1167 
backtrack choices) 

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

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

1171 
handle PROVE => Sequence.null); 
2854  1172 

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

1174 

4078  1175 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1176 

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

1177 

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

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

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

1180 

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

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

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

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

1184 
let val st = topthm() 
3030  1185 
val {sign,...} = rep_thm st 
4065  1186 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

1192 
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

1193 

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

1195 

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

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

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

1199 

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

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

1201 
(fullTrace:=[]; trail := []; ntrail := 0; 
3030  1202 
timeap prove (sign_of thy, 
4078  1203 
Data.claset(), 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

1206 

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

1207 

2854  1208 
end; 
1209 