section ‹More Theorems about the Multiset Order›
theory Multiset_Order
imports Multiset
begin
subsubsection ‹Alternative characterizations›
context order
begin
lemma reflp_le: "reflp (op ≤)"
unfolding reflp_def by simp
lemma antisymP_le: "antisymP (op ≤)"
unfolding antisym_def by auto
lemma transp_le: "transp (op ≤)"
unfolding transp_def by auto
lemma irreflp_less: "irreflp (op <)"
unfolding irreflp_def by simp
lemma antisymP_less: "antisymP (op <)"
unfolding antisym_def by auto
lemma transp_less: "transp (op <)"
unfolding transp_def by auto
lemmas le_trans = transp_le[unfolded transp_def, rule_format]
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) simp
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: le_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"
proof (unfold mult_def, induct rule: trancl_induct)
case (base P)
then show ?case
by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset⇩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>y. count M x < count N x)"
by (simp_all add: less_multiset⇩H⇩O_def)
from step(2) obtain M0 a K where
*: "P = M0 + {#a#}" "N = M0 + K" "a ∉# K" "⋀b. b ∈# K ⟹ b < a"
by (blast elim: mult1_lessE)
from ‹M ≠ N› ** *(1,2,3) have "M ≠ P" by (force dest: *(4) split: if_splits)
moreover
{ assume "count P a ≤ count M a"
with ‹a ∉# K› have "count N a < count M a" unfolding *(1,2)
by (auto simp add: not_in_iff)
with ** obtain z where z: "z > a" "count M z < count N z"
by blast
with * have "count N z ≤ count P z"
by (force simp add: not_in_iff)
with z have "∃z > a. 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>y. 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 "y < a" by simp
then show ?thesis by (cases "count P a ≤ count M a") (auto dest: count_a intro: less_trans)
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: "z > y" "count M z < count N z" by auto
show ?thesis
proof (cases "z ∈# K")
case True
with *(4) have "z < a" by simp
with z(1) show ?thesis
by (cases "count P a ≤ count M a") (auto dest!: count_a intro: less_trans)
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 less_multiset⇩H⇩O_def by blast
qed
lemma less_multiset⇩D⇩M_imp_mult:
"less_multiset⇩D⇩M M N ⟹ (M, N) ∈ mult {(x, y). x < y}"
proof -
assume "less_multiset⇩D⇩M M N"
then obtain X Y where
"X ≠ {#}" and "X ≤# N" and "M = N - X + Y" and "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)"
unfolding less_multiset⇩D⇩M_def by blast
then have "(N - X + Y, N - X + X) ∈ mult {(x, y). x < y}"
by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
with ‹M = N - X + Y› ‹X ≤# N› show "(M, N) ∈ mult {(x, y). x < y}"
by (metis subset_mset.diff_add)
qed
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
proof (intro iffI exI conjI)
assume "less_multiset⇩H⇩O M N"
then obtain z where z: "count M z < count N z"
unfolding less_multiset⇩H⇩O_def by (auto simp: multiset_eq_iff nat_neq_iff)
def X ≡ "N - M"
def 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 ∧ 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 ‹less_multiset⇩H⇩O M N› obtain a where "k < a" and "count M a < count N a"
unfolding less_multiset⇩H⇩O_def by blast
then show "∃a. a ∈# X ∧ k < a" unfolding X_def
by (auto simp add: in_diff_count)
qed
qed
lemma mult_less_multiset⇩D⇩M: "(M, N) ∈ mult {(x, y). x < y} ⟷ less_multiset⇩D⇩M M N"
by (metis less_multiset⇩D⇩M_imp_mult less_multiset⇩H⇩O_imp_less_multiset⇩D⇩M mult_imp_less_multiset⇩H⇩O)
lemma mult_less_multiset⇩H⇩O: "(M, N) ∈ mult {(x, y). x < y} ⟷ less_multiset⇩H⇩O M N"
by (metis less_multiset⇩D⇩M_imp_mult less_multiset⇩H⇩O_imp_less_multiset⇩D⇩M mult_imp_less_multiset⇩H⇩O)
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
context linorder
begin
lemma total_le: "total {(a :: 'a, b). a ≤ b}"
unfolding total_on_def by auto
lemma total_less: "total {(a :: 'a, b). a < b}"
unfolding total_on_def by auto
lemma linorder_mult: "class.linorder
(λM N. (M, N) ∈ mult {(x, y). x < y} ∨ M = N)
(λM N. (M, N) ∈ mult {(x, y). x < y})"
proof -
interpret o: order
"(λM N. (M, N) ∈ mult {(x, y). x < y} ∨ M = N)"
"(λM N. (M, N) ∈ mult {(x, y). x < y})"
by (rule order_mult)
show ?thesis by unfold_locales (auto 0 3 simp: mult⇩H⇩O not_less_iff_gr_or_eq)
qed
end
lemma less_multiset_less_multiset⇩H⇩O:
"M #⊂# N ⟷ less_multiset⇩H⇩O M N"
unfolding less_multiset_def mult⇩H⇩O less_multiset⇩H⇩O_def ..
lemmas less_multiset⇩D⇩M = mult⇩D⇩M[folded less_multiset_def]
lemmas less_multiset⇩H⇩O = mult⇩H⇩O[folded less_multiset_def]
lemma le_multiset⇩H⇩O:
fixes M N :: "('a :: linorder) multiset"
shows "M #⊆# N ⟷ (∀y. count N y < count M y ⟶ (∃x. y < x ∧ count M x < count N x))"
by (auto simp: le_multiset_def less_multiset⇩H⇩O)
lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M #⊂# N}"
unfolding less_multiset_def by (auto intro: wf_mult wf)
lemma order_multiset: "class.order
(le_multiset :: ('a :: order) multiset ⇒ ('a :: order) multiset ⇒ bool)
(less_multiset :: ('a :: order) multiset ⇒ ('a :: order) multiset ⇒ bool)"
by unfold_locales
lemma linorder_multiset: "class.linorder
(le_multiset :: ('a :: linorder) multiset ⇒ ('a :: linorder) multiset ⇒ bool)
(less_multiset :: ('a :: linorder) multiset ⇒ ('a :: linorder) multiset ⇒ bool)"
by unfold_locales (fastforce simp add: less_multiset⇩H⇩O le_multiset_def not_less_iff_gr_or_eq)
interpretation multiset_linorder: linorder
"le_multiset :: ('a :: linorder) multiset ⇒ ('a :: linorder) multiset ⇒ bool"
"less_multiset :: ('a :: linorder) multiset ⇒ ('a :: linorder) multiset ⇒ bool"
by (rule linorder_multiset)
interpretation multiset_wellorder: wellorder
"le_multiset :: ('a :: wellorder) multiset ⇒ ('a :: wellorder) multiset ⇒ bool"
"less_multiset :: ('a :: wellorder) multiset ⇒ ('a :: wellorder) multiset ⇒ bool"
by unfold_locales (blast intro: wf_less_multiset [unfolded wf_def, simplified, rule_format])
lemma le_multiset_total:
fixes M N :: "('a :: linorder) multiset"
shows "¬ M #⊆# N ⟹ N #⊆# M"
by (metis multiset_linorder.le_cases)
lemma less_eq_imp_le_multiset:
fixes M N :: "('a :: linorder) multiset"
shows "M ≤# N ⟹ M #⊆# N"
unfolding le_multiset_def less_multiset⇩H⇩O
by (simp add: less_le_not_le subseteq_mset_def)
lemma less_multiset_right_total:
fixes M :: "('a :: linorder) multiset"
shows "M #⊂# M + {#undefined#}"
unfolding le_multiset_def less_multiset⇩H⇩O by simp
lemma le_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
shows "{#} #⊆# M"
by (simp add: less_eq_imp_le_multiset)
lemma le_multiset_empty_right[simp]:
fixes M :: "('a :: linorder) multiset"
shows "M ≠ {#} ⟹ ¬ M #⊆# {#}"
by (metis le_multiset_empty_left multiset_order.antisym)
lemma less_multiset_empty_left[simp]:
fixes M :: "('a :: linorder) multiset"
shows "M ≠ {#} ⟹ {#} #⊂# M"
by (simp add: less_multiset⇩H⇩O)
lemma less_multiset_empty_right[simp]:
fixes M :: "('a :: linorder) multiset"
shows "¬ M #⊂# {#}"
using le_empty less_multiset⇩D⇩M by blast
lemma
fixes M N :: "('a :: linorder) multiset"
shows
le_multiset_plus_left[simp]: "N #⊆# (M + N)" and
le_multiset_plus_right[simp]: "M #⊆# (M + N)"
using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
lemma
fixes M N :: "('a :: linorder) multiset"
shows
less_multiset_plus_plus_left_iff[simp]: "M + N #⊂# M' + N ⟷ M #⊂# M'" and
less_multiset_plus_plus_right_iff[simp]: "M + N #⊂# M + N' ⟷ N #⊂# N'"
unfolding less_multiset⇩H⇩O by auto
lemma add_eq_self_empty_iff: "M + N = M ⟷ N = {#}"
by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
lemma
fixes M N :: "('a :: linorder) multiset"
shows
less_multiset_plus_left_nonempty[simp]: "M ≠ {#} ⟹ N #⊂# M + N" and
less_multiset_plus_right_nonempty[simp]: "N ≠ {#} ⟹ M #⊂# M + N"
using [[metis_verbose = false]]
by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
add.commute)+
lemma ex_gt_imp_less_multiset: "(∃y :: 'a :: linorder. 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 ex_gt_count_imp_less_multiset:
"(∀y :: 'a :: linorder. y ∈# M + N ⟶ y ≤ x) ⟹ count M x < count N x ⟹ M #⊂# N"
unfolding less_multiset⇩H⇩O
by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
lemma union_less_diff_plus: "P ≤# M ⟹ N #⊂# P ⟹ M - P + N #⊂# M"
by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
end