# HG changeset patch
# User haftmann
# Date 1370198695 -7200
# Node ID 83ce5d2841e72a3b4933f0da492bac2d0ecee25d
# Parent  ca4932dad084b84b97f785bd69b7813436c9fb81
type class for confined subtraction

diff -r ca4932dad084 -r 83ce5d2841e7 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Jun 02 10:57:21 2013 +0200
+++ b/src/HOL/Groups.thy	Sun Jun 02 20:44:55 2013 +0200
@@ -658,6 +658,68 @@
 
 end
 
+class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
+  assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
+begin
+
+context
+  fixes a b
+  assumes "a \<le> b"
+begin
+
+lemma add_diff_inverse:
+  "a + (b - a) = b"
+  using `a \<le> b` by (auto simp add: le_iff_add)
+
+lemma add_diff_assoc:
+  "c + (b - a) = c + b - a"
+  using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
+
+lemma add_diff_assoc2:
+  "b - a + c = b + c - a"
+  using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
+
+lemma diff_add_assoc:
+  "c + b - a = c + (b - a)"
+  using `a \<le> b` by (simp add: add_commute add_diff_assoc)
+
+lemma diff_add_assoc2:
+  "b + c - a = b - a + c"
+  using `a \<le> b`by (simp add: add_commute add_diff_assoc)
+
+lemma diff_diff_right:
+  "c - (b - a) = c + a - b"
+  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
+
+lemma diff_add:
+  "b - a + a = b"
+  by (simp add: add_commute add_diff_inverse)
+
+lemma le_add_diff:
+  "c \<le> b + c - a"
+  by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
+
+lemma le_imp_diff_is_add:
+  "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
+  by (auto simp add: add_commute add_diff_inverse)
+
+lemma le_diff_conv2:
+  "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then have "c + a \<le> b - a + a" by (rule add_right_mono)
+  then show ?Q by (simp add: add_diff_inverse add_commute)
+next
+  assume ?Q
+  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
+  then show ?P by simp
+qed
+
+end
+
+end
+
+
 subsection {* Support for reasoning about signs *}
 
 class ordered_comm_monoid_add =
diff -r ca4932dad084 -r 83ce5d2841e7 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Jun 02 10:57:21 2013 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Jun 02 20:44:55 2013 +0200
@@ -137,17 +137,25 @@
   by (simp add: minus_multiset.rep_eq)
 
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
-by(simp add: multiset_eq_iff)
+  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
 
 lemma diff_cancel[simp]: "A - A = {#}"
-by (rule multiset_eqI) simp
+  by (fact Groups.diff_cancel)
 
 lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
-by(simp add: multiset_eq_iff)
+  by (fact add_diff_cancel_right')
 
 lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
-by(simp add: multiset_eq_iff)
+  by (fact add_diff_cancel_left')
 
+lemma diff_right_commute:
+  "(M::'a multiset) - N - Q = M - Q - N"
+  by (fact diff_right_commute)
+
+lemma diff_add:
+  "(M::'a multiset) - (N + Q) = M - N - Q"
+  by (rule sym) (fact diff_diff_add)
+  
 lemma insert_DiffM:
   "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
   by (clarsimp simp: multiset_eq_iff)
@@ -156,14 +164,6 @@
   "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
   by (clarsimp simp: multiset_eq_iff)
 
-lemma diff_right_commute:
-  "(M::'a multiset) - N - Q = M - Q - N"
-  by (auto simp add: multiset_eq_iff)
-
-lemma diff_add:
-  "(M::'a multiset) - (N + Q) = M - N - Q"
-by (simp add: multiset_eq_iff)
-
 lemma diff_union_swap:
   "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
   by (auto simp add: multiset_eq_iff)
@@ -289,6 +289,9 @@
 apply (auto intro: multiset_eq_iff [THEN iffD2])
 done
 
+instance multiset :: (type) ordered_cancel_comm_monoid_diff
+  by default (simp, fact mset_le_exists_conv)
+
 lemma mset_le_mono_add_right_cancel [simp]:
   "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
   by (fact add_le_cancel_right)
diff -r ca4932dad084 -r 83ce5d2841e7 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Jun 02 10:57:21 2013 +0200
+++ b/src/HOL/Nat.thy	Sun Jun 02 20:44:55 2013 +0200
@@ -456,7 +456,8 @@
 end
 
 instance nat :: no_top
-  by default (auto intro: less_Suc_eq_le[THEN iffD2])
+  by default (auto intro: less_Suc_eq_le [THEN iffD2])
+
 
 subsubsection {* Introduction properties *}
 
@@ -714,10 +715,9 @@
 text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
 instance nat :: linordered_semidom
 proof
-  fix i j k :: nat
   show "0 < (1::nat)" by simp
-  show "i \<le> j ==> k + i \<le> k + j" by simp
-  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
+  show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
+  show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
 qed
 
 instance nat :: no_zero_divisors
@@ -1067,6 +1067,11 @@
 lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
 
+instance nat :: ordered_cancel_comm_monoid_diff
+proof
+  show "\<And>m n :: nat. m \<le> n \<longleftrightarrow> (\<exists>q. n = m + q)" by (fact le_iff_add)
+qed
+
 lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
 by (rule le_less_trans, rule diff_le_self)