--- 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 *}
--- 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)
--- 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)