--- 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.
--- 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
+
--- 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
+
--- 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
+