# HG changeset patch
# User desharna
# Date 1653293539 -7200
# Node ID 4117491aa7fe87b5ff1122fd5c5a40b95bab15a5
# Parent  160c9c18a707d4403eb2267010d5f8912c654c6b# Parent  cbf01167723594d0acc992e1e0817d8bf2b962f9
merged

diff -r 160c9c18a707 -r 4117491aa7fe src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat May 21 14:07:24 2022 +0000
+++ b/src/HOL/Library/Multiset.thy	Mon May 23 10:12:19 2022 +0200
@@ -1346,6 +1346,25 @@
   filter_mset_False[simp]: "{#y \<in># M. False#} = {#}"
   by (auto simp: multiset_eq_iff)
 
+lemma filter_mset_cong0:
+  assumes "\<And>x. x \<in># M \<Longrightarrow> f x \<longleftrightarrow> g x"
+  shows "filter_mset f M = filter_mset g M"
+proof (rule subset_mset.antisym; unfold subseteq_mset_def; rule allI)
+  fix x
+  show "count (filter_mset f M) x \<le> count (filter_mset g M) x"
+    using assms by (cases "x \<in># M") (simp_all add: not_in_iff)
+next
+  fix x
+  show "count (filter_mset g M) x \<le> count (filter_mset f M) x"
+    using assms by (cases "x \<in># M") (simp_all add: not_in_iff)
+qed
+
+lemma filter_mset_cong:
+  assumes "M = M'" and "\<And>x. x \<in># M' \<Longrightarrow> f x \<longleftrightarrow> g x"
+  shows "filter_mset f M = filter_mset g M'"
+  unfolding \<open>M = M'\<close>
+  using assms by (auto intro: filter_mset_cong0)
+
 
 subsubsection \<open>Size\<close>