move lemma add_eq_0_iff to Groups.thy
authorhuffman
Sat Aug 20 13:07:00 2011 -0700 (2011-08-20)
changeset 4434840101794c52f
parent 44347 0e19dcf19c61
child 44349 f057535311c5
move lemma add_eq_0_iff to Groups.thy
src/HOL/Groups.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Groups.thy	Sat Aug 20 12:51:15 2011 -0700
     1.2 +++ b/src/HOL/Groups.thy	Sat Aug 20 13:07:00 2011 -0700
     1.3 @@ -411,6 +411,10 @@
     1.4    ultimately show "a = - b" by simp
     1.5  qed
     1.6  
     1.7 +lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
     1.8 +  unfolding eq_neg_iff_add_eq_0 [symmetric]
     1.9 +  by (rule equation_minus_iff)
    1.10 +
    1.11  end
    1.12  
    1.13  class ab_group_add = minus + uminus + comm_monoid_add +
    1.14 @@ -466,7 +470,7 @@
    1.15  (* FIXME: duplicates right_minus_eq from class group_add *)
    1.16  (* but only this one is declared as a simp rule. *)
    1.17  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
    1.18 -by (simp add: algebra_simps)
    1.19 +  by (rule right_minus_eq)
    1.20  
    1.21  lemma diff_eq_diff_eq:
    1.22    "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
     2.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 12:51:15 2011 -0700
     2.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 13:07:00 2011 -0700
     2.3 @@ -1612,12 +1612,6 @@
     2.4    shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
     2.5  by (simp add: algebra_simps)
     2.6  
     2.7 -text {* TODO: move elsewhere *}
     2.8 -lemma add_eq_0_iff:
     2.9 -  fixes x y :: "'a::group_add"
    2.10 -  shows "x + y = 0 \<longleftrightarrow> y = - x"
    2.11 -by (auto dest: minus_unique)
    2.12 -
    2.13  text {* FIXME: declare this [simp] for all types, or not at all *}
    2.14  lemma real_two_squares_add_zero_iff [simp]:
    2.15    "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"