author  wenzelm 
Wed, 16 Nov 2005 17:45:23 +0100  
changeset 18177  7041d038acb0 
parent 18171  c4f873d65603 
child 18525  ce1ae48c320f 
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 

18171  11 
Given the typeargs system, constructor Const could be eliminated, with 
12 
TConst replaced by a constructor that takes the typargs list as an argument. 

13 
However, Const is heavily used for logical connectives. 

2894  14 

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

15 
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

16 
Blast_tac... 
4651  17 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
18 
this restriction is intrinsic 

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

21 
* ignores types, which can make HOL proofs fail 

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

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

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

24 
* its proof strategy is more general but can actually be slower 
2894  25 

26 
Known problems: 

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

28 
from expansion. This happens because newlycreated formulae always 
3092  29 
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

30 
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

31 
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

32 

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

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

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

36 
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

37 
"no DETERM" flag would prevent proofs failing here. 
2854  38 
*) 
39 

40 
(*Should be a type abbreviation?*) 

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

42 

43 

44 
(*Assumptions about constants: 

45 
The negation symbol is "Not" 

46 
The equality symbol is "op =" 

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

48 
*) 

49 
signature BLAST_DATA = 

50 
sig 

51 
type claset 

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

53 
val ccontr : thm 

54 
val contr_tac : int > tactic 

55 
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

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

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

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

69 

70 
signature BLAST = 

71 
sig 

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

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

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

74 
datatype term = 
18177  75 
Const of string * term list 
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 
17795  81 
 $ 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 = 

18177  117 
Const of string * term list (*typargs constantas a terms!*) 
2854  118 
 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

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

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

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

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

125 

126 
(** Basic syntactic operations **) 

127 

128 
fun is_Var (Var _) = true 

129 
 is_Var _ = false; 

130 

131 
fun dest_Var (Var x) = x; 

132 

133 
fun rand (f$x) = x; 

134 

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

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

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

139 
fun strip_comb u : term * term list = 

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

141 
 stripc x = x 

142 
in stripc(u,[]) end; 

143 

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

145 
fun head_of (f$t) = head_of f 

146 
 head_of u = u; 

147 

148 

149 
(** Particular constants **) 

150 

18177  151 
fun negate P = Const ("Not", []) $ P; 
2854  152 

18177  153 
fun mkGoal P = Const ("*Goal*", []) $ P; 
2854  154 

18177  155 
fun isGoal (Const ("*Goal*", _) $ _) = true 
2854  156 
 isGoal _ = false; 
157 

18177  158 
val TruepropC = ObjectLogic.judgment_name (the_context ()); 
159 
val TruepropT = Sign.the_const_type (the_context ()) TruepropC; 

18171  160 

18177  161 
fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); 
2854  162 

18177  163 
fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm 
164 
 strip_Trueprop tm = tm; 

165 

2854  166 

167 

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

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

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

17271  175 
(case (AList.lookup (op =) (!alist) ixn) of 
15531  176 
NONE => let val t' = Var(ref NONE) 
4065  177 
in alist := (ixn, t') :: !alist; t' 
178 
end 

15531  179 
 SOME v => v) 
2854  180 

17993  181 
(*refer to the theory in which blast is initialized*) 
18146  182 
val typargs = ref (fn ((_, T): string * typ) => [T]); 
2854  183 

18177  184 
fun fromConst alist (a, T) = 
185 
Const (a, map (fromType alist) (! typargs (a, T))); 

2854  186 

187 

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

18177  189 
fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us) 
2854  190 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) 
191 
 (Free a) aconv (Free b) = a=b 

15531  192 
 (Var(ref(SOME t))) aconv u = t aconv u 
193 
 t aconv (Var(ref(SOME u))) = t aconv u 

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

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

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

18177  198 
 _ aconv _ = false 
199 
and aconvs ([], []) = true 

200 
 aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us) 

201 
 aconvs _ = false; 

2854  202 

203 

204 
fun mem_term (_, []) = false 

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

206 

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

208 

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

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

211 

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

213 

214 

215 
(** Vars **) 

216 

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

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

15531  219 
 add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) 
220 
 add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) 

18177  221 
 add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars) 
2854  222 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
223 
 add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) 

224 
 add_term_vars (_, vars) = vars 

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

226 
and add_terms_vars ([], vars) = vars 

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

228 
(*Var list version.*) 

229 
and add_vars_vars ([], vars) = vars 

15531  230 
 add_vars_vars (ref (SOME u) :: vs, vars) = 
2854  231 
add_vars_vars (vs, add_term_vars(u,vars)) 
15531  232 
 add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) 
2854  233 
add_vars_vars (vs, ins_var (v, vars)); 
234 

235 

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

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

238 

239 

240 

241 
(*increment a term's nonlocal bound variables 

242 
inc is increment for bound variables 

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

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

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

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

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

248 

249 
fun incr_boundvars 0 t = t 

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

251 

252 

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

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

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

256 
else (ilev) ins_int js 

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

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

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

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

261 

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

263 

264 
fun subst_bound (arg, t) : term = 

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

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

267 
else if i=lev then incr_boundvars lev arg 

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

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

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

271 
 subst (t,lev) = t 

272 
in subst (t,0) end; 

273 

274 

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

275 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  276 
fun norm t = case t of 
2952  277 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
18177  278 
 Const(a,ts) => Const(a, map norm ts) 
15531  279 
 (Var (ref NONE)) => t 
280 
 (Var (ref (SOME u))) => norm u 

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

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

283 
 nf => nf $ norm u) 
2854  284 
 _ => t; 
285 

286 

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

288 
fun wkNormAux t = case t of 

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

15531  290 
SOME u => wkNorm u 
291 
 NONE => t) 

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

294 
 nf => nf $ u) 

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

297 
nb as (f $ t) => 

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

299 
then Abs(a,nb) 

300 
else wkNorm (incr_boundvars ~1 f) 

3092  301 
 nb => Abs (a,nb)) 
2854  302 
 _ => t 
303 
and wkNorm t = case head_of t of 

304 
Const _ => t 

305 
 Skolem(a,args) => t 

306 
 Free _ => t 

307 
 _ => wkNormAux t; 

308 

309 

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

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

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

313 
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

314 
 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

315 
and occ lev (Var w) = 
2854  316 
v=w orelse 
15531  317 
(case !w of NONE => false 
318 
 SOME u => occ lev u) 

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

319 
 occ lev (Skolem(_,args)) = occL lev (map Var args) 
18177  320 
(*ignore Const, since term variables can't occur in types (?) *) 
5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

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

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

323 
 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

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

325 
in occ 0 end; 
2854  326 

327 
exception UNIFY; 

328 

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

330 
val ntrail = ref 0; 

331 

332 

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

334 
fun clearTo n = 

3083  335 
while !ntrail<>n do 
15531  336 
(hd(!trail) := NONE; 
2854  337 
trail := tl (!trail); 
338 
ntrail := !ntrail  1); 

339 

340 

341 
(*Firstorder unification with bound variables. 

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

343 
on the trail (no point in doing so) 

344 
*) 

4065  345 
fun unify(vars,t,u) = 
2854  346 
let val n = !ntrail 
347 
fun update (t as Var v, u) = 

348 
if t aconv u then () 

349 
else if varOccur v u then raise UNIFY 

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

15531  353 
then dest_Var u := SOME t 
354 
else (v := SOME u; 

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

357 
case (wkNorm t, wkNorm u) of 

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

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

18177  360 
 (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts) 
4065  361 
else raise UNIFY 
2854  362 
 (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') 
363 
(*NB: can yield unifiers having dangling Bound vars!*) 

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

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

18177  366 
and unifysAux ([], []) = () 
367 
 unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us)) 

368 
 unifysAux _ = raise UNIFY; 

3083  369 
in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) 
2854  370 
end; 
371 

372 

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

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

374 
Code is similar to fromSubgoal.*) 
4065  375 
fun fromTerm t = 
376 
let val alistVar = ref [] 

377 
and alistTVar = ref [] 

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

2854  379 
 from (Term.Free (a,_)) = Free a 
380 
 from (Term.Bound i) = Bound i 

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

17271  382 
(case (AList.lookup (op =) (!alistVar) ixn) of 
15531  383 
NONE => let val t' = Var(ref NONE) 
4065  384 
in alistVar := (ixn, t') :: !alistVar; t' 
2854  385 
end 
15531  386 
 SOME v => v) 
2854  387 
 from (Term.Abs (a,_,u)) = 
388 
(case from u of 

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

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

391 
else incr_boundvars ~1 f 

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

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

394 
in from t end; 

395 

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

398 
fun instVars t = 

12902  399 
let val name = ref "a" 
4065  400 
val updated = ref [] 
18177  401 
fun inst (Const(a,ts)) = List.app inst ts 
15531  402 
 inst (Var(v as ref NONE)) = (updated := v :: (!updated); 
403 
v := SOME (Free ("?" ^ !name)); 

12902  404 
name := Symbol.bump_string (!name)) 
4065  405 
 inst (Abs(a,t)) = inst t 
406 
 inst (f $ u) = (inst f; inst u) 

407 
 inst _ = () 

15570  408 
fun revert() = List.app (fn v => v:=NONE) (!updated) 
4065  409 
in inst t; revert end; 
410 

411 

2854  412 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
18177  413 
fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B 
2854  414 
 strip_imp_prems _ = []; 
415 

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

18177  417 
fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B 
418 
 strip_imp_concl A = strip_Trueprop A; 

419 

2854  420 

421 

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

423 

9170  424 
exception ElimBadConcl and ElimBadPrem; 
425 

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

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

428 
PROOF FAILED*) 

429 
fun delete_concl [] = raise ElimBadPrem 

18177  430 
 delete_concl (Const ("*Goal*", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) = 
9170  431 
Ps 
18177  432 
 delete_concl (Const ("Not", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) = 
9170  433 
Ps 
434 
 delete_concl (P::Ps) = P :: delete_concl Ps; 

2854  435 

18177  436 
fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = 
2854  437 
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) 
438 
 skoPrem vars P = P; 

439 

440 
fun convertPrem t = 

9170  441 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  442 

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

444 
fun convertRule vars t = 

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

446 
val Var v = strip_imp_concl t 

18177  447 
in v := SOME (Const ("*False*", [])); 
2854  448 
(P, map (convertPrem o skoPrem vars) Ps) 
9170  449 
end 
450 
handle Bind => raise ElimBadConcl; 

2854  451 

452 

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

17257
0ab67cb765da
introduced binding priority 1 for linear combinators etc.
haftmann
parents:
16976
diff
changeset

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

456 

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

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

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

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

460 
fun nNewHyps [] = 0 
18177  461 
 nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps 
4391
cc3e8453d7f0
More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents:
4354
diff
changeset

462 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  463 

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

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

465 
 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

466 
 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

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

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

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

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

471 

2854  472 

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

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

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

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

476 
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

477 
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

478 
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

479 

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

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

481 
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

482 
Flag "dup" requests duplication of the affected formula.*) 
2854  483 
fun fromRule vars rl = 
4065  484 
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

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

486 
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

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

488 
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

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

492 
Option.NONE) 

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

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

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

496 
else (); 

497 
Option.NONE); 

2854  498 

499 

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

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

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

503 

504 
fun convertIntrRule vars t = 

505 
let val Ps = strip_imp_prems t 

506 
val P = strip_imp_concl t 

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

508 
end; 

509 

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

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

511 
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

512 
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

513 
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

514 
introduction rules.*) 
2854  515 
fun fromIntrRule vars rl = 
4065  516 
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

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

518 
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

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

520 
rot_subgoals_tac (rot, #2 trl) i 
2854  521 
in (trl, tac) end; 
522 

523 

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

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

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

528 
fun toTerm 0 _ = dummyVar 
18177  529 
 toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

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

535 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  536 

537 

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

539 
case P of 

18177  540 
(Const ("*Goal*", _) $ G) => 
541 
let val pG = mk_Trueprop (toTerm 2 G) 

2854  542 
val intrs = List.concat 
543 
(map (fn (inet,_) => Net.unify_term inet pG) 

544 
nps) 

11783  545 
in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end 
2854  546 
 _ => 
18177  547 
let val pP = mk_Trueprop (toTerm 3 P) 
2854  548 
val elims = List.concat 
549 
(map (fn (_,enet) => Net.unify_term enet pP) 

550 
nps) 

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

3092  553 

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

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

556 
{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

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

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

559 
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

560 
lim: int}; (*resource limit*) 
3092  561 

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

563 

564 
(*Normalize a branchfor tracing*) 

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

566 

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

568 

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

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

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

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

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

573 
lim = lim}; 
3092  574 

575 

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

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

581 
 showType (Var _) = dummyTVar 

582 
 showType t = 

583 
(case strip_comb t of 

18177  584 
(Const (a, _), us) => Term.Type(a, map showType us) 
4065  585 
 _ => dummyT); 
586 

587 
(*Display toplevel overloading if any*) 

18177  588 
fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts)) 
589 
 topType thy (Abs(a,t)) = topType thy t 

590 
 topType thy (f $ u) = (case topType thy f of NONE => topType thy u  some => some) 

591 
 topType _ _ = NONE; 

4065  592 

593 

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

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

15531  599 
 showTerm d (Var(ref(SOME u))) = showTerm d u 
600 
 showTerm d (Var(ref NONE)) = dummyVar2 

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

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

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

605 

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

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

610 
val stm = string_of sign 8 t' 

611 
in 

18177  612 
case topType sign t' of 
15531  613 
NONE => stm (*no type to attach*) 
614 
 SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T 

4065  615 
end; 
3092  616 

617 

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

619 
fun tracing sign brs = 

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

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

623 
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 
3092  624 
(fullTrace := brs0 :: !fullTrace; 
15570  625 
List.app (fn _ => immediate_output "+") brs; 
14984  626 
immediate_output (" [" ^ Int.toString lim ^ "] "); 
3092  627 
printPairs pairs; 
628 
writeln"") 

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

630 
end; 

631 

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

632 
fun traceMsg s = if !trace then writeln s else (); 
4065  633 

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

637 
(case !ntrailntrl of 

638 
0 => () 

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

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

3092  645 
else (); 
646 

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

648 
fun traceNew prems = 

649 
if !trace then 

650 
case length prems of 

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

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

3092  654 
else (); 
655 

656 

657 

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

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

661 
fun subst_atomic (old,new) t = 

15531  662 
let fun subst (Var(ref(SOME u))) = subst u 
2854  663 
 subst (Abs(a,body)) = Abs(a, subst body) 
664 
 subst (f$t) = subst f $ subst t 

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

666 
in subst t end; 

667 

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

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

670 
(case eta_contract2 body of 

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

672 
else eta_contract_atom (incr_boundvars ~1 f) 

673 
 _ => t0) 

674 
 eta_contract_atom t = t 

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

676 
 eta_contract2 t = eta_contract_atom t; 

677 

678 

679 
(*When can we safely delete the equality? 

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

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

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

683 
Prefer to eliminate Bound variables if possible. 

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

685 

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

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

687 
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

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

690 
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

691 
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

692 
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

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

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

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

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

697 
fun occEq u = (t aconv u) orelse occ u 
15531  698 
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

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

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

703 
in occEq end; 

704 

3092  705 
exception DEST_EQ; 
706 

18177  707 
(*Take apart an equality. NO constant Trueprop*) 
708 
fun dest_eq (Const ("op =", _) $ t $ u) = 

3092  709 
(eta_contract_atom t, eta_contract_atom u) 
710 
 dest_eq _ = raise DEST_EQ; 

711 

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

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

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

716 
THEN orient that equality ELSE raise exception DEST_EQ*) 

3092  717 
fun orientGoal (t,u) = case (t,u) of 
2854  718 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
719 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 

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

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

722 
 _ => raise DEST_EQ; 

723 

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

726 
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

727 
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092  728 
let val (t,u) = orientGoal(dest_eq G) 
729 
val subst = subst_atomic (t,u) 

2854  730 
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

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

732 
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

733 
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

734 
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

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

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

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

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

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

740 
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

741 
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

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

743 
fun subLit (lit, (changed, nlits)) = 
2854  744 
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

745 
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

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

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

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

752 
else (); 

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

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

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

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

756 
lim = lim} 
2854  757 
end; 
758 

759 

760 
exception NEWBRANCHES and CLOSEF; 

761 

762 
exception PROVE; 

763 

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

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

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

766 
(eq_assume_tac ORELSE' assume_tac); 
2854  767 

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

768 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  769 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
770 

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

18177  772 
fun tryClose (Const ("*Goal*", _) $ G, L) = 
15531  773 
if unify([],G,L) then SOME eAssume_tac else NONE 
18177  774 
 tryClose (G, Const ("*Goal*", _) $ L) = 
15531  775 
if unify([],G,L) then SOME eAssume_tac else NONE 
18177  776 
 tryClose (Const ("Not", _) $ G, L) = 
15531  777 
if unify([],G,L) then SOME eContr_tac else NONE 
18177  778 
 tryClose (G, Const ("Not", _) $ L) = 
15531  779 
if unify([],G,L) then SOME eContr_tac else NONE 
780 
 tryClose _ = NONE; 

2854  781 

782 

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

784 
fun hasSkolem (Skolem _) = true 

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

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

787 
 hasSkolem _ = false; 

788 

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

790 
Skolem terms then allow duplication.*) 

791 
fun joinMd md [] = [] 

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

793 

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

18177  796 
fun negOfGoal (Const ("*Goal*", _) $ G) = negate G 
797 
 negOfGoal G = G; 

2894  798 

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

800 

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

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

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

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

805 

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

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

807 
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

808 
rotate_tac ~1 i; 
2894  809 

2854  810 

811 
(** Backtracking and Pruning **) 

812 

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

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

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

816 
 clashVar vars = 

817 
let fun clash (0, _) = false 

818 
 clash (_, []) = false 

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

820 
in clash end; 

821 

822 

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

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

825 
next branch have been updated.*) 

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

827 
backtracking over bad proofs*) 

17795  828 
 prune (nbrs: int, nxtVars, choices) = 
2854  829 
let fun traceIt last = 
830 
let val ll = length last 

831 
and lc = length choices 

832 
in if !trace andalso ll<lc then 

3083  833 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
2854  834 
last) 
835 
else last 

836 
end 

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

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

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

842 
else (* nbrs'=nbrs *) 

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

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

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

846 
choices) 

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

848 

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

849 
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

850 
 nextVars [] = []; 
2854  851 

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

854 
Int.toString nbrs ^ " branches")) 

855 
else (); 

856 
raise exn) 

857 
 backtrack _ = raise PROVE; 

2854  858 

2894  859 
(*Add the literal G, handling *Goal* and detecting duplicates.*) 
18177  860 
fun addLit (Const ("*Goal*", _) $ G, lits) = 
2894  861 
(*New literal is a *Goal*, so change all other Goals to Nots*) 
18177  862 
let fun bad (Const ("*Goal*", _) $ _) = true 
863 
 bad (Const ("Not", _) $ G') = G aconv G' 

2854  864 
 bad _ = false; 
865 
fun change [] = [] 

18177  866 
 change (Const ("*Goal*", _) $ G' :: lits) = 
2854  867 
if G aconv G' then change lits 
18177  868 
else Const ("Not", []) $ G' :: change lits 
869 
 change (Const ("Not", _) $ G' :: lits) = 

2854  870 
if G aconv G' then change lits 
18177  871 
else Const ("Not", []) $ G' :: change lits 
2854  872 
 change (lit::lits) = lit :: change lits 
873 
in 

18177  874 
Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits) 
2854  875 
end 
876 
 addLit (G,lits) = ins_term(G, lits) 

877 

878 

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

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

882 

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

883 

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

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

885 
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

886 
fun match (Var _) u = true 
18177  887 
 match (Const ("*Goal*", _)) (Const ("Not", _)) = true 
888 
 match (Const ("Not", _)) (Const ("*Goal*", _)) = true 

889 
 match (Const (a,tas)) (Const (b,tbs)) = a=b andalso matchs tas tbs 

4065  890 
 match (Free a) (Free b) = (a=b) 
891 
 match (Bound i) (Bound j) = (i=j) 

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

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

18177  894 
 match t u = false 
895 
and matchs [] [] = true 

896 
 matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; 

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

897 

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

898 

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

901 
val nclosed = ref 0 

902 
and ntried = ref 1; 

903 

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

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

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

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

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

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

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

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

911 

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

912 

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

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

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

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

918 
fun prove (sign, start, cs, brs, cont) = 
4653  919 
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  920 
val safeList = [safe0_netpair, safep_netpair] 
921 
and hazList = [haz_netpair] 

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

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

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

926 
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

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

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

932 
val nbrs = length brs0 

933 
val nxtVars = nextVars brs 

934 
val G = norm G 

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

935 
val rules = netMkRules G vars safeList 
2854  936 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
2894  937 
fun newBr (vars',lim') prems = 
938 
map (fn prem => 

939 
if (exists isGoal prem) 

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

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

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

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

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

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

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

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

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

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

949 
lim = lim'}) 
2854  950 
prems @ 
951 
brs 

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

953 
to branch.*) 

954 
fun deeper [] = raise NEWBRANCHES 

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

4065  956 
if unify(add_term_vars(P,[]), P, G) 
3083  957 
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

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

959 
val lim' = if updated 
3083  960 
then lim  (1+log(length rules)) 
961 
else lim (*discourage branching updates*) 

962 
val vars = vars_in_vars vars 

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

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

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

966 
:: tacs (*no duplication; rotate*) 
3083  967 
in 
4065  968 
traceNew prems; traceVars sign ntrl; 
3083  969 
(if null prems then (*closed the branch: prune!*) 
4300  970 
(nclosed := !nclosed + 1; 
971 
prv(tacs', brs0::trs, 

972 
prune (nbrs, nxtVars, choices'), 

973 
brs)) 

974 
else (*prems nonnull*) 

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

976 
then (traceMsg"Excessive branching: KILLED"; 
4065  977 
clearTo ntrl; raise NEWBRANCHES) 
3083  978 
else 
4300  979 
(ntried := !ntried + length prems  1; 
980 
prv(tacs', brs0::trs, choices', 

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

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

983 
if updated then 
3083  984 
(*Backtrack at this level. 
985 
Reset Vars and try another rule*) 

986 
(clearTo ntrl; deeper grls) 

987 
else (*backtrack to previous level*) 

988 
backtrack choices 

989 
end 

990 
else deeper grls 

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

993 
 closeF (L::Ls) = 

3083  994 
case tryClose(G,L) of 
15531  995 
NONE => closeF Ls 
996 
 SOME tac => 

3083  997 
let val choices' = 
14984  998 
(if !trace then (immediate_output"branch closed"; 
4065  999 
traceVars sign ntrl) 
3083  1000 
else (); 
1001 
prune (nbrs, nxtVars, 

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

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

3083  1005 
handle PRV => 
1006 
(*reset Vars and try another literal 

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

1008 
(clearTo ntrl; closeF Ls) 

1009 
end 

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

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

1013 
closeF (map fst br) 

1014 
handle CLOSEF => closeF (map fst haz) 

1015 
handle CLOSEF => closeFl pairs 

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

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

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

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

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

1024 
:: brs) 
4065  1025 
handle DEST_EQ => closeF lits 
1026 
handle CLOSEF => closeFl ((br,haz)::pairs) 

1027 
handle CLOSEF => deeper rules 

2894  1028 
handle NEWBRANCHES => 
1029 
(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

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

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

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

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

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

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

1036 
lim = lim} :: brs)) 
2894  1037 
 _ => (*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

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

1039 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1063 
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

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

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

1066 
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

1067 
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

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

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

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

1071 
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

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

1073 
"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

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

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

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

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

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

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

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

1083 
to branch.*) 

1084 
fun deeper [] = raise NEWBRANCHES 

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

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

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

1090 
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

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

1092 
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

1093 
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

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

1095 
NB: boolean "recur" affects tracing only!*) 
3083  1096 
and recur = exists (exists (match P)) prems 
1097 
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

1098 
if updated then lim  (1+log(length rules)) 
3083  1099 
else lim1 
1100 
(*It is tempting to leave "lim" UNCHANGED if 

1101 
both dup and recur are false. Proofs are 

1102 
found at shallower depths, but looping 

1103 
occurs too often...*) 

3917  1104 
val mayUndo = 
1105 
(*Allowing backtracking from a rule application 

1106 
if other matching rules exist, if the rule 

1107 
updated variables, or if the rule did not 

1108 
introduce new variables. This latter condition 

1109 
means it is not a standard "gammarule" but 

1110 
some other form of unsafe rule. Aim is to 

1111 
emulate Fast_tac, which allows all unsafe steps 

1112 
to be undone.*) 

1113 
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

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

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

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

1118 
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

1119 
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

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

1121 

3083  1122 
in 
1123 
if lim'<0 andalso not (null prems) 

1124 
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

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

1128 
traceNew prems; 
14984  1129 
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

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

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

1133 
traceVars sign ntrl; 
4300  1134 
if null prems then nclosed := !nclosed + 1 
1135 
else ntried := !ntried + length prems  1; 

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

1136 
prv(tac' :: tacs, 
3083  1137 
brs0::trs, 
1138 
(ntrl, length brs0, PRV) :: choices, 

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

1139 
newBr (vars', P, dup, lim') prems) 
3083  1140 
handle PRV => 
1141 
if mayUndo 

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

1143 
(clearTo ntrl; deeper grls) 

1144 
else (*backtrack to previous level*) 

1145 
backtrack choices 

1146 
end 

1147 
else deeper grls 

1148 
in tracing sign brs0; 

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

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

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

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

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

1157 
lim = lim} :: brs) 
2854  1158 
end 
1159 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 

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

1162 

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

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

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

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

1168 
lim = lim}; 
2854  1169 

1170 

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

1172 

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

1174 
local open Term 

1175 
in 

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

1177 
 discard_foralls t = t; 

1178 
end; 

1179 

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

1181 
fun getVars [] i = [] 

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

1183 
if i mem is then getVars alist i 

1184 
else v :: getVars alist i; 

1185 

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

1186 
exception TRANS of string; 
2854  1187 

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

1188 
(*Translation of a subgoal: Skolemize all parameters*) 
4065  1189 
fun fromSubgoal t = 
1190 
let val alistVar = ref [] 

1191 
and alistTVar = ref [] 

2854  1192 
fun hdvar ((ix,(v,is))::_) = v 
1193 
fun from lev t = 

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

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

1196 
fun bounds [] = [] 

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

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

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

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

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

1202 
"Function unknown's argument not a bound variable" 
2854  1203 
in 
1204 
case ht of 

4065  1205 
Term.Const aT => apply (fromConst alistTVar aT) 
2854  1206 
 Term.Free (a,_) => apply (Free a) 
1207 
 Term.Bound i => apply (Bound i) 

1208 
 Term.Var (ix,_) => 

17271  1209 
(case (AList.lookup (op =) (!alistVar) ix) of 
15531  1210 
NONE => (alistVar := (ix, (ref NONE, bounds ts)) 
4065  1211 
:: !alistVar; 
1212 
Var (hdvar(!alistVar))) 

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

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

1216 
^ Syntax.string_of_vname ix)) 
2854  1217 
 Term.Abs (a,_,body) => 
1218 
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

1219 
else raise TRANS "argument not in normal form" 
2854  1220 
end 
1221 

1222 
val npars = length (Logic.strip_params t) 

1223 

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

1225 
fun skoSubgoal i t = 

1226 
if i<npars then 

1227 
skoSubgoal (i+1) 

4065  1228 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854  1229 
t)) 
1230 
else t 

1231 

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

1233 

1234 

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

1235 
fun initialize thy = 
4300  1236 
(fullTrace:=[]; trail := []; ntrail := 0; 
18058
f453c2cd4408
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
wenzelm
parents:
17993
diff
changeset

1237 
nclosed := 0; ntried := 1; typargs := Sign.const_typargs thy); 
4300  1238 

1239 

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

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

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

1244 
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

1245 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1264 
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

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

1266 
handle PROVE => Seq.empty; 
2854  1267 

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

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

1269 
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

1270 

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

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

1272 

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

1273 
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

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

1275 
THEN flexflex_tac) st 
14466  1276 
handle TRANS s => 
1277 
((if !trace then warning ("blast: " ^ s) else ()); 

1278 
Seq.empty); 

2854  1279 

4078  1280 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1281 

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

1282 

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

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

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

1285 

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

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

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

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

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

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

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

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

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

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

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

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

1297 
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

1298 

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

1300 

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

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

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

1304 

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

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

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

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

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

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

1312 

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

1313 

5926  1314 
(** method setup **) 
1315 

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

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

1318 
Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; 
7155  1319 

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

7155  1322 

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

1323 
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

1324 
"tableau prover")]]; 
5926  1325 

1326 

2854  1327 
end; 