# HG changeset patch
# User desharna
# Date 1638004962 -3600
# Node ID aa51e974b68876e2ff14677b0926db21927e99c4
# Parent  74ac414618e2296b86ce44d6143fc649c03ed28c
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max

diff -r 74ac414618e2 -r aa51e974b688 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:16:46 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:22:42 2021 +0100
@@ -3039,7 +3039,7 @@
 lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
 
 
-subsection \<open>The multiset extension is cancellative for multiset union\<close>
+subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
 
 lemma mult_cancel:
   assumes "trans s" and "irrefl s"
@@ -3074,9 +3074,17 @@
   thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
 qed
 
+lemmas multp_cancel =
+  mult_cancel[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
 lemmas mult_cancel_add_mset =
   mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
 
+lemmas multp_cancel_add_mset =
+  mult_cancel_add_mset[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
 lemma mult_cancel_max0:
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
@@ -3087,6 +3095,10 @@
 
 lemmas mult_cancel_max = mult_cancel_max0[simplified]
 
+lemmas multp_cancel_max =
+  mult_cancel_max[of "{(x, y). r x y}" for r,
+    folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
 
 subsection \<open>Quasi-executable version of the multiset extension\<close>