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