# HG changeset patch
# User desharna
# Date 1741090231 -3600
# Node ID eee83daed0d7242fc256dc120c165409b4bdee8f
# Parent  3e972fc58373ef1089e223554d656c29836d52c1
added lemmas filter_mset_mono_strong, filter_mset_sum_list, set_mset_sum_list[simp] (thanks to Manuel Eberl)

diff -r 3e972fc58373 -r eee83daed0d7 NEWS
--- a/NEWS	Tue Mar 04 10:15:29 2025 +0100
+++ b/NEWS	Tue Mar 04 13:10:31 2025 +0100
@@ -14,6 +14,12 @@
       monotone_on_inf_fun
       monotone_on_sup_fun
 
+* Theory "HOL-Library.Multiset":
+  - Added lemmas.
+      filter_mset_mono_strong
+      filter_mset_sum_list
+      set_mset_sum_list[simp]
+
 
 New in Isabelle2025 (March 2025)
 --------------------------------
diff -r 3e972fc58373 -r eee83daed0d7 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Mar 04 10:15:29 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 04 13:10:31 2025 +0100
@@ -1299,10 +1299,16 @@
 lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   by (simp add: mset_subset_eqI)
 
+lemma filter_mset_mono_strong:
+  assumes "A \<subseteq># B" "\<And>x. x \<in># A \<Longrightarrow> P x \<Longrightarrow> Q x"
+  shows   "filter_mset P A \<subseteq># filter_mset Q B"
+  by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)
+
+(* TODO: rename to filter_mset_mono_strong *)
 lemma multiset_filter_mono:
   assumes "A \<subseteq># B"
   shows "filter_mset f A \<subseteq># filter_mset f B"
-  by (metis assms filter_sup_mset subset_mset.order_iff)
+  using filter_mset_mono_strong[OF \<open>A \<subseteq># B\<close>] .
 
 lemma filter_mset_eq_conv:
   "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
@@ -2817,6 +2823,12 @@
 lemma mset_concat: "mset (concat xss) = (\<Sum>xs\<leftarrow>xss. mset xs)"
   by (induction xss) auto
 
+lemma set_mset_sum_list [simp]: "set_mset (sum_list xs) = (\<Union>x\<in>set xs. set_mset x)"
+  by (induction xs) auto
+
+lemma filter_mset_sum_list: "filter_mset P (sum_list xs) = sum_list (map (filter_mset P) xs)"
+  by (induction xs) simp_all
+
 lemma sum_mset_singleton_mset [simp]: "(\<Sum>x\<in>#A. {#f x#}) = image_mset f A"
   by (induction A) auto