renamed Normalizer to the more specific Semiring_Normalizer
authorhaftmann
Fri May 07 16:12:26 2010 +0200 (2010-05-07)
changeset 367535cf4e9128f22
parent 36752 cf558aeb35b0
child 36754 5ce217fc769a
renamed Normalizer to the more specific Semiring_Normalizer
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/IsaMakefile
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Semiring_Normalization.thy
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/ex/Groebner_Examples.thy
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri May 07 16:12:25 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri May 07 16:12:26 2010 +0200
     1.3 @@ -700,14 +700,14 @@
     1.4          val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
     1.5               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
     1.6          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
     1.7 -                   (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
     1.8 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
     1.9        in rth end
    1.10      | ("x+t",[t]) =>
    1.11         let
    1.12          val T = ctyp_of_term x
    1.13          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    1.14          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.15 -              (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.16 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.17         in  rth end
    1.18      | ("c*x",[c]) =>
    1.19         let
    1.20 @@ -744,14 +744,14 @@
    1.21          val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    1.22               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    1.23          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.24 -                   (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.25 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.26        in rth end
    1.27      | ("x+t",[t]) =>
    1.28         let
    1.29          val T = ctyp_of_term x
    1.30          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    1.31          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.32 -              (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.33 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.34         in  rth end
    1.35      | ("c*x",[c]) =>
    1.36         let
    1.37 @@ -786,14 +786,14 @@
    1.38          val th = implies_elim
    1.39                   (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    1.40          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.41 -                   (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.42 +                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.43        in rth end
    1.44      | ("x+t",[t]) =>
    1.45         let
    1.46          val T = ctyp_of_term x
    1.47          val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    1.48          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.49 -              (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.50 +              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.51         in  rth end
    1.52      | ("c*x",[c]) =>
    1.53         let
    1.54 @@ -822,7 +822,7 @@
    1.55         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    1.56         val nth = Conv.fconv_rule
    1.57           (Conv.arg_conv (Conv.arg1_conv
    1.58 -              (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.59 +              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.60         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    1.61     in rth end
    1.62  | Const(@{const_name Orderings.less_eq},_)$a$b =>
    1.63 @@ -831,7 +831,7 @@
    1.64         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    1.65         val nth = Conv.fconv_rule
    1.66           (Conv.arg_conv (Conv.arg1_conv
    1.67 -              (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.68 +              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.69         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    1.70     in rth end
    1.71  
    1.72 @@ -841,7 +841,7 @@
    1.73         val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
    1.74         val nth = Conv.fconv_rule
    1.75           (Conv.arg_conv (Conv.arg1_conv
    1.76 -              (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.77 +              (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    1.78         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    1.79     in rth end
    1.80  | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
     2.1 --- a/src/HOL/IsaMakefile	Fri May 07 16:12:25 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri May 07 16:12:26 2010 +0200
     2.3 @@ -284,10 +284,9 @@
     2.4    $(SRC)/Tools/Metis/metis.ML \
     2.5    Tools/ATP_Manager/atp_manager.ML \
     2.6    Tools/ATP_Manager/atp_systems.ML \
     2.7 -  Tools/Groebner_Basis/groebner.ML \
     2.8 -  Tools/Groebner_Basis/normalizer.ML \
     2.9    Tools/choice_specification.ML \
    2.10    Tools/int_arith.ML \
    2.11 +  Tools/groebner.ML \
    2.12    Tools/list_code.ML \
    2.13    Tools/meson.ML \
    2.14    Tools/nat_numeral_simprocs.ML \
    2.15 @@ -314,6 +313,7 @@
    2.16    Tools/Quotient/quotient_term.ML \
    2.17    Tools/Quotient/quotient_typ.ML \
    2.18    Tools/recdef.ML \
    2.19 +  Tools/semiring_normalizer.ML \
    2.20    Tools/Sledgehammer/meson_tactic.ML \
    2.21    Tools/Sledgehammer/metis_tactics.ML \
    2.22    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
     3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri May 07 16:12:25 2010 +0200
     3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri May 07 16:12:26 2010 +0200
     3.3 @@ -1194,8 +1194,8 @@
     3.4    (* FIXME: Replace tryfind by get_first !! *)
     3.5  fun real_nonlinear_prover proof_method ctxt =
     3.6   let
     3.7 -  val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
     3.8 -      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
     3.9 +  val {add,mul,neg,pow,sub,main} =  Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.10 +      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    3.11       simple_cterm_ord
    3.12    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
    3.13         real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
    3.14 @@ -1309,8 +1309,8 @@
    3.15  
    3.16  fun real_nonlinear_subst_prover prover ctxt =
    3.17   let
    3.18 -  val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.19 -      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    3.20 +  val {add,mul,neg,pow,sub,main} =  Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    3.21 +      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    3.22       simple_cterm_ord
    3.23  
    3.24    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
     4.1 --- a/src/HOL/Library/normarith.ML	Fri May 07 16:12:25 2010 +0200
     4.2 +++ b/src/HOL/Library/normarith.ML	Fri May 07 16:12:26 2010 +0200
     4.3 @@ -166,8 +166,8 @@
     4.4   let 
     4.5    (* FIXME : Should be computed statically!! *)
     4.6    val real_poly_conv = 
     4.7 -    Normalizer.semiring_normalize_wrapper ctxt
     4.8 -     (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
     4.9 +    Semiring_Normalizer.semiring_normalize_wrapper ctxt
    4.10 +     (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    4.11   in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
    4.12  end;
    4.13  
    4.14 @@ -277,8 +277,8 @@
    4.15    let 
    4.16     (* FIXME: Should be computed statically!!*)
    4.17     val real_poly_conv = 
    4.18 -      Normalizer.semiring_normalize_wrapper ctxt
    4.19 -       (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    4.20 +      Semiring_Normalizer.semiring_normalize_wrapper ctxt
    4.21 +       (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    4.22     val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
    4.23     val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
    4.24     val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
    4.25 @@ -383,8 +383,8 @@
    4.26   fun splitequation ctxt th acc =
    4.27    let 
    4.28     val real_poly_neg_conv = #neg
    4.29 -       (Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.30 -        (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    4.31 +       (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.32 +        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    4.33     val (th1,th2) = conj_pair(rawrule th)
    4.34    in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
    4.35    end
     5.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri May 07 16:12:25 2010 +0200
     5.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 07 16:12:26 2010 +0200
     5.3 @@ -747,8 +747,8 @@
     5.4   let
     5.5    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
     5.6    val {add,mul,neg,pow,sub,main} = 
     5.7 -     Normalizer.semiring_normalizers_ord_wrapper ctxt
     5.8 -      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     5.9 +     Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    5.10 +      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
    5.11       simple_cterm_ord
    5.12  in gen_real_arith ctxt
    5.13     (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
     6.1 --- a/src/HOL/Semiring_Normalization.thy	Fri May 07 16:12:25 2010 +0200
     6.2 +++ b/src/HOL/Semiring_Normalization.thy	Fri May 07 16:12:26 2010 +0200
     6.3 @@ -7,10 +7,10 @@
     6.4  theory Semiring_Normalization
     6.5  imports Numeral_Simprocs Nat_Transfer
     6.6  uses
     6.7 -  "Tools/Groebner_Basis/normalizer.ML"
     6.8 +  "Tools/semiring_normalizer.ML"
     6.9  begin
    6.10  
    6.11 -setup Normalizer.setup
    6.12 +setup Semiring_Normalizer.setup
    6.13  
    6.14  locale normalizing_semiring =
    6.15    fixes add mul pwr r0 r1
    6.16 @@ -159,7 +159,7 @@
    6.17  proof
    6.18  qed (simp_all add: algebra_simps)
    6.19  
    6.20 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
    6.21 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
    6.22  
    6.23  locale normalizing_ring = normalizing_semiring +
    6.24    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.25 @@ -186,7 +186,7 @@
    6.26  proof
    6.27  qed (simp_all add: diff_minus)
    6.28  
    6.29 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
    6.30 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
    6.31  
    6.32  locale normalizing_field = normalizing_ring +
    6.33    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.34 @@ -283,7 +283,7 @@
    6.35    qed (auto simp add: add_ac)
    6.36  qed (simp_all add: algebra_simps)
    6.37  
    6.38 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
    6.39 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
    6.40  
    6.41  interpretation normalizing_nat!: normalizing_semiring_cancel
    6.42    "op +" "op *" "op ^" "0::nat" "1"
    6.43 @@ -307,7 +307,7 @@
    6.44    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    6.45  qed
    6.46  
    6.47 -declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
    6.48 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
    6.49  
    6.50  locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
    6.51  begin
    6.52 @@ -331,6 +331,6 @@
    6.53  proof
    6.54  qed (simp_all add: divide_inverse)
    6.55  
    6.56 -declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
    6.57 +declaration {* Semiring_Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
    6.58  
    6.59  end
     7.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri May 07 16:12:25 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,913 +0,0 @@
     7.4 -(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     7.5 -    Author:     Amine Chaieb, TU Muenchen
     7.6 -
     7.7 -Normalization of expressions in semirings.
     7.8 -*)
     7.9 -
    7.10 -signature NORMALIZER = 
    7.11 -sig
    7.12 -  type entry
    7.13 -  val get: Proof.context -> (thm * entry) list
    7.14 -  val match: Proof.context -> cterm -> entry option
    7.15 -  val del: attribute
    7.16 -  val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
    7.17 -    field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
    7.18 -  val funs: thm -> {is_const: morphism -> cterm -> bool,
    7.19 -    dest_const: morphism -> cterm -> Rat.rat,
    7.20 -    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    7.21 -    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    7.22 -  val semiring_funs: thm -> declaration
    7.23 -  val field_funs: thm -> declaration
    7.24 -
    7.25 -  val semiring_normalize_conv: Proof.context -> conv
    7.26 -  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
    7.27 -  val semiring_normalize_wrapper: Proof.context -> entry -> conv
    7.28 -  val semiring_normalize_ord_wrapper: Proof.context -> entry
    7.29 -    -> (cterm -> cterm -> bool) -> conv
    7.30 -  val semiring_normalizers_conv: cterm list -> cterm list * thm list
    7.31 -    -> cterm list * thm list -> cterm list * thm list ->
    7.32 -      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    7.33 -        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    7.34 -  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    7.35 -    (cterm -> cterm -> bool) ->
    7.36 -      {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    7.37 -
    7.38 -  val setup: theory -> theory
    7.39 -end
    7.40 -
    7.41 -structure Normalizer: NORMALIZER = 
    7.42 -struct
    7.43 -
    7.44 -(** some conversion **)
    7.45 -
    7.46 -
    7.47 -
    7.48 -(** data **)
    7.49 -
    7.50 -type entry =
    7.51 - {vars: cterm list,
    7.52 -  semiring: cterm list * thm list,
    7.53 -  ring: cterm list * thm list,
    7.54 -  field: cterm list * thm list,
    7.55 -  idom: thm list,
    7.56 -  ideal: thm list} *
    7.57 - {is_const: cterm -> bool,
    7.58 -  dest_const: cterm -> Rat.rat,
    7.59 -  mk_const: ctyp -> Rat.rat -> cterm,
    7.60 -  conv: Proof.context -> cterm -> thm};
    7.61 -
    7.62 -structure Data = Generic_Data
    7.63 -(
    7.64 -  type T = (thm * entry) list;
    7.65 -  val empty = [];
    7.66 -  val extend = I;
    7.67 -  val merge = AList.merge Thm.eq_thm (K true);
    7.68 -);
    7.69 -
    7.70 -val get = Data.get o Context.Proof;
    7.71 -
    7.72 -fun match ctxt tm =
    7.73 -  let
    7.74 -    fun match_inst
    7.75 -        ({vars, semiring = (sr_ops, sr_rules), 
    7.76 -          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    7.77 -         fns as {is_const, dest_const, mk_const, conv}) pat =
    7.78 -       let
    7.79 -        fun h instT =
    7.80 -          let
    7.81 -            val substT = Thm.instantiate (instT, []);
    7.82 -            val substT_cterm = Drule.cterm_rule substT;
    7.83 -
    7.84 -            val vars' = map substT_cterm vars;
    7.85 -            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    7.86 -            val ring' = (map substT_cterm r_ops, map substT r_rules);
    7.87 -            val field' = (map substT_cterm f_ops, map substT f_rules);
    7.88 -            val idom' = map substT idom;
    7.89 -            val ideal' = map substT ideal;
    7.90 -
    7.91 -            val result = ({vars = vars', semiring = semiring', 
    7.92 -                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    7.93 -          in SOME result end
    7.94 -      in (case try Thm.match (pat, tm) of
    7.95 -           NONE => NONE
    7.96 -         | SOME (instT, _) => h instT)
    7.97 -      end;
    7.98 -
    7.99 -    fun match_struct (_,
   7.100 -        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
   7.101 -      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
   7.102 -  in get_first match_struct (get ctxt) end;
   7.103 -
   7.104 -
   7.105 -(* logical content *)
   7.106 -
   7.107 -val semiringN = "semiring";
   7.108 -val ringN = "ring";
   7.109 -val idomN = "idom";
   7.110 -val idealN = "ideal";
   7.111 -val fieldN = "field";
   7.112 -
   7.113 -fun undefined _ = raise Match;
   7.114 -
   7.115 -val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
   7.116 -
   7.117 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   7.118 -         field = (f_ops, f_rules), idom, ideal} =
   7.119 -  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   7.120 -    let
   7.121 -      val ctxt = Context.proof_of context;
   7.122 -
   7.123 -      fun check kind name xs n =
   7.124 -        null xs orelse length xs = n orelse
   7.125 -        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   7.126 -      val check_ops = check "operations";
   7.127 -      val check_rules = check "rules";
   7.128 -
   7.129 -      val _ =
   7.130 -        check_ops semiringN sr_ops 5 andalso
   7.131 -        check_rules semiringN sr_rules 37 andalso
   7.132 -        check_ops ringN r_ops 2 andalso
   7.133 -        check_rules ringN r_rules 2 andalso
   7.134 -        check_ops fieldN f_ops 2 andalso
   7.135 -        check_rules fieldN f_rules 2 andalso
   7.136 -        check_rules idomN idom 2;
   7.137 -
   7.138 -      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   7.139 -      val sr_rules' = map mk_meta sr_rules;
   7.140 -      val r_rules' = map mk_meta r_rules;
   7.141 -      val f_rules' = map mk_meta f_rules;
   7.142 -
   7.143 -      fun rule i = nth sr_rules' (i - 1);
   7.144 -
   7.145 -      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   7.146 -      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   7.147 -      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   7.148 -      val ((clx, crx), (cly, cry)) =
   7.149 -        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   7.150 -      val ((ca, cb), (cc, cd)) =
   7.151 -        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   7.152 -      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   7.153 -      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   7.154 -
   7.155 -      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   7.156 -      val semiring = (sr_ops, sr_rules');
   7.157 -      val ring = (r_ops, r_rules');
   7.158 -      val field = (f_ops, f_rules');
   7.159 -      val ideal' = map (symmetric o mk_meta) ideal
   7.160 -    in
   7.161 -      AList.delete Thm.eq_thm key #>
   7.162 -      cons (key, ({vars = vars, semiring = semiring, 
   7.163 -                          ring = ring, field = field, idom = idom, ideal = ideal'},
   7.164 -             {is_const = undefined, dest_const = undefined, mk_const = undefined,
   7.165 -             conv = undefined}))
   7.166 -    end);
   7.167 -
   7.168 -
   7.169 -(* extra-logical functions *)
   7.170 -
   7.171 -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   7.172 - Data.map (fn data =>
   7.173 -  let
   7.174 -    val key = Morphism.thm phi raw_key;
   7.175 -    val _ = AList.defined Thm.eq_thm data key orelse
   7.176 -      raise THM ("No data entry for structure key", 0, [key]);
   7.177 -    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   7.178 -      mk_const = mk_const phi, conv = conv phi};
   7.179 -  in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
   7.180 -
   7.181 -fun semiring_funs key = funs key
   7.182 -   {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
   7.183 -    dest_const = fn phi => fn ct =>
   7.184 -      Rat.rat_of_int (snd
   7.185 -        (HOLogic.dest_number (Thm.term_of ct)
   7.186 -          handle TERM _ => error "ring_dest_const")),
   7.187 -    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
   7.188 -      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
   7.189 -    conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
   7.190 -      then_conv Simplifier.rewrite (HOL_basic_ss addsimps
   7.191 -        (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
   7.192 -
   7.193 -fun field_funs key =
   7.194 -  let
   7.195 -    fun numeral_is_const ct =
   7.196 -      case term_of ct of
   7.197 -       Const (@{const_name Rings.divide},_) $ a $ b =>
   7.198 -         can HOLogic.dest_number a andalso can HOLogic.dest_number b
   7.199 -     | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   7.200 -     | t => can HOLogic.dest_number t
   7.201 -    fun dest_const ct = ((case term_of ct of
   7.202 -       Const (@{const_name Rings.divide},_) $ a $ b=>
   7.203 -        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   7.204 -     | Const (@{const_name Rings.inverse},_)$t => 
   7.205 -                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   7.206 -     | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   7.207 -       handle TERM _ => error "ring_dest_const")
   7.208 -    fun mk_const phi cT x =
   7.209 -      let val (a, b) = Rat.quotient_of_rat x
   7.210 -      in if b = 1 then Numeral.mk_cnumber cT a
   7.211 -        else Thm.capply
   7.212 -             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   7.213 -                         (Numeral.mk_cnumber cT a))
   7.214 -             (Numeral.mk_cnumber cT b)
   7.215 -      end
   7.216 -  in funs key
   7.217 -     {is_const = K numeral_is_const,
   7.218 -      dest_const = K dest_const,
   7.219 -      mk_const = mk_const,
   7.220 -      conv = K (K Numeral_Simprocs.field_comp_conv)}
   7.221 -  end;
   7.222 -
   7.223 -
   7.224 -
   7.225 -(** auxiliary **)
   7.226 -
   7.227 -fun is_comb ct =
   7.228 -  (case Thm.term_of ct of
   7.229 -    _ $ _ => true
   7.230 -  | _ => false);
   7.231 -
   7.232 -val concl = Thm.cprop_of #> Thm.dest_arg;
   7.233 -
   7.234 -fun is_binop ct ct' =
   7.235 -  (case Thm.term_of ct' of
   7.236 -    c $ _ $ _ => term_of ct aconv c
   7.237 -  | _ => false);
   7.238 -
   7.239 -fun dest_binop ct ct' =
   7.240 -  if is_binop ct ct' then Thm.dest_binop ct'
   7.241 -  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
   7.242 -
   7.243 -fun inst_thm inst = Thm.instantiate ([], inst);
   7.244 -
   7.245 -val dest_numeral = term_of #> HOLogic.dest_number #> snd;
   7.246 -val is_numeral = can dest_numeral;
   7.247 -
   7.248 -val numeral01_conv = Simplifier.rewrite
   7.249 -                         (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
   7.250 -val zero1_numeral_conv = 
   7.251 - Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
   7.252 -fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
   7.253 -val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   7.254 -                @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
   7.255 -                @{thm "less_nat_number_of"}];
   7.256 -
   7.257 -val nat_add_conv = 
   7.258 - zerone_conv 
   7.259 -  (Simplifier.rewrite 
   7.260 -    (HOL_basic_ss 
   7.261 -       addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
   7.262 -             @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
   7.263 -                 @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
   7.264 -             @ map (fn th => th RS sym) @{thms numerals}));
   7.265 -
   7.266 -val zeron_tm = @{cterm "0::nat"};
   7.267 -val onen_tm  = @{cterm "1::nat"};
   7.268 -val true_tm = @{cterm "True"};
   7.269 -
   7.270 -
   7.271 -(** normalizing conversions **)
   7.272 -
   7.273 -(* core conversion *)
   7.274 -
   7.275 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
   7.276 -  (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
   7.277 -let
   7.278 -
   7.279 -val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
   7.280 -     pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
   7.281 -     pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
   7.282 -     pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
   7.283 -     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
   7.284 -
   7.285 -val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
   7.286 -val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   7.287 -val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
   7.288 -
   7.289 -val dest_add = dest_binop add_tm
   7.290 -val dest_mul = dest_binop mul_tm
   7.291 -fun dest_pow tm =
   7.292 - let val (l,r) = dest_binop pow_tm tm
   7.293 - in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   7.294 - end;
   7.295 -val is_add = is_binop add_tm
   7.296 -val is_mul = is_binop mul_tm
   7.297 -fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   7.298 -
   7.299 -val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   7.300 -  (case (r_ops, r_rules) of
   7.301 -    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   7.302 -      let
   7.303 -        val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   7.304 -        val neg_tm = Thm.dest_fun neg_pat
   7.305 -        val dest_sub = dest_binop sub_tm
   7.306 -        val is_sub = is_binop sub_tm
   7.307 -      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   7.308 -          sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   7.309 -      end
   7.310 -    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
   7.311 -
   7.312 -val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
   7.313 -  (case (f_ops, f_rules) of 
   7.314 -   ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
   7.315 -     let val div_tm = funpow 2 Thm.dest_fun divide_pat
   7.316 -         val inv_tm = Thm.dest_fun inverse_pat
   7.317 -     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
   7.318 -     end
   7.319 -   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
   7.320 -
   7.321 -in fn variable_order =>
   7.322 - let
   7.323 -
   7.324 -(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   7.325 -(* Also deals with "const * const", but both terms must involve powers of    *)
   7.326 -(* the same variable, or both be constants, or behaviour may be incorrect.   *)
   7.327 -
   7.328 - fun powvar_mul_conv tm =
   7.329 -  let
   7.330 -  val (l,r) = dest_mul tm
   7.331 -  in if is_semiring_constant l andalso is_semiring_constant r
   7.332 -     then semiring_mul_conv tm
   7.333 -     else
   7.334 -      ((let
   7.335 -         val (lx,ln) = dest_pow l
   7.336 -        in
   7.337 -         ((let val (rx,rn) = dest_pow r
   7.338 -               val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   7.339 -                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.340 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   7.341 -           handle CTERM _ =>
   7.342 -            (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   7.343 -                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.344 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   7.345 -       handle CTERM _ =>
   7.346 -           ((let val (rx,rn) = dest_pow r
   7.347 -                val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   7.348 -                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   7.349 -               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   7.350 -           handle CTERM _ => inst_thm [(cx,l)] pthm_32
   7.351 -
   7.352 -))
   7.353 - end;
   7.354 -
   7.355 -(* Remove "1 * m" from a monomial, and just leave m.                         *)
   7.356 -
   7.357 - fun monomial_deone th =
   7.358 -       (let val (l,r) = dest_mul(concl th) in
   7.359 -           if l aconvc one_tm
   7.360 -          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   7.361 -       handle CTERM _ => th;
   7.362 -
   7.363 -(* Conversion for "(monomial)^n", where n is a numeral.                      *)
   7.364 -
   7.365 - val monomial_pow_conv =
   7.366 -  let
   7.367 -   fun monomial_pow tm bod ntm =
   7.368 -    if not(is_comb bod)
   7.369 -    then reflexive tm
   7.370 -    else
   7.371 -     if is_semiring_constant bod
   7.372 -     then semiring_pow_conv tm
   7.373 -     else
   7.374 -      let
   7.375 -      val (lopr,r) = Thm.dest_comb bod
   7.376 -      in if not(is_comb lopr)
   7.377 -         then reflexive tm
   7.378 -        else
   7.379 -          let
   7.380 -          val (opr,l) = Thm.dest_comb lopr
   7.381 -         in
   7.382 -           if opr aconvc pow_tm andalso is_numeral r
   7.383 -          then
   7.384 -            let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   7.385 -                val (l,r) = Thm.dest_comb(concl th1)
   7.386 -           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   7.387 -           end
   7.388 -           else
   7.389 -            if opr aconvc mul_tm
   7.390 -            then
   7.391 -             let
   7.392 -              val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   7.393 -             val (xy,z) = Thm.dest_comb(concl th1)
   7.394 -              val (x,y) = Thm.dest_comb xy
   7.395 -              val thl = monomial_pow y l ntm
   7.396 -              val thr = monomial_pow z r ntm
   7.397 -             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   7.398 -             end
   7.399 -             else reflexive tm
   7.400 -          end
   7.401 -      end
   7.402 -  in fn tm =>
   7.403 -   let
   7.404 -    val (lopr,r) = Thm.dest_comb tm
   7.405 -    val (opr,l) = Thm.dest_comb lopr
   7.406 -   in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   7.407 -      then raise CTERM ("monomial_pow_conv", [tm])
   7.408 -      else if r aconvc zeron_tm
   7.409 -      then inst_thm [(cx,l)] pthm_35
   7.410 -      else if r aconvc onen_tm
   7.411 -      then inst_thm [(cx,l)] pthm_36
   7.412 -      else monomial_deone(monomial_pow tm l r)
   7.413 -   end
   7.414 -  end;
   7.415 -
   7.416 -(* Multiplication of canonical monomials.                                    *)
   7.417 - val monomial_mul_conv =
   7.418 -  let
   7.419 -   fun powvar tm =
   7.420 -    if is_semiring_constant tm then one_tm
   7.421 -    else
   7.422 -     ((let val (lopr,r) = Thm.dest_comb tm
   7.423 -           val (opr,l) = Thm.dest_comb lopr
   7.424 -       in if opr aconvc pow_tm andalso is_numeral r then l 
   7.425 -          else raise CTERM ("monomial_mul_conv",[tm]) end)
   7.426 -     handle CTERM _ => tm)   (* FIXME !? *)
   7.427 -   fun  vorder x y =
   7.428 -    if x aconvc y then 0
   7.429 -    else
   7.430 -     if x aconvc one_tm then ~1
   7.431 -     else if y aconvc one_tm then 1
   7.432 -      else if variable_order x y then ~1 else 1
   7.433 -   fun monomial_mul tm l r =
   7.434 -    ((let val (lx,ly) = dest_mul l val vl = powvar lx
   7.435 -      in
   7.436 -      ((let
   7.437 -        val (rx,ry) = dest_mul r
   7.438 -         val vr = powvar rx
   7.439 -         val ord = vorder vl vr
   7.440 -        in
   7.441 -         if ord = 0
   7.442 -        then
   7.443 -          let
   7.444 -             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   7.445 -             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.446 -             val (tm3,tm4) = Thm.dest_comb tm1
   7.447 -             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   7.448 -             val th3 = transitive th1 th2
   7.449 -              val  (tm5,tm6) = Thm.dest_comb(concl th3)
   7.450 -              val  (tm7,tm8) = Thm.dest_comb tm6
   7.451 -             val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   7.452 -         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   7.453 -         end
   7.454 -         else
   7.455 -          let val th0 = if ord < 0 then pthm_16 else pthm_17
   7.456 -             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   7.457 -             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.458 -             val (tm3,tm4) = Thm.dest_comb tm2
   7.459 -         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.460 -         end
   7.461 -        end)
   7.462 -       handle CTERM _ =>
   7.463 -        (let val vr = powvar r val ord = vorder vl vr
   7.464 -        in
   7.465 -          if ord = 0 then
   7.466 -           let
   7.467 -           val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   7.468 -                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.469 -           val (tm3,tm4) = Thm.dest_comb tm1
   7.470 -           val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   7.471 -          in transitive th1 th2
   7.472 -          end
   7.473 -          else
   7.474 -          if ord < 0 then
   7.475 -            let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   7.476 -                val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.477 -                val (tm3,tm4) = Thm.dest_comb tm2
   7.478 -           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.479 -           end
   7.480 -           else inst_thm [(ca,l),(cb,r)] pthm_09
   7.481 -        end)) end)
   7.482 -     handle CTERM _ =>
   7.483 -      (let val vl = powvar l in
   7.484 -        ((let
   7.485 -          val (rx,ry) = dest_mul r
   7.486 -          val vr = powvar rx
   7.487 -           val ord = vorder vl vr
   7.488 -         in if ord = 0 then
   7.489 -              let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   7.490 -                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.491 -                 val (tm3,tm4) = Thm.dest_comb tm1
   7.492 -             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   7.493 -             end
   7.494 -             else if ord > 0 then
   7.495 -                 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   7.496 -                     val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.497 -                    val (tm3,tm4) = Thm.dest_comb tm2
   7.498 -                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   7.499 -                end
   7.500 -             else reflexive tm
   7.501 -         end)
   7.502 -        handle CTERM _ =>
   7.503 -          (let val vr = powvar r
   7.504 -               val  ord = vorder vl vr
   7.505 -          in if ord = 0 then powvar_mul_conv tm
   7.506 -              else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   7.507 -              else reflexive tm
   7.508 -          end)) end))
   7.509 -  in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   7.510 -             end
   7.511 -  end;
   7.512 -(* Multiplication by monomial of a polynomial.                               *)
   7.513 -
   7.514 - val polynomial_monomial_mul_conv =
   7.515 -  let
   7.516 -   fun pmm_conv tm =
   7.517 -    let val (l,r) = dest_mul tm
   7.518 -    in
   7.519 -    ((let val (y,z) = dest_add r
   7.520 -          val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   7.521 -          val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.522 -          val (tm3,tm4) = Thm.dest_comb tm1
   7.523 -          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   7.524 -      in transitive th1 th2
   7.525 -      end)
   7.526 -     handle CTERM _ => monomial_mul_conv tm)
   7.527 -   end
   7.528 - in pmm_conv
   7.529 - end;
   7.530 -
   7.531 -(* Addition of two monomials identical except for constant multiples.        *)
   7.532 -
   7.533 -fun monomial_add_conv tm =
   7.534 - let val (l,r) = dest_add tm
   7.535 - in if is_semiring_constant l andalso is_semiring_constant r
   7.536 -    then semiring_add_conv tm
   7.537 -    else
   7.538 -     let val th1 =
   7.539 -           if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   7.540 -           then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   7.541 -                    inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   7.542 -                else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   7.543 -           else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   7.544 -           then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   7.545 -           else inst_thm [(cm,r)] pthm_05
   7.546 -         val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.547 -         val (tm3,tm4) = Thm.dest_comb tm1
   7.548 -         val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   7.549 -         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   7.550 -         val tm5 = concl th3
   7.551 -      in
   7.552 -      if (Thm.dest_arg1 tm5) aconvc zero_tm
   7.553 -      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   7.554 -      else monomial_deone th3
   7.555 -     end
   7.556 - end;
   7.557 -
   7.558 -(* Ordering on monomials.                                                    *)
   7.559 -
   7.560 -fun striplist dest =
   7.561 - let fun strip x acc =
   7.562 -   ((let val (l,r) = dest x in
   7.563 -        strip l (strip r acc) end)
   7.564 -    handle CTERM _ => x::acc)    (* FIXME !? *)
   7.565 - in fn x => strip x []
   7.566 - end;
   7.567 -
   7.568 -
   7.569 -fun powervars tm =
   7.570 - let val ptms = striplist dest_mul tm
   7.571 - in if is_semiring_constant (hd ptms) then tl ptms else ptms
   7.572 - end;
   7.573 -val num_0 = 0;
   7.574 -val num_1 = 1;
   7.575 -fun dest_varpow tm =
   7.576 - ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   7.577 -   handle CTERM _ =>
   7.578 -   (tm,(if is_semiring_constant tm then num_0 else num_1)));
   7.579 -
   7.580 -val morder =
   7.581 - let fun lexorder l1 l2 =
   7.582 -  case (l1,l2) of
   7.583 -    ([],[]) => 0
   7.584 -  | (vps,[]) => ~1
   7.585 -  | ([],vps) => 1
   7.586 -  | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   7.587 -     if variable_order x1 x2 then 1
   7.588 -     else if variable_order x2 x1 then ~1
   7.589 -     else if n1 < n2 then ~1
   7.590 -     else if n2 < n1 then 1
   7.591 -     else lexorder vs1 vs2
   7.592 - in fn tm1 => fn tm2 =>
   7.593 -  let val vdegs1 = map dest_varpow (powervars tm1)
   7.594 -      val vdegs2 = map dest_varpow (powervars tm2)
   7.595 -      val deg1 = fold (Integer.add o snd) vdegs1 num_0
   7.596 -      val deg2 = fold (Integer.add o snd) vdegs2 num_0
   7.597 -  in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   7.598 -                            else lexorder vdegs1 vdegs2
   7.599 -  end
   7.600 - end;
   7.601 -
   7.602 -(* Addition of two polynomials.                                              *)
   7.603 -
   7.604 -val polynomial_add_conv =
   7.605 - let
   7.606 - fun dezero_rule th =
   7.607 -  let
   7.608 -   val tm = concl th
   7.609 -  in
   7.610 -   if not(is_add tm) then th else
   7.611 -   let val (lopr,r) = Thm.dest_comb tm
   7.612 -       val l = Thm.dest_arg lopr
   7.613 -   in
   7.614 -    if l aconvc zero_tm
   7.615 -    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   7.616 -        if r aconvc zero_tm
   7.617 -        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   7.618 -   end
   7.619 -  end
   7.620 - fun padd tm =
   7.621 -  let
   7.622 -   val (l,r) = dest_add tm
   7.623 -  in
   7.624 -   if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   7.625 -   else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   7.626 -   else
   7.627 -    if is_add l
   7.628 -    then
   7.629 -     let val (a,b) = dest_add l
   7.630 -     in
   7.631 -     if is_add r then
   7.632 -      let val (c,d) = dest_add r
   7.633 -          val ord = morder a c
   7.634 -      in
   7.635 -       if ord = 0 then
   7.636 -        let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   7.637 -            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.638 -            val (tm3,tm4) = Thm.dest_comb tm1
   7.639 -            val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   7.640 -        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   7.641 -        end
   7.642 -       else (* ord <> 0*)
   7.643 -        let val th1 =
   7.644 -                if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   7.645 -                else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   7.646 -            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.647 -        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.648 -        end
   7.649 -      end
   7.650 -     else (* not (is_add r)*)
   7.651 -      let val ord = morder a r
   7.652 -      in
   7.653 -       if ord = 0 then
   7.654 -        let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   7.655 -            val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.656 -            val (tm3,tm4) = Thm.dest_comb tm1
   7.657 -            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   7.658 -        in dezero_rule (transitive th1 th2)
   7.659 -        end
   7.660 -       else (* ord <> 0*)
   7.661 -        if ord > 0 then
   7.662 -          let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   7.663 -              val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.664 -          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.665 -          end
   7.666 -        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   7.667 -      end
   7.668 -    end
   7.669 -   else (* not (is_add l)*)
   7.670 -    if is_add r then
   7.671 -      let val (c,d) = dest_add r
   7.672 -          val  ord = morder l c
   7.673 -      in
   7.674 -       if ord = 0 then
   7.675 -         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   7.676 -             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.677 -             val (tm3,tm4) = Thm.dest_comb tm1
   7.678 -             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   7.679 -         in dezero_rule (transitive th1 th2)
   7.680 -         end
   7.681 -       else
   7.682 -        if ord > 0 then reflexive tm
   7.683 -        else
   7.684 -         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   7.685 -             val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.686 -         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   7.687 -         end
   7.688 -      end
   7.689 -    else
   7.690 -     let val ord = morder l r
   7.691 -     in
   7.692 -      if ord = 0 then monomial_add_conv tm
   7.693 -      else if ord > 0 then dezero_rule(reflexive tm)
   7.694 -      else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   7.695 -     end
   7.696 -  end
   7.697 - in padd
   7.698 - end;
   7.699 -
   7.700 -(* Multiplication of two polynomials.                                        *)
   7.701 -
   7.702 -val polynomial_mul_conv =
   7.703 - let
   7.704 -  fun pmul tm =
   7.705 -   let val (l,r) = dest_mul tm
   7.706 -   in
   7.707 -    if not(is_add l) then polynomial_monomial_mul_conv tm
   7.708 -    else
   7.709 -     if not(is_add r) then
   7.710 -      let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   7.711 -      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   7.712 -      end
   7.713 -     else
   7.714 -       let val (a,b) = dest_add l
   7.715 -           val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   7.716 -           val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.717 -           val (tm3,tm4) = Thm.dest_comb tm1
   7.718 -           val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   7.719 -           val th3 = transitive th1 (combination th2 (pmul tm2))
   7.720 -       in transitive th3 (polynomial_add_conv (concl th3))
   7.721 -       end
   7.722 -   end
   7.723 - in fn tm =>
   7.724 -   let val (l,r) = dest_mul tm
   7.725 -   in
   7.726 -    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   7.727 -    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   7.728 -    else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   7.729 -    else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   7.730 -    else pmul tm
   7.731 -   end
   7.732 - end;
   7.733 -
   7.734 -(* Power of polynomial (optimized for the monomial and trivial cases).       *)
   7.735 -
   7.736 -fun num_conv n =
   7.737 -  nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   7.738 -  |> Thm.symmetric;
   7.739 -
   7.740 -
   7.741 -val polynomial_pow_conv =
   7.742 - let
   7.743 -  fun ppow tm =
   7.744 -    let val (l,n) = dest_pow tm
   7.745 -    in
   7.746 -     if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   7.747 -     else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   7.748 -     else
   7.749 -         let val th1 = num_conv n
   7.750 -             val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   7.751 -             val (tm1,tm2) = Thm.dest_comb(concl th2)
   7.752 -             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   7.753 -             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   7.754 -         in transitive th4 (polynomial_mul_conv (concl th4))
   7.755 -         end
   7.756 -    end
   7.757 - in fn tm =>
   7.758 -       if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   7.759 - end;
   7.760 -
   7.761 -(* Negation.                                                                 *)
   7.762 -
   7.763 -fun polynomial_neg_conv tm =
   7.764 -   let val (l,r) = Thm.dest_comb tm in
   7.765 -        if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   7.766 -        let val th1 = inst_thm [(cx',r)] neg_mul
   7.767 -            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   7.768 -        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   7.769 -        end
   7.770 -   end;
   7.771 -
   7.772 -
   7.773 -(* Subtraction.                                                              *)
   7.774 -fun polynomial_sub_conv tm =
   7.775 -  let val (l,r) = dest_sub tm
   7.776 -      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   7.777 -      val (tm1,tm2) = Thm.dest_comb(concl th1)
   7.778 -      val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   7.779 -  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   7.780 -  end;
   7.781 -
   7.782 -(* Conversion from HOL term.                                                 *)
   7.783 -
   7.784 -fun polynomial_conv tm =
   7.785 - if is_semiring_constant tm then semiring_add_conv tm
   7.786 - else if not(is_comb tm) then reflexive tm
   7.787 - else
   7.788 -  let val (lopr,r) = Thm.dest_comb tm
   7.789 -  in if lopr aconvc neg_tm then
   7.790 -       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   7.791 -       in transitive th1 (polynomial_neg_conv (concl th1))
   7.792 -       end
   7.793 -     else if lopr aconvc inverse_tm then
   7.794 -       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   7.795 -       in transitive th1 (semiring_mul_conv (concl th1))
   7.796 -       end
   7.797 -     else
   7.798 -       if not(is_comb lopr) then reflexive tm
   7.799 -       else
   7.800 -         let val (opr,l) = Thm.dest_comb lopr
   7.801 -         in if opr aconvc pow_tm andalso is_numeral r
   7.802 -            then
   7.803 -              let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   7.804 -              in transitive th1 (polynomial_pow_conv (concl th1))
   7.805 -              end
   7.806 -         else if opr aconvc divide_tm 
   7.807 -            then
   7.808 -              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   7.809 -                                        (polynomial_conv r)
   7.810 -                  val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
   7.811 -                              (Thm.rhs_of th1)
   7.812 -              in transitive th1 th2
   7.813 -              end
   7.814 -            else
   7.815 -              if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   7.816 -              then
   7.817 -               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   7.818 -                   val f = if opr aconvc add_tm then polynomial_add_conv
   7.819 -                      else if opr aconvc mul_tm then polynomial_mul_conv
   7.820 -                      else polynomial_sub_conv
   7.821 -               in transitive th1 (f (concl th1))
   7.822 -               end
   7.823 -              else reflexive tm
   7.824 -         end
   7.825 -  end;
   7.826 - in
   7.827 -   {main = polynomial_conv,
   7.828 -    add = polynomial_add_conv,
   7.829 -    mul = polynomial_mul_conv,
   7.830 -    pow = polynomial_pow_conv,
   7.831 -    neg = polynomial_neg_conv,
   7.832 -    sub = polynomial_sub_conv}
   7.833 - end
   7.834 -end;
   7.835 -
   7.836 -val nat_exp_ss =
   7.837 -  HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
   7.838 -    addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
   7.839 -
   7.840 -fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
   7.841 -
   7.842 -
   7.843 -(* various normalizing conversions *)
   7.844 -
   7.845 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   7.846 -                                     {conv, dest_const, mk_const, is_const}) ord =
   7.847 -  let
   7.848 -    val pow_conv =
   7.849 -      Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
   7.850 -      then_conv Simplifier.rewrite
   7.851 -        (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   7.852 -      then_conv conv ctxt
   7.853 -    val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
   7.854 -  in semiring_normalizers_conv vars semiring ring field dat ord end;
   7.855 -
   7.856 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
   7.857 - #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);
   7.858 -
   7.859 -fun semiring_normalize_wrapper ctxt data = 
   7.860 -  semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   7.861 -
   7.862 -fun semiring_normalize_ord_conv ctxt ord tm =
   7.863 -  (case match ctxt tm of
   7.864 -    NONE => reflexive tm
   7.865 -  | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   7.866 - 
   7.867 -fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   7.868 -
   7.869 -
   7.870 -(** Isar setup **)
   7.871 -
   7.872 -local
   7.873 -
   7.874 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   7.875 -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   7.876 -fun keyword3 k1 k2 k3 =
   7.877 -  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   7.878 -
   7.879 -val opsN = "ops";
   7.880 -val rulesN = "rules";
   7.881 -
   7.882 -val normN = "norm";
   7.883 -val constN = "const";
   7.884 -val delN = "del";
   7.885 -
   7.886 -val any_keyword =
   7.887 -  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   7.888 -  keyword2 ringN opsN || keyword2 ringN rulesN ||
   7.889 -  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   7.890 -  keyword2 idomN rulesN || keyword2 idealN rulesN;
   7.891 -
   7.892 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   7.893 -val terms = thms >> map Drule.dest_term;
   7.894 -
   7.895 -fun optional scan = Scan.optional scan [];
   7.896 -
   7.897 -in
   7.898 -
   7.899 -val setup =
   7.900 -  Attrib.setup @{binding normalizer}
   7.901 -    (Scan.lift (Args.$$$ delN >> K del) ||
   7.902 -      ((keyword2 semiringN opsN |-- terms) --
   7.903 -       (keyword2 semiringN rulesN |-- thms)) --
   7.904 -      (optional (keyword2 ringN opsN |-- terms) --
   7.905 -       optional (keyword2 ringN rulesN |-- thms)) --
   7.906 -      (optional (keyword2 fieldN opsN |-- terms) --
   7.907 -       optional (keyword2 fieldN rulesN |-- thms)) --
   7.908 -      optional (keyword2 idomN rulesN |-- thms) --
   7.909 -      optional (keyword2 idealN rulesN |-- thms)
   7.910 -      >> (fn ((((sr, r), f), id), idl) => 
   7.911 -             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   7.912 -    "semiring normalizer data";
   7.913 -
   7.914 -end;
   7.915 -
   7.916 -end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Fri May 07 16:12:26 2010 +0200
     8.3 @@ -0,0 +1,909 @@
     8.4 +(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
     8.5 +    Author:     Amine Chaieb, TU Muenchen
     8.6 +
     8.7 +Normalization of expressions in semirings.
     8.8 +*)
     8.9 +
    8.10 +signature SEMIRING_NORMALIZER = 
    8.11 +sig
    8.12 +  type entry
    8.13 +  val get: Proof.context -> (thm * entry) list
    8.14 +  val match: Proof.context -> cterm -> entry option
    8.15 +  val del: attribute
    8.16 +  val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
    8.17 +    field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
    8.18 +  val funs: thm -> {is_const: morphism -> cterm -> bool,
    8.19 +    dest_const: morphism -> cterm -> Rat.rat,
    8.20 +    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
    8.21 +    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
    8.22 +  val semiring_funs: thm -> declaration
    8.23 +  val field_funs: thm -> declaration
    8.24 +
    8.25 +  val semiring_normalize_conv: Proof.context -> conv
    8.26 +  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
    8.27 +  val semiring_normalize_wrapper: Proof.context -> entry -> conv
    8.28 +  val semiring_normalize_ord_wrapper: Proof.context -> entry
    8.29 +    -> (cterm -> cterm -> bool) -> conv
    8.30 +  val semiring_normalizers_conv: cterm list -> cterm list * thm list
    8.31 +    -> cterm list * thm list -> cterm list * thm list ->
    8.32 +      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
    8.33 +        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    8.34 +  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
    8.35 +    (cterm -> cterm -> bool) ->
    8.36 +      {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
    8.37 +
    8.38 +  val setup: theory -> theory
    8.39 +end
    8.40 +
    8.41 +structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
    8.42 +struct
    8.43 +
    8.44 +(** data **)
    8.45 +
    8.46 +type entry =
    8.47 + {vars: cterm list,
    8.48 +  semiring: cterm list * thm list,
    8.49 +  ring: cterm list * thm list,
    8.50 +  field: cterm list * thm list,
    8.51 +  idom: thm list,
    8.52 +  ideal: thm list} *
    8.53 + {is_const: cterm -> bool,
    8.54 +  dest_const: cterm -> Rat.rat,
    8.55 +  mk_const: ctyp -> Rat.rat -> cterm,
    8.56 +  conv: Proof.context -> cterm -> thm};
    8.57 +
    8.58 +structure Data = Generic_Data
    8.59 +(
    8.60 +  type T = (thm * entry) list;
    8.61 +  val empty = [];
    8.62 +  val extend = I;
    8.63 +  val merge = AList.merge Thm.eq_thm (K true);
    8.64 +);
    8.65 +
    8.66 +val get = Data.get o Context.Proof;
    8.67 +
    8.68 +fun match ctxt tm =
    8.69 +  let
    8.70 +    fun match_inst
    8.71 +        ({vars, semiring = (sr_ops, sr_rules), 
    8.72 +          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
    8.73 +         fns as {is_const, dest_const, mk_const, conv}) pat =
    8.74 +       let
    8.75 +        fun h instT =
    8.76 +          let
    8.77 +            val substT = Thm.instantiate (instT, []);
    8.78 +            val substT_cterm = Drule.cterm_rule substT;
    8.79 +
    8.80 +            val vars' = map substT_cterm vars;
    8.81 +            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
    8.82 +            val ring' = (map substT_cterm r_ops, map substT r_rules);
    8.83 +            val field' = (map substT_cterm f_ops, map substT f_rules);
    8.84 +            val idom' = map substT idom;
    8.85 +            val ideal' = map substT ideal;
    8.86 +
    8.87 +            val result = ({vars = vars', semiring = semiring', 
    8.88 +                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
    8.89 +          in SOME result end
    8.90 +      in (case try Thm.match (pat, tm) of
    8.91 +           NONE => NONE
    8.92 +         | SOME (instT, _) => h instT)
    8.93 +      end;
    8.94 +
    8.95 +    fun match_struct (_,
    8.96 +        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
    8.97 +      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
    8.98 +  in get_first match_struct (get ctxt) end;
    8.99 +
   8.100 +
   8.101 +(* logical content *)
   8.102 +
   8.103 +val semiringN = "semiring";
   8.104 +val ringN = "ring";
   8.105 +val idomN = "idom";
   8.106 +val idealN = "ideal";
   8.107 +val fieldN = "field";
   8.108 +
   8.109 +fun undefined _ = raise Match;
   8.110 +
   8.111 +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
   8.112 +
   8.113 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   8.114 +         field = (f_ops, f_rules), idom, ideal} =
   8.115 +  Thm.declaration_attribute (fn key => fn context => context |> Data.map
   8.116 +    let
   8.117 +      val ctxt = Context.proof_of context;
   8.118 +
   8.119 +      fun check kind name xs n =
   8.120 +        null xs orelse length xs = n orelse
   8.121 +        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
   8.122 +      val check_ops = check "operations";
   8.123 +      val check_rules = check "rules";
   8.124 +
   8.125 +      val _ =
   8.126 +        check_ops semiringN sr_ops 5 andalso
   8.127 +        check_rules semiringN sr_rules 37 andalso
   8.128 +        check_ops ringN r_ops 2 andalso
   8.129 +        check_rules ringN r_rules 2 andalso
   8.130 +        check_ops fieldN f_ops 2 andalso
   8.131 +        check_rules fieldN f_rules 2 andalso
   8.132 +        check_rules idomN idom 2;
   8.133 +
   8.134 +      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
   8.135 +      val sr_rules' = map mk_meta sr_rules;
   8.136 +      val r_rules' = map mk_meta r_rules;
   8.137 +      val f_rules' = map mk_meta f_rules;
   8.138 +
   8.139 +      fun rule i = nth sr_rules' (i - 1);
   8.140 +
   8.141 +      val (cx, cy) = Thm.dest_binop (hd sr_ops);
   8.142 +      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.143 +      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   8.144 +      val ((clx, crx), (cly, cry)) =
   8.145 +        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.146 +      val ((ca, cb), (cc, cd)) =
   8.147 +        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   8.148 +      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
   8.149 +      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
   8.150 +
   8.151 +      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
   8.152 +      val semiring = (sr_ops, sr_rules');
   8.153 +      val ring = (r_ops, r_rules');
   8.154 +      val field = (f_ops, f_rules');
   8.155 +      val ideal' = map (symmetric o mk_meta) ideal
   8.156 +    in
   8.157 +      AList.delete Thm.eq_thm key #>
   8.158 +      cons (key, ({vars = vars, semiring = semiring, 
   8.159 +                          ring = ring, field = field, idom = idom, ideal = ideal'},
   8.160 +             {is_const = undefined, dest_const = undefined, mk_const = undefined,
   8.161 +             conv = undefined}))
   8.162 +    end);
   8.163 +
   8.164 +
   8.165 +(* extra-logical functions *)
   8.166 +
   8.167 +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
   8.168 + Data.map (fn data =>
   8.169 +  let
   8.170 +    val key = Morphism.thm phi raw_key;
   8.171 +    val _ = AList.defined Thm.eq_thm data key orelse
   8.172 +      raise THM ("No data entry for structure key", 0, [key]);
   8.173 +    val fns = {is_const = is_const phi, dest_const = dest_const phi,
   8.174 +      mk_const = mk_const phi, conv = conv phi};
   8.175 +  in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
   8.176 +
   8.177 +fun semiring_funs key = funs key
   8.178 +   {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
   8.179 +    dest_const = fn phi => fn ct =>
   8.180 +      Rat.rat_of_int (snd
   8.181 +        (HOLogic.dest_number (Thm.term_of ct)
   8.182 +          handle TERM _ => error "ring_dest_const")),
   8.183 +    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
   8.184 +      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
   8.185 +    conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
   8.186 +      then_conv Simplifier.rewrite (HOL_basic_ss addsimps
   8.187 +        (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
   8.188 +
   8.189 +fun field_funs key =
   8.190 +  let
   8.191 +    fun numeral_is_const ct =
   8.192 +      case term_of ct of
   8.193 +       Const (@{const_name Rings.divide},_) $ a $ b =>
   8.194 +         can HOLogic.dest_number a andalso can HOLogic.dest_number b
   8.195 +     | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   8.196 +     | t => can HOLogic.dest_number t
   8.197 +    fun dest_const ct = ((case term_of ct of
   8.198 +       Const (@{const_name Rings.divide},_) $ a $ b=>
   8.199 +        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   8.200 +     | Const (@{const_name Rings.inverse},_)$t => 
   8.201 +                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   8.202 +     | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   8.203 +       handle TERM _ => error "ring_dest_const")
   8.204 +    fun mk_const phi cT x =
   8.205 +      let val (a, b) = Rat.quotient_of_rat x
   8.206 +      in if b = 1 then Numeral.mk_cnumber cT a
   8.207 +        else Thm.capply
   8.208 +             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   8.209 +                         (Numeral.mk_cnumber cT a))
   8.210 +             (Numeral.mk_cnumber cT b)
   8.211 +      end
   8.212 +  in funs key
   8.213 +     {is_const = K numeral_is_const,
   8.214 +      dest_const = K dest_const,
   8.215 +      mk_const = mk_const,
   8.216 +      conv = K (K Numeral_Simprocs.field_comp_conv)}
   8.217 +  end;
   8.218 +
   8.219 +
   8.220 +
   8.221 +(** auxiliary **)
   8.222 +
   8.223 +fun is_comb ct =
   8.224 +  (case Thm.term_of ct of
   8.225 +    _ $ _ => true
   8.226 +  | _ => false);
   8.227 +
   8.228 +val concl = Thm.cprop_of #> Thm.dest_arg;
   8.229 +
   8.230 +fun is_binop ct ct' =
   8.231 +  (case Thm.term_of ct' of
   8.232 +    c $ _ $ _ => term_of ct aconv c
   8.233 +  | _ => false);
   8.234 +
   8.235 +fun dest_binop ct ct' =
   8.236 +  if is_binop ct ct' then Thm.dest_binop ct'
   8.237 +  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
   8.238 +
   8.239 +fun inst_thm inst = Thm.instantiate ([], inst);
   8.240 +
   8.241 +val dest_numeral = term_of #> HOLogic.dest_number #> snd;
   8.242 +val is_numeral = can dest_numeral;
   8.243 +
   8.244 +val numeral01_conv = Simplifier.rewrite
   8.245 +                         (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
   8.246 +val zero1_numeral_conv = 
   8.247 + Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
   8.248 +fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
   8.249 +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   8.250 +                @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 
   8.251 +                @{thm "less_nat_number_of"}];
   8.252 +
   8.253 +val nat_add_conv = 
   8.254 + zerone_conv 
   8.255 +  (Simplifier.rewrite 
   8.256 +    (HOL_basic_ss 
   8.257 +       addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
   8.258 +             @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
   8.259 +                 @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
   8.260 +             @ map (fn th => th RS sym) @{thms numerals}));
   8.261 +
   8.262 +val zeron_tm = @{cterm "0::nat"};
   8.263 +val onen_tm  = @{cterm "1::nat"};
   8.264 +val true_tm = @{cterm "True"};
   8.265 +
   8.266 +
   8.267 +(** normalizing conversions **)
   8.268 +
   8.269 +(* core conversion *)
   8.270 +
   8.271 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
   8.272 +  (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
   8.273 +let
   8.274 +
   8.275 +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
   8.276 +     pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
   8.277 +     pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
   8.278 +     pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
   8.279 +     pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
   8.280 +
   8.281 +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
   8.282 +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   8.283 +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
   8.284 +
   8.285 +val dest_add = dest_binop add_tm
   8.286 +val dest_mul = dest_binop mul_tm
   8.287 +fun dest_pow tm =
   8.288 + let val (l,r) = dest_binop pow_tm tm
   8.289 + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
   8.290 + end;
   8.291 +val is_add = is_binop add_tm
   8.292 +val is_mul = is_binop mul_tm
   8.293 +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
   8.294 +
   8.295 +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
   8.296 +  (case (r_ops, r_rules) of
   8.297 +    ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
   8.298 +      let
   8.299 +        val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   8.300 +        val neg_tm = Thm.dest_fun neg_pat
   8.301 +        val dest_sub = dest_binop sub_tm
   8.302 +        val is_sub = is_binop sub_tm
   8.303 +      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
   8.304 +          sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   8.305 +      end
   8.306 +    | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
   8.307 +
   8.308 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 
   8.309 +  (case (f_ops, f_rules) of 
   8.310 +   ([divide_pat, inverse_pat], [div_inv, inv_div]) => 
   8.311 +     let val div_tm = funpow 2 Thm.dest_fun divide_pat
   8.312 +         val inv_tm = Thm.dest_fun inverse_pat
   8.313 +     in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
   8.314 +     end
   8.315 +   | _ => (TrueI, TrueI, true_tm, true_tm, K false));
   8.316 +
   8.317 +in fn variable_order =>
   8.318 + let
   8.319 +
   8.320 +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
   8.321 +(* Also deals with "const * const", but both terms must involve powers of    *)
   8.322 +(* the same variable, or both be constants, or behaviour may be incorrect.   *)
   8.323 +
   8.324 + fun powvar_mul_conv tm =
   8.325 +  let
   8.326 +  val (l,r) = dest_mul tm
   8.327 +  in if is_semiring_constant l andalso is_semiring_constant r
   8.328 +     then semiring_mul_conv tm
   8.329 +     else
   8.330 +      ((let
   8.331 +         val (lx,ln) = dest_pow l
   8.332 +        in
   8.333 +         ((let val (rx,rn) = dest_pow r
   8.334 +               val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
   8.335 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   8.336 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   8.337 +           handle CTERM _ =>
   8.338 +            (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
   8.339 +                 val (tm1,tm2) = Thm.dest_comb(concl th1) in
   8.340 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
   8.341 +       handle CTERM _ =>
   8.342 +           ((let val (rx,rn) = dest_pow r
   8.343 +                val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
   8.344 +                val (tm1,tm2) = Thm.dest_comb(concl th1) in
   8.345 +               transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
   8.346 +           handle CTERM _ => inst_thm [(cx,l)] pthm_32
   8.347 +
   8.348 +))
   8.349 + end;
   8.350 +
   8.351 +(* Remove "1 * m" from a monomial, and just leave m.                         *)
   8.352 +
   8.353 + fun monomial_deone th =
   8.354 +       (let val (l,r) = dest_mul(concl th) in
   8.355 +           if l aconvc one_tm
   8.356 +          then transitive th (inst_thm [(ca,r)] pthm_13)  else th end)
   8.357 +       handle CTERM _ => th;
   8.358 +
   8.359 +(* Conversion for "(monomial)^n", where n is a numeral.                      *)
   8.360 +
   8.361 + val monomial_pow_conv =
   8.362 +  let
   8.363 +   fun monomial_pow tm bod ntm =
   8.364 +    if not(is_comb bod)
   8.365 +    then reflexive tm
   8.366 +    else
   8.367 +     if is_semiring_constant bod
   8.368 +     then semiring_pow_conv tm
   8.369 +     else
   8.370 +      let
   8.371 +      val (lopr,r) = Thm.dest_comb bod
   8.372 +      in if not(is_comb lopr)
   8.373 +         then reflexive tm
   8.374 +        else
   8.375 +          let
   8.376 +          val (opr,l) = Thm.dest_comb lopr
   8.377 +         in
   8.378 +           if opr aconvc pow_tm andalso is_numeral r
   8.379 +          then
   8.380 +            let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
   8.381 +                val (l,r) = Thm.dest_comb(concl th1)
   8.382 +           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
   8.383 +           end
   8.384 +           else
   8.385 +            if opr aconvc mul_tm
   8.386 +            then
   8.387 +             let
   8.388 +              val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
   8.389 +             val (xy,z) = Thm.dest_comb(concl th1)
   8.390 +              val (x,y) = Thm.dest_comb xy
   8.391 +              val thl = monomial_pow y l ntm
   8.392 +              val thr = monomial_pow z r ntm
   8.393 +             in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
   8.394 +             end
   8.395 +             else reflexive tm
   8.396 +          end
   8.397 +      end
   8.398 +  in fn tm =>
   8.399 +   let
   8.400 +    val (lopr,r) = Thm.dest_comb tm
   8.401 +    val (opr,l) = Thm.dest_comb lopr
   8.402 +   in if not (opr aconvc pow_tm) orelse not(is_numeral r)
   8.403 +      then raise CTERM ("monomial_pow_conv", [tm])
   8.404 +      else if r aconvc zeron_tm
   8.405 +      then inst_thm [(cx,l)] pthm_35
   8.406 +      else if r aconvc onen_tm
   8.407 +      then inst_thm [(cx,l)] pthm_36
   8.408 +      else monomial_deone(monomial_pow tm l r)
   8.409 +   end
   8.410 +  end;
   8.411 +
   8.412 +(* Multiplication of canonical monomials.                                    *)
   8.413 + val monomial_mul_conv =
   8.414 +  let
   8.415 +   fun powvar tm =
   8.416 +    if is_semiring_constant tm then one_tm
   8.417 +    else
   8.418 +     ((let val (lopr,r) = Thm.dest_comb tm
   8.419 +           val (opr,l) = Thm.dest_comb lopr
   8.420 +       in if opr aconvc pow_tm andalso is_numeral r then l 
   8.421 +          else raise CTERM ("monomial_mul_conv",[tm]) end)
   8.422 +     handle CTERM _ => tm)   (* FIXME !? *)
   8.423 +   fun  vorder x y =
   8.424 +    if x aconvc y then 0
   8.425 +    else
   8.426 +     if x aconvc one_tm then ~1
   8.427 +     else if y aconvc one_tm then 1
   8.428 +      else if variable_order x y then ~1 else 1
   8.429 +   fun monomial_mul tm l r =
   8.430 +    ((let val (lx,ly) = dest_mul l val vl = powvar lx
   8.431 +      in
   8.432 +      ((let
   8.433 +        val (rx,ry) = dest_mul r
   8.434 +         val vr = powvar rx
   8.435 +         val ord = vorder vl vr
   8.436 +        in
   8.437 +         if ord = 0
   8.438 +        then
   8.439 +          let
   8.440 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
   8.441 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.442 +             val (tm3,tm4) = Thm.dest_comb tm1
   8.443 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   8.444 +             val th3 = transitive th1 th2
   8.445 +              val  (tm5,tm6) = Thm.dest_comb(concl th3)
   8.446 +              val  (tm7,tm8) = Thm.dest_comb tm6
   8.447 +             val  th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
   8.448 +         in  transitive th3 (Drule.arg_cong_rule tm5 th4)
   8.449 +         end
   8.450 +         else
   8.451 +          let val th0 = if ord < 0 then pthm_16 else pthm_17
   8.452 +             val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
   8.453 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.454 +             val (tm3,tm4) = Thm.dest_comb tm2
   8.455 +         in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   8.456 +         end
   8.457 +        end)
   8.458 +       handle CTERM _ =>
   8.459 +        (let val vr = powvar r val ord = vorder vl vr
   8.460 +        in
   8.461 +          if ord = 0 then
   8.462 +           let
   8.463 +           val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
   8.464 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.465 +           val (tm3,tm4) = Thm.dest_comb tm1
   8.466 +           val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
   8.467 +          in transitive th1 th2
   8.468 +          end
   8.469 +          else
   8.470 +          if ord < 0 then
   8.471 +            let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
   8.472 +                val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.473 +                val (tm3,tm4) = Thm.dest_comb tm2
   8.474 +           in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   8.475 +           end
   8.476 +           else inst_thm [(ca,l),(cb,r)] pthm_09
   8.477 +        end)) end)
   8.478 +     handle CTERM _ =>
   8.479 +      (let val vl = powvar l in
   8.480 +        ((let
   8.481 +          val (rx,ry) = dest_mul r
   8.482 +          val vr = powvar rx
   8.483 +           val ord = vorder vl vr
   8.484 +         in if ord = 0 then
   8.485 +              let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
   8.486 +                 val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.487 +                 val (tm3,tm4) = Thm.dest_comb tm1
   8.488 +             in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
   8.489 +             end
   8.490 +             else if ord > 0 then
   8.491 +                 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
   8.492 +                     val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.493 +                    val (tm3,tm4) = Thm.dest_comb tm2
   8.494 +                in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
   8.495 +                end
   8.496 +             else reflexive tm
   8.497 +         end)
   8.498 +        handle CTERM _ =>
   8.499 +          (let val vr = powvar r
   8.500 +               val  ord = vorder vl vr
   8.501 +          in if ord = 0 then powvar_mul_conv tm
   8.502 +              else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
   8.503 +              else reflexive tm
   8.504 +          end)) end))
   8.505 +  in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
   8.506 +             end
   8.507 +  end;
   8.508 +(* Multiplication by monomial of a polynomial.                               *)
   8.509 +
   8.510 + val polynomial_monomial_mul_conv =
   8.511 +  let
   8.512 +   fun pmm_conv tm =
   8.513 +    let val (l,r) = dest_mul tm
   8.514 +    in
   8.515 +    ((let val (y,z) = dest_add r
   8.516 +          val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
   8.517 +          val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.518 +          val (tm3,tm4) = Thm.dest_comb tm1
   8.519 +          val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
   8.520 +      in transitive th1 th2
   8.521 +      end)
   8.522 +     handle CTERM _ => monomial_mul_conv tm)
   8.523 +   end
   8.524 + in pmm_conv
   8.525 + end;
   8.526 +
   8.527 +(* Addition of two monomials identical except for constant multiples.        *)
   8.528 +
   8.529 +fun monomial_add_conv tm =
   8.530 + let val (l,r) = dest_add tm
   8.531 + in if is_semiring_constant l andalso is_semiring_constant r
   8.532 +    then semiring_add_conv tm
   8.533 +    else
   8.534 +     let val th1 =
   8.535 +           if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
   8.536 +           then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
   8.537 +                    inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
   8.538 +                else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
   8.539 +           else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
   8.540 +           then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
   8.541 +           else inst_thm [(cm,r)] pthm_05
   8.542 +         val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.543 +         val (tm3,tm4) = Thm.dest_comb tm1
   8.544 +         val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
   8.545 +         val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
   8.546 +         val tm5 = concl th3
   8.547 +      in
   8.548 +      if (Thm.dest_arg1 tm5) aconvc zero_tm
   8.549 +      then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
   8.550 +      else monomial_deone th3
   8.551 +     end
   8.552 + end;
   8.553 +
   8.554 +(* Ordering on monomials.                                                    *)
   8.555 +
   8.556 +fun striplist dest =
   8.557 + let fun strip x acc =
   8.558 +   ((let val (l,r) = dest x in
   8.559 +        strip l (strip r acc) end)
   8.560 +    handle CTERM _ => x::acc)    (* FIXME !? *)
   8.561 + in fn x => strip x []
   8.562 + end;
   8.563 +
   8.564 +
   8.565 +fun powervars tm =
   8.566 + let val ptms = striplist dest_mul tm
   8.567 + in if is_semiring_constant (hd ptms) then tl ptms else ptms
   8.568 + end;
   8.569 +val num_0 = 0;
   8.570 +val num_1 = 1;
   8.571 +fun dest_varpow tm =
   8.572 + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
   8.573 +   handle CTERM _ =>
   8.574 +   (tm,(if is_semiring_constant tm then num_0 else num_1)));
   8.575 +
   8.576 +val morder =
   8.577 + let fun lexorder l1 l2 =
   8.578 +  case (l1,l2) of
   8.579 +    ([],[]) => 0
   8.580 +  | (vps,[]) => ~1
   8.581 +  | ([],vps) => 1
   8.582 +  | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
   8.583 +     if variable_order x1 x2 then 1
   8.584 +     else if variable_order x2 x1 then ~1
   8.585 +     else if n1 < n2 then ~1
   8.586 +     else if n2 < n1 then 1
   8.587 +     else lexorder vs1 vs2
   8.588 + in fn tm1 => fn tm2 =>
   8.589 +  let val vdegs1 = map dest_varpow (powervars tm1)
   8.590 +      val vdegs2 = map dest_varpow (powervars tm2)
   8.591 +      val deg1 = fold (Integer.add o snd) vdegs1 num_0
   8.592 +      val deg2 = fold (Integer.add o snd) vdegs2 num_0
   8.593 +  in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
   8.594 +                            else lexorder vdegs1 vdegs2
   8.595 +  end
   8.596 + end;
   8.597 +
   8.598 +(* Addition of two polynomials.                                              *)
   8.599 +
   8.600 +val polynomial_add_conv =
   8.601 + let
   8.602 + fun dezero_rule th =
   8.603 +  let
   8.604 +   val tm = concl th
   8.605 +  in
   8.606 +   if not(is_add tm) then th else
   8.607 +   let val (lopr,r) = Thm.dest_comb tm
   8.608 +       val l = Thm.dest_arg lopr
   8.609 +   in
   8.610 +    if l aconvc zero_tm
   8.611 +    then transitive th (inst_thm [(ca,r)] pthm_07)   else
   8.612 +        if r aconvc zero_tm
   8.613 +        then transitive th (inst_thm [(ca,l)] pthm_08)  else th
   8.614 +   end
   8.615 +  end
   8.616 + fun padd tm =
   8.617 +  let
   8.618 +   val (l,r) = dest_add tm
   8.619 +  in
   8.620 +   if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
   8.621 +   else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
   8.622 +   else
   8.623 +    if is_add l
   8.624 +    then
   8.625 +     let val (a,b) = dest_add l
   8.626 +     in
   8.627 +     if is_add r then
   8.628 +      let val (c,d) = dest_add r
   8.629 +          val ord = morder a c
   8.630 +      in
   8.631 +       if ord = 0 then
   8.632 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
   8.633 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.634 +            val (tm3,tm4) = Thm.dest_comb tm1
   8.635 +            val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
   8.636 +        in dezero_rule (transitive th1 (combination th2 (padd tm2)))
   8.637 +        end
   8.638 +       else (* ord <> 0*)
   8.639 +        let val th1 =
   8.640 +                if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   8.641 +                else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   8.642 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.643 +        in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   8.644 +        end
   8.645 +      end
   8.646 +     else (* not (is_add r)*)
   8.647 +      let val ord = morder a r
   8.648 +      in
   8.649 +       if ord = 0 then
   8.650 +        let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
   8.651 +            val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.652 +            val (tm3,tm4) = Thm.dest_comb tm1
   8.653 +            val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   8.654 +        in dezero_rule (transitive th1 th2)
   8.655 +        end
   8.656 +       else (* ord <> 0*)
   8.657 +        if ord > 0 then
   8.658 +          let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
   8.659 +              val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.660 +          in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   8.661 +          end
   8.662 +        else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   8.663 +      end
   8.664 +    end
   8.665 +   else (* not (is_add l)*)
   8.666 +    if is_add r then
   8.667 +      let val (c,d) = dest_add r
   8.668 +          val  ord = morder l c
   8.669 +      in
   8.670 +       if ord = 0 then
   8.671 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
   8.672 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.673 +             val (tm3,tm4) = Thm.dest_comb tm1
   8.674 +             val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
   8.675 +         in dezero_rule (transitive th1 th2)
   8.676 +         end
   8.677 +       else
   8.678 +        if ord > 0 then reflexive tm
   8.679 +        else
   8.680 +         let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
   8.681 +             val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.682 +         in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
   8.683 +         end
   8.684 +      end
   8.685 +    else
   8.686 +     let val ord = morder l r
   8.687 +     in
   8.688 +      if ord = 0 then monomial_add_conv tm
   8.689 +      else if ord > 0 then dezero_rule(reflexive tm)
   8.690 +      else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
   8.691 +     end
   8.692 +  end
   8.693 + in padd
   8.694 + end;
   8.695 +
   8.696 +(* Multiplication of two polynomials.                                        *)
   8.697 +
   8.698 +val polynomial_mul_conv =
   8.699 + let
   8.700 +  fun pmul tm =
   8.701 +   let val (l,r) = dest_mul tm
   8.702 +   in
   8.703 +    if not(is_add l) then polynomial_monomial_mul_conv tm
   8.704 +    else
   8.705 +     if not(is_add r) then
   8.706 +      let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
   8.707 +      in transitive th1 (polynomial_monomial_mul_conv(concl th1))
   8.708 +      end
   8.709 +     else
   8.710 +       let val (a,b) = dest_add l
   8.711 +           val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
   8.712 +           val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.713 +           val (tm3,tm4) = Thm.dest_comb tm1
   8.714 +           val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
   8.715 +           val th3 = transitive th1 (combination th2 (pmul tm2))
   8.716 +       in transitive th3 (polynomial_add_conv (concl th3))
   8.717 +       end
   8.718 +   end
   8.719 + in fn tm =>
   8.720 +   let val (l,r) = dest_mul tm
   8.721 +   in
   8.722 +    if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
   8.723 +    else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
   8.724 +    else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
   8.725 +    else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
   8.726 +    else pmul tm
   8.727 +   end
   8.728 + end;
   8.729 +
   8.730 +(* Power of polynomial (optimized for the monomial and trivial cases).       *)
   8.731 +
   8.732 +fun num_conv n =
   8.733 +  nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   8.734 +  |> Thm.symmetric;
   8.735 +
   8.736 +
   8.737 +val polynomial_pow_conv =
   8.738 + let
   8.739 +  fun ppow tm =
   8.740 +    let val (l,n) = dest_pow tm
   8.741 +    in
   8.742 +     if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
   8.743 +     else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
   8.744 +     else
   8.745 +         let val th1 = num_conv n
   8.746 +             val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
   8.747 +             val (tm1,tm2) = Thm.dest_comb(concl th2)
   8.748 +             val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
   8.749 +             val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
   8.750 +         in transitive th4 (polynomial_mul_conv (concl th4))
   8.751 +         end
   8.752 +    end
   8.753 + in fn tm =>
   8.754 +       if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
   8.755 + end;
   8.756 +
   8.757 +(* Negation.                                                                 *)
   8.758 +
   8.759 +fun polynomial_neg_conv tm =
   8.760 +   let val (l,r) = Thm.dest_comb tm in
   8.761 +        if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   8.762 +        let val th1 = inst_thm [(cx',r)] neg_mul
   8.763 +            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   8.764 +        in transitive th2 (polynomial_monomial_mul_conv (concl th2))
   8.765 +        end
   8.766 +   end;
   8.767 +
   8.768 +
   8.769 +(* Subtraction.                                                              *)
   8.770 +fun polynomial_sub_conv tm =
   8.771 +  let val (l,r) = dest_sub tm
   8.772 +      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   8.773 +      val (tm1,tm2) = Thm.dest_comb(concl th1)
   8.774 +      val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
   8.775 +  in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
   8.776 +  end;
   8.777 +
   8.778 +(* Conversion from HOL term.                                                 *)
   8.779 +
   8.780 +fun polynomial_conv tm =
   8.781 + if is_semiring_constant tm then semiring_add_conv tm
   8.782 + else if not(is_comb tm) then reflexive tm
   8.783 + else
   8.784 +  let val (lopr,r) = Thm.dest_comb tm
   8.785 +  in if lopr aconvc neg_tm then
   8.786 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   8.787 +       in transitive th1 (polynomial_neg_conv (concl th1))
   8.788 +       end
   8.789 +     else if lopr aconvc inverse_tm then
   8.790 +       let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
   8.791 +       in transitive th1 (semiring_mul_conv (concl th1))
   8.792 +       end
   8.793 +     else
   8.794 +       if not(is_comb lopr) then reflexive tm
   8.795 +       else
   8.796 +         let val (opr,l) = Thm.dest_comb lopr
   8.797 +         in if opr aconvc pow_tm andalso is_numeral r
   8.798 +            then
   8.799 +              let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
   8.800 +              in transitive th1 (polynomial_pow_conv (concl th1))
   8.801 +              end
   8.802 +         else if opr aconvc divide_tm 
   8.803 +            then
   8.804 +              let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
   8.805 +                                        (polynomial_conv r)
   8.806 +                  val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
   8.807 +                              (Thm.rhs_of th1)
   8.808 +              in transitive th1 th2
   8.809 +              end
   8.810 +            else
   8.811 +              if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
   8.812 +              then
   8.813 +               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
   8.814 +                   val f = if opr aconvc add_tm then polynomial_add_conv
   8.815 +                      else if opr aconvc mul_tm then polynomial_mul_conv
   8.816 +                      else polynomial_sub_conv
   8.817 +               in transitive th1 (f (concl th1))
   8.818 +               end
   8.819 +              else reflexive tm
   8.820 +         end
   8.821 +  end;
   8.822 + in
   8.823 +   {main = polynomial_conv,
   8.824 +    add = polynomial_add_conv,
   8.825 +    mul = polynomial_mul_conv,
   8.826 +    pow = polynomial_pow_conv,
   8.827 +    neg = polynomial_neg_conv,
   8.828 +    sub = polynomial_sub_conv}
   8.829 + end
   8.830 +end;
   8.831 +
   8.832 +val nat_exp_ss =
   8.833 +  HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
   8.834 +    addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
   8.835 +
   8.836 +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
   8.837 +
   8.838 +
   8.839 +(* various normalizing conversions *)
   8.840 +
   8.841 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
   8.842 +                                     {conv, dest_const, mk_const, is_const}) ord =
   8.843 +  let
   8.844 +    val pow_conv =
   8.845 +      Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
   8.846 +      then_conv Simplifier.rewrite
   8.847 +        (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
   8.848 +      then_conv conv ctxt
   8.849 +    val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
   8.850 +  in semiring_normalizers_conv vars semiring ring field dat ord end;
   8.851 +
   8.852 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
   8.853 + #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);
   8.854 +
   8.855 +fun semiring_normalize_wrapper ctxt data = 
   8.856 +  semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
   8.857 +
   8.858 +fun semiring_normalize_ord_conv ctxt ord tm =
   8.859 +  (case match ctxt tm of
   8.860 +    NONE => reflexive tm
   8.861 +  | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
   8.862 + 
   8.863 +fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
   8.864 +
   8.865 +
   8.866 +(** Isar setup **)
   8.867 +
   8.868 +local
   8.869 +
   8.870 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   8.871 +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
   8.872 +fun keyword3 k1 k2 k3 =
   8.873 +  Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
   8.874 +
   8.875 +val opsN = "ops";
   8.876 +val rulesN = "rules";
   8.877 +
   8.878 +val normN = "norm";
   8.879 +val constN = "const";
   8.880 +val delN = "del";
   8.881 +
   8.882 +val any_keyword =
   8.883 +  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
   8.884 +  keyword2 ringN opsN || keyword2 ringN rulesN ||
   8.885 +  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
   8.886 +  keyword2 idomN rulesN || keyword2 idealN rulesN;
   8.887 +
   8.888 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   8.889 +val terms = thms >> map Drule.dest_term;
   8.890 +
   8.891 +fun optional scan = Scan.optional scan [];
   8.892 +
   8.893 +in
   8.894 +
   8.895 +val setup =
   8.896 +  Attrib.setup @{binding normalizer}
   8.897 +    (Scan.lift (Args.$$$ delN >> K del) ||
   8.898 +      ((keyword2 semiringN opsN |-- terms) --
   8.899 +       (keyword2 semiringN rulesN |-- thms)) --
   8.900 +      (optional (keyword2 ringN opsN |-- terms) --
   8.901 +       optional (keyword2 ringN rulesN |-- thms)) --
   8.902 +      (optional (keyword2 fieldN opsN |-- terms) --
   8.903 +       optional (keyword2 fieldN rulesN |-- thms)) --
   8.904 +      optional (keyword2 idomN rulesN |-- thms) --
   8.905 +      optional (keyword2 idealN rulesN |-- thms)
   8.906 +      >> (fn ((((sr, r), f), id), idl) => 
   8.907 +             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   8.908 +    "semiring normalizer data";
   8.909 +
   8.910 +end;
   8.911 +
   8.912 +end;
     9.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri May 07 16:12:25 2010 +0200
     9.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Fri May 07 16:12:26 2010 +0200
     9.3 @@ -14,21 +14,21 @@
     9.4    fixes x :: int
     9.5    shows "x ^ 3 = x ^ 3" 
     9.6    apply (tactic {* ALLGOALS (CONVERSION
     9.7 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
     9.8 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
     9.9    by (rule refl)
    9.10  
    9.11  lemma
    9.12    fixes x :: int
    9.13    shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))" 
    9.14    apply (tactic {* ALLGOALS (CONVERSION
    9.15 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
    9.16 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
    9.17    by (rule refl)
    9.18  
    9.19  schematic_lemma
    9.20    fixes x :: int
    9.21    shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
    9.22    apply (tactic {* ALLGOALS (CONVERSION
    9.23 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
    9.24 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
    9.25    by (rule refl)
    9.26  
    9.27  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"