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