--- a/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:13 2016 +0100
@@ -1738,6 +1738,10 @@
"(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}"
by (metis image_mset_cong split_cong)
+lemma image_mset_const_eq:
+ "{#c. a \<in># M#} = replicate_mset (size M) c"
+ by (induct M) simp_all
+
subsection \<open>Further conversions\<close>
@@ -2310,6 +2314,9 @@
translations
"\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
+lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
+ by (simp add: image_mset_const_eq)
+
lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
assumes "A \<subseteq># B"
shows "prod_mset A dvd prod_mset B"