# HG changeset patch
# User desharna
# Date 1638005328 -3600
# Node ID 691131ce4641a268ee32178ab5111735042292c4
# Parent  aa51e974b68876e2ff14677b0926db21927e99c4
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp

diff -r aa51e974b688 -r 691131ce4641 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:22:42 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:28:48 2021 +0100
@@ -3140,6 +3140,11 @@
   qed
 qed
 
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+  using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+    folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+  by blast
+
 lemma multeqp_code_iff_reflcl_mult:
   assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
   shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
@@ -3154,6 +3159,12 @@
   thus ?thesis using multp_code_iff_mult[OF assms] by simp
 qed
 
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+  using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+    folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+  by blast
+
+
 subsubsection \<open>Partial-order properties\<close>
 
 lemma mult1_lessE: