--- a/NEWS Thu Nov 25 12:19:50 2021 +0100
+++ b/NEWS Thu Nov 25 14:02:51 2021 +0100
@@ -18,6 +18,9 @@
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.
+
New in Isabelle2021-1 (December 2021)
-------------------------------------
--- a/src/HOL/Library/Multiset.thy Thu Nov 25 12:19:50 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 25 14:02:51 2021 +0100
@@ -3116,14 +3116,15 @@
subsubsection \<open>Partial-order properties\<close>
-lemma (in preorder) mult1_lessE:
- assumes "(N, M) \<in> mult1 {(a, b). a < b}"
+lemma mult1_lessE:
+ assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
- "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
+ "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
proof -
from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
- *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
- moreover from * [of a] have "a \<notin># K" by auto
+ *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+ moreover from * [of a] have "a \<notin># K"
+ using \<open>asymp r\<close> by (meson asymp.cases)
ultimately show thesis by (auto intro: that)
qed
--- a/src/HOL/Library/Multiset_Order.thy Thu Nov 25 12:19:50 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Thu Nov 25 14:02:51 2021 +0100
@@ -70,7 +70,7 @@
by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
from step(2) obtain M0 a K where
*: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
- by (blast elim: mult1_lessE)
+ by (auto elim: mult1_lessE)
from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
moreover
{ assume "count P a \<le> count M a"
--- a/src/HOL/Relation.thy Thu Nov 25 12:19:50 2021 +0100
+++ b/src/HOL/Relation.thy Thu Nov 25 14:02:51 2021 +0100
@@ -259,6 +259,17 @@
lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
by (blast intro: asymI dest: asymD)
+context preorder begin
+
+lemma asymp_less[simp]: "asymp (<)"
+ by (auto intro: asympI dual_order.asym)
+
+lemma asymp_greater[simp]: "asymp (>)"
+ by (auto intro: asympI dual_order.asym)
+
+end
+
+
subsubsection \<open>Symmetry\<close>
definition sym :: "'a rel \<Rightarrow> bool"