# HG changeset patch
# User haftmann
# Date 1347732869 -7200
# Node ID 1ffd5a055acf65f7b7db9af05ba1246c7fd80323
# Parent  1677084562698abb87d3a47aa1ce976a67122db6
typeclass formalising bounded subtraction

diff -r 167708456269 -r 1ffd5a055acf NEWS
--- a/NEWS	Sat Sep 15 20:13:25 2012 +0200
+++ b/NEWS	Sat Sep 15 20:14:29 2012 +0200
@@ -47,6 +47,9 @@
 
 *** HOL ***
 
+* Class "comm_monoid_diff" formalised properties of bounded
+subtraction, with natural numbers and multisets as typical instances.
+
 * Theory "Library/Option_ord" provides instantiation of option type
 to lattice type classes.
 
diff -r 167708456269 -r 1ffd5a055acf src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Sep 15 20:13:25 2012 +0200
+++ b/src/HOL/Groups.thy	Sat Sep 15 20:14:29 2012 +0200
@@ -213,6 +213,57 @@
 subclass (in comm_monoid_add) monoid_add proof
 qed (fact add.left_neutral add.right_neutral)+
 
+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"
@@ -1263,3 +1314,4 @@
 lemmas diff_def = diff_minus
 
 end
+
diff -r 167708456269 -r 1ffd5a055acf src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Sep 15 20:13:25 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Sep 15 20:14:29 2012 +0200
@@ -122,13 +122,14 @@
 
 subsubsection {* Difference *}
 
-instantiation multiset :: (type) minus
+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 ..
+instance
+by default (transfer, simp add: fun_eq_iff)+
 
 end
 
@@ -161,6 +162,7 @@
 
 lemma diff_add:
   "(M::'a multiset) - (N + Q) = M - N - Q"
+  find_theorems solves
 by (simp add: multiset_eq_iff)
 
 lemma diff_union_swap:
@@ -1913,3 +1915,4 @@
 *}
 
 end
+
diff -r 167708456269 -r 1ffd5a055acf src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Sep 15 20:13:25 2012 +0200
+++ b/src/HOL/Nat.thy	Sat Sep 15 20:14:29 2012 +0200
@@ -134,7 +134,7 @@
 
 subsection {* Arithmetic operators *}
 
-instantiation nat :: "{minus, comm_monoid_add}"
+instantiation nat :: comm_monoid_diff
 begin
 
 primrec plus_nat where
@@ -169,6 +169,10 @@
   show "(n + m) + q = n + (m + q)" by (induct n) simp_all
   show "n + m = m + n" by (induct n) simp_all
   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
@@ -1814,3 +1818,4 @@
 hide_const (open) of_nat_aux
 
 end
+