src/HOL/Tools/Groebner_Basis/normalizer.ML
author wenzelm
Mon Oct 19 21:54:57 2009 +0200 (2009-10-19)
changeset 33002 f3f02f36a3e2
parent 31790 05c92381363c
child 35064 1bdef0c013d3
permissions -rw-r--r--
uniform use of Integer.add/mult/sum/prod;
     1 (*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 signature NORMALIZER = 
     6 sig
     7  val semiring_normalize_conv : Proof.context -> conv
     8  val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
     9  val semiring_normalize_tac : Proof.context -> int -> tactic
    10  val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> conv
    11  val semiring_normalizers_ord_wrapper :  
    12      Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) ->
    13       {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    14  val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
    15    (cterm -> cterm -> bool) -> conv
    16  val semiring_normalizers_conv :
    17      cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
    18      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    19        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    20 end
    21 
    22 structure Normalizer: NORMALIZER = 
    23 struct
    24 
    25 open Conv;
    26 
    27 (* Very basic stuff for terms *)
    28 
    29 fun is_comb ct =
    30   (case Thm.term_of ct of
    31     _ $ _ => true
    32   | _ => false);
    33 
    34 val concl = Thm.cprop_of #> Thm.dest_arg;
    35 
    36 fun is_binop ct ct' =
    37   (case Thm.term_of ct' of
    38     c $ _ $ _ => term_of ct aconv c
    39   | _ => false);
    40 
    41 fun dest_binop ct ct' =
    42   if is_binop ct ct' then Thm.dest_binop ct'
    43   else raise CTERM ("dest_binop: bad binop", [ct, ct'])
    44 
    45 fun inst_thm inst = Thm.instantiate ([], inst);
    46 
    47 val dest_numeral = term_of #> HOLogic.dest_number #> snd;
    48 val is_numeral = can dest_numeral;
    49 
    50 val numeral01_conv = Simplifier.rewrite
    51                          (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
    52 val zero1_numeral_conv = 
    53  Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
    54 fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
    55 val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
    56                 @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
    57                 @{thm "less_nat_number_of"}];
    58 val nat_add_conv = 
    59  zerone_conv 
    60   (Simplifier.rewrite 
    61     (HOL_basic_ss 
    62        addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
    63              @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
    64                  @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
    65              @ map (fn th => th RS sym) @{thms numerals}));
    66 
    67 val nat_mul_conv = nat_add_conv;
    68 val zeron_tm = @{cterm "0::nat"};
    69 val onen_tm  = @{cterm "1::nat"};
    70 val true_tm = @{cterm "True"};
    71 
    72 
    73 (* The main function! *)
    74 fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
    75   (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
    76 let
    77 
    78 val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
    79      pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
    80      pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
    81      pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
    82      pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
    83 
    84 val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
    85 val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
    86 val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
    87 
    88 val dest_add = dest_binop add_tm
    89 val dest_mul = dest_binop mul_tm
    90 fun dest_pow tm =
    91  let val (l,r) = dest_binop pow_tm tm
    92  in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
    93  end;
    94 val is_add = is_binop add_tm
    95 val is_mul = is_binop mul_tm
    96 fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
    97 
    98 val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
    99   (case (r_ops, r_rules) of
   100     ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   101       let
   102         val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   103         val neg_tm = Thm.dest_fun neg_pat
   104         val dest_sub = dest_binop sub_tm
   105         val is_sub = is_binop sub_tm
   106       in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   107           sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   108       end
   109     | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
   110 
   111 val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
   112   (case (f_ops, f_rules) of 
   113    ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
   114      let val div_tm = funpow 2 Thm.dest_fun divide_pat
   115          val inv_tm = Thm.dest_fun inverse_pat
   116      in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
   117      end
   118    | _ => (TrueI, TrueI, true_tm, true_tm, K false));
   119 
   120 in fn variable_order =>
   121  let
   122 
   123 (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   124 (* Also deals with "const * const", but both terms must involve powers of    *)
   125 (* the same variable, or both be constants, or behaviour may be incorrect.   *)
   126 
   127  fun powvar_mul_conv tm =
   128   let
   129   val (l,r) = dest_mul tm
   130   in if is_semiring_constant l andalso is_semiring_constant r
   131      then semiring_mul_conv tm
   132      else
   133       ((let
   134          val (lx,ln) = dest_pow l
   135         in
   136          ((let val (rx,rn) = dest_pow r
   137                val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   138                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   139                transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   140            handle CTERM _ =>
   141             (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   142                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
   143                transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   144        handle CTERM _ =>
   145            ((let val (rx,rn) = dest_pow r
   146                 val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   147                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   148                transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   149            handle CTERM _ => inst_thm [(cx,l)] pthm_32
   150 
   151 ))
   152  end;
   153 
   154 (* Remove "1 * m" from a monomial, and just leave m.                         *)
   155 
   156  fun monomial_deone th =
   157        (let val (l,r) = dest_mul(concl th) in
   158            if l aconvc one_tm
   159           then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   160        handle CTERM _ => th;
   161 
   162 (* Conversion for "(monomial)^n", where n is a numeral.                      *)
   163 
   164  val monomial_pow_conv =
   165   let
   166    fun monomial_pow tm bod ntm =
   167     if not(is_comb bod)
   168     then reflexive tm
   169     else
   170      if is_semiring_constant bod
   171      then semiring_pow_conv tm
   172      else
   173       let
   174       val (lopr,r) = Thm.dest_comb bod
   175       in if not(is_comb lopr)
   176          then reflexive tm
   177         else
   178           let
   179           val (opr,l) = Thm.dest_comb lopr
   180          in
   181            if opr aconvc pow_tm andalso is_numeral r
   182           then
   183             let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   184                 val (l,r) = Thm.dest_comb(concl th1)
   185            in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
   186            end
   187            else
   188             if opr aconvc mul_tm
   189             then
   190              let
   191               val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   192              val (xy,z) = Thm.dest_comb(concl th1)
   193               val (x,y) = Thm.dest_comb xy
   194               val thl = monomial_pow y l ntm
   195               val thr = monomial_pow z r ntm
   196              in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   197              end
   198              else reflexive tm
   199           end
   200       end
   201   in fn tm =>
   202    let
   203     val (lopr,r) = Thm.dest_comb tm
   204     val (opr,l) = Thm.dest_comb lopr
   205    in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   206       then raise CTERM ("monomial_pow_conv", [tm])
   207       else if r aconvc zeron_tm
   208       then inst_thm [(cx,l)] pthm_35
   209       else if r aconvc onen_tm
   210       then inst_thm [(cx,l)] pthm_36
   211       else monomial_deone(monomial_pow tm l r)
   212    end
   213   end;
   214 
   215 (* Multiplication of canonical monomials.                                    *)
   216  val monomial_mul_conv =
   217   let
   218    fun powvar tm =
   219     if is_semiring_constant tm then one_tm
   220     else
   221      ((let val (lopr,r) = Thm.dest_comb tm
   222            val (opr,l) = Thm.dest_comb lopr
   223        in if opr aconvc pow_tm andalso is_numeral r then l 
   224           else raise CTERM ("monomial_mul_conv",[tm]) end)
   225      handle CTERM _ => tm)   (* FIXME !? *)
   226    fun  vorder x y =
   227     if x aconvc y then 0
   228     else
   229      if x aconvc one_tm then ~1
   230      else if y aconvc one_tm then 1
   231       else if variable_order x y then ~1 else 1
   232    fun monomial_mul tm l r =
   233     ((let val (lx,ly) = dest_mul l val vl = powvar lx
   234       in
   235       ((let
   236         val (rx,ry) = dest_mul r
   237          val vr = powvar rx
   238          val ord = vorder vl vr
   239         in
   240          if ord = 0
   241         then
   242           let
   243              val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   244              val (tm1,tm2) = Thm.dest_comb(concl th1)
   245              val (tm3,tm4) = Thm.dest_comb tm1
   246              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   247              val th3 = transitive th1 th2
   248               val  (tm5,tm6) = Thm.dest_comb(concl th3)
   249               val  (tm7,tm8) = Thm.dest_comb tm6
   250              val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   251          in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   252          end
   253          else
   254           let val th0 = if ord < 0 then pthm_16 else pthm_17
   255              val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   256              val (tm1,tm2) = Thm.dest_comb(concl th1)
   257              val (tm3,tm4) = Thm.dest_comb tm2
   258          in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   259          end
   260         end)
   261        handle CTERM _ =>
   262         (let val vr = powvar r val ord = vorder vl vr
   263         in
   264           if ord = 0 then
   265            let
   266            val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   267                  val (tm1,tm2) = Thm.dest_comb(concl th1)
   268            val (tm3,tm4) = Thm.dest_comb tm1
   269            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   270           in transitive th1 th2
   271           end
   272           else
   273           if ord < 0 then
   274             let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   275                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   276                 val (tm3,tm4) = Thm.dest_comb tm2
   277            in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   278            end
   279            else inst_thm [(ca,l),(cb,r)] pthm_09
   280         end)) end)
   281      handle CTERM _ =>
   282       (let val vl = powvar l in
   283         ((let
   284           val (rx,ry) = dest_mul r
   285           val vr = powvar rx
   286            val ord = vorder vl vr
   287          in if ord = 0 then
   288               let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   289                  val (tm1,tm2) = Thm.dest_comb(concl th1)
   290                  val (tm3,tm4) = Thm.dest_comb tm1
   291              in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   292              end
   293              else if ord > 0 then
   294                  let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   295                      val (tm1,tm2) = Thm.dest_comb(concl th1)
   296                     val (tm3,tm4) = Thm.dest_comb tm2
   297                 in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   298                 end
   299              else reflexive tm
   300          end)
   301         handle CTERM _ =>
   302           (let val vr = powvar r
   303                val  ord = vorder vl vr
   304           in if ord = 0 then powvar_mul_conv tm
   305               else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   306               else reflexive tm
   307           end)) end))
   308   in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   309              end
   310   end;
   311 (* Multiplication by monomial of a polynomial.                               *)
   312 
   313  val polynomial_monomial_mul_conv =
   314   let
   315    fun pmm_conv tm =
   316     let val (l,r) = dest_mul tm
   317     in
   318     ((let val (y,z) = dest_add r
   319           val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   320           val (tm1,tm2) = Thm.dest_comb(concl th1)
   321           val (tm3,tm4) = Thm.dest_comb tm1
   322           val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   323       in transitive th1 th2
   324       end)
   325      handle CTERM _ => monomial_mul_conv tm)
   326    end
   327  in pmm_conv
   328  end;
   329 
   330 (* Addition of two monomials identical except for constant multiples.        *)
   331 
   332 fun monomial_add_conv tm =
   333  let val (l,r) = dest_add tm
   334  in if is_semiring_constant l andalso is_semiring_constant r
   335     then semiring_add_conv tm
   336     else
   337      let val th1 =
   338            if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   339            then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   340                     inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   341                 else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   342            else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   343            then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   344            else inst_thm [(cm,r)] pthm_05
   345          val (tm1,tm2) = Thm.dest_comb(concl th1)
   346          val (tm3,tm4) = Thm.dest_comb tm1
   347          val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   348          val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   349          val tm5 = concl th3
   350       in
   351       if (Thm.dest_arg1 tm5) aconvc zero_tm
   352       then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   353       else monomial_deone th3
   354      end
   355  end;
   356 
   357 (* Ordering on monomials.                                                    *)
   358 
   359 fun striplist dest =
   360  let fun strip x acc =
   361    ((let val (l,r) = dest x in
   362         strip l (strip r acc) end)
   363     handle CTERM _ => x::acc)    (* FIXME !? *)
   364  in fn x => strip x []
   365  end;
   366 
   367 
   368 fun powervars tm =
   369  let val ptms = striplist dest_mul tm
   370  in if is_semiring_constant (hd ptms) then tl ptms else ptms
   371  end;
   372 val num_0 = 0;
   373 val num_1 = 1;
   374 fun dest_varpow tm =
   375  ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   376    handle CTERM _ =>
   377    (tm,(if is_semiring_constant tm then num_0 else num_1)));
   378 
   379 val morder =
   380  let fun lexorder l1 l2 =
   381   case (l1,l2) of
   382     ([],[]) => 0
   383   | (vps,[]) => ~1
   384   | ([],vps) => 1
   385   | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   386      if variable_order x1 x2 then 1
   387      else if variable_order x2 x1 then ~1
   388      else if n1 < n2 then ~1
   389      else if n2 < n1 then 1
   390      else lexorder vs1 vs2
   391  in fn tm1 => fn tm2 =>
   392   let val vdegs1 = map dest_varpow (powervars tm1)
   393       val vdegs2 = map dest_varpow (powervars tm2)
   394       val deg1 = fold (Integer.add o snd) vdegs1 num_0
   395       val deg2 = fold (Integer.add o snd) vdegs2 num_0
   396   in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   397                             else lexorder vdegs1 vdegs2
   398   end
   399  end;
   400 
   401 (* Addition of two polynomials.                                              *)
   402 
   403 val polynomial_add_conv =
   404  let
   405  fun dezero_rule th =
   406   let
   407    val tm = concl th
   408   in
   409    if not(is_add tm) then th else
   410    let val (lopr,r) = Thm.dest_comb tm
   411        val l = Thm.dest_arg lopr
   412    in
   413     if l aconvc zero_tm
   414     then transitive th (inst_thm [(ca,r)] pthm_07)   else
   415         if r aconvc zero_tm
   416         then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   417    end
   418   end
   419  fun padd tm =
   420   let
   421    val (l,r) = dest_add tm
   422   in
   423    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   424    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   425    else
   426     if is_add l
   427     then
   428      let val (a,b) = dest_add l
   429      in
   430      if is_add r then
   431       let val (c,d) = dest_add r
   432           val ord = morder a c
   433       in
   434        if ord = 0 then
   435         let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   436             val (tm1,tm2) = Thm.dest_comb(concl th1)
   437             val (tm3,tm4) = Thm.dest_comb tm1
   438             val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   439         in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   440         end
   441        else (* ord <> 0*)
   442         let val th1 =
   443                 if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   444                 else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   445             val (tm1,tm2) = Thm.dest_comb(concl th1)
   446         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   447         end
   448       end
   449      else (* not (is_add r)*)
   450       let val ord = morder a r
   451       in
   452        if ord = 0 then
   453         let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   454             val (tm1,tm2) = Thm.dest_comb(concl th1)
   455             val (tm3,tm4) = Thm.dest_comb tm1
   456             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   457         in dezero_rule (transitive th1 th2)
   458         end
   459        else (* ord <> 0*)
   460         if ord > 0 then
   461           let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   462               val (tm1,tm2) = Thm.dest_comb(concl th1)
   463           in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   464           end
   465         else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   466       end
   467     end
   468    else (* not (is_add l)*)
   469     if is_add r then
   470       let val (c,d) = dest_add r
   471           val  ord = morder l c
   472       in
   473        if ord = 0 then
   474          let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   475              val (tm1,tm2) = Thm.dest_comb(concl th1)
   476              val (tm3,tm4) = Thm.dest_comb tm1
   477              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   478          in dezero_rule (transitive th1 th2)
   479          end
   480        else
   481         if ord > 0 then reflexive tm
   482         else
   483          let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   484              val (tm1,tm2) = Thm.dest_comb(concl th1)
   485          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   486          end
   487       end
   488     else
   489      let val ord = morder l r
   490      in
   491       if ord = 0 then monomial_add_conv tm
   492       else if ord > 0 then dezero_rule(reflexive tm)
   493       else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   494      end
   495   end
   496  in padd
   497  end;
   498 
   499 (* Multiplication of two polynomials.                                        *)
   500 
   501 val polynomial_mul_conv =
   502  let
   503   fun pmul tm =
   504    let val (l,r) = dest_mul tm
   505    in
   506     if not(is_add l) then polynomial_monomial_mul_conv tm
   507     else
   508      if not(is_add r) then
   509       let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   510       in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   511       end
   512      else
   513        let val (a,b) = dest_add l
   514            val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   515            val (tm1,tm2) = Thm.dest_comb(concl th1)
   516            val (tm3,tm4) = Thm.dest_comb tm1
   517            val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   518            val th3 = transitive th1 (combination th2 (pmul tm2))
   519        in transitive th3 (polynomial_add_conv (concl th3))
   520        end
   521    end
   522  in fn tm =>
   523    let val (l,r) = dest_mul tm
   524    in
   525     if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   526     else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   527     else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   528     else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   529     else pmul tm
   530    end
   531  end;
   532 
   533 (* Power of polynomial (optimized for the monomial and trivial cases).       *)
   534 
   535 fun num_conv n =
   536   nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   537   |> Thm.symmetric;
   538 
   539 
   540 val polynomial_pow_conv =
   541  let
   542   fun ppow tm =
   543     let val (l,n) = dest_pow tm
   544     in
   545      if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   546      else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   547      else
   548          let val th1 = num_conv n
   549              val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   550              val (tm1,tm2) = Thm.dest_comb(concl th2)
   551              val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   552              val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   553          in transitive th4 (polynomial_mul_conv (concl th4))
   554          end
   555     end
   556  in fn tm =>
   557        if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   558  end;
   559 
   560 (* Negation.                                                                 *)
   561 
   562 fun polynomial_neg_conv tm =
   563    let val (l,r) = Thm.dest_comb tm in
   564         if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   565         let val th1 = inst_thm [(cx',r)] neg_mul
   566             val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
   567         in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   568         end
   569    end;
   570 
   571 
   572 (* Subtraction.                                                              *)
   573 fun polynomial_sub_conv tm =
   574   let val (l,r) = dest_sub tm
   575       val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   576       val (tm1,tm2) = Thm.dest_comb(concl th1)
   577       val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   578   in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   579   end;
   580 
   581 (* Conversion from HOL term.                                                 *)
   582 
   583 fun polynomial_conv tm =
   584  if is_semiring_constant tm then semiring_add_conv tm
   585  else if not(is_comb tm) then reflexive tm
   586  else
   587   let val (lopr,r) = Thm.dest_comb tm
   588   in if lopr aconvc neg_tm then
   589        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   590        in transitive th1 (polynomial_neg_conv (concl th1))
   591        end
   592      else if lopr aconvc inverse_tm then
   593        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   594        in transitive th1 (semiring_mul_conv (concl th1))
   595        end
   596      else
   597        if not(is_comb lopr) then reflexive tm
   598        else
   599          let val (opr,l) = Thm.dest_comb lopr
   600          in if opr aconvc pow_tm andalso is_numeral r
   601             then
   602               let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   603               in transitive th1 (polynomial_pow_conv (concl th1))
   604               end
   605          else if opr aconvc divide_tm 
   606             then
   607               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   608                                         (polynomial_conv r)
   609                   val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) 
   610                               (Thm.rhs_of th1)
   611               in transitive th1 th2
   612               end
   613             else
   614               if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   615               then
   616                let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   617                    val f = if opr aconvc add_tm then polynomial_add_conv
   618                       else if opr aconvc mul_tm then polynomial_mul_conv
   619                       else polynomial_sub_conv
   620                in transitive th1 (f (concl th1))
   621                end
   622               else reflexive tm
   623          end
   624   end;
   625  in
   626    {main = polynomial_conv,
   627     add = polynomial_add_conv,
   628     mul = polynomial_mul_conv,
   629     pow = polynomial_pow_conv,
   630     neg = polynomial_neg_conv,
   631     sub = polynomial_sub_conv}
   632  end
   633 end;
   634 
   635 val nat_arith = @{thms "nat_arith"};
   636 val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
   637                               addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
   638 
   639 fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
   640 
   641 fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   642                                      {conv, dest_const, mk_const, is_const}) ord =
   643   let
   644     val pow_conv =
   645       arg_conv (Simplifier.rewrite nat_exp_ss)
   646       then_conv Simplifier.rewrite
   647         (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   648       then_conv conv ctxt
   649     val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
   650   in semiring_normalizers_conv vars semiring ring field dat ord end;
   651 
   652 fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
   653  #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);
   654 
   655 fun semiring_normalize_wrapper ctxt data = 
   656   semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   657 
   658 fun semiring_normalize_ord_conv ctxt ord tm =
   659   (case NormalizerData.match ctxt tm of
   660     NONE => reflexive tm
   661   | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   662  
   663 
   664 fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   665 
   666 fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
   667   rtac (semiring_normalize_conv ctxt
   668     (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
   669 end;