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