--- a/NEWS Thu Jul 28 20:39:51 2016 +0200
+++ b/NEWS Fri Jul 29 08:22:59 2016 +0200
@@ -433,8 +433,12 @@
linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.
INCOMPATIBILITY.
-* There are some new simplification rules about multisets and the multiset
-ordering.
+* There are some new simplification rules about multisets, the multiset
+ordering, and the subset ordering on multisets.
+INCOMPATIBILITY.
+
+* The subset ordering on multisets has now the interpretation
+ordered_ab_semigroup_monoid_add_imp_le.
INCOMPATIBILITY.
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
--- a/src/HOL/Library/Multiset.thy Thu Jul 28 20:39:51 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Jul 29 08:22:59 2016 +0200
@@ -469,9 +469,12 @@
apply (auto intro: multiset_eq_iff [THEN iffD2])
done
-interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
by standard (simp, fact mset_subset_eq_exists_conv)
+interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
+ by standard
+
lemma mset_subset_eq_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
by (fact subset_mset.add_le_cancel_right)
@@ -481,11 +484,11 @@
lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
by (fact subset_mset.add_mono)
-lemma mset_subset_eq_add_left [simp]: "(A::'a multiset) \<subseteq># A + B"
- unfolding subseteq_mset_def by auto
+lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
+ by simp
-lemma mset_subset_eq_add_right [simp]: "B \<subseteq># (A::'a multiset) + B"
- unfolding subseteq_mset_def by auto
+lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
+ by simp
lemma single_subset_iff [simp]:
"{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"