author chaieb Tue, 12 Jun 2007 10:15:48 +0200 changeset 23335 42b827dfa86b parent 23334 2443224cf6d7 child 23336 21a7433c4bd3
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;
```--- 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);
+   (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")];