author desharna Sat, 27 Nov 2021 10:28:48 +0100 changeset 74863 691131ce4641 parent 74862 aa51e974b688 child 74864 c256bba593f3
```--- 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:```