merged

--- a/NEWS	Thu Feb 23 15:21:14 2023 +0000
+++ b/NEWS	Thu Feb 23 15:21:22 2023 +0000
@@ -217,6 +217,9 @@
       asymp_multpHO
       asymp_not_liftable_to_multpHO
       irreflp_on_multpHO[simp]
+      multpDM_mono_strong
+      multpDM_plus_plusI[simp]
+      multpHO_mono_strong
       multpHO_plus_plus[simp]
       totalp_multpDM
       totalp_multpHO

--- a/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 15:21:14 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 15:21:22 2023 +0000
@@ -138,10 +138,50 @@
   using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
   by blast
 
+lemma multp\<^sub>D\<^sub>M_plus_plusI[simp]:
+  assumes "multp\<^sub>D\<^sub>M R M1 M2"
+  shows "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
+proof -
+  from assms obtain X Y where
+    "X \<noteq> {#}" and "X \<subseteq># M2" and "M1 = M2 - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> R k a)"
+  unfolding multp\<^sub>D\<^sub>M_def by auto
+
+  show "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
+    unfolding multp\<^sub>D\<^sub>M_def
+  proof (intro exI conjI)
+    show "X \<noteq> {#}"
+      using \<open>X \<noteq> {#}\<close> by simp
+  next
+    show "X \<subseteq># M + M2"
+      using \<open>X \<subseteq># M2\<close>
+      by (simp add: subset_mset.add_increasing)
+  next
+    show "M + M1 = M + M2 - X + Y"
+      using \<open>X \<subseteq># M2\<close> \<open>M1 = M2 - X + Y\<close>
+      by (metis multiset_diff_union_assoc union_assoc)
+  next
+    show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> R k a)"
+      using \<open>\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> R k a)\<close> by simp
+  qed
+qed
+
 lemma multp\<^sub>H\<^sub>O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
   unfolding multp\<^sub>H\<^sub>O_def by simp
 
 
+subsubsection \<open>Monotonicity\<close>
+
+lemma multp\<^sub>D\<^sub>M_mono_strong:
+  "multp\<^sub>D\<^sub>M R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>D\<^sub>M S M1 M2"
+  unfolding multp\<^sub>D\<^sub>M_def
+  by (metis add_diff_cancel_left' in_diffD subset_mset.diff_add)
+
+lemma multp\<^sub>H\<^sub>O_mono_strong:
+  "multp\<^sub>H\<^sub>O R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>H\<^sub>O S M1 M2"
+  unfolding multp\<^sub>H\<^sub>O_def
+  by (metis count_inI less_zeroE)
+
+
 subsubsection \<open>Properties of Preorders\<close>
 
 lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"