--- a/src/HOL/Library/Multiset.thy Wed Apr 12 09:18:36 2023 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Apr 12 19:56:05 2023 +0200
@@ -3257,6 +3257,28 @@
shows "monotone (multp orda) (multp ordb) (image_mset f)"
by (rule monotone_on_multp_multp_image_mset[OF assms, simplified])
+lemma multp_image_mset_image_msetI:
+ assumes "multp (\<lambda>x y. R (f x) (f y)) M1 M2" and "transp R"
+ shows "multp R (image_mset f M1) (image_mset f M2)"
+proof -
+ from \<open>transp R\<close> have "transp (\<lambda>x y. R (f x) (f y))"
+ by (auto intro: transpI dest: transpD)
+ with \<open>multp (\<lambda>x y. R (f x) (f y)) M1 M2\<close> obtain I J K where
+ "M2 = I + J" and "M1 = I + K" and "J \<noteq> {#}" and "\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)"
+ using multp_implies_one_step by blast
+
+ have "multp R (image_mset f I + image_mset f K) (image_mset f I + image_mset f J)"
+ proof (rule one_step_implies_multp)
+ show "image_mset f J \<noteq> {#}"
+ by (simp add: \<open>J \<noteq> {#}\<close>)
+ next
+ show "\<forall>k\<in>#image_mset f K. \<exists>j\<in>#image_mset f J. R k j"
+ by (simp add: \<open>\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)\<close>)
+ qed
+ thus ?thesis
+ by (simp add: \<open>M1 = I + K\<close> \<open>M2 = I + J\<close>)
+qed
+
lemma multp_image_mset_image_msetD:
assumes
"multp R (image_mset f A) (image_mset f B)" and