# HG changeset patch
# User desharna
# Date 1674481223 -3600
# Node ID 4b37cc497d7efbe9ed80e62077930cf60a6ee8d4
# Parent  e293216df99453da79c38dce22833456a1141848
added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO

diff -r e293216df994 -r 4b37cc497d7e NEWS
--- a/NEWS	Mon Jan 23 14:34:07 2023 +0100
+++ b/NEWS	Mon Jan 23 14:40:23 2023 +0100
@@ -208,6 +208,13 @@
       totalp_on_multp
       wfP_subset_mset[simp]
 
+* Theory "HOL-Library.Multiset_Order":
+  - Added lemmas.
+      totalp_multpDM
+      totalp_multpHO
+      totalp_on_multpDM
+      totalp_on_multpHO
+
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.
 
diff -r e293216df994 -r 4b37cc497d7e src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Jan 23 14:40:23 2023 +0100
@@ -138,8 +138,25 @@
   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
 
+
 subsubsection \<open>Properties of Preorders\<close>
 
+lemma totalp_on_multp\<^sub>D\<^sub>M:
+  "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>D\<^sub>M R)"
+  by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq
+      totalp_onD totalp_onI)
+
+lemma totalp_multp\<^sub>D\<^sub>M: "totalp R \<Longrightarrow> totalp (multp\<^sub>D\<^sub>M R)"
+  by (rule totalp_on_multp\<^sub>D\<^sub>M[of UNIV R UNIV, simplified])
+
+lemma totalp_on_multp\<^sub>H\<^sub>O:
+  "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>H\<^sub>O R)"
+  by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def not_less_iff_gr_or_eq totalp_onD
+      totalp_onI)
+
+lemma totalp_multp\<^sub>H\<^sub>O: "totalp R \<Longrightarrow> totalp (multp\<^sub>H\<^sub>O R)"
+  by (rule totalp_on_multp\<^sub>H\<^sub>O[of UNIV R UNIV, simplified])
+
 context preorder
 begin