--- 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 =
--- 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
--- 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;