src/Pure/meta_simplifier.ML

--- a/src/Pure/meta_simplifier.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -51,10 +51,10 @@
   val addsimprocs: simpset * simproc list -> simpset
   val delsimprocs: simpset * simproc list -> simpset
   val mksimps: simpset -> thm -> thm list
-  val setmksimps: simpset * (thm -> thm list) -> simpset
-  val setmkcong: simpset * (thm -> thm) -> simpset
-  val setmksym: simpset * (thm -> thm option) -> simpset
-  val setmkeqTrue: simpset * (thm -> thm option) -> simpset
+  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
+  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
+  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
+  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   val settermless: simpset * (term * term -> bool) -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   val setloop': simpset * (simpset -> int -> tactic) -> simpset
@@ -92,10 +92,10 @@
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
     mk_rews:
-     {mk: thm -> thm list,
-      mk_cong: thm -> thm,
-      mk_sym: thm -> thm option,
-      mk_eq_True: thm -> thm option,
+     {mk: simpset -> thm -> thm list,
+      mk_cong: simpset -> thm -> thm,
+      mk_sym: simpset -> thm -> thm option,
+      mk_eq_True: simpset -> thm -> thm option,
       reorient: theory -> term list -> term -> term -> bool},
     termless: term * term -> bool,
     subgoal_tac: simpset -> int -> tactic,
@@ -181,13 +181,6 @@
       mk_eq_True: turn P into P == True;
     termless: relation for ordered rewriting;*)
 
-type mk_rews =
- {mk: thm -> thm list,
-  mk_cong: thm -> thm,
-  mk_sym: thm -> thm option,
-  mk_eq_True: thm -> thm option,
-  reorient: theory -> term list -> term -> term -> bool};
-
 datatype simpset =
   Simpset of
    {rules: rrule Net.net,
@@ -197,7 +190,12 @@
     context: Proof.context option} *
    {congs: (string * thm) list * string list,
     procs: proc Net.net,
-    mk_rews: mk_rews,
+    mk_rews:
+     {mk: simpset -> thm -> thm list,
+      mk_cong: simpset -> thm -> thm,
+      mk_sym: simpset -> thm -> thm option,
+      mk_eq_True: simpset -> thm -> thm option,
+      reorient: theory -> term list -> term -> term -> bool},
     termless: term * term -> bool,
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (simpset -> int -> tactic)) list,
@@ -458,8 +456,8 @@
     else (lhs, rhs)
   end;
 
-fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
-  (case mk_eq_True thm of
+fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
+  (case mk_eq_True ss thm of
     NONE => []
   | SOME eq_True =>
       let
@@ -495,7 +493,7 @@
       if reorient thy prems rhs lhs
       then mk_eq_True ss (thm, name)
       else
-        (case mk_sym thm of
+        (case mk_sym ss thm of
           NONE => []
         | SOME thm' =>
             let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
@@ -503,8 +501,8 @@
     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   end;
 
-fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
+fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
+  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
 
 fun extract_safe_rrules (ss, thm) =
   maps (orient_rrule ss) (extract_rews (ss, [thm]));
@@ -588,7 +586,7 @@
         if is_full_cong thm then NONE else SOME a);
     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
 
-fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
+fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
 
 in
 
@@ -674,7 +672,7 @@
 
 in
 
-fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
+fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
 
 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
@@ -762,14 +760,14 @@
   init_ss mk_rews termless subgoal_tac solvers
   |> inherit_context ss;
 
-val basic_mk_rews: mk_rews =
- {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
-  mk_cong = I,
-  mk_sym = SOME o Drule.symmetric_fun,
-  mk_eq_True = K NONE,
-  reorient = default_reorient};
-
-val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
+val empty_ss =
+  init_ss
+    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+      mk_cong = K I,
+      mk_sym = K (SOME o Drule.symmetric_fun),
+      mk_eq_True = K (K NONE),
+      reorient = default_reorient}
+    Term_Ord.termless (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)