# HG changeset patch
# User haftmann
# Date 1273162567 -7200
# Node ID b09f3ad3208f8cde78e9cf5db14ec9cd04a25493
# Parent  5f612b6d64a8053c3a354d58d93e51b5fe8f9af8
moved generic lemmas to appropriate places

diff -r 5f612b6d64a8 -r b09f3ad3208f src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:59:20 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu May 06 18:16:07 2010 +0200
@@ -162,16 +162,6 @@
 proof
 qed (simp_all add: algebra_simps)
 
-lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
-  by simp
-
-lemmas semiring_norm =
-  Let_def arith_simps nat_arith rel_simps neg_simps if_False
-  if_True add_0 add_Suc add_number_of_left mult_number_of_left
-  numeral_1_eq_1[symmetric] Suc_eq_plus1
-  numeral_0_eq_0[symmetric] numerals[symmetric]
-  iszero_simps not_iszero_Numeral1
-
 ML {*
 local
 
@@ -589,6 +579,8 @@
 end
 *}
 
+lemmas comp_arith = semiring_norm (*FIXME*)
+
 
 subsection {* Groebner Bases *}
 
diff -r 5f612b6d64a8 -r b09f3ad3208f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 06 17:59:20 2010 +0200
+++ b/src/HOL/Int.thy	Thu May 06 18:16:07 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"
-by (simp add: iszero_def)
-
-lemma not_iszero_1: "~ iszero 1"
-by (simp add: iszero_def eq_commute)
+  by (simp add: iszero_def)
+
+lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
+  by (simp add: iszero_0)
+
+lemma not_iszero_1: "\<not> iszero 1"
+  by (simp add: iszero_def)
+
+lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
+  by (simp add: not_iszero_1)
 
 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)"
 unfolding iszero_def number_of_add number_of_minus
 by (simp add: algebra_simps)
 
diff -r 5f612b6d64a8 -r b09f3ad3208f src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Thu May 06 17:59:20 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu May 06 18:16:07 2010 +0200
@@ -694,6 +694,13 @@
   eq_nat_number_of
   less_nat_number_of
 
+lemmas semiring_norm =
+  Let_def arith_simps nat_arith rel_simps neg_simps if_False
+  if_True add_0 add_Suc add_number_of_left mult_number_of_left
+  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)