author  paulson 
Tue, 12 Jul 2005 12:49:46 +0200  
changeset 16774  515b6020cf5d 
parent 15786  81e9f17823ea 
child 16859  8ac6d4902b56 
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... 
4651  14 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
15 
this restriction is intrinsic 

2894  16 
* ignores elimination rules that don't have the correct format 
17 
(conclusion must be a formula variable) 

18 
* ignores types, which can make HOL proofs fail 

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

19 
* 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

20 
+ 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

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

23 
Known problems: 

3092  24 
"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

25 
from expansion. This happens because newlycreated formulae always 
3092  26 
have priority over existing ones. But obviously recursive rules 
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset

27 
such as transitivity are treated specially to prevent this. Sometimes 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

28 
the formulae get into the wrong order (see WRONG below). 
3021
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

29 

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

30 
With substition for equalities (hyp_subst_tac): 
3092  31 
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

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

33 
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

34 
"no DETERM" flag would prevent proofs failing here. 
2854  35 
*) 
36 

37 
(*Should be a type abbreviation?*) 

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

39 

40 

41 
(*Assumptions about constants: 

42 
The negation symbol is "Not" 

43 
The equality symbol is "op =" 

44 
The istrue judgement symbol is "Trueprop" 

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

46 
*) 

47 
signature BLAST_DATA = 

48 
sig 

49 
type claset 

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

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

51 
val is_hol : bool (*Is this HOL or FOL/ZF?*) 
2854  52 
val ccontr : thm 
53 
val contr_tac : int > tactic 

54 
val dup_intr : thm > thm 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

55 
val hyp_subst_tac : bool ref > int > tactic 
4078  56 
val claset : unit > claset 
4653  57 
val rep_cs : (* dependent on classical.ML *) 
2854  58 
claset > {safeIs: thm list, safeEs: thm list, 
59 
hazIs: thm list, hazEs: thm list, 

4651  60 
swrappers: (string * wrapper) list, 
61 
uwrappers: (string * wrapper) list, 

2854  62 
safe0_netpair: netpair, safep_netpair: netpair, 
12403  63 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} 
7272  64 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  65 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 
2854  66 
end; 
67 

68 

69 
signature BLAST = 

70 
sig 

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

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

72 
exception TRANS of string (*reports translation errors*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

74 
Const of string 
4065  75 
 TConst of string * term 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

80 
 Abs of string*term 
15786
81e9f17823ea
Added op in front of constructor for better parsing.
gagern
parents:
15661
diff
changeset

81 
 op $ of term*term; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

82 
type branch 
2883  83 
val depth_tac : claset > int > int > tactic 
15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

84 
val depth_limit : int ref 
2883  85 
val blast_tac : claset > int > tactic 
86 
val Blast_tac : int > tactic 

5926  87 
val setup : (theory > theory) list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

88 
(*debugging tools*) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

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

91 
val fullTrace : branch list list ref 
4065  92 
val fromType : (indexname * term) list ref > Term.typ > term 
93 
val fromTerm : Term.term > term 

94 
val fromSubgoal : Term.term > term 

95 
val instVars : term > (unit > unit) 

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

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

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

98 
val tryInThy : theory > int > string > 
3083  99 
(int>tactic) list * branch list list * (int*int*exn) list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

103 
(int>tactic) list * branch list list * (int*int*exn) list 

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

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

107 

3092  108 
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854  109 
struct 
110 

111 
type claset = Data.claset; 

112 

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

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

114 
and stats = ref false; (*for runtime and search statistics*) 
2854  115 

116 
datatype term = 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

117 
Const of string 
4065  118 
 TConst of string * term (*type of overloaded constantas a term!*) 
2854  119 
 Skolem of string * term option ref list 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

120 
 Free of string 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

121 
 Var of term option ref 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

122 
 Bound of int 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

123 
 Abs of string*term 
5613  124 
 op $ of term*term; 
2854  125 

126 

127 
(** Basic syntactic operations **) 

128 

129 
fun is_Var (Var _) = true 

130 
 is_Var _ = false; 

131 

132 
fun dest_Var (Var x) = x; 

133 

134 
fun rand (f$x) = x; 

135 

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

15570  137 
val list_comb : term * term list > term = Library.foldl (op $); 
2854  138 

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

140 
fun strip_comb u : term * term list = 

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

142 
 stripc x = x 

143 
in stripc(u,[]) end; 

144 

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

146 
fun head_of (f$t) = head_of f 

147 
 head_of u = u; 

148 

149 

150 
(** Particular constants **) 

151 

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

153 

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

155 

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

157 
 isGoal _ = false; 

158 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

159 
val boolT = if Data.is_hol then "bool" else "o"; 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

160 
val Trueprop = Term.Const("Trueprop", Type(boolT,[])>propT); 
2854  161 
fun mk_tprop P = Term.$ (Trueprop, P); 
162 

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

164 
 isTrueprop _ = false; 

165 

166 

4065  167 
(*** Dealing with overloaded constants ***) 
2854  168 

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

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

171 
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts) 
4065  172 
 fromType alist (Term.TFree(a,_)) = Free a 
173 
 fromType alist (Term.TVar (ixn,_)) = 

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

15531  175 
NONE => let val t' = Var(ref NONE) 
4065  176 
in alist := (ixn, t') :: !alist; t' 
177 
end 

15531  178 
 SOME v => v) 
2854  179 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

180 
(*Definitions of the theory in which blast is initialized.*) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

181 
val curr_defs = ref Defs.empty; 
2854  182 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

183 
(*Types aren't needed if the constant has at most one definition and is monomorphic*) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

184 
fun no_types_needed s = 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

185 
(case Defs.overloading_info (!curr_defs) s of 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

186 
NONE => true 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

187 
 SOME (T,defs,_) => length defs <= 1 andalso null (typ_tvars T)) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

188 
handle Option => (warning ("Defs.overloading_info failed for " ^ s); false); 
11119  189 

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

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

192 
For efficiency, Const is used for FOL and for the logical constants. 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

193 
We can't use it for all nonoverloaded operators because some preservation 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

194 
of type information is necessary to prevent PROOF FAILED elsewhere.*) 
13550  195 
fun fromConst alist (a,T) = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

196 
if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse no_types_needed a 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

197 
then Const a 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

198 
else TConst(a, fromType alist T); 
2854  199 

200 

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

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

4065  203 
 (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb 
2854  204 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
205 
 (Free a) aconv (Free b) = a=b 

15531  206 
 (Var(ref(SOME t))) aconv u = t aconv u 
207 
 t aconv (Var(ref(SOME u))) = t aconv u 

2854  208 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
209 
 (Bound i) aconv (Bound j) = i=j 

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

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

212 
 _ aconv _ = false; 

213 

214 

215 
fun mem_term (_, []) = false 

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

217 

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

219 

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

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

222 

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

224 

225 

226 
(** Vars **) 

227 

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

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

15531  230 
 add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) 
231 
 add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) 

4065  232 
 add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) 
2854  233 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
234 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

235 
 add_term_vars (_, vars) = vars 

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

237 
and add_terms_vars ([], vars) = vars 

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

239 
(*Var list version.*) 

240 
and add_vars_vars ([], vars) = vars 

15531  241 
 add_vars_vars (ref (SOME u) :: vs, vars) = 
2854  242 
add_vars_vars (vs, add_term_vars(u,vars)) 
15531  243 
 add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) 
2854  244 
add_vars_vars (vs, ins_var (v, vars)); 
245 

246 

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

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

249 

250 

251 

252 
(*increment a term's nonlocal bound variables 

253 
inc is increment for bound variables 

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

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

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

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

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

259 

260 
fun incr_boundvars 0 t = t 

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

262 

263 

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

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

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

267 
else (ilev) ins_int js 

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

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

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

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

272 

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

274 

275 
fun subst_bound (arg, t) : term = 

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

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

278 
else if i=lev then incr_boundvars lev arg 

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

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

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

282 
 subst (t,lev) = t 

283 
in subst (t,0) end; 

284 

285 

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

286 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  287 
fun norm t = case t of 
2952  288 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
4065  289 
 TConst(a,aT) => TConst(a, norm aT) 
15531  290 
 (Var (ref NONE)) => t 
291 
 (Var (ref (SOME u))) => norm u 

2854  292 
 (f $ u) => (case norm f of 
3101
e8a92f497295
Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents:
3092
diff
changeset

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

294 
 nf => nf $ norm u) 
2854  295 
 _ => t; 
296 

297 

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

299 
fun wkNormAux t = case t of 

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

15531  301 
SOME u => wkNorm u 
302 
 NONE => t) 

2854  303 
 (f $ u) => (case wkNormAux f of 
304 
Abs(_,body) => wkNorm (subst_bound (u, body)) 

305 
 nf => nf $ u) 

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

308 
nb as (f $ t) => 

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

310 
then Abs(a,nb) 

311 
else wkNorm (incr_boundvars ~1 f) 

3092  312 
 nb => Abs (a,nb)) 
2854  313 
 _ => t 
314 
and wkNorm t = case head_of t of 

315 
Const _ => t 

4065  316 
 TConst _ => t 
2854  317 
 Skolem(a,args) => t 
318 
 Free _ => t 

319 
 _ => wkNormAux t; 

320 

321 

5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

322 
(*Does variable v occur in u? For unification. 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

323 
Dangling bound vars are also forbidden.*) 
2854  324 
fun varOccur v = 
5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

325 
let fun occL lev [] = false (*same as (exists occ), but faster*) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

326 
 occL lev (u::us) = occ lev u orelse occL lev us 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

327 
and occ lev (Var w) = 
2854  328 
v=w orelse 
15531  329 
(case !w of NONE => false 
330 
 SOME u => occ lev u) 

5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

331 
 occ lev (Skolem(_,args)) = occL lev (map Var args) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

332 
(*ignore TConst, since term variables can't occur in types (?) *) 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

333 
 occ lev (Bound i) = lev <= i 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

334 
 occ lev (Abs(_,u)) = occ (lev+1) u 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

335 
 occ lev (f$u) = occ lev u orelse occ lev f 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

336 
 occ lev _ = false; 
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

337 
in occ 0 end; 
2854  338 

339 
exception UNIFY; 

340 

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

342 
val ntrail = ref 0; 

343 

344 

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

346 
fun clearTo n = 

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

351 

352 

353 
(*Firstorder unification with bound variables. 

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

355 
on the trail (no point in doing so) 

356 
*) 

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

360 
if t aconv u then () 

361 
else if varOccur v u then raise UNIFY 

15531  362 
else if mem_var(v, vars) then v := SOME u 
2854  363 
else (*avoid updating Vars in the branch if possible!*) 
364 
if is_Var u andalso mem_var(dest_Var u, vars) 

15531  365 
then dest_Var u := SOME t 
366 
else (v := SOME u; 

2854  367 
trail := v :: !trail; ntrail := !ntrail + 1) 
368 
fun unifyAux (t,u) = 

369 
case (wkNorm t, wkNorm u) of 

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

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

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

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

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

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

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

381 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

382 
(*Convert from "real" terms to prototerms; etacontract. 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

383 
Code is similar to fromSubgoal.*) 
4065  384 
fun fromTerm t = 
385 
let val alistVar = ref [] 

386 
and alistTVar = ref [] 

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

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

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

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

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

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

400 
else incr_boundvars ~1 f 

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

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

403 
in from t end; 

404 

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

407 
fun instVars t = 

12902  408 
let val name = ref "a" 
4065  409 
val updated = ref [] 
410 
fun inst (TConst(a,t)) = inst t 

15531  411 
 inst (Var(v as ref NONE)) = (updated := v :: (!updated); 
412 
v := SOME (Free ("?" ^ !name)); 

12902  413 
name := Symbol.bump_string (!name)) 
4065  414 
 inst (Abs(a,t)) = inst t 
415 
 inst (f $ u) = (inst f; inst u) 

416 
 inst _ = () 

15570  417 
fun revert() = List.app (fn v => v:=NONE) (!updated) 
4065  418 
in inst t; revert end; 
419 

420 

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

423 
A :: strip_imp_prems B 

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

425 
 strip_imp_prems _ = []; 

426 

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

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

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

430 
 strip_imp_concl A = A : term; 

431 

432 

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

434 

9170  435 
exception ElimBadConcl and ElimBadPrem; 
436 

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

438 
If we don't find it then the premise is illformed and could cause 

439 
PROOF FAILED*) 

440 
fun delete_concl [] = raise ElimBadPrem 

15531  441 
 delete_concl (Const "*Goal*" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = 
9170  442 
Ps 
15531  443 
 delete_concl (Const "Not" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = 
9170  444 
Ps 
445 
 delete_concl (P::Ps) = P :: delete_concl Ps; 

2854  446 

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

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

449 
 skoPrem vars P = P; 

450 

451 
fun convertPrem t = 

9170  452 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  453 

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

455 
fun convertRule vars t = 

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

457 
val Var v = strip_imp_concl t 

15531  458 
in v := SOME (Const"*False*"); 
2854  459 
(P, map (convertPrem o skoPrem vars) Ps) 
9170  460 
end 
461 
handle Bind => raise ElimBadConcl; 

2854  462 

463 

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

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

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

467 

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

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

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

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

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

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

473 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  474 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

476 
 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

477 
 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

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

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

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

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

482 

2854  483 

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

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

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

486 
(*Resolution/matching tactics: if upd then the proof state may be updated. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

487 
Matching makes the tactics more deterministic in the presence of Vars.*) 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

488 
fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]); 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

489 
fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]); 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

490 

871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

491 
(*Tableau rule from elimination rule. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

492 
Flag "upd" says that the inference updated the branch. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

493 
Flag "dup" requests duplication of the affected formula.*) 
2854  494 
fun fromRule vars rl = 
4065  495 
let val trl = rl > rep_thm > #prop > fromTerm > convertRule vars 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

496 
fun tac (upd, dup,rot) i = 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

497 
emtac upd (if dup then rev_dup_elim rl else rl) i 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

499 
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

500 
in Option.SOME (trl, tac) end 
9170  501 
handle ElimBadPrem => (*reject: prems don't preserve conclusion*) 
502 
(warning("Ignoring weak elimination rule\n" ^ string_of_thm rl); 

503 
Option.NONE) 

504 
 ElimBadConcl => (*ignore: conclusion is not just a variable*) 

505 
(if !trace then (warning("Ignoring illformed elimination rule:\n" ^ 

506 
"conclusion should be a variable\n" ^ string_of_thm rl)) 

507 
else (); 

508 
Option.NONE); 

2854  509 

510 

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

511 
(*** Conversion of Introduction Rules ***) 
2854  512 

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

514 

515 
fun convertIntrRule vars t = 

516 
let val Ps = strip_imp_prems t 

517 
val P = strip_imp_concl t 

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

519 
end; 

520 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

521 
(*Tableau rule from introduction rule. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

522 
Flag "upd" says that the inference updated the branch. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

523 
Flag "dup" requests duplication of the affected formula. 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

524 
Since haz rules are now delayed, "dup" is always FALSE for 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

525 
introduction rules.*) 
2854  526 
fun fromIntrRule vars rl = 
4065  527 
let val trl = rl > rep_thm > #prop > fromTerm > convertIntrRule vars 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

528 
fun tac (upd,dup,rot) i = 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

529 
rmtac upd (if dup then Data.dup_intr rl else rl) i 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

531 
rot_subgoals_tac (rot, #2 trl) i 
2854  532 
in (trl, tac) end; 
533 

534 

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

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

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

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

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

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

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

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

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

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

547 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  548 

549 

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

551 
case P of 

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

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

553 
let val pG = mk_tprop (toTerm 2 G) 
2854  554 
val intrs = List.concat 
555 
(map (fn (inet,_) => Net.unify_term inet pG) 

556 
nps) 

11783  557 
in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end 
2854  558 
 _ => 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

559 
let val pP = mk_tprop (toTerm 3 P) 
2854  560 
val elims = List.concat 
561 
(map (fn (_,enet) => Net.unify_term enet pP) 

562 
nps) 

11783  563 
in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end; 
2854  564 

3092  565 

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

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

567 
type branch = 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

568 
{pairs: ((term*bool) list * (*safe formulae on this level*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

569 
(term*bool) list) list, (*haz formulae on this level*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

570 
lits: term list, (*literals: irreducible formulae*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

571 
vars: term option ref list, (*variables occurring in branch*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

572 
lim: int}; (*resource limit*) 
3092  573 

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

575 

576 
(*Normalize a branchfor tracing*) 

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

578 

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

580 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

581 
fun normBr {pairs, lits, vars, lim} = 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

582 
{pairs = map normLev pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

583 
lits = map norm lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

584 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

585 
lim = lim}; 
3092  586 

587 

4065  588 
val dummyTVar = Term.TVar(("a",0), []); 
3092  589 
val dummyVar2 = Term.Var(("var",0), dummyT); 
590 

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

593 
 showType (Var _) = dummyTVar 

594 
 showType t = 

595 
(case strip_comb t of 

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

597 
 _ => dummyT); 

598 

599 
(*Display toplevel overloading if any*) 

15531  600 
fun topType (TConst(a,t)) = SOME (showType t) 
4065  601 
 topType (Abs(a,t)) = topType t 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

602 
 topType (f $ u) = (case topType f of NONE => topType u  some => some) 
15531  603 
 topType _ = NONE; 
4065  604 

605 

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

4065  608 
 showTerm d (TConst(a,_)) = Term.Const (a,dummyT) 
3092  609 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
610 
 showTerm d (Free a) = Term.Free (a,dummyT) 

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

15531  612 
 showTerm d (Var(ref(SOME u))) = showTerm d u 
613 
 showTerm d (Var(ref NONE)) = dummyVar2 

3092  614 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
615 
else Term.Abs(a, dummyT, showTerm (d1) t) 

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

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

618 

4065  619 
fun string_of sign d t = Sign.string_of_term sign (showTerm d t); 
3092  620 

4065  621 
fun traceTerm sign t = 
622 
let val t' = norm t 

623 
val stm = string_of sign 8 t' 

624 
in 

625 
case topType t' of 

15531  626 
NONE => stm (*no type to attach*) 
627 
 SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T 

4065  628 
end; 
3092  629 

630 

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

632 
fun tracing sign brs = 

14984  633 
let fun printPairs (((G,_)::_,_)::_) = immediate_output(traceTerm sign G) 
634 
 printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)") 

3092  635 
 printPairs _ = () 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

636 
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 
3092  637 
(fullTrace := brs0 :: !fullTrace; 
15570  638 
List.app (fn _ => immediate_output "+") brs; 
14984  639 
immediate_output (" [" ^ Int.toString lim ^ "] "); 
3092  640 
printPairs pairs; 
641 
writeln"") 

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

643 
end; 

644 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

645 
fun traceMsg s = if !trace then writeln s else (); 
4065  646 

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

650 
(case !ntrailntrl of 

651 
0 => () 

14984  652 
 1 => immediate_output"\t1 variable UPDATED:" 
653 
 n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); 

4065  654 
(*display the instantiations themselves, though no variable names*) 
15570  655 
List.app (fn v => immediate_output(" " ^ string_of sign 4 (valOf (!v)))) 
4065  656 
(List.take(!trail, !ntrailntrl)); 
657 
writeln"") 

3092  658 
else (); 
659 

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

661 
fun traceNew prems = 

662 
if !trace then 

663 
case length prems of 

14984  664 
0 => immediate_output"branch closed by rule" 
665 
 1 => immediate_output"branch extended (1 new subgoal)" 

666 
 n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals") 

3092  667 
else (); 
668 

669 

670 

2854  671 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
672 

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

674 
fun subst_atomic (old,new) t = 

15531  675 
let fun subst (Var(ref(SOME u))) = subst u 
2854  676 
 subst (Abs(a,body)) = Abs(a, subst body) 
677 
 subst (f$t) = subst f $ subst t 

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

679 
in subst t end; 

680 

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

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

683 
(case eta_contract2 body of 

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

685 
else eta_contract_atom (incr_boundvars ~1 f) 

686 
 _ => t0) 

687 
 eta_contract_atom t = t 

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

689 
 eta_contract2 t = eta_contract_atom t; 

690 

691 

692 
(*When can we safely delete the equality? 

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

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

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

696 
Prefer to eliminate Bound variables if possible. 

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

698 

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

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

700 
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

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

703 
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

704 
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

705 
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

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

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

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

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

710 
fun occEq u = (t aconv u) orelse occ u 
15531  711 
and occ (Var(ref(SOME u))) = occEq u 
4354
7f4da01bdf0e
Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents:
4323
diff
changeset

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

713 
 occ (Abs(_,u)) = occEq u 
2854  714 
 occ (f$u) = occEq u orelse occEq f 
715 
 occ (_) = false; 

716 
in occEq end; 

717 

3092  718 
exception DEST_EQ; 
719 

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

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

722 
(eta_contract_atom t, eta_contract_atom u) 

4065  723 
 dest_eq (TConst("op =",_) $ t $ u) = 
3092  724 
(eta_contract_atom t, eta_contract_atom u) 
725 
 dest_eq _ = raise DEST_EQ; 

726 

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

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

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

731 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  732 
fun orientGoal (t,u) = case (t,u) of 
2854  733 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
734 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

737 
 _ => raise DEST_EQ; 

738 

2894  739 
(*Substitute through the branch if an equality goal (else raise DEST_EQ). 
740 
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

741 
they should go: this could make proofs fail.*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

742 
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092  743 
let val (t,u) = orientGoal(dest_eq G) 
744 
val subst = subst_atomic (t,u) 

2854  745 
fun subst2(G,md) = (subst G, md) 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

746 
(*substitute throughout list; extract affected formulae*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

747 
fun subForm ((G,md), (changed, pairs)) = 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

748 
let val nG = subst G 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

749 
in if nG aconv G then (changed, (G,md)::pairs) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

750 
else ((nG,md)::changed, pairs) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

751 
end 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

752 
(*substitute throughout "stack frame"; extract affected formulae*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

753 
fun subFrame ((Gs,Hs), (changed, frames)) = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

754 
let val (changed', Gs') = foldr subForm (changed, []) Gs 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

755 
val (changed'', Hs') = foldr subForm (changed', []) Hs 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

756 
in (changed'', (Gs',Hs')::frames) end 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

757 
(*substitute throughout literals; extract affected ones*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

758 
fun subLit (lit, (changed, nlits)) = 
2854  759 
let val nlit = subst lit 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

760 
in if nlit aconv lit then (changed, nlit::nlits) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

761 
else ((nlit,true)::changed, nlits) 
2854  762 
end 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

763 
val (changed, lits') = foldr subLit ([], []) lits 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

764 
val (changed', pairs') = foldr subFrame (changed, []) pairs 
3092  765 
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ 
766 
" for " ^ traceTerm sign t ^ " in branch" ) 

767 
else (); 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

768 
{pairs = (changed',[])::pairs', (*affected formulas, and others*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

769 
lits = lits', (*unaffected literals*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

770 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

771 
lim = lim} 
2854  772 
end; 
773 

774 

775 
exception NEWBRANCHES and CLOSEF; 

776 

777 
exception PROVE; 

778 

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

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

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

781 
(eq_assume_tac ORELSE' assume_tac); 
2854  782 

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

783 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  784 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
785 

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

3083  787 
fun tryClose (Const"*Goal*" $ G, L) = 
15531  788 
if unify([],G,L) then SOME eAssume_tac else NONE 
3083  789 
 tryClose (G, Const"*Goal*" $ L) = 
15531  790 
if unify([],G,L) then SOME eAssume_tac else NONE 
3083  791 
 tryClose (Const"Not" $ G, L) = 
15531  792 
if unify([],G,L) then SOME eContr_tac else NONE 
3083  793 
 tryClose (G, Const"Not" $ L) = 
15531  794 
if unify([],G,L) then SOME eContr_tac else NONE 
795 
 tryClose _ = NONE; 

2854  796 

797 

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

799 
fun hasSkolem (Skolem _) = true 

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

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

802 
 hasSkolem _ = false; 

803 

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

805 
Skolem terms then allow duplication.*) 

806 
fun joinMd md [] = [] 

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

808 

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

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

812 
 negOfGoal G = G; 

813 

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

815 

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

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

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

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

820 

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

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

822 
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

823 
rotate_tac ~1 i; 
2894  824 

2854  825 

826 
(** Backtracking and Pruning **) 

827 

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

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

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

831 
 clashVar vars = 

832 
let fun clash (0, _) = false 

833 
 clash (_, []) = false 

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

835 
in clash end; 

836 

837 

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

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

840 
next branch have been updated.*) 

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

842 
backtracking over bad proofs*) 

843 
 prune (nbrs, nxtVars, choices) = 

844 
let fun traceIt last = 

845 
let val ll = length last 

846 
and lc = length choices 

847 
in if !trace andalso ll<lc then 

3083  848 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  849 
last) 
850 
else last 

851 
end 

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

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

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

857 
else (* nbrs'=nbrs *) 

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

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

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

861 
choices) 

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

863 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

864 
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

865 
 nextVars [] = []; 
2854  866 

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

869 
Int.toString nbrs ^ " branches")) 

870 
else (); 

871 
raise exn) 

872 
 backtrack _ = raise PROVE; 

2854  873 

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

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

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

879 
 bad _ = false; 

880 
fun change [] = [] 

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

882 
if G aconv G' then change lits 

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

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

885 
if G aconv G' then change lits 

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

887 
 change (lit::lits) = lit :: change lits 

888 
in 

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

890 
end 

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

892 

893 

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

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

897 

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

898 

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

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

900 
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

901 
fun match (Var _) u = true 
4065  902 
 match (Const"*Goal*") (Const"Not") = true 
903 
 match (Const"Not") (Const"*Goal*") = true 

904 
 match (Const a) (Const b) = (a=b) 

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

906 
 match (Free a) (Free b) = (a=b) 

907 
 match (Bound i) (Bound j) = (i=j) 

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

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

910 
 match t u = false; 

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

911 

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

912 

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

915 
val nclosed = ref 0 

916 
and ntried = ref 1; 

917 

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

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

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

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

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

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

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

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

925 

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

926 

2854  927 
(*Tableau prover based on leanTaP. Argument is a list of branches. Each 
928 
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

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

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

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

932 
fun prove (sign, start, cs, brs, cont) = 
4653  933 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  934 
val safeList = [safe0_netpair, safep_netpair] 
935 
and hazList = [haz_netpair] 

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

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

938 
cont (tacs, trs, choices)) (*all branches closed!*) 
2854  939 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

940 
brs0 as {pairs = ((G,md)::br, haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

941 
lits, vars, lim} :: brs) = 
3917  942 
(*apply a safe rule only (possibly allowing instantiation); 
943 
defer any haz formulae*) 

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

946 
val nbrs = length brs0 

947 
val nxtVars = nextVars brs 

948 
val G = norm G 

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

949 
val rules = netMkRules G vars safeList 
2854  950 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  951 
fun newBr (vars',lim') prems = 
952 
map (fn prem => 

953 
if (exists isGoal prem) 

5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

954 
then {pairs = ((joinMd md prem, []) :: 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

955 
negOfGoals ((br, haz)::pairs)), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

956 
lits = map negOfGoal lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

957 
vars = vars', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

958 
lim = lim'} 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

959 
else {pairs = ((joinMd md prem, []) :: 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

960 
(br, haz) :: pairs), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

961 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

962 
vars = vars', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

963 
lim = lim'}) 
2854  964 
prems @ 
965 
brs 

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

967 
to branch.*) 

968 
fun deeper [] = raise NEWBRANCHES 

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

4065  970 
if unify(add_term_vars(P,[]), P, G) 
3083  971 
then (*P comes from the rule; G comes from the branch.*) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

972 
let val updated = ntrl < !ntrail (*branch updated*) 
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

973 
val lim' = if updated 
3083  974 
then lim  (1+log(length rules)) 
975 
else lim (*discourage branching updates*) 

976 
val vars = vars_in_vars vars 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

977 
val vars' = foldr add_terms_vars vars prems 
3083  978 
val choices' = (ntrl, nbrs, PRV) :: choices 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

979 
val tacs' = (tac(updated,false,true)) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

980 
:: tacs (*no duplication; rotate*) 
3083  981 
in 
4065  982 
traceNew prems; traceVars sign ntrl; 
3083  983 
(if null prems then (*closed the branch: prune!*) 
4300  984 
(nclosed := !nclosed + 1; 
985 
prv(tacs', brs0::trs, 

986 
prune (nbrs, nxtVars, choices'), 

987 
brs)) 

988 
else (*prems nonnull*) 

3083  989 
if lim'<0 (*faster to kill ALL the alternatives*) 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

990 
then (traceMsg"Excessive branching: KILLED"; 
4065  991 
clearTo ntrl; raise NEWBRANCHES) 
3083  992 
else 
4300  993 
(ntried := !ntried + length prems  1; 
994 
prv(tacs', brs0::trs, choices', 

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

3083  996 
handle PRV => 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

997 
if updated then 
3083  998 
(*Backtrack at this level. 
999 
Reset Vars and try another rule*) 

1000 
(clearTo ntrl; deeper grls) 

1001 
else (*backtrack to previous level*) 

1002 
backtrack choices 

1003 
end 

1004 
else deeper grls 

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

1007 
 closeF (L::Ls) = 

3083  1008 
case tryClose(G,L) of 
15531  1009 
NONE => closeF Ls 
1010 
 SOME tac => 

3083  1011 
let val choices' = 
14984  1012 
(if !trace then (immediate_output"branch closed"; 
4065  1013 
traceVars sign ntrl) 
3083  1014 
else (); 
1015 
prune (nbrs, nxtVars, 

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

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

3083  1019 
handle PRV => 
1020 
(*reset Vars and try another literal 

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

1022 
(clearTo ntrl; closeF Ls) 

1023 
end 

11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1024 
(*Try to unify a queued formula (safe or haz) with head goal*) 
2894  1025 
fun closeFl [] = raise CLOSEF 
1026 
 closeFl ((br, haz)::pairs) = 

1027 
closeF (map fst br) 

1028 
handle CLOSEF => closeF (map fst haz) 

1029 
handle CLOSEF => closeFl pairs 

3083  1030 
in tracing sign brs0; 
4065  1031 
if lim<0 then (traceMsg "Limit reached. "; backtrack choices) 
2854  1032 
else 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1033 
prv (Data.hyp_subst_tac trace :: tacs, 
2854  1034 
brs0::trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1035 
equalSubst sign 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1036 
(G, {pairs = (br,haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1037 
lits = lits, vars = vars, lim = lim}) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1038 
:: brs) 
4065  1039 
handle DEST_EQ => closeF lits 
1040 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1041 
handle CLOSEF => deeper rules 

2894  1042 
handle NEWBRANCHES => 
1043 
(case netMkRules G vars hazList of 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1044 
[] => (*there are no plausible haz rules*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1045 
(traceMsg "moving formula to literals"; 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1046 
prv (tacs, brs0::trs, choices, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1047 
{pairs = (br,haz)::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1048 
lits = addLit(G,lits), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1049 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1050 
lim = lim} :: brs)) 
2894  1051 
 _ => (*G admits some haz rules: try later*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1052 
(traceMsg "moving formula to haz list"; 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4391
diff
changeset

1053 
prv (if isGoal G then negOfGoal_tac :: tacs 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1054 
else tacs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1055 
brs0::trs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1056 
choices, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1057 
{pairs = (br, haz@[(negOfGoal G, md)])::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1058 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1059 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1060 
lim = lim} :: brs))) 
2854  1061 
end 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1062 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

1065 
prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1066 
{pairs = (Gs,haz@haz')::pairs, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1067 
lits = lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1068 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1069 
lim = lim} :: brs) 
2854  1070 
 prv (tacs, trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1071 
brs0 as {pairs = [([], (H,md)::Hs)], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1072 
lits, vars, lim} :: brs) = 
2894  1073 
(*no safe steps possible at any level: apply a haz rule*) 
2854  1074 
let exception PRV (*backtrack to precisely this recursion!*) 
2894  1075 
val H = norm H 
2854  1076 
val ntrl = !ntrail 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1077 
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

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

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

1080 
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

1081 
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

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

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

1084 
else lits 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1085 
in {pairs = if exists (match P) prem then [(Gs',Hs')] 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1086 
(*Recursive in this premise. Don't make new 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1087 
"stack frame". New haz premises will end up 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1088 
at the BACK of the queue, preventing 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1089 
exclusion of others*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1090 
else [(Gs',[]), ([],Hs')], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1091 
lits = lits', 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1092 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

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

1097 
to branch.*) 

1098 
fun deeper [] = raise NEWBRANCHES 

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

4065  1100 
if unify(add_term_vars(P,[]), P, H) 
3083  1101 
then 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1102 
let val updated = ntrl < !ntrail (*branch updated*) 
3083  1103 
val vars = vars_in_vars vars 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1104 
val vars' = foldr add_terms_vars vars prems 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1105 
(*duplicate H if md permits*) 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1106 
val dup = md (*earlier had "andalso vars' <> vars": 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1107 
duplicate only if the subgoal has new vars*) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1108 
(*any instances of P in the subgoals? 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1109 
NB: boolean "recur" affects tracing only!*) 
3083  1110 
and recur = exists (exists (match P)) prems 
1111 
val lim' = (*Decrement "lim" extra if updates occur*) 

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1112 
if updated then lim  (1+log(length rules)) 
3083  1113 
else lim1 
1114 
(*It is tempting to leave "lim" UNCHANGED if 

1115 
both dup and recur are false. Proofs are 

1116 
found at shallower depths, but looping 

1117 
occurs too often...*) 

3917  1118 
val mayUndo = 
1119 
(*Allowing backtracking from a rule application 

1120 
if other matching rules exist, if the rule 

1121 
updated variables, or if the rule did not 

1122 
introduce new variables. This latter condition 

1123 
means it is not a standard "gammarule" but 

1124 
some other form of unsafe rule. Aim is to 

1125 
emulate Fast_tac, which allows all unsafe steps 

1126 
to be undone.*) 

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

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1128 
orelse updated 
3917  1129 
orelse vars=vars' (*no new Vars?*) 
5481
c41956742c2e
Less deterministic reconstruction: now more robust but perhaps slower
paulson
parents:
5463
diff
changeset

1130 
val tac' = tac(updated, dup, true) 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1131 
(*if recur then perhaps shouldn't call rotate_tac: new 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1132 
formulae should be last, but that's WRONG if the new 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1133 
formulae are Goals, since they remain in the first 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1134 
position*) 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1135 

3083  1136 
in 
1137 
if lim'<0 andalso not (null prems) 

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

5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

1139 
(traceMsg"Excessive branching: KILLED"; 
4065  1140 
clearTo ntrl; raise NEWBRANCHES) 
3083  1141 
else 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

1142 
traceNew prems; 
14984  1143 
if !trace andalso dup then immediate_output" (duplicating)" 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1144 
else (); 
14984  1145 
if !trace andalso recur then immediate_output" (recursive)" 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

1147 
traceVars sign ntrl; 
4300  1148 
if null prems then nclosed := !nclosed + 1 
1149 
else ntried := !ntried + length prems  1; 

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

1150 
prv(tac' :: tacs, 
3083  1151 
brs0::trs, 
1152 
(ntrl, length brs0, PRV) :: choices, 

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

1153 
newBr (vars', P, dup, lim') prems) 
3083  1154 
handle PRV => 
1155 
if mayUndo 

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

1157 
(clearTo ntrl; deeper grls) 

1158 
else (*backtrack to previous level*) 

1159 
backtrack choices 

1160 
end 

1161 
else deeper grls 

1162 
in tracing sign brs0; 

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

1164 
else deeper rules 
2854  1165 
handle NEWBRANCHES => 
2894  1166 
(*cannot close branch: move H to literals*) 
2854  1167 
prv (tacs, brs0::trs, choices, 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1168 
{pairs = [([], Hs)], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1169 
lits = H::lits, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1170 
vars = vars, 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1171 
lim = lim} :: brs) 
2854  1172 
end 
1173 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

12346  1174 
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 
2854  1175 

1176 

2883  1177 
(*Construct an initial branch.*) 
2854  1178 
fun initBranch (ts,lim) = 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1179 
{pairs = [(map (fn t => (t,true)) ts, [])], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1180 
lits = [], 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1181 
vars = add_terms_vars (ts,[]), 
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1182 
lim = lim}; 
2854  1183 

1184 

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

1186 

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

1188 
local open Term 

1189 
in 

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

1191 
 discard_foralls t = t; 

1192 
end; 

1193 

1194 

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

1196 
fun getVars [] i = [] 

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

1198 
if i mem is then getVars alist i 

1199 
else v :: getVars alist i; 

1200 

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

1201 
exception TRANS of string; 
2854  1202 

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

1203 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1204 
fun fromSubgoal t = 
1205 
let val alistVar = ref [] 

1206 
and alistTVar = ref [] 

2854  1207 
fun hdvar ((ix,(v,is))::_) = v 
1208 
fun from lev t = 

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

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

1211 
fun bounds [] = [] 

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

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

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

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

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

1217 
"Function unknown's argument not a bound variable" 
2854  1218 
in 
1219 
case ht of 

4065  1220 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1221 
 Term.Free (a,_) => apply (Free a) 
1222 
 Term.Bound i => apply (Bound i) 

1223 
 Term.Var (ix,_) => 

4065  1224 
(case (assoc_string_int(!alistVar,ix)) of 
15531  1225 
NONE => (alistVar := (ix, (ref NONE, bounds ts)) 
4065  1226 
:: !alistVar; 
1227 
Var (hdvar(!alistVar))) 

15531  1228 
 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

1229 
else raise TRANS 
5411  1230 
("Discrepancy among occurrences of " 
4233
85d004a96b98
Rationalized error handling: if lowlevel tactic (depth_tac) cannot accept the
paulson
parents:
4196
diff
changeset

1231 
^ Syntax.string_of_vname ix)) 
2854  1232 
 Term.Abs (a,_,body) => 
1233 
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

1234 
else raise TRANS "argument not in normal form" 
2854  1235 
end 
1236 

1237 
val npars = length (Logic.strip_params t) 

1238 

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

1240 
fun skoSubgoal i t = 

1241 
if i<npars then 

1242 
skoSubgoal (i+1) 

4065  1243 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1244 
t)) 
1245 
else t 

1246 

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

1248 

1249 

16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1250 
fun initialize thy = 
4300  1251 
(fullTrace:=[]; trail := []; ntrail := 0; 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1252 
nclosed := 0; ntried := 1; curr_defs := Theory.defs_of thy); 
4300  1253 

1254 

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

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

1257 
(also prints reconstruction time) 
2854  1258 
"lim" is depth limit.*) 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

1259 
fun timing_depth_tac start cs lim i st0 = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1260 
let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0); 
9486
2df511ebb956
handle actual objectlogic rules by atomizing the goal;
wenzelm
parents:
9170
diff
changeset

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

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

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

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

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

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

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

1268 
case Seq.pull(EVERY' (rev tacs) i st) of 
15531  1269 
NONE => (writeln ("PROOF FAILED for depth " ^ 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

1270 
Int.toString lim); 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1271 
if !trace then error "************************\n" 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

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

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

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

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

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

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

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

1279 
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

1280 
end 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1281 
handle PROVE => Seq.empty; 
2854  1282 

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

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

1284 
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

1285 

15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1286 
val depth_limit = ref 20; 
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1287 

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

1288 
fun blast_tac cs i st = 
15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1289 
((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1290 
THEN flexflex_tac) st 
14466  1291 
handle TRANS s => 
1292 
((if !trace then warning ("blast: " ^ s) else ()); 

1293 
Seq.empty); 

2854  1294 

4078  1295 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1296 

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

1297 

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

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

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

1300 

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

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

1302 
fun trygl cs lim i = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1303 
let val st = topthm() 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1304 
val {sign,...} = rep_thm st 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1305 
val skoprem = (initialize (theory_of_thm st); 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1306 
fromSubgoal (List.nth(prems_of st, i1))) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1307 
val hyps = strip_imp_prems skoprem 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1308 
and concl = strip_imp_concl skoprem 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1309 
in timeap prove (sign, startTiming(), cs, 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1310 
[initBranch (mkGoal concl :: hyps, lim)], I) 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1311 
end 
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1312 
handle Subscript => error("There is no subgoal " ^ Int.toString i); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1313 

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

1315 

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

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

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

1319 

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

1320 
fun tryInThy thy lim s = 
16774
515b6020cf5d
experimental code to reduce the amount of type information in blast
paulson
parents:
15786
diff
changeset

1321 
(initialize thy; 
6391  1322 
timeap prove (Theory.sign_of thy, 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

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

1324 
Data.claset(), 
6391  1325 
[initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

1327 

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

1328 

5926  1329 
(** method setup **) 
1330 

7559  1331 
fun blast_args m = 
11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1332 
Method.bang_sectioned_args' 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1333 
Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; 
7155  1334 

15531  1335 
fun blast_meth NONE = Data.cla_meth' blast_tac 
1336 
 blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim); 

7155  1337 

11152
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1338 
val setup = [Method.add_methods [("blast", blast_args blast_meth, 
32d002362005
Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents:
11119
diff
changeset

1339 
"tableau prover")]]; 
5926  1340 

1341 

2854  1342 
end; 