author  wenzelm 
Tue, 02 Dec 1997 12:42:28 +0100  
changeset 4345  7e9436ffb813 
parent 4318  9b672ea2dfe7 
child 4443  d55e85d7f0c2 
permissions  rwrr 
1460  1 
(* Title: Pure/logic.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

6 
Supporting code for defining the abstract type "thm" 

7 
*) 

8 

9 
infix occs; 

10 

11 
signature LOGIC = 

4345  12 
sig 
13 
val indexname_ord : indexname * indexname > order 

14 
val typ_ord : typ * typ > order 

15 
val typs_ord : typ list * typ list > order 

16 
val term_ord : term * term > order 

17 
val terms_ord : term list * term list > order 

18 
val termless : term * term > bool 

1460  19 
val assum_pairs : term > (term*term)list 
20 
val auto_rename : bool ref 

21 
val close_form : term > term 

22 
val count_prems : term * int > int 

23 
val dest_equals : term > term * term 

24 
val dest_flexpair : term > term * term 

25 
val dest_implies : term > term * term 

26 
val dest_inclass : term > typ * class 

27 
val dest_type : term > typ 

28 
val flatten_params : int > term > term 

29 
val incr_indexes : typ list * int > term > term 

3963
29c5ec9ecbaa
Corrected alphabetical order of entries in signature.
nipkow
parents:
3915
diff
changeset

30 
val is_equals : term > bool 
1460  31 
val lift_fns : term * int > (term > term) * (term > term) 
32 
val list_flexpairs : (term*term)list * term > term 

33 
val list_implies : term list * term > term 

0  34 
val list_rename_params: string list * term > term 
4116  35 
val rewrite_rule_extra_vars: term list > term > term > string option 
36 
val rewrite_rule_ok : Sign.sg > term list > term > term 

3893
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

37 
> string option * bool 
1460  38 
val mk_equals : term * term > term 
39 
val mk_flexpair : term * term > term 

40 
val mk_implies : term * term > term 

41 
val mk_inclass : typ * class > term 

42 
val mk_type : typ > term 

43 
val occs : term * term > bool 

44 
val rule_of : (term*term)list * term list * term > term 

45 
val set_rename_prefix : string > unit 

46 
val skip_flexpairs : term > term 

0  47 
val strip_assums_concl: term > term 
1460  48 
val strip_assums_hyp : term > term list 
49 
val strip_flexpairs : term > (term*term)list * term 

50 
val strip_horn : term > (term*term)list * term list * term 

51 
val strip_imp_concl : term > term 

52 
val strip_imp_prems : term > term list 

53 
val strip_params : term > (string * typ) list 

54 
val strip_prems : int * term list * term > term list * term 

2508  55 
val unvarify : term > term 
56 
val varify : term > term 

4345  57 
end; 
0  58 

1500  59 
structure Logic : LOGIC = 
0  60 
struct 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

61 

4345  62 

63 
(** type and term orders **) 

64 

65 
fun indexname_ord ((x, i), (y, j)) = 

66 
(case int_ord (i, j) of EQUAL => string_ord (x, y)  ord => ord); 

67 

68 

69 
(* typ_ord *) 

70 

71 
(*assumes that TFrees / TVars with the same name have same sorts*) 

72 
fun typ_ord (Type (a, Ts), Type (b, Us)) = 

73 
(case string_ord (a, b) of EQUAL => typs_ord (Ts, Us)  ord => ord) 

74 
 typ_ord (Type _, _) = GREATER 

75 
 typ_ord (TFree _, Type _) = LESS 

76 
 typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b) 

77 
 typ_ord (TFree _, TVar _) = GREATER 

78 
 typ_ord (TVar _, Type _) = LESS 

79 
 typ_ord (TVar _, TFree _) = LESS 

80 
 typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj) 

81 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 

82 

83 

84 
(* term_ord *) 

85 

86 
(*a linear wellfounded ACcompatible ordering for terms: 

87 
s < t <=> 1. size(s) < size(t) or 

88 
2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or 

89 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and 

90 
(s1..sn) < (t1..tn) (lexicographically)*) 

91 

92 
fun dest_hd (Const (a, T)) = (((a, 0), T), 0) 

93 
 dest_hd (Free (a, T)) = (((a, 0), T), 1) 

94 
 dest_hd (Var v) = (v, 2) 

95 
 dest_hd (Bound i) = ((("", i), dummyT), 3) 

96 
 dest_hd (Abs (_, T, _)) = ((("", 0), T), 4); 

97 

98 
fun term_ord (Abs (_, T, t), Abs(_, U, u)) = 

99 
(case term_ord (t, u) of EQUAL => typ_ord (T, U)  ord => ord) 

100 
 term_ord (t, u) = 

101 
(case int_ord (size_of_term t, size_of_term u) of 

102 
EQUAL => 

103 
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in 

104 
(case hd_ord (f, g) of EQUAL => terms_ord (ts, us)  ord => ord) 

105 
end 

106 
 ord => ord) 

107 
and hd_ord (f, g) = 

108 
prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) 

109 
and terms_ord (ts, us) = list_ord term_ord (ts, us); 

110 

111 
fun termless tu = (term_ord tu = LESS); 

112 

113 

114 

0  115 
(*** Abstract syntax operations on the metaconnectives ***) 
116 

117 
(** equality **) 

118 

1835  119 
(*Make an equality. DOES NOT CHECK TYPE OF u*) 
64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

120 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  121 

122 
fun dest_equals (Const("==",_) $ t $ u) = (t,u) 

123 
 dest_equals t = raise TERM("dest_equals", [t]); 

124 

637  125 
fun is_equals (Const ("==", _) $ _ $ _) = true 
126 
 is_equals _ = false; 

127 

128 

0  129 
(** implies **) 
130 

131 
fun mk_implies(A,B) = implies $ A $ B; 

132 

133 
fun dest_implies (Const("==>",_) $ A $ B) = (A,B) 

134 
 dest_implies A = raise TERM("dest_implies", [A]); 

135 

136 
(** nested implications **) 

137 

138 
(* [A1,...,An], B goes to A1==>...An==>B *) 

139 
fun list_implies ([], B) = B : term 

140 
 list_implies (A::AS, B) = implies $ A $ list_implies(AS,B); 

141 

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

143 
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B 

144 
 strip_imp_prems _ = []; 

145 

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

147 
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B 

148 
 strip_imp_concl A = A : term; 

149 

150 
(*Strip and return premises: (i, [], A1==>...Ai==>B) 

1460  151 
goes to ([Ai, A(i1),...,A1] , B) (REVERSED) 
0  152 
if i<0 or else i too big then raises TERM*) 
153 
fun strip_prems (0, As, B) = (As, B) 

154 
 strip_prems (i, As, Const("==>", _) $ A $ B) = 

1460  155 
strip_prems (i1, A::As, B) 
0  156 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
157 

158 
(*Count premises  quicker than (length ostrip_prems) *) 

159 
fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) 

160 
 count_prems (_,n) = n; 

161 

162 
(** flexflex constraints **) 

163 

64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

164 
(*Make a constraint.*) 
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

165 
fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; 
0  166 

167 
fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) 

168 
 dest_flexpair t = raise TERM("dest_flexpair", [t]); 

169 

170 
(*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) 

171 
goes to (a1=?=b1) ==>...(an=?=bn)==>C *) 

172 
fun list_flexpairs ([], A) = A 

173 
 list_flexpairs ((t,u)::pairs, A) = 

1460  174 
implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); 
0  175 

176 
(*Make the objectrule tpairs==>As==>B *) 

177 
fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B)); 

178 

179 
(*Remove and return flexflex pairs: 

1460  180 
(a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) 
0  181 
[Tail recursive in order to return a pair of results] *) 
182 
fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = 

183 
strip_flex_aux ((t,u)::pairs, C) 

184 
 strip_flex_aux (pairs,C) = (rev pairs, C); 

185 

186 
fun strip_flexpairs A = strip_flex_aux([], A); 

187 

188 
(*Discard flexflex pairs*) 

189 
fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) = 

1460  190 
skip_flexpairs C 
0  191 
 skip_flexpairs C = C; 
192 

193 
(*strip a proof state (Horn clause): 

194 
(a1==b1)==>...(am==bm)==>B1==>...Bn==>C 

195 
goes to ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C) *) 

196 
fun strip_horn A = 

197 
let val (tpairs,horn) = strip_flexpairs A 

198 
in (tpairs, strip_imp_prems horn, strip_imp_concl horn) end; 

199 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

200 
(** types as terms **) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

201 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

202 
fun mk_type ty = Const ("TYPE", itselfT ty); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

203 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

204 
fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

205 
 dest_type t = raise TERM ("dest_type", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

206 

447  207 
(** class constraints **) 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

208 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

209 
fun mk_inclass (ty, c) = 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

210 
Const (Sign.const_of_class c, itselfT ty > propT) $ mk_type ty; 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

211 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

212 
fun dest_inclass (t as Const (c_class, _) $ ty) = 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

213 
((dest_type ty, Sign.class_of_const c_class) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

214 
handle TERM _ => raise TERM ("dest_inclass", [t])) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

215 
 dest_inclass t = raise TERM ("dest_inclass", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

216 

0  217 

218 
(*** Lowlevel term operations ***) 

219 

220 
(*Does t occur in u? Or is alphaconvertible to u? 

221 
The term t must contain no loose bound variables*) 

222 
fun t occs u = (t aconv u) orelse 

223 
(case u of 

224 
Abs(_,_,body) => t occs body 

1460  225 
 f$t' => t occs f orelse t occs t' 
226 
 _ => false); 

0  227 

228 
(*Close up a formula over all free variables by quantification*) 

229 
fun close_form A = 

230 
list_all_free (map dest_Free (sort atless (term_frees A)), 

1460  231 
A); 
0  232 

233 

234 
(*** Specialized operations for resolution... ***) 

235 

236 
(*For all variables in the term, increment indexnames and lift over the Us 

237 
result is ?Gidx(B.(lev+n1),...,B.lev) where lev is abstraction level *) 

238 
fun incr_indexes (Us: typ list, inc:int) t = 

239 
let fun incr (Var ((a,i), T), lev) = 

1460  240 
Unify.combound (Var((a, i+inc), Us> incr_tvar inc T), 
241 
lev, length Us) 

242 
 incr (Abs (a,T,body), lev) = 

243 
Abs (a, incr_tvar inc T, incr(body,lev+1)) 

244 
 incr (Const(a,T),_) = Const(a, incr_tvar inc T) 

245 
 incr (Free(a,T),_) = Free(a, incr_tvar inc T) 

246 
 incr (f$t, lev) = incr(f,lev) $ incr(t,lev) 

247 
 incr (t,lev) = t 

0  248 
in incr(t,0) end; 
249 

250 
(*Make lifting functions from subgoal and increment. 

251 
lift_abs operates on tpairs (unification constraints) 

252 
lift_all operates on propositions *) 

253 
fun lift_fns (B,inc) = 

254 
let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u 

1460  255 
 lift_abs (Us, Const("all",_)$Abs(a,T,t)) u = 
256 
Abs(a, T, lift_abs (T::Us, t) u) 

257 
 lift_abs (Us, _) u = incr_indexes(rev Us, inc) u 

0  258 
fun lift_all (Us, Const("==>", _) $ A $ B) u = 
1460  259 
implies $ A $ lift_all (Us,B) u 
260 
 lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 

261 
all T $ Abs(a, T, lift_all (T::Us,t) u) 

262 
 lift_all (Us, _) u = incr_indexes(rev Us, inc) u; 

0  263 
in (lift_abs([],B), lift_all([],B)) end; 
264 

265 
(*Strips assumptions in goal, yielding list of hypotheses. *) 

266 
fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B 

267 
 strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t 

268 
 strip_assums_hyp B = []; 

269 

270 
(*Strips assumptions in goal, yielding conclusion. *) 

271 
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B 

272 
 strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t 

273 
 strip_assums_concl B = B; 

274 

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

276 
fun strip_params (Const("==>", _) $ H $ B) = strip_params B 

277 
 strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t 

278 
 strip_params B = []; 

279 

280 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 

281 
where j is the total number of parameters (precomputed) 

282 
If n>0 then deletes assumption n. *) 

283 
fun remove_params j n A = 

284 
if j=0 andalso n<=0 then A (*nothing left to do...*) 

285 
else case A of 

286 
Const("==>", _) $ H $ B => 

1460  287 
if n=1 then (remove_params j (n1) B) 
288 
else implies $ (incr_boundvars j H) $ (remove_params j (n1) B) 

0  289 
 Const("all",_)$Abs(a,T,t) => remove_params (j1) n t 
290 
 _ => if n>0 then raise TERM("remove_params", [A]) 

291 
else A; 

292 

293 
(** Autorenaming of parameters in subgoals **) 

294 

295 
val auto_rename = ref false 

296 
and rename_prefix = ref "ka"; 

297 

298 
(*rename_prefix is not exported; it is set by this function.*) 

299 
fun set_rename_prefix a = 

300 
if a<>"" andalso forall is_letter (explode a) 

301 
then (rename_prefix := a; auto_rename := true) 

302 
else error"rename prefix must be nonempty and consist of letters"; 

303 

304 
(*Makes parameters in a goal have distinctive names (not guaranteed unique!) 

305 
A name clash could cause the printer to rename bound vars; 

306 
then res_inst_tac would not work properly.*) 

307 
fun rename_vars (a, []) = [] 

308 
 rename_vars (a, (_,T)::vars) = 

309 
(a,T) :: rename_vars (bump_string a, vars); 

310 

311 
(*Move all parameters to the front of the subgoal, renaming them apart; 

312 
if n>0 then deletes assumption n. *) 

313 
fun flatten_params n A = 

314 
let val params = strip_params A; 

1460  315 
val vars = if !auto_rename 
316 
then rename_vars (!rename_prefix, params) 

2266  317 
else ListPair.zip (variantlist(map #1 params,[]), 
318 
map #2 params) 

0  319 
in list_all (vars, remove_params (length vars) n A) 
320 
end; 

321 

322 
(*Makes parameters in a goal have the names supplied by the list cs.*) 

323 
fun list_rename_params (cs, Const("==>", _) $ A $ B) = 

324 
implies $ A $ list_rename_params (cs, B) 

325 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 

326 
all T $ Abs(c, T, list_rename_params (cs, t)) 

327 
 list_rename_params (cs, B) = B; 

328 

329 
(*Strips assumptions in goal yielding ( [Hn,...,H1], [xm,...,x1], B ) 

330 
where H1,...,Hn are the hypotheses and x1...xm are the parameters. *) 

331 
fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 

1460  332 
strip_assums_aux (H::Hs, params, B) 
0  333 
 strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) = 
1460  334 
strip_assums_aux (Hs, (a,T)::params, t) 
0  335 
 strip_assums_aux (Hs, params, B) = (Hs, params, B); 
336 

337 
fun strip_assums A = strip_assums_aux ([],[],A); 

338 

339 

340 
(*Produces disagreement pairs, one for each assumption proof, in order. 

341 
A is the first premise of the lifted rule, and thus has the form 

342 
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B) *) 

343 
fun assum_pairs A = 

344 
let val (Hs, params, B) = strip_assums A 

345 
val D = Unify.rlist_abs(params, B) 

346 
fun pairrev ([],pairs) = pairs 

347 
 pairrev (H::Hs,pairs) = 

1460  348 
pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs) 
0  349 
in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *) 
350 
end; 

351 

352 

353 
(*Converts Frees to Vars and TFrees to TVars so that axioms can be written 

354 
without (?) everywhere*) 

355 
fun varify (Const(a,T)) = Const(a, Type.varifyT T) 

356 
 varify (Free(a,T)) = Var((a,0), Type.varifyT T) 

357 
 varify (Var(ixn,T)) = Var(ixn, Type.varifyT T) 

358 
 varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body) 

359 
 varify (f$t) = varify f $ varify t 

360 
 varify t = t; 

361 

546  362 
(*Inverse of varify. Converts axioms back to their original form.*) 
585  363 
fun unvarify (Const(a,T)) = Const(a, Type.unvarifyT T) 
364 
 unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T) 

365 
 unvarify (Var(ixn,T)) = Var(ixn, Type.unvarifyT T) (*non0 index!*) 

366 
 unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body) 

546  367 
 unvarify (f$t) = unvarify f $ unvarify t 
368 
 unvarify t = t; 

369 

2508  370 

371 

4116  372 
(** Test wellformedness of rewrite rules **) 
3893
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

373 

5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

374 
fun vperm (Var _, Var _) = true 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

375 
 vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

376 
 vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

377 
 vperm (t, u) = (t = u); 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

378 

5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

379 
fun var_perm (t, u) = 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

380 
vperm (t, u) andalso eq_set_term (term_vars t, term_vars u); 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

381 

5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

382 
(*simple test for looping rewrite*) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

383 
fun looptest sign prems lhs rhs = 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

384 
is_Var (head_of lhs) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

385 
orelse 
3915  386 
(exists (apl (lhs, op occs)) (rhs :: prems)) 
3893
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

387 
orelse 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

388 
(null prems andalso 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

389 
Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs)); 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

390 
(*the condition "null prems" in the last case is necessary because 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

391 
conditional rewrites with extra variables in the conditions may terminate 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

392 
although the rhs is an instance of the lhs. Example: 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

393 
?m < ?n ==> f(?n) == f(?m)*) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

394 

4116  395 
fun rewrite_rule_extra_vars prems elhs erhs = 
396 
if not ((term_vars erhs) subset 

397 
(union_term (term_vars elhs, List.concat(map term_vars prems)))) 

398 
then Some("extra Var(s) on rhs") else 

399 
if not ((term_tvars erhs) subset 

400 
(term_tvars elhs union List.concat(map term_tvars prems))) 

401 
then Some("extra TVar(s) on rhs") 

402 
else None; 

403 

404 
fun rewrite_rule_ok sign prems lhs rhs = 

3893
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

405 
let 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

406 
val elhs = Pattern.eta_contract lhs; 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

407 
val erhs = Pattern.eta_contract rhs; 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

408 
val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

409 
andalso not (is_Var elhs) 
4116  410 
in (case rewrite_rule_extra_vars prems elhs erhs of 
411 
None => if not perm andalso looptest sign prems elhs erhs 

412 
then Some("loops") 

413 
else None 

414 
 some => some 

3893
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

415 
,perm) 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

416 
end; 
5a1f22e7b359
The simplifier has been improved a little: equations s=t which used to be
nipkow
parents:
3408
diff
changeset

417 

0  418 
end; 