author  paulson 
Tue, 29 Aug 2017 17:41:27 +0100  
changeset 66553  6ab32ffb2bdd 
parent 63280  d2d26ff708d7 
child 69593  3dda49e08b9d 
permissions  rwrr 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1 
(* Title: Provers/blast.ML 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3083  3 
Copyright 1997 University of Cambridge 
2894  4 

5 
Generic tableau prover with proof reconstruction 

6 

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

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

12 
However, Const is heavily used for logical connectives. 

2894  13 

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

14 
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

15 
Blast_tac... 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

16 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
4651  17 
this restriction is intrinsic 
2894  18 
* ignores elimination rules that don't have the correct format 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

19 
(conclusion must be a formula variable) 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

20 
* rules must not require higherorder unification, e.g. apply_type in ZF 
61413  21 
+ message "Function unknown's argument not a bound variable" relates to this 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

24 
Known problems: 

3092  25 
"Recursive" chains of rules can sometimes exclude other unsafe formulae 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

26 
from expansion. This happens because newlycreated formulae always 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

27 
have priority over existing ones. But obviously recursive rules 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

28 
such as transitivity are treated specially to prevent this. Sometimes 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

29 
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

30 

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

31 
With substition for equalities (hyp_subst_tac): 
63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

32 
When substitution affects an unsafe formula or literal, it is moved 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

34 
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

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

38 
signature BLAST_DATA = 

32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32174
diff
changeset

39 
sig 
42477  40 
structure Classical: CLASSICAL 
42802  41 
val Trueprop_const: string * typ 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

42 
val equality_name: string 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

43 
val not_name: string 
42477  44 
val notE: thm (* [ ~P; P ] ==> R *) 
45 
val ccontr: thm 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

46 
val hyp_subst_tac: Proof.context > bool > int > tactic 
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32174
diff
changeset

47 
end; 
2854  48 

49 
signature BLAST = 

32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32174
diff
changeset

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

51 
exception TRANS of string (*reports translation errors*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

52 
datatype term = 
18177  53 
Const of string * term list 
32740  54 
 Skolem of string * term option Unsynchronized.ref list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

55 
 Free of string 
32740  56 
 Var of term option Unsynchronized.ref 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

58 
 Abs of string*term 
17795  59 
 $ of term*term; 
42793  60 
val depth_tac: Proof.context > int > int > tactic 
42477  61 
val depth_limit: int Config.T 
43349  62 
val trace: bool Config.T 
63 
val stats: bool Config.T 

42793  64 
val blast_tac: Proof.context > int > tactic 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

65 
(*debugging tools*) 
42477  66 
type branch 
42793  67 
val tryIt: Proof.context > int > string > 
42804  68 
{fullTrace: branch list list, 
69 
result: ((int > tactic) list * branch list list * (int * int * exn) list)} 

32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32174
diff
changeset

70 
end; 
2854  71 

42477  72 
functor Blast(Data: BLAST_DATA): BLAST = 
2854  73 
struct 
74 

42477  75 
structure Classical = Data.Classical; 
2854  76 

43346  77 
(* options *) 
78 

58826  79 
val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20); 
53536
69c943125fd3
do not expose internal flags to attribute name space;
wenzelm
parents:
46715
diff
changeset

80 
val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false); 
69c943125fd3
do not expose internal flags to attribute name space;
wenzelm
parents:
46715
diff
changeset

81 
val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false); 
43346  82 

2854  83 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

84 
datatype term = 
63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

85 
Const of string * term list (*typargs constantas a term!*) 
32740  86 
 Skolem of string * term option Unsynchronized.ref list 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

87 
 Free of string 
32740  88 
 Var of term option Unsynchronized.ref 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

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

90 
 Abs of string*term 
5613  91 
 op $ of term*term; 
2854  92 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

93 
(*Pending formulae carry md (may duplicate) flags*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

94 
type branch = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

95 
{pairs: ((term*bool) list * (*safe formulae on this level*) 
60943  96 
(term*bool) list) list, (*unsafe formulae on this level*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

97 
lits: term list, (*literals: irreducible formulae*) 
32740  98 
vars: term option Unsynchronized.ref list, (*variables occurring in branch*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

99 
lim: int}; (*resource limit*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

100 

845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

101 

845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

102 
(* global state information *) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

103 

845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

104 
datatype state = State of 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

105 
{ctxt: Proof.context, 
43349  106 
names: Name.context Unsynchronized.ref, 
32740  107 
fullTrace: branch list list Unsynchronized.ref, 
108 
trail: term option Unsynchronized.ref list Unsynchronized.ref, 

109 
ntrail: int Unsynchronized.ref, 

110 
nclosed: int Unsynchronized.ref, 

111 
ntried: int Unsynchronized.ref} 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

112 

63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

113 
fun reserved_const thy c = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

114 
is_some (Sign.const_type thy c) andalso 
63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

115 
error ("blast: theory contains reserved constant " ^ quote c); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

116 

42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

117 
fun initialize ctxt = 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

118 
let 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

119 
val thy = Proof_Context.theory_of ctxt; 
63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

120 
val _ = reserved_const thy "*Goal*"; 
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

121 
val _ = reserved_const thy "*False*"; 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

122 
in 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

123 
State 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

124 
{ctxt = ctxt, 
43349  125 
names = Unsynchronized.ref (Variable.names_of ctxt), 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

126 
fullTrace = Unsynchronized.ref [], 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

127 
trail = Unsynchronized.ref [], 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

128 
ntrail = Unsynchronized.ref 0, 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

129 
nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*) 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

130 
ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

131 
end; 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

132 

43349  133 
fun gensym (State {names, ...}) x = 
134 
Unsynchronized.change_result names (Name.variant x); 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

135 

2854  136 

137 
(** Basic syntactic operations **) 

138 

139 
fun is_Var (Var _) = true 

140 
 is_Var _ = false; 

141 

142 
fun dest_Var (Var x) = x; 

143 

144 
fun rand (f$x) = x; 

145 

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

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

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

150 
fun strip_comb u : term * term list = 
2854  151 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

152 
 stripc x = x 
2854  153 
in stripc(u,[]) end; 
154 

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

156 
fun head_of (f$t) = head_of f 

157 
 head_of u = u; 

158 

159 

160 
(** Particular constants **) 

161 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

162 
fun negate P = Const (Data.not_name, []) $ P; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

163 

ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

164 
fun isNot (Const (c, _) $ _) = c = Data.not_name 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

165 
 isNot _ = false; 
2854  166 

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

18177  169 
fun isGoal (Const ("*Goal*", _) $ _) = true 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

170 
 isGoal _ = false; 
2854  171 

42802  172 
val (TruepropC, TruepropT) = Data.Trueprop_const; 
18171  173 

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

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

178 

2854  179 

180 

4065  181 
(*** Dealing with overloaded constants ***) 
2854  182 

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

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

188 
(case (AList.lookup (op =) (!alist) ixn) of 
32740  189 
NONE => let val t' = Var (Unsynchronized.ref NONE) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

190 
in alist := (ixn, t') :: !alist; t' 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

191 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

192 
 SOME v => v) 
2854  193 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

194 
fun fromConst thy alist (a, T) = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

195 
Const (a, map (fromType alist) (Sign.const_typargs thy (a, T))); 
2854  196 

197 

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

32740  199 
fun (Const (a, ts)) aconv (Const (b, us)) = a = b andalso aconvs (ts, us) 
200 
 (Skolem (a,_)) aconv (Skolem (b,_)) = a = b (*arglists must then be equal*) 

201 
 (Free a) aconv (Free b) = a = b 

202 
 (Var (Unsynchronized.ref(SOME t))) aconv u = t aconv u 

203 
 t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

204 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
2854  205 
 (Bound i) aconv (Bound j) = i=j 
206 
 (Abs(_,t)) aconv (Abs(_,u)) = t aconv u 

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

18177  208 
 _ aconv _ = false 
209 
and aconvs ([], []) = true 

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

211 
 aconvs _ = false; 

2854  212 

213 

214 
fun mem_term (_, []) = false 

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

216 

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

218 

32740  219 
fun mem_var (v: term option Unsynchronized.ref, []) = false 
2854  220 
 mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); 
221 

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

223 

224 

225 
(** Vars **) 

226 

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

32740  228 
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) 
229 
 add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars) 

230 
 add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars) 

231 
 add_term_vars (Const (_, ts), vars) = add_terms_vars (ts, vars) 

232 
 add_term_vars (Abs (_, body), vars) = add_term_vars (body, vars) 

233 
 add_term_vars (f $ t, vars) = add_term_vars (f, add_term_vars (t, vars)) 

234 
 add_term_vars (_, vars) = vars 

2854  235 
(*Term list version. [The fold functionals are slow]*) 
236 
and add_terms_vars ([], vars) = vars 

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

238 
(*Var list version.*) 

32740  239 
and add_vars_vars ([], vars) = vars 
240 
 add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) = 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

241 
add_vars_vars (vs, add_term_vars(u,vars)) 
15531  242 
 add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

243 
add_vars_vars (vs, ins_var (v, vars)); 
2854  244 

245 

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

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

248 

249 

250 

251 
(*increment a term's nonlocal bound variables 

252 
inc is increment for bound variables 

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

254 
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
2854  255 
 incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body)) 
256 
 incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

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

258 

259 
fun incr_boundvars 0 t = t 

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

261 

262 

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

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

265 
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js 
20854  266 
else insert (op =) (i  lev) js 
2854  267 
 add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
268 
 add_loose_bnos (f$t, lev, js) = 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

269 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
2854  270 
 add_loose_bnos (_, _, js) = js; 
271 

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

273 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

274 
fun subst_bound (arg, t) : term = 
2854  275 
let fun subst (t as Bound i, lev) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

276 
if i<lev then t (*var is locally bound*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

277 
else if i=lev then incr_boundvars lev arg 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

278 
else Bound(i1) (*loose: change it*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

279 
 subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

280 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

281 
 subst (t,lev) = t 
2854  282 
in subst (t,0) end; 
283 

284 

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

285 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  286 
fun norm t = case t of 
32740  287 
Skolem (a, args) => Skolem (a, vars_in_vars args) 
288 
 Const (a, ts) => Const (a, map norm ts) 

289 
 (Var (Unsynchronized.ref NONE)) => t 

290 
 (Var (Unsynchronized.ref (SOME u))) => norm u 

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

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

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

296 

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

298 
fun wkNormAux t = case t of 

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

300 
SOME u => wkNorm u 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

301 
 NONE => t) 
2854  302 
 (f $ u) => (case wkNormAux f of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

303 
Abs(_,body) => wkNorm (subst_bound (u, body)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

304 
 nf => nf $ u) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

305 
 Abs (a,body) => (*etacontract if possible*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

306 
(case wkNormAux body of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

307 
nb as (f $ t) => 
20664  308 
if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

309 
then Abs(a,nb) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

310 
else wkNorm (incr_boundvars ~1 f) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

314 
Const _ => t 

315 
 Skolem(a,args) => t 

316 
 Free _ => t 

317 
 _ => wkNormAux t; 

318 

319 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

321 
Dangling bound vars are also forbidden.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

322 
fun varOccur v = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

323 
let fun occL lev [] = false (*same as (exists occ), but faster*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

324 
 occL lev (u::us) = occ lev u orelse occL lev us 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

325 
and occ lev (Var w) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

326 
v=w orelse 
15531  327 
(case !w of NONE => false 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

328 
 SOME u => occ lev u) 
5734
bebd10cb7a8d
occurs check now handles Bound variables (for soundness)
paulson
parents:
5613
diff
changeset

329 
 occ lev (Skolem(_,args)) = occL lev (map Var args) 
18177  330 
(*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

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

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

333 
 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

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

335 
in occ 0 end; 
2854  336 

337 
exception UNIFY; 

338 

339 

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

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

341 
fun clearTo (State {ntrail, trail, ...}) n = 
3083  342 
while !ntrail<>n do 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

343 
(hd(!trail) := NONE; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

344 
trail := tl (!trail); 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

345 
ntrail := !ntrail  1); 
2854  346 

347 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

348 
(*Firstorder unification with bound variables. 
2854  349 
"vars" is a list of variables local to the rule and NOT to be put 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

350 
on the trail (no point in doing so) 
2854  351 
*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

352 
fun unify state (vars,t,u) = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

353 
let val State {ntrail, trail, ...} = state 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

354 
val n = !ntrail 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

355 
fun update (t as Var v, u) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

356 
if t aconv u then () 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

357 
else if varOccur v u then raise UNIFY 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

358 
else if mem_var(v, vars) then v := SOME u 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

359 
else (*avoid updating Vars in the branch if possible!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

360 
if is_Var u andalso mem_var(dest_Var u, vars) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

361 
then dest_Var u := SOME t 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

362 
else (v := SOME u; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

363 
trail := v :: !trail; ntrail := !ntrail + 1) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

364 
fun unifyAux (t,u) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

365 
case (wkNorm t, wkNorm u) of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

366 
(nt as Var v, nu) => update(nt,nu) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

367 
 (nu, nt as Var v) => update(nt,nu) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

368 
 (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

369 
else raise UNIFY 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

370 
 (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

371 
(*NB: can yield unifiers having dangling Bound vars!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

372 
 (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

373 
 (nt, nu) => if nt aconv nu then () else raise UNIFY 
18177  374 
and unifysAux ([], []) = () 
375 
 unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us)) 

376 
 unifysAux _ = raise UNIFY; 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

380 

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

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

382 
Code is similar to fromSubgoal.*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

383 
fun fromTerm thy t = 
32740  384 
let val alistVar = Unsynchronized.ref [] 
385 
and alistTVar = Unsynchronized.ref [] 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

386 
fun from (Term.Const aT) = fromConst thy alistTVar aT 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

387 
 from (Term.Free (a,_)) = Free a 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

388 
 from (Term.Bound i) = Bound i 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

389 
 from (Term.Var (ixn,T)) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

390 
(case (AList.lookup (op =) (!alistVar) ixn) of 
32740  391 
NONE => let val t' = Var (Unsynchronized.ref NONE) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

392 
in alistVar := (ixn, t') :: !alistVar; t' 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

393 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

394 
 SOME v => v) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

395 
 from (Term.Abs (a,_,u)) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

396 
(case from u of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

397 
u' as (f $ Bound 0) => 
20664  398 
if member (op =) (loose_bnos f) 0 then Abs(a,u') 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

399 
else incr_boundvars ~1 f 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

400 
 u' => Abs(a,u')) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

401 
 from (Term.$ (f,u)) = from f $ from u 
2854  402 
in from t end; 
403 

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

406 
fun instVars t = 

32740  407 
let val name = Unsynchronized.ref "a" 
408 
val updated = Unsynchronized.ref [] 

18177  409 
fun inst (Const(a,ts)) = List.app inst ts 
32740  410 
 inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

411 
v := SOME (Free ("?" ^ !name)); 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

412 
name := Symbol.bump_string (!name)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

413 
 inst (Abs(a,t)) = inst t 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

414 
 inst (f $ u) = (inst f; inst u) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

419 

2854  420 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
56245  421 
fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) = 
422 
strip_Trueprop A :: strip_imp_prems B 

2854  423 
 strip_imp_prems _ = []; 
424 

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

56245  426 
fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B 
18177  427 
 strip_imp_concl A = strip_Trueprop A; 
428 

2854  429 

430 

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

432 

9170  433 
exception ElimBadConcl and ElimBadPrem; 
434 

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

436 
If we don't find it then the premise is illformed and could cause 
9170  437 
PROOF FAILED*) 
438 
fun delete_concl [] = raise ElimBadPrem 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

439 
 delete_concl (P :: Ps) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

440 
(case P of 
32740  441 
Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) => 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

442 
if c = "*Goal*" orelse c = Data.not_name then Ps 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

443 
else P :: delete_concl Ps 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

444 
 _ => P :: delete_concl Ps); 
2854  445 

56245  446 
fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) = 
43349  447 
skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P)) 
448 
 skoPrem _ _ P = P; 

2854  449 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

450 
fun convertPrem t = 
9170  451 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  452 

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

43349  454 
fun convertRule state vars t = 
2854  455 
let val (P::Ps) = strip_imp_prems t 
456 
val Var v = strip_imp_concl t 

18177  457 
in v := SOME (Const ("*False*", [])); 
43349  458 
(P, map (convertPrem o skoPrem state vars) Ps) 
9170  459 
end 
460 
handle Bind => raise ElimBadConcl; 

2854  461 

462 

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

58958  464 
fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) > Thm.assumption (SOME ctxt) 2 > Seq.hd; 
2854  465 

466 

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

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

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

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

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

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

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

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

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

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

478 
fun rot_subgoals_tac (rot, rl) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

481 

2854  482 

54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

483 
fun cond_tracing true msg = tracing (msg ()) 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

484 
 cond_tracing false _ = (); 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

485 

42804  486 
fun TRACE ctxt rl tac i st = 
61268  487 
(cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st); 
2854  488 

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

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

490 
Matching makes the tactics more deterministic in the presence of Vars.*) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

491 
fun emtac ctxt upd rl = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

492 
TRACE ctxt rl (if upd then eresolve_tac ctxt [rl] else ematch_tac ctxt [rl]); 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

493 

50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

494 
fun rmtac ctxt upd rl = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

495 
TRACE ctxt rl (if upd then resolve_tac ctxt [rl] else match_tac ctxt [rl]); 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

496 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

498 
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

499 
Flag "dup" requests duplication of the affected formula.*) 
61056  500 
fun fromRule (state as State {ctxt, ...}) vars rl0 = 
501 
let 

502 
val thy = Proof_Context.theory_of ctxt 

503 
val rl = Thm.transfer thy rl0 

504 
val trl = rl > Thm.prop_of > fromTerm thy > convertRule state vars 

505 
fun tac (upd, dup,rot) i = 

506 
emtac ctxt upd (if dup then rev_dup_elim ctxt rl else rl) i THEN 

507 
rot_subgoals_tac (rot, #2 trl) i 

508 
in SOME (trl, tac) end 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

509 
handle 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

510 
ElimBadPrem => (*reject: prems don't preserve conclusion*) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

511 
(if Context_Position.is_visible ctxt then 
61268  512 
warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

513 
else (); 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

514 
Option.NONE) 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

515 
 ElimBadConcl => (*ignore: conclusion is not just a variable*) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

516 
(cond_tracing (Config.get ctxt trace) 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

517 
(fn () => "Ignoring illformed elimination rule:\n" ^ 
61268  518 
"conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0); 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

519 
Option.NONE); 
2854  520 

521 

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

522 
(*** Conversion of Introduction Rules ***) 
2854  523 

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

525 

43349  526 
fun convertIntrRule state vars t = 
2854  527 
let val Ps = strip_imp_prems t 
528 
val P = strip_imp_concl t 

43349  529 
in (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps) 
2854  530 
end; 
531 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

533 
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

534 
Flag "dup" requests duplication of the affected formula. 
60943  535 
Since unsafe rules are now delayed, "dup" is always FALSE for 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

536 
introduction rules.*) 
61056  537 
fun fromIntrRule (state as State {ctxt, ...}) vars rl0 = 
538 
let 

539 
val thy = Proof_Context.theory_of ctxt 

540 
val rl = Thm.transfer thy rl0 

541 
val trl = rl > Thm.prop_of > fromTerm thy > convertIntrRule state vars 

542 
fun tac (upd,dup,rot) i = 

543 
rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i THEN 

544 
rot_subgoals_tac (rot, #2 trl) i 

2854  545 
in (trl, tac) end; 
546 

547 

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

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

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

552 
fun toTerm 0 _ = dummyVar 
18177  553 
 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

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

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

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

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

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

559 
 toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d1) u); 
2854  560 

63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

561 
(*Too flexible assertions or goals. Motivated by examples such as "(\<And>P. ~P) \<Longrightarrow> 0==1"*) 
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

562 
fun isVarForm (Var _) = true 
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

563 
 isVarForm (Const (c, _) $ Var _) = (c = Data.not_name) 
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

564 
 isVarForm _ = false; 
2854  565 

43349  566 
fun netMkRules state P vars (nps: Classical.netpair list) = 
2854  567 
case P of 
18177  568 
(Const ("*Goal*", _) $ G) => 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

569 
let val pG = mk_Trueprop (toTerm 2 G) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19037
diff
changeset

570 
val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps 
43349  571 
in map (fromIntrRule state vars o #2) (order_list intrs) end 
2854  572 
 _ => 
63265
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

573 
if isVarForm P then [] (*The formula is too flexible, reject*) 
9a2377b96ffd
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
paulson <lp15@cam.ac.uk>
parents:
61413
diff
changeset

574 
else 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

575 
let val pP = mk_Trueprop (toTerm 3 P) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19037
diff
changeset

576 
val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps 
43349  577 
in map_filter (fromRule state vars o #2) (order_list elims) end; 
3092  578 

579 

580 
(*Normalize a branchfor tracing*) 

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

582 

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

584 

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

585 
fun normBr {pairs, lits, vars, lim} = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

586 
{pairs = map normLev pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

587 
lits = map norm lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

589 
lim = lim}; 
3092  590 

591 

4065  592 
val dummyTVar = Term.TVar(("a",0), []); 
3092  593 
val dummyVar2 = Term.Var(("var",0), dummyT); 
594 

26938  595 
(*convert blast_tac's type representation to real types for tracing*) 
4065  596 
fun showType (Free a) = Term.TFree (a,[]) 
597 
 showType (Var _) = dummyTVar 

598 
 showType t = 

599 
(case strip_comb t of 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

600 
(Const (a, _), us) => Term.Type(a, map showType us) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

601 
 _ => dummyT); 
4065  602 

603 
(*Display toplevel overloading if any*) 

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

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

607 
 topType _ _ = NONE; 

4065  608 

609 

3092  610 
(*Convert from prototerms to ordinary terms with dummy types for tracing*) 
18177  611 
fun showTerm d (Const (a,_)) = Term.Const (a,dummyT) 
3092  612 
 showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 
32740  613 
 showTerm d (Free a) = Term.Free (a,dummyT) 
614 
 showTerm d (Bound i) = Term.Bound i 

615 
 showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u 

616 
 showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2 

3092  617 
 showTerm d (Abs(a,t)) = if d=0 then dummyVar 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

618 
else Term.Abs(a, dummyT, showTerm (d1) t) 
3092  619 
 showTerm d (f $ u) = if d=0 then dummyVar 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

620 
else Term.$ (showTerm d f, showTerm (d1) u); 
3092  621 

42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

622 
fun string_of ctxt d t = Syntax.string_of_term ctxt (showTerm d t); 
3092  623 

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

626 
fun negOfGoal (Const ("*Goal*", _) $ G) = negate G 

627 
 negOfGoal G = G; 

628 

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

630 

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

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

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

60943  634 
fun negOfGoals pairs = map (fn (Gs, unsafe) => (map negOfGoal2 Gs, unsafe)) pairs; 
19037  635 

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

42804  637 
fun negOfGoal_tac ctxt i = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

638 
TRACE ctxt Data.ccontr (resolve_tac ctxt [Data.ccontr]) i THEN rotate_tac ~1 i; 
19037  639 

42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

640 
fun traceTerm ctxt t = 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

641 
let val thy = Proof_Context.theory_of ctxt 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

642 
val t' = norm (negOfGoal t) 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

643 
val stm = string_of ctxt 8 t' 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

644 
in 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

645 
case topType thy t' of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

646 
NONE => stm (*no type to attach*) 
54943
1276861f2724
avoid hard tabs in output  somewhat illdefined;
wenzelm
parents:
54942
diff
changeset

647 
 SOME T => stm ^ " :: " ^ Syntax.string_of_typ ctxt T 
4065  648 
end; 
3092  649 

650 

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

54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

652 
fun trace_prover (State {ctxt, fullTrace, ...}) brs = 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

653 
let fun printPairs (((G,_)::_,_)::_) = tracing (traceTerm ctxt G) 
54943
1276861f2724
avoid hard tabs in output  somewhat illdefined;
wenzelm
parents:
54942
diff
changeset

654 
 printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ " (Unsafe)") 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

656 
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

657 
(fullTrace := brs0 :: !fullTrace; 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

658 
List.app (fn _ => tracing "+") brs; 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

659 
tracing (" [" ^ string_of_int lim ^ "] "); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

660 
printPairs pairs; 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

661 
tracing "") 
42804  662 
in if Config.get ctxt trace then printBrs (map normBr brs) else () end; 
3092  663 

664 
(*Tracing: variables updated in the last branch operation?*) 

42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

665 
fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl = 
42804  666 
if Config.get ctxt trace then 
4065  667 
(case !ntrailntrl of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

668 
0 => () 
54943
1276861f2724
avoid hard tabs in output  somewhat illdefined;
wenzelm
parents:
54942
diff
changeset

669 
 1 => tracing " 1 variable UPDATED:" 
1276861f2724
avoid hard tabs in output  somewhat illdefined;
wenzelm
parents:
54942
diff
changeset

670 
 n => tracing (" " ^ string_of_int n ^ " variables UPDATED:"); 
4065  671 
(*display the instantiations themselves, though no variable names*) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

672 
List.app (fn v => tracing (" " ^ string_of ctxt 4 (the (!v)))) 
4065  673 
(List.take(!trail, !ntrailntrl)); 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

674 
tracing "") 
3092  675 
else (); 
676 

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

42804  678 
fun traceNew true prems = 
679 
(case length prems of 

54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

680 
0 => tracing "branch closed by rule" 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

681 
 1 => tracing "branch extended (1 new subgoal)" 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

682 
 n => tracing ("branch split: "^ string_of_int n ^ " new subgoals")) 
42804  683 
 traceNew _ _ = (); 
3092  684 

685 

686 

2854  687 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
688 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

689 
(*Replace the ATOMIC term "old" by "new" in t*) 
2854  690 
fun subst_atomic (old,new) t = 
32740  691 
let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u 
692 
 subst (Abs(a,body)) = Abs(a, subst body) 

693 
 subst (f$t) = subst f $ subst t 

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

2854  695 
in subst t end; 
696 

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

698 
fun eta_contract_atom (t0 as Abs(a, body)) = 
2854  699 
(case eta_contract2 body of 
20664  700 
f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

701 
else eta_contract_atom (incr_boundvars ~1 f) 
2854  702 
 _ => t0) 
703 
 eta_contract_atom t = t 

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

705 
 eta_contract2 t = eta_contract_atom t; 

706 

707 

708 
(*When can we safely delete the equality? 

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

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

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

712 
Prefer to eliminate Bound variables if possible. 

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

714 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

716 
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

717 
REFLEXIVE because hyp_subst_tac fails on x=x.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

718 
fun substOccur t = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

720 
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

721 
be instantiated to a cycle. For example, x=?a is rejected because ?a 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

724 
Skolem(_,vars) => vars 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

726 
fun occEq u = (t aconv u) orelse occ u 
32740  727 
and occ (Var(Unsynchronized.ref(SOME u))) = occEq u 
728 
 occ (Var v) = not (mem_var (v, vars)) 

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

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

731 
 occ _ = false; 

2854  732 
in occEq end; 
733 

3092  734 
exception DEST_EQ; 
735 

18177  736 
(*Take apart an equality. NO constant Trueprop*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

737 
fun dest_eq (Const (c, _) $ t $ u) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

738 
if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

739 
else raise DEST_EQ 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

740 
 dest_eq _ = raise DEST_EQ; 
3092  741 

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

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

745 
(*IF the goal is an equality with a substitutable variable 
2854  746 
THEN orient that equality ELSE raise exception DEST_EQ*) 
3092  747 
fun orientGoal (t,u) = case (t,u) of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

748 
(Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

749 
 (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

750 
 (Free _, _) => check(t,u,(t,u)) (*eliminates t*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

751 
 (_, Free _) => check(u,t,(u,t)) (*eliminates u*) 
2854  752 
 _ => raise DEST_EQ; 
753 

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

756 
they should go: this could make proofs fail.*) 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

757 
fun equalSubst ctxt (G, {pairs, lits, vars, lim}) = 
3092  758 
let val (t,u) = orientGoal(dest_eq G) 
759 
val subst = subst_atomic (t,u) 

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

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

762 
fun subForm ((G,md), (changed, pairs)) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

763 
let val nG = subst G 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

764 
in if nG aconv G then (changed, (G,md)::pairs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

768 
fun subFrame ((Gs,Hs), (changed, frames)) = 
30190  769 
let val (changed', Gs') = List.foldr subForm (changed, []) Gs 
770 
val (changed'', Hs') = List.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

771 
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

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

773 
fun subLit (lit, (changed, nlits)) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

774 
let val nlit = subst lit 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

775 
in if nlit aconv lit then (changed, nlit::nlits) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

776 
else ((nlit,true)::changed, nlits) 
2854  777 
end 
30190  778 
val (changed, lits') = List.foldr subLit ([], []) lits 
779 
val (changed', pairs') = List.foldr subFrame (changed, []) pairs 

54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

780 
in if Config.get ctxt trace then tracing ("Substituting " ^ traceTerm ctxt u ^ 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

781 
" for " ^ traceTerm ctxt t ^ " in branch" ) 
3092  782 
else (); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

783 
{pairs = (changed',[])::pairs', (*affected formulas, and others*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

784 
lits = lits', (*unaffected literals*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

786 
lim = lim} 
2854  787 
end; 
788 

789 

790 
exception NEWBRANCHES and CLOSEF; 

791 

792 
exception PROVE; 

793 

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

794 
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) 
58957  795 
fun contr_tac ctxt = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

796 
ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); 
2854  797 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

798 
(*Try to unify complementary literals and return the corresponding tactic. *) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

799 
fun tryClose state (G, L) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

800 
let 
42804  801 
val State {ctxt, ...} = state; 
802 
val eContr_tac = TRACE ctxt Data.notE contr_tac; 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

803 
val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac ctxt); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

804 
fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

805 
fun arg (_ $ t) = t; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

806 
in 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

807 
if isGoal G then close (arg G) L eAssume_tac 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

808 
else if isGoal L then close G (arg L) eAssume_tac 
58957  809 
else if isNot G then close (arg G) L (eContr_tac ctxt) 
810 
else if isNot L then close G (arg L) (eContr_tac ctxt) 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

811 
else NONE 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

812 
end; 
2854  813 

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

815 
fun hasSkolem (Skolem _) = true 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

816 
 hasSkolem (Abs (_,body)) = hasSkolem body 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

817 
 hasSkolem (f$t) = hasSkolem f orelse hasSkolem t 
2854  818 
 hasSkolem _ = false; 
819 

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

821 
Skolem terms then allow duplication.*) 

822 
fun joinMd md [] = [] 

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

824 

825 

826 
(** Backtracking and Pruning **) 

827 

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

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

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

831 
 clashVar vars = 

832 
let fun clash (0, _) = false 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

833 
 clash (_, []) = false 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

834 
 clash (n, v::vs) = exists (varOccur v) vars orelse clash(n1,vs) 
2854  835 
in clash end; 
836 

837 

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

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

840 
next branch have been updated.*) 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

841 
fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

842 
backtracking over bad proofs*) 
42804  843 
 prune (State {ctxt, ntrail, trail, ...}) (nbrs: int, nxtVars, choices) = 
2854  844 
let fun traceIt last = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

845 
let val ll = length last 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

846 
and lc = length choices 
42804  847 
in if Config.get ctxt trace andalso ll<lc then 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

848 
(tracing ("Pruning " ^ string_of_int(lcll) ^ " levels"); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

849 
last) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

850 
else last 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

851 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

852 
fun pruneAux (last, _, _, []) = last 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

853 
 pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

854 
if nbrs' < nbrs 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

855 
then last (*don't backtrack beyond first solution of goal*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

856 
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

857 
else (* nbrs'=nbrs *) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

858 
if clashVar nxtVars (ntrlntrl', trl) then last 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

859 
else (*no clashes: can go back at least this far!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

860 
pruneAux(choices, ntrl', List.drop(trl, ntrlntrl'), 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

865 
 nextVars [] = []; 
2854  866 

42804  867 
fun backtrack trace (choices as (ntrl, nbrs, exn)::_) = 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

868 
(cond_tracing trace 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

869 
(fn () => "Backtracking; now there are " ^ string_of_int nbrs ^ " branches"); 
3083  870 
raise exn) 
42804  871 
 backtrack _ _ = raise PROVE; 
2854  872 

2894  873 
(*Add the literal G, handling *Goal* and detecting duplicates.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

874 
fun addLit (Const ("*Goal*", _) $ G, lits) = 
2894  875 
(*New literal is a *Goal*, so change all other Goals to Nots*) 
18177  876 
let fun bad (Const ("*Goal*", _) $ _) = true 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

877 
 bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G' 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

878 
 bad _ = false; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

879 
fun change [] = [] 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

880 
 change (lit :: lits) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

881 
(case lit of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

882 
Const (c, _) $ G' => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

883 
if c = "*Goal*" orelse c = Data.not_name then 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

884 
if G aconv G' then change lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

885 
else negate G' :: change lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

886 
else lit :: change lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

887 
 _ => lit :: change lits) 
2854  888 
in 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

889 
Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits) 
2854  890 
end 
891 
 addLit (G,lits) = ins_term(G, lits) 

892 

893 

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

3083  896 
fun log n = if n<4 then 0 else 1 + log(n div 4); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

897 

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

898 

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

899 
(*match(t,u) says whether the term u might be an instance of the pattern t 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

900 
Used to detect "recursive" rules such as transitivity*) 
39806db47be9
Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents:
2999
diff
changeset

901 
fun match (Var _) u = true 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

902 
 match (Const (a,tas)) (Const (b,tbs)) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

903 
a = "*Goal*" andalso b = Data.not_name orelse 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

904 
a = Data.not_name andalso b = "*Goal*" orelse 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

905 
a = b andalso matchs tas tbs 
4065  906 
 match (Free a) (Free b) = (a=b) 
907 
 match (Bound i) (Bound j) = (i=j) 

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

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

18177  910 
 match t u = false 
911 
and matchs [] [] = true 

912 
 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

913 

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

914 

24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

915 
fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

916 
if b then 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

917 
tracing (Timing.message (Timing.result start) ^ " for search. Closed: " 
41491  918 
^ string_of_int (!nclosed) ^ 
919 
" tried: " ^ string_of_int (!ntried) ^ 

920 
" tactics: " ^ string_of_int (length tacs)) 

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

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

922 

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

923 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

924 
(*Tableau prover based on leanTaP. Argument is a list of branches. Each 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

925 
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

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

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

928 
*) 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

929 
fun prove (state, start, brs, cont) = 
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

930 
let val State {ctxt, ntrail, nclosed, ntried, ...} = state; 
42804  931 
val trace = Config.get ctxt trace; 
932 
val stats = Config.get ctxt stats; 

60943  933 
val {safe0_netpair, safep_netpair, unsafe_netpair, ...} = 
42793  934 
Classical.rep_cs (Classical.claset_of ctxt); 
60943  935 
val safeList = [safe0_netpair, safep_netpair]; 
936 
val unsafeList = [unsafe_netpair]; 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

937 
fun prv (tacs, trs, choices, []) = 
42804  938 
(printStats state (trace orelse stats, start, tacs); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

939 
cont (tacs, trs, choices)) (*all branches closed!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

940 
 prv (tacs, trs, choices, 
60943  941 
brs0 as {pairs = ((G,md)::br, unsafe)::pairs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

942 
lits, vars, lim} :: brs) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

943 
(*apply a safe rule only (possibly allowing instantiation); 
60943  944 
defer any unsafe formulae*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

945 
let exception PRV (*backtrack to precisely this recursion!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

946 
val ntrl = !ntrail 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

947 
val nbrs = length brs0 
2854  948 
val nxtVars = nextVars brs 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

949 
val G = norm G 
43349  950 
val rules = netMkRules state G vars safeList 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

951 
(*Make a new branch, decrementing "lim" if instantiations occur*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

952 
fun newBr (vars',lim') prems = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

953 
map (fn prem => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

954 
if (exists isGoal prem) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

955 
then {pairs = ((joinMd md prem, []) :: 
60943  956 
negOfGoals ((br, unsafe)::pairs)), 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

957 
lits = map negOfGoal lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

958 
vars = vars', 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

959 
lim = lim'} 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

960 
else {pairs = ((joinMd md prem, []) :: 
60943  961 
(br, unsafe) :: pairs), 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

962 
lits = lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

963 
vars = vars', 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

964 
lim = lim'}) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

965 
prems @ 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

966 
brs 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

967 
(*Seek a matching rule. If unifiable then add new premises 
2854  968 
to branch.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

969 
fun deeper [] = raise NEWBRANCHES 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

970 
 deeper (((P,prems),tac)::grls) = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

971 
if unify state (add_term_vars(P,[]), P, G) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

972 
then (*P comes from the rule; G comes from the branch.*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

973 
let val updated = ntrl < !ntrail (*branch updated*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

974 
val lim' = if updated 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

975 
then lim  (1+log(length rules)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

976 
else lim (*discourage branching updates*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

977 
val vars = vars_in_vars vars 
30190  978 
val vars' = List.foldr add_terms_vars vars prems 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

979 
val choices' = (ntrl, nbrs, PRV) :: choices 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

981 
:: tacs (*no duplication; rotate*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

982 
in 
42804  983 
traceNew trace prems; traceVars state ntrl; 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

984 
(if null prems then (*closed the branch: prune!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

985 
(nclosed := !nclosed + 1; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

986 
prv(tacs', brs0::trs, 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

987 
prune state (nbrs, nxtVars, choices'), 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

988 
brs)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

989 
else (*prems nonnull*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

990 
if lim'<0 (*faster to kill ALL the alternatives*) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

991 
then (cond_tracing trace (fn () => "Excessive branching: KILLED"); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

992 
clearTo state ntrl; raise NEWBRANCHES) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

993 
else 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

994 
(ntried := !ntried + length prems  1; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

995 
prv(tacs', brs0::trs, choices', 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

996 
newBr (vars',lim') prems))) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

997 
handle PRV => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

998 
if updated then 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

999 
(*Backtrack at this level. 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1000 
Reset Vars and try another rule*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1001 
(clearTo state ntrl; deeper grls) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1002 
else (*backtrack to previous level*) 
42804  1003 
backtrack trace choices 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1004 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1005 
else deeper grls 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1006 
(*Try to close branch by unifying with head goal*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1007 
fun closeF [] = raise CLOSEF 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1008 
 closeF (L::Ls) = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1009 
case tryClose state (G,L) of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1010 
NONE => closeF Ls 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1011 
 SOME tac => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1012 
let val choices' = 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1013 
(if trace then (tracing "branch closed"; 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1014 
traceVars state ntrl) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1015 
else (); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1016 
prune state (nbrs, nxtVars, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1017 
(ntrl, nbrs, PRV) :: choices)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1018 
in nclosed := !nclosed + 1; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1019 
prv (tac::tacs, brs0::trs, choices', brs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1020 
handle PRV => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1021 
(*reset Vars and try another literal 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1022 
[this handler is pruned if possible!]*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1023 
(clearTo state ntrl; closeF Ls) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1024 
end 
60943  1025 
(*Try to unify a queued formula (safe or unsafe) with head goal*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1026 
fun closeFl [] = raise CLOSEF 
60943  1027 
 closeFl ((br, unsafe)::pairs) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1028 
closeF (map fst br) 
60943  1029 
handle CLOSEF => closeF (map fst unsafe) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1030 
handle CLOSEF => closeFl pairs 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1031 
in 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1032 
trace_prover state brs0; 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1033 
if lim<0 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1034 
else 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

1035 
prv (Data.hyp_subst_tac ctxt trace :: tacs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1036 
brs0::trs, choices, 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

1037 
equalSubst ctxt 
60943  1038 
(G, {pairs = (br,unsafe)::pairs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1039 
lits = lits, vars = vars, lim = lim}) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1040 
:: brs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1041 
handle DEST_EQ => closeF lits 
60943  1042 
handle CLOSEF => closeFl ((br,unsafe)::pairs) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1043 
handle CLOSEF => deeper rules 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1044 
handle NEWBRANCHES => 
60943  1045 
(case netMkRules state G vars unsafeList of 
1046 
[] => (*there are no plausible unsafe rules*) 

54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1047 
(cond_tracing trace (fn () => "moving formula to literals"); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1048 
prv (tacs, brs0::trs, choices, 
60943  1049 
{pairs = (br,unsafe)::pairs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1050 
lits = addLit(G,lits), 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1051 
vars = vars, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1052 
lim = lim} :: brs)) 
60943  1053 
 _ => (*G admits some unsafe rules: try later*) 
1054 
(cond_tracing trace (fn () => "moving formula to unsafe list"); 

42804  1055 
prv (if isGoal G then negOfGoal_tac ctxt :: tacs 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1056 
else tacs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1057 
brs0::trs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1058 
choices, 
60943  1059 
{pairs = (br, unsafe@[(negOfGoal G, md)])::pairs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1060 
lits = lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1061 
vars = vars, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1062 
lim = lim} :: brs))) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1063 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1064 
 prv (tacs, trs, choices, 
60943  1065 
{pairs = ([],unsafe)::(Gs,unsafe')::pairs, lits, vars, lim} :: brs) = 
1066 
(*no more "safe" formulae: transfer unsafe down a level*) 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1067 
prv (tacs, trs, choices, 
60943  1068 
{pairs = (Gs,unsafe@unsafe')::pairs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1069 
lits = lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1070 
vars = vars, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1071 
lim = lim} :: brs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1072 
 prv (tacs, trs, choices, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1073 
brs0 as {pairs = [([], (H,md)::Hs)], 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1074 
lits, vars, lim} :: brs) = 
60943  1075 
(*no safe steps possible at any level: apply a unsafe rule*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1076 
let exception PRV (*backtrack to precisely this recursion!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1077 
val H = norm H 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1078 
val ntrl = !ntrail 
60943  1079 
val rules = netMkRules state H vars unsafeList 
1080 
(*new premises of unsafe rules may NOT be duplicated*) 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1081 
fun newPrem (vars,P,dup,lim') prem = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1082 
let val Gs' = map (fn Q => (Q,false)) prem 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1083 
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1084 
and lits' = if (exists isGoal prem) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1085 
then map negOfGoal lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1086 
else lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1087 
in {pairs = if exists (match P) prem then [(Gs',Hs')] 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1088 
(*Recursive in this premise. Don't make new 
60943  1089 
"stack frame". New unsafe premises will end up 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1090 
at the BACK of the queue, preventing 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1091 
exclusion of others*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1092 
else [(Gs',[]), ([],Hs')], 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1093 
lits = lits', 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1094 
vars = vars, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1095 
lim = lim'} 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1096 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1097 
fun newBr x prems = map (newPrem x) prems @ brs 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1098 
(*Seek a matching rule. If unifiable then add new premises 
2854  1099 
to branch.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1100 
fun deeper [] = raise NEWBRANCHES 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1101 
 deeper (((P,prems),tac)::grls) = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1102 
if unify state (add_term_vars(P,[]), P, H) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1103 
then 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1104 
let val updated = ntrl < !ntrail (*branch updated*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1105 
val vars = vars_in_vars vars 
30190  1106 
val vars' = List.foldr add_terms_vars vars prems 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1107 
(*duplicate H if md permits*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1109 
duplicate only if the subgoal has new vars*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1110 
(*any instances of P in the subgoals? 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1111 
NB: boolean "recur" affects tracing only!*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1112 
and recur = exists (exists (match P)) prems 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1113 
val lim' = (*Decrement "lim" extra if updates occur*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1114 
if updated then lim  (1+log(length rules)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1115 
else lim1 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1116 
(*It is tempting to leave "lim" UNCHANGED if 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1117 
both dup and recur are false. Proofs are 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1118 
found at shallower depths, but looping 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1119 
occurs too often...*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1120 
val mayUndo = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1121 
(*Allowing backtracking from a rule application 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1122 
if other matching rules exist, if the rule 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1123 
updated variables, or if the rule did not 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1124 
introduce new variables. This latter condition 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1125 
means it is not a standard "gammarule" but 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1126 
some other form of unsafe rule. Aim is to 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1127 
emulate Fast_tac, which allows all unsafe steps 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1128 
to be undone.*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1129 
not(null grls) (*other rules to try?*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1130 
orelse updated 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1131 
orelse vars=vars' (*no new Vars?*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1132 
val tac' = tac(updated, dup, true) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1134 
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

1135 
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

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

1137 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1138 
in 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1139 
if lim'<0 andalso not (null prems) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1140 
then (*it's faster to kill ALL the alternatives*) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1141 
(cond_tracing trace (fn () => "Excessive branching: KILLED"); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1142 
clearTo state ntrl; raise NEWBRANCHES) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1143 
else 
42804  1144 
traceNew trace prems; 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1145 
cond_tracing (trace andalso dup) (fn () => " (duplicating)"); 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1146 
cond_tracing (trace andalso recur) (fn () => " (recursive)"); 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1147 
traceVars state ntrl; 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1148 
if null prems then nclosed := !nclosed + 1 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1149 
else ntried := !ntried + length prems  1; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1150 
prv(tac' :: tacs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1151 
brs0::trs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1152 
(ntrl, length brs0, PRV) :: choices, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1153 
newBr (vars', P, dup, lim') prems) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1154 
handle PRV => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1155 
if mayUndo 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1156 
then (*reset Vars and try another rule*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1157 
(clearTo state ntrl; deeper grls) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1158 
else (*backtrack to previous level*) 
42804  1159 
backtrack trace choices 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1160 
end 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1161 
else deeper grls 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1162 
in 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1163 
trace_prover state brs0; 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1164 
if lim<1 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1165 
else deeper rules 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1166 
handle NEWBRANCHES => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1167 
(*cannot close branch: move H to literals*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1168 
prv (tacs, brs0::trs, choices, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1169 
{pairs = [([], Hs)], 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1170 
lits = H::lits, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1171 
vars = vars, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1172 
lim = lim} :: brs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1173 
end 
42804  1174 
 prv (tacs, trs, choices, _ :: brs) = backtrack trace choices 
12346  1175 
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 
2854  1176 

1177 

2883  1178 
(*Construct an initial branch.*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1179 
fun initBranch (ts,lim) = 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1180 
{pairs = [(map (fn t => (t,true)) ts, [])], 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1181 
lits = [], 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1183 
lim = lim}; 
2854  1184 

1185 

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

1187 

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

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1189 
local open Term 
2854  1190 
in 
56245  1191 
fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t 
2854  1192 
 discard_foralls t = t; 
1193 
end; 

1194 

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

1196 
fun getVars [] i = [] 

20664  1197 
 getVars ((_,(v,is))::alist) (i: int) = 
1198 
if member (op =) is i then getVars alist i 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1199 
else v :: getVars alist i; 
2854  1200 

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

1201 
exception TRANS of string; 
2854  1202 

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

1203 
(*Translation of a subgoal: Skolemize all parameters*) 
43349  1204 
fun fromSubgoal (state as State {ctxt, ...}) t = 
1205 
let val thy = Proof_Context.theory_of ctxt 

1206 
val alistVar = Unsynchronized.ref [] 

32740  1207 
and alistTVar = Unsynchronized.ref [] 
2854  1208 
fun hdvar ((ix,(v,is))::_) = v 
1209 
fun from lev t = 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1210 
let val (ht,ts) = Term.strip_comb t 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1211 
fun apply u = list_comb (u, map (from lev) ts) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1212 
fun bounds [] = [] 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1213 
 bounds (Term.Bound i::ts) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1214 
if i<lev then raise TRANS 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1215 
"Function unknown's argument not a parameter" 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1216 
else ilev :: bounds ts 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1217 
 bounds ts = raise TRANS 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1218 
"Function unknown's argument not a bound variable" 
2854  1219 
in 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1220 
case ht of 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1221 
Term.Const aT => apply (fromConst thy alistTVar aT) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1222 
 Term.Free (a,_) => apply (Free a) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1223 
 Term.Bound i => apply (Bound i) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1224 
 Term.Var (ix,_) => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1225 
(case (AList.lookup (op =) (!alistVar) ix) of 
32740  1226 
NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1227 
:: !alistVar; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1228 
Var (hdvar(!alistVar))) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1229 
 SOME(v,is) => if is=bounds ts then Var v 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1230 
else raise TRANS 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1231 
("Discrepancy among occurrences of " 
22678  1232 
^ Term.string_of_vname ix)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1233 
 Term.Abs (a,_,body) => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1234 
if null ts then Abs(a, from (lev+1) body) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1238 
val npars = length (Logic.strip_params t) 

1239 

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

1241 
fun skoSubgoal i t = 

18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1242 
if i<npars then 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1243 
skoSubgoal (i+1) 
43349  1244 
(subst_bound (Skolem (gensym state "T", getVars (!alistVar) i), t)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1245 
else t 
2854  1246 

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

1248 

1249 

43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1250 
(*Tableau engine and proof reconstruction operating on subgoal 1. 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1251 
"start" is CPU time at start, for printing SEARCH time (also prints reconstruction time) 
2854  1252 
"lim" is depth limit.*) 
43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1253 
fun raw_blast start ctxt lim st = 
43349  1254 
let val state = initialize ctxt 
42804  1255 
val trace = Config.get ctxt trace; 
1256 
val stats = Config.get ctxt stats; 

43349  1257 
val skoprem = fromSubgoal state (#1 (Logic.dest_implies (Thm.prop_of st))) 
4323
561242f8606b
Printing of statistics including time for search & reconstruction
paulson
parents:
4300
diff
changeset

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

1259 
and concl = strip_imp_concl skoprem 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1260 
fun cont (tacs,_,choices) = 
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41491
diff
changeset

1261 
let val start = Timing.start () 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1262 
in 
42369  1263 
case Seq.pull(EVERY' (rev tacs) 1 st) of 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1264 
NONE => (cond_tracing trace (fn () => "PROOF FAILED for depth " ^ string_of_int lim); 
42804  1265 
backtrack trace choices) 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1266 
 cell => (cond_tracing (trace orelse stats) 
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1267 
(fn () => Timing.message (Timing.result start) ^ " for reconstruction"); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1268 
Seq.make(fn()=> cell)) 
63280
d2d26ff708d7
code to catch exception TERM in blast
paulson <lp15@cam.ac.uk>
parents:
63265
diff
changeset

1269 
end handle TERM _ => 
d2d26ff708d7
code to catch exception TERM in blast
paulson <lp15@cam.ac.uk>
parents:
63265
diff
changeset

1270 
(cond_tracing trace (fn () => "PROOF RAISED EXN TERM for depth " ^ string_of_int lim); 
d2d26ff708d7
code to catch exception TERM in blast
paulson <lp15@cam.ac.uk>
parents:
63265
diff
changeset

1271 
backtrack trace choices) 
42369  1272 
in 
42801
da4ad5f98953
proper Proof.context  eliminated global operations;
wenzelm
parents:
42793
diff
changeset

1273 
prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) 
42369  1274 
end 
43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1275 
handle PROVE => Seq.empty 
54942
ed36358c20d5
uniform output of tracing via official channel (usually depending on trace flag);
wenzelm
parents:
54897
diff
changeset

1276 
 TRANS s => (cond_tracing (Config.get ctxt trace) (fn () => "Blast: " ^ s); Seq.empty); 
2854  1277 

43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1278 
fun depth_tac ctxt lim i st = 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1279 
SELECT_GOAL 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53536
diff
changeset

1280 
(Object_Logic.atomize_prems_tac ctxt 1 THEN 
43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1281 
raw_blast (Timing.start ()) ctxt lim) i st; 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1282 

42793  1283 
fun blast_tac ctxt i st = 
43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1284 
let 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1285 
val start = Timing.start (); 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1286 
val lim = Config.get ctxt depth_limit; 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1287 
in 
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
43045
diff
changeset

1288 
SELECT_GOAL 
54742
7a86358a3c0b
proper context for basic Simpli 