improved tracing of permutative rules.
1 (* Title: Pure/meta_simplifier.ML
4 Copyright 1994 University of Cambridge
9 signature META_SIMPLIFIER =
11 exception SIMPLIFIER of string * thm
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
26 val del_simprocs : meta_simpset *
27 (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
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
50 structure MetaSimplifier : META_SIMPLIFIER =
55 exception SIMPLIFIER of string * thm;
57 fun prnt warn a = if warn then warning a else writeln a;
59 fun prtm warn a sign t =
60 (prnt warn a; prnt warn (Sign.string_of_term sign t));
63 (prnt warn a; prnt warn (Display.string_of_cterm t));
65 fun prthm warn a thm =
66 let val {sign, prop, ...} = rep_thm thm
67 in prtm warn a sign prop end;
69 val trace_simp = ref false;
70 val debug_simp = ref false;
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 ();
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 ();
79 fun trace_thm warn a thm =
80 let val {sign, prop, ...} = rep_thm thm
81 in trace_term warn a sign prop end;
85 (** meta simp sets **)
87 (* basic components *)
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
96 - elhs is used for matching,
97 lhs only for preservation of bound variable names.
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.
104 type cong = {thm: thm, lhs: cterm};
106 {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
108 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
109 #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
111 fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
112 #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
114 fun eq_prem (thm1, thm2) =
115 #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
117 fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
119 fun mk_simproc (name, proc, lhs, id) =
120 {name = name, proc = proc, lhs = lhs, id = id};
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;
142 datatype meta_simpset =
144 rules: rrule Net.net,
145 congs: (string * cong) list * string list,
146 procs: simproc Net.net,
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};
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};
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);
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;
165 fun clear_mss (Mss {mk_rews, termless, ...}) =
166 mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);
170 (** simpset operations **)
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);
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),
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};
190 (* merge_mss *) (*NOTE: ignores mk_rews and termless of 2nd 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, ...}) =
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,
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
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
220 (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
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);
227 fun var_perm (t, u) =
228 vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
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.
234 fun rewrite_rule_extra_vars prems elhs erhs =
235 not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
237 not ((term_tvars erhs) subset
238 (term_tvars elhs union List.concat(map term_tvars prems)));
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
246 (exists (apl (lhs, Logic.occs)) (rhs :: prems))
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)*)
254 (is_Const lhs andalso not(is_Const rhs))
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;
269 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
270 case mk_eq_True thm of
272 | Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
273 in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
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)
282 else mk_eq_True mss thm2 @ [rrule]
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)
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
305 let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
306 in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
308 else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
311 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
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
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);
323 foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
325 fun extract_safe_rrules(mss,thm) =
326 flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
328 fun add_safe_simp(mss,thm) =
329 foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
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))
337 (prthm true "Rewrite rule not in simpset:" thm; mss));
339 fun del_simps(mss,thms) =
340 orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
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))
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
364 f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
365 is_full_cong_prems prems (xs ~~ ys)
368 fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
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
380 mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
383 val (op add_congs) = foldl add_cong;
388 fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
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
401 mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
404 val (op del_congs) = foldl del_cong;
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")
414 mk_mss (rules, congs,
415 Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
417 (warning ("Ignoring duplicate simplification procedure \""
420 bounds, prems, mk_rews, termless))
423 fun add_simproc (mss, (name, lhss, proc, id)) =
424 foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
426 val add_simprocs = foldl add_simproc;
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)
436 (warning ("Simplification procedure \"" ^ name ^
437 "\" not in simpset"); procs),
438 bounds, prems, mk_rews, termless);
440 fun del_simproc (mss, (name, lhss, proc, id)) =
441 foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
443 val del_simprocs = foldl del_simproc;
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);
451 fun prems_of_mss (Mss {prems, ...}) = prems;
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},
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},
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},
477 (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
478 mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
485 Uses conversions, see:
486 L C Paulson, A higher-order implementation of rewriting,
487 Science of Computer Programming 3 (1983), pages 119-149.
490 type prover = meta_simpset -> thm -> thm option;
491 type termrec = (Sign.sg_ref * term list) * term;
492 type conv = meta_simpset -> termrec -> termrec;
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;
498 fun beta_eta_conversion t =
499 let val thm = beta_conversion true t;
500 in transitive thm (eta_conversion (rhs_of thm)) end;
502 fun check_conv msg thm thm' =
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
508 let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
510 (trace_thm false "Proved wrong thm (Check subgoaler?)" thm';
511 trace_term false "Should have proved:" sign prop0;
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}]
526 (* conversion to apply the meta simpset to a term *)
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.
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
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
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.
550 fun cond_skel(args as (congs,(lhs,rhs))) =
551 if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
557 (2) unconditional rewrite rules
558 (3) conditional rewrite rules
559 (4) simplification procedures
561 IMPORTANT: rewrite rules must not introduce new Vars or TVars!
565 fun rewritec (prover, signt, maxt)
566 (mss as Mss{rules, procs, termless, prems, congs, ...}) t =
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} =
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')
587 if perm andalso not (termless (rhs', lhs'))
588 then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
589 trace_thm false "Term does not become smaller:" thm'; None)
591 (trace_thm false "Applying instance of rewrite rule:" thm;
594 (trace_thm false "Rewriting:" thm';
595 let val lr = Logic.dest_equals prop;
596 val Some thm'' = check_conv false eta_thm thm'
597 in Some (thm'', uncond_skel (congs, lr)) end)
599 (trace_thm false "Trying to rewrite:" thm';
600 case prover mss thm' of
601 None => (trace_thm false "FAILED" thm'; None)
603 (case check_conv true eta_thm thm2 of
606 let val concl = Logic.strip_imp_concl prop
607 val lr = Logic.dest_equals concl
608 in Some (thm2', cond_skel (congs, lr)) end)))
612 | rews (rrule :: rrules) =
613 let val opt = rew rrule handle Pattern.MATCH => None
614 in case opt of None => rews rrules | some => some end;
616 fun sort_rrules rrs = let
617 fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
618 Const("==",_) $ _ $ _ => true
620 fun sort [] (re1,re2) = re1 @ re2
621 | sort (rr::rrs) (re1,re2) = if is_simple rr
622 then sort rrs (rr::re1,re2)
623 else sort rrs (re1,rr::re2)
624 in sort rrs ([],[]) end
626 fun proc_rews ([]:simproc list) = None
627 | proc_rews ({name, proc, lhs, ...} :: ps) =
628 if Pattern.matches tsigt (term_of lhs, term_of t) then
629 (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
630 case proc signt prems eta_t of
631 None => (debug false "FAILED"; proc_rews ps)
633 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
634 (case rews (mk_procrule raw_thm) of
635 None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
639 Abs _ $ _ => Some (transitive eta_thm
640 (beta_conversion false (rhs_of eta_thm)), skel0)
641 | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
642 None => proc_rews (Net.match_term procs eta_t)
647 (* conversion to apply a congruence rule to a term *)
649 fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
650 let val {sign, ...} = rep_thm cong
651 val _ = if Sign.subsig (sign, signt) then ()
652 else error("Congruence rule from different theory")
653 val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
654 val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
655 val insts = Thm.cterm_match (rlhs, t)
656 (* Pattern.match can raise Pattern.MATCH;
657 is handled when congc is called *)
658 val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
659 val unit = trace_thm false "Applying congruence rule:" thm';
660 fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
661 in case prover thm' of
662 None => err ("Could not prove", thm')
663 | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
664 None => err ("Should not have proved", thm2)
665 | Some thm2' => thm2')
669 apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
671 fun transitive' thm1 None = Some thm1
672 | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
674 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
676 fun botc skel mss t =
677 if is_Var skel then None
679 (case subc skel mss t of
681 (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
682 Some (thm2, skel2) =>
683 transitive' (transitive thm1 thm2)
684 (botc skel2 mss (rhs_of thm2))
687 (case rewritec (prover, sign, maxidx) mss t of
688 Some (thm2, skel2) => transitive' thm2
689 (botc skel2 mss (rhs_of thm2))
693 (case botc skel0 mss t of
694 Some trec1 => trec1 | None => (reflexive t))
697 (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
700 let val b = variant bounds a
701 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
702 val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
703 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
704 in case botc skel' mss' t' of
705 Some thm => Some (abstract_rule a v thm)
708 | t $ _ => (case t of
709 Const ("==>", _) $ _ =>
710 let val (s, u) = Drule.dest_implies t0
711 in impc (s, u, mss) end
713 let val thm = beta_conversion false t0
714 in case subc skel0 mss (rhs_of thm) of
716 | Some thm' => Some (transitive thm thm')
721 val (tskel, uskel) = case skel of
722 tskel $ uskel => (tskel, uskel)
723 | _ => (skel0, skel0);
724 val (ct, cu) = Thm.dest_comb t0
726 (case botc tskel mss ct of
728 (case botc uskel mss cu of
729 Some thm2 => Some (combination thm1 thm2)
730 | None => Some (combination thm1 (reflexive cu)))
732 (case botc uskel mss cu of
733 Some thm1 => Some (combination (reflexive ct) thm1)
736 val (h, ts) = strip_comb t
739 (case assoc_string (fst congs, a) of
742 (* post processing: some partial applications h t1 ... tj, j <= length ts,
743 may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
745 val thm = congc (prover mss, sign, maxidx) cong t0;
747 val (cl, cr) = Thm.dest_comb t
748 val dVar = Var(("", 0), dummyT)
750 list_comb (h, replicate (length ts) dVar)
751 in case botc skel mss cl of
753 | Some thm' => Some (transitive thm
754 (combination thm' (reflexive cr)))
755 end handle TERM _ => error "congc result"
756 | Pattern.MATCH => appc ()))
763 then let val (prem, conc, mss) = args
764 in apsome snd (mut_impc ([], prem, conc, mss)) end
765 else nonmut_impc args
767 and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
768 None => mut_impc1 (prems, prem, conc, mss)
770 let val prem1 = rhs_of thm1
771 in (case mut_impc1 (prems, prem1, conc, mss) of
773 combination (combination refl_implies thm1) (reflexive conc))
774 | Some (x, thm2) => Some (x, transitive (combination (combination
775 refl_implies thm1) (reflexive conc)) thm2))
778 and mut_impc1 (prems, prem1, conc, mss) =
780 fun uncond ({thm, lhs, elhs, perm}) =
781 if Thm.no_prems thm then Some lhs else None
784 if maxidx_of_term (term_of prem1) <> ~1
785 then (trace_cterm true
786 "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
788 else let val thm = assume prem1
789 val rrules1 = extract_safe_rrules (mss, thm)
790 val lhss1 = mapfilter uncond rrules1
791 val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
795 let val (cB', cC') = dest_eq thm
797 implies_elim (Thm.instantiate
798 ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
799 (implies_intr prem1 thm)
802 fun rebuild None = (case rewritec (prover, sign, maxidx) mss
803 (mk_implies (prem1, conc)) of
805 | Some (thm, _) => Some (None, thm))
806 | rebuild (Some thm2) =
807 let val thm = disch1 thm2
808 in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
809 None => Some (None, thm)
811 let val (prem, conc) = Drule.dest_implies (rhs_of thm')
812 in (case mut_impc (prems, prem, conc, mss) of
813 None => Some (None, transitive thm thm')
815 Some (x, transitive (transitive thm thm') thm''))
816 end handle TERM _ => Some (None, transitive thm thm'))
820 let val (s, t) = Drule.dest_implies conc
821 in case mut_impc (prems @ [prem1], s, t, mss1) of
823 | Some (Some i, thm2) =>
825 val (prem, cC') = Drule.dest_implies (rhs_of thm2);
826 val thm2' = transitive (disch1 thm2) (Thm.instantiate
827 ([], [(cA, prem1), (cB, prem), (cC, cC')])
829 in if i=0 then apsome (apsnd (transitive thm2'))
830 (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
831 else Some (Some (i-1), thm2')
833 | Some (None, thm) => rebuild (Some thm)
834 end handle TERM _ => rebuild (botc skel0 mss1 conc)
838 val tsig = Sign.tsig_of sign
840 exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
841 in case dropwhile (not o reducible) prems of
843 | red::rest => (trace_cterm false "Can now reduce premise:" red;
844 Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
848 (* legacy code - only for backwards compatibility *)
849 and nonmut_impc (prem, conc, mss) =
850 let val thm1 = if simprem then botc skel0 mss prem else None;
851 val prem1 = if_none (apsome rhs_of thm1) prem;
852 val maxidx1 = maxidx_of_term (term_of prem1)
854 if not useprem then mss else
856 then (trace_cterm true
857 "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
859 else let val thm = assume prem1
860 in add_safe_simp (add_prems (mss, [thm]), thm) end
861 in (case botc skel0 mss1 conc of
862 None => (case thm1 of
864 | Some thm1' => Some (combination
865 (combination refl_implies thm1') (reflexive conc)))
868 val conc2 = rhs_of thm2;
869 val thm2' = implies_elim (Thm.instantiate
870 ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
871 (implies_intr prem1 thm2)
874 | Some thm1' => Some (transitive (combination
875 (combination refl_implies thm1') (reflexive conc)) thm2'))
882 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
887 use A in simplifying B,
888 use prems of B (if B is again a meta-impl.) to simplify A)
889 when simplifying A ==> B
890 mss: contains equality theorems of the form [|p1,...|] ==> t==u
891 prover: how to solve premises in conditional rewrites and congruences
894 (* FIXME: check that #bounds(mss) does not "occur" in ct already *)
896 fun rewrite_cterm mode prover mss ct =
897 let val {sign, t, maxidx, ...} = rep_cterm ct
898 in bottomc (mode, prover, sign, maxidx) mss ct end
899 handle THM (s, _, thms) =>
900 error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
901 Pretty.string_of (pretty_thms thms));
903 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
904 (*Do not rewrite flex-flex pairs*)
905 fun goals_conv pred cv =
907 let val (A,B) = Drule.dest_implies ct
908 val (thA,j) = case term_of A of
909 Const("=?=",_)$_$_ => (reflexive A, i)
910 | _ => (if pred i then cv A else reflexive A, i+1)
911 in combination (combination refl_implies thA) (gconv j B) end
912 handle TERM _ => reflexive ct
915 (*Use a conversion to transform a theorem*)
916 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
918 (*Rewrite a theorem*)
919 fun rewrite_rule_aux _ [] = (fn th => th)
920 | rewrite_rule_aux prover thms =
921 fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms));
923 fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
925 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
926 fun rewrite_goals_rule_aux _ [] th = th
927 | rewrite_goals_rule_aux prover thms th =
928 fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
931 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
932 fun rewrite_goal_rule mode prover mss i thm =
933 if 0 < i andalso i <= nprems_of thm
934 then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
935 else raise THM("rewrite_goal_rule",i,[thm]);