src/HOL/RealDef.thy
changeset 44346 00dd3c4dabe0
parent 44344 49be3e7d4762
child 44347 0e19dcf19c61
equal deleted inserted replaced
44345:881c324470a2 44346:00dd3c4dabe0
  1628 text {* FIXME: declare this [simp] for all types, or not at all *}
  1628 text {* FIXME: declare this [simp] for all types, or not at all *}
  1629 lemma real_two_squares_add_zero_iff [simp]:
  1629 lemma real_two_squares_add_zero_iff [simp]:
  1630   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
  1630   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
  1631 by (rule sum_squares_eq_zero_iff)
  1631 by (rule sum_squares_eq_zero_iff)
  1632 
  1632 
  1633 text {* TODO: no longer real-specific; rename and move elsewhere *}
       
  1634 lemma real_squared_diff_one_factored:
       
  1635   fixes x :: "'a::ring_1"
       
  1636   shows "x * x - 1 = (x + 1) * (x - 1)"
       
  1637 by (simp add: algebra_simps)
       
  1638 
       
  1639 text {* FIXME: declare this [simp] for all types, or not at all *}
  1633 text {* FIXME: declare this [simp] for all types, or not at all *}
  1640 lemma realpow_two_sum_zero_iff [simp]:
  1634 lemma realpow_two_sum_zero_iff [simp]:
  1641      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
  1635      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
  1642 by (rule sum_power2_eq_zero_iff)
  1636 by (rule sum_power2_eq_zero_iff)
  1643 
  1637