Theory Min_Max_Least_Greatest_Multiset

theory Min_Max_Least_Greatest_Multiset
  imports
    Relation_Reachability
    Min_Max_Least_Greatest_Set
    "HOL-Library.Multiset"
    "HOL-Library.Multiset_Order"
begin

section ‹Minimal and maximal elements›

definition is_minimal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
    is_minimal_in_mset_wrt R X = is_minimal_in_set_wrt R (set_mset X)"

definition is_maximal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
    is_maximal_in_mset_wrt R X = is_maximal_in_set_wrt R (set_mset X)"

definition is_strictly_minimal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
    is_strictly_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {# x #}. ¬ (R⇧=⇧= y x))"

definition is_strictly_maximal_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹
    is_strictly_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {# x #}. ¬ (R⇧=⇧= x y))"

context
  fixes X R
  assumes
    trans: "transp_on (set_mset X) R" and
    asym: "asymp_on (set_mset X) R"
begin


subsection ‹Conversions›

lemma is_minimal_in_mset_wrt_iff:
  "is_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. y ≠ x ⟶ ¬ R y x)"
  using is_minimal_in_set_wrt_iff[OF trans asym]
  using is_minimal_in_mset_wrt_def[OF trans asym]
  by simp

lemma "is_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. ¬ R y x)"
  unfolding is_minimal_in_mset_wrt_iff
proof (rule refl_conj_eq, rule ball_cong)
  show "set_mset X = set_mset X" ..
next
  show "⋀y. y ∈# X ⟹ (y ≠ x ⟶ ¬ R y x) = (¬ R y x)"
    using asym[THEN asymp_onD] by metis
qed

lemma is_maximal_in_mset_wrt_iff:
  "is_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. y ≠ x ⟶ ¬ R x y)"
  using is_maximal_in_set_wrt_iff[OF trans asym]
  using is_maximal_in_mset_wrt_def[OF trans asym]
  by simp

lemma "is_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X. ¬ R x y)"
  unfolding is_maximal_in_mset_wrt_iff
proof (rule refl_conj_eq, rule ball_cong)
  show "set_mset X = set_mset X" ..
next
  show "⋀y. y ∈# X ⟹ (y ≠ x ⟶ ¬ R x y) = (¬ R x y)"
    using asym[THEN asymp_onD] by metis
qed

lemma is_strictly_minimal_in_mset_wrt_iff:
  "is_strictly_minimal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X- {# x #}. ¬ R⇧=⇧= y x)"
  unfolding is_strictly_minimal_in_mset_wrt_def[OF trans asym]
  by(rule refl)

lemma is_strictly_maximal_in_mset_wrt_iff:
  "is_strictly_maximal_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X- {# x #}. ¬ R⇧=⇧= x y)"
  unfolding is_strictly_maximal_in_mset_wrt_def[OF trans asym]
  by(rule refl)

lemma is_minimal_in_mset_wrt_if_is_strictly_minimal_in_mset_wrt: 
  "is_strictly_minimal_in_mset_wrt R X x ⟹ is_minimal_in_mset_wrt R X x"
  unfolding is_minimal_in_mset_wrt_iff is_strictly_minimal_in_mset_wrt_iff
  using multi_member_split by fastforce 

lemma is_maximal_in_mset_wrt_if_is_strictly_maximal_in_mset_wrt:
  "is_strictly_maximal_in_mset_wrt R X x ⟹ is_maximal_in_mset_wrt R X x"
  unfolding is_maximal_in_mset_wrt_iff is_strictly_maximal_in_mset_wrt_iff
  using multi_member_split by fastforce


subsection ‹Existence›

lemma ex_minimal_in_mset_wrt:
  "X ≠ {#} ⟹ ∃m. is_minimal_in_mset_wrt R X m"
  using trans asym ex_minimal_in_set_wrt[of "set_mset X" R] is_minimal_in_mset_wrt_def
  by (metis finite_set_mset set_mset_eq_empty_iff)

lemma ex_maximal_in_mset_wrt:
  "X ≠ {#} ⟹ ∃m. is_maximal_in_mset_wrt R X m"
  using trans asym ex_maximal_in_set_wrt[of "set_mset X" R] is_maximal_in_mset_wrt_def
  by (metis finite_set_mset set_mset_eq_empty_iff)


subsection ‹Miscellaneous›

lemma explode_maximal_in_mset_wrt:
  assumes max: "is_maximal_in_mset_wrt R X x"
  obtains n :: nat where "replicate_mset (Suc n) x + {#y ∈# X. y ≠ x#} = X"
  using max[unfolded is_maximal_in_mset_wrt_iff]
  by (metis filter_eq_replicate_mset in_countE multiset_partition)

lemma explode_strictly_maximal_in_mset_wrt:
  assumes max: "is_strictly_maximal_in_mset_wrt R X x"
  shows "add_mset x {#y ∈# X. y ≠ x#} = X"
proof -
  have "x ∈# X" and "∀y ∈# X - {#x#}. x ≠ y"
    using max unfolding is_strictly_maximal_in_mset_wrt_iff by simp_all

  have "add_mset x (X - {#x#}) = X"
    using ‹x ∈# X› by (metis insert_DiffM)

  moreover have "{#y ∈# X. y ≠ x#} = X - {#x#}"
    using ‹∀y ∈# X - {#x#}. x ≠ y›
    by (smt (verit, best) ‹x ∈# X› add_diff_cancel_left' diff_subset_eq_self filter_mset_eq_conv
        insert_DiffM2 set_mset_add_mset_insert set_mset_empty singletonD)

  ultimately show ?thesis
    by (simp only:)
qed

end

lemma is_minimal_in_filter_mset_wrt_iff:
  assumes
    tran: "transp_on (set_mset (filter_mset P X)) R" and
    asym: "asymp_on (set_mset (filter_mset P X)) R"
  shows "is_minimal_in_mset_wrt R (filter_mset P X) x ⟷
    (x ∈# X ∧ P x ∧ (∀y ∈# X - {#x#}. P y ⟶ ¬ R y x))"
proof -
  have "is_minimal_in_mset_wrt R (filter_mset P X) x ⟷
    is_minimal_in_set_wrt R ({y ∈ set_mset X. P y}) x"
    using is_minimal_in_mset_wrt_iff[OF tran asym]
    using is_minimal_in_set_wrt_iff[OF tran asym]
    by auto
  also have "… ⟷ x ∈# X ∧ P x ∧ (∀y ∈ set_mset X - {x}. P y ⟶ ¬ R y x)"
  proof (rule is_minimal_in_set_wrt_filter_iff)
    show "transp_on {y. y ∈# X ∧ P y} R"
      using tran by simp
  next
    show "asymp_on {y. y ∈# X ∧ P y} R"
      using asym by simp
  qed
  finally show ?thesis
    by (metis (no_types, lifting) DiffD1 asym asymp_onD at_most_one_mset_mset_diff insertE
        insert_Diff is_minimal_in_mset_wrt_iff more_than_one_mset_mset_diff tran)
qed

lemma multp_if_maximal_of_lhs_is_less:
  assumes
    trans: "transp R" and
    asym: "asymp_on (set_mset M1) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    "x1 ∈# M1" and "x2 ∈# M2" and
    "is_maximal_in_mset_wrt R M1 x1" and "R x1 x2"
  shows "multp R M1 M2"
proof (rule one_step_implies_multp[of _ _ _ "{#}", simplified])
  show "M2 ≠ {#}"
    using ‹x2 ∈# M2› by auto
next
  show "∀k∈#M1. ∃j∈#M2. R k j"
    using assms
    using is_maximal_in_mset_wrt_iff[OF transp_on_subset[OF trans subset_UNIV] asym]
    by (metis Un_iff totalp_onD transpE)
qed


subsection ‹Nonuniqueness›

lemma
  fixes x :: 'a and y :: 'a
  assumes "x ≠ y"
  shows
    not_Uniq_is_minimal_in_mset_if_two_distinct_elements:
      "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
        transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
        (∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x))" and
    not_Uniq_is_maximal_in_mset_wrt_if_two_distinct_elements:
      "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
        transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
        (∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x))" and
    not_Uniq_is_strictly_minimal_in_mset_if_two_distinct_elements:
      "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
        transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
        (∃⇩≤⇩1x. is_strictly_minimal_in_mset_wrt R X x))" and
    not_Uniq_is_strictly_maximal_in_mset_wrt_if_two_distinct_elements:
      "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
        transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
        (∃⇩≤⇩1x. is_strictly_maximal_in_mset_wrt R X x))"
proof -
  let ?R = "λ_ _. False"
  let ?X = "{#x, y#}"

  have trans: "transp_on (set_mset ?X) ?R" and asym: "asymp_on (set_mset ?X) ?R"
    by (simp_all add: transp_onI asymp_onI)

  have "is_minimal_in_mset_wrt ?R ?X x" and "is_minimal_in_mset_wrt ?R ?X y"
    using is_minimal_in_mset_wrt_iff[OF trans asym] by simp_all

  thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
    transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
    (∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x))"
    using ‹x ≠ y› trans asym
    by (metis Uniq_D)

  have "is_maximal_in_mset_wrt ?R ?X x" and "is_maximal_in_mset_wrt ?R ?X y"
    using is_maximal_in_mset_wrt_iff[OF trans asym] by simp_all

  thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
    transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
    (∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x))"
    using ‹x ≠ y› trans asym
    by (metis Uniq_D)

  have "is_strictly_minimal_in_mset_wrt ?R ?X x" and "is_strictly_minimal_in_mset_wrt ?R ?X y"
    using ‹x ≠ y› is_strictly_minimal_in_mset_wrt_iff[OF trans asym] by simp_all

  thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
    transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
    (∃⇩≤⇩1x. is_strictly_minimal_in_mset_wrt R X x))"
    using ‹x ≠ y› trans asym
    by (metis Uniq_D)

  have "is_strictly_maximal_in_mset_wrt ?R ?X x" and "is_strictly_maximal_in_mset_wrt ?R ?X y"
    using ‹x ≠ y› is_strictly_maximal_in_mset_wrt_iff[OF trans asym] by simp_all

  thus "¬ (∀(R :: 'a ⇒ 'a ⇒ bool) (X :: 'a multiset).
    transp_on (set_mset X) R ⟶ asymp_on (set_mset X) R ⟶
    (∃⇩≤⇩1x. is_strictly_maximal_in_mset_wrt R X x))"
    using ‹x ≠ y› trans asym
    by (metis Uniq_D)
qed


section ‹Least and greatest elements›

definition is_least_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹ totalp_on (set_mset X) R ⟹
    is_least_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"

definition is_greatest_in_mset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a ⇒ bool" where
  "transp_on (set_mset X) R ⟹ asymp_on (set_mset X) R ⟹ totalp_on (set_mset X) R ⟹
    is_greatest_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R y x)"

context
  fixes X R
  assumes
    trans: "transp_on (set_mset X) R" and
    asym: "asymp_on (set_mset X) R" and
    tot: "totalp_on (set_mset X) R"
begin

subsection ‹Conversions›

lemma is_least_in_mset_wrt_iff:
  "is_least_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"
  using is_least_in_mset_wrt_def[OF trans asym tot] .

lemma is_greatest_in_mset_wrt_iff:
  "is_greatest_in_mset_wrt R X x ⟷ x ∈# X ∧ (∀y ∈# X - {#x#}. R y x)"
  using is_greatest_in_mset_wrt_def[OF trans asym tot] .

lemma is_minimal_in_mset_wrt_if_is_least_in_mset_wrt[intro]:
  "is_least_in_mset_wrt R X x ⟹ is_minimal_in_mset_wrt R X x"
  unfolding is_minimal_in_mset_wrt_iff[OF trans asym]
  unfolding is_least_in_mset_wrt_def[OF trans asym tot]
  by (metis add_mset_remove_trivial_eq asym asymp_onD insert_noteq_member)

lemma is_maximal_in_mset_wrt_if_is_greatest_in_mset_wrt[intro]:
  "is_greatest_in_mset_wrt R X x ⟹ is_maximal_in_mset_wrt R X x"
  unfolding is_maximal_in_mset_wrt_iff[OF trans asym]
  unfolding is_greatest_in_mset_wrt_def[OF trans asym tot]
  by (metis add_mset_remove_trivial_eq asym asymp_onD insert_noteq_member)

lemma is_strictly_minimal_in_mset_wrt_iff_is_least_in_mset_wrt: 
  "is_strictly_minimal_in_mset_wrt R X = is_least_in_mset_wrt R X"
  unfolding is_strictly_minimal_in_mset_wrt_iff[OF trans asym] is_least_in_mset_wrt_iff 
proof(intro ext iffI)
  fix x
  show "x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= y x) ⟹ x ∈# X ∧ (∀y ∈# X - {#x#}. R x y)"
    by (metis (mono_tags, lifting) in_diffD sup2CI tot totalp_onD)
next 
  fix x
  show "x ∈# X ∧ (∀y ∈# X - {#x#}. R x y) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= y x)"
    by (metis (full_types) asym asymp_onD in_diffD sup2E)
qed

lemma is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt: 
  "is_strictly_maximal_in_mset_wrt R X = is_greatest_in_mset_wrt R X"
  unfolding is_strictly_maximal_in_mset_wrt_iff[OF trans asym] is_greatest_in_mset_wrt_iff 
proof(intro ext iffI)
  fix x
  show "x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= x y) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. R y x)"
    by (metis (mono_tags, lifting) in_diffD sup2CI tot totalp_onD)
next 
  fix x
  show "x ∈# X ∧ (∀y∈#X - {#x#}. R y x) ⟹ x ∈# X ∧ (∀y∈#X - {#x#}. ¬ R⇧=⇧= x y)"
    by (metis (full_types) asym asymp_onD in_diffD sup2E)
qed

subsection ‹Uniqueness›

lemma Uniq_is_minimal_in_mset_wrt[intro]:
  "∃⇩≤⇩1x. is_minimal_in_mset_wrt R X x"
  unfolding is_minimal_in_mset_wrt_iff[OF trans asym]
  by (smt (verit, best) Uniq_I tot totalp_onD)

lemma Uniq_is_maximal_in_mset_wrt[intro]:
  "∃⇩≤⇩1x. is_maximal_in_mset_wrt R X x"
  unfolding is_maximal_in_mset_wrt_iff[OF trans asym]
  by (smt (verit, best) Uniq_I tot totalp_onD)

lemma Uniq_is_least_in_mset_wrt[intro]:
  "∃⇩≤⇩1x. is_least_in_mset_wrt R X x"
  using is_least_in_mset_wrt_iff
  by (smt (verit, best) Uniq_I asym asymp_onD insert_DiffM insert_noteq_member)

lemma Uniq_is_greatest_in_mset_wrt[intro]:
  "∃⇩≤⇩1x. is_greatest_in_mset_wrt R X x"
  unfolding is_greatest_in_mset_wrt_iff
  by (smt (verit, best) Uniq_I asym asymp_onD insert_DiffM insert_noteq_member)


subsection ‹Miscellaneous›

lemma is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one:
  "is_least_in_mset_wrt R X x ⟷ is_minimal_in_mset_wrt R X x ∧ count X x = 1"
proof (rule iffI)
  assume "is_least_in_mset_wrt R X x"
  thus "is_minimal_in_mset_wrt R X x ∧ count X x = 1"
    unfolding is_least_in_mset_wrt_iff is_minimal_in_mset_wrt_iff[OF trans asym]
    by (metis One_nat_def add_mset_remove_trivial_eq asym asymp_onD count_add_mset not_in_iff)
next
  assume "is_minimal_in_mset_wrt R X x ∧ count X x = 1"
  then show "is_least_in_mset_wrt R X x"
    unfolding is_least_in_mset_wrt_iff is_minimal_in_mset_wrt_iff[OF trans asym]
    by (metis count_single in_diffD in_diff_count nat_less_le tot totalp_onD)
qed

lemma is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one:
  "is_greatest_in_mset_wrt R X x ⟷ is_maximal_in_mset_wrt R X x ∧ count X x = 1"
proof (rule iffI)
  assume "is_greatest_in_mset_wrt R X x"
  thus "is_maximal_in_mset_wrt R X x ∧ count X x = 1"
    unfolding is_greatest_in_mset_wrt_iff is_maximal_in_mset_wrt_iff[OF trans asym]
    by (metis One_nat_def add_mset_remove_trivial_eq asym asymp_onD count_add_mset not_in_iff)
next
  assume "is_maximal_in_mset_wrt R X x ∧ count X x = 1"
  then show "is_greatest_in_mset_wrt R X x"
    unfolding is_greatest_in_mset_wrt_iff is_maximal_in_mset_wrt_iff[OF trans asym]
    by (metis count_single in_diffD in_diff_count nat_less_le tot totalp_onD)
qed

lemma count_ge_2_if_minimal_in_mset_wrt_and_not_least_in_mset_wrt:
  assumes "is_minimal_in_mset_wrt R X x" and "¬ is_least_in_mset_wrt R X x"
  shows "count X x ≥ 2"
  using assms
  unfolding is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one
  by (metis Suc_1 Suc_le_eq antisym_conv1 asym count_greater_eq_one_iff is_minimal_in_mset_wrt_iff
      trans)

lemma count_ge_2_if_maximal_in_mset_wrt_and_not_greatest_in_mset_wrt:
  assumes "is_maximal_in_mset_wrt R X x" and "¬ is_greatest_in_mset_wrt R X x"
  shows "count X x ≥ 2"
  using assms
  unfolding is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one
  by (metis Suc_1 Suc_le_eq antisym_conv1 asym count_greater_eq_one_iff is_maximal_in_mset_wrt_iff
      trans)

lemma explode_greatest_in_mset_wrt:
  assumes max: "is_greatest_in_mset_wrt R X x"
  shows "add_mset x {#y ∈# X. y ≠ x#} = X"
  using max[folded is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt]
  using explode_strictly_maximal_in_mset_wrt[OF trans asym]
  by metis

end


lemma multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
    "R x1 x2"
  shows "multp⇩H⇩O R M1 M2"
proof -
  have
    trans1: "transp_on (set_mset M1) R" and trans2: "transp_on (set_mset M2) R" and
    asym1: "asymp_on (set_mset M1) R" and asym2: "asymp_on (set_mset M2) R" and
    tot1: "totalp_on (set_mset M1) R" and tot2: "totalp_on (set_mset M2) R"
    using trans[THEN transp_on_subset] asym[THEN asymp_on_subset] tot[THEN totalp_on_subset]
    by simp_all

  have x1_in: "x1 ∈# M1" and x1_gr: "∀y∈#M1. y ≠ x1 ⟶ ¬ R x1 y"
    using x1_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans1 asym1]] by argo+

  have x2_in: "x2 ∈# M2" and x2_gr: "∀y∈#M2. y ≠ x2 ⟶ ¬ R x2 y"
    using x2_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans2 asym2]] by argo+

  show "multp⇩H⇩O R M1 M2"
    unfolding multp⇩H⇩O_def
  proof (intro conjI)
    show "M1 ≠ M2"
      using x1_in x2_in x1_gr
      by (metis ‹R x1 x2› asym2 asymp_onD)
  next
    show "∀y. count M2 y < count M1 y ⟶ (∃x. R y x ∧ count M1 x < count M2 x)"
      using x1_in x2_in x1_gr x2_gr
      by (smt (verit, best) assms(6) asym1 asymp_onD count_greater_zero_iff count_inI
          dual_order.strict_trans local.trans subsetD sup_ge1 sup_ge2 tot1 totalp_onD transp_onD)
  qed
qed

lemma multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
    "R x1 x2"
  shows "multp⇩D⇩M R M1 M2"
  using multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt[OF assms, THEN multp⇩H⇩O_imp_multp⇩D⇩M] .

lemma multp_if_maximal_wrt_less_that_maximal_wrt:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    x1_maximal: "is_maximal_in_mset_wrt R M1 x1" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
    "R x1 x2"
  shows "multp R M1 M2"
  using multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt[OF assms, THEN multp⇩D⇩M_imp_multp] .


lemma multp⇩H⇩O_if_same_maximal_wrt_and_count_lt:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    x1_maximal: "is_maximal_in_mset_wrt R M1 x" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x" and
    "count M1 x < count M2 x"
  shows "multp⇩H⇩O R M1 M2"
  by (metis assms(6) asym asymp_on_subset count_inI is_greatest_in_set_wrt_iff
      is_maximal_in_mset_wrt_def is_maximal_in_set_wrt_eq_is_greatest_in_set_wrt less_zeroE
      local.trans multp⇩H⇩O_def order_less_imp_not_less sup_ge1 tot totalp_on_subset transp_on_subset
      x1_maximal)

lemma multp_if_same_maximal_wrt_and_count_lt:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M1 ∪ set_mset M2) R" and
    tot: "totalp_on (set_mset M1 ∪ set_mset M2) R" and
    x1_maximal: "is_maximal_in_mset_wrt R M1 x" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x" and
    "count M1 x < count M2 x"
  shows "multp R M1 M2"
  using multp⇩H⇩O_if_same_maximal_wrt_and_count_lt[
      OF assms, THEN multp⇩H⇩O_imp_multp⇩D⇩M, THEN multp⇩D⇩M_imp_multp] .

lemma less_than_maximal_wrt_if_multp⇩H⇩O:
  assumes
    trans: "transp_on (set_mset M1 ∪ set_mset M2) R" and
    asym: "asymp_on (set_mset M2) R" and
    tot: "totalp_on (set_mset M2) R" and
    x2_maximal: "is_maximal_in_mset_wrt R M2 x2" and
    "multp⇩H⇩O R M1 M2" and
    "x1 ∈# M1"
  shows "R⇧=⇧= x1 x2"
proof -
  have
    trans2: "transp_on (set_mset M2) R" and
    asym2: "asymp_on (set_mset M2) R" and
    tot2: "totalp_on (set_mset M2) R"
    using trans[THEN transp_on_subset] asym[THEN asymp_on_subset] tot[THEN totalp_on_subset]
    by simp_all

  have x2_in: "x2 ∈# M2" and x2_gr: "∀y∈#M2. y ≠ x2 ⟶ ¬ R x2 y"
    using x2_maximal[unfolded is_maximal_in_mset_wrt_iff[OF trans2 asym2]] by argo+

  show ?thesis
  proof (cases "x1 ∈# M2")
    case True
    thus ?thesis
      using x2_gr by (metis (mono_tags) sup2CI tot2 totalp_onD x2_in)
  next
    case False

    hence "x1 ∈# M1 - M2"
      using ‹x1 ∈# M1› by (simp add: in_diff_count not_in_iff)

    moreover have "∀k∈#M1 - M2. ∃x∈#M2 - M1. R k x"
      using multp⇩H⇩O_implies_one_step_strong(2)[OF ‹multp⇩H⇩O R M1 M2›] .

    ultimately obtain x where "x ∈# M2 - M1" and "R x1 x"
      by metis

    hence "x ≠ x2 ⟶ ¬ R x2 x"
      using x2_gr by (metis in_diffD)

    hence "x ≠ x2 ⟶ R x x2"
      by (metis ‹x ∈# M2 - M1› in_diffD tot2 totalp_onD x2_in)

    thus ?thesis
      using ‹R x1 x›
      by (meson Un_iff ‹x ∈# M2 - M1› assms(6) in_diffD local.trans sup2I1 transp_onD x2_in)
  qed
qed


section ‹Examples of duplicate handling in set and multiset definitions›

lemma
  fixes M :: "nat multiset"
  defines "M ≡ {#0, 0, 1, 1, 2, 2#}"
  shows
    "is_minimal_in_set_wrt (<) (set_mset M) 0"
    "is_minimal_in_mset_wrt (<) M 0"
    "is_least_in_set_wrt (<) (set_mset M) 0"
    "∄y. is_least_in_mset_wrt (<) M y"
  by (auto simp: M_def is_minimal_in_set_wrt_iff is_minimal_in_mset_wrt_def
      is_least_in_set_wrt_iff is_least_in_mset_wrt_def)

lemma
  fixes x y :: 'a and M :: "'a multiset"
  defines "M ≡ {#x, y, y#}"
  defines "R ≡ λ_ _. False"
  assumes "x ≠ y"
  shows
    "is_maximal_in_mset_wrt R M x"
    "is_maximal_in_mset_wrt R M y"
    "is_strictly_maximal_in_mset_wrt R M x"
    "¬ is_strictly_maximal_in_mset_wrt R M y"
proof -
  have transp_on_False[simp]: "⋀A. transp_on A (λ_ _. False)"
    by (simp add: transp_onI)

  have asymp_on_False[simp]: "⋀A. asymp_on A (λ_ _. False)"
    by (simp add: asymp_onI)

  show
    "is_maximal_in_mset_wrt R M x"
    "is_maximal_in_mset_wrt R M y"
    "is_strictly_maximal_in_mset_wrt R M x"
    "¬ is_strictly_maximal_in_mset_wrt R M y"
    unfolding is_maximal_in_mset_wrt_iff[of M R, unfolded R_def, simplified, folded R_def]
    unfolding is_strictly_maximal_in_mset_wrt_iff[of M R, unfolded R_def, simplified, folded R_def]
    unfolding atomize_conj
    using ‹x ≠ y›
    by (simp add: M_def)
qed


section ‹Hide stuff›

text ‹We restrict the public interface to ease future internal changes.›

hide_fact is_minimal_in_mset_wrt_def is_maximal_in_mset_wrt_def
hide_fact is_strictly_minimal_in_mset_wrt_def is_strictly_maximal_in_mset_wrt_def
hide_fact is_least_in_mset_wrt_def is_greatest_in_mset_wrt_def


section ‹Integration in type classes›

abbreviation (in order) is_minimal_in_mset where
  "is_minimal_in_mset ≡ is_minimal_in_mset_wrt (<)"

abbreviation (in order) is_maximal_in_mset where
  "is_maximal_in_mset ≡ is_maximal_in_mset_wrt (<)"

lemmas (in order) is_minimal_in_mset_iff =
  is_minimal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]

lemmas (in order) is_maximal_in_mset_iff =
  is_maximal_in_mset_wrt_iff[OF transp_on_less asymp_on_less]

lemmas (in order) ex_minimal_in_mset =
  ex_minimal_in_mset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) ex_maximal_in_mset =
  ex_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) explode_maximal_in_mset =
  explode_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) explode_strictly_maximal_in_mset =
  explode_strictly_maximal_in_mset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) is_minimal_in_filter_mset_iff =
  is_minimal_in_filter_mset_wrt_iff[OF transp_on_less asymp_on_less]


abbreviation (in linorder) is_least_in_mset where
  "is_least_in_mset ≡ is_least_in_mset_wrt (<)"

abbreviation (in linorder) is_greatest_in_mset where
  "is_greatest_in_mset ≡ is_greatest_in_mset_wrt (<)"

lemmas (in linorder) is_least_in_mset_iff =
  is_least_in_mset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_greatest_in_mset_iff =
  is_greatest_in_mset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_minimal_in_mset_if_is_least_in_mset[intro] =
  is_minimal_in_mset_wrt_if_is_least_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_maximal_in_mset_if_is_greatest_in_mset[intro] =
  is_maximal_in_mset_wrt_if_is_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_minimal_in_mset[intro] =
  Uniq_is_minimal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_maximal_in_mset[intro] =
  Uniq_is_maximal_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_least_in_mset[intro] =
  Uniq_is_least_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_greatest_in_mset[intro] =
  Uniq_is_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_least_in_mset_iff_is_minimal_and_count_eq_one =
  is_least_in_mset_wrt_iff_is_minimal_and_count_eq_one[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) is_greatest_in_mset_iff_is_maximal_and_count_eq_one =
  is_greatest_in_mset_wrt_iff_is_maximal_and_count_eq_one[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) count_ge_2_if_minimal_in_mset_and_not_least_in_mset =
  count_ge_2_if_minimal_in_mset_wrt_and_not_least_in_mset_wrt[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) count_ge_2_if_maximal_in_mset_and_not_greatest_in_mset =
  count_ge_2_if_maximal_in_mset_wrt_and_not_greatest_in_mset_wrt[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) explode_greatest_in_mset =
  explode_greatest_in_mset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) multp⇩H⇩O_if_maximal_less_that_maximal =
  multp⇩H⇩O_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) multp⇩D⇩M_if_maximal_less_that_maximal =
  multp⇩D⇩M_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) multp_if_maximal_less_that_maximal =
  multp_if_maximal_wrt_less_that_maximal_wrt[OF transp_on_less asymp_on_less
    totalp_on_less]

lemmas (in linorder) multp⇩H⇩O_if_same_maximal_and_count_lt =
  multp⇩H⇩O_if_same_maximal_wrt_and_count_lt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) multp_if_same_maximal_and_count_lt =
  multp_if_same_maximal_wrt_and_count_lt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) less_than_maximal_if_multp⇩H⇩O =
  less_than_maximal_wrt_if_multp⇩H⇩O[OF transp_on_less asymp_on_less totalp_on_less]

lemma (in linorder)
  assumes"is_greatest_in_mset C L"
  shows "C - {#L#} = {#K ∈# C. K ≠ L#}"
  using assms
  by (smt (verit, del_insts) add_diff_cancel_left' diff_subset_eq_self diff_zero filter_empty_mset
      filter_mset_add_mset filter_mset_eq_conv insert_DiffM2 local.is_greatest_in_mset_iff
      local.not_less_iff_gr_or_eq)

end