# HG changeset patch
# User desharna
# Date 1681372417 -7200
# Node ID 9137085647ee50178efaee7c46ab0b8ab179a3c5
# Parent  8260d8971d871970b0d65e1e559de88c132c547d# Parent  d95beee6d9d755b5788680cd93ee3ffc282d21e1
merged

diff -r d95beee6d9d7 -r 9137085647ee NEWS
--- a/NEWS	Thu Apr 13 15:36:30 2023 +1000
+++ b/NEWS	Thu Apr 13 09:53:37 2023 +0200
@@ -230,6 +230,7 @@
       mult_mono_strong
       multeqp_code_iff_reflclp_multp
       multp_code_iff_multp
+      multp_image_mset_image_msetI
       multp_mono_strong
       multp_repeat_mset_repeat_msetI
       total_mult
diff -r d95beee6d9d7 -r 9137085647ee src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Apr 13 15:36:30 2023 +1000
+++ b/src/HOL/Library/Multiset.thy	Thu Apr 13 09:53:37 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