# HG changeset patch
# User desharna
# Date 1741102634 -3600
# Node ID c8ed5e759d2210a7b1c9817b41bf1a7bc42122a7
# Parent  96cca71aa2125bb823c1981af268b20ddf5b15e5
added lemma size_mset_sum_mset_conv[simp] (thanks to Manuel Eberl)

diff -r 96cca71aa212 -r c8ed5e759d22 NEWS
--- a/NEWS	Tue Mar 04 16:07:55 2025 +0100
+++ b/NEWS	Tue Mar 04 16:37:14 2025 +0100
@@ -22,6 +22,7 @@
       filter_mset_mono_strong
       filter_mset_sum_list
       set_mset_sum_list[simp]
+      size_mset_sum_mset_conv[simp]
 
 
 New in Isabelle2025 (March 2025)
diff -r 96cca71aa212 -r c8ed5e759d22 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Mar 04 16:07:55 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 04 16:37:14 2025 +0100
@@ -2844,8 +2844,14 @@
 lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
   by(induction m) auto
 
+lemma size_mset_sum_mset_conv [simp]: "size (\<Sum>\<^sub># A :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
+  by (induction A) auto
+
 lemma size_multiset_sum_mset [simp]: "size (\<Sum>X\<in>#A. X :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
-  by (induction A) auto
+  unfolding size_mset_sum_mset_conv
+  unfolding image_mset.identity
+  unfolding id_apply
+  ..
 
 lemma sum_mset_image_mset_mono_strong:
   assumes "A \<subseteq># B" and f_subeq_g: "\<And>x. x \<in># A \<Longrightarrow> f x \<subseteq># g x"