# HG changeset patch # User desharna # Date 1677151906 -3600 # Node ID 42accfbf4d850f906928972185cb2df08d2e637e # Parent c6e2c7887d4700f2ca1561832a4ab7956ea7e48f added lemmas multpDM_mono_strong and multpHO_mono_strong diff -r c6e2c7887d47 -r 42accfbf4d85 NEWS --- a/NEWS Wed Feb 22 22:01:26 2023 +0000 +++ b/NEWS Thu Feb 23 12:31:46 2023 +0100 @@ -217,6 +217,8 @@ asymp_multpHO asymp_not_liftable_to_multpHO irreflp_on_multpHO[simp] + multpDM_mono_strong + multpHO_mono_strong multpHO_plus_plus[simp] totalp_multpDM totalp_multpHO diff -r c6e2c7887d47 -r 42accfbf4d85 src/HOL/Library/Multiset_Order.thy --- a/src/HOL/Library/Multiset_Order.thy Wed Feb 22 22:01:26 2023 +0000 +++ b/src/HOL/Library/Multiset_Order.thy Thu Feb 23 12:31:46 2023 +0100 @@ -142,6 +142,19 @@ unfolding multp\<^sub>H\<^sub>O_def by simp +subsubsection \Monotonicity\ + +lemma multp\<^sub>D\<^sub>M_mono_strong: + "multp\<^sub>D\<^sub>M R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>D\<^sub>M S M1 M2" + unfolding multp\<^sub>D\<^sub>M_def + by (metis add_diff_cancel_left' in_diffD subset_mset.diff_add) + +lemma multp\<^sub>H\<^sub>O_mono_strong: + "multp\<^sub>H\<^sub>O R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>H\<^sub>O S M1 M2" + unfolding multp\<^sub>H\<^sub>O_def + by (metis count_inI less_zeroE) + + subsubsection \Properties of Preorders\ lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"