diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Library/Multiset.thy Sat Nov 11 18:41:08 2017 +0000
@@ -2155,6 +2155,42 @@
"image_mset f (replicate_mset n a) = replicate_mset n (f a)"
by (induct n) simp_all
+lemma replicate_mset_msubseteq_iff:
+ "replicate_mset m a \# replicate_mset n b \ m = 0 \ a = b \ m \ n"
+ by (cases m)
+ (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+
+lemma msubseteq_replicate_msetE:
+ assumes "A \# replicate_mset n a"
+ obtains m where "m \ n" and "A = replicate_mset m a"
+proof (cases "n = 0")
+ case True
+ with assms that show thesis
+ by simp
+next
+ case False
+ from assms have "set_mset A \ set_mset (replicate_mset n a)"
+ by (rule set_mset_mono)
+ with False have "set_mset A \ {a}"
+ by simp
+ then have "\m. A = replicate_mset m a"
+ proof (induction A)
+ case empty
+ then show ?case
+ by simp
+ next
+ case (add b A)
+ then obtain m where "A = replicate_mset m a"
+ by auto
+ with add.prems show ?case
+ by (auto intro: exI [of _ "Suc m"])
+ qed
+ then obtain m where A: "A = replicate_mset m a" ..
+ with assms have "m \ n"
+ by (auto simp add: replicate_mset_msubseteq_iff)
+ then show thesis using A ..
+qed
+
subsection \Big operators\