# HG changeset patch
# User desharna
# Date 1677152137 -3600
# Node ID 347d7133c1716dfa306da4c6f5672866a0803f8f
# Parent  42accfbf4d850f906928972185cb2df08d2e637e
added lemma multpDM_plus_plusI[simp]

diff -r 42accfbf4d85 -r 347d7133c171 NEWS
--- a/NEWS	Thu Feb 23 12:31:46 2023 +0100
+++ b/NEWS	Thu Feb 23 12:35:37 2023 +0100
@@ -218,6 +218,7 @@
       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
diff -r 42accfbf4d85 -r 347d7133c171 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 12:31:46 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 12:35:37 2023 +0100
@@ -138,6 +138,33 @@
   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