generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
authorhuffman
Sat Feb 14 16:51:18 2009 -0800 (2009-02-14)
changeset 29914c9ced4f54e82
parent 29913 89eadbe71e97
child 29915 2146e512cec9
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
src/HOL/Library/Formal_Power_Series.thy
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 15:30:26 2009 -0800
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 16:51:18 2009 -0800
     1.3 @@ -691,16 +691,6 @@
     1.4    by (simp_all add: fps_power_def)
     1.5  end
     1.6  
     1.7 -lemma eq_neg_iff_add_eq_0: "(a::'a::ring) = -b \<longleftrightarrow> a + b = 0"
     1.8 -proof-
     1.9 -  {assume "a = -b" hence "b + a = b + -b" by simp
    1.10 -    hence "a + b = 0" by (simp add: ring_simps)}
    1.11 -  moreover
    1.12 -  {assume "a + b = 0" hence "a + b - b = -b" by simp
    1.13 -    hence "a = -b" by simp}
    1.14 -  ultimately show ?thesis by blast
    1.15 -qed
    1.16 -
    1.17  lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
    1.18  proof-
    1.19    {assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
     2.1 --- a/src/HOL/OrderedGroup.thy	Sat Feb 14 15:30:26 2009 -0800
     2.2 +++ b/src/HOL/OrderedGroup.thy	Sat Feb 14 16:51:18 2009 -0800
     2.3 @@ -254,6 +254,16 @@
     2.4  
     2.5  declare diff_minus[symmetric, algebra_simps]
     2.6  
     2.7 +lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
     2.8 +proof
     2.9 +  assume "a = - b" then show "a + b = 0" by simp
    2.10 +next
    2.11 +  assume "a + b = 0"
    2.12 +  moreover have "a + (b + - b) = (a + b) + - b"
    2.13 +    by (simp only: add_assoc)
    2.14 +  ultimately show "a = - b" by simp
    2.15 +qed
    2.16 +
    2.17  end
    2.18  
    2.19  class ab_group_add = minus + uminus + comm_monoid_add +