# HG changeset patch
# User desharna
# Date 1666964375 -7200
# Node ID e7e8fbc898703b2e46858d51c772a2723cb35638
# Parent  5ca3391244a3072550c32d83bc74848d9357ae5b
added lemmas multp_mono_strong and mult_mono_strong

diff -r 5ca3391244a3 -r e7e8fbc89870 NEWS
--- a/NEWS	Fri Oct 28 13:18:27 2022 +0200
+++ b/NEWS	Fri Oct 28 15:39:35 2022 +0200
@@ -47,7 +47,10 @@
       wfP_pfsubset
 
 * Theory "HOL-Library.Multiset":
-  - Added lemma wfP_subset_mset[simp].
+  - Added lemmas.
+      mult_mono_strong
+      multp_mono_strong
+      wfP_subset_mset[simp]
 
 
 *** ML ***
diff -r 5ca3391244a3 -r e7e8fbc89870 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 28 13:18:27 2022 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 28 15:39:35 2022 +0200
@@ -3193,6 +3193,30 @@
 
 subsubsection \<open>Monotonicity\<close>
 
+lemma multp_mono_strong:
+  assumes "multp R M1 M2" and "transp R" and
+    S_if_R: "\<And>x y. x \<in> set_mset M1 \<Longrightarrow> y \<in> set_mset M2 \<Longrightarrow> R x y \<Longrightarrow> S x y"
+  shows "multp S M1 M2"
+proof -
+  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 k x"
+    using multp_implies_one_step[OF \<open>transp R\<close> \<open>multp R M1 M2\<close>] by auto
+  show ?thesis
+    unfolding \<open>M2 = I + J\<close> \<open>M1 = I + K\<close>
+  proof (rule one_step_implies_multp[OF \<open>J \<noteq> {#}\<close>])
+    show "\<forall>k\<in>#K. \<exists>j\<in>#J. S k j"
+      using S_if_R
+      by (metis \<open>M1 = I + K\<close> \<open>M2 = I + J\<close> \<open>\<forall>k\<in>#K. \<exists>x\<in>#J. R k x\<close> union_iff)
+  qed
+qed
+
+lemma mult_mono_strong:
+  assumes "(M1, M2) \<in> mult r" and "trans r" and
+    S_if_R: "\<And>x y. x \<in> set_mset M1 \<Longrightarrow> y \<in> set_mset M2 \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s"
+  shows "(M1, M2) \<in> mult s"
+  using assms multp_mono_strong[of "\<lambda>x y. (x, y) \<in> r" M1 M2 "\<lambda>x y. (x, y) \<in> s",
+      unfolded multp_def transp_trans_eq, simplified]
+  by blast
+
 lemma monotone_on_multp_multp_image_mset:
   assumes "monotone_on A orda ordb f" and "transp orda"
   shows "monotone_on {M. set_mset M \<subseteq> A} (multp orda) (multp ordb) (image_mset f)"