remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
authorhuffman
Sat Aug 20 12:51:15 2011 -0700 (2011-08-20)
changeset 443470e19dcf19c61
parent 44346 00dd3c4dabe0
child 44348 40101794c52f
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 10:08:47 2011 -0700
     1.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 12:51:15 2011 -0700
     1.3 @@ -1618,13 +1618,6 @@
     1.4    shows "x + y = 0 \<longleftrightarrow> y = - x"
     1.5  by (auto dest: minus_unique)
     1.6  
     1.7 -text {* TODO: no longer real-specific; rename and move elsewhere *}
     1.8 -lemma realpow_two_disj:
     1.9 -  fixes x :: "'a::idom"
    1.10 -  shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
    1.11 -using realpow_two_diff [of x y]
    1.12 -by (auto simp add: add_eq_0_iff)
    1.13 -
    1.14  text {* FIXME: declare this [simp] for all types, or not at all *}
    1.15  lemma real_two_squares_add_zero_iff [simp]:
    1.16    "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"