--- a/src/HOL/Nat_Numeral.thy Mon May 10 21:33:48 2010 -0700
+++ b/src/HOL/Nat_Numeral.thy Tue May 11 06:27:06 2010 -0700
@@ -83,7 +83,7 @@
end
-context comm_ring_1
+context ring_1
begin
lemma power2_minus [simp]:
@@ -113,6 +113,19 @@
end
+context ring_1_no_zero_divisors
+begin
+
+lemma zero_eq_power2 [simp]:
+ "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
+ unfolding power2_eq_square by simp
+
+lemma power2_eq_1_iff [simp]:
+ "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
+ unfolding power2_eq_square by simp
+
+end
+
context linordered_ring
begin
@@ -163,10 +176,6 @@
context linordered_idom
begin
-lemma zero_eq_power2 [simp]:
- "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
- by (force simp add: power2_eq_square)
-
lemma zero_le_power2 [simp]:
"0 \<le> a\<twosuperior>"
by (simp add: power2_eq_square)