# HG changeset patch
# User nipkow
# Date 1536836943 -7200
# Node ID 93546c85374a6cdfd4b3206eac9196eb78b550f5
# Parent  5d35fd21a0b9caeb4f12dad5453f054b1eada4e9
more simp lemmas

diff -r 5d35fd21a0b9 -r 93546c85374a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 08:36:51 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 13:09:03 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