moved presimplification rules for algebraic methods into named thms functor
authorhaftmann
Thu May 06 16:40:02 2010 +0200 (2010-05-06)
changeset 36702b455ebd63799
parent 36701 787c33a0e468
child 36703 6e870d7f32e5
moved presimplification rules for algebraic methods into named thms functor
src/HOL/Groebner_Basis.thy
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:21 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:40:02 2010 +0200
     1.3 @@ -412,6 +412,15 @@
     1.4      "\<not> P \<Longrightarrow> (P \<equiv> False)"
     1.5    by auto
     1.6  
     1.7 +ML {*
     1.8 +structure Algebra_Simplification = Named_Thms(
     1.9 +  val name = "algebra"
    1.10 +  val description = "pre-simplification rules for algebraic methods"
    1.11 +)
    1.12 +*}
    1.13 +
    1.14 +setup Algebra_Simplification.setup
    1.15 +
    1.16  use "Tools/Groebner_Basis/groebner.ML"
    1.17  
    1.18  method_setup algebra =
     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 16:32:21 2010 +0200
     2.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 16:40:02 2010 +0200
     2.3 @@ -966,10 +966,12 @@
     2.4            dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
     2.5            (semiring_normalize_wrapper ctxt res)) form));
     2.6  
     2.7 +fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt
     2.8 +  (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms));
     2.9 +
    2.10  fun ring_tac add_ths del_ths ctxt =
    2.11    Object_Logic.full_atomize_tac
    2.12 -  THEN' asm_full_simp_tac
    2.13 -    (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths)
    2.14 +  THEN' presimplify ctxt add_ths del_ths
    2.15    THEN' CSUBGOAL (fn (p, i) =>
    2.16      rtac (let val form = Object_Logic.dest_judgment p
    2.17            in case get_ring_ideal_convs ctxt form of
    2.18 @@ -988,8 +990,7 @@
    2.19     | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
    2.20  in 
    2.21  fun ideal_tac add_ths del_ths ctxt = 
    2.22 -  asm_full_simp_tac 
    2.23 -   (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths) 
    2.24 +  presimplify ctxt add_ths del_ths
    2.25   THEN'
    2.26   CSUBGOAL (fn (p, i) =>
    2.27    case get_ring_ideal_convs ctxt p of
     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:32:21 2010 +0200
     3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:40:02 2010 +0200
     3.3 @@ -113,11 +113,6 @@
     3.4  fun del_data key = apsnd (remove eq_data (key, []));
     3.5  
     3.6  val del = Thm.declaration_attribute (Data.map o del_data);
     3.7 -val add_ss = Thm.declaration_attribute 
     3.8 -   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
     3.9 -
    3.10 -val del_ss = Thm.declaration_attribute 
    3.11 -   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
    3.12  
    3.13  fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
    3.14           field = (f_ops, f_rules), idom, ideal} =
    3.15 @@ -872,8 +867,6 @@
    3.16  
    3.17  (* theory setup *)
    3.18  
    3.19 -val setup =
    3.20 -  normalizer_setup #>
    3.21 -  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
    3.22 +val setup = normalizer_setup
    3.23  
    3.24  end;