# HG changeset patch
# User huffman
# Date 1261196003 28800
# Node ID 319616f4eecf79c8325f2522a6de4971e6335f28
# Parent  14595e0c27e877832883fcb006e2ef6895ac6522
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs

diff -r 14595e0c27e8 -r 319616f4eecf src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Dec 18 19:00:11 2009 -0800
+++ b/src/HOL/OrderedGroup.thy	Fri Dec 18 20:13:23 2009 -0800
@@ -159,21 +159,26 @@
   assumes diff_minus: "a - b = a + (- b)"
 begin
 
-lemma minus_add_cancel: "- a + (a + b) = b"
-by (simp add: add_assoc[symmetric])
+lemma minus_unique:
+  assumes "a + b = 0" shows "- a = b"
+proof -
+  have "- a = - a + (a + b)" using assms by simp
+  also have "\<dots> = b" by (simp add: add_assoc [symmetric])
+  finally show ?thesis .
+qed
+
+lemmas equals_zero_I = minus_unique (* legacy name *)
 
 lemma minus_zero [simp]: "- 0 = 0"
 proof -
-  have "- 0 = - 0 + (0 + 0)" by (simp only: add_0_right)
-  also have "\<dots> = 0" by (rule minus_add_cancel)
-  finally show ?thesis .
+  have "0 + 0 = 0" by (rule add_0_right)
+  thus "- 0 = 0" by (rule minus_unique)
 qed
 
 lemma minus_minus [simp]: "- (- a) = a"
 proof -
-  have "- (- a) = - (- a) + (- a + a)" by simp
-  also have "\<dots> = a" by (rule minus_add_cancel)
-  finally show ?thesis .
+  have "- a + a = 0" by (rule left_minus)
+  thus "- (- a) = a" by (rule minus_unique)
 qed
 
 lemma right_minus [simp]: "a + - a = 0"
@@ -183,6 +188,20 @@
   finally show ?thesis .
 qed
 
+lemma minus_add_cancel: "- a + (a + b) = b"
+by (simp add: add_assoc [symmetric])
+
+lemma add_minus_cancel: "a + (- a + b) = b"
+by (simp add: add_assoc [symmetric])
+
+lemma minus_add: "- (a + b) = - b + - a"
+proof -
+  have "(a + b) + (- b + - a) = 0"
+    by (simp add: add_assoc add_minus_cancel)
+  thus "- (a + b) = - b + - a"
+    by (rule minus_unique)
+qed
+
 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
 proof
   assume "a - b = 0"
@@ -193,16 +212,6 @@
   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
 qed
 
-lemma minus_unique:
-  assumes "a + b = 0" shows "- a = b"
-proof -
-  have "- a = - a + (a + b)" using assms by simp
-  also have "\<dots> = b" by (simp add: add_assoc[symmetric])
-  finally show ?thesis .
-qed
-
-lemmas equals_zero_I = minus_unique (* legacy name *)
-
 lemma diff_self [simp]: "a - a = 0"
 by (simp add: diff_minus)
 
@@ -1312,9 +1321,6 @@
 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
 by (simp add: diff_minus)
 
-lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
-by (simp add: add_assoc[symmetric])
-
 lemma le_add_right_mono: 
   assumes 
   "a <= b + (c::'a::pordered_ab_group_add)"