# HG changeset patch
# User desharna
# Date 1671525277 -3600
# Node ID b5f4ae037fe2b78242440a5681b830713e10b582
# Parent  91d2903bfbcbd25ba92c4beef3e2258624f537dd
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element

diff -r 91d2903bfbcb -r b5f4ae037fe2 NEWS
--- 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
diff -r 91d2903bfbcb -r b5f4ae037fe2 src/HOL/Library/Multiset.thy
--- 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