--- a/src/HOL/Library/Multiset.thy Thu Sep 13 11:41:39 2018 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Sep 13 15:15:50 2018 +0200
@@ -1830,7 +1830,7 @@
lemma mset_append [simp]: "mset (xs @ ys) = mset xs + mset ys"
by (induct xs arbitrary: ys) auto
-lemma mset_filter: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
+lemma mset_filter[simp]: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
by (induct xs) simp_all
lemma mset_rev [simp]:
@@ -1887,6 +1887,9 @@
apply simp
done
+lemma union_mset_compl[simp]: "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
+by (induction M) simp_all
+
lemma mset_compl_union: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
by (induct xs) auto