src/HOL/Library/Multiset.thy

   then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
     by (simp add: \<open>b \<noteq> c\<close>)
   then show ?thesis using B by simp
 qed
 
+lemma add_mset_eq_singleton_iff[iff]:
+  "add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y"
+  by auto
+
 
 subsubsection \<open>Pointwise ordering induced by count\<close>
 
 definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
   where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"

 lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
   by (auto simp: subset_mset_def elim: mset_add)
 
 lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
   by (auto simp: multiset_eq_iff subseteq_mset_def)
+
+lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b"
+proof
+  assume A: "add_mset a M \<subseteq># {#b#}"
+  then have \<open>a = b\<close>
+    by (auto dest: mset_subset_eq_insertD)
+  then show "M={#} \<and> a=b"
+    using A by (simp add: mset_subset_eq_add_mset_cancel)
+qed simp
 
 
 subsubsection \<open>Intersection and bounded union\<close>
 
 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where

 qed
 
 lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
   by (auto simp: multiset_eq_iff)
 
+lemma
+  filter_mset_True[simp]: "{#y \<in># M. True#} = M" and
+  filter_mset_False[simp]: "{#y \<in># M. False#} = {#}"
+  by (auto simp: multiset_eq_iff)
+
 
 subsubsection \<open>Size\<close>
 
 definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
 

 by (induction M) auto
 
 lemma sum_mset_0_iff [simp]:
   "sum_mset M = (0::'a::canonically_ordered_monoid_add)
    \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
-by(induction M) (auto simp: add_eq_0_iff_both_eq_0)
+by(induction M) auto
 
 lemma sum_mset_diff:
   fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
   shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
   by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)

 qed
 
 lemma size_mset_set [simp]: "size (mset_set A) = card A"
 by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
 
+lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs"
+  by (induction xs) auto
+
 syntax (ASCII)
   "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
 syntax
   "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
 translations

 proof -
   from assms have "image_mset normalize A = A"
     by (induct A) simp_all
   then show ?thesis by (simp add: normalize_prod_mset)
 qed
+
+lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs"
+  by (induct xs) auto
 
 
 subsection \<open>Alternative representations\<close>
 
 subsubsection \<open>Lists\<close>