# HG changeset patch
# User desharna
# Date 1674574374 -3600
# Node ID 0e375276227b1809d9c5746cb9052765a8cb2f99
# Parent  1d5872cb52ec8ef99b0c2039ae6e1ef466913251# Parent  e06463478a3fa322dd7674e7882267a44ad4868d
merged

diff -r 1d5872cb52ec -r 0e375276227b NEWS
--- a/NEWS	Tue Jan 24 15:04:01 2023 +0000
+++ b/NEWS	Tue Jan 24 16:32:54 2023 +0100
@@ -212,6 +212,14 @@
       totalp_on_multp
       wfP_subset_mset[simp]
 
+* Theory "HOL-Library.Multiset_Order":
+  - Added lemmas.
+      irreflp_on_multpHO[simp]
+      totalp_multpDM
+      totalp_multpHO
+      totalp_on_multpDM
+      totalp_on_multpHO
+
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.
 
diff -r 1d5872cb52ec -r 0e375276227b src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Tue Jan 24 15:04:01 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Tue Jan 24 16:32:54 2023 +0100
@@ -138,8 +138,28 @@
   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 irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"
+    by (simp add: irreflp_onI multp\<^sub>H\<^sub>O_def)
+
+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