author huffman Sat Feb 14 16:51:18 2009 -0800 (2009-02-14) changeset 29914 c9ced4f54e82 parent 29913 89eadbe71e97 child 29915 2146e512cec9
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
```     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.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