# HG changeset patch
# User desharna
# Date 1676748849 -3600
# Node ID 3a2670c37e5c26c6def0e89a9cd4835c5babc3e8
# Parent  8543e6b10a569d38bdc3463ca253664ded927fb1
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO

diff -r 8543e6b10a56 -r 3a2670c37e5c NEWS
--- a/NEWS	Sat Feb 18 18:10:05 2023 +0000
+++ b/NEWS	Sat Feb 18 20:34:09 2023 +0100
@@ -216,6 +216,8 @@
 
 * Theory "HOL-Library.Multiset_Order":
   - Added lemmas.
+      asymp_multpHO
+      asymp_not_liftable_to_multpHO
       irreflp_on_multpHO[simp]
       multpHO_plus_plus[simp]
       totalp_multpDM
diff -r 8543e6b10a56 -r 3a2670c37e5c src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sat Feb 18 18:10:05 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Sat Feb 18 20:34:09 2023 +0100
@@ -147,6 +147,48 @@
 lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"
     by (simp add: irreflp_onI multp\<^sub>H\<^sub>O_def)
 
+text \<open>The following lemma is a negative result stating that asymmetry of an arbitrary binary
+relation cannot be simply lifted to @{const multp\<^sub>H\<^sub>O}. It suffices to have four distinct values to
+build a counterexample.\<close>
+
+lemma asymp_not_liftable_to_multp\<^sub>H\<^sub>O:
+  fixes a b c d :: 'a
+  assumes "distinct [a, b, c, d]"
+  shows "\<not> (\<forall>(R :: 'a \<Rightarrow> 'a \<Rightarrow> bool). asymp R \<longrightarrow> asymp (multp\<^sub>H\<^sub>O R))"
+proof -
+  define R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+    "R = (\<lambda>x y. x = a \<and> y = c \<or> x = b \<and> y = d \<or> x = c \<and> y = b \<or> x = d \<and> y = a)"
+
+  from assms(1) have "{#a, b#} \<noteq> {#c, d#}"
+    by (metis add_mset_add_single distinct.simps(2) list.set(1) list.simps(15) multi_member_this
+        set_mset_add_mset_insert set_mset_single)
+
+  from assms(1) have "asymp R"
+    by (auto simp: R_def intro: asymp_onI)
+  moreover have "\<not> asymp (multp\<^sub>H\<^sub>O R)"
+    unfolding asymp_on_def Set.ball_simps not_all not_imp not_not
+  proof (intro exI conjI)
+    show "multp\<^sub>H\<^sub>O R {#a, b#} {#c, d#}"
+      unfolding multp\<^sub>H\<^sub>O_def
+      using \<open>{#a, b#} \<noteq> {#c, d#}\<close> R_def assms by auto
+  next
+    show "multp\<^sub>H\<^sub>O R {#c, d#} {#a, b#}"
+      unfolding multp\<^sub>H\<^sub>O_def
+      using \<open>{#a, b#} \<noteq> {#c, d#}\<close> R_def assms by auto
+  qed
+  ultimately show ?thesis
+    unfolding not_all not_imp by auto
+qed
+
+text \<open>However, if the binary relation is both asymmetric and transitive, then @{const multp\<^sub>H\<^sub>O} is
+also asymmetric.\<close>
+
+lemma asymp_multp\<^sub>H\<^sub>O:
+  assumes "asymp R" and "transp R"
+  shows "asymp (multp\<^sub>H\<^sub>O R)"
+  using assms
+  by (metis asymp_on_iff_irreflp_on_if_transp_on irreflp_multp multp_eq_multp\<^sub>H\<^sub>O transp_multp)
+
 lemma totalp_on_multp\<^sub>D\<^sub>M:
   "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>D\<^sub>M R)"
   by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq