explicit commutative additive inverse operation;
more explicit focal point for commutative monoids with an inverse operation

--- a/NEWS	Mon Mar 23 19:05:14 2015 +0100
+++ b/NEWS	Mon Mar 23 19:05:14 2015 +0100
@@ -90,6 +90,9 @@
 
 *** HOL ***
 
+* Type classes cancel_ab_semigroup_add / cancel_monoid_add specify
+explicit additive inverse operation.  INCOMPATIBILITY.
+
 * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
   single-step rewriting with subterm selection based on patterns.
 

--- a/src/HOL/Groups.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Groups.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -248,55 +248,52 @@
 
 end
 
-class cancel_ab_semigroup_add = ab_semigroup_add +
-  assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+class cancel_ab_semigroup_add = ab_semigroup_add + minus +
+  assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"
+  assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"
 begin
 
+lemma add_diff_cancel_right' [simp]:
+  "(a + b) - b = a"
+  using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
+
 subclass cancel_semigroup_add
 proof
   fix a b c :: 'a
-  assume "a + b = a + c" 
-  then show "b = c" by (rule add_imp_eq)
+  assume "a + b = a + c"
+  then have "a + b - a = a + c - a"
+    by simp
+  then show "b = c"
+    by simp
 next
   fix a b c :: 'a
   assume "b + a = c + a"
-  then have "a + b = a + c" by (simp only: add.commute)
-  then show "b = c" by (rule add_imp_eq)
+  then have "b + a - a = c + a - a"
+    by simp
+  then show "b = c"
+    by simp
 qed
 
+lemma add_diff_cancel_left [simp]:
+  "(c + a) - (c + b) = a - b"
+  unfolding diff_diff_add [symmetric] by simp
+
+lemma add_diff_cancel_right [simp]:
+  "(a + c) - (b + c) = a - b"
+  using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
+
+lemma diff_right_commute:
+  "a - c - b = a - b - c"
+  by (simp add: diff_diff_add add.commute)
+
 end
 
 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
-
-class comm_monoid_diff = comm_monoid_add + minus +
-  assumes diff_zero [simp]: "a - 0 = a"
-    and zero_diff [simp]: "0 - a = 0"
-    and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
-    and diff_diff_add: "a - b - c = a - (b + c)"
 begin
 
-lemma add_diff_cancel_right [simp]:
-  "(a + c) - (b + c) = a - b"
-  using add_diff_cancel_left [symmetric] by (simp add: add.commute)
-
-lemma add_diff_cancel_left' [simp]:
-  "(b + a) - b = a"
-proof -
-  have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
-  then show ?thesis by simp
-qed
-
-lemma add_diff_cancel_right' [simp]:
-  "(a + b) - b = a"
-  using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
-
-lemma diff_add_zero [simp]:
-  "a - (a + b) = 0"
-proof -
-  have "a - (a + b) = (a + 0) - (a + b)" by simp
-  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
-  finally show ?thesis .
-qed
+lemma diff_zero [simp]:
+  "a - 0 = a"
+  using add_diff_cancel_right' [of a 0] by simp
 
 lemma diff_cancel [simp]:
   "a - a = 0"
@@ -305,10 +302,6 @@
   then show ?thesis by simp
 qed
 
-lemma diff_right_commute:
-  "a - c - b = a - b - c"
-  by (simp add: diff_diff_add add.commute)
-
 lemma add_implies_diff:
   assumes "c + b = a"
   shows "c = a - b"
@@ -317,6 +310,20 @@
   then show "c = a - b" by simp
 qed
 
+end  
+
+class comm_monoid_diff = cancel_comm_monoid_add +
+  assumes zero_diff [simp]: "0 - a = 0"
+begin
+
+lemma diff_add_zero [simp]:
+  "a - (a + b) = 0"
+proof -
+  have "a - (a + b) = (a + 0) - (a + b)" by simp
+  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
+  finally show ?thesis .
+qed
+
 end
 
 
@@ -527,10 +534,12 @@
 subclass cancel_comm_monoid_add
 proof
   fix a b c :: 'a
-  assume "a + b = a + c"
-  then have "- a + a + b = - a + a + c"
-    by (simp only: add.assoc)
-  then show "b = c" by simp
+  have "b + a - a = b"
+    by simp
+  then show "a + b - a = b"
+    by (simp add: ac_simps)
+  show "a - b - c = a - (b + c)"
+    by (simp add: algebra_simps)
 qed
 
 lemma uminus_add_conv_diff [simp]:
@@ -545,18 +554,6 @@
   "(a - b) + c = (a + c) - b"
   by (simp add: algebra_simps)
 
-lemma diff_diff_eq [algebra_simps, field_simps]:
-  "(a - b) - c = a - (b + c)"
-  by (simp add: algebra_simps)
-
-lemma diff_add_eq_diff_diff:
-  "a - (b + c) = a - b - c"
-  using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)
-
-lemma add_diff_cancel_left [simp]:
-  "(c + a) - (c + b) = a - b"
-  by (simp add: algebra_simps)
-
 end
 
 
@@ -1375,7 +1372,13 @@
 
 end
 
-hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
+hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
+
+lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>
+lemmas mult_1 = mult_1_left -- \<open>FIXME duplicate\<close>
+lemmas ab_left_minus = left_minus -- \<open>FIXME duplicate\<close>
+lemmas diff_diff_eq = diff_diff_add -- \<open>FIXME duplicate\<close>
+
 
 subsection {* Tools setup *}
 

--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -207,8 +207,8 @@
 instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
 proof
   fix a b c :: "'a fps"
-  assume "a + b = a + c"
-  then show "b = c" by (simp add: expand_fps_eq)
+  show "a + b - a = b" by (simp add: expand_fps_eq)
+  show "a - b - c = a - (b + c)" by (simp add: expand_fps_eq diff_diff_eq)
 qed
 
 instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..

--- a/src/HOL/Library/Function_Algebras.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -71,7 +71,7 @@
   by default (simp add: fun_eq_iff add.commute)
 
 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-  by default simp
+  by default (simp_all add: fun_eq_iff diff_diff_eq)
 
 instance "fun" :: (type, monoid_add) monoid_add
   by default (simp_all add: fun_eq_iff)

--- a/src/HOL/Library/Multiset.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -95,8 +95,11 @@
 lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
 by (rule union_preserves_multiset)
 
+lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
+by (rule diff_preserves_multiset)
+
 instance
-by default (transfer, simp add: fun_eq_iff)+
+  by default (transfer, simp add: fun_eq_iff)+
 
 end
 
@@ -129,9 +132,6 @@
 instantiation multiset :: (type) comm_monoid_diff
 begin
 
-lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
-by (rule diff_preserves_multiset)
-
 instance
 by default (transfer, simp add: fun_eq_iff)+
 

--- a/src/HOL/Library/Polynomial.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -559,13 +559,32 @@
 
 end
 
-instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
-proof
+instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
+begin
+
+lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+  is "\<lambda>p q n. coeff p n - coeff q n"
+proof (rule almost_everywhere_zeroI) 
+  fix q p :: "'a poly" and i
+  assume "max (degree q) (degree p) < i"
+  then show "coeff p i - coeff q i = 0"
+    by (simp add: coeff_eq_0)
+qed
+
+lemma coeff_diff [simp]:
+  "coeff (p - q) n = coeff p n - coeff q n"
+  by (simp add: minus_poly.rep_eq)
+
+instance proof
   fix p q r :: "'a poly"
-  assume "p + q = p + r" thus "q = r"
+  show "p + q - p = q"
     by (simp add: poly_eq_iff)
+  show "p - q - r = p - (q + r)"
+    by (simp add: poly_eq_iff diff_diff_eq)
 qed
 
+end
+
 instantiation poly :: (ab_group_add) ab_group_add
 begin
 
@@ -578,22 +597,9 @@
     by (simp add: coeff_eq_0)
 qed
 
-lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
-  is "\<lambda>p q n. coeff p n - coeff q n"
-proof (rule almost_everywhere_zeroI) 
-  fix q p :: "'a poly" and i
-  assume "max (degree q) (degree p) < i"
-  then show "coeff p i - coeff q i = 0"
-    by (simp add: coeff_eq_0)
-qed
-
 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   by (simp add: uminus_poly.rep_eq)
 
-lemma coeff_diff [simp]:
-  "coeff (p - q) n = coeff p n - coeff q n"
-  by (simp add: minus_poly.rep_eq)
-
 instance proof
   fix p q :: "'a poly"
   show "- p + p = 0"
@@ -641,20 +647,27 @@
   using degree_add_eq_right [of q p]
   by (simp add: add.commute)
 
-lemma degree_minus [simp]: "degree (- p) = degree p"
+lemma degree_minus [simp]:
+  "degree (- p) = degree p"
   unfolding degree_def by simp
 
-lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
+lemma degree_diff_le_max:
+  fixes p q :: "'a :: ab_group_add poly"
+  shows "degree (p - q) \<le> max (degree p) (degree q)"
   using degree_add_le [where p=p and q="-q"]
   by simp
 
 lemma degree_diff_le:
-  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
-  using degree_add_le [of p n "- q"] by simp
+  fixes p q :: "'a :: ab_group_add poly"
+  assumes "degree p \<le> n" and "degree q \<le> n"
+  shows "degree (p - q) \<le> n"
+  using assms degree_add_le [of p n "- q"] by simp
 
 lemma degree_diff_less:
-  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
-  using degree_add_less [of p n "- q"] by simp
+  fixes p q :: "'a :: ab_group_add poly"
+  assumes "degree p < n" and "degree q < n"
+  shows "degree (p - q) < n"
+  using assms degree_add_less [of p n "- q"] by simp
 
 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   by (rule poly_eqI) simp

--- a/src/HOL/Library/Product_plus.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Product_plus.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -98,7 +98,7 @@
 
 instance prod ::
   (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-    by default (simp add: prod_eq_iff)
+    by default (simp_all add: prod_eq_iff diff_diff_eq)
 
 instance prod ::
   (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -133,7 +133,7 @@
     apply (simp add: LIM_zero_iff [where l = D, symmetric])
     apply (simp add: Lim_within dist_norm)
     apply (simp add: nonzero_norm_divide [symmetric])
-    apply (simp add: 1 diff_add_eq_diff_diff ac_simps)
+    apply (simp add: 1 diff_diff_eq ac_simps)
     done
 qed
 
@@ -299,14 +299,14 @@
   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
     (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
-    eventually_at dist_norm diff_add_eq_diff_diff
+    eventually_at dist_norm diff_diff_eq
   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_within_alt2:
   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
     (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
-    eventually_at dist_norm diff_add_eq_diff_diff
+    eventually_at dist_norm diff_diff_eq
   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_at_alt:

--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -110,7 +110,7 @@
   by default (simp_all add: vec_eq_iff)
 
 instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
-  by default (simp add: vec_eq_iff)
+  by default (simp_all add: vec_eq_iff diff_diff_eq)
 
 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
 

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -5392,11 +5392,7 @@
     unfolding mem_interior by auto
   then have "ball (x - a) e \<subseteq> s"
     unfolding subset_eq Ball_def mem_ball dist_norm
-    apply auto
-    apply (erule_tac x="a + xa" in allE)
-    unfolding ab_group_add_class.diff_diff_eq[symmetric]
-    apply auto
-    done
+    by (auto simp add: diff_diff_eq)
   then show "x \<in> op + a ` interior s"
     unfolding image_iff
     apply (rule_tac x="x - a" in bexI)

--- a/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -795,7 +795,7 @@
 done
 
 instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
-by (intro_classes, transfer, rule add_left_imp_eq)
+by intro_classes (transfer, simp add: diff_diff_eq)+
 
 instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
 

--- a/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -246,11 +246,10 @@
   fix n m q :: nat
   show "(n + m) + q = n + (m + q)" by (induct n) simp_all
   show "n + m = m + n" by (induct n) simp_all
+  show "m + n - m = n" by (induct m) simp_all
+  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
   show "0 + n = n" by simp
-  show "n - 0 = n" by simp
   show "0 - n = 0" by simp
-  show "(q + n) - (q + m) = n - m" by (induct q) simp_all
-  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
 qed
 
 end
@@ -283,7 +282,6 @@
   show "n * m = m * n" by (induct n) simp_all
   show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
-  assume "n + m = n + q" thus "m = q" by (induct n) simp_all
 qed
 
 end
@@ -355,7 +353,7 @@
   by (fact add_diff_cancel_right')
 
 lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
-  by (fact comm_monoid_diff_class.add_diff_cancel_left)
+  by (fact add_diff_cancel_left)
 
 lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
   by (fact add_diff_cancel_right)

--- a/src/HOL/ex/Dedekind_Real.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -1079,11 +1079,17 @@
 lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
 by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
 
-lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
+lemma preal_add_less_cancel_left [simp]: "(T + (R::preal) < T + S) = (R < S)"
 by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
 
-lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
-by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
+lemma preal_add_less_cancel_right [simp]: "((R::preal) + T < S + T) = (R < S)"
+  using preal_add_less_cancel_left [symmetric, of R S T] by (simp add: ac_simps)
+
+lemma preal_add_le_cancel_left [simp]: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
+by (simp add: linorder_not_less [symmetric]) 
+
+lemma preal_add_le_cancel_right [simp]: "((R::preal) + T \<le> S + T) = (R \<le> S)"
+  using preal_add_le_cancel_left [symmetric, of R S T] by (simp add: ac_simps)
 
 lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
 apply (insert linorder_less_linear [of R S], safe)
@@ -1093,10 +1099,9 @@
 lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
 by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
 
-instance preal :: linordered_cancel_ab_semigroup_add
+instance preal :: linordered_ab_semigroup_add
 proof
   fix a b c :: preal
-  show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
   show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
 qed
 
@@ -1249,7 +1254,7 @@
   also have "... = x2 + (x + y1)"  by (simp add: assms)
   also have "... = (x2 + y1) + x"  by (simp add: ac_simps)
   finally have "(x1 + y2) + x = (x2 + y1) + x" .
-  thus ?thesis by (rule add_right_imp_eq)
+  thus ?thesis by (rule preal_add_right_cancel)
 qed
 
 
@@ -1361,7 +1366,7 @@
          UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
 
 lemma real_mult_commute: "(z::real) * w = w * z"
-by (cases z, cases w, simp add: real_mult ac_simps ac_simps)
+by (cases z, cases w, simp add: real_mult ac_simps)
 
 lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
 apply (cases z1, cases z2, cases z3)
@@ -1383,8 +1388,8 @@
 proof -
   have "(1::preal) < 1 + 1"
     by (simp add: preal_self_less_add_left)
-  thus ?thesis
-    by (simp add: real_zero_def real_one_def)
+  then show ?thesis
+    by (simp add: real_zero_def real_one_def neq_iff)
 qed
 
 instance real :: comm_ring_1
@@ -1451,7 +1456,7 @@
   assumes eq: "a+b = c+d" and le: "c \<le> a"
   shows "b \<le> (d::preal)"
 proof -
-  have "c+d \<le> a+d" by (simp add: le)
+  from le have "c+d \<le> a+d" by simp
   hence "a+b \<le> a+d" by (simp add: eq)
   thus "b \<le> d" by simp
 qed
@@ -1621,11 +1626,9 @@
 by (simp add: linorder_not_less [symmetric])
 
 lemma real_of_preal_zero_less: "0 < real_of_preal m"
-apply (insert preal_self_less_add_left [of 1 m])
-apply (auto simp add: real_zero_def real_of_preal_def
-                      real_less_def real_le_def ac_simps)
-apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
-apply (simp add: ac_simps)
+using preal_self_less_add_left [of 1 m]
+apply (auto simp add: real_zero_def real_of_preal_def real_less_def real_le_def ac_simps neq_iff)
+apply (metis Rep_preal_self_subset add.commute preal_le_def)
 done
 
 lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"