# HG changeset patch
# User huffman
# Date 1313870820 25200
# Node ID 40101794c52f7ddcfe76bd73639af122886f2dcd
# Parent  0e19dcf19c61e85a2d04f4b579dca50271fee1ed
move lemma add_eq_0_iff to Groups.thy

diff -r 0e19dcf19c61 -r 40101794c52f src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Aug 20 12:51:15 2011 -0700
+++ b/src/HOL/Groups.thy	Sat Aug 20 13:07:00 2011 -0700
@@ -411,6 +411,10 @@
   ultimately show "a = - b" by simp
 qed
 
+lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
+  unfolding eq_neg_iff_add_eq_0 [symmetric]
+  by (rule equation_minus_iff)
+
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +
@@ -466,7 +470,7 @@
 (* FIXME: duplicates right_minus_eq from class group_add *)
 (* but only this one is declared as a simp rule. *)
 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
-by (simp add: algebra_simps)
+  by (rule right_minus_eq)
 
 lemma diff_eq_diff_eq:
   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
diff -r 0e19dcf19c61 -r 40101794c52f src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Aug 20 12:51:15 2011 -0700
+++ b/src/HOL/RealDef.thy	Sat Aug 20 13:07:00 2011 -0700
@@ -1612,12 +1612,6 @@
   shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
 by (simp add: algebra_simps)
 
-text {* TODO: move elsewhere *}
-lemma add_eq_0_iff:
-  fixes x y :: "'a::group_add"
-  shows "x + y = 0 \<longleftrightarrow> y = - x"
-by (auto dest: minus_unique)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma real_two_squares_add_zero_iff [simp]:
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"