# HG changeset patch
# User desharna
# Date 1720426087 -7200
# Node ID a0aa61689cdd8a81a3cc42e0c34352dfbee3cf2a
# Parent  532156e8f15f335991a61d62cdf39800e61251a1
added lemma minus_add_mset_if_not_in_lhs[simp]

diff -r 532156e8f15f -r a0aa61689cdd NEWS
--- 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
diff -r 532156e8f15f -r a0aa61689cdd src/HOL/Library/Multiset.thy
--- 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)