# HG changeset patch
# User nipkow
# Date 1107445559 -3600
# Node ID 3263daa9616705c9470e8d81ac831f432c0e5596
# Parent  50fde6f04e4c3818bf5e6df6d25961cd61f26747
added find_rewrites

diff -r 50fde6f04e4c -r 3263daa96167 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Feb 03 16:06:19 2005 +0100
+++ b/src/Provers/simplifier.ML	Thu Feb 03 16:45:59 2005 +0100
@@ -103,6 +103,7 @@
   val get_delta_simpset: ProofContext.context -> Thm.thm list
   val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
 
+  val find_rewrites: string -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure Simplifier: SIMPLIFIER =
@@ -226,6 +227,21 @@
 val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
 
 
+(* find rewrites *)
+
+fun find_rewrites s = Toplevel.keep (fn state =>
+  let
+    val pstate = Toplevel.enter_forward_proof state
+    val ctxt = Proof.context_of pstate;
+    val prt_fact = ProofContext.pretty_fact ctxt
+    val thy = ProofContext.theory_of ctxt
+    val t = ProofContext.read_term ctxt s;
+    val (_, {mk_rews = {mk,...}, ...})  = rep_ss (simpset_of thy)
+    val lhs = fst o Logic.dest_equals o Logic.strip_imp_concl
+    val rews = map (apsnd single) (PureThy.find_matching_thms (mk,lhs) thy t)
+  in map prt_fact (rev rews) |> Pretty.chunks |> Pretty.writeln end);
+
+
 (* change global simpset *)
 
 fun change_simpset_of f x thy =
@@ -545,7 +561,11 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
       (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
 
-val _ = OuterSyntax.add_parsers [print_simpsetP];
+val find_rewritesP =
+  OuterSyntax.improper_command "find_rewrites" "find and print rewrites" OuterSyntax.Keyword.diag
+    (OuterParse.term >> (Toplevel.no_timing oo find_rewrites));
+
+val _ = OuterSyntax.add_parsers [print_simpsetP,find_rewritesP];
 
 end;