# HG changeset patch
# User desharna
# Date 1653037713 -7200
# Node ID cbf01167723594d0acc992e1e0817d8bf2b962f9
# Parent  91c16c5ad3e95efe98c0b29043ee74e4b8dc19ca
added lemmas filter_mset_cong{0,}

diff -r 91c16c5ad3e9 -r cbf011677235 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 17 14:10:14 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri May 20 11:08:33 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>