author  paulson 
Fri, 12 Dec 1997 10:34:21 +0100  
changeset 4391  cc3e8453d7f0 
parent 4354  7f4da01bdf0e 
child 4466  305390f23734 
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 
(*Should be a type abbreviation?*) 

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

46 

47 

48 
(*Assumptions about constants: 

49 
The negation symbol is "Not" 

50 
The equality symbol is "op =" 

51 
The istrue judgement symbol is "Trueprop" 

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

53 
*) 

54 
signature BLAST_DATA = 

55 
sig 

56 
type claset 

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

58 
val ccontr : thm 

59 
val contr_tac : int > tactic 

60 
val dup_intr : thm > thm 

61 
val vars_gen_hyp_subst_tac : bool > int > tactic 

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

65 
hazIs: thm list, hazEs: thm list, 

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

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

68 
safe0_netpair: netpair, safep_netpair: netpair, 

69 
haz_netpair: netpair, dup_netpair: netpair} 

70 
end; 

71 

72 

73 
signature BLAST = 

74 
sig 

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

75 
type claset 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

76 
exception TRANS of string (*reports translation errors*) 
2924
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 

4240
8ba60a4cd380
Renamed "overload" to "overloaded" for sml/nj compatibility
paulson
parents:
4233
diff
changeset

90 
val overloaded : 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*) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

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

94 
val fullTrace : branch list list ref 
4065  95 
val fromType : (indexname * term) list ref > Term.typ > term 
96 
val fromTerm : Term.term > term 

97 
val fromSubgoal : Term.term > term 

98 
val instVars : term > (unit > unit) 

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

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

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

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

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

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

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

110 

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

114 
type claset = Data.claset; 

115 

4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

116 
val trace = ref false 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

117 
and stats = ref false; (*for runtime and search statistics*) 
2854  118 

119 
datatype term = 

120 
Const of string 

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

124 
 Var of term option ref 

125 
 Bound of int 

126 
 Abs of string*term 

127 
 op $ of term*term; 

128 

129 

130 
(** Basic syntactic operations **) 

131 

132 
fun is_Var (Var _) = true 

133 
 is_Var _ = false; 

134 

135 
fun dest_Var (Var x) = x; 

136 

137 

138 
fun rand (f$x) = x; 

139 

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

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

142 

143 

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

145 
fun strip_comb u : term * term list = 

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

147 
 stripc x = x 

148 
in stripc(u,[]) end; 

149 

150 

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

152 
fun head_of (f$t) = head_of f 

153 
 head_of u = u; 

154 

155 

156 
(** Particular constants **) 

157 

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

159 

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

161 

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

163 
 isGoal _ = false; 

164 

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

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

167 

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

169 
 isTrueprop _ = false; 

170 

171 

4065  172 
(*** Dealing with overloaded constants ***) 
2854  173 

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

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

177 
map (fromType alist) Ts) 

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

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

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

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

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

183 
end 

184 
 Some v => v) 

2854  185 

186 
local 

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

4240
8ba60a4cd380
Renamed "overload" to "overloaded" for sml/nj compatibility
paulson
parents:
4233
diff
changeset

190 
fun overloaded arg = (overloads := arg :: (!overloads)); 
2854  191 

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

194 
fun fromConst alist (a,T) = 

195 
case assoc_string (!overloads, a) of 

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

197 
 Some f => 

198 
let val T' = f T 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

199 
handle Match => error 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

200 
("Blast_tac: unexpected type for overloaded constant " ^ a) 
4065  201 
in TConst(a, fromType alist T') end; 
202 

2854  203 
end; 
204 

205 

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

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

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

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

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

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

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

217 
 _ aconv _ = false; 

218 

219 

220 
fun mem_term (_, []) = false 

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

222 

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

224 

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

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

227 

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

229 

230 

231 
(** Vars **) 

232 

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

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

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

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

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

240 
 add_term_vars (_, vars) = vars 

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

242 
and add_terms_vars ([], vars) = vars 

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

244 
(*Var list version.*) 

245 
and add_vars_vars ([], vars) = vars 

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

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

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

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

250 

251 

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

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

254 

255 

256 

257 
(*increment a term's nonlocal bound variables 

258 
inc is increment for bound variables 

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

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

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

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

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

264 

265 
fun incr_boundvars 0 t = t 

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

267 

268 

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

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

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

272 
else (ilev) ins_int js 

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

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

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

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

277 

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

279 

280 
fun subst_bound (arg, t) : term = 

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

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

283 
else if i=lev then incr_boundvars lev arg 

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

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

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

287 
 subst (t,lev) = t 

288 
in subst (t,0) end; 

289 

290 

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

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

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

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

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

299 
 nf => nf $ norm u) 
2854  300 
 _ => t; 
301 

302 

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

304 
fun wkNormAux t = case t of 

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

306 
Some u => wkNorm u 

307 
 None => t) 

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

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

310 
 nf => nf $ u) 

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

313 
nb as (f $ t) => 

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

315 
then Abs(a,nb) 

316 
else wkNorm (incr_boundvars ~1 f) 

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

320 
Const _ => t 

4065  321 
 TConst _ => t 
2854  322 
 Skolem(a,args) => t 
323 
 Free _ => t 

324 
 _ => wkNormAux t; 

325 

326 

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

328 
fun varOccur v = 

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

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

331 
and occ (Var w) = 

332 
v=w orelse 

333 
(case !w of None => false 

334 
 Some u => occ u) 

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

4065  336 
 occ (TConst(_,u)) = occ u 
2854  337 
 occ (Abs(_,u)) = occ u 
338 
 occ (f$u) = occ u orelse occ f 

339 
 occ (_) = false; 

340 
in occ end; 

341 

342 
exception UNIFY; 

343 

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

345 
val ntrail = ref 0; 

346 

347 

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

349 
fun clearTo n = 

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

353 
ntrail := !ntrail  1); 

354 

355 

356 
(*Firstorder unification with bound variables. 

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

358 
on the trail (no point in doing so) 

359 
*) 

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

363 
if t aconv u then () 

364 
else if varOccur v u then raise UNIFY 

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

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

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

368 
then dest_Var u := Some t 

369 
else (v := Some u; 

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

371 
fun unifyAux (t,u) = 

372 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

384 

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

387 
fun fromTerm t = 

388 
let val alistVar = ref [] 

389 
and alistTVar = ref [] 

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

2854  391 
 from (Term.Free (a,_)) = Free a 
392 
 from (Term.Bound i) = Bound i 

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

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

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

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

403 
else incr_boundvars ~1 f 

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

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

406 
in from t end; 

407 

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

410 
fun instVars t = 

411 
let val name = ref "A" 

412 
val updated = ref [] 

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

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

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

416 
name := bump_string (!name)) 

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

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

419 
 inst _ = () 

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

421 
in inst t; revert end; 

422 

423 

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

426 
A :: strip_imp_prems B 

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

428 
 strip_imp_prems _ = []; 

429 

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

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

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

433 
 strip_imp_concl A = A : term; 

434 

435 

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

437 

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

439 
fun squash_nots [] = [] 

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

441 
squash_nots Ps 

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

443 
squash_nots Ps 

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

445 

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

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

448 
 skoPrem vars P = P; 

449 

450 
fun convertPrem t = 

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

452 

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

454 
fun convertRule vars t = 

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

456 
val Var v = strip_imp_concl t 

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

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

459 
end; 

460 

461 

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

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
4240
diff
changeset

463 
fun rev_dup_elim th = th RSN (2, revcut_rl) > assumption 2 > Seq.hd; 
2854  464 

465 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

466 
(*Rotate the assumptions in all new subgoals for the LIFO discipline*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

467 
local 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

468 
(*Count new hyps so that they can be rotated*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

469 
fun nNewHyps [] = 0 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

470 
 nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

473 
fun rot_tac [] i st = Seq.single st 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

474 
 rot_tac (0::ks) i st = rot_tac ks (i+1) st 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

475 
 rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st); 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

476 
in 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

477 
fun rot_subgoals_tac (rot, rl) = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

478 
rot_tac (if rot then map nNewHyps rl else []) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

479 
end; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

480 

2854  481 

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

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

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

485 
affected formula.*) 

486 
fun fromRule vars rl = 

4065  487 
let val trl = rl > rep_thm > #prop > fromTerm > convertRule vars 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

488 
fun tac (dup,rot) i = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

489 
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

490 
THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

491 
rot_subgoals_tac (rot, #2 trl) i 
3244
71b760618f30
Basis library version of type "option" now resides in its own structure Option
paulson
parents:
3101
diff
changeset

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

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

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

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

497 
Option.NONE); 
2854  498 

499 

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

500 
(*** Conversion of Introduction Rules ***) 
2854  501 

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

503 

504 
fun convertIntrRule vars t = 

505 
let val Ps = strip_imp_prems t 

506 
val P = strip_imp_concl t 

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

508 
end; 

509 

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

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

512 
fun fromIntrRule vars rl = 

4065  513 
let val trl = rl > rep_thm > #prop > fromTerm > convertIntrRule vars 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

514 
fun tac (dup,rot) i = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

515 
TRACE rl (rtac (if dup then Data.dup_intr rl else rl)) i 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

516 
THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

517 
rot_subgoals_tac (rot, #2 trl) i 
2854  518 
in (trl, tac) end; 
519 

520 

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

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

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

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

526 
 toTerm d (Const a) = Term.Const (a,dummyT) 
4065  527 
 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

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

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

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

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

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

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

535 

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

537 
case P of 

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

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

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

542 
nps) 

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

544 
 _ => 

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

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

548 
nps) 

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

550 

551 
(** 

552 
end; 

553 
**) 

554 

3092  555 

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

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

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

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

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

561 
int; (*resource limit*) 

562 

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

564 

565 
(*Normalize a branchfor tracing*) 

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

567 

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

569 

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

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

572 

573 

4065  574 
val dummyTVar = Term.TVar(("a",0), []); 
3092  575 
val dummyVar2 = Term.Var(("var",0), dummyT); 
576 

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

579 
 showType (Var _) = dummyTVar 

580 
 showType t = 

581 
(case strip_comb t of 

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

583 
 _ => dummyT); 

584 

585 
(*Display toplevel overloading if any*) 

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

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

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

589 
None => topType u 

590 
 some => some) 

591 
 topType _ = None; 

592 

593 

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

4065  596 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  597 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
598 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

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

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

601 
 showTerm d (Var(ref None)) = dummyVar2 
3092  602 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
603 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

606 

4065  607 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  608 

4065  609 
fun traceTerm sign t = 
610 
let val t' = norm t 

611 
val stm = string_of sign 8 t' 

612 
in 

613 
case topType t' of 

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

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

616 
end; 

3092  617 

618 

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

620 
fun tracing sign brs = 

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

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

623 
 printPairs _ = () 

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

625 
(fullTrace := brs0 :: !fullTrace; 

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

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

628 
printPairs pairs; 

629 
writeln"") 

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

631 
end; 

632 

4065  633 
fun traceMsg s = if !trace then prs s else (); 
634 

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

638 
(case !ntrailntrl of 

639 
0 => () 

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

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

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

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

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

645 
writeln"") 

3092  646 
else (); 
647 

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

649 
fun traceNew prems = 

650 
if !trace then 

651 
case length prems of 

652 
0 => prs"branch closed by rule" 

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

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

655 
else (); 

656 

657 

658 

2854  659 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
660 

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

662 
fun subst_atomic (old,new) t = 

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

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

665 
 subst (f$t) = subst f $ subst t 

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

667 
in subst t end; 

668 

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

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

671 
(case eta_contract2 body of 

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

673 
else eta_contract_atom (incr_boundvars ~1 f) 

674 
 _ => t0) 

675 
 eta_contract_atom t = t 

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

677 
 eta_contract2 t = eta_contract_atom t; 

678 

679 

680 
(*When can we safely delete the equality? 

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

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

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

684 
Prefer to eliminate Bound variables if possible. 

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

686 

4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

687 
(*Can t occur in u? For substitution. 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

688 
Does NOT examine the 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

689 
REFLEXIVE because hyp_subst_tac fails on x=x.*) 
2854  690 
fun substOccur t = 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

691 
let (*NO vars are permitted in u except the arguments of t, if it is 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

692 
a Skolem term. This ensures that no equations are deleted that could 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

693 
be instantiated to a cycle. For example, x=?a is rejected because ?a 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

694 
could be instantiated to Suc(x).*) 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

695 
val vars = case t of 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

696 
Skolem(_,vars) => vars 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

697 
 _ => [] 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

698 
fun occEq u = (t aconv u) orelse occ u 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

699 
and occ (Var(ref(Some u))) = occEq u 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

700 
 occ (Var v) = not (mem_var (v, vars)) 
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

701 
 occ (Abs(_,u)) = occEq u 
2854  702 
 occ (f$u) = occEq u orelse occEq f 
703 
 occ (_) = false; 

704 
in occEq end; 

705 

3092  706 
exception DEST_EQ; 
707 

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

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

710 
(eta_contract_atom t, eta_contract_atom u) 

4065  711 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  712 
(eta_contract_atom t, eta_contract_atom u) 
713 
 dest_eq _ = raise DEST_EQ; 

714 

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

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

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

719 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  720 
fun orientGoal (t,u) = case (t,u) of 
2854  721 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
722 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

725 
 _ => raise DEST_EQ; 

726 

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

729 
they should go: this could make proofs fail.*) 
3092  730 
fun equalSubst sign (G, pairs, lits, vars, lim) = 
731 
let val (t,u) = orientGoal(dest_eq G) 

732 
val subst = subst_atomic (t,u) 

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

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

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

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

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

738 
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

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

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

741 
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

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

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

2854  746 
let val nlit = subst lit 
2894  747 
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) 
748 
else subLits (lits, (nlit,true)::Gs, nlits) 

2854  749 
end 
3092  750 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
751 
" for " ^ traceTerm sign t ^ " in branch" ) 

752 
else (); 

3083  753 
subLits (rev lits, [], []) 
2854  754 
end; 
755 

756 

757 
exception NEWBRANCHES and CLOSEF; 

758 

759 
exception PROVE; 

760 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

761 
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

762 
val contr_tac = ematch_tac [Data.notE] THEN' 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

763 
(eq_assume_tac ORELSE' assume_tac); 
2854  764 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

765 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  766 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
767 

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

3083  769 
fun tryClose (Const"*Goal*" $ G, L) = 
4065  770 
if unify([],G,L) then Some eAssume_tac else None 
3083  771 
 tryClose (G, Const"*Goal*" $ L) = 
4065  772 
if unify([],G,L) then Some eAssume_tac else None 
3083  773 
 tryClose (Const"Not" $ G, L) = 
4065  774 
if unify([],G,L) then Some eContr_tac else None 
3083  775 
 tryClose (G, Const"Not" $ L) = 
4065  776 
if unify([],G,L) then Some eContr_tac else None 
3083  777 
 tryClose _ = None; 
2854  778 

779 

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

781 
fun hasSkolem (Skolem _) = true 

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

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

784 
 hasSkolem _ = false; 

785 

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

787 
Skolem terms then allow duplication.*) 

788 
fun joinMd md [] = [] 

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

790 

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

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

794 
 negOfGoal G = G; 

795 

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

797 

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

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

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

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

802 

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

804 
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

805 
rotate_tac ~1 i; 
2894  806 

2854  807 

808 
(** Backtracking and Pruning **) 

809 

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

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

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

813 
 clashVar vars = 

814 
let fun clash (0, _) = false 

815 
 clash (_, []) = false 

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

817 
in clash end; 

818 

819 

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

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

822 
next branch have been updated.*) 

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

824 
backtracking over bad proofs*) 

825 
 prune (nbrs, nxtVars, choices) = 

826 
let fun traceIt last = 

827 
let val ll = length last 

828 
and lc = length choices 

829 
in if !trace andalso ll<lc then 

3083  830 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  831 
last) 
832 
else last 

833 
end 

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

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

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

839 
else (* nbrs'=nbrs *) 

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

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

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

843 
choices) 

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

845 

2894  846 
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars 
3083  847 
 nextVars [] = []; 
2854  848 

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

851 
Int.toString nbrs ^ " branches")) 

852 
else (); 

853 
raise exn) 

854 
 backtrack _ = raise PROVE; 

2854  855 

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

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

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

861 
 bad _ = false; 

862 
fun change [] = [] 

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

864 
if G aconv G' then change lits 

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

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

867 
if G aconv G' then change lits 

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

869 
 change (lit::lits) = lit :: change lits 

870 
in 

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

872 
end 

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

874 

875 

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

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

879 

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

880 

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

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

882 
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

883 
fun match (Var _) u = true 
4065  884 
 match (Const"*Goal*") (Const"Not") = true 
885 
 match (Const"Not") (Const"*Goal*") = true 

886 
 match (Const a) (Const b) = (a=b) 

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

888 
 match (Free a) (Free b) = (a=b) 

889 
 match (Bound i) (Bound j) = (i=j) 

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

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

892 
 match t u = false; 

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

893 

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

894 

4300  895 
(*Branches closed: number of branches closed during the search 
896 
Branches tried: number of branches created by splitting (counting from 1)*) 

897 
val nclosed = ref 0 

898 
and ntried = ref 1; 

899 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

900 
fun printStats (b, start, tacs) = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

901 
if b then 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

902 
writeln (endTiming start ^ " for search. Closed: " 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

903 
^ Int.toString (!nclosed) ^ 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

904 
" tried: " ^ Int.toString (!ntried) ^ 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

905 
" tactics: " ^ Int.toString (length tacs)) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

906 
else (); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

907 

561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

908 

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

911 
bound on unsafe expansions. 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

912 
"start" is CPU time at start, for printing search time 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

913 
*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

914 
fun prove (sign, start, cs, brs, cont) = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

915 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs 
2854  916 
val safeList = [safe0_netpair, safep_netpair] 
917 
and hazList = [haz_netpair] 

4065  918 
fun prv (tacs, trs, choices, []) = 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

919 
(printStats (!trace orelse !stats, start, tacs); 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

920 
cont (tacs, trs, choices)) (*all branches closed!*) 
2854  921 
 prv (tacs, trs, choices, 
2894  922 
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = 
3917  923 
(*apply a safe rule only (possibly allowing instantiation); 
924 
defer any haz formulae*) 

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

927 
val nbrs = length brs0 

928 
val nxtVars = nextVars brs 

929 
val G = norm G 

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

930 
val rules = netMkRules G vars safeList 
2854  931 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  932 
fun newBr (vars',lim') prems = 
933 
map (fn prem => 

934 
if (exists isGoal prem) 

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

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

937 
map negOfGoal lits, 

938 
vars', lim') 

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

940 
lits, vars', lim')) 

2854  941 
prems @ 
942 
brs 

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

944 
to branch.*) 

945 
fun deeper [] = raise NEWBRANCHES 

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

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

950 
val lim' = if ntrl < !ntrail 

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

952 
else lim (*discourage branching updates*) 

953 
val vars = vars_in_vars vars 

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

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

956 
val tacs' = (DETERM o tac(false,true)) :: tacs 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

957 
(*no duplication; rotate*) 
3083  958 
in 
4065  959 
traceNew prems; traceVars sign ntrl; 
3083  960 
(if null prems then (*closed the branch: prune!*) 
4300  961 
(nclosed := !nclosed + 1; 
962 
prv(tacs', brs0::trs, 

963 
prune (nbrs, nxtVars, choices'), 

964 
brs)) 

965 
else (*prems nonnull*) 

3083  966 
if lim'<0 (*faster to kill ALL the alternatives*) 
4065  967 
then (traceMsg"Excessive branching: KILLED\n"; 
968 
clearTo ntrl; raise NEWBRANCHES) 

3083  969 
else 
4300  970 
(ntried := !ntried + length prems  1; 
971 
prv(tacs', brs0::trs, choices', 

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

3083  973 
handle PRV => 
974 
if ntrl < ntrl' (*Vars have been updated*) 

4065  975 
then 
3083  976 
(*Backtrack at this level. 
977 
Reset Vars and try another rule*) 

978 
(clearTo ntrl; deeper grls) 

979 
else (*backtrack to previous level*) 

980 
backtrack choices 

981 
end 

982 
else deeper grls 

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

985 
 closeF (L::Ls) = 

3083  986 
case tryClose(G,L) of 
987 
None => closeF Ls 

988 
 Some tac => 

989 
let val choices' = 

3092  990 
(if !trace then (prs"branch closed"; 
4065  991 
traceVars sign ntrl) 
3083  992 
else (); 
993 
prune (nbrs, nxtVars, 

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

4300  995 
in nclosed := !nclosed + 1; 
996 
prv (tac::tacs, brs0::trs, choices', brs) 

3083  997 
handle PRV => 
998 
(*reset Vars and try another literal 

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

1000 
(clearTo ntrl; closeF Ls) 

1001 
end 

2894  1002 
fun closeFl [] = raise CLOSEF 
1003 
 closeFl ((br, haz)::pairs) = 

1004 
closeF (map fst br) 

1005 
handle CLOSEF => closeF (map fst haz) 

1006 
handle CLOSEF => closeFl pairs 

3083  1007 
in tracing sign brs0; 
4065  1008 
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) 
2854  1009 
else 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

1010 
prv (Data.vars_gen_hyp_subst_tac false :: tacs, 
2854  1011 
brs0::trs, choices, 
3092  1012 
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) 
4065  1013 
handle DEST_EQ => closeF lits 
1014 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1015 
handle CLOSEF => deeper rules 

2894  1016 
handle NEWBRANCHES => 
1017 
(case netMkRules G vars hazList of 

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

1021 
::brs) 

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

1023 
prv (if isGoal G then negOfGoal_tac :: tacs 

1024 
else tacs, 

1025 
brs0::trs, choices, 

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

1027 
lits, vars, lim) :: brs)) 

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

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

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

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

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

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

1040 
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

1041 
(*new premises of haz rules may NOT be duplicated*) 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1042 
fun newPrem (vars,P,dup,lim') prem = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1043 
let val Gs' = map (fn Q => (Q,false)) prem 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

1044 
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

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

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

1047 
else lits 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1048 
in (if exists (match P) prem 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1049 
then (*Recursive in this premise. 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1050 
Don't make new "stack frame". 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1051 
New haz premises will end up at the BACK of the 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1052 
queue, preventing exclusion of others*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

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

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

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

1059 
to branch.*) 

1060 
fun deeper [] = raise NEWBRANCHES 

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

4065  1062 
if unify(add_term_vars(P,[]), P, H) 
3083  1063 
then 
1064 
let val ntrl' = !ntrail 

1065 
val vars = vars_in_vars vars 

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

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

1068 
val dup = md andalso vars' <> vars 

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

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

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

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

1073 
else lim1 

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

1075 
both dup and recur are false. Proofs are 

1076 
found at shallower depths, but looping 

1077 
occurs too often...*) 

3917  1078 
val mayUndo = 
1079 
(*Allowing backtracking from a rule application 

1080 
if other matching rules exist, if the rule 

1081 
updated variables, or if the rule did not 

1082 
introduce new variables. This latter condition 

1083 
means it is not a standard "gammarule" but 

1084 
some other form of unsafe rule. Aim is to 

1085 
emulate Fast_tac, which allows all unsafe steps 

1086 
to be undone.*) 

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

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

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

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1090 
val tac' = if mayUndo then tac(dup, true) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1091 
else DETERM o tac(dup, true) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1092 
(*if recur then doesn't call rotate_tac: 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1093 
new formulae should be last*) 
3083  1094 
in 
1095 
if lim'<0 andalso not (null prems) 

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

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

3083  1099 
else 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1100 
traceNew prems; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1101 
if !trace andalso recur then prs" (recursive)" 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1102 
else (); 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1103 
traceVars sign ntrl; 
4300  1104 
if null prems then nclosed := !nclosed + 1 
1105 
else ntried := !ntried + length prems  1; 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1106 
prv(tac' :: tacs, 
3083  1107 
brs0::trs, 
1108 
(ntrl, length brs0, PRV) :: choices, 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1109 
newBr (vars', P, dup, lim') prems) 
3083  1110 
handle PRV => 
1111 
if mayUndo 

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

1113 
(clearTo ntrl; deeper grls) 

1114 
else (*backtrack to previous level*) 

1115 
backtrack choices 

1116 
end 

1117 
else deeper grls 

1118 
in tracing sign brs0; 

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

1120 
else deeper rules 
2854  1121 
handle NEWBRANCHES => 
2894  1122 
(*cannot close branch: move H to literals*) 
2854  1123 
prv (tacs, brs0::trs, choices, 
2894  1124 
([([], Hs)], H::lits, vars, lim)::brs) 
2854  1125 
end 
1126 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

4065  1127 
in init_gensym(); 
1128 
prv ([], [], [(!ntrail, length brs, PROVE)], brs) 

1129 
end; 

2854  1130 

1131 

2883  1132 
(*Construct an initial branch.*) 
2854  1133 
fun initBranch (ts,lim) = 
2894  1134 
([(map (fn t => (t,true)) ts, [])], 
1135 
[], add_terms_vars (ts,[]), lim); 

2854  1136 

1137 

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

1139 

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

1141 
local open Term 

1142 
in 

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

1144 
 discard_foralls t = t; 

1145 
end; 

1146 

1147 

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

1149 
fun getVars [] i = [] 

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

1151 
if i mem is then getVars alist i 

1152 
else v :: getVars alist i; 

1153 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1154 
exception TRANS of string; 
2854  1155 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1156 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1157 
fun fromSubgoal t = 
1158 
let val alistVar = ref [] 

1159 
and alistTVar = ref [] 

2854  1160 
fun hdvar ((ix,(v,is))::_) = v 
1161 
fun from lev t = 

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

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

1164 
fun bounds [] = [] 

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

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1166 
if i<lev then raise TRANS 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1167 
"Function unknown's argument not a parameter" 
2854  1168 
else ilev :: bounds ts 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1169 
 bounds ts = raise TRANS 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1170 
"Function unknown's argument not a bound variable" 
2854  1171 
in 
1172 
case ht of 

4065  1173 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1174 
 Term.Free (a,_) => apply (Free a) 
1175 
 Term.Bound i => apply (Bound i) 

1176 
 Term.Var (ix,_) => 

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

1179 
:: !alistVar; 

1180 
Var (hdvar(!alistVar))) 

2854  1181 
 Some(v,is) => if is=bounds ts then Var v 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1182 
else raise TRANS 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1183 
("Discrepancy among occurrences of ?" 
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1184 
^ Syntax.string_of_vname ix)) 
2854  1185 
 Term.Abs (a,_,body) => 
1186 
if null ts then Abs(a, from (lev+1) body) 

4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1187 
else raise TRANS "argument not in normal form" 
2854  1188 
end 
1189 

1190 
val npars = length (Logic.strip_params t) 

1191 

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

1193 
fun skoSubgoal i t = 

1194 
if i<npars then 

1195 
skoSubgoal (i+1) 

4065  1196 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1197 
t)) 
1198 
else t 

1199 

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

1201 

1202 

4300  1203 
fun initialize() = 
1204 
(fullTrace:=[]; trail := []; ntrail := 0; 

1205 
nclosed := 0; ntried := 1); 

1206 

1207 

2854  1208 
(*Tactic using tableau engine and proof reconstruction. 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1209 
"start" is CPU time at start, for printing SEARCH time 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1210 
(also prints reconstruction time) 
2854  1211 
"lim" is depth limit.*) 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1212 
fun timing_depth_tac start cs lim i st = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1213 
(initialize(); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1214 
let val {sign,...} = rep_thm st 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1215 
val skoprem = fromSubgoal (List.nth(prems_of st, i1)) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1216 
val hyps = strip_imp_prems skoprem 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1217 
and concl = strip_imp_concl skoprem 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1218 
fun cont (tacs,_,choices) = 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1219 
let val start = startTiming() 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1220 
in 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1221 
case Seq.pull(EVERY' (rev tacs) i st) of 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1222 
None => (writeln ("PROOF FAILED for depth " ^ 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1223 
Int.toString lim); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1224 
backtrack choices) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1225 
 cell => (if (!trace orelse !stats) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1226 
then writeln (endTiming start ^ " for reconstruction") 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1227 
else (); 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1228 
Seq.make(fn()=> cell)) 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1229 
end 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1230 
in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1231 
end 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1232 
handle PROVE => Seq.empty); 
2854  1233 

4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1234 
(*Public version with fixed depth*) 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1235 
fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1236 

cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1237 
fun blast_tac cs i st = 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1238 
(DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i st 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1239 
handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); 
2854  1240 

4078  1241 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1242 

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

1243 

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

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

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

1246 

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

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

1248 
fun trygl cs lim i = 
4300  1249 
(initialize(); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1250 
let val st = topthm() 
3030  1251 
val {sign,...} = rep_thm st 
4065  1252 
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

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

1254 
and concl = strip_imp_concl skoprem 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1255 
in timeap prove (sign, startTiming(), cs, 
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1256 
[initBranch (mkGoal concl :: hyps, lim)], I) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

1258 
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

1259 

4078  1260 
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

1261 

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

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

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

1265 

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

1266 
fun tryInThy thy lim s = 
4300  1267 
(initialize(); 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1268 
timeap prove (sign_of thy, 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1269 
startTiming(), 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1270 
Data.claset(), 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1271 
[initBranch ([readGoal (sign_of thy) s], lim)], 
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

1273 

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

1274 

2854  1275 
end; 
1276 