author haftmann Fri, 07 May 2010 09:59:59 +0200 changeset 36726 47ba1770da8e parent 36696 1b69f78be286 (current diff) parent 36725 34c36a5cb808 (diff) child 36727 51e3b38a5e41 child 36728 ae397b810c8b child 36750 912080b2c449
merged
 src/HOL/Tools/Groebner_Basis/misc.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Groebner_Basis/normalizer_data.ML file | annotate | diff | comparison | revisions
```--- a/NEWS	Thu May 06 11:08:19 2010 -0700
+++ b/NEWS	Fri May 07 09:59:59 2010 +0200
@@ -140,6 +140,8 @@

*** HOL ***

+* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
+
* Theory 'Finite_Set': various folding_* locales facilitate the application
of the various fold combinators on finite sets.
```
```--- a/src/HOL/Fields.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Fields.thy	Fri May 07 09:59:59 2010 +0200
@@ -234,6 +234,18 @@
"1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
by (simp add: eq_commute [of 1])

+lemma times_divide_times_eq:
+  "(x / y) * (z / w) = (x * z) / (y * w)"
+  by simp
+
+  "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
+
+  "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
+
end

```
```--- a/src/HOL/Groebner_Basis.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Groebner_Basis.thy	Fri May 07 09:59:59 2010 +0200
@@ -5,20 +5,17 @@
header {* Semiring normalization and Groebner Bases *}

theory Groebner_Basis
-imports Numeral_Simprocs
+imports Numeral_Simprocs Nat_Transfer
uses
-  "Tools/Groebner_Basis/misc.ML"
-  "Tools/Groebner_Basis/normalizer_data.ML"
-  ("Tools/Groebner_Basis/normalizer.ML")
+  "Tools/Groebner_Basis/normalizer.ML"
("Tools/Groebner_Basis/groebner.ML")
begin

subsection {* Semiring normalization *}

-setup NormalizerData.setup
+setup Normalizer.setup

-
-locale gb_semiring =
+locale normalizing_semiring =
fixes add mul pwr r0 r1
@@ -59,9 +56,6 @@
thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
qed

-
-subsubsection {* Declaring the abstract theory *}
-
lemma semiring_ops:
shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
and "TERM r0" and "TERM r1" .
@@ -156,71 +150,21 @@
qed

-lemmas gb_semiring_axioms' =
-  gb_semiring_axioms [normalizer
+lemmas normalizing_semiring_axioms' =
+  normalizing_semiring_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules]

end

-interpretation class_semiring: gb_semiring
-    "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
-  proof qed (auto simp add: algebra_simps)
-
-lemmas nat_arith =
-  diff_nat_number_of
-  mult_nat_number_of
-  eq_nat_number_of
-  less_nat_number_of
-
-lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
-  by simp
-
-lemmas comp_arith =
-  Let_def arith_simps nat_arith rel_simps neg_simps if_False
-  numeral_1_eq_1[symmetric] Suc_eq_plus1
-  numeral_0_eq_0[symmetric] numerals[symmetric]
-  iszero_simps not_iszero_Numeral1
-
-lemmas semiring_norm = comp_arith
-
-ML {*
-local
-
-open Conv;
+sublocale comm_semiring_1
+  < normalizing!: normalizing_semiring plus times power zero one
+proof

-fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
-
-fun int_of_rat x =
-  (case Rat.quotient_of_rat x of (i, 1) => i
-  | _ => error "int_of_rat: bad int");
-
-val numeral_conv =
-  Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) then_conv
-    (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}));
-
-in
+declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}

-fun normalizer_funs key =
-  NormalizerData.funs key
-   {is_const = fn phi => numeral_is_const,
-    dest_const = fn phi => fn ct =>
-      Rat.rat_of_int (snd
-        (HOLogic.dest_number (Thm.term_of ct)
-          handle TERM _ => error "ring_dest_const")),
-    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT (int_of_rat x),
-    conv = fn phi => K numeral_conv}
-
-end
-*}
-
-declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
-
-
-locale gb_ring = gb_semiring +
+locale normalizing_ring = normalizing_semiring +
fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and neg :: "'a \<Rightarrow> 'a"
assumes neg_mul: "neg x = mul (neg r1) x"
@@ -231,8 +175,8 @@

-lemmas gb_ring_axioms' =
-  gb_ring_axioms [normalizer
+lemmas normalizing_ring_axioms' =
+  normalizing_ring_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
@@ -240,23 +184,14 @@

end

-
-interpretation class_ring: gb_ring "op +" "op *" "op ^"
-    "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
-  proof qed simp_all
-
-
-declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
+sublocale comm_ring_1
+  < normalizing!: normalizing_ring plus times power zero one minus uminus
+proof

-use "Tools/Groebner_Basis/normalizer.ML"
-
+declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}

-method_setup sring_norm = {*
-  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
-*} "semiring normalizer"
-
-
-locale gb_field = gb_ring +
+locale normalizing_field = normalizing_ring +
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and inverse:: "'a \<Rightarrow> 'a"
assumes divide_inverse: "divide x y = mul x (inverse y)"
@@ -267,8 +202,8 @@

lemmas field_rules = divide_inverse inverse_divide

-lemmas gb_field_axioms' =
-  gb_field_axioms [normalizer
+lemmas normalizing_field_axioms' =
+  normalizing_field_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
@@ -278,10 +213,7 @@

end

-
-subsection {* Groebner Bases *}
-
-locale semiringb = gb_semiring +
+locale normalizing_semiring_cancel = normalizing_semiring +
add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
@@ -313,22 +245,23 @@
qed

-declare gb_semiring_axioms' [normalizer del]
+declare normalizing_semiring_axioms' [normalizer del]

-lemmas semiringb_axioms' = semiringb_axioms [normalizer
-  semiring ops: semiring_ops
-  semiring rules: semiring_rules
+lemmas normalizing_semiring_cancel_axioms' =
+  normalizing_semiring_cancel_axioms [normalizer
+    semiring ops: semiring_ops
+    semiring rules: semiring_rules

end

-locale ringb = semiringb + gb_ring +
+locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring +
assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
begin

-declare gb_ring_axioms' [normalizer del]
+declare normalizing_ring_axioms' [normalizer del]

-lemmas ringb_axioms' = ringb_axioms [normalizer
+lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
@@ -338,33 +271,24 @@

end

-
-lemma no_zero_divirors_neq0:
-  assumes az: "(a::'a::no_zero_divisors) \<noteq> 0"
-    and ab: "a*b = 0" shows "b = 0"
-proof -
-  { assume bz: "b \<noteq> 0"
-    from no_zero_divisors [OF az bz] ab have False by blast }
-  thus "b = 0" by blast
-qed
+sublocale idom
+  < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
+proof
+  fix w x y z
+  show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
+  proof
+    assume "w * y + x * z = w * z + x * y"
+    then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps)
+    then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
+    then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
+    then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
+    then show "w = x \<or> y = z" by auto

-interpretation class_ringb: ringb
-  "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
-  fix w x y z ::"'a::{idom,number_ring}"
-  assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
-  hence ynz': "y - z \<noteq> 0" by simp
-  from p have "w * y + x* z - w*z - x*y = 0" by simp
-  hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps)
-  hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
-  with  no_zero_divirors_neq0 [OF ynz']
-  have "w - x = 0" by blast
-  thus "w = x"  by simp
-qed
+declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}

-declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
-
-interpretation natgb: semiringb
+interpretation normalizing_nat!: normalizing_semiring_cancel
"op +" "op *" "op ^" "0::nat" "1"
fix w x y z ::"nat"
@@ -386,14 +310,14 @@
thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
qed

-declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *}
+declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}

-locale fieldgb = ringb + gb_field
+locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
begin

-declare gb_field_axioms' [normalizer del]
+declare normalizing_field_axioms' [normalizer del]

-lemmas fieldgb_axioms' = fieldgb_axioms [normalizer
+lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
@@ -405,8 +329,18 @@

end

+sublocale field
+  < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse
+proof
+
+declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
+
+
+subsection {* Groebner Bases *}

lemmas bool_simps = simp_thms(1-34)
+
lemma dnf:
"(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
"(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
@@ -423,23 +357,16 @@
"P \<equiv> False \<Longrightarrow> \<not> P"
"\<not> P \<Longrightarrow> (P \<equiv> False)"
by auto
-use "Tools/Groebner_Basis/groebner.ML"

-method_setup algebra =
-{*
-let
- fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
- val delN = "del"
- val any_keyword = keyword addN || keyword delN
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-in
-  ((Scan.optional (keyword addN |-- thms) []) --
-   (Scan.optional (keyword delN |-- thms) [])) >>
-  (fn (add_ths, del_ths) => fn ctxt =>
-       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
-end
-*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
+ML {*
+structure Algebra_Simplification = Named_Thms(
+  val name = "algebra"
+  val description = "pre-simplification rules for algebraic methods"
+)
+*}
+
+setup Algebra_Simplification.setup
+
declare dvd_def[algebra]
declare dvd_eq_mod_eq_0[symmetric, algebra]
declare mod_div_trivial[algebra]
@@ -468,222 +395,9 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]

-subsection{* Groebner Bases for fields *}
-
-interpretation class_fieldgb:
-  fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
-
-lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp
-lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
-  by simp
-lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)"
-  by simp
-lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
-  by simp
-lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
-  by simp
-
-lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
-
-lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::field_inverse_zero) / y + z = (x + z*y) / y"
-lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::field_inverse_zero) / y = (x + z*y) / y"
-
-ML {*
-let open Conv
-in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
-end
-*}
-
-ML{*
-local
- val zr = @{cpat "0"}
- val zT = ctyp_of_term zr
- val geq = @{cpat "op ="}
- val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
-
- fun prove_nz ss T t =
-    let
-      val z = instantiate_cterm ([(zT,T)],[]) zr
-      val eq = instantiate_cterm ([(eqT,T)],[]) geq
-      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
-           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
-                  (Thm.capply (Thm.capply eq t) z)))
-    in equal_elim (symmetric th) TrueI
-    end
-
- fun proc phi ss ct =
-  let
-    val ((x,y),(w,z)) =
-         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
-    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
-    val T = ctyp_of_term x
-    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
-    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
-  in SOME (implies_elim (implies_elim th y_nz) z_nz)
-  end
-  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
-
- fun proc2 phi ss ct =
-  let
-    val (l,r) = Thm.dest_binop ct
-    val T = ctyp_of_term l
-  in (case (term_of l, term_of r) of
-      (Const(@{const_name Rings.divide},_)\$_\$_, _) =>
-        let val (x,y) = Thm.dest_binop l val z = r
-            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ss T y
-        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
-        end
-     | (_, Const (@{const_name Rings.divide},_)\$_\$_) =>
-        let val (x,y) = Thm.dest_binop r val z = l
-            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ss T y
-        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
-        end
-     | _ => NONE)
-  end
-  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
-
- fun is_number (Const(@{const_name Rings.divide},_)\$a\$b) = is_number a andalso is_number b
-   | is_number t = can HOLogic.dest_number t
-
- val is_number = is_number o term_of
+use "Tools/Groebner_Basis/groebner.ML"

- fun proc3 phi ss ct =
-  (case term_of ct of
-    Const(@{const_name Orderings.less},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
-      let
-        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
-      in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less_eq},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
-      let
-        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
-      in SOME (mk_meta_eq th) end
-  | Const("op =",_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
-      let
-        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
-      in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
-    let
-      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
-      in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less_eq},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
-    let
-      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
-      in SOME (mk_meta_eq th) end
-  | Const("op =",_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
-    let
-      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
-        val _ = map is_number [a,b,c]
-        val T = ctyp_of_term c
-        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
-      in SOME (mk_meta_eq th) end
-  | _ => NONE)
-  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
-
-       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
-                     proc = proc, identifier = []}
-
-       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
-                     proc = proc2, identifier = []}
-
-val ord_frac_simproc =
-  make_simproc
-    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
-             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
-             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
-             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
-             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
-             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
-             name = "ord_frac_simproc", proc = proc3, identifier = []}
-
-local
-open Conv
-in
-
-val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
-           @{thm "divide_Numeral1"},
-           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
-           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
-           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
-           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
-           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
-           @{thm "diff_def"}, @{thm "minus_divide_left"},
-           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
-           @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
-           fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
-           (@{thm field_divide_inverse} RS sym)]
-
-val comp_conv = (Simplifier.rewrite
-                            ord_frac_simproc]
-  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
-end
-
-fun numeral_is_const ct =
-  case term_of ct of
-   Const (@{const_name Rings.divide},_) \$ a \$ b =>
-     can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (@{const_name Rings.inverse},_)\$t => can HOLogic.dest_number t
- | t => can HOLogic.dest_number t
-
-fun dest_const ct = ((case term_of ct of
-   Const (@{const_name Rings.divide},_) \$ a \$ b=>
-    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (@{const_name Rings.inverse},_)\$t =>
-               Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
- | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
-   handle TERM _ => error "ring_dest_const")
-
-fun mk_const phi cT x =
- let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Numeral.mk_cnumber cT a
-    else Thm.capply
-         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
-                     (Numeral.mk_cnumber cT a))
-         (Numeral.mk_cnumber cT b)
-  end
-
-in
- val field_comp_conv = comp_conv;
- val fieldgb_declaration =
-  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
-   {is_const = K numeral_is_const,
-    dest_const = K dest_const,
-    mk_const = mk_const,
-    conv = K (K comp_conv)}
-end;
-*}
-
-declaration fieldgb_declaration
+method_setup algebra = Groebner.algebra_method
+  "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"

end```
```--- a/src/HOL/Int.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Int.thy	Fri May 07 09:59:59 2010 +0200
@@ -1063,20 +1063,24 @@

text {* First version by Norbert Voelker *}

-definition (*for simplifying equalities*)
-  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
-where
+definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
"iszero z \<longleftrightarrow> z = 0"

lemma iszero_0: "iszero 0"
-
-lemma not_iszero_1: "~ iszero 1"
+
+lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
+
+lemma not_iszero_1: "\<not> iszero 1"
+
+lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"

lemma eq_number_of_eq [simp]:
"((number_of x::'a::number_ring) = number_of y) =
-   iszero (number_of (x + uminus y) :: 'a)"
+     iszero (number_of (x + uminus y) :: 'a)"

@@ -2021,6 +2025,14 @@

lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]

+lemma divide_Numeral1:
+  "(x::'a::{field, number_ring}) / Numeral1 = x"
+  by simp
+
+lemma divide_Numeral0:
+  "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
+  by simp
+

subsection {* The divides relation *}
```
```--- a/src/HOL/IsaMakefile	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/IsaMakefile	Fri May 07 09:59:59 2010 +0200
@@ -284,9 +284,7 @@
Tools/ATP_Manager/atp_manager.ML \
Tools/ATP_Manager/atp_systems.ML \
Tools/Groebner_Basis/groebner.ML \
-  Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML \
-  Tools/Groebner_Basis/normalizer_data.ML \
Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/list_code.ML \```
```--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri May 07 09:59:59 2010 +0200
@@ -1195,7 +1195,7 @@
fun real_nonlinear_prover proof_method ctxt =
let
-      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
@@ -1222,7 +1222,7 @@
in
(let val th = tryfind trivial_axiom (keq @ klep @ kltp)
in
-    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial)
+    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial)
end)
handle Failure _ =>
(let val proof =
@@ -1310,7 +1310,7 @@
fun real_nonlinear_subst_prover prover ctxt =
let
-      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord

```--- a/src/HOL/Library/normarith.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Library/normarith.ML	Fri May 07 09:59:59 2010 +0200
@@ -167,8 +167,8 @@
(* FIXME : Should be computed statically!! *)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
-     (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
- in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
+     (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
+ in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv)))
end;

fun absc cv ct = case term_of ct of
@@ -190,8 +190,8 @@
val apply_pth5 = rewr_conv @{thm pth_5};
val apply_pth6 = rewr_conv @{thm pth_6};
val apply_pth7 = rewrs_conv @{thms pth_7};
- val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
- val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv);
+ val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
+ val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv);
val apply_ptha = rewr_conv @{thm pth_a};
val apply_pthb = rewrs_conv @{thms pth_b};
val apply_pthc = rewrs_conv @{thms pth_c};
@@ -204,7 +204,7 @@
| _ => error "headvector: non-canonical term"

fun vector_cmul_conv ct =
-   ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv
+   ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv
(apply_pth6 then_conv binop_conv vector_cmul_conv)) ct

fun vector_add_conv ct = apply_pth7 ct
@@ -278,7 +278,7 @@
(* FIXME: Should be computed statically!!*)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
-       (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+       (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
@@ -384,7 +384,7 @@
let
val real_poly_neg_conv = #neg
(Normalizer.semiring_normalizers_ord_wrapper ctxt
-        (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
+        (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
val (th1,th2) = conj_pair(rawrule th)
in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
end
@@ -396,7 +396,7 @@
fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
(HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
-   then_conv field_comp_conv
+   then_conv Normalizer.field_comp_conv
then_conv nnf_conv

fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);```
```--- a/src/HOL/Library/positivstellensatz.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Library/positivstellensatz.ML	Fri May 07 09:59:59 2010 +0200
@@ -748,10 +748,10 @@
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
Normalizer.semiring_normalizers_ord_wrapper ctxt
-      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
in gen_real_arith ctxt
-   (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
+   (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv,
end;
```
```--- a/src/HOL/Metis_Examples/BT.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Metis_Examples/BT.thy	Fri May 07 09:59:59 2010 +0200
@@ -88,7 +88,7 @@
case Lf thus ?case by (metis reflect.simps(1))
next
case (Br a t1 t2) thus ?case
-    by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+    by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
qed

declare [[ atp_problem_prefix = "BT__depth_reflect" ]]```
```--- a/src/HOL/Metis_Examples/BigO.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Metis_Examples/BigO.thy	Fri May 07 09:59:59 2010 +0200
@@ -41,7 +41,7 @@
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
-  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
@@ -70,7 +70,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
@@ -92,7 +92,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
@@ -111,7 +111,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
@@ -145,12 +145,12 @@
declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
lemma bigo_refl [intro]: "f : O(f)"
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)

declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
lemma bigo_zero: "0 : O(g)"
apply (auto simp add: bigo_def func_zero)
-by (metis class_semiring.mul_0 order_refl)
+by (metis normalizing.mul_0 order_refl)

lemma bigo_zero2: "O(%x.0) = {%x.0}"
@@ -307,7 +307,7 @@
apply (auto simp add: diff_minus fun_Compl_def func_plus)
prefer 2
apply (drule_tac x = x in spec)+
proof -
fix x :: 'a
assume "\<forall>x. lb x \<le> f x"
@@ -318,13 +318,13 @@
lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
apply (unfold bigo_def)
apply auto
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)

declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
lemma bigo_abs2: "f =o O(%x. abs(f x))"
apply (unfold bigo_def)
apply auto
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)

lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
proof -```
```--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 07 09:59:59 2010 +0200
@@ -1877,7 +1877,7 @@
using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
apply (rule mult_left_le_imp_le[of "1 - u"])
-      unfolding class_semiring.mul_a using `u<1` by auto
+      unfolding normalizing.mul_a using `u<1` by auto
thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
using as unfolding scaleR_scaleR by auto qed auto
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
@@ -2231,7 +2231,7 @@
apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
fix z assume z:"z\<in>{x - ?d..x + ?d}"
have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
-      by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
+      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption```
```--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri May 07 09:59:59 2010 +0200
@@ -698,7 +698,7 @@
unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
-    case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules)
+    case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
@@ -810,7 +810,7 @@
guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this
show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k"
hence "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)" using d' k by auto
-      also have "\<dots> \<le> e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`]
+      also have "\<dots> \<le> e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`]
using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps)
finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)" by simp qed(insert k, auto) qed qed
```
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 07 09:59:59 2010 +0200
@@ -2533,7 +2533,7 @@
show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
-        note this[unfolded real_scaleR_def real_norm_def class_semiring.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
+        note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \$ k - c\<bar> \<le> d})) < e"
apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
@@ -4723,7 +4723,7 @@
have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
\<longrightarrow> norm(ig) < dia + e"
proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
-      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
+      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
qed note norm=this[rule_format]```
```--- a/src/HOL/Nat_Numeral.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Nat_Numeral.thy	Fri May 07 09:59:59 2010 +0200
@@ -319,6 +319,10 @@
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"

+lemma Numeral1_eq1_nat:
+  "(1::nat) = Numeral1"
+  by simp
+
lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
by (simp only: nat_numeral_1_eq_1 One_nat_def)

@@ -687,6 +691,20 @@
lemmas nat_number' =
nat_number_of_Bit0 nat_number_of_Bit1

+lemmas nat_arith =
+  diff_nat_number_of
+  mult_nat_number_of
+  eq_nat_number_of
+  less_nat_number_of
+
+lemmas semiring_norm =
+  Let_def arith_simps nat_arith rel_simps neg_simps if_False
+  numeral_1_eq_1 [symmetric] Suc_eq_plus1
+  numeral_0_eq_0 [symmetric] numerals [symmetric]
+  iszero_simps not_iszero_Numeral1
+
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (fact Let_def)
```
```--- a/src/HOL/Parity.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Parity.thy	Fri May 07 09:59:59 2010 +0200
@@ -229,7 +229,7 @@
lemma zero_le_odd_power: "odd n ==>
(0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
-apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
+apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
done

lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =```
```--- a/src/HOL/Probability/Lebesgue.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Probability/Lebesgue.thy	Fri May 07 09:59:59 2010 +0200
@@ -938,17 +938,17 @@
proof safe
fix t assume t: "t \<in> space M"
{ fix m n :: nat assume "m \<le> n"
-      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
+      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
apply (subst *)
-        apply (subst class_semiring.mul_a)
+        apply (subst normalizing.mul_a)
apply (subst real_of_nat_le_iff)
apply (rule le_mult_natfloor)
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
apply (subst *)
-        apply (subst (3) class_semiring.mul_c)
-        apply (subst class_semiring.mul_a)
+        apply (subst (3) normalizing.mul_c)
+        apply (subst normalizing.mul_a)
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)```
```--- a/src/HOL/Rings.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Rings.thy	Fri May 07 09:59:59 2010 +0200
@@ -183,9 +183,21 @@

end

-
class no_zero_divisors = zero + times +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
+begin
+
+lemma divisors_zero:
+  assumes "a * b = 0"
+  shows "a = 0 \<or> b = 0"
+proof (rule classical)
+  assume "\<not> (a = 0 \<or> b = 0)"
+  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+  with no_zero_divisors have "a * b \<noteq> 0" by blast
+  with assms show ?thesis by simp
+qed
+
+end

class semiring_1_cancel = semiring + cancel_comm_monoid_add
+ zero_neq_one + monoid_mult```
```--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Fri May 07 09:59:59 2010 +0200
@@ -9,19 +9,20 @@
vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
(cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
conv ->  conv ->
- {ring_conv : conv,
- simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
- multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
- poly_eq_ss: simpset, unwind_conv : conv}
-    val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
-    val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
-    val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
+     {ring_conv : conv,
+     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
+     multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
+     poly_eq_ss: simpset, unwind_conv : conv}
+  val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val algebra_method: (Proof.context -> Method.method) context_parser
end

structure Groebner : GROEBNER =
struct

-open Conv Normalizer Drule Thm;
+open Conv Drule Thm;

fun is_comb ct =
(case Thm.term_of ct of
@@ -50,11 +51,11 @@
val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));

val (eqF_intr, eqF_elim) =
-  let val [th1,th2] = thms "PFalse"
+  let val [th1,th2] = @{thms PFalse}
in (fn th => th COMP th2, fn th => th COMP th1) end;

val (PFalse, PFalse') =
- let val PFalse_eq = nth (thms "simp_thms") 13
+ let val PFalse_eq = nth @{thms simp_thms} 13
in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;

@@ -398,7 +399,7 @@
compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
| _ => rfn tm ;

-val notnotD = @{thm "notnotD"};
+val notnotD = @{thm notnotD};
fun mk_binop ct x y = capply (capply ct x) y

val mk_comb = capply;
@@ -440,10 +441,10 @@
| _ => false;

val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
-val bool_simps = @{thms "bool_simps"};
-val nnf_simps = @{thms "nnf_simps"};
+val bool_simps = @{thms bool_simps};
+val nnf_simps = @{thms nnf_simps};
-val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms "weak_dnf_simps"});
+val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps});
val initial_conv =
Simplifier.rewrite
@@ -947,29 +948,31 @@
case try (find_term 0) form of
NONE => NONE
| SOME tm =>
-  (case NormalizerData.match ctxt tm of
+  (case Normalizer.match ctxt tm of
NONE => NONE
| SOME (res as (theory, {is_const, dest_const,
mk_const, conv = ring_eq_conv})) =>
SOME (ring_and_ideal_conv theory
dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
-          (semiring_normalize_wrapper ctxt res)))
+          (Normalizer.semiring_normalize_wrapper ctxt res)))

fun ring_solve ctxt form =
(case try (find_term 0 (* FIXME !? *)) form of
NONE => reflexive form
| SOME tm =>
-      (case NormalizerData.match ctxt tm of
+      (case Normalizer.match ctxt tm of
NONE => reflexive form
| SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
#ring_conv (ring_and_ideal_conv theory
dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
-          (semiring_normalize_wrapper ctxt res)) form));
+          (Normalizer.semiring_normalize_wrapper ctxt res)) form));
+
+fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt

fun ring_tac add_ths del_ths ctxt =
Object_Logic.full_atomize_tac
-  THEN' asm_full_simp_tac
+  THEN' presimplify ctxt add_ths del_ths
THEN' CSUBGOAL (fn (p, i) =>
rtac (let val form = Object_Logic.dest_judgment p
in case get_ring_ideal_convs ctxt form of
@@ -988,8 +991,7 @@
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
in
fun ideal_tac add_ths del_ths ctxt =
-  asm_full_simp_tac
THEN'
CSUBGOAL (fn (p, i) =>
case get_ring_ideal_convs ctxt p of
@@ -1023,6 +1025,21 @@
fun algebra_tac add_ths del_ths ctxt i =

-
+local
+
+fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
+val delN = "del"
+val any_keyword = keyword addN || keyword delN
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+
+in
+
+val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
+   (Scan.optional (keyword delN |-- thms) [])) >>
+  (fn (add_ths, del_ths) => fn ctxt =>
+       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))

end;
+
+end;```
```--- a/src/HOL/Tools/Groebner_Basis/misc.ML	Thu May 06 11:08:19 2010 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      HOL/Tools/Groebner_Basis/misc.ML
-    ID:         \$Id\$
-    Author:     Amine Chaieb, TU Muenchen
-
-Very basic stuff for cterms.
-*)
-
-structure Misc =
-struct
-
-fun is_comb ct =
-  (case Thm.term_of ct of
-    _ \$ _ => true
-  | _ => false);
-
-val concl = Thm.cprop_of #> Thm.dest_arg;
-
-fun is_binop ct ct' =
-  (case Thm.term_of ct' of
-    c \$ _ \$ _ => term_of ct aconv c
-  | _ => false);
-
-fun dest_binop ct ct' =
-  if is_binop ct ct' then Thm.dest_binop ct'
-  else raise CTERM ("dest_binop: bad binop", [ct, ct'])
-
-fun inst_thm inst = Thm.instantiate ([], inst);
-
-end;```
```--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri May 07 09:59:59 2010 +0200
@@ -1,30 +1,376 @@
(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
Author:     Amine Chaieb, TU Muenchen
+
+Normalization of expressions in semirings.
*)

signature NORMALIZER =
sig
- val semiring_normalize_conv : Proof.context -> conv
- val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv
- val semiring_normalize_tac : Proof.context -> int -> tactic
- val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> conv
- val semiring_normalizers_ord_wrapper :
-     Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) ->
+  type entry
+  val get: Proof.context -> (thm * entry) list
+  val match: Proof.context -> cterm -> entry option
+  val del: attribute
+  val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
+    field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
+  val funs: thm -> {is_const: morphism -> cterm -> bool,
+    dest_const: morphism -> cterm -> Rat.rat,
+    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
+    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
+  val semiring_funs: thm -> declaration
+  val field_funs: thm -> declaration
+
+  val semiring_normalize_conv: Proof.context -> conv
+  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
+  val semiring_normalize_wrapper: Proof.context -> entry -> conv
+  val semiring_normalize_ord_wrapper: Proof.context -> entry
+    -> (cterm -> cterm -> bool) -> conv
+  val semiring_normalizers_conv: cterm list -> cterm list * thm list
+    -> cterm list * thm list -> cterm list * thm list ->
+      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
+        {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
+  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
+    (cterm -> cterm -> bool) ->
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
- val semiring_normalize_ord_wrapper :  Proof.context -> NormalizerData.entry ->
-   (cterm -> cterm -> bool) -> conv
- val semiring_normalizers_conv :
-     cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list ->
-     (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
-       {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
+  val field_comp_conv: conv
+
+  val setup: theory -> theory
end

structure Normalizer: NORMALIZER =
struct

-open Conv;
+(** some conversion **)
+
+local
+ val zr = @{cpat "0"}
+ val zT = ctyp_of_term zr
+ val geq = @{cpat "op ="}
+ val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
+
+ fun prove_nz ss T t =
+    let
+      val z = instantiate_cterm ([(zT,T)],[]) zr
+      val eq = instantiate_cterm ([(eqT,T)],[]) geq
+      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
+           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
+                  (Thm.capply (Thm.capply eq t) z)))
+    in equal_elim (symmetric th) TrueI
+    end
+
+ fun proc phi ss ct =
+  let
+    val ((x,y),(w,z)) =
+         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
+    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
+    val T = ctyp_of_term x
+    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
+    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
+  in SOME (implies_elim (implies_elim th y_nz) z_nz)
+  end
+  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
+
+ fun proc2 phi ss ct =
+  let
+    val (l,r) = Thm.dest_binop ct
+    val T = ctyp_of_term l
+  in (case (term_of l, term_of r) of
+      (Const(@{const_name Rings.divide},_)\$_\$_, _) =>
+        let val (x,y) = Thm.dest_binop l val z = r
+            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
+            val ynz = prove_nz ss T y
+        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
+        end
+     | (_, Const (@{const_name Rings.divide},_)\$_\$_) =>
+        let val (x,y) = Thm.dest_binop r val z = l
+            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
+            val ynz = prove_nz ss T y
+        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
+        end
+     | _ => NONE)
+  end
+  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
+
+ fun is_number (Const(@{const_name Rings.divide},_)\$a\$b) = is_number a andalso is_number b
+   | is_number t = can HOLogic.dest_number t
+
+ val is_number = is_number o term_of
+
+ fun proc3 phi ss ct =
+  (case term_of ct of
+    Const(@{const_name Orderings.less},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
+      let
+        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
+      in SOME (mk_meta_eq th) end
+  | Const(@{const_name Orderings.less_eq},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
+      let
+        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
+      in SOME (mk_meta_eq th) end
+  | Const("op =",_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
+      let
+        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
+      in SOME (mk_meta_eq th) end
+  | Const(@{const_name Orderings.less},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
+    let
+      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
+      in SOME (mk_meta_eq th) end
+  | Const(@{const_name Orderings.less_eq},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
+    let
+      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
+      in SOME (mk_meta_eq th) end
+  | Const("op =",_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
+    let
+      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
+        val _ = map is_number [a,b,c]
+        val T = ctyp_of_term c
+        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
+      in SOME (mk_meta_eq th) end
+  | _ => NONE)
+  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
+
+       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
+                     proc = proc, identifier = []}
+
+       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
+                     proc = proc2, identifier = []}
+
+val ord_frac_simproc =
+  make_simproc
+    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
+             @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"},
+             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
+             @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"},
+             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
+             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
+             name = "ord_frac_simproc", proc = proc3, identifier = []}
+
+val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
+           @{thm "divide_Numeral1"},
+           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
+           @{thm "divide_divide_eq_left"},
+           @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
+           @{thm "times_divide_times_eq"},
+           @{thm "divide_divide_eq_right"},
+           @{thm "diff_def"}, @{thm "minus_divide_left"},
+           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
+           @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
+           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))
+           (@{thm field_divide_inverse} RS sym)]
+
+in
+
+val field_comp_conv = (Simplifier.rewrite
+                            ord_frac_simproc]
+  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
+
+end
+
+
+(** data **)

-(* Very basic stuff for terms *)
+type entry =
+ {vars: cterm list,
+  semiring: cterm list * thm list,
+  ring: cterm list * thm list,
+  field: cterm list * thm list,
+  idom: thm list,
+  ideal: thm list} *
+ {is_const: cterm -> bool,
+  dest_const: cterm -> Rat.rat,
+  mk_const: ctyp -> Rat.rat -> cterm,
+  conv: Proof.context -> cterm -> thm};
+
+structure Data = Generic_Data
+(
+  type T = (thm * entry) list;
+  val empty = [];
+  val extend = I;
+  val merge = AList.merge Thm.eq_thm (K true);
+);
+
+val get = Data.get o Context.Proof;
+
+fun match ctxt tm =
+  let
+    fun match_inst
+        ({vars, semiring = (sr_ops, sr_rules),
+          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
+         fns as {is_const, dest_const, mk_const, conv}) pat =
+       let
+        fun h instT =
+          let
+            val substT = Thm.instantiate (instT, []);
+            val substT_cterm = Drule.cterm_rule substT;
+
+            val vars' = map substT_cterm vars;
+            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
+            val ring' = (map substT_cterm r_ops, map substT r_rules);
+            val field' = (map substT_cterm f_ops, map substT f_rules);
+            val idom' = map substT idom;
+            val ideal' = map substT ideal;
+
+            val result = ({vars = vars', semiring = semiring',
+                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
+          in SOME result end
+      in (case try Thm.match (pat, tm) of
+           NONE => NONE
+         | SOME (instT, _) => h instT)
+      end;
+
+    fun match_struct (_,
+        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
+      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
+  in get_first match_struct (get ctxt) end;
+
+
+(* logical content *)
+
+val semiringN = "semiring";
+val ringN = "ring";
+val idomN = "idom";
+val idealN = "ideal";
+val fieldN = "field";
+
+fun undefined _ = raise Match;
+
+val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
+
+fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
+         field = (f_ops, f_rules), idom, ideal} =
+  Thm.declaration_attribute (fn key => fn context => context |> Data.map
+    let
+      val ctxt = Context.proof_of context;
+
+      fun check kind name xs n =
+        null xs orelse length xs = n orelse
+        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
+      val check_ops = check "operations";
+      val check_rules = check "rules";
+
+      val _ =
+        check_ops semiringN sr_ops 5 andalso
+        check_rules semiringN sr_rules 37 andalso
+        check_ops ringN r_ops 2 andalso
+        check_rules ringN r_rules 2 andalso
+        check_ops fieldN f_ops 2 andalso
+        check_rules fieldN f_rules 2 andalso
+        check_rules idomN idom 2;
+
+      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
+      val sr_rules' = map mk_meta sr_rules;
+      val r_rules' = map mk_meta r_rules;
+      val f_rules' = map mk_meta f_rules;
+
+      fun rule i = nth sr_rules' (i - 1);
+
+      val (cx, cy) = Thm.dest_binop (hd sr_ops);
+      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
+      val ((clx, crx), (cly, cry)) =
+        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+      val ((ca, cb), (cc, cd)) =
+        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
+      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
+
+      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
+      val semiring = (sr_ops, sr_rules');
+      val ring = (r_ops, r_rules');
+      val field = (f_ops, f_rules');
+      val ideal' = map (symmetric o mk_meta) ideal
+    in
+      AList.delete Thm.eq_thm key #>
+      cons (key, ({vars = vars, semiring = semiring,
+                          ring = ring, field = field, idom = idom, ideal = ideal'},
+             {is_const = undefined, dest_const = undefined, mk_const = undefined,
+             conv = undefined}))
+    end);
+
+
+(* extra-logical functions *)
+
+fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
+ Data.map (fn data =>
+  let
+    val key = Morphism.thm phi raw_key;
+    val _ = AList.defined Thm.eq_thm data key orelse
+      raise THM ("No data entry for structure key", 0, [key]);
+    val fns = {is_const = is_const phi, dest_const = dest_const phi,
+      mk_const = mk_const phi, conv = conv phi};
+  in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
+
+fun semiring_funs key = funs key
+   {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
+    dest_const = fn phi => fn ct =>
+      Rat.rat_of_int (snd
+        (HOLogic.dest_number (Thm.term_of ct)
+          handle TERM _ => error "ring_dest_const")),
+    mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
+      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
+    conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
+        (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
+
+fun field_funs key =
+  let
+    fun numeral_is_const ct =
+      case term_of ct of
+       Const (@{const_name Rings.divide},_) \$ a \$ b =>
+         can HOLogic.dest_number a andalso can HOLogic.dest_number b
+     | Const (@{const_name Rings.inverse},_)\$t => can HOLogic.dest_number t
+     | t => can HOLogic.dest_number t
+    fun dest_const ct = ((case term_of ct of
+       Const (@{const_name Rings.divide},_) \$ a \$ b=>
+        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+     | Const (@{const_name Rings.inverse},_)\$t =>
+                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
+     | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
+       handle TERM _ => error "ring_dest_const")
+    fun mk_const phi cT x =
+      let val (a, b) = Rat.quotient_of_rat x
+      in if b = 1 then Numeral.mk_cnumber cT a
+        else Thm.capply
+             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+                         (Numeral.mk_cnumber cT a))
+             (Numeral.mk_cnumber cT b)
+      end
+  in funs key
+     {is_const = K numeral_is_const,
+      dest_const = K dest_const,
+      mk_const = mk_const,
+      conv = K (K field_comp_conv)}
+  end;
+
+
+
+(** auxiliary **)

fun is_comb ct =
(case Thm.term_of ct of
@@ -55,6 +401,7 @@
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
@{thm "less_nat_number_of"}];
+
zerone_conv
(Simplifier.rewrite
@@ -64,13 +411,15 @@
@ map (fn th => th RS sym) @{thms numerals}));

val zeron_tm = @{cterm "0::nat"};
val onen_tm  = @{cterm "1::nat"};
val true_tm = @{cterm "True"};

-(* The main function! *)
+(** normalizing conversions **)
+
+(* core conversion *)
+
fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
let
@@ -182,7 +531,7 @@
then
let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
val (l,r) = Thm.dest_comb(concl th1)
-           in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r))
+           in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
end
else
if opr aconvc mul_tm
@@ -563,7 +912,7 @@
let val (l,r) = Thm.dest_comb tm in
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
let val th1 = inst_thm [(cx',r)] neg_mul
-            val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
+            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
in transitive th2 (polynomial_monomial_mul_conv (concl th2))
end
end;
@@ -606,7 +955,7 @@
then
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
(polynomial_conv r)
-                  val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv)
+                  val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
(Thm.rhs_of th1)
in transitive th1 th2
end
@@ -638,11 +987,14 @@

fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;

+
+(* various normalizing conversions *)
+
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
{conv, dest_const, mk_const, is_const}) ord =
let
val pow_conv =
-      arg_conv (Simplifier.rewrite nat_exp_ss)
+      Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
then_conv Simplifier.rewrite
(HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
then_conv conv ctxt
@@ -656,14 +1008,57 @@
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;

fun semiring_normalize_ord_conv ctxt ord tm =
-  (case NormalizerData.match ctxt tm of
+  (case match ctxt tm of
NONE => reflexive tm
| SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);

-
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;

-fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>
-  rtac (semiring_normalize_conv ctxt
-    (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i);
+
+(** Isar setup **)
+
+local
+
+fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ();
+fun keyword2 k1 k2 = Scan.lift (Args.\$\$\$ k1 -- Args.\$\$\$ k2 -- Args.colon) >> K ();
+fun keyword3 k1 k2 k3 =
+  Scan.lift (Args.\$\$\$ k1 -- Args.\$\$\$ k2 -- Args.\$\$\$ k3 -- Args.colon) >> K ();
+
+val opsN = "ops";
+val rulesN = "rules";
+
+val normN = "norm";
+val constN = "const";
+val delN = "del";
+
+val any_keyword =
+  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
+  keyword2 ringN opsN || keyword2 ringN rulesN ||
+  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
+  keyword2 idomN rulesN || keyword2 idealN rulesN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map Drule.dest_term;
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+val setup =
+  Attrib.setup @{binding normalizer}
+    (Scan.lift (Args.\$\$\$ delN >> K del) ||
+      ((keyword2 semiringN opsN |-- terms) --
+       (keyword2 semiringN rulesN |-- thms)) --
+      (optional (keyword2 ringN opsN |-- terms) --
+       optional (keyword2 ringN rulesN |-- thms)) --
+      (optional (keyword2 fieldN opsN |-- terms) --
+       optional (keyword2 fieldN rulesN |-- thms)) --
+      optional (keyword2 idomN rulesN |-- thms) --
+      optional (keyword2 idealN rulesN |-- thms)
+      >> (fn ((((sr, r), f), id), idl) =>
+             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+    "semiring normalizer data";
+
end;
+
+end;```
```--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu May 06 11:08:19 2010 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(*  Title:      HOL/Tools/Groebner_Basis/normalizer_data.ML
-    ID:         \$Id\$
-    Author:     Amine Chaieb, TU Muenchen
-
-Ring normalization data.
-*)
-
-signature NORMALIZER_DATA =
-sig
-  type entry
-  val get: Proof.context -> simpset * (thm * entry) list
-  val match: Proof.context -> cterm -> entry option
-  val del: attribute
-  val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
-    -> attribute
-  val funs: thm -> {is_const: morphism -> cterm -> bool,
-    dest_const: morphism -> cterm -> Rat.rat,
-    mk_const: morphism -> ctyp -> Rat.rat -> cterm,
-    conv: morphism -> Proof.context -> cterm -> thm} -> declaration
-  val setup: theory -> theory
-end;
-
-structure NormalizerData: NORMALIZER_DATA =
-struct
-
-(* data *)
-
-type entry =
- {vars: cterm list,
-  semiring: cterm list * thm list,
-  ring: cterm list * thm list,
-  field: cterm list * thm list,
-  idom: thm list,
-  ideal: thm list} *
- {is_const: cterm -> bool,
-  dest_const: cterm -> Rat.rat,
-  mk_const: ctyp -> Rat.rat -> cterm,
-  conv: Proof.context -> cterm -> thm};
-
-val eq_key = Thm.eq_thm;
-fun eq_data arg = eq_fst eq_key arg;
-
-structure Data = Generic_Data
-(
-  type T = simpset * (thm * entry) list;
-  val empty = (HOL_basic_ss, []);
-  val extend = I;
-  fun merge ((ss, e), (ss', e')) : T =
-    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
-);
-
-val get = Data.get o Context.Proof;
-
-
-(* match data *)
-
-fun match ctxt tm =
-  let
-    fun match_inst
-        ({vars, semiring = (sr_ops, sr_rules),
-          ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
-         fns as {is_const, dest_const, mk_const, conv}) pat =
-       let
-        fun h instT =
-          let
-            val substT = Thm.instantiate (instT, []);
-            val substT_cterm = Drule.cterm_rule substT;
-
-            val vars' = map substT_cterm vars;
-            val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
-            val ring' = (map substT_cterm r_ops, map substT r_rules);
-            val field' = (map substT_cterm f_ops, map substT f_rules);
-            val idom' = map substT idom;
-            val ideal' = map substT ideal;
-
-            val result = ({vars = vars', semiring = semiring',
-                           ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
-          in SOME result end
-      in (case try Thm.match (pat, tm) of
-           NONE => NONE
-         | SOME (instT, _) => h instT)
-      end;
-
-    fun match_struct (_,
-        entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
-      get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
-  in get_first match_struct (snd (get ctxt)) end;
-
-
-(* logical content *)
-
-val semiringN = "semiring";
-val ringN = "ring";
-val idomN = "idom";
-val idealN = "ideal";
-val fieldN = "field";
-
-fun undefined _ = raise Match;
-
-fun del_data key = apsnd (remove eq_data (key, []));
-
-val del = Thm.declaration_attribute (Data.map o del_data);
-   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-val del_ss = Thm.declaration_attribute
-   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
-
-fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
-         field = (f_ops, f_rules), idom, ideal} =
-  Thm.declaration_attribute (fn key => fn context => context |> Data.map
-    let
-      val ctxt = Context.proof_of context;
-
-      fun check kind name xs n =
-        null xs orelse length xs = n orelse
-        error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
-      val check_ops = check "operations";
-      val check_rules = check "rules";
-
-      val _ =
-        check_ops semiringN sr_ops 5 andalso
-        check_rules semiringN sr_rules 37 andalso
-        check_ops ringN r_ops 2 andalso
-        check_rules ringN r_rules 2 andalso
-        check_ops fieldN f_ops 2 andalso
-        check_rules fieldN f_rules 2 andalso
-        check_rules idomN idom 2;
-
-      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
-      val sr_rules' = map mk_meta sr_rules;
-      val r_rules' = map mk_meta r_rules;
-      val f_rules' = map mk_meta f_rules;
-
-      fun rule i = nth sr_rules' (i - 1);
-
-      val (cx, cy) = Thm.dest_binop (hd sr_ops);
-      val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
-      val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
-      val ((clx, crx), (cly, cry)) =
-        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
-      val ((ca, cb), (cc, cd)) =
-        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
-      val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
-      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
-
-      val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
-      val semiring = (sr_ops, sr_rules');
-      val ring = (r_ops, r_rules');
-      val field = (f_ops, f_rules');
-      val ideal' = map (symmetric o mk_meta) ideal
-    in
-      del_data key #>
-      apsnd (cons (key, ({vars = vars, semiring = semiring,
-                          ring = ring, field = field, idom = idom, ideal = ideal'},
-             {is_const = undefined, dest_const = undefined, mk_const = undefined,
-             conv = undefined})))
-    end);
-
-
-(* extra-logical functions *)
-
-fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
- (Data.map o apsnd) (fn data =>
-  let
-    val key = Morphism.thm phi raw_key;
-    val _ = AList.defined eq_key data key orelse
-      raise THM ("No data entry for structure key", 0, [key]);
-    val fns = {is_const = is_const phi, dest_const = dest_const phi,
-      mk_const = mk_const phi, conv = conv phi};
-  in AList.map_entry eq_key key (apsnd (K fns)) data end);
-
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ();
-fun keyword2 k1 k2 = Scan.lift (Args.\$\$\$ k1 -- Args.\$\$\$ k2 -- Args.colon) >> K ();
-fun keyword3 k1 k2 k3 =
-  Scan.lift (Args.\$\$\$ k1 -- Args.\$\$\$ k2 -- Args.\$\$\$ k3 -- Args.colon) >> K ();
-
-val opsN = "ops";
-val rulesN = "rules";
-
-val normN = "norm";
-val constN = "const";
-val delN = "del";
-
-val any_keyword =
-  keyword2 semiringN opsN || keyword2 semiringN rulesN ||
-  keyword2 ringN opsN || keyword2 ringN rulesN ||
-  keyword2 fieldN opsN || keyword2 fieldN rulesN ||
-  keyword2 idomN rulesN || keyword2 idealN rulesN;
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map Drule.dest_term;
-
-fun optional scan = Scan.optional scan [];
-
-in
-
-val normalizer_setup =
-  Attrib.setup @{binding normalizer}
-    (Scan.lift (Args.\$\$\$ delN >> K del) ||
-      ((keyword2 semiringN opsN |-- terms) --
-       (keyword2 semiringN rulesN |-- thms)) --
-      (optional (keyword2 ringN opsN |-- terms) --
-       optional (keyword2 ringN rulesN |-- thms)) --
-      (optional (keyword2 fieldN opsN |-- terms) --
-       optional (keyword2 fieldN rulesN |-- thms)) --
-      optional (keyword2 idomN rulesN |-- thms) --
-      optional (keyword2 idealN rulesN |-- thms)
-      >> (fn ((((sr, r), f), id), idl) =>
-             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
-    "semiring normalizer data";
-
-end;
-
-
-(* theory setup *)
-
-val setup =
-  normalizer_setup #>
-
-end;```
```--- a/src/HOL/Tools/Qelim/cooper.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 07 09:59:59 2010 +0200
@@ -3,7 +3,7 @@
*)

signature COOPER =
- sig
+sig
val cooper_conv : Proof.context -> conv
exception COOPER of string * exn
end;
@@ -12,7 +12,6 @@
struct

open Conv;
-open Normalizer;

exception COOPER of string * exn;
fun simp_thms_conv ctxt =```
```--- a/src/HOL/Tools/Qelim/cooper_data.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Fri May 07 09:59:59 2010 +0200
@@ -1,5 +1,4 @@
(*  Title:      HOL/Tools/Qelim/cooper_data.ML
-    ID:         \$Id\$
Author:     Amine Chaieb, TU Muenchen
*)

@@ -16,8 +15,7 @@
struct

type entry = simpset * (term list);
-val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
+
val allowed_consts =
[@{term "op + :: int => _"}, @{term "op + :: nat => _"},
@{term "op - :: int => _"}, @{term "op - :: nat => _"},
@@ -47,7 +45,7 @@
structure Data = Generic_Data
(
type T = simpset * term list;
-  val empty = (start_ss, allowed_consts);
+  val empty = (HOL_ss, allowed_consts);
val extend  = I;
fun merge ((ss1, ts1), (ss2, ts2)) =
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
@@ -64,7 +62,7 @@
(ss delsimps [th], subtract (op aconv) ts' ts )))

-(* concrete syntax *)
+(* theory setup *)

local

@@ -79,16 +77,11 @@

in

-val presburger_setup =
+val setup =
Attrib.setup @{binding presburger}
((Scan.lift (Args.\$\$\$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
optional (keyword constsN |-- terms) >> add) "Cooper data";

end;

-
-(* theory setup *)
-
-val setup = presburger_setup;
-
end;```
```--- a/src/HOL/Tools/Qelim/presburger.ML	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri May 07 09:59:59 2010 +0200
@@ -11,7 +11,7 @@
struct

open Conv;
-val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
+val comp_ss = HOL_ss addsimps @{thms semiring_norm};

fun strip_objimp ct =
(case Thm.term_of ct of```
```--- a/src/HOL/ex/Groebner_Examples.thy	Thu May 06 11:08:19 2010 -0700
+++ b/src/HOL/ex/Groebner_Examples.thy	Fri May 07 09:59:59 2010 +0200
@@ -10,18 +10,30 @@

subsection {* Basic examples *}

-schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
-  by sring_norm
+lemma
+  fixes x :: int
+  shows "x ^ 3 = x ^ 3"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

-schematic_lemma "(x - (-2))^5 == ?X::int"
-  by sring_norm
+lemma
+  fixes x :: int
+  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

-schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
-  by sring_norm
+schematic_lemma
+  fixes x :: int
+  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
apply (simp only: power_Suc power_0)
-  apply (simp only: comp_arith)
+  apply (simp only: semiring_norm)
oops

lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"```