author  paulson 
Sat, 01 Nov 1997 13:02:39 +0100  
changeset 4065  8862fcb5d44a 
parent 3917  6ea5f9101c3e 
child 4078  c107ab1c7626 
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 
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)) 

472 
handle OPTION _ => Sequence.null; 

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. 

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

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 

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

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

702 
THEN orient that equality ELSE raise exception DEST_EQ*) 

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

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

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

708 
 _ => raise DEST_EQ; 

709 

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

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

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

715 
val subst = subst_atomic (t,u) 

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

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

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

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

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

721 
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

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

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

724 
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

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

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

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

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

735 
else (); 

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

739 

740 
exception NEWBRANCHES and CLOSEF; 

741 

742 
exception PROVE; 

743 

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

745 

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

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

748 

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

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

760 

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

762 
fun hasSkolem (Skolem _) = true 

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

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

765 
 hasSkolem _ = false; 

766 

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

768 
Skolem terms then allow duplication.*) 

769 
fun joinMd md [] = [] 

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

771 

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

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

775 
 negOfGoal G = G; 

776 

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

778 

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

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

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

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

783 

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

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

786 

2854  787 

788 
(** Backtracking and Pruning **) 

789 

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

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

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

793 
 clashVar vars = 

794 
let fun clash (0, _) = false 

795 
 clash (_, []) = false 

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

797 
in clash end; 

798 

799 

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

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

802 
next branch have been updated.*) 

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

804 
backtracking over bad proofs*) 

805 
 prune (nbrs, nxtVars, choices) = 

806 
let fun traceIt last = 

807 
let val ll = length last 

808 
and lc = length choices 

809 
in if !trace andalso ll<lc then 

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

813 
end 

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

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

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

819 
else (* nbrs'=nbrs *) 

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

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

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

823 
choices) 

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

825 

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

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

831 
Int.toString nbrs ^ " branches")) 

832 
else (); 

833 
raise exn) 

834 
 backtrack _ = raise PROVE; 

2854  835 

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

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

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

841 
 bad _ = false; 

842 
fun change [] = [] 

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

844 
if G aconv G' then change lits 

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

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

847 
if G aconv G' then change lits 

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

849 
 change (lit::lits) = lit :: change lits 

850 
in 

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

852 
end 

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

854 

855 

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

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

859 

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

860 

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

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

862 
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

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

866 
 match (Const a) (Const b) = (a=b) 

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

868 
 match (Free a) (Free b) = (a=b) 

869 
 match (Bound i) (Bound j) = (i=j) 

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

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

872 
 match t u = false; 

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

873 

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

874 

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

877 
bound on unsafe expansions.*) 

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

881 
and hazList = [haz_netpair] 

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

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

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

890 
val nbrs = length brs0 

891 
val nxtVars = nextVars brs 

892 
val G = norm G 

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

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

897 
if (exists isGoal prem) 

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

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

900 
map negOfGoal lits, 

901 
vars', lim') 

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

903 
lits, vars', lim')) 

2854  904 
prems @ 
905 
brs 

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

907 
to branch.*) 

908 
fun deeper [] = raise NEWBRANCHES 

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

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

913 
val lim' = if ntrl < !ntrail 

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

915 
else lim (*discourage branching updates*) 

916 
val vars = vars_in_vars vars 

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

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

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

920 
(*no duplication*) 

921 
in 

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

925 
prune (nbrs, nxtVars, choices'), 

926 
brs) 

927 
else 

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

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

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

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

934 
handle PRV => 

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

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

939 
(clearTo ntrl; deeper grls) 

940 
else (*backtrack to previous level*) 

941 
backtrack choices 

942 
end 

943 
else deeper grls 

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

946 
 closeF (L::Ls) = 

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

949 
 Some tac => 

950 
let val choices' = 

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

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

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

957 
handle PRV => 

958 
(*reset Vars and try another literal 

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

960 
(clearTo ntrl; closeF Ls) 

961 
end 

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

964 
closeF (map fst br) 

965 
handle CLOSEF => closeF (map fst haz) 

966 
handle CLOSEF => closeFl pairs 

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

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

973 
still succeed!*) 

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

978 
handle CLOSEF => deeper rules 

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

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

984 
::brs) 

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

986 
prv (if isGoal G then negOfGoal_tac :: tacs 

987 
else tacs, 

988 
brs0::trs, choices, 

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

990 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

1003 
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

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

1005 
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

1006 
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

1007 
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

1008 
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

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

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

1013 
to branch.*) 

1014 
fun deeper [] = raise NEWBRANCHES 

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

4065  1016 
if unify(add_term_vars(P,[]), P, H) 
3083  1017 
then 
1018 
let val ntrl' = !ntrail 

1019 
val vars = vars_in_vars vars 

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

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

1022 
val dup = md andalso vars' <> vars 

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

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

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

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

1027 
else lim1 

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

1029 
both dup and recur are false. Proofs are 

1030 
found at shallower depths, but looping 

1031 
occurs too often...*) 

3917  1032 
val mayUndo = 
1033 
(*Allowing backtracking from a rule application 

1034 
if other matching rules exist, if the rule 

1035 
updated variables, or if the rule did not 

1036 
introduce new variables. This latter condition 

1037 
means it is not a standard "gammarule" but 

1038 
some other form of unsafe rule. Aim is to 

1039 
emulate Fast_tac, which allows all unsafe steps 

1040 
to be undone.*) 

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

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

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

3083  1044 
val tac' = if mayUndo then tac dup 
1045 
else DETERM o (tac dup) 

1046 
in 

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

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

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

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

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

1055 
call rotate_tac: new formulae should be last*) 
3083  1056 
brs0::trs, 
1057 
(ntrl, length brs0, PRV) :: choices, 

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

1059 
handle PRV => 

1060 
if mayUndo 

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

1062 
(clearTo ntrl; deeper grls) 

1063 
else (*backtrack to previous level*) 

1064 
backtrack choices 

1065 
end 

1066 
else deeper grls 

1067 
in tracing sign brs0; 

4065  1068 
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

1069 
else deeper rules 
2854  1070 
handle NEWBRANCHES => 
2894  1071 
(*cannot close branch: move H to literals*) 
2854  1072 
prv (tacs, brs0::trs, choices, 
2894  1073 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1074 
end 
1075 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1076 
in init_gensym(); 
1077 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1078 
end; 

2854  1079 

1080 

2883  1081 
(*Construct an initial branch.*) 
2854  1082 
fun initBranch (ts,lim) = 
2894  1083 
([(map (fn t => (t,true)) ts, [])], 
1084 
[], add_terms_vars (ts,[]), lim); 

2854  1085 

1086 

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

1088 

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

1090 
local open Term 

1091 
in 

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

1093 
 discard_foralls t = t; 

1094 
end; 

1095 

1096 

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

1098 
fun getVars [] i = [] 

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

1100 
if i mem is then getVars alist i 

1101 
else v :: getVars alist i; 

1102 

1103 

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

4065  1105 
fun fromSubgoal t = 
1106 
let val alistVar = ref [] 

1107 
and alistTVar = ref [] 

2854  1108 
fun hdvar ((ix,(v,is))::_) = v 
1109 
fun from lev t = 

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

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

1112 
fun bounds [] = [] 

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

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

1115 
else ilev :: bounds ts 

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

1117 
in 

1118 
case ht of 

4065  1119 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1120 
 Term.Free (a,_) => apply (Free a) 
1121 
 Term.Bound i => apply (Bound i) 

1122 
 Term.Var (ix,_) => 

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

1125 
:: !alistVar; 

1126 
Var (hdvar(!alistVar))) 

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

1129 
^ Syntax.string_of_vname ix)) 

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

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

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

1133 
end 

1134 

1135 
val npars = length (Logic.strip_params t) 

1136 

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

1138 
fun skoSubgoal i t = 

1139 
if i<npars then 

1140 
skoSubgoal (i+1) 

4065  1141 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1142 
t)) 
1143 
else t 

1144 

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

1146 

1147 

1148 
(*Tactic using tableau engine and proof reconstruction. 

1149 
"lim" is depth limit.*) 

1150 
fun depth_tac cs lim i st = 

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

3030  1152 
let val {sign,...} = rep_thm st 
4065  1153 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
2854  1154 
val hyps = strip_imp_prems skoprem 
1155 
and concl = strip_imp_concl skoprem 

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

1159 
Int.toString lim); 

1160 
backtrack choices) 

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

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

1164 
handle PROVE => Sequence.null); 
2854  1165 

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

1167 

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

1169 

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

1170 

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

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

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

1173 

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

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

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

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

1177 
let val st = topthm() 
3030  1178 
val {sign,...} = rep_thm st 
4065  1179 
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

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

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

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

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

1185 
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

1186 

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

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

1188 

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

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

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

1192 

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

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

1194 
(fullTrace:=[]; trail := []; ntrail := 0; 
3030  1195 
timeap prove (sign_of thy, 
1196 
!Data.claset, 

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

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

1198 
I)); 
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 

2854  1201 
end; 
1202 