merged

--- a/src/HOL/Fun.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/Fun.thy	Sat Dec 19 06:07:33 2009 -0800
@@ -467,6 +467,11 @@
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
 by (rule ext, simp add: fun_upd_def swap_def)
 
+lemma swap_triple:
+  assumes "a \<noteq> c" and "b \<noteq> c"
+  shows "swap a b (swap b c (swap a b f)) = swap a c f"
+  using assms by (simp add: expand_fun_eq swap_def)
+
 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
 by (rule ext, simp add: fun_upd_def swap_def)
 

--- a/src/HOL/Library/FrechetDeriv.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Sat Dec 19 06:07:33 2009 -0800
@@ -438,7 +438,7 @@
     hence 2: "x + h \<noteq> 0"
       apply (rule contrapos_nn)
       apply (rule sym)
-      apply (erule equals_zero_I)
+      apply (erule minus_unique)
       done
     show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
           = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"

--- a/src/HOL/NSA/NSA.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/NSA/NSA.thy	Sat Dec 19 06:07:33 2009 -0800
@@ -1711,7 +1711,7 @@
 lemma Infinitesimal_add_not_zero:
      "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> star_of x + h \<noteq> 0"
 apply auto
-apply (subgoal_tac "h = - star_of x", auto intro: equals_zero_I [symmetric])
+apply (subgoal_tac "h = - star_of x", auto intro: minus_unique [symmetric])
 done
 
 lemma Infinitesimal_square_cancel [simp]:

--- a/src/HOL/NSA/NSComplex.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Sat Dec 19 06:07:33 2009 -0800
@@ -161,7 +161,7 @@
 
 lemma hcomplex_add_minus_eq_minus:
       "x + y = (0::hcomplex) ==> x = -y"
-apply (drule OrderedGroup.equals_zero_I)
+apply (drule OrderedGroup.minus_unique)
 apply (simp add: minus_equation_iff [of x y])
 done
 

--- a/src/HOL/OrderedGroup.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Sat Dec 19 06:07:33 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,14 +212,6 @@
   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
 qed
 
-lemma equals_zero_I:
-  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
-
 lemma diff_self [simp]: "a - a = 0"
 by (simp add: diff_minus)
 
@@ -291,7 +302,7 @@
 
 lemma minus_add_distrib [simp]:
   "- (a + b) = - a + - b"
-by (rule equals_zero_I) (simp add: add_ac)
+by (rule minus_unique) (simp add: add_ac)
 
 lemma minus_diff_eq [simp]:
   "- (a - b) = b - a"
@@ -1310,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)"

--- a/src/HOL/Ring_and_Field.thy	Fri Dec 18 16:52:36 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sat Dec 19 06:07:33 2009 -0800
@@ -228,10 +228,10 @@
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
+by (rule minus_unique) (simp add: left_distrib [symmetric]) 
 
 lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
+by (rule minus_unique) (simp add: right_distrib [symmetric]) 
 
 text{*Extract signs from products*}
 lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]