src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Apr 03 16:56:45 2017 +0200
@@ -1894,6 +1894,9 @@
   ultimately show ?case by simp
 qed
 
+lemma mset_shuffle [simp]: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
+  by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
+
 lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"
   by (induct xs) simp_all