move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
authorhuffman
Mon May 10 21:27:52 2010 -0700 (2010-05-10)
changeset 368219207505d1ee5
parent 36796 d75a28a13639
child 36822 38a480e0346f
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
src/HOL/RealPow.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/RealPow.thy	Mon May 10 14:53:33 2010 -0700
     1.2 +++ b/src/HOL/RealPow.thy	Mon May 10 21:27:52 2010 -0700
     1.3 @@ -69,18 +69,6 @@
     1.4    shows "x * x - 1 = (x + 1) * (x - 1)"
     1.5  by (simp add: algebra_simps)
     1.6  
     1.7 -(* TODO: no longer real-specific; rename and move elsewhere *)
     1.8 -lemma real_mult_is_one [simp]:
     1.9 -  fixes x :: "'a::ring_1_no_zero_divisors"
    1.10 -  shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
    1.11 -proof -
    1.12 -  have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
    1.13 -    by (simp add: algebra_simps)
    1.14 -  also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
    1.15 -    by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
    1.16 -  finally show ?thesis .
    1.17 -qed
    1.18 -
    1.19  (* FIXME: declare this [simp] for all types, or not at all *)
    1.20  lemma realpow_two_sum_zero_iff [simp]:
    1.21       "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
     2.1 --- a/src/HOL/Rings.thy	Mon May 10 14:53:33 2010 -0700
     2.2 +++ b/src/HOL/Rings.thy	Mon May 10 21:27:52 2010 -0700
     2.3 @@ -349,6 +349,17 @@
     2.4  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
     2.5  begin
     2.6  
     2.7 +lemma square_eq_1_iff [simp]:
     2.8 +  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
     2.9 +proof -
    2.10 +  have "(x - 1) * (x + 1) = x * x - 1"
    2.11 +    by (simp add: algebra_simps)
    2.12 +  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
    2.13 +    by simp
    2.14 +  thus ?thesis
    2.15 +    by (simp add: eq_neg_iff_add_eq_0)
    2.16 +qed
    2.17 +
    2.18  lemma mult_cancel_right1 [simp]:
    2.19    "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
    2.20  by (insert mult_cancel_right [of 1 c b], force)