author  wenzelm 
Sat, 17 May 2008 13:54:30 +0200  
changeset 26928  ca87aff1ad2d 
parent 25365  4e7a1dabd7ef 
child 26938  64e850c3da9e 
permissions  rwrr 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

6 
Generic tableau prover with proof reconstruction 

7 

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

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

13 
However, Const is heavily used for logical connectives. 

2894  14 

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

15 
Blast_tac is often more powerful than fast_tac, but has some limitations. 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

17 
* ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
4651  18 
this restriction is intrinsic 
2894  19 
* 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

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

21 
* rules must not require higherorder unification, e.g. apply_type in ZF 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

22 
+ message "Function Var's argument not a bound variable" relates to this 
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

25 
Known problems: 

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

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

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

29 
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

30 
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

31 

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

32 
With substition for equalities (hyp_subst_tac): 
3092  33 
When substitution affects a haz formula or literal, it is moved 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

35 
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

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

39 
(*Should be a type abbreviation?*) 

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

41 

42 
signature BLAST_DATA = 

43 
sig 

44 
type claset 

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

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

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

47 
val notE : thm (* [ ~P; P ] ==> R *) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

49 
val contr_tac : int > tactic 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

50 
val dup_intr : thm > thm 
23908  51 
val hyp_subst_tac : bool > int > tactic 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

53 
val rep_cs : (* dependent on classical.ML *) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

54 
claset > {safeIs: thm list, safeEs: thm list, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

56 
swrappers: (string * wrapper) list, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

57 
uwrappers: (string * wrapper) list, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

59 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} 
7272  60 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  61 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 
2854  62 
end; 
63 

64 

65 
signature BLAST = 

66 
sig 

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

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

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

69 
datatype term = 
18177  70 
Const of string * term list 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

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

75 
 Abs of string*term 
17795  76 
 $ of term*term; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

78 
val depth_tac : claset > int > int > tactic 
24112  79 
val depth_limit : int Config.T 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

80 
val blast_tac : claset > int > tactic 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

81 
val Blast_tac : int > tactic 
18708  82 
val setup : theory > theory 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

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

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

86 
val fullTrace : branch list list ref 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

87 
val fromType : (indexname * term) list ref > Term.typ > term 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

88 
val fromTerm : theory > Term.term > term 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

89 
val fromSubgoal : theory > Term.term > term 
4065  90 
val instVars : term > (unit > unit) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

91 
val toTerm : int > term > Term.term 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

92 
val readGoal : theory > string > term 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

93 
val tryInThy : theory > int > string > 
3083  94 
(int>tactic) list * branch list list * (int*int*exn) list 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

95 
val normBr : branch > branch 
2854  96 
end; 
97 

98 

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

99 
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854  100 
struct 
101 

102 
type claset = Data.claset; 

103 

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

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

105 
and stats = ref false; (*for runtime and search statistics*) 
2854  106 

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

107 
datatype term = 
18177  108 
Const of string * term list (*typargs constantas a terms!*) 
2854  109 
 Skolem of string * term option ref list 
5343
871b77df79a0
new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents:
4653
diff
changeset

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

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

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

113 
 Abs of string*term 
5613  114 
 op $ of term*term; 
2854  115 

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

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

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

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

119 
(term*bool) list) list, (*haz formulae on this level*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

120 
lits: term list, (*literals: irreducible formulae*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

121 
vars: term option ref list, (*variables occurring in branch*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

123 

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

124 

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

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

126 

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

127 
datatype state = State of 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

128 
{thy: theory, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

129 
fullTrace: branch list list ref, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

130 
trail: term option ref list ref, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

131 
ntrail: int ref, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

132 
nclosed: int ref, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

133 
ntried: int ref} 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

134 

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

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

136 
is_some (Sign.const_type thy c) andalso 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

138 

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

139 
fun initialize thy = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

140 
(reject_const thy "*Goal*"; 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

141 
reject_const thy "*False*"; 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

143 
{thy = thy, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

144 
fullTrace = ref [], 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

145 
trail = ref [], 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

146 
ntrail = ref 0, 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

147 
nclosed = ref 0, (*branches closed: number of branches closed during the search*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

148 
ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

149 

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

150 

2854  151 

152 
(** Basic syntactic operations **) 

153 

154 
fun is_Var (Var _) = true 

155 
 is_Var _ = false; 

156 

157 
fun dest_Var (Var x) = x; 

158 

159 
fun rand (f$x) = x; 

160 

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

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

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

165 
fun strip_comb u : term * term list = 
2854  166 
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

167 
 stripc x = x 
2854  168 
in stripc(u,[]) end; 
169 

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

171 
fun head_of (f$t) = head_of f 

172 
 head_of u = u; 

173 

174 

175 
(** Particular constants **) 

176 

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

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

178 

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

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

180 
 isNot _ = false; 
2854  181 

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

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

185 
 isGoal _ = false; 
2854  186 

18177  187 
val TruepropC = ObjectLogic.judgment_name (the_context ()); 
188 
val TruepropT = Sign.the_const_type (the_context ()) TruepropC; 

18171  189 

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

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

194 

2854  195 

196 

4065  197 
(*** Dealing with overloaded constants ***) 
2854  198 

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

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

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

204 
(case (AList.lookup (op =) (!alist) ixn) of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

205 
NONE => let val t' = Var(ref NONE) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

208 
 SOME v => v) 
2854  209 

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

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

211 
Const (a, map (fromType alist) (Sign.const_typargs thy (a, T))); 
2854  212 

213 

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

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

15531  218 
 (Var(ref(SOME t))) aconv u = t aconv u 
219 
 t aconv (Var(ref(SOME u))) = t aconv u 

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

220 
 (Var v) aconv (Var w) = v=w (*both Vars are unassigned*) 
2854  221 
 (Bound i) aconv (Bound j) = i=j 
222 
 (Abs(_,t)) aconv (Abs(_,u)) = t aconv u 

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

18177  224 
 _ aconv _ = false 
225 
and aconvs ([], []) = true 

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

227 
 aconvs _ = false; 

2854  228 

229 

230 
fun mem_term (_, []) = false 

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

232 

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

234 

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

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

237 

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

239 

240 

241 
(** Vars **) 

242 

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

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

244 
fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

245 
 add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) 
15531  246 
 add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

247 
 add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

248 
 add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

250 
 add_term_vars (_, vars) = vars 
2854  251 
(*Term list version. [The fold functionals are slow]*) 
252 
and add_terms_vars ([], vars) = vars 

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

254 
(*Var list version.*) 

255 
and add_vars_vars ([], vars) = vars 

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

256 
 add_vars_vars (ref (SOME u) :: vs, vars) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

257 
add_vars_vars (vs, add_term_vars(u,vars)) 
15531  258 
 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

259 
add_vars_vars (vs, ins_var (v, vars)); 
2854  260 

261 

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

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

264 

265 

266 

267 
(*increment a term's nonlocal bound variables 

268 
inc is increment for bound variables 

269 
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

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

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

274 

275 
fun incr_boundvars 0 t = t 

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

277 

278 

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

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

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

281 
fun add_loose_bnos (Bound i, lev, js) = if i<lev then js 
20854  282 
else insert (op =) (i  lev) js 
2854  283 
 add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
284 
 add_loose_bnos (f$t, lev, js) = 

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

285 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
2854  286 
 add_loose_bnos (_, _, js) = js; 
287 

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

289 

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

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

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

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

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

295 
 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

296 
 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

297 
 subst (t,lev) = t 
2854  298 
in subst (t,0) end; 
299 

300 

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

301 
(*Normalize...but not the bodies of ABSTRACTIONS*) 
2854  302 
fun norm t = case t of 
2952  303 
Skolem (a,args) => Skolem(a, vars_in_vars args) 
18177  304 
 Const(a,ts) => Const(a, map norm ts) 
15531  305 
 (Var (ref NONE)) => t 
306 
 (Var (ref (SOME u))) => norm u 

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

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

309 
 nf => nf $ norm u) 
2854  310 
 _ => t; 
311 

312 

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

314 
fun wkNormAux t = case t of 

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

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

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

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

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

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

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

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

323 
nb as (f $ t) => 
20664  324 
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

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

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

327 
 nb => Abs (a,nb)) 
2854  328 
 _ => t 
329 
and wkNorm t = case head_of t of 

330 
Const _ => t 

331 
 Skolem(a,args) => t 

332 
 Free _ => t 

333 
 _ => wkNormAux t; 

334 

335 

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

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

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

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

339 
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

340 
 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

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

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

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

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

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

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

349 
 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

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

351 
in occ 0 end; 
2854  352 

353 
exception UNIFY; 

354 

355 

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

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

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

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

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

361 
ntrail := !ntrail  1); 
2854  362 

363 

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

364 
(*Firstorder unification with bound variables. 
2854  365 
"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

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

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

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

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

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

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

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

374 
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

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

376 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

392 
 unifysAux _ = raise UNIFY; 

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

393 
in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false) 
2854  394 
end; 
395 

396 

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

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

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

399 
fun fromTerm thy t = 
4065  400 
let val alistVar = ref [] 
401 
and alistTVar = ref [] 

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

402 
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

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

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

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

406 
(case (AList.lookup (op =) (!alistVar) ixn) of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

407 
NONE => let val t' = Var(ref NONE) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

413 
u' as (f $ Bound 0) => 
20664  414 
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

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

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

417 
 from (Term.$ (f,u)) = from f $ from u 
2854  418 
in from t end; 
419 

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

422 
fun instVars t = 

12902  423 
let val name = ref "a" 
4065  424 
val updated = ref [] 
18177  425 
fun inst (Const(a,ts)) = List.app inst ts 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

426 
 inst (Var(v as ref NONE)) = (updated := v :: (!updated); 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

431 
 inst _ = () 
15570  432 
fun revert() = List.app (fn v => v:=NONE) (!updated) 
4065  433 
in inst t; revert end; 
434 

435 

2854  436 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
18177  437 
fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B 
2854  438 
 strip_imp_prems _ = []; 
439 

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

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

443 

2854  444 

445 

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

447 

9170  448 
exception ElimBadConcl and ElimBadPrem; 
449 

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

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

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

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

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

456 
Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

457 
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

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

459 
 _ => P :: delete_concl Ps); 
2854  460 

18177  461 
fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = 
2854  462 
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) 
463 
 skoPrem vars P = P; 

464 

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

465 
fun convertPrem t = 
9170  466 
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 
2854  467 

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

469 
fun convertRule vars t = 

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

471 
val Var v = strip_imp_concl t 

18177  472 
in v := SOME (Const ("*False*", [])); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

473 
(P, map (convertPrem o skoPrem vars) Ps) 
9170  474 
end 
475 
handle Bind => raise ElimBadConcl; 

2854  476 

477 

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

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

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

481 

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

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

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

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

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

487 
 nNewHyps (P::Ps) = 1 + nNewHyps Ps; 
2854  488 

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

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

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

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

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

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

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

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

496 

2854  497 

26928  498 
fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i; 
2854  499 

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

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

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

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

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

504 

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

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

506 
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

507 
Flag "dup" requests duplication of the affected formula.*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

508 
fun fromRule thy vars rl = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

509 
let val trl = rl > Thm.prop_of > fromTerm thy > convertRule vars 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

510 
fun tac (upd, dup,rot) i = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

511 
emtac upd (if dup then rev_dup_elim rl else rl) i 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

514 
in Option.SOME (trl, tac) end 
9170  515 
handle ElimBadPrem => (*reject: prems don't preserve conclusion*) 
26928  516 
(warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

517 
Option.NONE) 
9170  518 
 ElimBadConcl => (*ignore: conclusion is not just a variable*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

519 
(if !trace then (warning("Ignoring illformed elimination rule:\n" ^ 
26928  520 
"conclusion should be a variable\n" ^ Display.string_of_thm rl)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

522 
Option.NONE); 
2854  523 

524 

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

525 
(*** Conversion of Introduction Rules ***) 
2854  526 

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

528 

529 
fun convertIntrRule vars t = 

530 
let val Ps = strip_imp_prems t 

531 
val P = strip_imp_concl t 

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

532 
in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 
2854  533 
end; 
534 

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

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

536 
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

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

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

539 
introduction rules.*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

540 
fun fromIntrRule thy vars rl = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

541 
let val trl = rl > Thm.prop_of > fromTerm thy > convertIntrRule vars 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

542 
fun tac (upd,dup,rot) i = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

543 
rmtac upd (if dup then Data.dup_intr rl else rl) i 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

545 
rot_subgoals_tac (rot, #2 trl) i 
2854  546 
in (trl, tac) end; 
547 

548 

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

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

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

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

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

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

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

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

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

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

562 

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

563 
fun netMkRules thy P vars (nps: netpair list) = 
2854  564 
case P of 
18177  565 
(Const ("*Goal*", _) $ G) => 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

567 
val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

568 
in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end 
2854  569 
 _ => 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

571 
val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

572 
in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end; 
3092  573 

574 

575 
(*Normalize a branchfor tracing*) 

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

577 

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

579 

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

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

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

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

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

584 
lim = lim}; 
3092  585 

586 

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

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

592 
 showType (Var _) = dummyTVar 

593 
 showType t = 

594 
(case strip_comb t of 

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

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

596 
 _ => dummyT); 
4065  597 

598 
(*Display toplevel overloading if any*) 

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

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

602 
 topType _ _ = NONE; 

4065  603 

604 

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

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

15531  610 
 showTerm d (Var(ref(SOME u))) = showTerm d u 
611 
 showTerm d (Var(ref NONE)) = dummyVar2 

3092  612 
 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

613 
else Term.Abs(a, dummyT, showTerm (d1) t) 
3092  614 
 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

615 
else Term.$ (showTerm d f, showTerm (d1) u); 
3092  616 

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

617 
fun string_of thy d t = Sign.string_of_term thy (showTerm d t); 
3092  618 

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

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

622 
 negOfGoal G = G; 

623 

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

625 

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

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

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

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

630 

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

632 
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN 

633 
rotate_tac ~1 i; 

634 

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

635 
fun traceTerm thy t = 
19037  636 
let val t' = norm (negOfGoal t) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

640 
NONE => stm (*no type to attach*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

641 
 SOME T => stm ^ "\t:: " ^ Sign.string_of_typ thy T 
4065  642 
end; 
3092  643 

644 

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

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

646 
fun tracing (State {thy, fullTrace, ...}) brs = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

647 
let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G) 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

648 
 printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)") 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

651 
(fullTrace := brs0 :: !fullTrace; 
22580  652 
List.app (fn _ => Output.immediate_output "+") brs; 
653 
Output.immediate_output (" [" ^ Int.toString lim ^ "] "); 

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

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

655 
writeln"") 
3092  656 
in if !trace then printBrs (map normBr brs) else () 
657 
end; 

658 

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

659 
fun traceMsg s = if !trace then writeln s else (); 
4065  660 

3092  661 
(*Tracing: variables updated in the last branch operation?*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

662 
fun traceVars (State {thy, ntrail, trail, ...}) ntrl = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

663 
if !trace then 
4065  664 
(case !ntrailntrl of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

665 
0 => () 
22580  666 
 1 => Output.immediate_output"\t1 variable UPDATED:" 
667 
 n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); 

4065  668 
(*display the instantiations themselves, though no variable names*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

669 
List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v)))) 
4065  670 
(List.take(!trail, !ntrailntrl)); 
671 
writeln"") 

3092  672 
else (); 
673 

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

675 
fun traceNew prems = 

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

676 
if !trace then 
3092  677 
case length prems of 
22580  678 
0 => Output.immediate_output"branch closed by rule" 
679 
 1 => Output.immediate_output"branch extended (1 new subgoal)" 

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

3092  681 
else (); 
682 

683 

684 

2854  685 
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 
686 

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

687 
(*Replace the ATOMIC term "old" by "new" in t*) 
2854  688 
fun subst_atomic (old,new) t = 
15531  689 
let fun subst (Var(ref(SOME u))) = subst u 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

692 
 subst t = if t aconv old then new else t 
2854  693 
in subst t end; 
694 

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

696 
fun eta_contract_atom (t0 as Abs(a, body)) = 
2854  697 
(case eta_contract2 body of 
20664  698 
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

699 
else eta_contract_atom (incr_boundvars ~1 f) 
2854  700 
 _ => t0) 
701 
 eta_contract_atom t = t 

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

703 
 eta_contract2 t = eta_contract_atom t; 

704 

705 

706 
(*When can we safely delete the equality? 

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

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

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

710 
Prefer to eliminate Bound variables if possible. 

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

712 

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

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

714 
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

715 
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

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

717 
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

718 
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

719 
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

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

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

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

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

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

726 
 occ (Var v) = not (mem_var (v, vars)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

727 
 occ (Abs(_,u)) = occEq u 
2854  728 
 occ (f$u) = occEq u orelse occEq f 
729 
 occ (_) = false; 

730 
in occEq end; 

731 

3092  732 
exception DEST_EQ; 
733 

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

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

736 
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

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

738 
 dest_eq _ = raise DEST_EQ; 
3092  739 

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

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

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

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

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

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

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

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

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

754 
they should go: this could make proofs fail.*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

755 
fun equalSubst thy (G, {pairs, lits, vars, lim}) = 
3092  756 
let val (t,u) = orientGoal(dest_eq G) 
757 
val subst = subst_atomic (t,u) 

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

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

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

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

762 
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

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

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

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

766 
fun subFrame ((Gs,Hs), (changed, frames)) = 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

769 
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

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

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

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

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

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

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

777 
val (changed', pairs') = foldr subFrame (changed, []) pairs 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

778 
in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

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

784 
lim = lim} 
2854  785 
end; 
786 

787 

788 
exception NEWBRANCHES and CLOSEF; 

789 

790 
exception PROVE; 

791 

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

792 
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

794 
(eq_assume_tac ORELSE' assume_tac); 
2854  795 

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

796 
val eContr_tac = TRACE Data.notE contr_tac; 
2854  797 
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); 
798 

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

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

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

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

802 
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

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

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

805 
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

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

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

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

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

810 
end; 
2854  811 

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

813 
fun hasSkolem (Skolem _) = true 

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

814 
 hasSkolem (Abs (_,body)) = hasSkolem body 
2854  815 
 hasSkolem (f$t) = hasSkolem f orelse hasSkolem t 
816 
 hasSkolem _ = false; 

817 

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

819 
Skolem terms then allow duplication.*) 

820 
fun joinMd md [] = [] 

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

822 

823 

824 
(** Backtracking and Pruning **) 

825 

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

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

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

829 
 clashVar vars = 

830 
let fun clash (0, _) = false 

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

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

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

835 

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

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

838 
next branch have been updated.*) 

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

839 
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

840 
backtracking over bad proofs*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

845 
in if !trace andalso ll<lc then 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

846 
(writeln("Pruning " ^ Int.toString(lcll) ^ " levels"); 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

853 
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

854 
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

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

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

857 
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

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

859 
choices) 
2854  860 
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; 
861 

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

862 
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

863 
 nextVars [] = []; 
2854  864 

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

865 
fun backtrack (choices as (ntrl, nbrs, exn)::_) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

866 
(if !trace then (writeln ("Backtracking; now there are " ^ 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

867 
Int.toString nbrs ^ " branches")) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

868 
else (); 
3083  869 
raise exn) 
870 
 backtrack _ = raise PROVE; 

2854  871 

2894  872 
(*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

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

876 
 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

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

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

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

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

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

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

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

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

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

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

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

891 

892 

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

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

896 

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

897 

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

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

899 
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

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

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

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

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

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

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

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

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

911 
 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

912 

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

913 

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

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

915 
if b then 
21295
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
20854
diff
changeset

916 
writeln (end_timing start ^ " for search. Closed: " 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

921 

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

922 

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

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

924 
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

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

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

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

928 
fun prove (state, start, cs, brs, cont) = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

930 
val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs 
2854  931 
val safeList = [safe0_netpair, safep_netpair] 
932 
and hazList = [haz_netpair] 

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

933 
fun prv (tacs, trs, choices, []) = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

934 
(printStats state (!trace orelse !stats, start, tacs); 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

937 
brs0 as {pairs = ((G,md)::br, haz)::pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

945 
val G = norm G 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

946 
val rules = netMkRules thy G vars safeList 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

951 
then {pairs = ((joinMd md prem, []) :: 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

952 
negOfGoals ((br, haz)::pairs)), 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

957 
(br, haz) :: pairs), 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

967 
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

968 
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

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

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

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

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

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

974 
val vars' = foldr add_terms_vars vars prems 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

986 
if lim'<0 (*faster to kill ALL the alternatives*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

987 
then (traceMsg"Excessive branching: KILLED"; 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

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

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

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

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

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

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

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

998 
else (*backtrack to previous level*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

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

1008 
let val choices' = 
22580  1009 
(if !trace then (Output.immediate_output"branch closed"; 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

1023 
 closeFl ((br, haz)::pairs) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1024 
closeF (map fst br) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1025 
handle CLOSEF => closeF (map fst haz) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1026 
handle CLOSEF => closeFl pairs 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

1029 
else 
23908  1030 
prv (Data.hyp_subst_tac (!trace) :: tacs, 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1031 
brs0::trs, choices, 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

1033 
(G, {pairs = (br,haz)::pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

1036 
handle DEST_EQ => closeF lits 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1037 
handle CLOSEF => closeFl ((br,haz)::pairs) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1039 
handle NEWBRANCHES => 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1040 
(case netMkRules thy G vars hazList of 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1041 
[] => (*there are no plausible haz rules*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1042 
(traceMsg "moving formula to literals"; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1044 
{pairs = (br,haz)::pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

1048 
 _ => (*G admits some haz rules: try later*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1049 
(traceMsg "moving formula to haz list"; 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

1054 
{pairs = (br, haz@[(negOfGoal G, md)])::pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

1060 
{pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1061 
(*no more "safe" formulae: transfer haz down a level*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1063 
{pairs = (Gs,haz@haz')::pairs, 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

1070 
(*no safe steps possible at any level: apply a haz rule*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

1073 
val ntrl = !ntrail 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1074 
val rules = netMkRules thy H vars hazList 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1075 
(*new premises of haz rules may NOT be duplicated*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

1078 
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

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

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

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

1082 
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

1083 
(*Recursive in this premise. Don't make new 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1084 
"stack frame". New haz premises will end up 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

1097 
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

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

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

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

1101 
val vars' = foldr add_terms_vars vars prems 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1103 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1129 
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

1130 
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

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

1132 

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

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

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

1135 
then (*it's faster to kill ALL the alternatives*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1136 
(traceMsg"Excessive branching: KILLED"; 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

1139 
traceNew prems; 
22580  1140 
if !trace andalso dup then Output.immediate_output" (duplicating)" 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1141 
else (); 
22580  1142 
if !trace andalso recur then Output.immediate_output" (recursive)" 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

1155 
else (*backtrack to previous level*) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

1169 
end 
2854  1170 
 prv (tacs, trs, choices, _ :: brs) = backtrack choices 
12346  1171 
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 
2854  1172 

1173 

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

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

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

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

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

1179 
lim = lim}; 
2854  1180 

1181 

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

1183 

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

1185 
local open Term 
2854  1186 
in 
1187 
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t 

1188 
 discard_foralls t = t; 

1189 
end; 

1190 

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

1192 
fun getVars [] i = [] 

20664  1193 
 getVars ((_,(v,is))::alist) (i: int) = 
1194 
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

1195 
else v :: getVars alist i; 
2854  1196 

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

1197 
exception TRANS of string; 
2854  1198 

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

1199 
(*Translation of a subgoal: Skolemize all parameters*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1200 
fun fromSubgoal thy t = 
4065  1201 
let val alistVar = ref [] 
1202 
and alistTVar = ref [] 

2854  1203 
fun hdvar ((ix,(v,is))::_) = v 
1204 
fun from lev t = 

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

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

1206 
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

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

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

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

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

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

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

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

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

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

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

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

1219 
 Term.Var (ix,_) => 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1220 
(case (AList.lookup (op =) (!alistVar) ix) of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1221 
NONE => (alistVar := (ix, (ref NONE, bounds ts)) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1223 
Var (hdvar(!alistVar))) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1224 
 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

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

1226 
("Discrepancy among occurrences of " 
22678  1227 
^ Term.string_of_vname ix)) 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1229 
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

1230 
else raise TRANS "argument not in normal form" 
2854  1231 
end 
1232 

1233 
val npars = length (Logic.strip_params t) 

1234 

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

1236 
fun skoSubgoal i t = 

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

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

1238 
skoSubgoal (i+1) 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1239 
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1241 
else t 
2854  1242 

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

1244 

1245 

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

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

1247 
"start" is CPU time at start, for printing SEARCH time 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1248 
(also prints reconstruction time) 
2854  1249 
"lim" is depth limit.*) 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1250 
fun timing_depth_tac start cs lim i st0 = 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1251 
let val thy = Thm.theory_of_thm st0 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1252 
val state = initialize thy 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1253 
val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

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

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

1257 
fun cont (tacs,_,choices) = 
21295
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
20854
diff
changeset

1258 
let val start = start_timing () 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

1260 
case Seq.pull(EVERY' (rev tacs) i st) of 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1261 
NONE => (writeln ("PROOF FAILED for depth " ^ 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1262 
Int.toString lim); 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1263 
if !trace then error "************************\n" 
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

1266 
 cell => (if (!trace orelse !stats) 
21295
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
20854
diff
changeset

1267 
then writeln (end_timing start ^ " for reconstruction") 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

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

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

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

1271 
in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1272 
handle PROVE => Seq.empty 
2854  1273 

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

1274 
(*Public version with fixed depth*) 
21295
63552bc99cfb
tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents:
20854
diff
changeset

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

1276 

24112  1277 
val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20; 
15162
670ab8497818
depth limit (previously hardcoded with a value of 20) made a reference
webertj
parents:
14984
diff
changeset

1278 

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

1279 
fun blast_tac cs i st = 
24112  1280 
((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit) 
24099
6534fd4c5d46
replaced depth_limit ref by blast_depth_limit configuration option;
wenzelm
parents:
24062
diff
changeset

1281 
(timing_depth_tac (start_timing ()) cs) 0) i 
5463
a5479f5cd482
Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents:
5411
diff
changeset

1282 
THEN flexflex_tac) st 
14466  1283 
handle TRANS s => 
18525
ce1ae48c320f
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
wenzelm
parents:
18177
diff
changeset

1284 
((if !trace then warning ("blast: " ^ s) else ()); 
14466  1285 
Seq.empty); 
2854  1286 

4078  1287 
fun Blast_tac i = blast_tac (Data.claset()) i; 
2854  1288 

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

1289 

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

1290 
(*** For debugging: these apply the prover to a subgoal and return 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

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

1292 

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

1293 
val fullTrace = ref ([]: branch list list); 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1294 

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

1295 
(*Read a string to make an initial, singleton branch*) 
25365  1296 
fun readGoal thy s = Syntax.read_prop_global thy s > fromTerm thy > rand > mkGoal; 
2924
af506c35b4ed
Control over excessive branching by applying a log2 penalty
paulson
parents:
2894
diff
changeset

1297 

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

1298 
fun tryInThy thy lim s = 
24062
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

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

1300 
val state as State {fullTrace = ft, ...} = initialize thy; 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1301 
val res = timeap prove 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1302 
(state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I); 
845c0d693328
explicit global state argument  no longer CRITICAL;
wenzelm
parents:
23985
diff
changeset

1303 
val _ = fullTrace := !ft; 