src/HOL/Tools/semiring_normalizer.ML
changeset 36754 5ce217fc769a
parent 36731 08cd7eccb043
parent 36753 5cf4e9128f22
child 36771 3e08b6789e66
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 08 17:15:50 2010 +0200
     1.3 @@ -0,0 +1,907 @@
     1.4 +(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     1.5 +    Author:     Amine Chaieb, TU Muenchen
     1.6 +
     1.7 +Normalization of expressions in semirings.
     1.8 +*)
     1.9 +
    1.10 +signature SEMIRING_NORMALIZER = 
    1.11 +sig
    1.12 +  type entry
    1.13 +  val get: Proof.context -> (thm * entry) list
    1.14 +  val match: Proof.context -> cterm -> entry option
    1.15 +  val del: attribute
    1.16 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
    1.17 +    field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
    1.18 +  val funs: thm -> {is_const: morphism -> cterm -> bool,
    1.19 +    dest_const: morphism -> cterm -> Rat.rat,
    1.20 +    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    1.21 +    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    1.22 +  val semiring_funs: thm -> declaration
    1.23 +  val field_funs: thm -> declaration
    1.24 +
    1.25 +  val semiring_normalize_conv: Proof.context -> conv
    1.26 +  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
    1.27 +  val semiring_normalize_wrapper: Proof.context -> entry -> conv
    1.28 +  val semiring_normalize_ord_wrapper: Proof.context -> entry
    1.29 +    -> (cterm -> cterm -> bool) -> conv
    1.30 +  val semiring_normalizers_conv: cterm list -> cterm list * thm list
    1.31 +    -> cterm list * thm list -> cterm list * thm list ->
    1.32 +      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    1.33 +        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    1.34 +  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    1.35 +    (cterm -> cterm -> bool) ->
    1.36 +      {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    1.37 +
    1.38 +  val setup: theory -> theory
    1.39 +end
    1.40 +
    1.41 +structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
    1.42 +struct
    1.43 +
    1.44 +(** data **)
    1.45 +
    1.46 +type entry =
    1.47 + {vars: cterm list,
    1.48 +  semiring: cterm list * thm list,
    1.49 +  ring: cterm list * thm list,
    1.50 +  field: cterm list * thm list,
    1.51 +  idom: thm list,
    1.52 +  ideal: thm list} *
    1.53 + {is_const: cterm -> bool,
    1.54 +  dest_const: cterm -> Rat.rat,
    1.55 +  mk_const: ctyp -> Rat.rat -> cterm,
    1.56 +  conv: Proof.context -> cterm -> thm};
    1.57 +
    1.58 +structure Data = Generic_Data
    1.59 +(
    1.60 +  type T = (thm * entry) list;
    1.61 +  val empty = [];
    1.62 +  val extend = I;
    1.63 +  val merge = AList.merge Thm.eq_thm (K true);
    1.64 +);
    1.65 +
    1.66 +val get = Data.get o Context.Proof;
    1.67 +
    1.68 +fun match ctxt tm =
    1.69 +  let
    1.70 +    fun match_inst
    1.71 +        ({vars, semiring = (sr_ops, sr_rules), 
    1.72 +          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    1.73 +         fns as {is_const, dest_const, mk_const, conv}) pat =
    1.74 +       let
    1.75 +        fun h instT =
    1.76 +          let
    1.77 +            val substT = Thm.instantiate (instT, []);
    1.78 +            val substT_cterm = Drule.cterm_rule substT;
    1.79 +
    1.80 +            val vars' = map substT_cterm vars;
    1.81 +            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    1.82 +            val ring' = (map substT_cterm r_ops, map substT r_rules);
    1.83 +            val field' = (map substT_cterm f_ops, map substT f_rules);
    1.84 +            val idom' = map substT idom;
    1.85 +            val ideal' = map substT ideal;
    1.86 +
    1.87 +            val result = ({vars = vars', semiring = semiring', 
    1.88 +                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    1.89 +          in SOME result end
    1.90 +      in (case try Thm.match (pat, tm) of
    1.91 +           NONE => NONE
    1.92 +         | SOME (instT, _) => h instT)
    1.93 +      end;
    1.94 +
    1.95 +    fun match_struct (_,
    1.96 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
    1.97 +      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
    1.98 +  in get_first match_struct (get ctxt) end;
    1.99 +
   1.100 +
   1.101 +(* logical content *)
   1.102 +
   1.103 +val semiringN = "semiring";
   1.104 +val ringN = "ring";
   1.105 +val idomN = "idom";
   1.106 +val idealN = "ideal";
   1.107 +val fieldN = "field";
   1.108 +
   1.109 +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
   1.110 +
   1.111 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   1.112 +         field = (f_ops, f_rules), idom, ideal} =
   1.113 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   1.114 +    let
   1.115 +      val ctxt = Context.proof_of context;
   1.116 +
   1.117 +      fun check kind name xs n =
   1.118 +        null xs orelse length xs = n orelse
   1.119 +        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   1.120 +      val check_ops = check "operations";
   1.121 +      val check_rules = check "rules";
   1.122 +
   1.123 +      val _ =
   1.124 +        check_ops semiringN sr_ops 5 andalso
   1.125 +        check_rules semiringN sr_rules 37 andalso
   1.126 +        check_ops ringN r_ops 2 andalso
   1.127 +        check_rules ringN r_rules 2 andalso
   1.128 +        check_ops fieldN f_ops 2 andalso
   1.129 +        check_rules fieldN f_rules 2 andalso
   1.130 +        check_rules idomN idom 2;
   1.131 +
   1.132 +      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   1.133 +      val sr_rules' = map mk_meta sr_rules;
   1.134 +      val r_rules' = map mk_meta r_rules;
   1.135 +      val f_rules' = map mk_meta f_rules;
   1.136 +
   1.137 +      fun rule i = nth sr_rules' (i - 1);
   1.138 +
   1.139 +      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   1.140 +      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   1.141 +      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   1.142 +      val ((clx, crx), (cly, cry)) =
   1.143 +        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   1.144 +      val ((ca, cb), (cc, cd)) =
   1.145 +        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   1.146 +      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   1.147 +      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   1.148 +
   1.149 +      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   1.150 +      val semiring = (sr_ops, sr_rules');
   1.151 +      val ring = (r_ops, r_rules');
   1.152 +      val field = (f_ops, f_rules');
   1.153 +      val ideal' = map (symmetric o mk_meta) ideal
   1.154 +    in
   1.155 +      AList.delete Thm.eq_thm key #>
   1.156 +      cons (key, ({vars = vars, semiring = semiring, 
   1.157 +                          ring = ring, field = field, idom = idom, ideal = ideal'},
   1.158 +             {is_const = undefined, dest_const = undefined, mk_const = undefined,
   1.159 +             conv = undefined}))
   1.160 +    end);
   1.161 +
   1.162 +
   1.163 +(* extra-logical functions *)
   1.164 +
   1.165 +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   1.166 + Data.map (fn data =>
   1.167 +  let
   1.168 +    val key = Morphism.thm phi raw_key;
   1.169 +    val _ = AList.defined Thm.eq_thm data key orelse
   1.170 +      raise THM ("No data entry for structure key", 0, [key]);
   1.171 +    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   1.172 +      mk_const = mk_const phi, conv = conv phi};
   1.173 +  in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
   1.174 +
   1.175 +fun semiring_funs key = funs key
   1.176 +   {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
   1.177 +    dest_const = fn phi => fn ct =>
   1.178 +      Rat.rat_of_int (snd
   1.179 +        (HOLogic.dest_number (Thm.term_of ct)
   1.180 +          handle TERM _ => error "ring_dest_const")),
   1.181 +    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
   1.182 +      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
   1.183 +    conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
   1.184 +      then_conv Simplifier.rewrite (HOL_basic_ss addsimps
   1.185 +        (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
   1.186 +
   1.187 +fun field_funs key =
   1.188 +  let
   1.189 +    fun numeral_is_const ct =
   1.190 +      case term_of ct of
   1.191 +       Const (@{const_name Rings.divide},_) $ a $ b =>
   1.192 +         can HOLogic.dest_number a andalso can HOLogic.dest_number b
   1.193 +     | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   1.194 +     | t => can HOLogic.dest_number t
   1.195 +    fun dest_const ct = ((case term_of ct of
   1.196 +       Const (@{const_name Rings.divide},_) $ a $ b=>
   1.197 +        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   1.198 +     | Const (@{const_name Rings.inverse},_)$t => 
   1.199 +                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   1.200 +     | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   1.201 +       handle TERM _ => error "ring_dest_const")
   1.202 +    fun mk_const phi cT x =
   1.203 +      let val (a, b) = Rat.quotient_of_rat x
   1.204 +      in if b = 1 then Numeral.mk_cnumber cT a
   1.205 +        else Thm.capply
   1.206 +             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   1.207 +                         (Numeral.mk_cnumber cT a))
   1.208 +             (Numeral.mk_cnumber cT b)
   1.209 +      end
   1.210 +  in funs key
   1.211 +     {is_const = K numeral_is_const,
   1.212 +      dest_const = K dest_const,
   1.213 +      mk_const = mk_const,
   1.214 +      conv = K (K Numeral_Simprocs.field_comp_conv)}
   1.215 +  end;
   1.216 +
   1.217 +
   1.218 +
   1.219 +(** auxiliary **)
   1.220 +
   1.221 +fun is_comb ct =
   1.222 +  (case Thm.term_of ct of
   1.223 +    _ $ _ => true
   1.224 +  | _ => false);
   1.225 +
   1.226 +val concl = Thm.cprop_of #> Thm.dest_arg;
   1.227 +
   1.228 +fun is_binop ct ct' =
   1.229 +  (case Thm.term_of ct' of
   1.230 +    c $ _ $ _ => term_of ct aconv c
   1.231 +  | _ => false);
   1.232 +
   1.233 +fun dest_binop ct ct' =
   1.234 +  if is_binop ct ct' then Thm.dest_binop ct'
   1.235 +  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
   1.236 +
   1.237 +fun inst_thm inst = Thm.instantiate ([], inst);
   1.238 +
   1.239 +val dest_numeral = term_of #> HOLogic.dest_number #> snd;
   1.240 +val is_numeral = can dest_numeral;
   1.241 +
   1.242 +val numeral01_conv = Simplifier.rewrite
   1.243 +                         (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
   1.244 +val zero1_numeral_conv = 
   1.245 + Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
   1.246 +fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
   1.247 +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   1.248 +                @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
   1.249 +                @{thm "less_nat_number_of"}];
   1.250 +
   1.251 +val nat_add_conv = 
   1.252 + zerone_conv 
   1.253 +  (Simplifier.rewrite 
   1.254 +    (HOL_basic_ss 
   1.255 +       addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
   1.256 +             @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
   1.257 +                 @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
   1.258 +             @ map (fn th => th RS sym) @{thms numerals}));
   1.259 +
   1.260 +val zeron_tm = @{cterm "0::nat"};
   1.261 +val onen_tm  = @{cterm "1::nat"};
   1.262 +val true_tm = @{cterm "True"};
   1.263 +
   1.264 +
   1.265 +(** normalizing conversions **)
   1.266 +
   1.267 +(* core conversion *)
   1.268 +
   1.269 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
   1.270 +  (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
   1.271 +let
   1.272 +
   1.273 +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
   1.274 +     pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
   1.275 +     pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
   1.276 +     pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
   1.277 +     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
   1.278 +
   1.279 +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
   1.280 +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   1.281 +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
   1.282 +
   1.283 +val dest_add = dest_binop add_tm
   1.284 +val dest_mul = dest_binop mul_tm
   1.285 +fun dest_pow tm =
   1.286 + let val (l,r) = dest_binop pow_tm tm
   1.287 + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   1.288 + end;
   1.289 +val is_add = is_binop add_tm
   1.290 +val is_mul = is_binop mul_tm
   1.291 +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   1.292 +
   1.293 +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   1.294 +  (case (r_ops, r_rules) of
   1.295 +    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   1.296 +      let
   1.297 +        val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   1.298 +        val neg_tm = Thm.dest_fun neg_pat
   1.299 +        val dest_sub = dest_binop sub_tm
   1.300 +        val is_sub = is_binop sub_tm
   1.301 +      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   1.302 +          sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   1.303 +      end
   1.304 +    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
   1.305 +
   1.306 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
   1.307 +  (case (f_ops, f_rules) of 
   1.308 +   ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
   1.309 +     let val div_tm = funpow 2 Thm.dest_fun divide_pat
   1.310 +         val inv_tm = Thm.dest_fun inverse_pat
   1.311 +     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
   1.312 +     end
   1.313 +   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
   1.314 +
   1.315 +in fn variable_order =>
   1.316 + let
   1.317 +
   1.318 +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   1.319 +(* Also deals with "const * const", but both terms must involve powers of    *)
   1.320 +(* the same variable, or both be constants, or behaviour may be incorrect.   *)
   1.321 +
   1.322 + fun powvar_mul_conv tm =
   1.323 +  let
   1.324 +  val (l,r) = dest_mul tm
   1.325 +  in if is_semiring_constant l andalso is_semiring_constant r
   1.326 +     then semiring_mul_conv tm
   1.327 +     else
   1.328 +      ((let
   1.329 +         val (lx,ln) = dest_pow l
   1.330 +        in
   1.331 +         ((let val (rx,rn) = dest_pow r
   1.332 +               val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   1.333 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.334 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   1.335 +           handle CTERM _ =>
   1.336 +            (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   1.337 +                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.338 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   1.339 +       handle CTERM _ =>
   1.340 +           ((let val (rx,rn) = dest_pow r
   1.341 +                val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   1.342 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.343 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   1.344 +           handle CTERM _ => inst_thm [(cx,l)] pthm_32
   1.345 +
   1.346 +))
   1.347 + end;
   1.348 +
   1.349 +(* Remove "1 * m" from a monomial, and just leave m.                         *)
   1.350 +
   1.351 + fun monomial_deone th =
   1.352 +       (let val (l,r) = dest_mul(concl th) in
   1.353 +           if l aconvc one_tm
   1.354 +          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   1.355 +       handle CTERM _ => th;
   1.356 +
   1.357 +(* Conversion for "(monomial)^n", where n is a numeral.                      *)
   1.358 +
   1.359 + val monomial_pow_conv =
   1.360 +  let
   1.361 +   fun monomial_pow tm bod ntm =
   1.362 +    if not(is_comb bod)
   1.363 +    then reflexive tm
   1.364 +    else
   1.365 +     if is_semiring_constant bod
   1.366 +     then semiring_pow_conv tm
   1.367 +     else
   1.368 +      let
   1.369 +      val (lopr,r) = Thm.dest_comb bod
   1.370 +      in if not(is_comb lopr)
   1.371 +         then reflexive tm
   1.372 +        else
   1.373 +          let
   1.374 +          val (opr,l) = Thm.dest_comb lopr
   1.375 +         in
   1.376 +           if opr aconvc pow_tm andalso is_numeral r
   1.377 +          then
   1.378 +            let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   1.379 +                val (l,r) = Thm.dest_comb(concl th1)
   1.380 +           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   1.381 +           end
   1.382 +           else
   1.383 +            if opr aconvc mul_tm
   1.384 +            then
   1.385 +             let
   1.386 +              val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   1.387 +             val (xy,z) = Thm.dest_comb(concl th1)
   1.388 +              val (x,y) = Thm.dest_comb xy
   1.389 +              val thl = monomial_pow y l ntm
   1.390 +              val thr = monomial_pow z r ntm
   1.391 +             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   1.392 +             end
   1.393 +             else reflexive tm
   1.394 +          end
   1.395 +      end
   1.396 +  in fn tm =>
   1.397 +   let
   1.398 +    val (lopr,r) = Thm.dest_comb tm
   1.399 +    val (opr,l) = Thm.dest_comb lopr
   1.400 +   in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   1.401 +      then raise CTERM ("monomial_pow_conv", [tm])
   1.402 +      else if r aconvc zeron_tm
   1.403 +      then inst_thm [(cx,l)] pthm_35
   1.404 +      else if r aconvc onen_tm
   1.405 +      then inst_thm [(cx,l)] pthm_36
   1.406 +      else monomial_deone(monomial_pow tm l r)
   1.407 +   end
   1.408 +  end;
   1.409 +
   1.410 +(* Multiplication of canonical monomials.                                    *)
   1.411 + val monomial_mul_conv =
   1.412 +  let
   1.413 +   fun powvar tm =
   1.414 +    if is_semiring_constant tm then one_tm
   1.415 +    else
   1.416 +     ((let val (lopr,r) = Thm.dest_comb tm
   1.417 +           val (opr,l) = Thm.dest_comb lopr
   1.418 +       in if opr aconvc pow_tm andalso is_numeral r then l 
   1.419 +          else raise CTERM ("monomial_mul_conv",[tm]) end)
   1.420 +     handle CTERM _ => tm)   (* FIXME !? *)
   1.421 +   fun  vorder x y =
   1.422 +    if x aconvc y then 0
   1.423 +    else
   1.424 +     if x aconvc one_tm then ~1
   1.425 +     else if y aconvc one_tm then 1
   1.426 +      else if variable_order x y then ~1 else 1
   1.427 +   fun monomial_mul tm l r =
   1.428 +    ((let val (lx,ly) = dest_mul l val vl = powvar lx
   1.429 +      in
   1.430 +      ((let
   1.431 +        val (rx,ry) = dest_mul r
   1.432 +         val vr = powvar rx
   1.433 +         val ord = vorder vl vr
   1.434 +        in
   1.435 +         if ord = 0
   1.436 +        then
   1.437 +          let
   1.438 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   1.439 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.440 +             val (tm3,tm4) = Thm.dest_comb tm1
   1.441 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   1.442 +             val th3 = transitive th1 th2
   1.443 +              val  (tm5,tm6) = Thm.dest_comb(concl th3)
   1.444 +              val  (tm7,tm8) = Thm.dest_comb tm6
   1.445 +             val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   1.446 +         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   1.447 +         end
   1.448 +         else
   1.449 +          let val th0 = if ord < 0 then pthm_16 else pthm_17
   1.450 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   1.451 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.452 +             val (tm3,tm4) = Thm.dest_comb tm2
   1.453 +         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.454 +         end
   1.455 +        end)
   1.456 +       handle CTERM _ =>
   1.457 +        (let val vr = powvar r val ord = vorder vl vr
   1.458 +        in
   1.459 +          if ord = 0 then
   1.460 +           let
   1.461 +           val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   1.462 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.463 +           val (tm3,tm4) = Thm.dest_comb tm1
   1.464 +           val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   1.465 +          in transitive th1 th2
   1.466 +          end
   1.467 +          else
   1.468 +          if ord < 0 then
   1.469 +            let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   1.470 +                val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.471 +                val (tm3,tm4) = Thm.dest_comb tm2
   1.472 +           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.473 +           end
   1.474 +           else inst_thm [(ca,l),(cb,r)] pthm_09
   1.475 +        end)) end)
   1.476 +     handle CTERM _ =>
   1.477 +      (let val vl = powvar l in
   1.478 +        ((let
   1.479 +          val (rx,ry) = dest_mul r
   1.480 +          val vr = powvar rx
   1.481 +           val ord = vorder vl vr
   1.482 +         in if ord = 0 then
   1.483 +              let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   1.484 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.485 +                 val (tm3,tm4) = Thm.dest_comb tm1
   1.486 +             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   1.487 +             end
   1.488 +             else if ord > 0 then
   1.489 +                 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   1.490 +                     val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.491 +                    val (tm3,tm4) = Thm.dest_comb tm2
   1.492 +                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.493 +                end
   1.494 +             else reflexive tm
   1.495 +         end)
   1.496 +        handle CTERM _ =>
   1.497 +          (let val vr = powvar r
   1.498 +               val  ord = vorder vl vr
   1.499 +          in if ord = 0 then powvar_mul_conv tm
   1.500 +              else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   1.501 +              else reflexive tm
   1.502 +          end)) end))
   1.503 +  in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   1.504 +             end
   1.505 +  end;
   1.506 +(* Multiplication by monomial of a polynomial.                               *)
   1.507 +
   1.508 + val polynomial_monomial_mul_conv =
   1.509 +  let
   1.510 +   fun pmm_conv tm =
   1.511 +    let val (l,r) = dest_mul tm
   1.512 +    in
   1.513 +    ((let val (y,z) = dest_add r
   1.514 +          val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   1.515 +          val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.516 +          val (tm3,tm4) = Thm.dest_comb tm1
   1.517 +          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   1.518 +      in transitive th1 th2
   1.519 +      end)
   1.520 +     handle CTERM _ => monomial_mul_conv tm)
   1.521 +   end
   1.522 + in pmm_conv
   1.523 + end;
   1.524 +
   1.525 +(* Addition of two monomials identical except for constant multiples.        *)
   1.526 +
   1.527 +fun monomial_add_conv tm =
   1.528 + let val (l,r) = dest_add tm
   1.529 + in if is_semiring_constant l andalso is_semiring_constant r
   1.530 +    then semiring_add_conv tm
   1.531 +    else
   1.532 +     let val th1 =
   1.533 +           if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   1.534 +           then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   1.535 +                    inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   1.536 +                else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   1.537 +           else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   1.538 +           then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   1.539 +           else inst_thm [(cm,r)] pthm_05
   1.540 +         val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.541 +         val (tm3,tm4) = Thm.dest_comb tm1
   1.542 +         val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   1.543 +         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   1.544 +         val tm5 = concl th3
   1.545 +      in
   1.546 +      if (Thm.dest_arg1 tm5) aconvc zero_tm
   1.547 +      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   1.548 +      else monomial_deone th3
   1.549 +     end
   1.550 + end;
   1.551 +
   1.552 +(* Ordering on monomials.                                                    *)
   1.553 +
   1.554 +fun striplist dest =
   1.555 + let fun strip x acc =
   1.556 +   ((let val (l,r) = dest x in
   1.557 +        strip l (strip r acc) end)
   1.558 +    handle CTERM _ => x::acc)    (* FIXME !? *)
   1.559 + in fn x => strip x []
   1.560 + end;
   1.561 +
   1.562 +
   1.563 +fun powervars tm =
   1.564 + let val ptms = striplist dest_mul tm
   1.565 + in if is_semiring_constant (hd ptms) then tl ptms else ptms
   1.566 + end;
   1.567 +val num_0 = 0;
   1.568 +val num_1 = 1;
   1.569 +fun dest_varpow tm =
   1.570 + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   1.571 +   handle CTERM _ =>
   1.572 +   (tm,(if is_semiring_constant tm then num_0 else num_1)));
   1.573 +
   1.574 +val morder =
   1.575 + let fun lexorder l1 l2 =
   1.576 +  case (l1,l2) of
   1.577 +    ([],[]) => 0
   1.578 +  | (vps,[]) => ~1
   1.579 +  | ([],vps) => 1
   1.580 +  | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   1.581 +     if variable_order x1 x2 then 1
   1.582 +     else if variable_order x2 x1 then ~1
   1.583 +     else if n1 < n2 then ~1
   1.584 +     else if n2 < n1 then 1
   1.585 +     else lexorder vs1 vs2
   1.586 + in fn tm1 => fn tm2 =>
   1.587 +  let val vdegs1 = map dest_varpow (powervars tm1)
   1.588 +      val vdegs2 = map dest_varpow (powervars tm2)
   1.589 +      val deg1 = fold (Integer.add o snd) vdegs1 num_0
   1.590 +      val deg2 = fold (Integer.add o snd) vdegs2 num_0
   1.591 +  in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   1.592 +                            else lexorder vdegs1 vdegs2
   1.593 +  end
   1.594 + end;
   1.595 +
   1.596 +(* Addition of two polynomials.                                              *)
   1.597 +
   1.598 +val polynomial_add_conv =
   1.599 + let
   1.600 + fun dezero_rule th =
   1.601 +  let
   1.602 +   val tm = concl th
   1.603 +  in
   1.604 +   if not(is_add tm) then th else
   1.605 +   let val (lopr,r) = Thm.dest_comb tm
   1.606 +       val l = Thm.dest_arg lopr
   1.607 +   in
   1.608 +    if l aconvc zero_tm
   1.609 +    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   1.610 +        if r aconvc zero_tm
   1.611 +        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   1.612 +   end
   1.613 +  end
   1.614 + fun padd tm =
   1.615 +  let
   1.616 +   val (l,r) = dest_add tm
   1.617 +  in
   1.618 +   if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   1.619 +   else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   1.620 +   else
   1.621 +    if is_add l
   1.622 +    then
   1.623 +     let val (a,b) = dest_add l
   1.624 +     in
   1.625 +     if is_add r then
   1.626 +      let val (c,d) = dest_add r
   1.627 +          val ord = morder a c
   1.628 +      in
   1.629 +       if ord = 0 then
   1.630 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   1.631 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.632 +            val (tm3,tm4) = Thm.dest_comb tm1
   1.633 +            val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   1.634 +        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   1.635 +        end
   1.636 +       else (* ord <> 0*)
   1.637 +        let val th1 =
   1.638 +                if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.639 +                else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.640 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.641 +        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.642 +        end
   1.643 +      end
   1.644 +     else (* not (is_add r)*)
   1.645 +      let val ord = morder a r
   1.646 +      in
   1.647 +       if ord = 0 then
   1.648 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   1.649 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.650 +            val (tm3,tm4) = Thm.dest_comb tm1
   1.651 +            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.652 +        in dezero_rule (transitive th1 th2)
   1.653 +        end
   1.654 +       else (* ord <> 0*)
   1.655 +        if ord > 0 then
   1.656 +          let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.657 +              val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.658 +          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.659 +          end
   1.660 +        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.661 +      end
   1.662 +    end
   1.663 +   else (* not (is_add l)*)
   1.664 +    if is_add r then
   1.665 +      let val (c,d) = dest_add r
   1.666 +          val  ord = morder l c
   1.667 +      in
   1.668 +       if ord = 0 then
   1.669 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   1.670 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.671 +             val (tm3,tm4) = Thm.dest_comb tm1
   1.672 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.673 +         in dezero_rule (transitive th1 th2)
   1.674 +         end
   1.675 +       else
   1.676 +        if ord > 0 then reflexive tm
   1.677 +        else
   1.678 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.679 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.680 +         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.681 +         end
   1.682 +      end
   1.683 +    else
   1.684 +     let val ord = morder l r
   1.685 +     in
   1.686 +      if ord = 0 then monomial_add_conv tm
   1.687 +      else if ord > 0 then dezero_rule(reflexive tm)
   1.688 +      else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.689 +     end
   1.690 +  end
   1.691 + in padd
   1.692 + end;
   1.693 +
   1.694 +(* Multiplication of two polynomials.                                        *)
   1.695 +
   1.696 +val polynomial_mul_conv =
   1.697 + let
   1.698 +  fun pmul tm =
   1.699 +   let val (l,r) = dest_mul tm
   1.700 +   in
   1.701 +    if not(is_add l) then polynomial_monomial_mul_conv tm
   1.702 +    else
   1.703 +     if not(is_add r) then
   1.704 +      let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   1.705 +      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   1.706 +      end
   1.707 +     else
   1.708 +       let val (a,b) = dest_add l
   1.709 +           val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   1.710 +           val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.711 +           val (tm3,tm4) = Thm.dest_comb tm1
   1.712 +           val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   1.713 +           val th3 = transitive th1 (combination th2 (pmul tm2))
   1.714 +       in transitive th3 (polynomial_add_conv (concl th3))
   1.715 +       end
   1.716 +   end
   1.717 + in fn tm =>
   1.718 +   let val (l,r) = dest_mul tm
   1.719 +   in
   1.720 +    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   1.721 +    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   1.722 +    else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   1.723 +    else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   1.724 +    else pmul tm
   1.725 +   end
   1.726 + end;
   1.727 +
   1.728 +(* Power of polynomial (optimized for the monomial and trivial cases).       *)
   1.729 +
   1.730 +fun num_conv n =
   1.731 +  nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   1.732 +  |> Thm.symmetric;
   1.733 +
   1.734 +
   1.735 +val polynomial_pow_conv =
   1.736 + let
   1.737 +  fun ppow tm =
   1.738 +    let val (l,n) = dest_pow tm
   1.739 +    in
   1.740 +     if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   1.741 +     else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   1.742 +     else
   1.743 +         let val th1 = num_conv n
   1.744 +             val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   1.745 +             val (tm1,tm2) = Thm.dest_comb(concl th2)
   1.746 +             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   1.747 +             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   1.748 +         in transitive th4 (polynomial_mul_conv (concl th4))
   1.749 +         end
   1.750 +    end
   1.751 + in fn tm =>
   1.752 +       if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   1.753 + end;
   1.754 +
   1.755 +(* Negation.                                                                 *)
   1.756 +
   1.757 +fun polynomial_neg_conv tm =
   1.758 +   let val (l,r) = Thm.dest_comb tm in
   1.759 +        if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   1.760 +        let val th1 = inst_thm [(cx',r)] neg_mul
   1.761 +            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   1.762 +        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   1.763 +        end
   1.764 +   end;
   1.765 +
   1.766 +
   1.767 +(* Subtraction.                                                              *)
   1.768 +fun polynomial_sub_conv tm =
   1.769 +  let val (l,r) = dest_sub tm
   1.770 +      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   1.771 +      val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.772 +      val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   1.773 +  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   1.774 +  end;
   1.775 +
   1.776 +(* Conversion from HOL term.                                                 *)
   1.777 +
   1.778 +fun polynomial_conv tm =
   1.779 + if is_semiring_constant tm then semiring_add_conv tm
   1.780 + else if not(is_comb tm) then reflexive tm
   1.781 + else
   1.782 +  let val (lopr,r) = Thm.dest_comb tm
   1.783 +  in if lopr aconvc neg_tm then
   1.784 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   1.785 +       in transitive th1 (polynomial_neg_conv (concl th1))
   1.786 +       end
   1.787 +     else if lopr aconvc inverse_tm then
   1.788 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   1.789 +       in transitive th1 (semiring_mul_conv (concl th1))
   1.790 +       end
   1.791 +     else
   1.792 +       if not(is_comb lopr) then reflexive tm
   1.793 +       else
   1.794 +         let val (opr,l) = Thm.dest_comb lopr
   1.795 +         in if opr aconvc pow_tm andalso is_numeral r
   1.796 +            then
   1.797 +              let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   1.798 +              in transitive th1 (polynomial_pow_conv (concl th1))
   1.799 +              end
   1.800 +         else if opr aconvc divide_tm 
   1.801 +            then
   1.802 +              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   1.803 +                                        (polynomial_conv r)
   1.804 +                  val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
   1.805 +                              (Thm.rhs_of th1)
   1.806 +              in transitive th1 th2
   1.807 +              end
   1.808 +            else
   1.809 +              if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   1.810 +              then
   1.811 +               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   1.812 +                   val f = if opr aconvc add_tm then polynomial_add_conv
   1.813 +                      else if opr aconvc mul_tm then polynomial_mul_conv
   1.814 +                      else polynomial_sub_conv
   1.815 +               in transitive th1 (f (concl th1))
   1.816 +               end
   1.817 +              else reflexive tm
   1.818 +         end
   1.819 +  end;
   1.820 + in
   1.821 +   {main = polynomial_conv,
   1.822 +    add = polynomial_add_conv,
   1.823 +    mul = polynomial_mul_conv,
   1.824 +    pow = polynomial_pow_conv,
   1.825 +    neg = polynomial_neg_conv,
   1.826 +    sub = polynomial_sub_conv}
   1.827 + end
   1.828 +end;
   1.829 +
   1.830 +val nat_exp_ss =
   1.831 +  HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
   1.832 +    addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
   1.833 +
   1.834 +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
   1.835 +
   1.836 +
   1.837 +(* various normalizing conversions *)
   1.838 +
   1.839 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   1.840 +                                     {conv, dest_const, mk_const, is_const}) ord =
   1.841 +  let
   1.842 +    val pow_conv =
   1.843 +      Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
   1.844 +      then_conv Simplifier.rewrite
   1.845 +        (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   1.846 +      then_conv conv ctxt
   1.847 +    val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
   1.848 +  in semiring_normalizers_conv vars semiring ring field dat ord end;
   1.849 +
   1.850 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
   1.851 + #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);
   1.852 +
   1.853 +fun semiring_normalize_wrapper ctxt data = 
   1.854 +  semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   1.855 +
   1.856 +fun semiring_normalize_ord_conv ctxt ord tm =
   1.857 +  (case match ctxt tm of
   1.858 +    NONE => reflexive tm
   1.859 +  | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   1.860 + 
   1.861 +fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   1.862 +
   1.863 +
   1.864 +(** Isar setup **)
   1.865 +
   1.866 +local
   1.867 +
   1.868 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   1.869 +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   1.870 +fun keyword3 k1 k2 k3 =
   1.871 +  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   1.872 +
   1.873 +val opsN = "ops";
   1.874 +val rulesN = "rules";
   1.875 +
   1.876 +val normN = "norm";
   1.877 +val constN = "const";
   1.878 +val delN = "del";
   1.879 +
   1.880 +val any_keyword =
   1.881 +  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   1.882 +  keyword2 ringN opsN || keyword2 ringN rulesN ||
   1.883 +  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   1.884 +  keyword2 idomN rulesN || keyword2 idealN rulesN;
   1.885 +
   1.886 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   1.887 +val terms = thms >> map Drule.dest_term;
   1.888 +
   1.889 +fun optional scan = Scan.optional scan [];
   1.890 +
   1.891 +in
   1.892 +
   1.893 +val setup =
   1.894 +  Attrib.setup @{binding normalizer}
   1.895 +    (Scan.lift (Args.$$$ delN >> K del) ||
   1.896 +      ((keyword2 semiringN opsN |-- terms) --
   1.897 +       (keyword2 semiringN rulesN |-- thms)) --
   1.898 +      (optional (keyword2 ringN opsN |-- terms) --
   1.899 +       optional (keyword2 ringN rulesN |-- thms)) --
   1.900 +      (optional (keyword2 fieldN opsN |-- terms) --
   1.901 +       optional (keyword2 fieldN rulesN |-- thms)) --
   1.902 +      optional (keyword2 idomN rulesN |-- thms) --
   1.903 +      optional (keyword2 idealN rulesN |-- thms)
   1.904 +      >> (fn ((((sr, r), f), id), idl) => 
   1.905 +             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   1.906 +    "semiring normalizer data";
   1.907 +
   1.908 +end;
   1.909 +
   1.910 +end;