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