# HG changeset patch
# User chaieb
# Date 1181636148 -7200
# Node ID 42b827dfa86b05a1731978617ecb4675e1e6b736
# Parent  2443224cf6d79ba598cddd9bd60af95738c9c46a
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;

diff -r 2443224cf6d7 -r 42b827dfa86b src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Tue Jun 12 10:15:45 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Tue Jun 12 10:15:48 2007 +0200
@@ -8,7 +8,7 @@
 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}
@@ -40,10 +40,11 @@
 
 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;
@@ -77,7 +78,7 @@
     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 *)
@@ -88,9 +89,14 @@
 
 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
@@ -132,15 +138,16 @@
       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
@@ -193,6 +200,8 @@
 (* 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;