# Theory Multiset_Order

```(*  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⇩D⇩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⇩D⇩M r M N ⟹ multp r M N"
proof -
assume "multp⇩D⇩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"
qed

subsubsection ‹The Huet--Oppen Ordering›

definition multp⇩H⇩O where
"multp⇩H⇩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⇩H⇩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)"
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›
moreover
{ assume "count P a ≤ count M a"
with ‹a ∉# K› have "count N a < count M a" unfolding *(1,2)
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›
diff_single_trivial in_diff_count not_le_imp_less)
with z have "∃z. r a z ∧ count M z < count P z" by auto
} note count_a = this
{ fix y
assume count_y: "count P y < count M y"
have "∃x. r y x ∧ count M x < count P x"
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)
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 *
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⇩H⇩O r M N ⟹ multp⇩D⇩M r M N"
unfolding multp⇩D⇩M_def
proof (intro iffI exI conjI)
assume "multp⇩H⇩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
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
qed
qed

lemma multp_eq_multp⇩D⇩M: "asymp r ⟹ transp r ⟹ multp r = multp⇩D⇩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⇩H⇩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⇩D⇩M R M1 M2"
shows "multp⇩D⇩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⇩D⇩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›
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⇩H⇩O R (M + M1) (M + M2) ⟷ multp⇩H⇩O R M1 M2"
unfolding multp⇩H⇩O_def by simp

lemma strict_subset_implies_multp⇩D⇩M: "A ⊂# B ⟹ multp⇩D⇩M r A B"
unfolding multp⇩D⇩M_def
set_mset_empty subset_mset.lessE)

lemma strict_subset_implies_multp⇩H⇩O: "A ⊂# B ⟹ multp⇩H⇩O r A B"
unfolding multp⇩H⇩O_def

lemma multp⇩H⇩O_implies_one_step_strong:
assumes "multp⇩H⇩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

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⇩H⇩O R (M1 - M2) (M2 - M1) ⟷ multp⇩H⇩O R M1 M2"
by (metis diff_intersect_left_idem multiset_inter_commute multp⇩H⇩O_plus_plus

lemma multp⇩H⇩O_iff_set_mset_less⇩H⇩O_set_mset:
"multp⇩H⇩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⇩D⇩M R M1 M2 ⟹ (⋀x y. x ∈# M1 ⟹ y ∈# M2 ⟹ R x y ⟹ S x y) ⟹ multp⇩D⇩M S M1 M2"
unfolding multp⇩D⇩M_def

lemma multp⇩H⇩O_mono_strong:
"multp⇩H⇩O R M1 M2 ⟹ (⋀x y. x ∈# M1 ⟹ y ∈# M2 ⟹ R x y ⟹ S x y) ⟹ multp⇩H⇩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⇩H⇩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#}"

from assms(1) have "asymp R"
by (auto simp: R_def intro: asymp_onI)
moreover have "¬ asymp (multp⇩H⇩O R)"
unfolding asymp_on_def Set.ball_simps not_all not_imp not_not
proof (intro exI conjI)
show "multp⇩H⇩O R {#a, b#} {#c, d#}"
unfolding multp⇩H⇩O_def
using ‹{#a, b#} ≠ {#c, d#}› R_def assms by auto
next
show "multp⇩H⇩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⇩H⇩O R)"
proof (rule asymp_onI)
fix M1 M2 :: "'a multiset"
assume "M1 ∈ B" "M2 ∈ B" "multp⇩H⇩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⇩H⇩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⇩H⇩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⇩H⇩O R)"

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⇩H⇩O R)"
proof (rule transp_onI)
from assms have "asymp_on B (multp⇩H⇩O R)"
using asymp_on_multp⇩H⇩O by metis

fix M1 M2 M3
assume hyps: "M1 ∈ B" "M2 ∈ B" "M3 ∈ B" "multp⇩H⇩O R M1 M2" "multp⇩H⇩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›

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⇩H⇩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⇩H⇩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⇧=⇧= 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⇧=⇧= 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⇧=⇧= 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⇧=⇧= 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⇩H⇩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⇩D⇩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⇩D⇩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⇩H⇩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⇩H⇩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⇩D⇩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⇩H⇩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⇩H⇩O M N"
unfolding multp_def[of "(<)", symmetric]
using multp_imp_multp⇩H⇩O[of "(<)"]

lemma less_multiset⇩D⇩M_imp_mult:
"less_multiset⇩D⇩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⇩H⇩O M N ⟹ less_multiset⇩D⇩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⇩D⇩M M N"
unfolding multp_def[of "(<)", symmetric]
using multp_eq_multp⇩D⇩M[of "(<)", simplified]

lemma mult_less_multiset⇩H⇩O: "(M, N) ∈ mult {(x, y). x < y} ⟷ less_multiset⇩H⇩O M N"
unfolding multp_def[of "(<)", symmetric]
using multp_eq_multp⇩H⇩O[of "(<)", simplified]

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⇩H⇩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

(* 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]:
shows "{#} ≤ M"

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"

(* 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"

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"

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
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⇩H⇩O R (repeat_mset n A) (repeat_mset n B) ⟷ multp⇩H⇩O R A B"
proof (rule iffI)
assume hyp: "multp⇩H⇩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)"

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⇩H⇩O R A B"
next
assume "multp⇩H⇩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)"

from 1 have "repeat_mset n A ≠ repeat_mset n B"

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⇩H⇩O R (repeat_mset n A) (repeat_mset n B)"
qed

lemma multp⇩H⇩O_double_double[simp]: "multp⇩H⇩O R (A + A) (B + B) ⟷ multp⇩H⇩O R A B"
using multp⇩H⇩O_repeat_mset_repeat_mset[of 2]

subsection ‹Simprocs›

"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"
then show ?thesis
qed

"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"
then show ?thesis
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›

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

by standard (metis less_eq_multiset⇩H⇩O not_less_iff_gr_or_eq)

lemma less_eq_multiset_total:
fixes M N :: "'a :: linorder multiset"
shows "¬ M ≤ N ⟹ N ≤ M"
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

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

by fastforce

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

by fastforce

by fastforce

assumes a_lt_b: "a < b" and A_le_B: "A < B"

lemma add_mset_lt_lt_le: "a < b ⟹ A ≤ B ⟹ add_mset a A < add_mset b B"

lemma add_mset_lt_le_lt: "a ≤ b ⟹ A < B ⟹ add_mset a A < add_mset b B" for a :: "'a :: linorder"

fixes a :: "'a :: linorder"
assumes a_le_b: "a ≤ b" and A_le_B: "A ≤ 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
{
fix y
assume "count N y < count M y"
hence "y ∈# M"