# HG changeset patch
# User haftmann
# Date 1420737809 -3600
# Node ID 8ccecf1415b03a7e8ffed95bdf1853a7f6878c27
# Parent  2b40fb12b09dac37a3171f87e1b4e95330320011
tuned order

diff -r 2b40fb12b09d -r 8ccecf1415b0 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Jan 08 18:23:27 2015 +0100
+++ b/src/HOL/Groups.thy	Thu Jan 08 18:23:29 2015 +0100
@@ -208,57 +208,6 @@
 
 end
 
-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_cancel [simp]:
-  "a - a = 0"
-proof -
-  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
-  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"
-proof -
-  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
-  then show "c = a - b" by simp
-qed
-
-end
-
 class monoid_mult = one + semigroup_mult +
   assumes mult_1_left: "1 * a  = a"
     and mult_1_right: "a * 1 = a"
@@ -319,6 +268,57 @@
 
 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_cancel [simp]:
+  "a - a = 0"
+proof -
+  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
+  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"
+proof -
+  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
+  then show "c = a - b" by simp
+qed
+
+end
+
 
 subsection {* Groups *}