# HG changeset patch
# User desharna
# Date 1637845371 -3600
# Node ID ba59c691b3ee1d4e67df1f8c41a77810c700846a
# Parent  b65336541c19a54c88e2abdef94eef9834c96556
added asymp_{less,greater} to preorder and moved mult1_lessE out

diff -r b65336541c19 -r ba59c691b3ee NEWS
--- 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)
 -------------------------------------
diff -r b65336541c19 -r ba59c691b3ee src/HOL/Library/Multiset.thy
--- 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
 
diff -r b65336541c19 -r ba59c691b3ee src/HOL/Library/Multiset_Order.thy
--- 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"
diff -r b65336541c19 -r ba59c691b3ee src/HOL/Relation.thy
--- 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"