# HG changeset patch
# User desharna
# Date 1638004606 -3600
# Node ID 74ac414618e2296b86ce44d6143fc649c03ed28c
# Parent  3e55e47a37e7f569bc710ea4baa1857a5a84c466
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp

diff -r 3e55e47a37e7 -r 74ac414618e2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:05:59 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:16:46 2021 +0100
@@ -2986,6 +2986,9 @@
   qed
 qed
 
+lemmas multp_implies_one_step =
+  mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
 lemma one_step_implies_mult:
   assumes
     "J \<noteq> {#}" and
@@ -3018,6 +3021,9 @@
   qed
 qed
 
+lemmas one_step_implies_multp =
+  one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
 lemma subset_implies_mult:
   assumes sub: "A \<subset># B"
   shows "(A, B) \<in> mult r"
@@ -3030,6 +3036,8 @@
     by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
 qed
 
+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>