src/HOL/Tools/Groebner_Basis/normalizer.ML
changeset 23252 67268bb40b21
child 23259 ccee01b8d1c5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 16:26:04 2007 +0200
     1.3 @@ -0,0 +1,649 @@
     1.4 +(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +signature NORMALIZER = 
    1.10 +sig
    1.11 + val mk_cnumber : ctyp -> int -> cterm
    1.12 + val mk_cnumeral : int -> cterm
    1.13 + val semiring_normalize_conv : Proof.context -> Conv.conv
    1.14 + val semiring_normalize_tac : Proof.context -> int -> tactic
    1.15 + val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
    1.16 + val semiring_normalizers_conv :
    1.17 +     cterm list -> cterm list * thm list -> cterm list * thm list ->
    1.18 +     (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) ->
    1.19 +       {add: Conv.conv, mul: Conv.conv, neg: Conv.conv, main: Conv.conv, 
    1.20 +        pow: Conv.conv, sub: Conv.conv}
    1.21 +end
    1.22 +
    1.23 +structure Normalizer: NORMALIZER = 
    1.24 +struct
    1.25 +open Misc;
    1.26 +
    1.27 +local
    1.28 + val pls_const = @{cterm "Numeral.Pls"}
    1.29 +   and min_const = @{cterm "Numeral.Min"}
    1.30 +   and bit_const = @{cterm "Numeral.Bit"}
    1.31 +   and zero = @{cpat "0"}
    1.32 +   and one = @{cpat "1"}
    1.33 + fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
    1.34 +  | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
    1.35 +  | mk_cbit _ = raise CTERM ("mk_cbit", []);
    1.36 +
    1.37 +in
    1.38 +
    1.39 +fun mk_cnumeral 0 = pls_const
    1.40 +  | mk_cnumeral ~1 = min_const
    1.41 +  | mk_cnumeral i =
    1.42 +      let val (q, r) = IntInf.divMod (i, 2)
    1.43 +      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r)) 
    1.44 +      end;
    1.45 +
    1.46 +fun mk_cnumber cT = 
    1.47 + let 
    1.48 +  val [nb_of, z, on] = 
    1.49 +    map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one]
    1.50 +  fun h 0 = z
    1.51 +    | h 1 = on
    1.52 +    | h x = Thm.capply nb_of (mk_cnumeral x)
    1.53 + in h end;
    1.54 +end;
    1.55 +
    1.56 +
    1.57 +(* Very basic stuff for terms *)
    1.58 +val dest_numeral = term_of #> HOLogic.dest_number #> snd;
    1.59 +val is_numeral = can dest_numeral;
    1.60 +
    1.61 +val numeral01_conv = Simplifier.rewrite
    1.62 +                         (HOL_basic_ss addsimps [numeral_1_eq_1, numeral_0_eq_0]);
    1.63 +val zero1_numeral_conv = 
    1.64 + Simplifier.rewrite (HOL_basic_ss addsimps [numeral_1_eq_1 RS sym, numeral_0_eq_0 RS sym]);
    1.65 +val zerone_conv = fn cv => zero1_numeral_conv then_conv cv then_conv numeral01_conv;
    1.66 +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
    1.67 +                @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
    1.68 +                @{thm "less_nat_number_of"}];
    1.69 +val nat_add_conv = 
    1.70 + zerone_conv 
    1.71 +  (Simplifier.rewrite 
    1.72 +    (HOL_basic_ss 
    1.73 +       addsimps arith_simps @ natarith @ rel_simps
    1.74 +             @ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1]
    1.75 +             @ map (fn th => th RS sym) numerals));
    1.76 +
    1.77 +val nat_mul_conv = nat_add_conv;
    1.78 +val zeron_tm = @{cterm "0::nat"};
    1.79 +val onen_tm  = @{cterm "1::nat"};
    1.80 +val true_tm = @{cterm "True"};
    1.81 +
    1.82 +
    1.83 +(* The main function! *)
    1.84 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules)
    1.85 +  (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
    1.86 +let
    1.87 +
    1.88 +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
    1.89 +     pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
    1.90 +     pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
    1.91 +     pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
    1.92 +     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
    1.93 +
    1.94 +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
    1.95 +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
    1.96 +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
    1.97 +
    1.98 +val dest_add = dest_binop add_tm
    1.99 +val dest_mul = dest_binop mul_tm
   1.100 +fun dest_pow tm =
   1.101 + let val (l,r) = dest_binop pow_tm tm
   1.102 + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   1.103 + end;
   1.104 +val is_add = is_binop add_tm
   1.105 +val is_mul = is_binop mul_tm
   1.106 +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   1.107 +
   1.108 +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   1.109 +  (case (r_ops, r_rules) of
   1.110 +    ([], []) => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)
   1.111 +  | ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   1.112 +      let
   1.113 +        val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   1.114 +        val neg_tm = Thm.dest_fun neg_pat
   1.115 +        val dest_sub = dest_binop sub_tm
   1.116 +        val is_sub = is_binop sub_tm
   1.117 +      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   1.118 +          sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   1.119 +      end);
   1.120 +in fn variable_order =>
   1.121 + let
   1.122 +
   1.123 +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   1.124 +(* Also deals with "const * const", but both terms must involve powers of    *)
   1.125 +(* the same variable, or both be constants, or behaviour may be incorrect.   *)
   1.126 +
   1.127 + fun powvar_mul_conv tm =
   1.128 +  let
   1.129 +  val (l,r) = dest_mul tm
   1.130 +  in if is_semiring_constant l andalso is_semiring_constant r
   1.131 +     then semiring_mul_conv tm
   1.132 +     else
   1.133 +      ((let
   1.134 +         val (lx,ln) = dest_pow l
   1.135 +        in
   1.136 +         ((let val (rx,rn) = dest_pow r
   1.137 +               val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   1.138 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.139 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   1.140 +           handle CTERM _ =>
   1.141 +            (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   1.142 +                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.143 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   1.144 +       handle CTERM _ =>
   1.145 +           ((let val (rx,rn) = dest_pow r
   1.146 +                val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   1.147 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   1.148 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   1.149 +           handle CTERM _ => inst_thm [(cx,l)] pthm_32
   1.150 +
   1.151 +))
   1.152 + end;
   1.153 +
   1.154 +(* Remove "1 * m" from a monomial, and just leave m.                         *)
   1.155 +
   1.156 + fun monomial_deone th =
   1.157 +       (let val (l,r) = dest_mul(concl th) in
   1.158 +           if l aconvc one_tm
   1.159 +          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   1.160 +       handle CTERM _ => th;
   1.161 +
   1.162 +(* Conversion for "(monomial)^n", where n is a numeral.                      *)
   1.163 +
   1.164 + val monomial_pow_conv =
   1.165 +  let
   1.166 +   fun monomial_pow tm bod ntm =
   1.167 +    if not(is_comb bod)
   1.168 +    then reflexive tm
   1.169 +    else
   1.170 +     if is_semiring_constant bod
   1.171 +     then semiring_pow_conv tm
   1.172 +     else
   1.173 +      let
   1.174 +      val (lopr,r) = Thm.dest_comb bod
   1.175 +      in if not(is_comb lopr)
   1.176 +         then reflexive tm
   1.177 +        else
   1.178 +          let
   1.179 +          val (opr,l) = Thm.dest_comb lopr
   1.180 +         in
   1.181 +           if opr aconvc pow_tm andalso is_numeral r
   1.182 +          then
   1.183 +            let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   1.184 +                val (l,r) = Thm.dest_comb(concl th1)
   1.185 +           in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
   1.186 +           end
   1.187 +           else
   1.188 +            if opr aconvc mul_tm
   1.189 +            then
   1.190 +             let
   1.191 +              val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   1.192 +             val (xy,z) = Thm.dest_comb(concl th1)
   1.193 +              val (x,y) = Thm.dest_comb xy
   1.194 +              val thl = monomial_pow y l ntm
   1.195 +              val thr = monomial_pow z r ntm
   1.196 +             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   1.197 +             end
   1.198 +             else reflexive tm
   1.199 +          end
   1.200 +      end
   1.201 +  in fn tm =>
   1.202 +   let
   1.203 +    val (lopr,r) = Thm.dest_comb tm
   1.204 +    val (opr,l) = Thm.dest_comb lopr
   1.205 +   in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   1.206 +      then raise CTERM ("monomial_pow_conv", [tm])
   1.207 +      else if r aconvc zeron_tm
   1.208 +      then inst_thm [(cx,l)] pthm_35
   1.209 +      else if r aconvc onen_tm
   1.210 +      then inst_thm [(cx,l)] pthm_36
   1.211 +      else monomial_deone(monomial_pow tm l r)
   1.212 +   end
   1.213 +  end;
   1.214 +
   1.215 +(* Multiplication of canonical monomials.                                    *)
   1.216 + val monomial_mul_conv =
   1.217 +  let
   1.218 +   fun powvar tm =
   1.219 +    if is_semiring_constant tm then one_tm
   1.220 +    else
   1.221 +     ((let val (lopr,r) = Thm.dest_comb tm
   1.222 +           val (opr,l) = Thm.dest_comb lopr
   1.223 +       in if opr aconvc pow_tm andalso is_numeral r then l 
   1.224 +          else raise CTERM ("monomial_mul_conv",[tm]) end)
   1.225 +     handle CTERM _ => tm)   (* FIXME !? *)
   1.226 +   fun  vorder x y =
   1.227 +    if x aconvc y then 0
   1.228 +    else
   1.229 +     if x aconvc one_tm then ~1
   1.230 +     else if y aconvc one_tm then 1
   1.231 +      else if variable_order x y then ~1 else 1
   1.232 +   fun monomial_mul tm l r =
   1.233 +    ((let val (lx,ly) = dest_mul l val vl = powvar lx
   1.234 +      in
   1.235 +      ((let
   1.236 +        val (rx,ry) = dest_mul r
   1.237 +         val vr = powvar rx
   1.238 +         val ord = vorder vl vr
   1.239 +        in
   1.240 +         if ord = 0
   1.241 +        then
   1.242 +          let
   1.243 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   1.244 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.245 +             val (tm3,tm4) = Thm.dest_comb tm1
   1.246 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   1.247 +             val th3 = transitive th1 th2
   1.248 +              val  (tm5,tm6) = Thm.dest_comb(concl th3)
   1.249 +              val  (tm7,tm8) = Thm.dest_comb tm6
   1.250 +             val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   1.251 +         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   1.252 +         end
   1.253 +         else
   1.254 +          let val th0 = if ord < 0 then pthm_16 else pthm_17
   1.255 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   1.256 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.257 +             val (tm3,tm4) = Thm.dest_comb tm2
   1.258 +         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.259 +         end
   1.260 +        end)
   1.261 +       handle CTERM _ =>
   1.262 +        (let val vr = powvar r val ord = vorder vl vr
   1.263 +        in
   1.264 +          if ord = 0 then
   1.265 +           let
   1.266 +           val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   1.267 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.268 +           val (tm3,tm4) = Thm.dest_comb tm1
   1.269 +           val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   1.270 +          in transitive th1 th2
   1.271 +          end
   1.272 +          else
   1.273 +          if ord < 0 then
   1.274 +            let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   1.275 +                val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.276 +                val (tm3,tm4) = Thm.dest_comb tm2
   1.277 +           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.278 +           end
   1.279 +           else inst_thm [(ca,l),(cb,r)] pthm_09
   1.280 +        end)) end)
   1.281 +     handle CTERM _ =>
   1.282 +      (let val vl = powvar l in
   1.283 +        ((let
   1.284 +          val (rx,ry) = dest_mul r
   1.285 +          val vr = powvar rx
   1.286 +           val ord = vorder vl vr
   1.287 +         in if ord = 0 then
   1.288 +              let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   1.289 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.290 +                 val (tm3,tm4) = Thm.dest_comb tm1
   1.291 +             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   1.292 +             end
   1.293 +             else if ord > 0 then
   1.294 +                 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   1.295 +                     val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.296 +                    val (tm3,tm4) = Thm.dest_comb tm2
   1.297 +                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   1.298 +                end
   1.299 +             else reflexive tm
   1.300 +         end)
   1.301 +        handle CTERM _ =>
   1.302 +          (let val vr = powvar r
   1.303 +               val  ord = vorder vl vr
   1.304 +          in if ord = 0 then powvar_mul_conv tm
   1.305 +              else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   1.306 +              else reflexive tm
   1.307 +          end)) end))
   1.308 +  in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   1.309 +             end
   1.310 +  end;
   1.311 +(* Multiplication by monomial of a polynomial.                               *)
   1.312 +
   1.313 + val polynomial_monomial_mul_conv =
   1.314 +  let
   1.315 +   fun pmm_conv tm =
   1.316 +    let val (l,r) = dest_mul tm
   1.317 +    in
   1.318 +    ((let val (y,z) = dest_add r
   1.319 +          val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   1.320 +          val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.321 +          val (tm3,tm4) = Thm.dest_comb tm1
   1.322 +          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   1.323 +      in transitive th1 th2
   1.324 +      end)
   1.325 +     handle CTERM _ => monomial_mul_conv tm)
   1.326 +   end
   1.327 + in pmm_conv
   1.328 + end;
   1.329 +
   1.330 +(* Addition of two monomials identical except for constant multiples.        *)
   1.331 +
   1.332 +fun monomial_add_conv tm =
   1.333 + let val (l,r) = dest_add tm
   1.334 + in if is_semiring_constant l andalso is_semiring_constant r
   1.335 +    then semiring_add_conv tm
   1.336 +    else
   1.337 +     let val th1 =
   1.338 +           if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   1.339 +           then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   1.340 +                    inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   1.341 +                else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   1.342 +           else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   1.343 +           then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   1.344 +           else inst_thm [(cm,r)] pthm_05
   1.345 +         val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.346 +         val (tm3,tm4) = Thm.dest_comb tm1
   1.347 +         val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   1.348 +         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   1.349 +         val tm5 = concl th3
   1.350 +      in
   1.351 +      if (Thm.dest_arg1 tm5) aconvc zero_tm
   1.352 +      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   1.353 +      else monomial_deone th3
   1.354 +     end
   1.355 + end;
   1.356 +
   1.357 +(* Ordering on monomials.                                                    *)
   1.358 +
   1.359 +fun striplist dest =
   1.360 + let fun strip x acc =
   1.361 +   ((let val (l,r) = dest x in
   1.362 +        strip l (strip r acc) end)
   1.363 +    handle CTERM _ => x::acc)    (* FIXME !? *)
   1.364 + in fn x => strip x []
   1.365 + end;
   1.366 +
   1.367 +
   1.368 +fun powervars tm =
   1.369 + let val ptms = striplist dest_mul tm
   1.370 + in if is_semiring_constant (hd ptms) then tl ptms else ptms
   1.371 + end;
   1.372 +val num_0 = 0;
   1.373 +val num_1 = 1;
   1.374 +fun dest_varpow tm =
   1.375 + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   1.376 +   handle CTERM _ =>
   1.377 +   (tm,(if is_semiring_constant tm then num_0 else num_1)));
   1.378 +
   1.379 +val morder =
   1.380 + let fun lexorder l1 l2 =
   1.381 +  case (l1,l2) of
   1.382 +    ([],[]) => 0
   1.383 +  | (vps,[]) => ~1
   1.384 +  | ([],vps) => 1
   1.385 +  | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   1.386 +     if variable_order x1 x2 then 1
   1.387 +     else if variable_order x2 x1 then ~1
   1.388 +     else if n1 < n2 then ~1
   1.389 +     else if n2 < n1 then 1
   1.390 +     else lexorder vs1 vs2
   1.391 + in fn tm1 => fn tm2 =>
   1.392 +  let val vdegs1 = map dest_varpow (powervars tm1)
   1.393 +      val vdegs2 = map dest_varpow (powervars tm2)
   1.394 +      val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
   1.395 +      val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
   1.396 +  in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   1.397 +                            else lexorder vdegs1 vdegs2
   1.398 +  end
   1.399 + end;
   1.400 +
   1.401 +(* Addition of two polynomials.                                              *)
   1.402 +
   1.403 +val polynomial_add_conv =
   1.404 + let
   1.405 + fun dezero_rule th =
   1.406 +  let
   1.407 +   val tm = concl th
   1.408 +  in
   1.409 +   if not(is_add tm) then th else
   1.410 +   let val (lopr,r) = Thm.dest_comb tm
   1.411 +       val l = Thm.dest_arg lopr
   1.412 +   in
   1.413 +    if l aconvc zero_tm
   1.414 +    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   1.415 +        if r aconvc zero_tm
   1.416 +        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   1.417 +   end
   1.418 +  end
   1.419 + fun padd tm =
   1.420 +  let
   1.421 +   val (l,r) = dest_add tm
   1.422 +  in
   1.423 +   if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   1.424 +   else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   1.425 +   else
   1.426 +    if is_add l
   1.427 +    then
   1.428 +     let val (a,b) = dest_add l
   1.429 +     in
   1.430 +     if is_add r then
   1.431 +      let val (c,d) = dest_add r
   1.432 +          val ord = morder a c
   1.433 +      in
   1.434 +       if ord = 0 then
   1.435 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   1.436 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.437 +            val (tm3,tm4) = Thm.dest_comb tm1
   1.438 +            val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   1.439 +        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   1.440 +        end
   1.441 +       else (* ord <> 0*)
   1.442 +        let val th1 =
   1.443 +                if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.444 +                else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.445 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.446 +        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.447 +        end
   1.448 +      end
   1.449 +     else (* not (is_add r)*)
   1.450 +      let val ord = morder a r
   1.451 +      in
   1.452 +       if ord = 0 then
   1.453 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   1.454 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.455 +            val (tm3,tm4) = Thm.dest_comb tm1
   1.456 +            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.457 +        in dezero_rule (transitive th1 th2)
   1.458 +        end
   1.459 +       else (* ord <> 0*)
   1.460 +        if ord > 0 then
   1.461 +          let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   1.462 +              val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.463 +          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.464 +          end
   1.465 +        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.466 +      end
   1.467 +    end
   1.468 +   else (* not (is_add l)*)
   1.469 +    if is_add r then
   1.470 +      let val (c,d) = dest_add r
   1.471 +          val  ord = morder l c
   1.472 +      in
   1.473 +       if ord = 0 then
   1.474 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   1.475 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.476 +             val (tm3,tm4) = Thm.dest_comb tm1
   1.477 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   1.478 +         in dezero_rule (transitive th1 th2)
   1.479 +         end
   1.480 +       else
   1.481 +        if ord > 0 then reflexive tm
   1.482 +        else
   1.483 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   1.484 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.485 +         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   1.486 +         end
   1.487 +      end
   1.488 +    else
   1.489 +     let val ord = morder l r
   1.490 +     in
   1.491 +      if ord = 0 then monomial_add_conv tm
   1.492 +      else if ord > 0 then dezero_rule(reflexive tm)
   1.493 +      else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   1.494 +     end
   1.495 +  end
   1.496 + in padd
   1.497 + end;
   1.498 +
   1.499 +(* Multiplication of two polynomials.                                        *)
   1.500 +
   1.501 +val polynomial_mul_conv =
   1.502 + let
   1.503 +  fun pmul tm =
   1.504 +   let val (l,r) = dest_mul tm
   1.505 +   in
   1.506 +    if not(is_add l) then polynomial_monomial_mul_conv tm
   1.507 +    else
   1.508 +     if not(is_add r) then
   1.509 +      let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   1.510 +      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   1.511 +      end
   1.512 +     else
   1.513 +       let val (a,b) = dest_add l
   1.514 +           val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   1.515 +           val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.516 +           val (tm3,tm4) = Thm.dest_comb tm1
   1.517 +           val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   1.518 +           val th3 = transitive th1 (combination th2 (pmul tm2))
   1.519 +       in transitive th3 (polynomial_add_conv (concl th3))
   1.520 +       end
   1.521 +   end
   1.522 + in fn tm =>
   1.523 +   let val (l,r) = dest_mul tm
   1.524 +   in
   1.525 +    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   1.526 +    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   1.527 +    else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   1.528 +    else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   1.529 +    else pmul tm
   1.530 +   end
   1.531 + end;
   1.532 +
   1.533 +(* Power of polynomial (optimized for the monomial and trivial cases).       *)
   1.534 +
   1.535 +val Succ = @{cterm "Suc"};
   1.536 +val num_conv = fn n =>
   1.537 +        nat_add_conv (Thm.capply (Succ) (mk_cnumber @{ctyp "nat"} ((dest_numeral n) - 1)))
   1.538 +                     |> Thm.symmetric;
   1.539 +
   1.540 +
   1.541 +val polynomial_pow_conv =
   1.542 + let
   1.543 +  fun ppow tm =
   1.544 +    let val (l,n) = dest_pow tm
   1.545 +    in
   1.546 +     if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   1.547 +     else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   1.548 +     else
   1.549 +         let val th1 = num_conv n
   1.550 +             val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   1.551 +             val (tm1,tm2) = Thm.dest_comb(concl th2)
   1.552 +             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   1.553 +             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   1.554 +         in transitive th4 (polynomial_mul_conv (concl th4))
   1.555 +         end
   1.556 +    end
   1.557 + in fn tm =>
   1.558 +       if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   1.559 + end;
   1.560 +
   1.561 +(* Negation.                                                                 *)
   1.562 +
   1.563 +val polynomial_neg_conv =
   1.564 + fn tm =>
   1.565 +   let val (l,r) = Thm.dest_comb tm in
   1.566 +        if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   1.567 +        let val th1 = inst_thm [(cx',r)] neg_mul
   1.568 +            val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
   1.569 +        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   1.570 +        end
   1.571 +   end;
   1.572 +
   1.573 +
   1.574 +(* Subtraction.                                                              *)
   1.575 +val polynomial_sub_conv = fn tm =>
   1.576 +  let val (l,r) = dest_sub tm
   1.577 +      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   1.578 +      val (tm1,tm2) = Thm.dest_comb(concl th1)
   1.579 +      val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   1.580 +  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   1.581 +  end;
   1.582 +
   1.583 +(* Conversion from HOL term.                                                 *)
   1.584 +
   1.585 +fun polynomial_conv tm =
   1.586 + if not(is_comb tm) orelse is_semiring_constant tm
   1.587 + then reflexive tm
   1.588 + else
   1.589 +  let val (lopr,r) = Thm.dest_comb tm
   1.590 +  in if lopr aconvc neg_tm then
   1.591 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   1.592 +       in transitive th1 (polynomial_neg_conv (concl th1))
   1.593 +       end
   1.594 +     else
   1.595 +       if not(is_comb lopr) then reflexive tm
   1.596 +       else
   1.597 +         let val (opr,l) = Thm.dest_comb lopr
   1.598 +         in if opr aconvc pow_tm andalso is_numeral r
   1.599 +            then
   1.600 +              let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   1.601 +              in transitive th1 (polynomial_pow_conv (concl th1))
   1.602 +              end
   1.603 +            else
   1.604 +              if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   1.605 +              then
   1.606 +               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   1.607 +                   val f = if opr aconvc add_tm then polynomial_add_conv
   1.608 +                      else if opr aconvc mul_tm then polynomial_mul_conv
   1.609 +                      else polynomial_sub_conv
   1.610 +               in transitive th1 (f (concl th1))
   1.611 +               end
   1.612 +              else reflexive tm
   1.613 +         end
   1.614 +  end;
   1.615 + in
   1.616 +   {main = polynomial_conv,
   1.617 +    add = polynomial_add_conv,
   1.618 +    mul = polynomial_mul_conv,
   1.619 +    pow = polynomial_pow_conv,
   1.620 +    neg = polynomial_neg_conv,
   1.621 +    sub = polynomial_sub_conv}
   1.622 + end
   1.623 +end;
   1.624 +
   1.625 +val nat_arith = @{thms "nat_arith"};
   1.626 +val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
   1.627 +                              addsimps [Let_def, if_False, if_True, add_0, add_Suc];
   1.628 +
   1.629 +fun semiring_normalize_wrapper ({vars, semiring, ring, idom}, 
   1.630 +                                     {conv, dest_const, mk_const, is_const}) =
   1.631 +  let
   1.632 +    fun ord t u = Term.term_ord (term_of t, term_of u) = LESS
   1.633 +
   1.634 +    val pow_conv =
   1.635 +      arg_conv (Simplifier.rewrite nat_exp_ss)
   1.636 +      then_conv Simplifier.rewrite
   1.637 +        (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   1.638 +      then_conv conv
   1.639 +    val dat = (is_const, conv, conv, pow_conv)
   1.640 +    val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
   1.641 +  in main end;
   1.642 +
   1.643 +fun semiring_normalize_conv ctxt tm =
   1.644 +  (case NormalizerData.match ctxt tm of
   1.645 +    NONE => reflexive tm
   1.646 +  | SOME res => semiring_normalize_wrapper res tm);
   1.647 +
   1.648 +
   1.649 +fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
   1.650 +  rtac (semiring_normalize_conv ctxt
   1.651 +    (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
   1.652 +end;