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