# HG changeset patch
# User huffman
# Date 1321551060 -3600
# Node ID 3e2722d661694f00de89c5eb5563bb3c5fd7adfb
# Parent  94c37f3df10f431da463e820ff5741607c648c70
Groups.thy: generalize several lemmas from class ab_group_add to class group_add

diff -r 94c37f3df10f -r 3e2722d66169 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Nov 17 15:07:46 2011 +0100
+++ b/src/HOL/Groups.thy	Thu Nov 17 18:31:00 2011 +0100
@@ -284,7 +284,6 @@
   finally show ?thesis .
 qed
 
-
 lemmas equals_zero_I = minus_unique (* legacy name *)
 
 lemma minus_zero [simp]: "- 0 = 0"
@@ -413,6 +412,28 @@
   unfolding eq_neg_iff_add_eq_0 [symmetric]
   by (rule equation_minus_iff)
 
+lemma minus_diff_eq [simp]: "- (a - b) = b - a"
+  by (simp add: diff_minus minus_add)
+
+lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
+  by (simp add: diff_minus add_assoc)
+
+lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
+  by (auto simp add: diff_minus add_assoc)
+
+lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
+  by (auto simp add: diff_minus add_assoc)
+
+lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
+  by (simp add: diff_minus minus_add add_assoc)
+
+lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
+  by (fact right_minus_eq [symmetric])
+
+lemma diff_eq_diff_eq:
+  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+  by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
+
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +
@@ -440,40 +461,17 @@
   "- (a + b) = - a + - b"
 by (rule minus_unique) (simp add: add_ac)
 
-lemma minus_diff_eq [simp]:
-  "- (a - b) = b - a"
-by (simp add: diff_minus add_commute)
-
-lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
-by (simp add: diff_minus add_ac)
-
 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
 by (simp add: diff_minus add_ac)
 
-lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
-by (auto simp add: diff_minus add_assoc)
-
-lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
-by (auto simp add: diff_minus add_assoc)
-
 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
 by (simp add: diff_minus add_ac)
 
-lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
-by (simp add: diff_minus add_ac)
-
-lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
-by (simp add: algebra_simps)
-
 (* FIXME: duplicates right_minus_eq from class group_add *)
 (* but only this one is declared as a simp rule. *)
 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   by (rule right_minus_eq)
 
-lemma diff_eq_diff_eq:
-  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
-  by (auto simp add: algebra_simps)
-  
 end
 
 
diff -r 94c37f3df10f -r 3e2722d66169 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Thu Nov 17 15:07:46 2011 +0100
+++ b/src/HOL/Import/HOL/real.imp	Thu Nov 17 18:31:00 2011 +0100
@@ -113,7 +113,7 @@
   "REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
   "REAL_NOT_LT" > "HOL4Compat.real_lte"
   "REAL_NOT_LE" > "Orderings.linorder_class.not_le"
-  "REAL_NEG_SUB" > "Groups.ab_group_add_class.minus_diff_eq"
+  "REAL_NEG_SUB" > "Groups.group_add_class.minus_diff_eq"
   "REAL_NEG_RMUL" > "Int.int_arith_rules_14"
   "REAL_NEG_NEG" > "Groups.group_add_class.minus_minus"
   "REAL_NEG_MUL2" > "Rings.ring_class.minus_mult_minus"
diff -r 94c37f3df10f -r 3e2722d66169 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 17 15:07:46 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 17 18:31:00 2011 +0100
@@ -3861,7 +3861,7 @@
   then obtain y e where "e>0" and e:"ball y e \<subseteq> s" and y:"x = a + y" unfolding image_iff Bex_def mem_interior by auto
   { fix z have *:"a + y - z = y + a - z" by auto
     assume "z\<in>ball x e"
-    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y ab_group_add_class.diff_diff_eq2 * by auto
+    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 * by auto
     hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"])  }
   hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
   thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto