# 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 @@ "\ P \ (P \ 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;