rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
authorhuffman
Sat Aug 20 10:08:47 2011 -0700 (2011-08-20)
changeset 4434600dd3c4dabe0
parent 44345 881c324470a2
child 44347 0e19dcf19c61
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
src/HOL/RealDef.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 09:59:28 2011 -0700
     1.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 10:08:47 2011 -0700
     1.3 @@ -1630,12 +1630,6 @@
     1.4    "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
     1.5  by (rule sum_squares_eq_zero_iff)
     1.6  
     1.7 -text {* TODO: no longer real-specific; rename and move elsewhere *}
     1.8 -lemma real_squared_diff_one_factored:
     1.9 -  fixes x :: "'a::ring_1"
    1.10 -  shows "x * x - 1 = (x + 1) * (x - 1)"
    1.11 -by (simp add: algebra_simps)
    1.12 -
    1.13  text {* FIXME: declare this [simp] for all types, or not at all *}
    1.14  lemma realpow_two_sum_zero_iff [simp]:
    1.15       "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
     2.1 --- a/src/HOL/Rings.thy	Sat Aug 20 09:59:28 2011 -0700
     2.2 +++ b/src/HOL/Rings.thy	Sat Aug 20 10:08:47 2011 -0700
     2.3 @@ -277,6 +277,10 @@
     2.4  
     2.5  subclass semiring_1_cancel ..
     2.6  
     2.7 +lemma square_diff_one_factored:
     2.8 +  "x * x - 1 = (x + 1) * (x - 1)"
     2.9 +  by (simp add: algebra_simps)
    2.10 +
    2.11  end
    2.12  
    2.13  class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult