--- a/NEWS Thu Nov 25 12:13:49 2021 +0100
+++ b/NEWS Thu Nov 25 12:19:50 2021 +0100
@@ -14,6 +14,8 @@
multeqp ~> multeqp_code
multp_cancel_add_mset ~> multp_cancel_add_mset0
multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+ multp_code_iff ~> multp_code_iff_mult
+ multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
Minor INCOMPATIBILITY.
--- a/src/HOL/Library/Multiset.thy Thu Nov 25 12:13:49 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 25 12:19:50 2021 +0100
@@ -3079,7 +3079,7 @@
(let Z = M \<inter># N; X = M - Z; Y = N - Z in
(\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
-lemma multp_code_iff:
+lemma multp_code_iff_mult:
assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
proof -
@@ -3100,7 +3100,7 @@
qed
qed
-lemma multeqp_code_iff:
+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>="
proof -
@@ -3111,10 +3111,9 @@
}
then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
- thus ?thesis using multp_code_iff[OF assms] by simp
+ thus ?thesis using multp_code_iff_mult[OF assms] by simp
qed
-
subsubsection \<open>Partial-order properties\<close>
lemma (in preorder) mult1_lessE: