src/HOL/Tools/semiring_normalizer.ML
author wenzelm
Sat May 15 21:50:05 2010 +0200 (2010-05-15)
changeset 36945 9bec62c10714
parent 36771 3e08b6789e66
child 37744 3daaf23b9ab4
permissions -rw-r--r--
less pervasive names from structure Thm;
     1 (*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Normalization of expressions in semirings.
     5 *)
     6 
     7 signature SEMIRING_NORMALIZER = 
     8 sig
     9   type entry
    10   val get: Proof.context -> (thm * entry) list
    11   val match: Proof.context -> cterm -> entry option
    12   val del: attribute
    13   val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
    14     field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
    15   val funs: thm -> {is_const: morphism -> cterm -> bool,
    16     dest_const: morphism -> cterm -> Rat.rat,
    17     mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    18     conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    19   val semiring_funs: thm -> declaration
    20   val field_funs: thm -> declaration
    21 
    22   val semiring_normalize_conv: Proof.context -> conv
    23   val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
    24   val semiring_normalize_wrapper: Proof.context -> entry -> conv
    25   val semiring_normalize_ord_wrapper: Proof.context -> entry
    26     -> (cterm -> cterm -> bool) -> conv
    27   val semiring_normalizers_conv: cterm list -> cterm list * thm list
    28     -> cterm list * thm list -> cterm list * thm list ->
    29       (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    30         {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    31   val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    32     (cterm -> cterm -> bool) ->
    33       {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    34 
    35   val setup: theory -> theory
    36 end
    37 
    38 structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
    39 struct
    40 
    41 (** data **)
    42 
    43 type entry =
    44  {vars: cterm list,
    45   semiring: cterm list * thm list,
    46   ring: cterm list * thm list,
    47   field: cterm list * thm list,
    48   idom: thm list,
    49   ideal: thm list} *
    50  {is_const: cterm -> bool,
    51   dest_const: cterm -> Rat.rat,
    52   mk_const: ctyp -> Rat.rat -> cterm,
    53   conv: Proof.context -> cterm -> thm};
    54 
    55 structure Data = Generic_Data
    56 (
    57   type T = (thm * entry) list;
    58   val empty = [];
    59   val extend = I;
    60   fun merge data = AList.merge Thm.eq_thm (K true) data;
    61 );
    62 
    63 val get = Data.get o Context.Proof;
    64 
    65 fun match ctxt tm =
    66   let
    67     fun match_inst
    68         ({vars, semiring = (sr_ops, sr_rules), 
    69           ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    70          fns as {is_const, dest_const, mk_const, conv}) pat =
    71        let
    72         fun h instT =
    73           let
    74             val substT = Thm.instantiate (instT, []);
    75             val substT_cterm = Drule.cterm_rule substT;
    76 
    77             val vars' = map substT_cterm vars;
    78             val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    79             val ring' = (map substT_cterm r_ops, map substT r_rules);
    80             val field' = (map substT_cterm f_ops, map substT f_rules);
    81             val idom' = map substT idom;
    82             val ideal' = map substT ideal;
    83 
    84             val result = ({vars = vars', semiring = semiring', 
    85                            ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    86           in SOME result end
    87       in (case try Thm.match (pat, tm) of
    88            NONE => NONE
    89          | SOME (instT, _) => h instT)
    90       end;
    91 
    92     fun match_struct (_,
    93         entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
    94       get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
    95   in get_first match_struct (get ctxt) end;
    96 
    97 
    98 (* logical content *)
    99 
   100 val semiringN = "semiring";
   101 val ringN = "ring";
   102 val idomN = "idom";
   103 val idealN = "ideal";
   104 val fieldN = "field";
   105 
   106 val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
   107 
   108 fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   109          field = (f_ops, f_rules), idom, ideal} =
   110   Thm.declaration_attribute (fn key => fn context => context |> Data.map
   111     let
   112       val ctxt = Context.proof_of context;
   113 
   114       fun check kind name xs n =
   115         null xs orelse length xs = n orelse
   116         error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   117       val check_ops = check "operations";
   118       val check_rules = check "rules";
   119 
   120       val _ =
   121         check_ops semiringN sr_ops 5 andalso
   122         check_rules semiringN sr_rules 37 andalso
   123         check_ops ringN r_ops 2 andalso
   124         check_rules ringN r_rules 2 andalso
   125         check_ops fieldN f_ops 2 andalso
   126         check_rules fieldN f_rules 2 andalso
   127         check_rules idomN idom 2;
   128 
   129       val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   130       val sr_rules' = map mk_meta sr_rules;
   131       val r_rules' = map mk_meta r_rules;
   132       val f_rules' = map mk_meta f_rules;
   133 
   134       fun rule i = nth sr_rules' (i - 1);
   135 
   136       val (cx, cy) = Thm.dest_binop (hd sr_ops);
   137       val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   138       val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   139       val ((clx, crx), (cly, cry)) =
   140         rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   141       val ((ca, cb), (cc, cd)) =
   142         rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   143       val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   144       val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   145 
   146       val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   147       val semiring = (sr_ops, sr_rules');
   148       val ring = (r_ops, r_rules');
   149       val field = (f_ops, f_rules');
   150       val ideal' = map (Thm.symmetric o mk_meta) ideal
   151     in
   152       AList.delete Thm.eq_thm key #>
   153       cons (key, ({vars = vars, semiring = semiring, 
   154                           ring = ring, field = field, idom = idom, ideal = ideal'},
   155              {is_const = undefined, dest_const = undefined, mk_const = undefined,
   156              conv = undefined}))
   157     end);
   158 
   159 
   160 (* extra-logical functions *)
   161 
   162 fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   163  Data.map (fn data =>
   164   let
   165     val key = Morphism.thm phi raw_key;
   166     val _ = AList.defined Thm.eq_thm data key orelse
   167       raise THM ("No data entry for structure key", 0, [key]);
   168     val fns = {is_const = is_const phi, dest_const = dest_const phi,
   169       mk_const = mk_const phi, conv = conv phi};
   170   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
   171 
   172 fun semiring_funs key = funs key
   173    {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
   174     dest_const = fn phi => fn ct =>
   175       Rat.rat_of_int (snd
   176         (HOLogic.dest_number (Thm.term_of ct)
   177           handle TERM _ => error "ring_dest_const")),
   178     mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
   179       (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
   180     conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
   181       then_conv Simplifier.rewrite (HOL_basic_ss addsimps
   182         (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
   183 
   184 fun field_funs key =
   185   let
   186     fun numeral_is_const ct =
   187       case term_of ct of
   188        Const (@{const_name Rings.divide},_) $ a $ b =>
   189          can HOLogic.dest_number a andalso can HOLogic.dest_number b
   190      | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   191      | t => can HOLogic.dest_number t
   192     fun dest_const ct = ((case term_of ct of
   193        Const (@{const_name Rings.divide},_) $ a $ b=>
   194         Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   195      | Const (@{const_name Rings.inverse},_)$t => 
   196                    Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   197      | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   198        handle TERM _ => error "ring_dest_const")
   199     fun mk_const phi cT x =
   200       let val (a, b) = Rat.quotient_of_rat x
   201       in if b = 1 then Numeral.mk_cnumber cT a
   202         else Thm.capply
   203              (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   204                          (Numeral.mk_cnumber cT a))
   205              (Numeral.mk_cnumber cT b)
   206       end
   207   in funs key
   208      {is_const = K numeral_is_const,
   209       dest_const = K dest_const,
   210       mk_const = mk_const,
   211       conv = K (K Numeral_Simprocs.field_comp_conv)}
   212   end;
   213 
   214 
   215 
   216 (** auxiliary **)
   217 
   218 fun is_comb ct =
   219   (case Thm.term_of ct of
   220     _ $ _ => true
   221   | _ => false);
   222 
   223 val concl = Thm.cprop_of #> Thm.dest_arg;
   224 
   225 fun is_binop ct ct' =
   226   (case Thm.term_of ct' of
   227     c $ _ $ _ => term_of ct aconv c
   228   | _ => false);
   229 
   230 fun dest_binop ct ct' =
   231   if is_binop ct ct' then Thm.dest_binop ct'
   232   else raise CTERM ("dest_binop: bad binop", [ct, ct'])
   233 
   234 fun inst_thm inst = Thm.instantiate ([], inst);
   235 
   236 val dest_numeral = term_of #> HOLogic.dest_number #> snd;
   237 val is_numeral = can dest_numeral;
   238 
   239 val numeral01_conv = Simplifier.rewrite
   240                          (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
   241 val zero1_numeral_conv = 
   242  Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
   243 fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
   244 val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   245                 @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
   246                 @{thm "less_nat_number_of"}];
   247 
   248 val nat_add_conv = 
   249  zerone_conv 
   250   (Simplifier.rewrite 
   251     (HOL_basic_ss 
   252        addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
   253              @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
   254                  @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
   255              @ map (fn th => th RS sym) @{thms numerals}));
   256 
   257 val zeron_tm = @{cterm "0::nat"};
   258 val onen_tm  = @{cterm "1::nat"};
   259 val true_tm = @{cterm "True"};
   260 
   261 
   262 (** normalizing conversions **)
   263 
   264 (* core conversion *)
   265 
   266 fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
   267   (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
   268 let
   269 
   270 val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
   271      pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
   272      pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
   273      pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
   274      pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
   275 
   276 val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
   277 val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   278 val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
   279 
   280 val dest_add = dest_binop add_tm
   281 val dest_mul = dest_binop mul_tm
   282 fun dest_pow tm =
   283  let val (l,r) = dest_binop pow_tm tm
   284  in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   285  end;
   286 val is_add = is_binop add_tm
   287 val is_mul = is_binop mul_tm
   288 fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   289 
   290 val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   291   (case (r_ops, r_rules) of
   292     ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   293       let
   294         val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   295         val neg_tm = Thm.dest_fun neg_pat
   296         val dest_sub = dest_binop sub_tm
   297         val is_sub = is_binop sub_tm
   298       in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   299           sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   300       end
   301     | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
   302 
   303 val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
   304   (case (f_ops, f_rules) of 
   305    ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
   306      let val div_tm = funpow 2 Thm.dest_fun divide_pat
   307          val inv_tm = Thm.dest_fun inverse_pat
   308      in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
   309      end
   310    | _ => (TrueI, TrueI, true_tm, true_tm, K false));
   311 
   312 in fn variable_order =>
   313  let
   314 
   315 (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   316 (* Also deals with "const * const", but both terms must involve powers of    *)
   317 (* the same variable, or both be constants, or behaviour may be incorrect.   *)
   318 
   319  fun powvar_mul_conv tm =
   320   let
   321   val (l,r) = dest_mul tm
   322   in if is_semiring_constant l andalso is_semiring_constant r
   323      then semiring_mul_conv tm
   324      else
   325       ((let
   326          val (lx,ln) = dest_pow l
   327         in
   328          ((let val (rx,rn) = dest_pow r
   329                val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   330                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   331                Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   332            handle CTERM _ =>
   333             (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   334                  val (tm1,tm2) = Thm.dest_comb(concl th1) in
   335                Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   336        handle CTERM _ =>
   337            ((let val (rx,rn) = dest_pow r
   338                 val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   339                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   340                Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   341            handle CTERM _ => inst_thm [(cx,l)] pthm_32
   342 
   343 ))
   344  end;
   345 
   346 (* Remove "1 * m" from a monomial, and just leave m.                         *)
   347 
   348  fun monomial_deone th =
   349        (let val (l,r) = dest_mul(concl th) in
   350            if l aconvc one_tm
   351           then Thm.transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   352        handle CTERM _ => th;
   353 
   354 (* Conversion for "(monomial)^n", where n is a numeral.                      *)
   355 
   356  val monomial_pow_conv =
   357   let
   358    fun monomial_pow tm bod ntm =
   359     if not(is_comb bod)
   360     then Thm.reflexive tm
   361     else
   362      if is_semiring_constant bod
   363      then semiring_pow_conv tm
   364      else
   365       let
   366       val (lopr,r) = Thm.dest_comb bod
   367       in if not(is_comb lopr)
   368          then Thm.reflexive tm
   369         else
   370           let
   371           val (opr,l) = Thm.dest_comb lopr
   372          in
   373            if opr aconvc pow_tm andalso is_numeral r
   374           then
   375             let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   376                 val (l,r) = Thm.dest_comb(concl th1)
   377            in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   378            end
   379            else
   380             if opr aconvc mul_tm
   381             then
   382              let
   383               val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   384              val (xy,z) = Thm.dest_comb(concl th1)
   385               val (x,y) = Thm.dest_comb xy
   386               val thl = monomial_pow y l ntm
   387               val thr = monomial_pow z r ntm
   388              in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr)
   389              end
   390              else Thm.reflexive tm
   391           end
   392       end
   393   in fn tm =>
   394    let
   395     val (lopr,r) = Thm.dest_comb tm
   396     val (opr,l) = Thm.dest_comb lopr
   397    in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   398       then raise CTERM ("monomial_pow_conv", [tm])
   399       else if r aconvc zeron_tm
   400       then inst_thm [(cx,l)] pthm_35
   401       else if r aconvc onen_tm
   402       then inst_thm [(cx,l)] pthm_36
   403       else monomial_deone(monomial_pow tm l r)
   404    end
   405   end;
   406 
   407 (* Multiplication of canonical monomials.                                    *)
   408  val monomial_mul_conv =
   409   let
   410    fun powvar tm =
   411     if is_semiring_constant tm then one_tm
   412     else
   413      ((let val (lopr,r) = Thm.dest_comb tm
   414            val (opr,l) = Thm.dest_comb lopr
   415        in if opr aconvc pow_tm andalso is_numeral r then l 
   416           else raise CTERM ("monomial_mul_conv",[tm]) end)
   417      handle CTERM _ => tm)   (* FIXME !? *)
   418    fun  vorder x y =
   419     if x aconvc y then 0
   420     else
   421      if x aconvc one_tm then ~1
   422      else if y aconvc one_tm then 1
   423       else if variable_order x y then ~1 else 1
   424    fun monomial_mul tm l r =
   425     ((let val (lx,ly) = dest_mul l val vl = powvar lx
   426       in
   427       ((let
   428         val (rx,ry) = dest_mul r
   429          val vr = powvar rx
   430          val ord = vorder vl vr
   431         in
   432          if ord = 0
   433         then
   434           let
   435              val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   436              val (tm1,tm2) = Thm.dest_comb(concl th1)
   437              val (tm3,tm4) = Thm.dest_comb tm1
   438              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   439              val th3 = Thm.transitive th1 th2
   440               val  (tm5,tm6) = Thm.dest_comb(concl th3)
   441               val  (tm7,tm8) = Thm.dest_comb tm6
   442              val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   443          in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4)
   444          end
   445          else
   446           let val th0 = if ord < 0 then pthm_16 else pthm_17
   447              val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   448              val (tm1,tm2) = Thm.dest_comb(concl th1)
   449              val (tm3,tm4) = Thm.dest_comb tm2
   450          in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   451          end
   452         end)
   453        handle CTERM _ =>
   454         (let val vr = powvar r val ord = vorder vl vr
   455         in
   456           if ord = 0 then
   457            let
   458            val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   459                  val (tm1,tm2) = Thm.dest_comb(concl th1)
   460            val (tm3,tm4) = Thm.dest_comb tm1
   461            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   462           in Thm.transitive th1 th2
   463           end
   464           else
   465           if ord < 0 then
   466             let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   467                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   468                 val (tm3,tm4) = Thm.dest_comb tm2
   469            in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   470            end
   471            else inst_thm [(ca,l),(cb,r)] pthm_09
   472         end)) end)
   473      handle CTERM _ =>
   474       (let val vl = powvar l in
   475         ((let
   476           val (rx,ry) = dest_mul r
   477           val vr = powvar rx
   478            val ord = vorder vl vr
   479          in if ord = 0 then
   480               let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   481                  val (tm1,tm2) = Thm.dest_comb(concl th1)
   482                  val (tm3,tm4) = Thm.dest_comb tm1
   483              in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   484              end
   485              else if ord > 0 then
   486                  let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   487                      val (tm1,tm2) = Thm.dest_comb(concl th1)
   488                     val (tm3,tm4) = Thm.dest_comb tm2
   489                 in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   490                 end
   491              else Thm.reflexive tm
   492          end)
   493         handle CTERM _ =>
   494           (let val vr = powvar r
   495                val  ord = vorder vl vr
   496           in if ord = 0 then powvar_mul_conv tm
   497               else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   498               else Thm.reflexive tm
   499           end)) end))
   500   in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   501              end
   502   end;
   503 (* Multiplication by monomial of a polynomial.                               *)
   504 
   505  val polynomial_monomial_mul_conv =
   506   let
   507    fun pmm_conv tm =
   508     let val (l,r) = dest_mul tm
   509     in
   510     ((let val (y,z) = dest_add r
   511           val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   512           val (tm1,tm2) = Thm.dest_comb(concl th1)
   513           val (tm3,tm4) = Thm.dest_comb tm1
   514           val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   515       in Thm.transitive th1 th2
   516       end)
   517      handle CTERM _ => monomial_mul_conv tm)
   518    end
   519  in pmm_conv
   520  end;
   521 
   522 (* Addition of two monomials identical except for constant multiples.        *)
   523 
   524 fun monomial_add_conv tm =
   525  let val (l,r) = dest_add tm
   526  in if is_semiring_constant l andalso is_semiring_constant r
   527     then semiring_add_conv tm
   528     else
   529      let val th1 =
   530            if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   531            then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   532                     inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   533                 else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   534            else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   535            then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   536            else inst_thm [(cm,r)] pthm_05
   537          val (tm1,tm2) = Thm.dest_comb(concl th1)
   538          val (tm3,tm4) = Thm.dest_comb tm1
   539          val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   540          val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2)
   541          val tm5 = concl th3
   542       in
   543       if (Thm.dest_arg1 tm5) aconvc zero_tm
   544       then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   545       else monomial_deone th3
   546      end
   547  end;
   548 
   549 (* Ordering on monomials.                                                    *)
   550 
   551 fun striplist dest =
   552  let fun strip x acc =
   553    ((let val (l,r) = dest x in
   554         strip l (strip r acc) end)
   555     handle CTERM _ => x::acc)    (* FIXME !? *)
   556  in fn x => strip x []
   557  end;
   558 
   559 
   560 fun powervars tm =
   561  let val ptms = striplist dest_mul tm
   562  in if is_semiring_constant (hd ptms) then tl ptms else ptms
   563  end;
   564 val num_0 = 0;
   565 val num_1 = 1;
   566 fun dest_varpow tm =
   567  ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   568    handle CTERM _ =>
   569    (tm,(if is_semiring_constant tm then num_0 else num_1)));
   570 
   571 val morder =
   572  let fun lexorder l1 l2 =
   573   case (l1,l2) of
   574     ([],[]) => 0
   575   | (vps,[]) => ~1
   576   | ([],vps) => 1
   577   | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   578      if variable_order x1 x2 then 1
   579      else if variable_order x2 x1 then ~1
   580      else if n1 < n2 then ~1
   581      else if n2 < n1 then 1
   582      else lexorder vs1 vs2
   583  in fn tm1 => fn tm2 =>
   584   let val vdegs1 = map dest_varpow (powervars tm1)
   585       val vdegs2 = map dest_varpow (powervars tm2)
   586       val deg1 = fold (Integer.add o snd) vdegs1 num_0
   587       val deg2 = fold (Integer.add o snd) vdegs2 num_0
   588   in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   589                             else lexorder vdegs1 vdegs2
   590   end
   591  end;
   592 
   593 (* Addition of two polynomials.                                              *)
   594 
   595 val polynomial_add_conv =
   596  let
   597  fun dezero_rule th =
   598   let
   599    val tm = concl th
   600   in
   601    if not(is_add tm) then th else
   602    let val (lopr,r) = Thm.dest_comb tm
   603        val l = Thm.dest_arg lopr
   604    in
   605     if l aconvc zero_tm
   606     then Thm.transitive th (inst_thm [(ca,r)] pthm_07)   else
   607         if r aconvc zero_tm
   608         then Thm.transitive th (inst_thm [(ca,l)] pthm_08)  else th
   609    end
   610   end
   611  fun padd tm =
   612   let
   613    val (l,r) = dest_add tm
   614   in
   615    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   616    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   617    else
   618     if is_add l
   619     then
   620      let val (a,b) = dest_add l
   621      in
   622      if is_add r then
   623       let val (c,d) = dest_add r
   624           val ord = morder a c
   625       in
   626        if ord = 0 then
   627         let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   628             val (tm1,tm2) = Thm.dest_comb(concl th1)
   629             val (tm3,tm4) = Thm.dest_comb tm1
   630             val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   631         in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2)))
   632         end
   633        else (* ord <> 0*)
   634         let val th1 =
   635                 if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   636                 else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   637             val (tm1,tm2) = Thm.dest_comb(concl th1)
   638         in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   639         end
   640       end
   641      else (* not (is_add r)*)
   642       let val ord = morder a r
   643       in
   644        if ord = 0 then
   645         let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   646             val (tm1,tm2) = Thm.dest_comb(concl th1)
   647             val (tm3,tm4) = Thm.dest_comb tm1
   648             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   649         in dezero_rule (Thm.transitive th1 th2)
   650         end
   651        else (* ord <> 0*)
   652         if ord > 0 then
   653           let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   654               val (tm1,tm2) = Thm.dest_comb(concl th1)
   655           in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   656           end
   657         else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   658       end
   659     end
   660    else (* not (is_add l)*)
   661     if is_add r then
   662       let val (c,d) = dest_add r
   663           val  ord = morder l c
   664       in
   665        if ord = 0 then
   666          let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   667              val (tm1,tm2) = Thm.dest_comb(concl th1)
   668              val (tm3,tm4) = Thm.dest_comb tm1
   669              val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   670          in dezero_rule (Thm.transitive th1 th2)
   671          end
   672        else
   673         if ord > 0 then Thm.reflexive tm
   674         else
   675          let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   676              val (tm1,tm2) = Thm.dest_comb(concl th1)
   677          in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   678          end
   679       end
   680     else
   681      let val ord = morder l r
   682      in
   683       if ord = 0 then monomial_add_conv tm
   684       else if ord > 0 then dezero_rule(Thm.reflexive tm)
   685       else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   686      end
   687   end
   688  in padd
   689  end;
   690 
   691 (* Multiplication of two polynomials.                                        *)
   692 
   693 val polynomial_mul_conv =
   694  let
   695   fun pmul tm =
   696    let val (l,r) = dest_mul tm
   697    in
   698     if not(is_add l) then polynomial_monomial_mul_conv tm
   699     else
   700      if not(is_add r) then
   701       let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   702       in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1))
   703       end
   704      else
   705        let val (a,b) = dest_add l
   706            val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   707            val (tm1,tm2) = Thm.dest_comb(concl th1)
   708            val (tm3,tm4) = Thm.dest_comb tm1
   709            val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   710            val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2))
   711        in Thm.transitive th3 (polynomial_add_conv (concl th3))
   712        end
   713    end
   714  in fn tm =>
   715    let val (l,r) = dest_mul tm
   716    in
   717     if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   718     else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   719     else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   720     else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   721     else pmul tm
   722    end
   723  end;
   724 
   725 (* Power of polynomial (optimized for the monomial and trivial cases).       *)
   726 
   727 fun num_conv n =
   728   nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   729   |> Thm.symmetric;
   730 
   731 
   732 val polynomial_pow_conv =
   733  let
   734   fun ppow tm =
   735     let val (l,n) = dest_pow tm
   736     in
   737      if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   738      else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   739      else
   740          let val th1 = num_conv n
   741              val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   742              val (tm1,tm2) = Thm.dest_comb(concl th2)
   743              val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   744              val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   745          in Thm.transitive th4 (polynomial_mul_conv (concl th4))
   746          end
   747     end
   748  in fn tm =>
   749        if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   750  end;
   751 
   752 (* Negation.                                                                 *)
   753 
   754 fun polynomial_neg_conv tm =
   755    let val (l,r) = Thm.dest_comb tm in
   756         if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   757         let val th1 = inst_thm [(cx',r)] neg_mul
   758             val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   759         in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2))
   760         end
   761    end;
   762 
   763 
   764 (* Subtraction.                                                              *)
   765 fun polynomial_sub_conv tm =
   766   let val (l,r) = dest_sub tm
   767       val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   768       val (tm1,tm2) = Thm.dest_comb(concl th1)
   769       val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   770   in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2)))
   771   end;
   772 
   773 (* Conversion from HOL term.                                                 *)
   774 
   775 fun polynomial_conv tm =
   776  if is_semiring_constant tm then semiring_add_conv tm
   777  else if not(is_comb tm) then Thm.reflexive tm
   778  else
   779   let val (lopr,r) = Thm.dest_comb tm
   780   in if lopr aconvc neg_tm then
   781        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   782        in Thm.transitive th1 (polynomial_neg_conv (concl th1))
   783        end
   784      else if lopr aconvc inverse_tm then
   785        let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   786        in Thm.transitive th1 (semiring_mul_conv (concl th1))
   787        end
   788      else
   789        if not(is_comb lopr) then Thm.reflexive tm
   790        else
   791          let val (opr,l) = Thm.dest_comb lopr
   792          in if opr aconvc pow_tm andalso is_numeral r
   793             then
   794               let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   795               in Thm.transitive th1 (polynomial_pow_conv (concl th1))
   796               end
   797          else if opr aconvc divide_tm 
   798             then
   799               let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   800                                         (polynomial_conv r)
   801                   val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
   802                               (Thm.rhs_of th1)
   803               in Thm.transitive th1 th2
   804               end
   805             else
   806               if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   807               then
   808                let val th1 =
   809                     Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   810                    val f = if opr aconvc add_tm then polynomial_add_conv
   811                       else if opr aconvc mul_tm then polynomial_mul_conv
   812                       else polynomial_sub_conv
   813                in Thm.transitive th1 (f (concl th1))
   814                end
   815               else Thm.reflexive tm
   816          end
   817   end;
   818  in
   819    {main = polynomial_conv,
   820     add = polynomial_add_conv,
   821     mul = polynomial_mul_conv,
   822     pow = polynomial_pow_conv,
   823     neg = polynomial_neg_conv,
   824     sub = polynomial_sub_conv}
   825  end
   826 end;
   827 
   828 val nat_exp_ss =
   829   HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
   830     addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
   831 
   832 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
   833 
   834 
   835 (* various normalizing conversions *)
   836 
   837 fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   838                                      {conv, dest_const, mk_const, is_const}) ord =
   839   let
   840     val pow_conv =
   841       Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
   842       then_conv Simplifier.rewrite
   843         (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   844       then_conv conv ctxt
   845     val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
   846   in semiring_normalizers_conv vars semiring ring field dat ord end;
   847 
   848 fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
   849  #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);
   850 
   851 fun semiring_normalize_wrapper ctxt data = 
   852   semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   853 
   854 fun semiring_normalize_ord_conv ctxt ord tm =
   855   (case match ctxt tm of
   856     NONE => Thm.reflexive tm
   857   | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   858  
   859 fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   860 
   861 
   862 (** Isar setup **)
   863 
   864 local
   865 
   866 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   867 fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   868 fun keyword3 k1 k2 k3 =
   869   Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   870 
   871 val opsN = "ops";
   872 val rulesN = "rules";
   873 
   874 val normN = "norm";
   875 val constN = "const";
   876 val delN = "del";
   877 
   878 val any_keyword =
   879   keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   880   keyword2 ringN opsN || keyword2 ringN rulesN ||
   881   keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   882   keyword2 idomN rulesN || keyword2 idealN rulesN;
   883 
   884 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   885 val terms = thms >> map Drule.dest_term;
   886 
   887 fun optional scan = Scan.optional scan [];
   888 
   889 in
   890 
   891 val setup =
   892   Attrib.setup @{binding normalizer}
   893     (Scan.lift (Args.$$$ delN >> K del) ||
   894       ((keyword2 semiringN opsN |-- terms) --
   895        (keyword2 semiringN rulesN |-- thms)) --
   896       (optional (keyword2 ringN opsN |-- terms) --
   897        optional (keyword2 ringN rulesN |-- thms)) --
   898       (optional (keyword2 fieldN opsN |-- terms) --
   899        optional (keyword2 fieldN rulesN |-- thms)) --
   900       optional (keyword2 idomN rulesN |-- thms) --
   901       optional (keyword2 idealN rulesN |-- thms)
   902       >> (fn ((((sr, r), f), id), idl) => 
   903              add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   904     "semiring normalizer data";
   905 
   906 end;
   907 
   908 end;