# HG changeset patch
# User huffman
# Date 1273584426 25200
# Node ID 001d1aad99de73fe225cd41a7f2f23e4da04771d
# Parent  38a480e0346f9e9a3c5a2844ef4a5377bd298a28
add lemma power2_eq_1_iff; generalize some other lemmas

diff -r 38a480e0346f -r 001d1aad99de src/HOL/Nat_Numeral.thy
--- 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)