1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 03 18:03:29 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 05:07:10 2009 +0100
     1.3 @@ -191,8 +191,7 @@
     1.4  
     1.5  open Conv;
     1.6  
     1.7 -fun numeral_is_const ct =
     1.8 -  can HOLogic.dest_number (Thm.term_of ct);
     1.9 +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
    1.10  
    1.11  fun int_of_rat x =
    1.12    (case Rat.quotient_of_rat x of (i, 1) => i
    1.13 @@ -260,16 +259,22 @@
    1.14  locale gb_field = gb_ring +
    1.15    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.16      and inverse:: "'a \<Rightarrow> 'a"
    1.17 -  assumes divide: "divide x y = mul x (inverse y)"
    1.18 -     and inverse: "inverse x = divide r1 x"
    1.19 +  assumes divide_inverse: "divide x y = mul x (inverse y)"
    1.20 +     and inverse_divide: "inverse x = divide r1 x"
    1.21  begin
    1.22  
    1.23 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
    1.24 +
    1.25 +lemmas field_rules = divide_inverse inverse_divide
    1.26 +
    1.27  lemmas gb_field_axioms' =
    1.28    gb_field_axioms [normalizer
    1.29      semiring ops: semiring_ops
    1.30      semiring rules: semiring_rules
    1.31      ring ops: ring_ops
    1.32 -    ring rules: ring_rules]
    1.33 +    ring rules: ring_rules
    1.34 +    field ops: field_ops
    1.35 +    field rules: field_rules]
    1.36  
    1.37  end
    1.38  
    1.39 @@ -393,6 +398,8 @@
    1.40    semiring rules: semiring_rules
    1.41    ring ops: ring_ops
    1.42    ring rules: ring_rules
    1.43 +  field ops: field_ops
    1.44 +  field rules: field_rules
    1.45    idom rules: noteq_reduce add_scale_eq_noteq
    1.46    ideal rules: subr0_iff add_r0_iff]
    1.47  
    1.48 @@ -636,8 +643,8 @@
    1.49  fun numeral_is_const ct =
    1.50    case term_of ct of
    1.51     Const (@{const_name "HOL.divide"},_) $ a $ b =>
    1.52 -     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
    1.53 - | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
    1.54 +     can HOLogic.dest_number a andalso can HOLogic.dest_number b
    1.55 + | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
    1.56   | t => can HOLogic.dest_number t
    1.57  
    1.58  fun dest_const ct = ((case term_of ct of

     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Fri Apr 03 18:03:29 2009 +0200
     2.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Apr 05 05:07:10 2009 +0100
     2.3 @@ -5,8 +5,8 @@
     2.4  signature GROEBNER =
     2.5  sig
     2.6    val ring_and_ideal_conv :
     2.7 -    {idom: thm list, ring: cterm list * thm list, vars: cterm list,
     2.8 -     semiring: cterm list * thm list, ideal : thm list} ->
     2.9 +    {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
    2.10 +     vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
    2.11      (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
    2.12      conv ->  conv ->
    2.13   {ring_conv : conv, 
    2.14 @@ -581,7 +581,8 @@
    2.15  (** main **)
    2.16  
    2.17  fun ring_and_ideal_conv
    2.18 -  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal}
    2.19 +  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
    2.20 +   field = (f_ops, f_rules), idom, ideal}
    2.21    dest_const mk_const ring_eq_conv ring_normalize_conv =
    2.22  let
    2.23    val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
    2.24 @@ -590,32 +591,37 @@
    2.25  
    2.26    val (ring_sub_tm, ring_neg_tm) =
    2.27      (case r_ops of
    2.28 -      [] => (@{cterm "True"}, @{cterm "True"})
    2.29 -    | [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat));
    2.30 +     [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
    2.31 +    |_  => (@{cterm "True"}, @{cterm "True"}));
    2.32 +
    2.33 +  val (field_div_tm, field_inv_tm) =
    2.34 +    (case f_ops of
    2.35 +       [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
    2.36 +     | _ => (@{cterm "True"}, @{cterm "True"}));
    2.37  
    2.38    val [idom_thm, neq_thm] = idom;
    2.39    val [idl_sub, idl_add0] = 
    2.40       if length ideal = 2 then ideal else [eq_commute, eq_commute]
    2.41 -  val ring_dest_neg =
    2.42 -    fn t => let val (l,r) = dest_comb t in
    2.43 -        if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
    2.44 -      end
    2.45 +  fun ring_dest_neg t =
    2.46 +    let val (l,r) = dest_comb t 
    2.47 +    in if Term.could_unify(term_of l,term_of ring_neg_tm) then r 
    2.48 +       else raise CTERM ("ring_dest_neg", [t])
    2.49 +    end
    2.50  
    2.51   val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
    2.52 -(*
    2.53 - fun ring_dest_inv t =
    2.54 + fun field_dest_inv t =
    2.55      let val (l,r) = dest_comb t in
    2.56 -        if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
    2.57 +        if Term.could_unify(term_of l, term_of field_inv_tm) then r 
    2.58 +        else raise CTERM ("field_dest_inv", [t])
    2.59      end
    2.60 -*)
    2.61   val ring_dest_add = dest_binary ring_add_tm;
    2.62   val ring_mk_add = mk_binop ring_add_tm;
    2.63   val ring_dest_sub = dest_binary ring_sub_tm;
    2.64   val ring_mk_sub = mk_binop ring_sub_tm;
    2.65   val ring_dest_mul = dest_binary ring_mul_tm;
    2.66   val ring_mk_mul = mk_binop ring_mul_tm;
    2.67 -(* val ring_dest_div = dest_binary ring_div_tm;
    2.68 - val ring_mk_div = mk_binop ring_div_tm;*)
    2.69 + val field_dest_div = dest_binary field_div_tm;
    2.70 + val field_mk_div = mk_binop field_div_tm;
    2.71   val ring_dest_pow = dest_binary ring_pow_tm;
    2.72   val ring_mk_pow = mk_binop ring_pow_tm ;
    2.73   fun grobvars tm acc =
    2.74 @@ -625,16 +631,16 @@
    2.75      else if can ring_dest_add tm orelse can ring_dest_sub tm
    2.76              orelse can ring_dest_mul tm
    2.77      then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
    2.78 -(*    else if can ring_dest_inv tm
    2.79 -       then
    2.80 -             let val gvs = grobvars (dest_arg tm) [] in
    2.81 -             if gvs = [] then acc else tm::acc
    2.82 -             end
    2.83 -    else if can ring_dest_div tm then
    2.84 -              let val lvs = grobvars (dest_arg1 tm) acc
    2.85 -                val gvs = grobvars (dest_arg tm) []
    2.86 -              in if gvs = [] then lvs else tm::acc
    2.87 -             end *)
    2.88 +    else if can field_dest_inv tm
    2.89 +         then
    2.90 +          let val gvs = grobvars (dest_arg tm) [] 
    2.91 +          in if null gvs then acc else tm::acc
    2.92 +          end
    2.93 +    else if can field_dest_div tm then
    2.94 +         let val lvs = grobvars (dest_arg1 tm) acc
    2.95 +             val gvs = grobvars (dest_arg tm) []
    2.96 +          in if null gvs then lvs else tm::acc
    2.97 +          end 
    2.98      else tm::acc ;
    2.99  
   2.100  fun grobify_term vars tm =
   2.101 @@ -648,8 +654,8 @@
   2.102    ((grob_neg(grobify_term vars (ring_dest_neg tm)))
   2.103    handle CTERM _ =>
   2.104     (
   2.105 -(*   (grob_inv(grobify_term vars (ring_dest_inv tm)))
   2.106 -   handle CTERM _ => *)
   2.107 +   (grob_inv(grobify_term vars (field_dest_inv tm)))
   2.108 +   handle CTERM _ => 
   2.109      ((let val (l,r) = ring_dest_add tm
   2.110      in grob_add (grobify_term vars l) (grobify_term vars r)
   2.111      end)
   2.112 @@ -662,18 +668,15 @@
   2.113        in grob_mul (grobify_term vars l) (grobify_term vars r)
   2.114        end)
   2.115         handle CTERM _ =>
   2.116 -        (
   2.117 -(*  (let val (l,r) = ring_dest_div tm
   2.118 +        (  (let val (l,r) = field_dest_div tm
   2.119            in grob_div (grobify_term vars l) (grobify_term vars r)
   2.120            end)
   2.121 -         handle CTERM _ => *)
   2.122 +         handle CTERM _ =>
   2.123            ((let val (l,r) = ring_dest_pow tm
   2.124            in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
   2.125            end)
   2.126             handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
   2.127  val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
   2.128 -(*ring_integral |> hd |> concl |> dest_arg
   2.129 -                          |> dest_abs NONE |> snd |> dest_fun |> dest_fun; *)
   2.130  val dest_eq = dest_binary eq_tm;
   2.131  
   2.132  fun grobify_equation vars tm =

     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri Apr 03 18:03:29 2009 +0200
     3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Sun Apr 05 05:07:10 2009 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4   val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
     3.5     (cterm -> cterm -> bool) -> conv
     3.6   val semiring_normalizers_conv :
     3.7 -     cterm list -> cterm list * thm list -> cterm list * thm list ->
     3.8 +     cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
     3.9       (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    3.10         {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    3.11  end
    3.12 @@ -71,7 +71,7 @@
    3.13  
    3.14  
    3.15  (* The main function! *)
    3.16 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
    3.17 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
    3.18    (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
    3.19  let
    3.20  
    3.21 @@ -97,8 +97,7 @@
    3.22  
    3.23  val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
    3.24    (case (r_ops, r_rules) of
    3.25 -    ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
    3.26 -  | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
    3.27 +    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
    3.28        let
    3.29          val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
    3.30          val neg_tm = Thm.dest_fun neg_pat
    3.31 @@ -106,7 +105,18 @@
    3.32          val is_sub = is_binop sub_tm
    3.33        in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
    3.34            sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
    3.35 -      end);
    3.36 +      end
    3.37 +    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
    3.38 +
    3.39 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
    3.40 +  (case (f_ops, f_rules) of 
    3.41 +   ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
    3.42 +     let val div_tm = funpow 2 Thm.dest_fun divide_pat
    3.43 +         val inv_tm = Thm.dest_fun inverse_pat
    3.44 +     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
    3.45 +     end
    3.46 +   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
    3.47 +
    3.48  in fn variable_order =>
    3.49   let
    3.50  
    3.51 @@ -579,6 +589,10 @@
    3.52         let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
    3.53         in transitive th1 (polynomial_neg_conv (concl th1))
    3.54         end
    3.55 +     else if lopr aconvc inverse_tm then
    3.56 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
    3.57 +       in transitive th1 (semiring_mul_conv (concl th1))
    3.58 +       end
    3.59       else
    3.60         if not(is_comb lopr) then reflexive tm
    3.61         else
    3.62 @@ -588,6 +602,14 @@
    3.63                let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
    3.64                in transitive th1 (polynomial_pow_conv (concl th1))
    3.65                end
    3.66 +         else if opr aconvc divide_tm 
    3.67 +            then
    3.68 +              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
    3.69 +                                        (polynomial_conv r)
    3.70 +                  val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) 
    3.71 +                              (Thm.rhs_of th1)
    3.72 +              in transitive th1 th2
    3.73 +              end
    3.74              else
    3.75                if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
    3.76                then
    3.77 @@ -616,7 +638,7 @@
    3.78  
    3.79  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
    3.80  
    3.81 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, 
    3.82 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
    3.83                                       {conv, dest_const, mk_const, is_const}) ord =
    3.84    let
    3.85      val pow_conv =
    3.86 @@ -625,10 +647,10 @@
    3.87          (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
    3.88        then_conv conv ctxt
    3.89      val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
    3.90 -  in semiring_normalizers_conv vars semiring ring dat ord end;
    3.91 +  in semiring_normalizers_conv vars semiring ring field dat ord end;
    3.92  
    3.93 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    3.94 - #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
    3.95 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
    3.96 + #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
    3.97  
    3.98  fun semiring_normalize_wrapper ctxt data = 
    3.99    semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;

     4.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Fri Apr 03 18:03:29 2009 +0200
     4.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Apr 05 05:07:10 2009 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4    val get: Proof.context -> simpset * (thm * entry) list
     4.5    val match: Proof.context -> cterm -> entry option
     4.6    val del: attribute
     4.7 -  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
     4.8 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
     4.9      -> attribute
    4.10    val funs: thm -> {is_const: morphism -> cterm -> bool,
    4.11      dest_const: morphism -> cterm -> Rat.rat,
    4.12 @@ -29,6 +29,7 @@
    4.13   {vars: cterm list,
    4.14    semiring: cterm list * thm list,
    4.15    ring: cterm list * thm list,
    4.16 +  field: cterm list * thm list,
    4.17    idom: thm list,
    4.18    ideal: thm list} *
    4.19   {is_const: cterm -> bool,
    4.20 @@ -57,7 +58,7 @@
    4.21    let
    4.22      fun match_inst
    4.23          ({vars, semiring = (sr_ops, sr_rules), 
    4.24 -          ring = (r_ops, r_rules), idom, ideal},
    4.25 +          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    4.26           fns as {is_const, dest_const, mk_const, conv}) pat =
    4.27         let
    4.28          fun h instT =
    4.29 @@ -68,11 +69,12 @@
    4.30              val vars' = map substT_cterm vars;
    4.31              val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    4.32              val ring' = (map substT_cterm r_ops, map substT r_rules);
    4.33 +            val field' = (map substT_cterm f_ops, map substT f_rules);
    4.34              val idom' = map substT idom;
    4.35              val ideal' = map substT ideal;
    4.36  
    4.37              val result = ({vars = vars', semiring = semiring', 
    4.38 -                           ring = ring', idom = idom', ideal = ideal'}, fns);
    4.39 +                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    4.40            in SOME result end
    4.41        in (case try Thm.match (pat, tm) of
    4.42             NONE => NONE
    4.43 @@ -80,8 +82,8 @@
    4.44        end;
    4.45  
    4.46      fun match_struct (_,
    4.47 -        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
    4.48 -      get_first (match_inst entry) (sr_ops @ r_ops);
    4.49 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
    4.50 +      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
    4.51    in get_first match_struct (snd (get ctxt)) end;
    4.52  
    4.53  
    4.54 @@ -91,6 +93,7 @@
    4.55  val ringN = "ring";
    4.56  val idomN = "idom";
    4.57  val idealN = "ideal";
    4.58 +val fieldN = "field";
    4.59  
    4.60  fun undefined _ = raise Match;
    4.61  
    4.62 @@ -103,7 +106,8 @@
    4.63  val del_ss = Thm.declaration_attribute 
    4.64     (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
    4.65  
    4.66 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} =
    4.67 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
    4.68 +         field = (f_ops, f_rules), idom, ideal} =
    4.69    Thm.declaration_attribute (fn key => fn context => context |> Data.map
    4.70      let
    4.71        val ctxt = Context.proof_of context;
    4.72 @@ -119,11 +123,14 @@
    4.73          check_rules semiringN sr_rules 37 andalso
    4.74          check_ops ringN r_ops 2 andalso
    4.75          check_rules ringN r_rules 2 andalso
    4.76 +        check_ops fieldN f_ops 2 andalso
    4.77 +        check_rules fieldN f_rules 2 andalso
    4.78          check_rules idomN idom 2;
    4.79  
    4.80        val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
    4.81        val sr_rules' = map mk_meta sr_rules;
    4.82        val r_rules' = map mk_meta r_rules;
    4.83 +      val f_rules' = map mk_meta f_rules;
    4.84  
    4.85        fun rule i = nth sr_rules' (i - 1);
    4.86  
    4.87 @@ -140,11 +147,12 @@
    4.88        val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
    4.89        val semiring = (sr_ops, sr_rules');
    4.90        val ring = (r_ops, r_rules');
    4.91 +      val field = (f_ops, f_rules');
    4.92        val ideal' = map (symmetric o mk_meta) ideal
    4.93      in
    4.94        del_data key #>
    4.95        apsnd (cons (key, ({vars = vars, semiring = semiring, 
    4.96 -                          ring = ring, idom = idom, ideal = ideal'},
    4.97 +                          ring = ring, field = field, idom = idom, ideal = ideal'},
    4.98               {is_const = undefined, dest_const = undefined, mk_const = undefined,
    4.99               conv = undefined})))
   4.100      end);
   4.101 @@ -182,6 +190,7 @@
   4.102  val any_keyword =
   4.103    keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   4.104    keyword2 ringN opsN || keyword2 ringN rulesN ||
   4.105 +  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   4.106    keyword2 idomN rulesN || keyword2 idealN rulesN;
   4.107  
   4.108  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   4.109 @@ -198,9 +207,12 @@
   4.110         (keyword2 semiringN rulesN |-- thms)) --
   4.111        (optional (keyword2 ringN opsN |-- terms) --
   4.112         optional (keyword2 ringN rulesN |-- thms)) --
   4.113 +      (optional (keyword2 fieldN opsN |-- terms) --
   4.114 +       optional (keyword2 fieldN rulesN |-- thms)) --
   4.115        optional (keyword2 idomN rulesN |-- thms) --
   4.116        optional (keyword2 idealN rulesN |-- thms)
   4.117 -      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
   4.118 +      >> (fn ((((sr, r), f), id), idl) => 
   4.119 +             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   4.120      "semiring normalizer data";
   4.121  
   4.122  end;