10413
|
1 |
(* Title: Pure/meta_simplifier.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
|
6 |
Meta Simplification
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature META_SIMPLIFIER =
|
|
10 |
sig
|
|
11 |
exception SIMPLIFIER of string * thm
|
|
12 |
type meta_simpset
|
|
13 |
val dest_mss : meta_simpset ->
|
|
14 |
{simps: thm list, congs: thm list, procs: (string * cterm list) list}
|
|
15 |
val empty_mss : meta_simpset
|
|
16 |
val clear_mss : meta_simpset -> meta_simpset
|
|
17 |
val merge_mss : meta_simpset * meta_simpset -> meta_simpset
|
|
18 |
val add_simps : meta_simpset * thm list -> meta_simpset
|
|
19 |
val del_simps : meta_simpset * thm list -> meta_simpset
|
|
20 |
val mss_of : thm list -> meta_simpset
|
|
21 |
val add_congs : meta_simpset * thm list -> meta_simpset
|
|
22 |
val del_congs : meta_simpset * thm list -> meta_simpset
|
|
23 |
val add_simprocs : meta_simpset *
|
|
24 |
(string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
|
|
25 |
-> meta_simpset
|
|
26 |
val del_simprocs : meta_simpset *
|
|
27 |
(string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
|
|
28 |
-> meta_simpset
|
|
29 |
val add_prems : meta_simpset * thm list -> meta_simpset
|
|
30 |
val prems_of_mss : meta_simpset -> thm list
|
|
31 |
val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset
|
|
32 |
val set_mk_sym : meta_simpset * (thm -> thm option) -> meta_simpset
|
|
33 |
val set_mk_eq_True : meta_simpset * (thm -> thm option) -> meta_simpset
|
|
34 |
val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset
|
|
35 |
val trace_simp : bool ref
|
|
36 |
val debug_simp : bool ref
|
|
37 |
val rewrite_cterm : bool * bool * bool
|
|
38 |
-> (meta_simpset -> thm -> thm option)
|
|
39 |
-> meta_simpset -> cterm -> thm
|
|
40 |
val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
|
|
41 |
val rewrite_thm : bool * bool * bool
|
|
42 |
-> (meta_simpset -> thm -> thm option)
|
|
43 |
-> meta_simpset -> thm -> thm
|
|
44 |
val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
|
|
45 |
val rewrite_goal_rule : bool* bool * bool
|
|
46 |
-> (meta_simpset -> thm -> thm option)
|
|
47 |
-> meta_simpset -> int -> thm -> thm
|
|
48 |
end;
|
|
49 |
|
|
50 |
structure MetaSimplifier : META_SIMPLIFIER =
|
|
51 |
struct
|
|
52 |
|
|
53 |
(** diagnostics **)
|
|
54 |
|
|
55 |
exception SIMPLIFIER of string * thm;
|
|
56 |
|
|
57 |
fun prnt warn a = if warn then warning a else writeln a;
|
|
58 |
|
|
59 |
fun prtm warn a sign t =
|
|
60 |
(prnt warn a; prnt warn (Sign.string_of_term sign t));
|
|
61 |
|
|
62 |
fun prctm warn a t =
|
|
63 |
(prnt warn a; prnt warn (Display.string_of_cterm t));
|
|
64 |
|
|
65 |
fun prthm warn a thm =
|
|
66 |
let val {sign, prop, ...} = rep_thm thm
|
|
67 |
in prtm warn a sign prop end;
|
|
68 |
|
|
69 |
val trace_simp = ref false;
|
|
70 |
val debug_simp = ref false;
|
|
71 |
|
|
72 |
fun trace warn a = if !trace_simp then prnt warn a else ();
|
|
73 |
fun debug warn a = if !debug_simp then prnt warn a else ();
|
|
74 |
|
|
75 |
fun trace_term warn a sign t = if !trace_simp then prtm warn a sign t else ();
|
|
76 |
fun trace_cterm warn a t = if !trace_simp then prctm warn a t else ();
|
|
77 |
fun debug_term warn a sign t = if !debug_simp then prtm warn a sign t else ();
|
|
78 |
|
|
79 |
fun trace_thm warn a thm =
|
|
80 |
let val {sign, prop, ...} = rep_thm thm
|
|
81 |
in trace_term warn a sign prop end;
|
|
82 |
|
|
83 |
|
|
84 |
|
|
85 |
(** meta simp sets **)
|
|
86 |
|
|
87 |
(* basic components *)
|
|
88 |
|
|
89 |
type rrule = {thm: thm, lhs: term, elhs: cterm, fo: bool, perm: bool};
|
|
90 |
(* thm: the rewrite rule
|
|
91 |
lhs: the left-hand side
|
|
92 |
elhs: the etac-contracted lhs.
|
|
93 |
fo: use first-order matching
|
|
94 |
perm: the rewrite rule is permutative
|
|
95 |
Reamrks:
|
|
96 |
- elhs is used for matching,
|
|
97 |
lhs only for preservation of bound variable names.
|
|
98 |
- fo is set iff
|
|
99 |
either elhs is first-order (no Var is applied),
|
|
100 |
in which case fo-matching is complete,
|
|
101 |
or elhs is not a pattern,
|
|
102 |
in which case there is nothing better to do.
|
|
103 |
*)
|
|
104 |
type cong = {thm: thm, lhs: cterm};
|
|
105 |
type simproc =
|
|
106 |
{name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
|
|
107 |
|
|
108 |
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
|
|
109 |
#prop (rep_thm thm1) aconv #prop (rep_thm thm2);
|
|
110 |
|
|
111 |
fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
|
|
112 |
#prop (rep_thm thm1) aconv #prop (rep_thm thm2);
|
|
113 |
|
|
114 |
fun eq_prem (thm1, thm2) =
|
|
115 |
#prop (rep_thm thm1) aconv #prop (rep_thm thm2);
|
|
116 |
|
|
117 |
fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
|
|
118 |
|
|
119 |
fun mk_simproc (name, proc, lhs, id) =
|
|
120 |
{name = name, proc = proc, lhs = lhs, id = id};
|
|
121 |
|
|
122 |
|
|
123 |
(* datatype mss *)
|
|
124 |
|
|
125 |
(*
|
|
126 |
A "mss" contains data needed during conversion:
|
|
127 |
rules: discrimination net of rewrite rules;
|
|
128 |
congs: association list of congruence rules and
|
|
129 |
a list of `weak' congruence constants.
|
|
130 |
A congruence is `weak' if it avoids normalization of some argument.
|
|
131 |
procs: discrimination net of simplification procedures
|
|
132 |
(functions that prove rewrite rules on the fly);
|
|
133 |
bounds: names of bound variables already used
|
|
134 |
(for generating new names when rewriting under lambda abstractions);
|
|
135 |
prems: current premises;
|
|
136 |
mk_rews: mk: turns simplification thms into rewrite rules;
|
|
137 |
mk_sym: turns == around; (needs Drule!)
|
|
138 |
mk_eq_True: turns P into P == True - logic specific;
|
|
139 |
termless: relation for ordered rewriting;
|
|
140 |
*)
|
|
141 |
|
|
142 |
datatype meta_simpset =
|
|
143 |
Mss of {
|
|
144 |
rules: rrule Net.net,
|
|
145 |
congs: (string * cong) list * string list,
|
|
146 |
procs: simproc Net.net,
|
|
147 |
bounds: string list,
|
|
148 |
prems: thm list,
|
|
149 |
mk_rews: {mk: thm -> thm list,
|
|
150 |
mk_sym: thm -> thm option,
|
|
151 |
mk_eq_True: thm -> thm option},
|
|
152 |
termless: term * term -> bool};
|
|
153 |
|
|
154 |
fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
|
|
155 |
Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
|
|
156 |
prems=prems, mk_rews=mk_rews, termless=termless};
|
|
157 |
|
|
158 |
fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
|
|
159 |
mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
|
|
160 |
|
|
161 |
val empty_mss =
|
|
162 |
let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
|
|
163 |
in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless) end;
|
|
164 |
|
|
165 |
fun clear_mss (Mss {mk_rews, termless, ...}) =
|
|
166 |
mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);
|
|
167 |
|
|
168 |
|
|
169 |
|
|
170 |
(** simpset operations **)
|
|
171 |
|
|
172 |
(* term variables *)
|
|
173 |
|
|
174 |
val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
|
|
175 |
fun term_varnames t = add_term_varnames ([], t);
|
|
176 |
|
|
177 |
|
|
178 |
(* dest_mss *)
|
|
179 |
|
|
180 |
fun dest_mss (Mss {rules, congs, procs, ...}) =
|
|
181 |
{simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
|
|
182 |
congs = map (fn (_, {thm, ...}) => thm) (fst congs),
|
|
183 |
procs =
|
|
184 |
map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
|
|
185 |
|> partition_eq eq_snd
|
|
186 |
|> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
|
|
187 |
|> Library.sort_wrt #1};
|
|
188 |
|
|
189 |
|
|
190 |
(* merge_mss *) (*NOTE: ignores mk_rews and termless of 2nd mss*)
|
|
191 |
|
|
192 |
fun merge_mss
|
|
193 |
(Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
|
|
194 |
bounds = bounds1, prems = prems1, mk_rews, termless},
|
|
195 |
Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
|
|
196 |
bounds = bounds2, prems = prems2, ...}) =
|
|
197 |
mk_mss
|
|
198 |
(Net.merge (rules1, rules2, eq_rrule),
|
|
199 |
(generic_merge (eq_cong o pairself snd) I I congs1 congs2,
|
|
200 |
merge_lists weak1 weak2),
|
|
201 |
Net.merge (procs1, procs2, eq_simproc),
|
|
202 |
merge_lists bounds1 bounds2,
|
|
203 |
generic_merge eq_prem I I prems1 prems2,
|
|
204 |
mk_rews, termless);
|
|
205 |
|
|
206 |
|
|
207 |
(* add_simps *)
|
|
208 |
|
|
209 |
fun mk_rrule2{thm,lhs,elhs,perm} =
|
|
210 |
let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
|
|
211 |
in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
|
|
212 |
|
|
213 |
fun insert_rrule(mss as Mss {rules,...},
|
|
214 |
rrule as {thm,lhs,elhs,perm}) =
|
|
215 |
(trace_thm false "Adding rewrite rule:" thm;
|
|
216 |
let val rrule2 as {elhs,...} = mk_rrule2 rrule
|
|
217 |
val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
|
|
218 |
in upd_rules(mss,rules') end
|
|
219 |
handle Net.INSERT =>
|
|
220 |
(prthm true "Ignoring duplicate rewrite rule:" thm; mss));
|
|
221 |
|
|
222 |
fun vperm (Var _, Var _) = true
|
|
223 |
| vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
|
|
224 |
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
|
|
225 |
| vperm (t, u) = (t = u);
|
|
226 |
|
|
227 |
fun var_perm (t, u) =
|
|
228 |
vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
|
|
229 |
|
|
230 |
(* FIXME: it seems that the conditions on extra variables are too liberal if
|
|
231 |
prems are nonempty: does solving the prems really guarantee instantiation of
|
|
232 |
all its Vars? Better: a dynamic check each time a rule is applied.
|
|
233 |
*)
|
|
234 |
fun rewrite_rule_extra_vars prems elhs erhs =
|
|
235 |
not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
|
|
236 |
orelse
|
|
237 |
not ((term_tvars erhs) subset
|
|
238 |
(term_tvars elhs union List.concat(map term_tvars prems)));
|
|
239 |
|
|
240 |
(*Simple test for looping rewrite rules and stupid orientations*)
|
|
241 |
fun reorient sign prems lhs rhs =
|
|
242 |
rewrite_rule_extra_vars prems lhs rhs
|
|
243 |
orelse
|
|
244 |
is_Var (head_of lhs)
|
|
245 |
orelse
|
|
246 |
(exists (apl (lhs, Logic.occs)) (rhs :: prems))
|
|
247 |
orelse
|
|
248 |
(null prems andalso
|
|
249 |
Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
|
|
250 |
(*the condition "null prems" is necessary because conditional rewrites
|
|
251 |
with extra variables in the conditions may terminate although
|
|
252 |
the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
|
|
253 |
orelse
|
|
254 |
(is_Const lhs andalso not(is_Const rhs))
|
|
255 |
|
|
256 |
fun decomp_simp thm =
|
|
257 |
let val {sign, prop, ...} = rep_thm thm;
|
|
258 |
val prems = Logic.strip_imp_prems prop;
|
|
259 |
val concl = Drule.strip_imp_concl (cprop_of thm);
|
|
260 |
val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
|
|
261 |
raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
|
|
262 |
val elhs = snd (Drule.dest_equals (cprop_of (Thm.eta_conversion lhs)));
|
|
263 |
val elhs = if elhs=lhs then lhs else elhs (* try to share *)
|
|
264 |
val erhs = Pattern.eta_contract (term_of rhs);
|
|
265 |
val perm = var_perm (term_of elhs, erhs) andalso not (term_of elhs aconv erhs)
|
|
266 |
andalso not (is_Var (term_of elhs))
|
|
267 |
in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
|
|
268 |
|
|
269 |
fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
|
|
270 |
case mk_eq_True thm of
|
|
271 |
None => []
|
|
272 |
| Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
|
|
273 |
in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
|
|
274 |
|
|
275 |
(* create the rewrite rule and possibly also the ==True variant,
|
|
276 |
in case there are extra vars on the rhs *)
|
|
277 |
fun rrule_eq_True(thm,lhs,elhs,rhs,mss,thm2) =
|
|
278 |
let val rrule = {thm=thm, lhs=lhs, elhs=elhs, perm=false}
|
|
279 |
in if (term_varnames rhs) subset (term_varnames lhs) andalso
|
|
280 |
(term_tvars rhs) subset (term_tvars lhs)
|
|
281 |
then [rrule]
|
|
282 |
else mk_eq_True mss thm2 @ [rrule]
|
|
283 |
end;
|
|
284 |
|
|
285 |
fun mk_rrule mss thm =
|
|
286 |
let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
|
|
287 |
in if perm then [{thm=thm, lhs=lhs, elhs=elhs, perm=true}] else
|
|
288 |
(* weak test for loops: *)
|
|
289 |
if rewrite_rule_extra_vars prems lhs rhs orelse
|
|
290 |
is_Var (term_of elhs)
|
|
291 |
then mk_eq_True mss thm
|
|
292 |
else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
|
|
293 |
end;
|
|
294 |
|
|
295 |
fun orient_rrule mss thm =
|
|
296 |
let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
|
|
297 |
in if perm then [{thm=thm,lhs=lhs,elhs=elhs,perm=true}]
|
|
298 |
else if reorient sign prems lhs rhs
|
|
299 |
then if reorient sign prems rhs lhs
|
|
300 |
then mk_eq_True mss thm
|
|
301 |
else let val Mss{mk_rews={mk_sym,...},...} = mss
|
|
302 |
in case mk_sym thm of
|
|
303 |
None => []
|
|
304 |
| Some thm' =>
|
|
305 |
let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
|
|
306 |
in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
|
|
307 |
end
|
|
308 |
else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
|
|
309 |
end;
|
|
310 |
|
|
311 |
fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
|
|
312 |
|
|
313 |
fun orient_comb_simps comb mk_rrule (mss,thms) =
|
|
314 |
let val rews = extract_rews(mss,thms)
|
|
315 |
val rrules = flat (map mk_rrule rews)
|
|
316 |
in foldl comb (mss,rrules) end
|
|
317 |
|
|
318 |
(* Add rewrite rules explicitly; do not reorient! *)
|
|
319 |
fun add_simps(mss,thms) =
|
|
320 |
orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
|
|
321 |
|
|
322 |
fun mss_of thms =
|
|
323 |
foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
|
|
324 |
|
|
325 |
fun extract_safe_rrules(mss,thm) =
|
|
326 |
flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
|
|
327 |
|
|
328 |
fun add_safe_simp(mss,thm) =
|
|
329 |
foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
|
|
330 |
|
|
331 |
(* del_simps *)
|
|
332 |
|
|
333 |
fun del_rrule(mss as Mss {rules,...},
|
|
334 |
rrule as {thm, elhs, ...}) =
|
|
335 |
(upd_rules(mss, Net.delete_term ((term_of elhs, rrule), rules, eq_rrule))
|
|
336 |
handle Net.DELETE =>
|
|
337 |
(prthm true "Rewrite rule not in simpset:" thm; mss));
|
|
338 |
|
|
339 |
fun del_simps(mss,thms) =
|
|
340 |
orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
|
|
341 |
|
|
342 |
|
|
343 |
(* add_congs *)
|
|
344 |
|
|
345 |
fun is_full_cong_prems [] varpairs = null varpairs
|
|
346 |
| is_full_cong_prems (p::prems) varpairs =
|
|
347 |
(case Logic.strip_assums_concl p of
|
|
348 |
Const("==",_) $ lhs $ rhs =>
|
|
349 |
let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
|
|
350 |
in is_Var x andalso forall is_Bound xs andalso
|
|
351 |
null(findrep(xs)) andalso xs=ys andalso
|
|
352 |
(x,y) mem varpairs andalso
|
|
353 |
is_full_cong_prems prems (varpairs\(x,y))
|
|
354 |
end
|
|
355 |
| _ => false);
|
|
356 |
|
|
357 |
fun is_full_cong thm =
|
|
358 |
let val prems = prems_of thm
|
|
359 |
and concl = concl_of thm
|
|
360 |
val (lhs,rhs) = Logic.dest_equals concl
|
|
361 |
val (f,xs) = strip_comb lhs
|
|
362 |
and (g,ys) = strip_comb rhs
|
|
363 |
in
|
|
364 |
f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
|
|
365 |
is_full_cong_prems prems (xs ~~ ys)
|
|
366 |
end
|
|
367 |
|
|
368 |
fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
|
|
369 |
let
|
|
370 |
val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
|
|
371 |
raise SIMPLIFIER ("Congruence not a meta-equality", thm);
|
|
372 |
(* val lhs = Pattern.eta_contract lhs; *)
|
|
373 |
val (a, _) = dest_Const (head_of (term_of lhs)) handle TERM _ =>
|
|
374 |
raise SIMPLIFIER ("Congruence must start with a constant", thm);
|
|
375 |
val (alist,weak) = congs
|
|
376 |
val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
|
|
377 |
("Overwriting congruence rule for " ^ quote a);
|
|
378 |
val weak2 = if is_full_cong thm then weak else a::weak
|
|
379 |
in
|
|
380 |
mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
|
|
381 |
end;
|
|
382 |
|
|
383 |
val (op add_congs) = foldl add_cong;
|
|
384 |
|
|
385 |
|
|
386 |
(* del_congs *)
|
|
387 |
|
|
388 |
fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
|
|
389 |
let
|
|
390 |
val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
|
|
391 |
raise SIMPLIFIER ("Congruence not a meta-equality", thm);
|
|
392 |
(* val lhs = Pattern.eta_contract lhs; *)
|
|
393 |
val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
|
|
394 |
raise SIMPLIFIER ("Congruence must start with a constant", thm);
|
|
395 |
val (alist,_) = congs
|
|
396 |
val alist2 = filter (fn (x,_)=> x<>a) alist
|
|
397 |
val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
|
|
398 |
else Some a)
|
|
399 |
alist2
|
|
400 |
in
|
|
401 |
mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
|
|
402 |
end;
|
|
403 |
|
|
404 |
val (op del_congs) = foldl del_cong;
|
|
405 |
|
|
406 |
|
|
407 |
(* add_simprocs *)
|
|
408 |
|
|
409 |
fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
|
|
410 |
(name, lhs, proc, id)) =
|
|
411 |
let val {sign, t, ...} = rep_cterm lhs
|
|
412 |
in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
|
|
413 |
sign t;
|
|
414 |
mk_mss (rules, congs,
|
|
415 |
Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
|
|
416 |
handle Net.INSERT =>
|
|
417 |
(warning ("Ignoring duplicate simplification procedure \""
|
|
418 |
^ name ^ "\"");
|
|
419 |
procs),
|
|
420 |
bounds, prems, mk_rews, termless))
|
|
421 |
end;
|
|
422 |
|
|
423 |
fun add_simproc (mss, (name, lhss, proc, id)) =
|
|
424 |
foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
|
|
425 |
|
|
426 |
val add_simprocs = foldl add_simproc;
|
|
427 |
|
|
428 |
|
|
429 |
(* del_simprocs *)
|
|
430 |
|
|
431 |
fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
|
|
432 |
(name, lhs, proc, id)) =
|
|
433 |
mk_mss (rules, congs,
|
|
434 |
Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
|
|
435 |
handle Net.DELETE =>
|
|
436 |
(warning ("Simplification procedure \"" ^ name ^
|
|
437 |
"\" not in simpset"); procs),
|
|
438 |
bounds, prems, mk_rews, termless);
|
|
439 |
|
|
440 |
fun del_simproc (mss, (name, lhss, proc, id)) =
|
|
441 |
foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
|
|
442 |
|
|
443 |
val del_simprocs = foldl del_simproc;
|
|
444 |
|
|
445 |
|
|
446 |
(* prems *)
|
|
447 |
|
|
448 |
fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
|
|
449 |
mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
|
|
450 |
|
|
451 |
fun prems_of_mss (Mss {prems, ...}) = prems;
|
|
452 |
|
|
453 |
|
|
454 |
(* mk_rews *)
|
|
455 |
|
|
456 |
fun set_mk_rews
|
|
457 |
(Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
|
|
458 |
mk_mss (rules, congs, procs, bounds, prems,
|
|
459 |
{mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
|
|
460 |
termless);
|
|
461 |
|
|
462 |
fun set_mk_sym
|
|
463 |
(Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
|
|
464 |
mk_mss (rules, congs, procs, bounds, prems,
|
|
465 |
{mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
|
|
466 |
termless);
|
|
467 |
|
|
468 |
fun set_mk_eq_True
|
|
469 |
(Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
|
|
470 |
mk_mss (rules, congs, procs, bounds, prems,
|
|
471 |
{mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
|
|
472 |
termless);
|
|
473 |
|
|
474 |
(* termless *)
|
|
475 |
|
|
476 |
fun set_termless
|
|
477 |
(Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
|
|
478 |
mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
|
|
479 |
|
|
480 |
|
|
481 |
|
|
482 |
(** rewriting **)
|
|
483 |
|
|
484 |
(*
|
|
485 |
Uses conversions, see:
|
|
486 |
L C Paulson, A higher-order implementation of rewriting,
|
|
487 |
Science of Computer Programming 3 (1983), pages 119-149.
|
|
488 |
*)
|
|
489 |
|
|
490 |
type prover = meta_simpset -> thm -> thm option;
|
|
491 |
type termrec = (Sign.sg_ref * term list) * term;
|
|
492 |
type conv = meta_simpset -> termrec -> termrec;
|
|
493 |
|
|
494 |
val dest_eq = Drule.dest_equals o cprop_of;
|
|
495 |
val lhs_of = fst o dest_eq;
|
|
496 |
val rhs_of = snd o dest_eq;
|
|
497 |
|
|
498 |
fun beta_eta_conversion t =
|
|
499 |
let val thm = beta_conversion true t;
|
|
500 |
in transitive thm (eta_conversion (rhs_of thm)) end;
|
|
501 |
|
|
502 |
fun check_conv msg thm thm' =
|
|
503 |
let
|
|
504 |
val thm'' = transitive thm (transitive
|
|
505 |
(symmetric (beta_eta_conversion (lhs_of thm'))) thm')
|
|
506 |
in (if msg then trace_thm false "SUCCEEDED" thm' else (); Some thm'') end
|
|
507 |
handle THM _ =>
|
|
508 |
let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
|
|
509 |
in
|
|
510 |
(trace_thm false "Proved wrong thm (Check subgoaler?)" thm';
|
|
511 |
trace_term false "Should have proved:" sign prop0;
|
|
512 |
None)
|
|
513 |
end;
|
|
514 |
|
|
515 |
|
|
516 |
(* mk_procrule *)
|
|
517 |
|
|
518 |
fun mk_procrule thm =
|
|
519 |
let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
|
|
520 |
in if rewrite_rule_extra_vars prems lhs rhs
|
|
521 |
then (prthm true "Extra vars on rhs:" thm; [])
|
|
522 |
else [mk_rrule2{thm=thm, lhs=lhs, elhs=elhs, perm=false}]
|
|
523 |
end;
|
|
524 |
|
|
525 |
|
|
526 |
(* conversion to apply the meta simpset to a term *)
|
|
527 |
|
|
528 |
(* Since the rewriting strategy is bottom-up, we avoid re-normalizing already
|
|
529 |
normalized terms by carrying around the rhs of the rewrite rule just
|
|
530 |
applied. This is called the `skeleton'. It is decomposed in parallel
|
|
531 |
with the term. Once a Var is encountered, the corresponding term is
|
|
532 |
already in normal form.
|
|
533 |
skel0 is a dummy skeleton that is to enforce complete normalization.
|
|
534 |
*)
|
|
535 |
val skel0 = Bound 0;
|
|
536 |
|
|
537 |
(* Use rhs as skeleton only if the lhs does not contain unnormalized bits.
|
|
538 |
The latter may happen iff there are weak congruence rules for constants
|
|
539 |
in the lhs.
|
|
540 |
*)
|
|
541 |
fun uncond_skel((_,weak),(lhs,rhs)) =
|
|
542 |
if null weak then rhs (* optimization *)
|
|
543 |
else if exists_Const (fn (c,_) => c mem weak) lhs then skel0
|
|
544 |
else rhs;
|
|
545 |
|
|
546 |
(* Behaves like unconditional rule if rhs does not contain vars not in the lhs.
|
|
547 |
Otherwise those vars may become instantiated with unnormalized terms
|
|
548 |
while the premises are solved.
|
|
549 |
*)
|
|
550 |
fun cond_skel(args as (congs,(lhs,rhs))) =
|
|
551 |
if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
|
|
552 |
else skel0;
|
|
553 |
|
|
554 |
(*
|
|
555 |
we try in order:
|
|
556 |
(1) beta reduction
|
|
557 |
(2) unconditional rewrite rules
|
|
558 |
(3) conditional rewrite rules
|
|
559 |
(4) simplification procedures
|
|
560 |
|
|
561 |
IMPORTANT: rewrite rules must not introduce new Vars or TVars!
|
|
562 |
|
|
563 |
*)
|
|
564 |
|
|
565 |
fun rewritec (prover, signt, maxt)
|
|
566 |
(mss as Mss{rules, procs, termless, prems, congs, ...}) t =
|
|
567 |
let
|
|
568 |
val eta_thm = Thm.eta_conversion t;
|
|
569 |
val eta_t' = rhs_of eta_thm;
|
|
570 |
val eta_t = term_of eta_t';
|
|
571 |
val tsigt = Sign.tsig_of signt;
|
|
572 |
fun rew {thm, lhs, elhs, fo, perm} =
|
|
573 |
let
|
|
574 |
val {sign, prop, maxidx, ...} = rep_thm thm;
|
|
575 |
val _ = if Sign.subsig (sign, signt) then ()
|
|
576 |
else (prthm true "Ignoring rewrite rule from different theory:" thm;
|
|
577 |
raise Pattern.MATCH);
|
|
578 |
val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
|
|
579 |
else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
|
|
580 |
val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
|
|
581 |
else Thm.cterm_match (elhs', eta_t');
|
|
582 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
|
|
583 |
val prop' = #prop (rep_thm thm');
|
|
584 |
val unconditional = (Logic.count_prems (prop',0) = 0);
|
|
585 |
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
|
|
586 |
in
|
|
587 |
if perm andalso not (termless (rhs', lhs')) then None
|
|
588 |
else
|
|
589 |
(trace_thm false "Applying instance of rewrite rule:" thm;
|
|
590 |
if unconditional
|
|
591 |
then
|
|
592 |
(trace_thm false "Rewriting:" thm';
|
|
593 |
let val lr = Logic.dest_equals prop;
|
|
594 |
val Some thm'' = check_conv false eta_thm thm'
|
|
595 |
in Some (thm'', uncond_skel (congs, lr)) end)
|
|
596 |
else
|
|
597 |
(trace_thm false "Trying to rewrite:" thm';
|
|
598 |
case prover mss thm' of
|
|
599 |
None => (trace_thm false "FAILED" thm'; None)
|
|
600 |
| Some thm2 =>
|
|
601 |
(case check_conv true eta_thm thm2 of
|
|
602 |
None => None |
|
|
603 |
Some thm2' =>
|
|
604 |
let val concl = Logic.strip_imp_concl prop
|
|
605 |
val lr = Logic.dest_equals concl
|
|
606 |
in Some (thm2', cond_skel (congs, lr)) end)))
|
|
607 |
end
|
|
608 |
|
|
609 |
fun rews [] = None
|
|
610 |
| rews (rrule :: rrules) =
|
|
611 |
let val opt = rew rrule handle Pattern.MATCH => None
|
|
612 |
in case opt of None => rews rrules | some => some end;
|
|
613 |
|
|
614 |
fun sort_rrules rrs = let
|
|
615 |
fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
|
|
616 |
Const("==",_) $ _ $ _ => true
|
|
617 |
| _ => false
|
|
618 |
fun sort [] (re1,re2) = re1 @ re2
|
|
619 |
| sort (rr::rrs) (re1,re2) = if is_simple rr
|
|
620 |
then sort rrs (rr::re1,re2)
|
|
621 |
else sort rrs (re1,rr::re2)
|
|
622 |
in sort rrs ([],[]) end
|
|
623 |
|
|
624 |
fun proc_rews ([]:simproc list) = None
|
|
625 |
| proc_rews ({name, proc, lhs, ...} :: ps) =
|
|
626 |
if Pattern.matches tsigt (term_of lhs, term_of t) then
|
|
627 |
(debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
|
|
628 |
case proc signt prems eta_t of
|
|
629 |
None => (debug false "FAILED"; proc_rews ps)
|
|
630 |
| Some raw_thm =>
|
|
631 |
(trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
|
|
632 |
(case rews (mk_procrule raw_thm) of
|
|
633 |
None => (trace false "IGNORED"; proc_rews ps)
|
|
634 |
| some => some)))
|
|
635 |
else proc_rews ps;
|
|
636 |
in case eta_t of
|
|
637 |
Abs _ $ _ => Some (transitive eta_thm
|
|
638 |
(beta_conversion false (rhs_of eta_thm)), skel0)
|
|
639 |
| _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
|
|
640 |
None => proc_rews (Net.match_term procs eta_t)
|
|
641 |
| some => some)
|
|
642 |
end;
|
|
643 |
|
|
644 |
|
|
645 |
(* conversion to apply a congruence rule to a term *)
|
|
646 |
|
|
647 |
fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
|
|
648 |
let val {sign, ...} = rep_thm cong
|
|
649 |
val _ = if Sign.subsig (sign, signt) then ()
|
|
650 |
else error("Congruence rule from different theory")
|
|
651 |
val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
|
|
652 |
val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
|
|
653 |
val insts = Thm.cterm_match (rlhs, t)
|
|
654 |
(* Pattern.match can raise Pattern.MATCH;
|
|
655 |
is handled when congc is called *)
|
|
656 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
|
|
657 |
val unit = trace_thm false "Applying congruence rule:" thm';
|
|
658 |
fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
|
|
659 |
in case prover thm' of
|
|
660 |
None => err ("Could not prove", thm')
|
|
661 |
| Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
|
|
662 |
None => err ("Should not have proved", thm2)
|
|
663 |
| Some thm2' => thm2')
|
|
664 |
end;
|
|
665 |
|
|
666 |
val (cA, (cB, cC)) =
|
|
667 |
apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
|
|
668 |
|
|
669 |
fun transitive' thm1 None = Some thm1
|
|
670 |
| transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
|
|
671 |
|
|
672 |
fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
|
|
673 |
let
|
|
674 |
fun botc skel mss t =
|
|
675 |
if is_Var skel then None
|
|
676 |
else
|
|
677 |
(case subc skel mss t of
|
|
678 |
some as Some thm1 =>
|
|
679 |
(case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
|
|
680 |
Some (thm2, skel2) =>
|
|
681 |
transitive' (transitive thm1 thm2)
|
|
682 |
(botc skel2 mss (rhs_of thm2))
|
|
683 |
| None => some)
|
|
684 |
| None =>
|
|
685 |
(case rewritec (prover, sign, maxidx) mss t of
|
|
686 |
Some (thm2, skel2) => transitive' thm2
|
|
687 |
(botc skel2 mss (rhs_of thm2))
|
|
688 |
| None => None))
|
|
689 |
|
|
690 |
and try_botc mss t =
|
|
691 |
(case botc skel0 mss t of
|
|
692 |
Some trec1 => trec1 | None => (reflexive t))
|
|
693 |
|
|
694 |
and subc skel
|
|
695 |
(mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
|
|
696 |
(case term_of t0 of
|
|
697 |
Abs (a, T, t) =>
|
|
698 |
let val b = variant bounds a
|
|
699 |
val (v, t') = dest_abs (Some ("." ^ b)) t0
|
|
700 |
val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
|
|
701 |
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
|
|
702 |
in case botc skel' mss' t' of
|
|
703 |
Some thm => Some (abstract_rule a v thm)
|
|
704 |
| None => None
|
|
705 |
end
|
|
706 |
| t $ _ => (case t of
|
|
707 |
Const ("==>", _) $ _ =>
|
|
708 |
let val (s, u) = Drule.dest_implies t0
|
|
709 |
in impc (s, u, mss) end
|
|
710 |
| Abs _ =>
|
|
711 |
let val thm = beta_conversion false t0
|
|
712 |
in case subc skel0 mss (rhs_of thm) of
|
|
713 |
None => Some thm
|
|
714 |
| Some thm' => Some (transitive thm thm')
|
|
715 |
end
|
|
716 |
| _ =>
|
|
717 |
let fun appc () =
|
|
718 |
let
|
|
719 |
val (tskel, uskel) = case skel of
|
|
720 |
tskel $ uskel => (tskel, uskel)
|
|
721 |
| _ => (skel0, skel0);
|
|
722 |
val (ct, cu) = dest_comb t0
|
|
723 |
in
|
|
724 |
(case botc tskel mss ct of
|
|
725 |
Some thm1 =>
|
|
726 |
(case botc uskel mss cu of
|
|
727 |
Some thm2 => Some (combination thm1 thm2)
|
|
728 |
| None => Some (combination thm1 (reflexive cu)))
|
|
729 |
| None =>
|
|
730 |
(case botc uskel mss cu of
|
|
731 |
Some thm1 => Some (combination (reflexive ct) thm1)
|
|
732 |
| None => None))
|
|
733 |
end
|
|
734 |
val (h, ts) = strip_comb t
|
|
735 |
in case h of
|
|
736 |
Const(a, _) =>
|
|
737 |
(case assoc_string (fst congs, a) of
|
|
738 |
None => appc ()
|
|
739 |
| Some cong =>
|
|
740 |
(* post processing: some partial applications h t1 ... tj, j <= length ts,
|
|
741 |
may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
|
|
742 |
(let
|
|
743 |
val thm = congc (prover mss, sign, maxidx) cong t0;
|
|
744 |
val t = rhs_of thm;
|
|
745 |
val (cl, cr) = dest_comb t
|
|
746 |
val dVar = Var(("", 0), dummyT)
|
|
747 |
val skel =
|
|
748 |
list_comb (h, replicate (length ts) dVar)
|
|
749 |
in case botc skel mss cl of
|
|
750 |
None => Some thm
|
|
751 |
| Some thm' => Some (transitive thm
|
|
752 |
(combination thm' (reflexive cr)))
|
|
753 |
end handle TERM _ => error "congc result"
|
|
754 |
| Pattern.MATCH => appc ()))
|
|
755 |
| _ => appc ()
|
|
756 |
end)
|
|
757 |
| _ => None)
|
|
758 |
|
|
759 |
and impc args =
|
|
760 |
if mutsimp
|
|
761 |
then let val (prem, conc, mss) = args
|
|
762 |
in apsome snd (mut_impc ([], prem, conc, mss)) end
|
|
763 |
else nonmut_impc args
|
|
764 |
|
|
765 |
and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
|
|
766 |
None => mut_impc1 (prems, prem, conc, mss)
|
|
767 |
| Some thm1 =>
|
|
768 |
let val prem1 = rhs_of thm1
|
|
769 |
in (case mut_impc1 (prems, prem1, conc, mss) of
|
|
770 |
None => Some (None,
|
|
771 |
combination (combination refl_implies thm1) (reflexive conc))
|
|
772 |
| Some (x, thm2) => Some (x, transitive (combination (combination
|
|
773 |
refl_implies thm1) (reflexive conc)) thm2))
|
|
774 |
end)
|
|
775 |
|
|
776 |
and mut_impc1 (prems, prem1, conc, mss) =
|
|
777 |
let
|
|
778 |
fun uncond ({thm, lhs, elhs, perm}) =
|
|
779 |
if Thm.no_prems thm then Some lhs else None
|
|
780 |
|
|
781 |
val (lhss1, mss1) =
|
|
782 |
if maxidx_of_term (term_of prem1) <> ~1
|
|
783 |
then (trace_cterm true
|
|
784 |
"Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
|
|
785 |
([],mss))
|
|
786 |
else let val thm = assume prem1
|
|
787 |
val rrules1 = extract_safe_rrules (mss, thm)
|
|
788 |
val lhss1 = mapfilter uncond rrules1
|
|
789 |
val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
|
|
790 |
in (lhss1, mss1) end
|
|
791 |
|
|
792 |
fun disch1 thm =
|
|
793 |
let val (cB', cC') = dest_eq thm
|
|
794 |
in
|
|
795 |
implies_elim (Thm.instantiate
|
|
796 |
([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
|
|
797 |
(implies_intr prem1 thm)
|
|
798 |
end
|
|
799 |
|
|
800 |
fun rebuild None = (case rewritec (prover, sign, maxidx) mss
|
|
801 |
(mk_implies (prem1, conc)) of
|
|
802 |
None => None
|
|
803 |
| Some (thm, _) => Some (None, thm))
|
|
804 |
| rebuild (Some thm2) =
|
|
805 |
let val thm = disch1 thm2
|
|
806 |
in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
|
|
807 |
None => Some (None, thm)
|
|
808 |
| Some (thm', _) =>
|
|
809 |
let val (prem, conc) = Drule.dest_implies (rhs_of thm')
|
|
810 |
in (case mut_impc (prems, prem, conc, mss) of
|
|
811 |
None => Some (None, transitive thm thm')
|
|
812 |
| Some (x, thm'') =>
|
|
813 |
Some (x, transitive (transitive thm thm') thm''))
|
|
814 |
end handle TERM _ => Some (None, transitive thm thm'))
|
|
815 |
end
|
|
816 |
|
|
817 |
fun simpconc () =
|
|
818 |
let val (s, t) = Drule.dest_implies conc
|
|
819 |
in case mut_impc (prems @ [prem1], s, t, mss1) of
|
|
820 |
None => rebuild None
|
|
821 |
| Some (Some i, thm2) =>
|
|
822 |
let
|
|
823 |
val (prem, cC') = Drule.dest_implies (rhs_of thm2);
|
|
824 |
val thm2' = transitive (disch1 thm2) (Thm.instantiate
|
|
825 |
([], [(cA, prem1), (cB, prem), (cC, cC')])
|
|
826 |
Drule.swap_prems_eq)
|
|
827 |
in if i=0 then apsome (apsnd (transitive thm2'))
|
|
828 |
(mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
|
|
829 |
else Some (Some (i-1), thm2')
|
|
830 |
end
|
|
831 |
| Some (None, thm) => rebuild (Some thm)
|
|
832 |
end handle TERM _ => rebuild (botc skel0 mss1 conc)
|
|
833 |
|
|
834 |
in
|
|
835 |
let
|
|
836 |
val tsig = Sign.tsig_of sign
|
|
837 |
fun reducible t =
|
|
838 |
exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
|
|
839 |
in case dropwhile (not o reducible) prems of
|
|
840 |
[] => simpconc ()
|
|
841 |
| red::rest => (trace_cterm false "Can now reduce premise:" red;
|
|
842 |
Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
|
|
843 |
end
|
|
844 |
end
|
|
845 |
|
|
846 |
(* legacy code - only for backwards compatibility *)
|
|
847 |
and nonmut_impc (prem, conc, mss) =
|
|
848 |
let val thm1 = if simprem then botc skel0 mss prem else None;
|
|
849 |
val prem1 = if_none (apsome rhs_of thm1) prem;
|
|
850 |
val maxidx1 = maxidx_of_term (term_of prem1)
|
|
851 |
val mss1 =
|
|
852 |
if not useprem then mss else
|
|
853 |
if maxidx1 <> ~1
|
|
854 |
then (trace_cterm true
|
|
855 |
"Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
|
|
856 |
mss)
|
|
857 |
else let val thm = assume prem1
|
|
858 |
in add_safe_simp (add_prems (mss, [thm]), thm) end
|
|
859 |
in (case botc skel0 mss1 conc of
|
|
860 |
None => (case thm1 of
|
|
861 |
None => None
|
|
862 |
| Some thm1' => Some (combination
|
|
863 |
(combination refl_implies thm1') (reflexive conc)))
|
|
864 |
| Some thm2 =>
|
|
865 |
let
|
|
866 |
val conc2 = rhs_of thm2;
|
|
867 |
val thm2' = implies_elim (Thm.instantiate
|
|
868 |
([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
|
|
869 |
(implies_intr prem1 thm2)
|
|
870 |
in (case thm1 of
|
|
871 |
None => Some thm2'
|
|
872 |
| Some thm1' => Some (transitive (combination
|
|
873 |
(combination refl_implies thm1') (reflexive conc)) thm2'))
|
|
874 |
end)
|
|
875 |
end
|
|
876 |
|
|
877 |
in try_botc end;
|
|
878 |
|
|
879 |
|
|
880 |
(*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
|
|
881 |
|
|
882 |
(*
|
|
883 |
Parameters:
|
|
884 |
mode = (simplify A,
|
|
885 |
use A in simplifying B,
|
|
886 |
use prems of B (if B is again a meta-impl.) to simplify A)
|
|
887 |
when simplifying A ==> B
|
|
888 |
mss: contains equality theorems of the form [|p1,...|] ==> t==u
|
|
889 |
prover: how to solve premises in conditional rewrites and congruences
|
|
890 |
*)
|
|
891 |
|
|
892 |
(* FIXME: check that #bounds(mss) does not "occur" in ct already *)
|
|
893 |
|
|
894 |
fun rewrite_cterm mode prover mss ct =
|
|
895 |
let val {sign, t, maxidx, ...} = rep_cterm ct
|
|
896 |
in bottomc (mode, prover, sign, maxidx) mss ct end
|
|
897 |
handle THM (s, _, thms) =>
|
|
898 |
error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
|
|
899 |
Pretty.string_of (pretty_thms thms));
|
|
900 |
|
|
901 |
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
|
|
902 |
(*Do not rewrite flex-flex pairs*)
|
|
903 |
fun goals_conv pred cv =
|
|
904 |
let fun gconv i ct =
|
|
905 |
let val (A,B) = Drule.dest_implies ct
|
|
906 |
val (thA,j) = case term_of A of
|
|
907 |
Const("=?=",_)$_$_ => (reflexive A, i)
|
|
908 |
| _ => (if pred i then cv A else reflexive A, i+1)
|
|
909 |
in combination (combination refl_implies thA) (gconv j B) end
|
|
910 |
handle TERM _ => reflexive ct
|
|
911 |
in gconv 1 end;
|
|
912 |
|
|
913 |
(*Use a conversion to transform a theorem*)
|
|
914 |
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
|
|
915 |
|
|
916 |
(*Rewrite a theorem*)
|
|
917 |
fun rewrite_rule_aux _ [] = (fn th => th)
|
|
918 |
| rewrite_rule_aux prover thms =
|
|
919 |
fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms));
|
|
920 |
|
|
921 |
fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
|
|
922 |
|
|
923 |
(*Rewrite the subgoals of a proof state (represented by a theorem) *)
|
|
924 |
fun rewrite_goals_rule_aux _ [] th = th
|
|
925 |
| rewrite_goals_rule_aux prover thms th =
|
|
926 |
fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
|
|
927 |
(mss_of thms))) th;
|
|
928 |
|
|
929 |
(*Rewrite the subgoal of a proof state (represented by a theorem) *)
|
|
930 |
fun rewrite_goal_rule mode prover mss i thm =
|
|
931 |
if 0 < i andalso i <= nprems_of thm
|
|
932 |
then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
|
|
933 |
else raise THM("rewrite_goal_rule",i,[thm]);
|
|
934 |
|
|
935 |
end;
|
|
936 |
|
|
937 |
open MetaSimplifier;
|