# HG changeset patch
# User huffman
# Date 1273552072 25200
# Node ID 9207505d1ee563e03169368e24b4265fd90f9df0
# Parent  d75a28a13639e21ae91432d113bbee4c05612bb9
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

diff -r d75a28a13639 -r 9207505d1ee5 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Mon May 10 14:53:33 2010 -0700
+++ b/src/HOL/RealPow.thy	Mon May 10 21:27:52 2010 -0700
@@ -69,18 +69,6 @@
   shows "x * x - 1 = (x + 1) * (x - 1)"
 by (simp add: algebra_simps)
 
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma real_mult_is_one [simp]:
-  fixes x :: "'a::ring_1_no_zero_divisors"
-  shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
-proof -
-  have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
-    by (simp add: algebra_simps)
-  also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
-    by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
-  finally show ?thesis .
-qed
-
 (* FIXME: declare this [simp] for all types, or not at all *)
 lemma realpow_two_sum_zero_iff [simp]:
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
diff -r d75a28a13639 -r 9207505d1ee5 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon May 10 14:53:33 2010 -0700
+++ b/src/HOL/Rings.thy	Mon May 10 21:27:52 2010 -0700
@@ -349,6 +349,17 @@
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
+lemma square_eq_1_iff [simp]:
+  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+  have "(x - 1) * (x + 1) = x * x - 1"
+    by (simp add: algebra_simps)
+  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
+    by simp
+  thus ?thesis
+    by (simp add: eq_neg_iff_add_eq_0)
+qed
+
 lemma mult_cancel_right1 [simp]:
   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
 by (insert mult_cancel_right [of 1 c b], force)