src/HOL/Tools/Groebner_Basis/normalizer_data.ML

 *)
 
 signature NORMALIZER_DATA =
 sig
   type entry
-  val get: Proof.context -> (thm * entry) list
+  val get: Proof.context -> simpset * ((thm * entry) list)
   val match: Proof.context -> cterm -> entry option
   val del: attribute
   val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
     -> attribute
   val funs: thm -> {is_const: morphism -> cterm -> bool,

 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
 structure Data = GenericDataFun
 (
-  type T = (thm * entry) list;
-  val empty = [];
+  type T = simpset * ((thm * entry) list);
+  val empty = (HOL_basic_ss, []);
   val extend = I;
-  fun merge _ = AList.merge eq_key (K true);
+  fun merge _ ((ss, e), (ss', e')) = (merge_ss (ss, ss'), 
+                                      AList.merge eq_key (K true) (e,e'));
 );
 
 val get = Data.get o Context.Proof;
 
 

       end;
 
     fun match_struct (_,
         entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
       get_first (match_inst entry) (sr_ops @ r_ops);
-  in get_first match_struct (get ctxt) end;
+  in get_first match_struct (snd (get ctxt)) end;
 
 
 (* logical content *)
 
 val semiringN = "semiring";
 val ringN = "ring";
 val idomN = "idom";
 
 fun undefined _ = raise Match;
 
-fun del_data key = remove eq_data (key, []);
+fun del_data key = apsnd (remove eq_data (key, []));
 
 val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+val del_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
 
 fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom} =
   Thm.declaration_attribute (fn key => fn context => context |> Data.map
     let
       val ctxt = Context.proof_of context;

       val _ = map print_thm sr_rules';
       val semiring = (sr_ops, sr_rules');
       val ring = (r_ops, r_rules');
     in
       del_data key #>
-      cons (key, ({vars = vars, semiring = semiring, ring = ring, idom = idom},
-        {is_const = undefined, dest_const = undefined, mk_const = undefined,
-          conv = undefined}))
+      apsnd (cons (key, ({vars = vars, semiring = semiring, ring = ring, idom = idom},
+             {is_const = undefined, dest_const = undefined, mk_const = undefined,
+             conv = undefined})))
     end);
 
 
 (* extra-logical functions *)
 
-fun funs raw_key {is_const, dest_const, mk_const, conv} phi = Data.map (fn data =>
+fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
+ (Data.map o apsnd) (fn data =>
   let
     val key = Morphism.thm phi raw_key;
     val _ = AList.defined eq_key data key orelse
       raise THM ("No data entry for structure key", 0, [key]);
     val fns = {is_const = is_const phi, dest_const = dest_const phi,

 
 
 (* theory setup *)
 
 val setup =
-  Attrib.add_attributes [("normalizer", att_syntax, "semiring normalizer data")];
+  Attrib.add_attributes 
+     [("normalizer", att_syntax, "semiring normalizer data"),
+      ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")];
 
 end;