# HG changeset patch
# User desharna
# Date 1637921650 -3600
# Node ID c5059f9fbfba7f9736d300cc4483b20c725ebb3d
# Parent  5280c02f29dccf0a640f5f7e87b2275c34cea001
added Multiset.multp as predicate equivalent of Multiset.mult

diff -r 5280c02f29dc -r c5059f9fbfba NEWS
--- a/NEWS	Fri Nov 26 19:44:21 2021 +0100
+++ b/NEWS	Fri Nov 26 11:14:10 2021 +0100
@@ -9,17 +9,22 @@
 
 *** HOL ***
 
-* Theory "HOL-Library.Multiset": consolidated operation and fact names
-    multp ~> multp_code
-    multeqp ~> multeqp_code
-    multp_cancel_add_mset ~> multp_cancel_add_mset0
-    multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
-    multp_code_iff ~> multp_code_iff_mult
-    multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
-  Minor INCOMPATIBILITY.
-
-* Theory "HOL-Library.Multiset": move mult1_lessE out of preorder type
-class and add explicit assumption. Minor INCOMPATIBILITY.
+* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
+  type class preorder.
+
+* Theory "HOL-Library.Multiset":
+  - Consolidated operation and fact names.
+        multp ~> multp_code
+        multeqp ~> multeqp_code
+        multp_cancel_add_mset ~> multp_cancel_add_mset0
+        multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
+        multp_code_iff ~> multp_code_iff_mult
+        multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
+    Minor INCOMPATIBILITY.
+  - Moved mult1_lessE out of preorder type class and add explicit
+    assumption. Minor INCOMPATIBILITY.
+  - Added predicate multp equivalent to set mult. Reuse name previously
+    used for what is now called multp_code. Minor INCOMPATIBILITY.
 
 
 New in Isabelle2021-1 (December 2021)
diff -r 5280c02f29dc -r c5059f9fbfba src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Nov 26 19:44:21 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Nov 26 11:14:10 2021 +0100
@@ -2798,6 +2798,9 @@
 definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   "mult r = (mult1 r)\<^sup>+"
 
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
 lemma mult1I:
   assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   shows "(N, M) \<in> mult1 r"
@@ -2810,14 +2813,14 @@
 
 lemma mono_mult1:
   assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+  unfolding mult1_def using assms by blast
 
 lemma mono_mult:
   assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+  unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+  by (simp add: mult1_def)
 
 lemma less_add:
   assumes mult1: "(N, add_mset a M0) \<in> mult1 r"