--- 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)
--- 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"