# HG changeset patch
# User nipkow
# Date 1473746360 -7200
# Node ID caae34eabcef8b45abf3fac261ff7defe58d63d4
# Parent  dca6fabd806006f5ed9ef71b7038dd884414d35a
more lemmas

diff -r dca6fabd8060 -r caae34eabcef src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 12 23:17:55 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Sep 13 07:59:20 2016 +0200
@@ -2070,6 +2070,15 @@
 
 end
 
+lemma of_nat_sum_mset [simp]:
+  "of_nat (sum_mset M) = sum_mset (image_mset of_nat M)"
+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)
+
 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"
@@ -2086,7 +2095,7 @@
 qed
 
 lemma size_mset_set [simp]: "size (mset_set A) = card A"
-  by (simp only: size_eq_sum_mset card_eq_setsum setsum_unfold_sum_mset)
+by (simp only: size_eq_sum_mset card_eq_setsum setsum_unfold_sum_mset)
 
 syntax (ASCII)
   "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
@@ -2095,6 +2104,11 @@
 translations
   "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
 
+lemma sum_mset_distrib_left:
+  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+  shows "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
+by (induction M) (simp_all add: distrib_left)
+
 abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
   where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
     could likewise refer to \<open>\<Squnion>#\<close>\<close>