Quelle  Multiset_Order.thy   Sprache: Isabelle

(*  Title:      HOL/Library/Multiset_Order.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

section ‹More Theorems about the Multiset Order›

theory Multiset_Order
imports Multiset
begin

subsection ‹Alternative Characterizations›

subsubsection ‹The Dershowitz--Manna Ordering›

definition multp🚫D🚫M where
  "multp\<^sub>D\<^sub>M r M N \
   (∃X Y. X ≠ {#} ∧ X ⊆# N ∧ M = (N - X) + Y ∧ (∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ r k a)))"

lemma multp🚫D🚫M_imp_multp:
  "multp\<^sub>D\<^sub>M r M N \ multp r M N"
proof -
  assume "multp\<^sub>D\<^sub>M r M N"
  then obtain X Y where
    "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ r k a)"
    unfolding multp🚫D🚫M_def by blast
  then have "multp r (N - X + Y) (N - X + X)"
    by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
  with ‹M = N - X + Y› ‹X ⊆# N› show "multp r M N"
    by (metis subset_mset.diff_add)
qed

subsubsection ‹The Huet--Oppen Ordering›

definition multp🚫H🚫O where
  "multp\<^sub>H\<^sub>O r M N \ M \ N \ (\y. count N y < count M y \ (\x. r y x \ count M x < count N x))"

lemma multp_imp_multp🚫H🚫O:
  assumes "asymp r" and "transp r"
  shows "multp r M N \ multp\<^sub>H\<^sub>O r M N"
  unfolding multp_def mult_def
proof (induction rule: trancl_induct)
  case (base P)
  then show ?case
    using ‹asymp r›
    by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp🚫H🚫O_def split: if_splits
        dest!: Suc_lessD)
next
  case (step N P)
  from step(3) have "M \ N" and
    **: "\y. count N y < count M y \ (\x. r y x \ count M x < count N x)"
    by (simp_all add: multp🚫H🚫O_def)
  from step(2) obtain M0 a K where
    *: "P = add_mset a M0" "N = M0 + K" "a \# K" "\b. b \# K \ r b a"
    using ‹asymp r› by (auto elim: mult1_lessE)
  from ‹M ≠ N› ** *(1,2,3) have "M \ P"
    using *(4) ‹asymp r›
    by (metis asympD add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
        count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
  moreover
  have count_a: "\z. r a z \ count M z < count P z" if "count P a \ count M a"
  proof -
    from ‹a ∉# K› and that have "count N a < count M a"
      unfolding *(1,2) by (auto simp add: not_in_iff)
    with ** obtain z where z: "r a z" "count M z < count N z"
      by blast
    with * have "count N z \ count P z"
      using ‹asymp r›
      by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
          diff_single_trivial in_diff_count not_le_imp_less)
    with z show ?thesis by auto
  qed
  have "\x. r y x \ count M x < count P x" if count_y: "count P y < count M y" for y
  proof (cases "y = a")
    case True
    with count_y count_a show ?thesis by auto
  next
    case False
    show ?thesis
    proof (cases "y \# K")
      case True
      with *(4) have "r y a" by simp
      then show ?thesis
        by (cases "count P a \ count M a") (auto dest: count_a intro: ‹transp r›[THEN transpD])
    next
      case False
      with ‹y ≠ a› have "count P y = count N y" unfolding *(1,2)
        by (simp add: not_in_iff)
      with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
      show ?thesis
      proof (cases "z \# K")
        case True
        with *(4) have "r z a" by simp
        with z(1) show ?thesis
          by (cases "count P a \ count M a") (auto dest!: count_a intro: ‹transp r›[THEN transpD])
      next
        case False
        with ‹a ∉# K› have "count N z \ count P z" unfolding *
          by (auto simp add: not_in_iff)
        with z show ?thesis by auto
      qed
    qed
  qed
  ultimately show ?case unfolding multp🚫H🚫O_def by blast
qed

lemma multp🚫H🚫O_imp_multp🚫D🚫M: "multp\<^sub>H\<^sub>O r M N \ multp\<^sub>D\<^sub>M r M N"
unfolding multp🚫D🚫M_def
proof (intro iffI exI conjI)
  assume "multp\<^sub>H\<^sub>O r M N"
  then obtain z where z: "count M z < count N z"
    unfolding multp🚫H🚫O_def by (auto simp: multiset_eq_iff nat_neq_iff)
  define X where "X = N - M"
  define Y where "Y = M - N"
  from z show "X \ {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
  from z show "X \# N" unfolding X_def by auto
  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
  show "\k. k \# Y \ (\a. a \# X \ r k a)"
  proof (intro allI impI)
    fix k
    assume "k \# Y"
    then have "count N k < count M k" unfolding Y_def
      by (auto simp add: in_diff_count)
    with ‹multp🚫H🚫O r M N› obtain a where "r k a" and "count M a < count N a"
      unfolding multp🚫H🚫O_def by blast
    then show "\a. a \# X \ r k a" unfolding X_def
      by (auto simp add: in_diff_count)
  qed
qed

lemma multp_eq_multp🚫D🚫M: "asymp r \ transp r \ multp r = multp\<^sub>D\<^sub>M r"
  using multp🚫D🚫M_imp_multp multp_imp_multp🚫H🚫O[THEN multp🚫H🚫O_imp_multp🚫D🚫M]
  by blast

lemma multp_eq_multp🚫H🚫O: "asymp r \ transp r \ multp r = multp\<^sub>H\<^sub>O r"
  using multp🚫H🚫O_imp_multp🚫D🚫M[THEN multp🚫D🚫M_imp_multp] multp_imp_multp🚫H🚫O
  by blast

lemma multp🚫D🚫M_plus_plusI[simp]:
  assumes "multp\<^sub>D\<^sub>M R M1 M2"
  shows "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
proof -
  from assms obtain X Y where
    "X \ {#}" and "X \# M2" and "M1 = M2 - X + Y" and "\k. k \# Y \ (\a. a \# X \ R k a)"
  unfolding multp🚫D🚫M_def by auto

  show "multp\<^sub>D\<^sub>M R (M + M1) (M + M2)"
    unfolding multp🚫D🚫M_def
  proof (intro exI conjI)
    show "X \ {#}"
      using ‹X ≠ {#}› by simp
  next
    show "X \# M + M2"
      using ‹X ⊆# M2›
      by (simp add: subset_mset.add_increasing)
  next
    show "M + M1 = M + M2 - X + Y"
      using ‹X ⊆# M2› ‹M1 = M2 - X + Y›
      by (metis multiset_diff_union_assoc union_assoc)
  next
    show "\k. k \# Y \ (\a. a \# X \ R k a)"
      using ‹∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ R k a)› by simp
  qed
qed

lemma multp🚫H🚫O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \ multp\<^sub>H\<^sub>O R M1 M2"
  unfolding multp🚫H🚫O_def by simp

lemma strict_subset_implies_multp🚫D🚫M: "A \# B \ multp\<^sub>D\<^sub>M r A B"
  unfolding multp🚫D🚫M_def
  by (metis add.right_neutral add_diff_cancel_right' empty_iff mset_subset_eq_add_right
      set_mset_empty subset_mset.lessE)

lemma strict_subset_implies_multp🚫H🚫O: "A \# B \ multp\<^sub>H\<^sub>O r A B"
  unfolding multp🚫H🚫O_def
  by (simp add: leD mset_subset_eq_count)

lemma multp🚫H🚫O_implies_one_step_strong:
  assumes "multp\<^sub>H\<^sub>O R A B"
  defines "J \ B - A" and "K \ A - B"
  shows "J \ {#}" and "\k \# K. \x \# J. R k x"
proof -
  show "J \ {#}"
  using ‹multp🚫H🚫O R A B›
  by (metis Diff_eq_empty_iff_mset J_def add.right_neutral multp🚫D🚫M_def multp🚫H🚫O_imp_multp🚫D🚫M
      multp🚫H🚫O_plus_plus subset_mset.add_diff_inverse subset_mset.le_zero_eq)

  show "\k\#K. \x\#J. R k x"
    using ‹multp🚫H🚫O R A B›
    by (metis J_def K_def in_diff_count multp🚫H🚫O_def)
qed

lemma multp🚫H🚫O_minus_inter_minus_inter_iff:
  fixes M1 M2 :: "_ multiset"
  shows "multp\<^sub>H\<^sub>O R (M1 - M2) (M2 - M1) \ multp\<^sub>H\<^sub>O R M1 M2"
  by (metis diff_intersect_left_idem multiset_inter_commute multp🚫H🚫O_plus_plus
      subset_mset.add_diff_inverse subset_mset.inf.cobounded1)

lemma multp🚫H🚫O_iff_set_mset_less🚫H🚫O_set_mset:
  "multp\<^sub>H\<^sub>O R M1 M2 \ (set_mset (M1 - M2) \ set_mset (M2 - M1) \
    (∀y ∈# M1 - M2. (∃x ∈# M2 - M1. R y x)))"
  unfolding multp🚫H🚫O_minus_inter_minus_inter_iff[of R M1 M2, symmetric]
  unfolding multp🚫H🚫O_def
  unfolding count_minus_inter_lt_count_minus_inter_iff
  unfolding minus_inter_eq_minus_inter_iff
  by auto


subsubsection ‹Monotonicity›

lemma multp🚫D🚫M_mono_strong:
  "multp\<^sub>D\<^sub>M R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>D\<^sub>M S M1 M2"
  unfolding multp🚫D🚫M_def
  by (metis add_diff_cancel_left' in_diffD subset_mset.diff_add)

lemma multp🚫H🚫O_mono_strong:
  "multp\<^sub>H\<^sub>O R M1 M2 \ (\x y. x \# M1 \ y \# M2 \ R x y \ S x y) \ multp\<^sub>H\<^sub>O S M1 M2"
  unfolding multp🚫H🚫O_def
  by (metis count_inI less_zeroE)


subsubsection ‹Properties of Orders›

paragraph ‹Asymmetry›

text ‹The following lemma is a negative result stating that asymmetry of an arbitrary binary
relation cannot be simply lifted to @{const multp🚫H🚫O}. It suffices to have four distinct values to
build a counterexample.›

lemma asymp_not_liftable_to_multp🚫H🚫O:
  fixes a b c d :: 'a
  assumes "distinct [a, b, c, d]"
  shows "\ (\(R :: 'a \ 'a \ bool). asymp R \ asymp (multp\<^sub>H\<^sub>O R))"
proof -
  define R :: "'a \ 'a \ bool" where
    "R = (\x y. x = a \ y = c \ x = b \ y = d \ x = c \ y = b \ x = d \ y = a)"

  from assms(1) have "{#a, b#} \ {#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 "\ 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🚫H🚫O_def
      using ‹{#a, b#} ≠ {#c, d#}› R_def assms by auto
  next
    show "multp\<^sub>H\<^sub>O R {#c, d#} {#a, b#}"
      unfolding multp🚫H🚫O_def
      using ‹{#a, b#} ≠ {#c, d#}› R_def assms by auto
  qed
  ultimately show ?thesis
    unfolding not_all not_imp by auto
qed

text ‹However, if the binary relation is both asymmetric and transitive, then @{const multp🚫H🚫O} is
also asymmetric.›

lemma asymp_on_multp🚫H🚫O:
  assumes "asymp_on A R" and "transp_on A R" and
    B_sub_A: "\M. M \ B \ set_mset M \ A"
  shows "asymp_on B (multp\<^sub>H\<^sub>O R)"
proof (rule asymp_onI)
  fix M1 M2 :: "'a multiset"
  assume "M1 \ B" "M2 \ B" "multp\<^sub>H\<^sub>O R M1 M2"

  from ‹transp_on A R› B_sub_A have tran: "transp_on (set_mset (M1 - M2)) R"
    using ‹M1 ∈ B›
    by (meson in_diffD subset_eq transp_on_subset)

  from ‹asymp_on A R› B_sub_A have asym: "asymp_on (set_mset (M1 - M2)) R"
    using ‹M1 ∈ B›
    by (meson in_diffD subset_eq asymp_on_subset)

  show "\ multp\<^sub>H\<^sub>O R M2 M1"
  proof (cases "M1 - M2 = {#}")
    case True
    then show ?thesis
      using multp🚫H🚫O_implies_one_step_strong(1) by metis
  next
    case False
    hence "\m\#M1 - M2. \x\#M1 - M2. x \ m \ \ R m x"
      using Finite_Set.bex_max_element[of "set_mset (M1 - M2)" R, OF finite_set_mset asym tran]
      by simp
    with ‹transp_on A R› B_sub_A have "\y\#M2 - M1. \x\#M1 - M2. \ R y x"
      using ‹multp🚫H🚫O R M1 M2›[THEN multp🚫H🚫O_implies_one_step_strong(2)]
      using asym[THEN irreflp_on_if_asymp_on, THEN irreflp_onD]
      by (metis ‹M1 ∈ B› ‹M2 ∈ B› in_diffD subsetD transp_onD)
    thus ?thesis
      unfolding multp🚫H🚫O_iff_set_mset_less🚫H🚫O_set_mset by simp
  qed
qed

lemma asymp_multp🚫H🚫O:
  assumes "asymp R" and "transp R"
  shows "asymp (multp\<^sub>H\<^sub>O R)"
  using assms asymp_on_multp🚫H🚫O[of UNIV, simplified] by metis


paragraph ‹Irreflexivity›

lemma irreflp_on_multp🚫H🚫O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"
    by (simp add: irreflp_onI multp🚫H🚫O_def)


paragraph ‹Transitivity›

lemma transp_on_multp🚫H🚫O:
  assumes "asymp_on A R" and "transp_on A R" and B_sub_A: "\M. M \ B \ set_mset M \ A"
  shows "transp_on B (multp\<^sub>H\<^sub>O R)"
proof (rule transp_onI)
  from assms have "asymp_on B (multp\<^sub>H\<^sub>O R)"
    using asymp_on_multp🚫H🚫O by metis

  fix M1 M2 M3
  assume hyps: "M1 \ B" "M2 \ B" "M3 \ B" "multp\<^sub>H\<^sub>O R M1 M2" "multp\<^sub>H\<^sub>O R M2 M3"

  from assms have
    [intro]: "asymp_on (set_mset M1 \ set_mset M2) R" "transp_on (set_mset M1 \ set_mset M2) R"
    using ‹M1 ∈ B› ‹M2 ∈ B›
    by (simp_all add: asymp_on_subset transp_on_subset)

  from assms have "transp_on (set_mset M1) R"
    by (meson transp_on_subset hyps(1))

  from ‹multp🚫H🚫O R M1 M2› have
    "M1 \ M2" and
    "\y. count M2 y < count M1 y \ (\x. R y x \ count M1 x < count M2 x)"
    unfolding multp🚫H🚫O_def by simp_all

  from ‹multp🚫H🚫O R M2 M3› have
    "M2 \ M3" and
    "\y. count M3 y < count M2 y \ (\x. R y x \ count M2 x < count M3 x)"
    unfolding multp🚫H🚫O_def by simp_all

  show "multp\<^sub>H\<^sub>O R M1 M3"
  proof (rule ccontr)
    let ?P = "\x. count M3 x < count M1 x \ (\y. R x y \ count M1 y \ count M3 y)"

    assume "\ multp\<^sub>H\<^sub>O R M1 M3"
    hence "M1 = M3 \ (\x. ?P x)"
      unfolding multp🚫H🚫O_def by force
    thus False
    proof (elim disjE)
      assume "M1 = M3"
      thus False
        using ‹asymp_on B (multp🚫H🚫O R)›[THEN asymp_onD]
        using ‹M2 ∈ B› ‹M3 ∈ B› ‹multp🚫H🚫O R M1 M2› ‹multp🚫H🚫O R M2 M3›
        by metis
    next
      assume "\x. ?P x"
      hence "\x \# M1 + M2. ?P x"
        by (auto simp: count_inI)
      have "\y \# M1 + M2. ?P y \ (\z \# M1 + M2. R y z \ \ ?P z)"
      proof (rule Finite_Set.bex_max_element_with_property)
        show "\x \# M1 + M2. ?P x"
          using ‹∃x. ?P x›
          by (auto simp: count_inI)
      qed auto
      then obtain x where
        "x \# M1 + M2" and
        "count M3 x < count M1 x" and
        "\y. R x y \ count M1 y \ count M3 y" and
        "\y \# M1 + M2. R x y \ count M3 y < count M1 y \ (\z. R y z \ count M1 z < count M3 z)"
        by force

      let ?Q = "\x'. R\<^sup>=\<^sup>= x x' \ count M3 x' < count M2 x'"
      show False
      proof (cases "\x'. ?Q x'")
        case True
        have "\y \# M1 + M2. ?Q y \ (\z \# M1 + M2. R y z \ \ ?Q z)"
        proof (rule Finite_Set.bex_max_element_with_property)
          show "\x \# M1 + M2. ?Q x"
            using ‹∃x. ?Q x›
            by (auto simp: count_inI)
        qed auto
        then obtain x' where
          "x' \# M1 + M2" and
          "R\<^sup>=\<^sup>= x x'" and
          "count M3 x' < count M2 x'" and
          maximality_x': "\z \# M1 + M2. R x' z ⟶ ¬ (R🚫=🚫= x z) ∨ count M3 z ≥ count M2 z"
          by (auto simp: linorder_not_less)
        with ‹multp🚫H🚫O R M2 M3› obtain y' where
          "R x' y'" and "count M2 y' < count M3 y'"
          unfolding multp🚫H🚫O_def by auto
        hence "count M2 y' < count M1 y'"
          by (smt (verit) ‹R🚫=🚫= x x'\ \\y. R x y \ count M3 y \ count M1 y\
              ‹count M3 x < count M1 x› ‹count M3 x' < count M2 x'› assms(2) count_inI
              dual_order.strict_trans1 hyps(1) hyps(2) hyps(3) less_nat_zero_code B_sub_A subsetD
              sup2E transp_onD)
        with ‹multp🚫H🚫O R M1 M2› obtain y'' where
          "R y' y''" and "count M1 y'' < count M2 y''"
          unfolding multp🚫H🚫O_def by auto
        hence "count M3 y'' < count M2 y''"
          by (smt (verit, del_insts) ‹R x' y'› ‹R🚫=🚫= x x'\ \\y. R x y \ count M3 y \ count M1 y\
              ‹count M2 y' < count M3 y'› ‹count M3 x < count M1 x› ‹count M3 x' < count M2 x'›
              assms(2) count_greater_zero_iff dual_order.strict_trans1 hyps(1) hyps(2) hyps(3)
              less_nat_zero_code linorder_not_less B_sub_A subset_iff sup2E transp_onD)

        moreover have "count M2 y'' \ count M3 y''"
        proof -
          have "y'' \# M1 + M2"
            by (metis ‹count M1 y'' < count M2 y''› count_inI not_less_iff_gr_or_eq union_iff)

          moreover have "R x' y''"
            by (metis ‹R x' y'› ‹R y' y''\ \count M2 y' < count M1 y'\
                ‹transp_on (set_mset M1 ∪ set_mset M2) R› ‹x' \# M1 + M2\ calculation count_inI
                nat_neq_iff set_mset_union transp_onD union_iff)

          moreover have "R\<^sup>=\<^sup>= x y''"
            using ‹R🚫=🚫= x x'\
            by (metis (mono_tags, opaque_lifting) ‹transp_on (set_mset M1 ∪ set_mset M2) R›
                ‹x ∈# M1 + M2› ‹x' \# M1 + M2\ calculation(1) calculation(2) set_mset_union sup2I1
                transp_onD transp_on_reflclp)

          ultimately show ?thesis
            using maximality_x'[rule_format, of y''] by metis
        qed

        ultimately show ?thesis
          by linarith
      next
        case False
        hence "\x'. R\<^sup>=\<^sup>= x x' \ count M2 x' \ count M3 x'"
          by auto
        hence "count M2 x \ count M3 x"
          by simp
        hence "count M2 x < count M1 x"
          using ‹count M3 x < count M1 x› by linarith
        with ‹multp🚫H🚫O R M1 M2› obtain y where
          "R x y" and "count M1 y < count M2 y"
          unfolding multp🚫H🚫O_def by auto
        hence "count M3 y < count M2 y"
          using ‹∀y. R x y ⟶ count M3 y ≤ count M1 y› dual_order.strict_trans2 by metis
        then show ?thesis
          using False ‹R x y› by auto
      qed
    qed
  qed
qed

lemma transp_multp🚫H🚫O:
  assumes "asymp R" and "transp R"
  shows "transp (multp\<^sub>H\<^sub>O R)"
  using assms transp_on_multp🚫H🚫O[of UNIV, simplified] by metis


paragraph ‹Totality›

lemma totalp_on_multp🚫D🚫M:
  "totalp_on A R \ (\M. M \ B \ set_mset M \ A) \ totalp_on B (multp\<^sub>D\<^sub>M R)"
  by (smt (verit, ccfv_SIG) count_inI in_mono multp🚫H🚫O_def multp🚫H🚫O_imp_multp🚫D🚫M not_less_iff_gr_or_eq
      totalp_onD totalp_onI)

lemma totalp_multp🚫D🚫M: "totalp R \ totalp (multp\<^sub>D\<^sub>M R)"
  by (rule totalp_on_multp🚫D🚫M[of UNIV R UNIV, simplified])

lemma totalp_on_multp🚫H🚫O:
  "totalp_on A R \ (\M. M \ B \ set_mset M \ A) \ totalp_on B (multp\<^sub>H\<^sub>O R)"
  by (smt (verit, ccfv_SIG) count_inI in_mono multp🚫H🚫O_def not_less_iff_gr_or_eq totalp_onD
      totalp_onI)

lemma totalp_multp🚫H🚫O: "totalp R \ totalp (multp\<^sub>H\<^sub>O R)"
  by (rule totalp_on_multp🚫H🚫O[of UNIV R UNIV, simplified])


paragraph ‹Type Classes›

context preorder
begin

lemma order_mult: "class.order
  (λM N. (M, N) ∈ mult {(x, y). x < y} ∨ M = N)
  (λM N. (M, N) ∈ mult {(x, y). x < y})"
  (is "class.order ?le ?less")
proof -
  have irrefl: "\M :: 'a multiset. \ ?less M M"
  proof
    fix M :: "'a multiset"
    have "trans {(x'::'a, x). x' < x}"
      by (rule transI) (blast intro: less_trans)
    moreover
    assume "(M, M) \ mult {(x, y). x < y}"
    ultimately have "\I J K. M = I + J \ M = I + K
      ∧ J ≠ {#} ∧ (∀k∈set_mset K. ∃j∈set_mset J. (k, j) ∈ {(x, y). x < y})"
      by (rule mult_implies_one_step)
    then obtain I J K where "M = I + J" and "M = I + K"
      and "J \ {#}" and "(\k\set_mset K. \j\set_mset J. (k, j) \ {(x, y). x < y})" by blast
    then have aux1: "K \ {#}" and aux2: "\k\set_mset K. \j\set_mset K. k < j" by auto
    have "finite (set_mset K)" by simp
    moreover note aux2
    ultimately have "set_mset K = {}"
      by (induct rule: finite_induct)
       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    with aux1 show False by simp
  qed
  have trans: "\K M N :: 'a multiset. ?less K M \ ?less M N \ ?less K N"
    unfolding mult_def by (blast intro: trancl_trans)
  show "class.order ?le ?less"
    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
qed

text ‹The Dershowitz--Manna ordering:›

definition less_multiset🚫D🚫M where
  "less_multiset\<^sub>D\<^sub>M M N \
   (∃X Y. X ≠ {#} ∧ X ⊆# N ∧ M = (N - X) + Y ∧ (∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)))"


text ‹The Huet--Oppen ordering:›

definition less_multiset🚫H🚫O where
  "less_multiset\<^sub>H\<^sub>O M N \ M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))"

lemma mult_imp_less_multiset🚫H🚫O:
  "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>H\<^sub>O M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_imp_multp🚫H🚫O[of "(<)"]
  by (simp add: less_multiset🚫H🚫O_def multp🚫H🚫O_def)

lemma less_multiset🚫D🚫M_imp_mult:
  "less_multiset\<^sub>D\<^sub>M M N \ (M, N) \ mult {(x, y). x < y}"
  unfolding multp_def[of "(<)", symmetric]
  by (rule multp🚫D🚫M_imp_multp[of "(<)" M N]) (simp add: less_multiset🚫D🚫M_def multp🚫D🚫M_def)

lemma less_multiset🚫H🚫O_imp_less_multiset🚫D🚫M: "less_multiset\<^sub>H\<^sub>O M N \ less_multiset\<^sub>D\<^sub>M M N"
  unfolding less_multiset🚫D🚫M_def less_multiset🚫H🚫O_def
  unfolding multp🚫D🚫M_def[symmetric] multp🚫H🚫O_def[symmetric]
  by (rule multp🚫H🚫O_imp_multp🚫D🚫M)

lemma mult_less_multiset🚫D🚫M: "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>D\<^sub>M M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multp🚫D🚫M[of "(<)", simplified]
  by (simp add: multp🚫D🚫M_def less_multiset🚫D🚫M_def)

lemma mult_less_multiset🚫H🚫O: "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>H\<^sub>O M N"
  unfolding multp_def[of "(<)", symmetric]
  using multp_eq_multp🚫H🚫O[of "(<)", simplified]
  by (simp add: multp🚫H🚫O_def less_multiset🚫H🚫O_def)

lemmas mult🚫D🚫M = mult_less_multiset🚫D🚫M[unfolded less_multiset🚫D🚫M_def]
lemmas mult🚫H🚫O = mult_less_multiset🚫H🚫O[unfolded less_multiset🚫H🚫O_def]

end

lemma less_multiset_less_multiset🚫H🚫O: "M < N \ less_multiset\<^sub>H\<^sub>O M N"
  unfolding less_multiset_def multp_def mult🚫H🚫O less_multiset🚫H🚫O_def ..

lemma less_multiset🚫D🚫M:
  "M < N \ (\X Y. X \ {#} \ X \# N \ M = N - X + Y \ (\k. k \# Y \ (\a. a \# X \ k < a)))"
  by (rule mult🚫D🚫M[folded multp_def less_multiset_def])

lemma less_multiset🚫H🚫O:
  "M < N \ M \ N \ (\y. count N y < count M y \ (\x>y. count M x < count N x))"
  by (rule mult🚫H🚫O[folded multp_def less_multiset_def])

lemma subset_eq_imp_le_multiset:
  shows "M \# N \ M \ N"
  unfolding less_eq_multiset_def less_multiset🚫H🚫O
  by (simp add: less_le_not_le subseteq_mset_def)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_right_total: "M < add_mset x M"
  unfolding less_eq_multiset_def less_multiset🚫H🚫O by simp

lemma less_eq_multiset_empty_left[simp]: "{#} \ M"
  by (simp add: subset_eq_imp_le_multiset)

lemma ex_gt_imp_less_multiset: "(\y. y \# N \ (\x. x \# M \ x < y)) \ M < N"
  unfolding less_multiset🚫H🚫O
  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)

lemma less_eq_multiset_empty_right[simp]: "M \ {#} \ \ M \ {#}"
  by (metis less_eq_multiset_empty_left antisym)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_left[simp]: "M \ {#} \ {#} < M"
  by (simp add: less_multiset🚫H🚫O)

(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "\ M < {#}"
  using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset🚫D🚫M by blast

(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P \# M \ N < P \ M - P + N < M"
  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)

instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
begin

lemma less_eq_multiset🚫H🚫O:
  "M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))"
  by (auto simp: less_eq_multiset_def less_multiset🚫H🚫O)

instance by standard (auto simp: less_eq_multiset🚫H🚫O)

lemma
  fixes M N :: "'a multiset"
  shows less_eq_multiset_plus_left: "N \ (M + N)"
    and less_eq_multiset_plus_right: "M \ (M + N)"
  by simp_all

lemma
  fixes M N :: "'a multiset"
  shows le_multiset_plus_left_nonempty: "M \ {#} \ N < M + N"
    and le_multiset_plus_right_nonempty: "N \ {#} \ M < M + N"
    by simp_all

end

lemma all_lt_Max_imp_lt_mset: "N \ {#} \ (\a \# M. a < Max (set_mset N)) \ M < N"
  by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff)

lemma lt_imp_ex_count_lt: "M < N \ \y. count M y < count N y"
  by (meson less_eq_multiset🚫H🚫O less_le_not_le)

lemma subset_imp_less_mset: "A \# B \ A < B"
  by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)

lemma image_mset_strict_mono:
  assumes mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y"
    and less: "M < N"
  shows "image_mset f M < image_mset f N"
proof -
  obtain Y X where
    y_nemp: "Y \ {#}" and y_sub_N: "Y \# N" and M_eq: "M = N - Y + X" and
    ex_y: "\x. x \# X \ (\y. y \# Y \ x < y)"
    using less[unfolded less_multiset🚫D🚫M] by blast

  have x_sub_M: "X \# M"
    using M_eq by simp

  let ?fY = "image_mset f Y"
  let ?fX = "image_mset f X"

  show ?thesis
    unfolding less_multiset🚫D🚫M
  proof (intro exI conjI)
    show "image_mset f M = image_mset f N - ?fY + ?fX"
      using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
      by (metis image_mset_Diff image_mset_union)
  next
    obtain y where y: "\x. x \# X \ y x \# Y \ x < y x"
      using ex_y by metis

    show "\fx. fx \# ?fX \ (\fy. fy \# ?fY \ fx < fy)"
    proof (intro allI impI)
      fix fx
      assume "fx \# ?fX"
      then obtain x where fx: "fx = f x" and x_in: "x \# X"
        by auto
      hence y_in: "y x \# Y" and y_gt: "x < y x"
        using y[rule_format, OF x_in] by blast+
      hence "f (y x) \# ?fY \ f x < f (y x)"
        using mono_f y_sub_N x_sub_M x_in
        by (metis image_eqI in_image_mset mset_subset_eqD)
      thus "\fy. fy \# ?fY \ fx < fy"
        unfolding fx by auto
    qed
  qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono)
qed

lemma image_mset_mono:
  assumes mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y"
    and less: "M \ N"
  shows "image_mset f M \ image_mset f N"
  by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)

lemma mset_lt_single_right_iff[simp]: "M < {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder"
proof (rule iffI)
  assume M_lt_y: "M < {#y#}"
  show "\x \# M. x < y"
  proof
    fix x
    assume x_in: "x \# M"
    hence M: "M - {#x#} + {#x#} = M"
      by (meson insert_DiffM2)
    hence "\ {#x#} < {#y#} \ x < y"
      using x_in M_lt_y
      by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans)
    also have "\ {#y#} < M"
      using M_lt_y mset_le_not_sym by blast
    ultimately show "x < y"
      by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE
        less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert
        set_mset_eq_empty_iff x_in)
  qed
next
  assume y_max: "\x \# M. x < y"
  show "M < {#y#}"
    by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max)
qed

lemma mset_le_single_right_iff[simp]:
  "M \ {#y#} \ M = {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder"
  by (meson less_eq_multiset_def mset_lt_single_right_iff)


subsubsection ‹Simplifications›

lemma multp🚫H🚫O_repeat_mset_repeat_mset[simp]:
  assumes "n \ 0"
  shows "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B) \ multp\<^sub>H\<^sub>O R A B"
proof (rule iffI)
  assume hyp: "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
  hence
    1: "repeat_mset n A \ repeat_mset n B" and
    2: "\y. n * count B y < n * count A y \ (\x. R y x \ n * count A x < n * count B x)"
    by (simp_all add: multp🚫H🚫O_def)

  from 1 ‹n ≠ 0› have "A \ B"
    by auto

  moreover from 2 ‹n ≠ 0› have "\y. count B y < count A y \ (\x. R y x \ count A x < count B x)"
    by auto

  ultimately show "multp\<^sub>H\<^sub>O R A B"
    by (simp add: multp🚫H🚫O_def)
next
  assume "multp\<^sub>H\<^sub>O R A B"
  hence 1: "A \ B" and 2: "\y. count B y < count A y \ (\x. R y x \ count A x < count B x)"
    by (simp_all add: multp🚫H🚫O_def)

  from 1 have "repeat_mset n A \ repeat_mset n B"
    by (simp add: assms repeat_mset_cancel1)

  moreover from 2 have "\y. n * count B y < n * count A y \
    (∃x. R y x ∧ n * count A x < n * count B x)"
    by auto

  ultimately show "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
    by (simp add: multp🚫H🚫O_def)
qed

lemma multp🚫H🚫O_double_double[simp]: "multp\<^sub>H\<^sub>O R (A + A) (B + B) \ multp\<^sub>H\<^sub>O R A B"
  using multp🚫H🚫O_repeat_mset_repeat_mset[of 2]
  by (simp add: numeral_Bit0)


subsection ‹Simprocs›

lemma mset_le_add_iff1:
  "j \ (i::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (repeat_mset (i-j) u + m \ n)"
proof -
  assume "j \ i"
  then have "j + (i - j) = i"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

lemma mset_le_add_iff2:
  "i \ (j::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (m \ repeat_mset (j-i) u + n)"
proof -
  assume "i \ j"
  then have "i + (j - i) = j"
    using le_add_diff_inverse by blast
  then show ?thesis
    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
qed

simproc_setup msetless_cancel
  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
   "add_mset a m < n" | "m < add_mset a n" |
   "replicate_mset p a < n" | "m < replicate_mset p a" |
   "repeat_mset p m < n" | "m < repeat_mset p n") =
  ‹K Cancel_Simprocs.less_cancel›

simproc_setup msetle_cancel
  ("(l::'a::preorder multiset) + m \ n" | "(l::'a multiset) \ m + n" |
   "add_mset a m \ n" | "m \ add_mset a n" |
   "replicate_mset p a \ n" | "m \ replicate_mset p a" |
   "repeat_mset p m \ n" | "m \ repeat_mset p n") =
  ‹K Cancel_Simprocs.less_eq_cancel›


subsection ‹Additional facts and instantiations›

lemma ex_gt_count_imp_le_multiset:
  "(\y :: 'a :: order. y \# M + N \ y \ x) \ count M x < count N x \ M < N"
  unfolding less_multiset🚫H🚫O
  by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)

lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \ x < y"
  unfolding less_multiset🚫H🚫O by simp

lemma mset_le_single_iff[iff]: "{#x#} \ {#y#} \ x \ y" for x y :: "'a::order"
  unfolding less_eq_multiset🚫H🚫O by force

instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
  by standard (metis less_eq_multiset🚫H🚫O not_less_iff_gr_or_eq)

lemma less_eq_multiset_total: "\ M \ N \ N \ M" for M N :: "'a :: linorder multiset"
  by simp

instantiation multiset :: (wellorder) wellorder
begin

lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
  unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)

instance
proof intro_classes
  fix P :: "'a multiset \ bool" and a :: "'a multiset"
  have "wfp ((<) :: 'a \ 'a \ bool)"
    using wfp_on_less .
  hence "wfp ((<) :: 'a multiset \ 'a multiset \ bool)"
    unfolding less_multiset_def by (rule wfp_multp)
  thus "(\x. (\y. y < x \ P y) \ P x) \ P a"
    unfolding wfp_on_def[of UNIV, simplified] by metis
qed

end

instantiation multiset :: (preorder) order_bot
begin

definition bot_multiset :: "'a multiset" where "bot_multiset = {#}"

instance by standard (simp add: bot_multiset_def)

end

instance multiset :: (preorder) no_top
proof standard
  fix x :: "'a multiset"
  obtain a :: 'a where True by simp
  have "x < x + (x + {#a#})"
    by simp
  then show "\y. x < y"
    by blast
qed

instance multiset :: (preorder) ordered_cancel_comm_monoid_add
  by standard

instantiation multiset :: (linorder) distrib_lattice
begin

definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where
  "inf_multiset A B = (if A < B then A else B)"

definition sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where
  "sup_multiset A B = (if B > A then B else A)"

instance
  by intro_classes (auto simp: inf_multiset_def sup_multiset_def)

end

lemma add_mset_lt_left_lt: "a < b \ add_mset a A < add_mset b A"
  by fastforce

lemma add_mset_le_left_le: "a \ b \ add_mset a A \ add_mset b A" for a :: "'a :: linorder"
  by fastforce

lemma add_mset_lt_right_lt: "A < B \ add_mset a A < add_mset a B"
  by fastforce

lemma add_mset_le_right_le: "A \ B \ add_mset a A \ add_mset a B"
  by fastforce

lemma add_mset_lt_lt_lt:
  assumes a_lt_b: "a < b" and A_le_B: "A < B"
  shows "add_mset a A < add_mset b B"
  by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])

lemma add_mset_lt_lt_le: "a < b \ A \ B \ add_mset a A < add_mset b B"
  using add_mset_lt_lt_lt le_neq_trans by fastforce

lemma add_mset_lt_le_lt: "a \ b \ A < B \ add_mset a A < add_mset b B" for a :: "'a :: linorder"
  using add_mset_lt_lt_lt by (metis add_mset_lt_right_lt le_less)

lemma add_mset_le_le_le:
  fixes a :: "'a :: linorder"
  assumes a_le_b: "a \ b" and A_le_B: "A \ B"
  shows "add_mset a A \ add_mset b B"
  by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])

lemma Max_lt_imp_lt_mset:
  assumes n_nemp: "N \ {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
  shows "M < N"
proof (cases "M = {#}")
  case m_nemp: False

  have max_n_in_n: "?max_N \# N"
    using n_nemp by simp
  have max_n_nin_m: "?max_N \# M"
    using max Max_ge leD by auto

  have "M \ N"
    using max by auto
  moreover
  have "\x > y. count M x < count N x" if "count N y < count M y" for y
  proof -
    from that have "y \# M"
      by (simp add: count_inI)
    then have "?max_M \ y"
      by simp
    then have "?max_N > y"
      using max by auto
    then show ?thesis
      using max_n_nin_m max_n_in_n count_inI by force
  qed
  ultimately show ?thesis
    unfolding less_multiset🚫H🚫O by blast
qed (auto simp: n_nemp)

end