src/HOL/Tools/Groebner_Basis/normalizer_data.ML

 sig
   type entry
   val get: Proof.context -> simpset * (thm * entry) list
   val match: Proof.context -> cterm -> entry option
   val del: attribute
-  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list}
+  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
     -> attribute
   val funs: thm -> {is_const: morphism -> cterm -> bool,
     dest_const: morphism -> cterm -> Rat.rat,
     mk_const: morphism -> ctyp -> Rat.rat -> cterm,
     conv: morphism -> Proof.context -> cterm -> thm} -> declaration

 
 type entry =
  {vars: cterm list,
   semiring: cterm list * thm list,
   ring: cterm list * thm list,
+  field: cterm list * thm list,
   idom: thm list,
   ideal: thm list} *
  {is_const: cterm -> bool,
   dest_const: cterm -> Rat.rat,
   mk_const: ctyp -> Rat.rat -> cterm,

 
 fun match ctxt tm =
   let
     fun match_inst
         ({vars, semiring = (sr_ops, sr_rules), 
-          ring = (r_ops, r_rules), idom, ideal},
+          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
          fns as {is_const, dest_const, mk_const, conv}) pat =
        let
         fun h instT =
           let
             val substT = Thm.instantiate (instT, []);
             val substT_cterm = Drule.cterm_rule substT;
 
             val vars' = map substT_cterm vars;
             val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
             val ring' = (map substT_cterm r_ops, map substT r_rules);
+            val field' = (map substT_cterm f_ops, map substT f_rules);
             val idom' = map substT idom;
             val ideal' = map substT ideal;
 
             val result = ({vars = vars', semiring = semiring', 
-                           ring = ring', idom = idom', ideal = ideal'}, fns);
+                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
           in SOME result end
       in (case try Thm.match (pat, tm) of
            NONE => NONE
          | SOME (instT, _) => h instT)
       end;
 
     fun match_struct (_,
-        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
-      get_first (match_inst entry) (sr_ops @ r_ops);
+        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
+      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
   in get_first match_struct (snd (get ctxt)) end;
 
 
 (* logical content *)
 
 val semiringN = "semiring";
 val ringN = "ring";
 val idomN = "idom";
 val idealN = "ideal";
+val fieldN = "field";
 
 fun undefined _ = raise Match;
 
 fun del_data key = apsnd (remove eq_data (key, []));
 

    (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), idom, ideal} =
+fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
+         field = (f_ops, f_rules), idom, ideal} =
   Thm.declaration_attribute (fn key => fn context => context |> Data.map
     let
       val ctxt = Context.proof_of context;
 
       fun check kind name xs n =

       val _ =
         check_ops semiringN sr_ops 5 andalso
         check_rules semiringN sr_rules 37 andalso
         check_ops ringN r_ops 2 andalso
         check_rules ringN r_rules 2 andalso
+        check_ops fieldN f_ops 2 andalso
+        check_rules fieldN f_rules 2 andalso
         check_rules idomN idom 2;
 
       val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
       val sr_rules' = map mk_meta sr_rules;
       val r_rules' = map mk_meta r_rules;
+      val f_rules' = map mk_meta f_rules;
 
       fun rule i = nth sr_rules' (i - 1);
 
       val (cx, cy) = Thm.dest_binop (hd sr_ops);
       val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;

       val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
 
       val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
       val semiring = (sr_ops, sr_rules');
       val ring = (r_ops, r_rules');
+      val field = (f_ops, f_rules');
       val ideal' = map (symmetric o mk_meta) ideal
     in
       del_data key #>
       apsnd (cons (key, ({vars = vars, semiring = semiring, 
-                          ring = ring, idom = idom, ideal = ideal'},
+                          ring = ring, field = field, idom = idom, ideal = ideal'},
              {is_const = undefined, dest_const = undefined, mk_const = undefined,
              conv = undefined})))
     end);
 
 

 val delN = "del";
 
 val any_keyword =
   keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   keyword2 ringN opsN || keyword2 ringN rulesN ||
+  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   keyword2 idomN rulesN || keyword2 idealN rulesN;
 
 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
 val terms = thms >> map Drule.dest_term;
 

     (Scan.lift (Args.$$$ delN >> K del) ||
       ((keyword2 semiringN opsN |-- terms) --
        (keyword2 semiringN rulesN |-- thms)) --
       (optional (keyword2 ringN opsN |-- terms) --
        optional (keyword2 ringN rulesN |-- thms)) --
+      (optional (keyword2 fieldN opsN |-- terms) --
+       optional (keyword2 fieldN rulesN |-- thms)) --
       optional (keyword2 idomN rulesN |-- thms) --
       optional (keyword2 idealN rulesN |-- thms)
-      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+      >> (fn ((((sr, r), f), id), idl) => 
+             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
     "semiring normalizer data";
 
 end;