# 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 \<subseteq> r'" shows "mult r \<subseteq> mult r'"
   unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
 
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+  unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+  fix M N :: "'a multiset"
+  assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+  hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+    by blast
+  thus "multp r M N \<Longrightarrow> multp r' M N"
+    unfolding multp_def
+    by (fact mono_mult[THEN subsetD, rotated])
+qed
+
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)