# HG changeset patch # User desharna # Date 1638003700 -3600 # Node ID 250ab13343095694af1d04dcfe6fac9f54d97666 # Parent c5059f9fbfba7f9736d300cc4483b20c725ebb3d added lemma mono_multp diff -r c5059f9fbfba -r 250ab1334309 NEWS --- a/NEWS Fri Nov 26 11:14:10 2021 +0100 +++ b/NEWS Sat Nov 27 10:01:40 2021 +0100 @@ -25,6 +25,7 @@ assumption. Minor INCOMPATIBILITY. - Added predicate multp equivalent to set mult. Reuse name previously used for what is now called multp_code. Minor INCOMPATIBILITY. + - Lifted multiple lemmas from mult to multp. New in Isabelle2021-1 (December 2021) diff -r c5059f9fbfba -r 250ab1334309 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Nov 26 11:14:10 2021 +0100 +++ b/src/HOL/Library/Multiset.thy Sat Nov 27 10:01:40 2021 +0100 @@ -2819,6 +2819,18 @@ assumes "r \ r'" shows "mult r \ mult r'" unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast +lemma mono_multp[mono]: "r \ r' \ multp r \ multp r'" + unfolding le_fun_def le_bool_def +proof (intro allI impI) + fix M N :: "'a multiset" + assume "\x xa. r x xa \ r' x xa" + hence "{(x, y). r x y} \ {(x, y). r' x y}" + by blast + thus "multp r M N \ multp r' M N" + unfolding multp_def + by (fact mono_mult[THEN subsetD, rotated]) +qed + lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" by (simp add: mult1_def)