--- a/src/HOL/Library/Multiset.thy Fri Oct 07 17:58:36 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 07 17:59:19 2016 +0200
@@ -656,6 +656,9 @@
lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
by (auto simp: subset_mset_def elim: mset_add)
+lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
+ by (auto simp: multiset_eq_iff subseteq_mset_def)
+
subsubsection \<open>Intersection and bounded union\<close>
@@ -749,6 +752,12 @@
qed
qed
+lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
+ by (meson disjunct_not_in union_iff)
+
+lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}"
+ by (meson disjunct_not_in union_iff)
+
lemma add_mset_inter_add_mset[simp]:
"add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)"
by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
@@ -1305,6 +1314,9 @@
qed
qed
+lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
+ by (auto simp: multiset_eq_iff)
+
subsubsection \<open>Size\<close>
@@ -1732,6 +1744,12 @@
lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
by (induct x) auto
+lemma mset_single_iff[iff]: "mset xs = {#x#} \<longleftrightarrow> xs = [x]"
+ by (cases xs) auto
+
+lemma mset_single_iff_right[iff]: "{#x#} = mset xs \<longleftrightarrow> xs = [x]"
+ by (cases xs) auto
+
lemma set_mset_mset[simp]: "set_mset (mset xs) = set xs"
by (induct xs) auto
@@ -2033,6 +2051,9 @@
lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
by (auto simp: multiset_eq_iff)
+lemma repeat_mset_eq_empty_iff: "repeat_mset n A = {#} \<longleftrightarrow> n = 0 \<or> A = {#}"
+ by (cases n) auto
+
lemma image_replicate_mset [simp]:
"image_mset f (replicate_mset n a) = replicate_mset n (f a)"
by (induct n) simp_all