# HG changeset patch
# User haftmann
# Date 1273156802 -7200
# Node ID b455ebd637999ae73120a0a6a147bd12df8fa7dc
# Parent  787c33a0e4682a6a05429996bd1d29f9347237a0
moved presimplification rules for algebraic methods into named thms functor

diff -r 787c33a0e468 -r b455ebd63799 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:21 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:40:02 2010 +0200
@@ -412,6 +412,15 @@
     "\<not> P \<Longrightarrow> (P \<equiv> False)"
   by auto
 
+ML {*
+structure Algebra_Simplification = Named_Thms(
+  val name = "algebra"
+  val description = "pre-simplification rules for algebraic methods"
+)
+*}
+
+setup Algebra_Simplification.setup
+
 use "Tools/Groebner_Basis/groebner.ML"
 
 method_setup algebra =
diff -r 787c33a0e468 -r b455ebd63799 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 16:32:21 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 16:40:02 2010 +0200
@@ -966,10 +966,12 @@
           dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
           (semiring_normalize_wrapper ctxt res)) form));
 
+fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt
+  (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms));
+
 fun ring_tac add_ths del_ths ctxt =
   Object_Logic.full_atomize_tac
-  THEN' asm_full_simp_tac
-    (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths)
+  THEN' presimplify ctxt add_ths del_ths
   THEN' CSUBGOAL (fn (p, i) =>
     rtac (let val form = Object_Logic.dest_judgment p
           in case get_ring_ideal_convs ctxt form of
@@ -988,8 +990,7 @@
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
 in 
 fun ideal_tac add_ths del_ths ctxt = 
-  asm_full_simp_tac 
-   (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths) 
+  presimplify ctxt add_ths del_ths
  THEN'
  CSUBGOAL (fn (p, i) =>
   case get_ring_ideal_convs ctxt p of
diff -r 787c33a0e468 -r b455ebd63799 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:32:21 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:40:02 2010 +0200
@@ -113,11 +113,6 @@
 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), 
          field = (f_ops, f_rules), idom, ideal} =
@@ -872,8 +867,6 @@
 
 (* theory setup *)
 
-val setup =
-  normalizer_setup #>
-  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
+val setup = normalizer_setup
 
 end;