dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
authorhaftmann
Thu May 06 16:32:20 2010 +0200 (2010-05-06)
changeset 367009b85b9d74b83
parent 36699 816da1023508
child 36701 787c33a0e468
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
src/HOL/Groebner_Basis.thy
src/HOL/IsaMakefile
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
src/HOL/ex/Groebner_Examples.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:53:21 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:20 2010 +0200
     1.3 @@ -7,14 +7,13 @@
     1.4  theory Groebner_Basis
     1.5  imports Numeral_Simprocs Nat_Transfer
     1.6  uses
     1.7 -  "Tools/Groebner_Basis/normalizer_data.ML"
     1.8    "Tools/Groebner_Basis/normalizer.ML"
     1.9    ("Tools/Groebner_Basis/groebner.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Semiring normalization *}
    1.13  
    1.14 -setup NormalizerData.setup
    1.15 +setup Normalizer.setup
    1.16  
    1.17  locale gb_semiring =
    1.18    fixes add mul pwr r0 r1
    1.19 @@ -203,7 +202,7 @@
    1.20  in
    1.21  
    1.22  fun normalizer_funs key =
    1.23 -  NormalizerData.funs key
    1.24 +  Normalizer.funs key
    1.25     {is_const = fn phi => numeral_is_const,
    1.26      dest_const = fn phi => fn ct =>
    1.27        Rat.rat_of_int (snd
    1.28 @@ -217,7 +216,6 @@
    1.29  
    1.30  declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
    1.31  
    1.32 -
    1.33  locale gb_ring = gb_semiring +
    1.34    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.35      and neg :: "'a \<Rightarrow> 'a"
    1.36 @@ -246,14 +244,6 @@
    1.37  
    1.38  declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
    1.39  
    1.40 -use "Tools/Groebner_Basis/normalizer.ML"
    1.41 -
    1.42 -
    1.43 -method_setup sring_norm = {*
    1.44 -  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
    1.45 -*} "semiring normalizer"
    1.46 -
    1.47 -
    1.48  locale gb_field = gb_ring +
    1.49    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.50      and inverse:: "'a \<Rightarrow> 'a"
    1.51 @@ -421,6 +411,7 @@
    1.52      "P \<equiv> False \<Longrightarrow> \<not> P"
    1.53      "\<not> P \<Longrightarrow> (P \<equiv> False)"
    1.54    by auto
    1.55 +
    1.56  use "Tools/Groebner_Basis/groebner.ML"
    1.57  
    1.58  method_setup algebra =
    1.59 @@ -674,7 +665,7 @@
    1.60  in
    1.61   val field_comp_conv = comp_conv;
    1.62   val fieldgb_declaration = 
    1.63 -  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
    1.64 +  Normalizer.funs @{thm class_fieldgb.fieldgb_axioms'}
    1.65     {is_const = K numeral_is_const,
    1.66      dest_const = K dest_const,
    1.67      mk_const = mk_const,
     2.1 --- a/src/HOL/IsaMakefile	Wed May 05 16:53:21 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu May 06 16:32:20 2010 +0200
     2.3 @@ -284,9 +284,7 @@
     2.4    Tools/ATP_Manager/atp_manager.ML \
     2.5    Tools/ATP_Manager/atp_systems.ML \
     2.6    Tools/Groebner_Basis/groebner.ML \
     2.7 -  Tools/Groebner_Basis/misc.ML \
     2.8    Tools/Groebner_Basis/normalizer.ML \
     2.9 -  Tools/Groebner_Basis/normalizer_data.ML \
    2.10    Tools/choice_specification.ML \
    2.11    Tools/int_arith.ML \
    2.12    Tools/list_code.ML \
     3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed May 05 16:53:21 2010 +0200
     3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 16:32:20 2010 +0200
     3.3 @@ -1195,7 +1195,7 @@
     3.4  fun real_nonlinear_prover proof_method ctxt =
     3.5   let
     3.6    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
     3.7 -      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
     3.8 +      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
     3.9       simple_cterm_ord
    3.10    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
    3.11         real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
    3.12 @@ -1310,7 +1310,7 @@
    3.13  fun real_nonlinear_subst_prover prover ctxt =
    3.14   let
    3.15    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.16 -      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    3.17 +      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    3.18       simple_cterm_ord
    3.19  
    3.20    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
     4.1 --- a/src/HOL/Library/normarith.ML	Wed May 05 16:53:21 2010 +0200
     4.2 +++ b/src/HOL/Library/normarith.ML	Thu May 06 16:32:20 2010 +0200
     4.3 @@ -167,7 +167,7 @@
     4.4    (* FIXME : Should be computed statically!! *)
     4.5    val real_poly_conv = 
     4.6      Normalizer.semiring_normalize_wrapper ctxt
     4.7 -     (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
     4.8 +     (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
     4.9   in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
    4.10  end;
    4.11  
    4.12 @@ -278,7 +278,7 @@
    4.13     (* FIXME: Should be computed statically!!*)
    4.14     val real_poly_conv = 
    4.15        Normalizer.semiring_normalize_wrapper ctxt
    4.16 -       (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    4.17 +       (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    4.18     val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
    4.19     val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
    4.20     val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
    4.21 @@ -384,7 +384,7 @@
    4.22    let 
    4.23     val real_poly_neg_conv = #neg
    4.24         (Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.25 -        (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    4.26 +        (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    4.27     val (th1,th2) = conj_pair(rawrule th)
    4.28    in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
    4.29    end
     5.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed May 05 16:53:21 2010 +0200
     5.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 16:32:20 2010 +0200
     5.3 @@ -748,7 +748,7 @@
     5.4    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
     5.5    val {add,mul,neg,pow,sub,main} = 
     5.6       Normalizer.semiring_normalizers_ord_wrapper ctxt
     5.7 -      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
     5.8 +      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     5.9       simple_cterm_ord
    5.10  in gen_real_arith ctxt
    5.11     (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
     6.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed May 05 16:53:21 2010 +0200
     6.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 16:32:20 2010 +0200
     6.3 @@ -947,7 +947,7 @@
     6.4   case try (find_term 0) form of
     6.5    NONE => NONE
     6.6  | SOME tm =>
     6.7 -  (case NormalizerData.match ctxt tm of
     6.8 +  (case Normalizer.match ctxt tm of
     6.9      NONE => NONE
    6.10    | SOME (res as (theory, {is_const, dest_const, 
    6.11            mk_const, conv = ring_eq_conv})) =>
    6.12 @@ -959,7 +959,7 @@
    6.13    (case try (find_term 0 (* FIXME !? *)) form of
    6.14      NONE => reflexive form
    6.15    | SOME tm =>
    6.16 -      (case NormalizerData.match ctxt tm of
    6.17 +      (case Normalizer.match ctxt tm of
    6.18          NONE => reflexive form
    6.19        | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
    6.20          #ring_conv (ring_and_ideal_conv theory
    6.21 @@ -969,7 +969,7 @@
    6.22  fun ring_tac add_ths del_ths ctxt =
    6.23    Object_Logic.full_atomize_tac
    6.24    THEN' asm_full_simp_tac
    6.25 -    (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
    6.26 +    (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths)
    6.27    THEN' CSUBGOAL (fn (p, i) =>
    6.28      rtac (let val form = Object_Logic.dest_judgment p
    6.29            in case get_ring_ideal_convs ctxt form of
    6.30 @@ -989,7 +989,7 @@
    6.31  in 
    6.32  fun ideal_tac add_ths del_ths ctxt = 
    6.33    asm_full_simp_tac 
    6.34 -   (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths) 
    6.35 +   (Simplifier.context ctxt (fst (Normalizer.get ctxt)) delsimps del_ths addsimps add_ths) 
    6.36   THEN'
    6.37   CSUBGOAL (fn (p, i) =>
    6.38    case get_ring_ideal_convs ctxt p of
     7.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed May 05 16:53:21 2010 +0200
     7.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:32:20 2010 +0200
     7.3 @@ -1,27 +1,235 @@
     7.4  (*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     7.5      Author:     Amine Chaieb, TU Muenchen
     7.6 +
     7.7 +Normalization of expressions in semirings.
     7.8  *)
     7.9  
    7.10  signature NORMALIZER = 
    7.11  sig
    7.12 - val semiring_normalize_conv : Proof.context -> conv
    7.13 - val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
    7.14 - val semiring_normalize_tac : Proof.context -> int -> tactic
    7.15 - val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> conv
    7.16 - val semiring_normalizers_ord_wrapper :  
    7.17 -     Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) ->
    7.18 +  type entry
    7.19 +  val get: Proof.context -> simpset * (thm * entry) list
    7.20 +  val match: Proof.context -> cterm -> entry option
    7.21 +  val del: attribute
    7.22 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
    7.23 +    -> attribute
    7.24 +  val funs: thm -> {is_const: morphism -> cterm -> bool,
    7.25 +    dest_const: morphism -> cterm -> Rat.rat,
    7.26 +    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    7.27 +    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    7.28 +
    7.29 +  val semiring_normalize_conv : Proof.context -> conv
    7.30 +  val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
    7.31 +  val semiring_normalize_wrapper :  Proof.context -> entry -> conv
    7.32 +  val semiring_normalize_ord_wrapper :  Proof.context -> entry ->
    7.33 +    (cterm -> cterm -> bool) -> conv
    7.34 +  val semiring_normalizers_conv :
    7.35 +    cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
    7.36 +      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    7.37 +        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    7.38 +  val semiring_normalizers_ord_wrapper :  
    7.39 +    Proof.context -> entry -> (cterm -> cterm -> bool) ->
    7.40        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    7.41 - val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
    7.42 -   (cterm -> cterm -> bool) -> conv
    7.43 - val semiring_normalizers_conv :
    7.44 -     cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
    7.45 -     (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    7.46 -       {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    7.47 +
    7.48 +  val setup: theory -> theory
    7.49  end
    7.50  
    7.51  structure Normalizer: NORMALIZER = 
    7.52  struct
    7.53  
    7.54 +(* data *)
    7.55 +
    7.56 +type entry =
    7.57 + {vars: cterm list,
    7.58 +  semiring: cterm list * thm list,
    7.59 +  ring: cterm list * thm list,
    7.60 +  field: cterm list * thm list,
    7.61 +  idom: thm list,
    7.62 +  ideal: thm list} *
    7.63 + {is_const: cterm -> bool,
    7.64 +  dest_const: cterm -> Rat.rat,
    7.65 +  mk_const: ctyp -> Rat.rat -> cterm,
    7.66 +  conv: Proof.context -> cterm -> thm};
    7.67 +
    7.68 +val eq_key = Thm.eq_thm;
    7.69 +fun eq_data arg = eq_fst eq_key arg;
    7.70 +
    7.71 +structure Data = Generic_Data
    7.72 +(
    7.73 +  type T = simpset * (thm * entry) list;
    7.74 +  val empty = (HOL_basic_ss, []);
    7.75 +  val extend = I;
    7.76 +  fun merge ((ss, e), (ss', e')) : T =
    7.77 +    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
    7.78 +);
    7.79 +
    7.80 +val get = Data.get o Context.Proof;
    7.81 +
    7.82 +
    7.83 +(* match data *)
    7.84 +
    7.85 +fun match ctxt tm =
    7.86 +  let
    7.87 +    fun match_inst
    7.88 +        ({vars, semiring = (sr_ops, sr_rules), 
    7.89 +          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    7.90 +         fns as {is_const, dest_const, mk_const, conv}) pat =
    7.91 +       let
    7.92 +        fun h instT =
    7.93 +          let
    7.94 +            val substT = Thm.instantiate (instT, []);
    7.95 +            val substT_cterm = Drule.cterm_rule substT;
    7.96 +
    7.97 +            val vars' = map substT_cterm vars;
    7.98 +            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    7.99 +            val ring' = (map substT_cterm r_ops, map substT r_rules);
   7.100 +            val field' = (map substT_cterm f_ops, map substT f_rules);
   7.101 +            val idom' = map substT idom;
   7.102 +            val ideal' = map substT ideal;
   7.103 +
   7.104 +            val result = ({vars = vars', semiring = semiring', 
   7.105 +                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
   7.106 +          in SOME result end
   7.107 +      in (case try Thm.match (pat, tm) of
   7.108 +           NONE => NONE
   7.109 +         | SOME (instT, _) => h instT)
   7.110 +      end;
   7.111 +
   7.112 +    fun match_struct (_,
   7.113 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
   7.114 +      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
   7.115 +  in get_first match_struct (snd (get ctxt)) end;
   7.116 +
   7.117 +
   7.118 +(* logical content *)
   7.119 +
   7.120 +val semiringN = "semiring";
   7.121 +val ringN = "ring";
   7.122 +val idomN = "idom";
   7.123 +val idealN = "ideal";
   7.124 +val fieldN = "field";
   7.125 +
   7.126 +fun undefined _ = raise Match;
   7.127 +
   7.128 +fun del_data key = apsnd (remove eq_data (key, []));
   7.129 +
   7.130 +val del = Thm.declaration_attribute (Data.map o del_data);
   7.131 +val add_ss = Thm.declaration_attribute 
   7.132 +   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
   7.133 +
   7.134 +val del_ss = Thm.declaration_attribute 
   7.135 +   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
   7.136 +
   7.137 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   7.138 +         field = (f_ops, f_rules), idom, ideal} =
   7.139 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   7.140 +    let
   7.141 +      val ctxt = Context.proof_of context;
   7.142 +
   7.143 +      fun check kind name xs n =
   7.144 +        null xs orelse length xs = n orelse
   7.145 +        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   7.146 +      val check_ops = check "operations";
   7.147 +      val check_rules = check "rules";
   7.148 +
   7.149 +      val _ =
   7.150 +        check_ops semiringN sr_ops 5 andalso
   7.151 +        check_rules semiringN sr_rules 37 andalso
   7.152 +        check_ops ringN r_ops 2 andalso
   7.153 +        check_rules ringN r_rules 2 andalso
   7.154 +        check_ops fieldN f_ops 2 andalso
   7.155 +        check_rules fieldN f_rules 2 andalso
   7.156 +        check_rules idomN idom 2;
   7.157 +
   7.158 +      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   7.159 +      val sr_rules' = map mk_meta sr_rules;
   7.160 +      val r_rules' = map mk_meta r_rules;
   7.161 +      val f_rules' = map mk_meta f_rules;
   7.162 +
   7.163 +      fun rule i = nth sr_rules' (i - 1);
   7.164 +
   7.165 +      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   7.166 +      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   7.167 +      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   7.168 +      val ((clx, crx), (cly, cry)) =
   7.169 +        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   7.170 +      val ((ca, cb), (cc, cd)) =
   7.171 +        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   7.172 +      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   7.173 +      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   7.174 +
   7.175 +      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   7.176 +      val semiring = (sr_ops, sr_rules');
   7.177 +      val ring = (r_ops, r_rules');
   7.178 +      val field = (f_ops, f_rules');
   7.179 +      val ideal' = map (symmetric o mk_meta) ideal
   7.180 +    in
   7.181 +      del_data key #>
   7.182 +      apsnd (cons (key, ({vars = vars, semiring = semiring, 
   7.183 +                          ring = ring, field = field, idom = idom, ideal = ideal'},
   7.184 +             {is_const = undefined, dest_const = undefined, mk_const = undefined,
   7.185 +             conv = undefined})))
   7.186 +    end);
   7.187 +
   7.188 +
   7.189 +(* extra-logical functions *)
   7.190 +
   7.191 +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   7.192 + (Data.map o apsnd) (fn data =>
   7.193 +  let
   7.194 +    val key = Morphism.thm phi raw_key;
   7.195 +    val _ = AList.defined eq_key data key orelse
   7.196 +      raise THM ("No data entry for structure key", 0, [key]);
   7.197 +    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   7.198 +      mk_const = mk_const phi, conv = conv phi};
   7.199 +  in AList.map_entry eq_key key (apsnd (K fns)) data end);
   7.200 +
   7.201 +
   7.202 +(* concrete syntax *)
   7.203 +
   7.204 +local
   7.205 +
   7.206 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   7.207 +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   7.208 +fun keyword3 k1 k2 k3 =
   7.209 +  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   7.210 +
   7.211 +val opsN = "ops";
   7.212 +val rulesN = "rules";
   7.213 +
   7.214 +val normN = "norm";
   7.215 +val constN = "const";
   7.216 +val delN = "del";
   7.217 +
   7.218 +val any_keyword =
   7.219 +  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   7.220 +  keyword2 ringN opsN || keyword2 ringN rulesN ||
   7.221 +  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   7.222 +  keyword2 idomN rulesN || keyword2 idealN rulesN;
   7.223 +
   7.224 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   7.225 +val terms = thms >> map Drule.dest_term;
   7.226 +
   7.227 +fun optional scan = Scan.optional scan [];
   7.228 +
   7.229 +in
   7.230 +
   7.231 +val normalizer_setup =
   7.232 +  Attrib.setup @{binding normalizer}
   7.233 +    (Scan.lift (Args.$$$ delN >> K del) ||
   7.234 +      ((keyword2 semiringN opsN |-- terms) --
   7.235 +       (keyword2 semiringN rulesN |-- thms)) --
   7.236 +      (optional (keyword2 ringN opsN |-- terms) --
   7.237 +       optional (keyword2 ringN rulesN |-- thms)) --
   7.238 +      (optional (keyword2 fieldN opsN |-- terms) --
   7.239 +       optional (keyword2 fieldN rulesN |-- thms)) --
   7.240 +      optional (keyword2 idomN rulesN |-- thms) --
   7.241 +      optional (keyword2 idealN rulesN |-- thms)
   7.242 +      >> (fn ((((sr, r), f), id), idl) => 
   7.243 +             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   7.244 +    "semiring normalizer data";
   7.245 +
   7.246 +end;
   7.247 +
   7.248  open Conv;
   7.249  
   7.250  (* Very basic stuff for terms *)
   7.251 @@ -55,6 +263,7 @@
   7.252  val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   7.253                  @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
   7.254                  @{thm "less_nat_number_of"}];
   7.255 +
   7.256  val nat_add_conv = 
   7.257   zerone_conv 
   7.258    (Simplifier.rewrite 
   7.259 @@ -64,7 +273,6 @@
   7.260                   @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
   7.261               @ map (fn th => th RS sym) @{thms numerals}));
   7.262  
   7.263 -val nat_mul_conv = nat_add_conv;
   7.264  val zeron_tm = @{cterm "0::nat"};
   7.265  val onen_tm  = @{cterm "1::nat"};
   7.266  val true_tm = @{cterm "True"};
   7.267 @@ -182,7 +390,7 @@
   7.268            then
   7.269              let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   7.270                  val (l,r) = Thm.dest_comb(concl th1)
   7.271 -           in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
   7.272 +           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   7.273             end
   7.274             else
   7.275              if opr aconvc mul_tm
   7.276 @@ -656,14 +864,16 @@
   7.277    semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   7.278  
   7.279  fun semiring_normalize_ord_conv ctxt ord tm =
   7.280 -  (case NormalizerData.match ctxt tm of
   7.281 +  (case match ctxt tm of
   7.282      NONE => reflexive tm
   7.283    | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   7.284   
   7.285 -
   7.286  fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   7.287  
   7.288 -fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
   7.289 -  rtac (semiring_normalize_conv ctxt
   7.290 -    (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
   7.291 +(* theory setup *)
   7.292 +
   7.293 +val setup =
   7.294 +  normalizer_setup #>
   7.295 +  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
   7.296 +
   7.297  end;
     8.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Wed May 05 16:53:21 2010 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,226 +0,0 @@
     8.4 -(*  Title:      HOL/Tools/Groebner_Basis/normalizer_data.ML
     8.5 -    Author:     Amine Chaieb, TU Muenchen
     8.6 -
     8.7 -Ring normalization data.
     8.8 -*)
     8.9 -
    8.10 -signature NORMALIZER_DATA =
    8.11 -sig
    8.12 -  type entry
    8.13 -  val get: Proof.context -> simpset * (thm * entry) list
    8.14 -  val match: Proof.context -> cterm -> entry option
    8.15 -  val del: attribute
    8.16 -  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
    8.17 -    -> attribute
    8.18 -  val funs: thm -> {is_const: morphism -> cterm -> bool,
    8.19 -    dest_const: morphism -> cterm -> Rat.rat,
    8.20 -    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    8.21 -    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    8.22 -  val setup: theory -> theory
    8.23 -end;
    8.24 -
    8.25 -structure NormalizerData: NORMALIZER_DATA =
    8.26 -struct
    8.27 -
    8.28 -(* data *)
    8.29 -
    8.30 -type entry =
    8.31 - {vars: cterm list,
    8.32 -  semiring: cterm list * thm list,
    8.33 -  ring: cterm list * thm list,
    8.34 -  field: cterm list * thm list,
    8.35 -  idom: thm list,
    8.36 -  ideal: thm list} *
    8.37 - {is_const: cterm -> bool,
    8.38 -  dest_const: cterm -> Rat.rat,
    8.39 -  mk_const: ctyp -> Rat.rat -> cterm,
    8.40 -  conv: Proof.context -> cterm -> thm};
    8.41 -
    8.42 -val eq_key = Thm.eq_thm;
    8.43 -fun eq_data arg = eq_fst eq_key arg;
    8.44 -
    8.45 -structure Data = Generic_Data
    8.46 -(
    8.47 -  type T = simpset * (thm * entry) list;
    8.48 -  val empty = (HOL_basic_ss, []);
    8.49 -  val extend = I;
    8.50 -  fun merge ((ss, e), (ss', e')) : T =
    8.51 -    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
    8.52 -);
    8.53 -
    8.54 -val get = Data.get o Context.Proof;
    8.55 -
    8.56 -
    8.57 -(* match data *)
    8.58 -
    8.59 -fun match ctxt tm =
    8.60 -  let
    8.61 -    fun match_inst
    8.62 -        ({vars, semiring = (sr_ops, sr_rules), 
    8.63 -          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    8.64 -         fns as {is_const, dest_const, mk_const, conv}) pat =
    8.65 -       let
    8.66 -        fun h instT =
    8.67 -          let
    8.68 -            val substT = Thm.instantiate (instT, []);
    8.69 -            val substT_cterm = Drule.cterm_rule substT;
    8.70 -
    8.71 -            val vars' = map substT_cterm vars;
    8.72 -            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    8.73 -            val ring' = (map substT_cterm r_ops, map substT r_rules);
    8.74 -            val field' = (map substT_cterm f_ops, map substT f_rules);
    8.75 -            val idom' = map substT idom;
    8.76 -            val ideal' = map substT ideal;
    8.77 -
    8.78 -            val result = ({vars = vars', semiring = semiring', 
    8.79 -                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    8.80 -          in SOME result end
    8.81 -      in (case try Thm.match (pat, tm) of
    8.82 -           NONE => NONE
    8.83 -         | SOME (instT, _) => h instT)
    8.84 -      end;
    8.85 -
    8.86 -    fun match_struct (_,
    8.87 -        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
    8.88 -      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
    8.89 -  in get_first match_struct (snd (get ctxt)) end;
    8.90 -
    8.91 -
    8.92 -(* logical content *)
    8.93 -
    8.94 -val semiringN = "semiring";
    8.95 -val ringN = "ring";
    8.96 -val idomN = "idom";
    8.97 -val idealN = "ideal";
    8.98 -val fieldN = "field";
    8.99 -
   8.100 -fun undefined _ = raise Match;
   8.101 -
   8.102 -fun del_data key = apsnd (remove eq_data (key, []));
   8.103 -
   8.104 -val del = Thm.declaration_attribute (Data.map o del_data);
   8.105 -val add_ss = Thm.declaration_attribute 
   8.106 -   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
   8.107 -
   8.108 -val del_ss = Thm.declaration_attribute 
   8.109 -   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
   8.110 -
   8.111 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   8.112 -         field = (f_ops, f_rules), idom, ideal} =
   8.113 -  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   8.114 -    let
   8.115 -      val ctxt = Context.proof_of context;
   8.116 -
   8.117 -      fun check kind name xs n =
   8.118 -        null xs orelse length xs = n orelse
   8.119 -        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   8.120 -      val check_ops = check "operations";
   8.121 -      val check_rules = check "rules";
   8.122 -
   8.123 -      val _ =
   8.124 -        check_ops semiringN sr_ops 5 andalso
   8.125 -        check_rules semiringN sr_rules 37 andalso
   8.126 -        check_ops ringN r_ops 2 andalso
   8.127 -        check_rules ringN r_rules 2 andalso
   8.128 -        check_ops fieldN f_ops 2 andalso
   8.129 -        check_rules fieldN f_rules 2 andalso
   8.130 -        check_rules idomN idom 2;
   8.131 -
   8.132 -      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   8.133 -      val sr_rules' = map mk_meta sr_rules;
   8.134 -      val r_rules' = map mk_meta r_rules;
   8.135 -      val f_rules' = map mk_meta f_rules;
   8.136 -
   8.137 -      fun rule i = nth sr_rules' (i - 1);
   8.138 -
   8.139 -      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   8.140 -      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.141 -      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.142 -      val ((clx, crx), (cly, cry)) =
   8.143 -        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.144 -      val ((ca, cb), (cc, cd)) =
   8.145 -        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.146 -      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   8.147 -      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   8.148 -
   8.149 -      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   8.150 -      val semiring = (sr_ops, sr_rules');
   8.151 -      val ring = (r_ops, r_rules');
   8.152 -      val field = (f_ops, f_rules');
   8.153 -      val ideal' = map (symmetric o mk_meta) ideal
   8.154 -    in
   8.155 -      del_data key #>
   8.156 -      apsnd (cons (key, ({vars = vars, semiring = semiring, 
   8.157 -                          ring = ring, field = field, idom = idom, ideal = ideal'},
   8.158 -             {is_const = undefined, dest_const = undefined, mk_const = undefined,
   8.159 -             conv = undefined})))
   8.160 -    end);
   8.161 -
   8.162 -
   8.163 -(* extra-logical functions *)
   8.164 -
   8.165 -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   8.166 - (Data.map o apsnd) (fn data =>
   8.167 -  let
   8.168 -    val key = Morphism.thm phi raw_key;
   8.169 -    val _ = AList.defined eq_key data key orelse
   8.170 -      raise THM ("No data entry for structure key", 0, [key]);
   8.171 -    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   8.172 -      mk_const = mk_const phi, conv = conv phi};
   8.173 -  in AList.map_entry eq_key key (apsnd (K fns)) data end);
   8.174 -
   8.175 -
   8.176 -(* concrete syntax *)
   8.177 -
   8.178 -local
   8.179 -
   8.180 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   8.181 -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   8.182 -fun keyword3 k1 k2 k3 =
   8.183 -  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   8.184 -
   8.185 -val opsN = "ops";
   8.186 -val rulesN = "rules";
   8.187 -
   8.188 -val normN = "norm";
   8.189 -val constN = "const";
   8.190 -val delN = "del";
   8.191 -
   8.192 -val any_keyword =
   8.193 -  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   8.194 -  keyword2 ringN opsN || keyword2 ringN rulesN ||
   8.195 -  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   8.196 -  keyword2 idomN rulesN || keyword2 idealN rulesN;
   8.197 -
   8.198 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   8.199 -val terms = thms >> map Drule.dest_term;
   8.200 -
   8.201 -fun optional scan = Scan.optional scan [];
   8.202 -
   8.203 -in
   8.204 -
   8.205 -val normalizer_setup =
   8.206 -  Attrib.setup @{binding normalizer}
   8.207 -    (Scan.lift (Args.$$$ delN >> K del) ||
   8.208 -      ((keyword2 semiringN opsN |-- terms) --
   8.209 -       (keyword2 semiringN rulesN |-- thms)) --
   8.210 -      (optional (keyword2 ringN opsN |-- terms) --
   8.211 -       optional (keyword2 ringN rulesN |-- thms)) --
   8.212 -      (optional (keyword2 fieldN opsN |-- terms) --
   8.213 -       optional (keyword2 fieldN rulesN |-- thms)) --
   8.214 -      optional (keyword2 idomN rulesN |-- thms) --
   8.215 -      optional (keyword2 idealN rulesN |-- thms)
   8.216 -      >> (fn ((((sr, r), f), id), idl) => 
   8.217 -             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   8.218 -    "semiring normalizer data";
   8.219 -
   8.220 -end;
   8.221 -
   8.222 -
   8.223 -(* theory setup *)
   8.224 -
   8.225 -val setup =
   8.226 -  normalizer_setup #>
   8.227 -  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
   8.228 -
   8.229 -end;
     9.1 --- a/src/HOL/ex/Groebner_Examples.thy	Wed May 05 16:53:21 2010 +0200
     9.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Thu May 06 16:32:20 2010 +0200
     9.3 @@ -10,14 +10,26 @@
     9.4  
     9.5  subsection {* Basic examples *}
     9.6  
     9.7 -schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
     9.8 -  by sring_norm
     9.9 +lemma
    9.10 +  fixes x :: int
    9.11 +  shows "x ^ 3 = x ^ 3" 
    9.12 +  apply (tactic {* ALLGOALS (CONVERSION
    9.13 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
    9.14 +  by (rule refl)
    9.15  
    9.16 -schematic_lemma "(x - (-2))^5 == ?X::int"
    9.17 -  by sring_norm
    9.18 +lemma
    9.19 +  fixes x :: int
    9.20 +  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))" 
    9.21 +  apply (tactic {* ALLGOALS (CONVERSION
    9.22 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
    9.23 +  by (rule refl)
    9.24  
    9.25 -schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
    9.26 -  by sring_norm
    9.27 +schematic_lemma
    9.28 +  fixes x :: int
    9.29 +  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
    9.30 +  apply (tactic {* ALLGOALS (CONVERSION
    9.31 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
    9.32 +  by (rule refl)
    9.33  
    9.34  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
    9.35    apply (simp only: power_Suc power_0)