--- a/NEWS Mon Dec 19 16:20:57 2022 +0100
+++ b/NEWS Tue Dec 20 09:34:37 2022 +0100
@@ -166,6 +166,8 @@
multp_cancel_add_mset
multp_cancel_max
multp_code_iff_mult
+ - Used transp_on in assumptions of lemmas bex_least_element and
+ bex_greatest_element. Minor INCOMPATIBILITIES.
- Added lemmas.
mult_mono_strong
multeqp_code_iff_reflclp_multp
--- a/src/HOL/Library/Multiset.thy Mon Dec 19 16:20:57 2022 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Dec 20 09:34:37 2022 +0100
@@ -1614,8 +1614,7 @@
qualified lemma
assumes
- (* FIXME: Replace by transp_on (set_mset M) R if it gets introduced. *)
- "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset M. \<forall>z \<in> set_mset M. R x y \<longrightarrow> R y z \<longrightarrow> R x z" and
+ "transp_on (set_mset M) R" and
"totalp_on (set_mset M) R" and
"M \<noteq> {#}"
shows
@@ -1629,12 +1628,10 @@
thus ?case ..
next
case (add x M)
- from add.prems(1) have transp_on_x_M_raw: "\<forall>y\<in>#M. \<forall>z\<in>#M. R x y \<and> R y z \<longrightarrow> R x z"
- by (metis insert_iff set_mset_add_mset_insert)
-
- from add.prems(1) have transp_on_R_M:
- "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset M. \<forall>z \<in> set_mset M. R x y \<longrightarrow> R y z \<longrightarrow> R x z"
- by (meson mset_subsetD multi_psub_of_add_self)
+ from add.prems(1) have
+ transp_on_x_M_raw: "\<forall>y\<in>#M. \<forall>z\<in>#M. R x y \<and> R y z \<longrightarrow> R x z" and
+ transp_on_R_M: "transp_on (set_mset M) R"
+ by (auto intro: transp_onI dest: transp_onD)
from add.prems(2) have
totalp_on_x_M_raw: "\<forall>y \<in># M. x \<noteq> y \<longrightarrow> R x y \<or> R y x" and