--- 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 =
--- 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)
--- 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)