# HG changeset patch
# User desharna
# Date 1683559593 -7200
# Node ID bdb5de00379a2fdf588fdfe701ca0cf53a195f3d
# Parent  e30a56be9c7bdfb154ad74760aa2a2617c5ed07f# Parent  515a69e976c3957a3c3b9a409af5b245e9843b78
merged

diff -r e30a56be9c7b -r bdb5de00379a NEWS
--- a/NEWS	Sun May 07 22:51:23 2023 +0200
+++ b/NEWS	Mon May 08 17:26:33 2023 +0200
@@ -238,6 +238,8 @@
   - Used transp_on and reorder assumptions of lemmas bex_least_element and
     bex_greatest_element. Minor INCOMPATIBILITIES.
   - Added lemmas.
+      count_minus_inter_lt_count_minus_inter_iff
+      minus_inter_eq_minus_inter_iff
       mult_mono_strong
       multeqp_code_iff_reflclp_multp
       multp_code_iff_multp
@@ -254,10 +256,14 @@
   - Added lemmas.
       asymp_multpHO
       asymp_not_liftable_to_multpHO
+      asymp_on_multpHO
       irreflp_on_multpHO[simp]
       multpDM_mono_strong
       multpDM_plus_plusI[simp]
       multpHO_double_double[simp]
+      multpHO_iff_set_mset_lessHO_set_mset
+      multpHO_implies_one_step_strong
+      multpHO_minus_inter_minus_inter_iff
       multpHO_mono_strong
       multpHO_plus_plus[simp]
       multpHO_repeat_mset_repeat_mset[simp]
diff -r e30a56be9c7b -r bdb5de00379a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun May 07 22:51:23 2023 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon May 08 17:26:33 2023 +0200
@@ -375,6 +375,15 @@
   "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
   by auto
 
+lemma count_minus_inter_lt_count_minus_inter_iff:
+  "count (M2 - M1) y < count (M1 - M2) y \<longleftrightarrow> y \<in># M1 - M2"
+  by (meson count_greater_zero_iff gr_implies_not_zero in_diff_count leI order.strict_trans2
+      order_less_asym)
+
+lemma minus_inter_eq_minus_inter_iff:
+  "(M1 - M2) = (M2 - M1) \<longleftrightarrow> set_mset (M1 - M2) = set_mset (M2 - M1)"
+  by (metis add.commute count_diff count_eq_zero_iff diff_add_zero in_diff_countE multiset_eq_iff)
+
 
 subsubsection \<open>Min and Max\<close>
 
diff -r e30a56be9c7b -r bdb5de00379a src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sun May 07 22:51:23 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Mon May 08 17:26:33 2023 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Library/Multiset_Order.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Author:     Martin Desharnais, MPI-INF Saarbruecken
 *)
 
 section \<open>More Theorems about the Multiset Order\<close>
@@ -177,6 +178,36 @@
   unfolding multp\<^sub>H\<^sub>O_def
   by (simp add: leD mset_subset_eq_count)
 
+lemma multp\<^sub>H\<^sub>O_implies_one_step_strong:
+  assumes "multp\<^sub>H\<^sub>O R A B"
+  defines "J \<equiv> B - A" and "K \<equiv> A - B"
+  shows "J \<noteq> {#}" and "\<forall>k \<in># K. \<exists>x \<in># J. R k x"
+proof -
+  show "J \<noteq> {#}"
+  using \<open>multp\<^sub>H\<^sub>O R A B\<close>
+  by (metis Diff_eq_empty_iff_mset J_def add.right_neutral multp\<^sub>D\<^sub>M_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M
+      multp\<^sub>H\<^sub>O_plus_plus subset_mset.add_diff_inverse subset_mset.le_zero_eq)
+
+  show "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x"
+    using \<open>multp\<^sub>H\<^sub>O R A B\<close>
+    by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def)
+qed
+
+lemma multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff:
+  fixes M1 M2 :: "_ multiset"
+  shows "multp\<^sub>H\<^sub>O R (M1 - M2) (M2 - M1) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
+  by (metis diff_intersect_left_idem multiset_inter_commute multp\<^sub>H\<^sub>O_plus_plus
+      subset_mset.add_diff_inverse subset_mset.inf.cobounded1)
+
+lemma multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset:
+  "multp\<^sub>H\<^sub>O R M1 M2 \<longleftrightarrow> (set_mset (M1 - M2) \<noteq> set_mset (M2 - M1) \<and>
+    (\<forall>y \<in># M1 - M2. (\<exists>x \<in># M2 - M1. R y x)))"
+  unfolding multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff[of R M1 M2, symmetric]
+  unfolding multp\<^sub>H\<^sub>O_def
+  unfolding count_minus_inter_lt_count_minus_inter_iff
+  unfolding minus_inter_eq_minus_inter_iff
+  by auto
+
 
 subsubsection \<open>Monotonicity\<close>
 
@@ -232,11 +263,45 @@
 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_on_multp\<^sub>H\<^sub>O:
+  assumes "asymp_on A R" and "transp_on A R" and
+    B_sub_A: "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
+  shows "asymp_on B (multp\<^sub>H\<^sub>O R)"
+proof (rule asymp_onI)
+  fix M1 M2 :: "'a multiset"
+  assume "M1 \<in> B" "M2 \<in> B" "multp\<^sub>H\<^sub>O R M1 M2"
+
+  from \<open>transp_on A R\<close> B_sub_A have tran: "transp_on (set_mset (M1 - M2)) R"
+    using \<open>M1 \<in> B\<close>
+    by (meson in_diffD subset_eq transp_on_subset)
+
+  from \<open>asymp_on A R\<close> B_sub_A have asym: "asymp_on (set_mset (M1 - M2)) R"
+    using \<open>M1 \<in> B\<close>
+    by (meson in_diffD subset_eq asymp_on_subset)
+
+  show "\<not> multp\<^sub>H\<^sub>O R M2 M1"
+  proof (cases "M1 - M2 = {#}")
+    case True
+    then show ?thesis
+      using multp\<^sub>H\<^sub>O_implies_one_step_strong(1) by metis
+  next
+    case False
+    hence "\<exists>m\<in>#M1 - M2. \<forall>x\<in>#M1 - M2. x \<noteq> m \<longrightarrow> \<not> R m x"
+      using Finite_Set.bex_max_element[of "set_mset (M1 - M2)" R, OF finite_set_mset _ tran asym]
+      by simp
+    with \<open>transp_on A R\<close> B_sub_A have "\<exists>y\<in>#M2 - M1. \<forall>x\<in>#M1 - M2. \<not> R y x"
+      using \<open>multp\<^sub>H\<^sub>O R M1 M2\<close>[THEN multp\<^sub>H\<^sub>O_implies_one_step_strong(2)]
+      using asym[THEN irreflp_on_if_asymp_on, THEN irreflp_onD]
+      by (metis \<open>M1 \<in> B\<close> \<open>M2 \<in> B\<close> in_diffD subsetD transp_onD)
+    thus ?thesis
+      unfolding multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset by simp
+  qed
+qed
+
 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)
+  using assms asymp_on_multp\<^sub>H\<^sub>O[of UNIV, simplified] by metis
 
 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)"