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\