# HG changeset patch
# User haftmann
# Date 1216026287 -7200
# Node ID 33f215fa079e3685b1f6d9efd20aeebd2a67fe8b
# Parent  15173149326426230ae93cc2be65e84c6cce871a
added further simple interfaces

diff -r 151731493264 -r 33f215fa079e src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Mon Jul 14 11:04:46 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Mon Jul 14 11:04:47 2008 +0200
@@ -42,7 +42,7 @@
   val mk_func: thm -> thm
   val head_func: thm -> string * ((string * sort) list * typ)
   val expand_eta: int -> thm -> thm
-  val rewrite_func: thm list -> thm -> thm
+  val rewrite_func: MetaSimplifier.simpset -> thm -> thm
   val norm_args: thm list -> thm list 
   val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list
 
@@ -147,8 +147,8 @@
       else conv ct;
   in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
 
-val rewrite_func = Conv.fconv_rule o func_conv o MetaSimplifier.rewrite false;
-
+fun rewrite_func ss thm = (Conv.fconv_rule o func_conv o
+  (MetaSimplifier.rewrite' (ProofContext.init (Thm.theory_of_thm thm)) false)) ss thm;
 val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
 
 fun norm_args thms =
diff -r 151731493264 -r 33f215fa079e src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Jul 14 11:04:46 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Jul 14 11:04:47 2008 +0200
@@ -41,9 +41,10 @@
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (simpset -> int -> tactic)) list,
     solvers: solver list * solver list}
-  val print_ss: simpset -> unit
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
+  val pretty_ss: simpset -> Pretty.T
+  val print_ss: simpset -> unit
   type simproc
   val eq_simproc: simproc * simproc -> bool
   val morph_simproc: morphism -> simproc -> simproc
@@ -92,6 +93,8 @@
 sig
   include BASIC_META_SIMPLIFIER
   exception SIMPLIFIER of string * thm
+  val add_simp: thm -> simpset -> simpset
+  val del_simp: thm -> simpset -> simpset
   val solver: simpset -> solver -> int -> tactic
   val simp_depth_limit_value: Config.value Config.T
   val simp_depth_limit: int Config.T
@@ -118,7 +121,9 @@
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
   val rewrite: bool -> thm list -> conv
+  val rewrite': Proof.context -> bool -> simpset -> conv;
   val simplify: bool -> thm list -> thm -> thm
+  val simplify': Proof.context -> bool -> simpset -> thm -> thm;
 end;
 
 structure MetaSimplifier: META_SIMPLIFIER =
@@ -327,7 +332,7 @@
 
 (* print simpsets *)
 
-fun print_ss ss =
+fun pretty_ss ss =
   let
     val pretty_thms = map Display.pretty_thm;
 
@@ -350,8 +355,10 @@
       Pretty.strs ("loopers:" :: map (quote o fst) loop_tacs),
       Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
       Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
-    |> Pretty.chunks |> Pretty.writeln
+    |> Pretty.chunks
   end;
+  
+val print_ss = Pretty.writeln o pretty_ss;
 
 
 
@@ -545,6 +552,8 @@
 fun ss delsimps thms =
   comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
 
+fun add_simp thm ss = ss addsimps [thm];
+fun del_simp thm ss = ss delsimps [thm];
 
 (* congs *)
 
@@ -1254,13 +1263,13 @@
 val simple_prover =
   SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
 
-(*Rewrite a cterm*)
+fun rewrite' ctxt full ss = rewrite_cterm (full, false, false) simple_prover (context ctxt ss);
+fun simplify' ctxt full ss = Conv.fconv_rule (rewrite' ctxt full ss);
+
 fun rewrite _ [] ct = Thm.reflexive ct
-  | rewrite full thms ct =
-      rewrite_cterm (full, false, false) simple_prover
-        (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+  | rewrite full thms ct = rewrite' (ProofContext.init (Thm.theory_of_cterm ct))
+      full (empty_ss addsimps thms) ct;
 
-(*Rewrite a theorem*)
 fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 val rewrite_rule = simplify true;