--- a/NEWS Sun Jul 07 22:25:34 2024 +0100
+++ b/NEWS Mon Jul 08 10:08:07 2024 +0200
@@ -38,6 +38,8 @@
wfP_less_multiset ~> wfp_less_multiset
wfP_multp ~> wfp_multp
wfP_subset_mset ~> wfp_subset_mset
+ - Added lemmas.
+ minus_add_mset_if_not_in_lhs[simp]
* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and supposed to
be removed in a furure release. Minor INCOMPATIBILITY. Import
--- a/src/HOL/Library/Multiset.thy Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Jul 08 10:08:07 2024 +0200
@@ -1729,6 +1729,9 @@
finally show ?thesis by simp
qed
+lemma minus_add_mset_if_not_in_lhs[simp]: "x \<notin># A \<Longrightarrow> A - add_mset x B = A - B"
+ by (metis diff_intersect_left_idem inter_add_right1)
+
lemma count_image_mset:
\<open>count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)\<close>
proof (induction A)