# 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. *) - "\x \ set_mset M. \y \ set_mset M. \z \ set_mset M. R x y \ R y z \ R x z" and + "transp_on (set_mset M) R" and "totalp_on (set_mset M) R" and "M \ {#}" shows @@ -1629,12 +1628,10 @@ thus ?case .. next case (add x M) - from add.prems(1) have transp_on_x_M_raw: "\y\#M. \z\#M. R x y \ R y z \ R x z" - by (metis insert_iff set_mset_add_mset_insert) - - from add.prems(1) have transp_on_R_M: - "\x \ set_mset M. \y \ set_mset M. \z \ set_mset M. R x y \ R y z \ R x z" - by (meson mset_subsetD multi_psub_of_add_self) + from add.prems(1) have + transp_on_x_M_raw: "\y\#M. \z\#M. R x y \ R y z \ 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: "\y \# M. x \ y \ R x y \ R y x" and