# Theory Multiset_More

(*  Title:       More about Multisets
Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2015
Author:      Jasmin Blanchette <blanchette at in.tum.de>, 2014, 2015
Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
Author:      Dmitriy Traytel <traytel at in.tum.de>, 2014
Maintainer:  Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>
*)

theory Multiset_More
imports
"HOL-Library.Multiset_Order"
"HOL-Library.Sublist"
begin

text ‹
Isabelle's theory of finite multisets is not as developed as other areas, such as lists and sets.
The present theory introduces some missing concepts and lemmas. Some of it is expected to move to
Isabelle's library.
›

subsection ‹Basic Setup›

declare
diff_single_trivial [simp]
in_image_mset [iff]
image_mset.compositionality [simp]

(*To have the same rules as the set counter-part*)
mset_subset_eqD[dest, intro?] (*@{thm subsetD}*)

Multiset.in_multiset_in_set[simp]

sum_mset_sum_list[simp]

subsection ‹Lemmas about Intersection, Union and Pointwise Inclusion›

by (auto simp add: subseteq_mset_def le_SucI)

lemma subset_add_mset_notin_subset_mset: ‹A ⊆# add_mset b B ⟹ b ∉# A ⟹ A ⊆# B›

lemma subset_msetE: "⟦A ⊂# B; ⟦A ⊆# B; ¬ B ⊆# A⟧ ⟹ R⟧ ⟹ R"

lemma Diff_triv_mset: "M ∩# N = {#} ⟹ M - N = M"
by (metis diff_intersect_left_idem diff_zero)

lemma diff_intersect_sym_diff: "(A - B) ∩# (B - A) = {#}"
by (rule multiset_eqI) simp

declare subset_msetE [elim!]

lemma subseq_mset_subseteq_mset: "subseq xs ys ⟹ mset xs ⊆# mset ys"
proof (induct xs arbitrary: ys)
case (Cons x xs)
note Outer_Cons = this
then show ?case
proof (induct ys)
case (Cons y ys)
have "subseq xs ys"
by (metis Cons.prems(2) subseq_Cons' subseq_Cons2_iff)
then show ?case
using Cons by (metis mset.simps(2) mset_subset_eq_add_mset_cancel subseq_Cons2_iff
qed simp
qed simp

lemma finite_mset_set_inter:
‹finite A ⟹ finite B ⟹ mset_set (A ∩ B) = mset_set A ∩# mset_set B›
apply (induction A rule: finite_induct)
subgoal by auto
subgoal for a A
by (cases ‹a ∈ B›; cases ‹a ∈# mset_set B›)
(use multi_member_split[of a ‹mset_set B›] in
‹auto simp: mset_set.insert_remove›)
done

subsection ‹Lemmas about Filter and Image›

lemma count_image_mset_ge_count: "count (image_mset f A) (f b) ≥ count A b"
by (induction A) auto

lemma count_image_mset_inj:
assumes ‹inj f›
shows ‹count (image_mset f M) (f x) = count M x›
by (induct M) (use assms in ‹auto simp: inj_on_def›)

lemma count_image_mset_le_count_inj_on:
"inj_on f (set_mset M) ⟹ count (image_mset f M) y ≤ count M (inv_into (set_mset M) f y)"
proof (induct M)
note ih = this(1) and inj_xM = this(2)

have inj_M: "inj_on f (set_mset M)"
using inj_xM by simp

show ?case
proof (cases "x ∈# M")
case x_in_M: True
show ?thesis
proof (cases "y = f x")
case y_eq_fx: True
show ?thesis
using x_in_M ih[OF inj_M] unfolding y_eq_fx by (simp add: inj_M insert_absorb)
next
case y_ne_fx: False
show ?thesis
using x_in_M ih[OF inj_M] y_ne_fx insert_absorb by fastforce
qed
next
case x_ni_M: False
show ?thesis
proof (cases "y = f x")
case y_eq_fx: True
have "f x ∉# image_mset f M"
using x_ni_M inj_xM by force
thus ?thesis
unfolding y_eq_fx
by (metis (no_types) inj_xM count_add_mset count_greater_eq_Suc_zero_iff count_inI
next
case y_ne_fx: False
show ?thesis
proof (rule ccontr)
assume neg_conj: "¬ count (image_mset f (add_mset x M)) y
≤ count (add_mset x M) (inv_into (set_mset (add_mset x M)) f y)"

have cnt_y: "count (add_mset (f x) (image_mset f M)) y = count (image_mset f M) y"
using y_ne_fx by simp

have "inv_into (set_mset M) f y ∈# add_mset x M ⟹
inv_into (set_mset (add_mset x M)) f (f (inv_into (set_mset M) f y)) =
inv_into (set_mset M) f y"
by (meson inj_xM inv_into_f_f)
hence "0 < count (image_mset f (add_mset x M)) y ⟹
count M (inv_into (set_mset M) f y) = 0 ∨ x = inv_into (set_mset M) f y"
using neg_conj cnt_y ih[OF inj_M]
by (metis (no_types) count_add_mset count_greater_zero_iff count_inI f_inv_into_f
thus False
using neg_conj cnt_y x_ni_M ih[OF inj_M]
by (metis (no_types) count_greater_zero_iff count_inI eq_iff image_mset_add_mset
less_imp_le)
qed
qed
qed
qed simp

lemma mset_filter_compl: "mset (filter p xs) + mset (filter (Not ∘ p) xs) = mset xs"
by (induction xs) (auto simp: ac_simps)

text ‹Near duplicate of @{thm [source] filter_eq_replicate_mset}: @{thm filter_eq_replicate_mset}.›

lemma filter_mset_eq: "filter_mset ((=) L) A = replicate_mset (count A L) L"
by (auto simp: multiset_eq_iff)

lemma filter_mset_cong[fundef_cong]:
assumes "M = M'" "⋀a. a ∈# M ⟹ P a = Q a"
shows "filter_mset P M = filter_mset Q M"
proof -
have "M - filter_mset Q M = filter_mset (λa. ¬Q a) M"
then show ?thesis
by (auto simp: filter_mset_eq_conv assms)
qed

lemma image_mset_filter_swap: "image_mset f {# x ∈# M. P (f x)#} = {# x ∈# image_mset f M. P x#}"
by (induction M) auto

lemma image_mset_cong2:
"(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ image_mset f M = image_mset g N"
by (hypsubst, rule image_mset_cong)

lemma filter_mset_empty_conv: ‹(filter_mset P M = {#}) = (∀L∈#M. ¬ P L)›
by (induction M) auto

lemma multiset_filter_mono2: ‹filter_mset P A ⊆# filter_mset Q A ⟷ (∀a∈#A. P a ⟶ Q a)›
by (induction A) (auto intro: subset_mset.trans)

lemma image_filter_cong:
assumes ‹⋀C. C ∈# M ⟹ P C ⟹ f C = g C›
shows ‹{#f C. C ∈# {#C ∈# M. P C#}#} = {#g C | C∈# M. P C#}›
using assms by (induction M) auto

lemma image_mset_filter_swap2: ‹{#C ∈# {#P x. x ∈# D#}. Q C #} = {#P x. x ∈# {#C| C ∈# D. Q (P C)#}#}›

declare image_mset_cong2 [cong]

lemma filter_mset_empty_if_finite_and_filter_set_empty:
assumes
"{x ∈ X. P x} = {}" and
"finite X"
shows "{#x ∈# mset_set X. P x#} = {#}"
proof -
have empty_empty: "⋀Y. set_mset Y = {} ⟹ Y = {#}"
by auto
from assms have "set_mset {#x ∈# mset_set X. P x#} = {}"
by auto
then show ?thesis
by (rule empty_empty)
qed

lemma sum_image_mset_sum_map[simp]: "sum_mset (image_mset f (mset xs)) = sum_list (map f xs)"
by (metis mset_map sum_mset_sum_list)

lemma sum_image_mset_mono:
fixes f :: "'a ⇒ 'b::canonically_ordered_monoid_add"
assumes sub: "A ⊆# B"
shows "(∑m ∈# A. f m) ≤ (∑m ∈# B. f m)"

lemma sum_image_mset_mono_mem:
"n ∈# M ⟹ f n ≤ (∑m ∈# M. f m)" for f :: "'a ⇒ 'b::canonically_ordered_monoid_add"

lemma count_sum_mset_if_1_0: ‹count M a = (∑x∈#M. if x = a then 1 else 0)›
by (induction M) auto

lemma sum_mset_dvd:
fixes k :: "'a::comm_semiring_1_cancel"
assumes "∀m ∈# M. k dvd f m"
shows "k dvd (∑m ∈# M. f m)"
using assms by (induct M) auto

lemma sum_mset_distrib_div_if_dvd:
fixes k :: "'a::unique_euclidean_semiring"
assumes "∀m ∈# M. k dvd f m"
shows "(∑m ∈# M. f m) div k = (∑m ∈# M. f m div k)"
using assms by (induct M) (auto simp: div_plus_div_distrib_dvd_left)

lemma set_mset_minus_replicate_mset[simp]:
"n ≥ count A a ⟹ set_mset (A - replicate_mset n a) = set_mset A - {a}"
"n < count A a ⟹ set_mset (A - replicate_mset n a) = set_mset A"
unfolding set_mset_def by (auto split: if_split simp: not_in_iff)

abbreviation removeAll_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" where
"removeAll_mset C M ≡ M - replicate_mset (count M C) C"

lemma mset_removeAll[simp, code]: "removeAll_mset C (mset L) = mset (removeAll C L)"
by (induction L) (auto simp: ac_simps multiset_eq_iff split: if_split_asm)

lemma removeAll_mset_filter_mset: "removeAll_mset C M = filter_mset ((≠) C) M"
by (induction M) (auto simp: ac_simps multiset_eq_iff)

abbreviation remove1_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" where
"remove1_mset C M ≡ M - {#C#}"

lemma removeAll_subseteq_remove1_mset: "removeAll_mset x M ⊆# remove1_mset x M"
by (auto simp: subseteq_mset_def)

lemma in_remove1_mset_neq:
assumes ab: "a ≠ b"
shows "a ∈# remove1_mset b C ⟷ a ∈# C"
by (metis assms diff_single_trivial in_diffD insert_DiffM insert_noteq_member)

lemma size_mset_removeAll_mset_le_iff: "size (removeAll_mset x M) < size M ⟷ x ∈# M"
by (auto intro: count_inI mset_subset_size simp: subset_mset_def multiset_eq_iff)

lemma size_remove1_mset_If: ‹size (remove1_mset x M) = size M - (if x ∈# M then 1 else 0)›
by (auto simp: size_Diff_subset_Int)

lemma size_mset_remove1_mset_le_iff: "size (remove1_mset x M) < size M ⟷ x ∈# M"
using less_irrefl
by (fastforce intro!: mset_subset_size elim: in_countE simp: subset_mset_def multiset_eq_iff)

lemma remove_1_mset_id_iff_notin: "remove1_mset a M = M ⟷ a ∉# M"
by (meson diff_single_trivial multi_drop_mem_not_eq)

lemma id_remove_1_mset_iff_notin: "M = remove1_mset a M ⟷ a ∉# M"
using remove_1_mset_id_iff_notin by metis

lemma remove1_mset_eqE:
"remove1_mset L x1 = M ⟹
(L ∈# x1 ⟹ x1 = M + {#L#} ⟹ P) ⟹
(L ∉# x1 ⟹ x1 = M ⟹ P) ⟹
P"
by (cases "L ∈# x1") auto

lemma image_filter_ne_mset[simp]:
"image_mset f {#x ∈# M. f x ≠ y#} = removeAll_mset y (image_mset f M)"
by (induction M) simp_all

lemma image_mset_remove1_mset_if:
"image_mset f (remove1_mset a M) =
(if a ∈# M then remove1_mset (f a) (image_mset f M) else image_mset f M)"
by (auto simp: image_mset_Diff)

lemma filter_mset_neq: "{#x ∈# M. x ≠ y#} = removeAll_mset y M"

lemma filter_mset_neq_cond: "{#x ∈# M. P x ∧ x ≠ y#} = removeAll_mset y {# x∈#M. P x#}"
by (metis filter_filter_mset filter_mset_neq)

"remove1_mset L (add_mset L' C) = (if L = L' then C else remove1_mset L C + {#L'#})"
by (auto simp: multiset_eq_iff)

lemma minus_remove1_mset_if:
"A - remove1_mset b B = (if b ∈# B ∧ b ∈# A ∧ count A b ≥ count B b then {#b#} + (A - B) else A - B)"
by (auto simp: multiset_eq_iff count_greater_zero_iff[symmetric]
simp del: count_greater_zero_iff)

"a ≠ b ⟹ add_mset a A = add_mset b B ⟷ a ∈# B ∧ b ∈# A ∧ A = add_mset b (B - {#a#})"
by (metis (no_types, lifting) diff_single_eq_union diff_union_swap multi_self_add_other_not_self
remove_1_mset_id_iff_notin union_single_eq_diff)

(a = b ∧ M = M') ∨ (a ≠ b ∧ b ∈# M ∧ add_mset a (M - {#b#}) = M')›

(* TODO move to Multiset: could replace add_mset_remove_trivial_eq? *)
lemma add_mset_remove_trivial_iff: ‹N = add_mset a (N - {#b#}) ⟷ a ∈# N ∧ a = b›
size_mset_remove1_mset_le_iff union_single_eq_member)

lemma trivial_add_mset_remove_iff: ‹add_mset a (N - {#b#}) = N ⟷ a ∈# N ∧ a = b›

lemma remove1_single_empty_iff[simp]: ‹remove1_mset L {#L'#} = {#} ⟷ L = L'›

assumes xM_lt_N: "add_mset x M < N"
shows "M < remove1_mset x N"
proof -
have "M < N"
using assms le_multiset_right_total mset_le_trans by blast
then show ?thesis
qed

lemma remove_diff_multiset[simp]: ‹x13 ∉# A ⟹ A - add_mset x13 B = A - B›

lemma removeAll_notin: ‹a ∉# A ⟹ removeAll_mset a A = A›
using count_inI by force

lemma mset_drop_upto: ‹mset (drop a N) = {#N!i. i ∈# mset_set {a..<length N}#}›
proof (induction N arbitrary: a)
case Nil
then show ?case by simp
next
case (Cons c N)
have upt: ‹{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}›
by auto
then have H: ‹mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})›
unfolding upt by auto
have mset_case_Suc: ‹{#case x of 0 ⇒ c | Suc x ⇒ N ! x . x ∈# mset_set {Suc a..<Suc b}#} =
{#N ! (x-1) . x ∈# mset_set {Suc a..<Suc b}#}› for a b
by (rule image_mset_cong) (auto split: nat.splits)
have Suc_Suc: ‹{Suc a..<Suc b} = Suc  {a..<b}› for a b
by auto
then have mset_set_Suc_Suc: ‹mset_set {Suc a..<Suc b} = {#Suc n. n ∈# mset_set {a..<b}#}› for a b
unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
have *: ‹{#N ! (x-Suc 0) . x ∈# mset_set {Suc a..<Suc b}#} = {#N ! x . x ∈# mset_set {a..<b}#}›
for a b
show ?case
apply (cases a)
using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
qed

lemma replicate_mset_minus_replicate_mset_same[simp]:
"replicate_mset m x - replicate_mset n x = replicate_mset (m - n) x"
by (induct m arbitrary: n, simp, metis left_diff_repeat_mset_distrib' repeat_mset_replicate_mset)

lemma replicate_mset_subset_iff_lt[simp]: "replicate_mset m x ⊂# replicate_mset n x ⟷ m < n"
by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI)

lemma replicate_mset_subseteq_iff_le[simp]: "replicate_mset m x ⊆# replicate_mset n x ⟷ m ≤ n"
by (induct n m rule: diff_induct) auto

lemma replicate_mset_lt_iff_lt[simp]: "replicate_mset m x < replicate_mset n x ⟷ m < n"
by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI gr_zeroI)

lemma replicate_mset_le_iff_le[simp]: "replicate_mset m x ≤ replicate_mset n x ⟷ m ≤ n"
by (induct n m rule: diff_induct) auto

lemma replicate_mset_eq_iff[simp]:
"replicate_mset m x = replicate_mset n y ⟷ m = n ∧ (m ≠ 0 ⟶ x = y)"
by (cases m; cases n; simp)
(metis in_replicate_mset insert_noteq_member size_replicate_mset union_single_eq_diff)

lemma replicate_mset_plus: "replicate_mset (a + b) C = replicate_mset a C + replicate_mset b C"
by (induct a) (auto simp: ac_simps)

lemma mset_replicate_replicate_mset: "mset (replicate n L) = replicate_mset n L"
by (induction n) auto

lemma set_mset_single_iff_replicate_mset: "set_mset U = {a} ⟷ (∃n > 0. U = replicate_mset n a)"
by (rule, metis count_greater_zero_iff count_replicate_mset insertI1 multi_count_eq singletonD
zero_less_iff_neq_zero, force)

lemma ex_replicate_mset_if_all_elems_eq:
assumes "∀x ∈# M. x = y"
shows "∃n. M = replicate_mset n y"
using assms by (metis count_replicate_mset mem_Collect_eq multiset_eqI neq0_conv set_mset_def)

subsection ‹Multiset and Set Conversions›

lemma count_mset_set_if: "count (mset_set A) a = (if a ∈ A ∧ finite A then 1 else 0)"
by auto

lemma mset_set_set_mset_empty_mempty[iff]: "mset_set (set_mset D) = {#} ⟷ D = {#}"

lemma count_mset_set_le_one: "count (mset_set A) x ≤ 1"

lemma mset_set_set_mset_subseteq[simp]: "mset_set (set_mset A) ⊆# A"

lemma mset_sorted_list_of_set[simp]: "mset (sorted_list_of_set A) = mset_set A"
by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)

lemma sorted_sorted_list_of_multiset[simp]:
"sorted (sorted_list_of_multiset (M :: 'a::linorder multiset))"
by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_mset sorted_sort)

lemma mset_take_subseteq: "mset (take n xs) ⊆# mset xs"
apply (induct xs arbitrary: n)
apply simp
by (case_tac n) simp_all

lemma sorted_list_of_multiset_eq_Nil[simp]: "sorted_list_of_multiset M = [] ⟷ M = {#}"
by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_empty)

subsection ‹Duplicate Removal›

(* TODO: use abbreviation? *)
definition remdups_mset :: "'v multiset ⇒ 'v multiset" where
"remdups_mset S = mset_set (set_mset S)"

lemma set_mset_remdups_mset[simp]: ‹set_mset (remdups_mset A) = set_mset A›
unfolding remdups_mset_def by auto

lemma count_remdups_mset_eq_1: "a ∈# remdups_mset A ⟷ count (remdups_mset A) a = 1"
unfolding remdups_mset_def by (auto simp: count_eq_zero_iff intro: count_inI)

lemma remdups_mset_empty[simp]: "remdups_mset {#} = {#}"
unfolding remdups_mset_def by auto

lemma remdups_mset_singleton[simp]: "remdups_mset {#a#} = {#a#}"
unfolding remdups_mset_def by auto

lemma remdups_mset_eq_empty[iff]: "remdups_mset D = {#} ⟷ D = {#}"
unfolding remdups_mset_def by blast

lemma remdups_mset_singleton_sum[simp]:
"remdups_mset (add_mset a A) = (if a ∈# A then remdups_mset A else add_mset a (remdups_mset A))"
unfolding remdups_mset_def by (simp_all add: insert_absorb)

lemma mset_remdups_remdups_mset[simp]: "mset (remdups D) = remdups_mset (mset D)"
by (induction D) (auto simp add: ac_simps)

declare mset_remdups_remdups_mset[symmetric, code]

lemma count_remdups_mset_If: ‹count (remdups_mset A) a = (if a ∈# A then 1 else 0)›
unfolding remdups_mset_def by auto

‹a ∉# A ⟹ add_mset a (remdups_mset A) = remdups_mset (add_mset a A)›
by auto

subsection ‹Repeat Operation›

lemma repeat_mset_compower: "repeat_mset n A = (((+) A) ^^ n) {#}"
by (induction n) auto

lemma repeat_mset_prod: "repeat_mset (m * n) A = (((+) (repeat_mset n A)) ^^ m) {#}"
by (induction m) (auto simp: repeat_mset_distrib)

subsection ‹Cartesian Product›

text ‹Definition of the cartesian products over multisets. The construction mimics of the cartesian
product on sets and use the same theorem names (adding only the suffix ‹_mset› to Sigma
and Times). See file @{file ‹~~/src/HOL/Product_Type.thy›}›

definition Sigma_mset :: "'a multiset ⇒ ('a ⇒ 'b multiset) ⇒ ('a × 'b) multiset" where
"Sigma_mset A B ≡ ∑⇩# {#{#(a, b). b ∈# B a#}. a ∈# A #}"

abbreviation Times_mset :: "'a multiset ⇒ 'b multiset ⇒ ('a × 'b) multiset" (infixr "×#" 80) where
"Times_mset A B ≡ Sigma_mset A (λ_. B)"

hide_const (open) Times_mset

text ‹Contrary to the set version @{term ‹SIGMA x:A. B›}, we use the non-ASCII symbol ‹∈#›.›

syntax
"_Sigma_mset" :: "[pttrn, 'a multiset, 'b multiset] => ('a * 'b) multiset"
("(3SIGMAMSET _∈#_./ _)" [0, 0, 10] 10)
translations
"SIGMAMSET x∈#A. B" == "CONST Sigma_mset A (λx. B)"

text ‹Link between the multiset and the set cartesian product:›

lemma Times_mset_Times: "set_mset (A ×# B) = set_mset A × set_mset B"
unfolding Sigma_mset_def by auto

lemma Sigma_msetI [intro!]: "⟦a ∈# A; b ∈# B a⟧ ⟹ (a, b) ∈# Sigma_mset A B"
by (unfold Sigma_mset_def) auto

lemma Sigma_msetE[elim!]: "⟦c ∈# Sigma_mset A B; ⋀x y. ⟦x ∈# A; y ∈# B x; c = (x, y)⟧ ⟹ P⟧ ⟹ P"
by (unfold Sigma_mset_def) auto

text ‹Elimination of @{term "(a, b) ∈# A ×# B"} -- introduces no eigenvariables.›

lemma Sigma_msetD1: "(a, b) ∈# Sigma_mset A B ⟹ a ∈# A"
by blast

lemma Sigma_msetD2: "(a, b) ∈# Sigma_mset A B ⟹ b ∈# B a"
by blast

lemma Sigma_msetE2: "⟦(a, b) ∈# Sigma_mset A B; ⟦a ∈# A; b ∈# B a⟧ ⟹ P⟧ ⟹ P"
by blast

lemma Sigma_mset_cong:
"⟦A = B; ⋀x. x ∈# B ⟹ C x = D x⟧ ⟹ (SIGMAMSET x ∈# A. C x) = (SIGMAMSET x ∈# B. D x)"
by (metis (mono_tags, lifting) Sigma_mset_def image_mset_cong)

lemma count_sum_mset: "count (∑⇩# M) b = (∑P ∈# M. count P b)"
by (induction M) auto

lemma Sigma_mset_plus_distrib1[simp]: "Sigma_mset (A + B) C = Sigma_mset A C + Sigma_mset B C"
unfolding Sigma_mset_def by auto

lemma Sigma_mset_plus_distrib2[simp]:
"Sigma_mset A (λi. B i + C i) = Sigma_mset A B + Sigma_mset A C"
unfolding Sigma_mset_def by (induction A) (auto simp: multiset_eq_iff)

lemma Times_mset_single_left: "{#a#} ×# B = image_mset (Pair a) B"
unfolding Sigma_mset_def by auto

lemma Times_mset_single_right: "A ×# {#b#} = image_mset (λa. Pair a b) A"
unfolding Sigma_mset_def by (induction A) auto

lemma Times_mset_single_single[simp]: "{#a#} ×# {#b#} = {#(a, b)#}"
unfolding Sigma_mset_def by simp

lemma count_image_mset_Pair:
"count (image_mset (Pair a) B) (x, b) = (if x = a then count B b else 0)"
by (induction B) auto

lemma count_Sigma_mset: "count (Sigma_mset A B) (a, b) = count A a * count (B a) b"
by (induction A) (auto simp: Sigma_mset_def count_image_mset_Pair)

lemma Sigma_mset_empty1[simp]: "Sigma_mset {#} B = {#}"
unfolding Sigma_mset_def by auto

lemma Sigma_mset_empty2[simp]: "A ×# {#} = {#}"
by (auto simp: multiset_eq_iff count_Sigma_mset)

lemma Sigma_mset_mono:
assumes "A ⊆# C" and "⋀x. x ∈# A ⟹ B x ⊆# D x"
shows "Sigma_mset A B ⊆# Sigma_mset C D"
proof -
have "count A a * count (B a) b ≤ count C a * count (D a) b" for a b
using assms unfolding subseteq_mset_def by (metis count_inI eq_iff mult_eq_0_iff mult_le_mono)
then show ?thesis
by (auto simp: subseteq_mset_def count_Sigma_mset)
qed

lemma mem_Sigma_mset_iff[iff]: "((a,b) ∈# Sigma_mset A B) = (a ∈# A ∧ b ∈# B a)"
by blast

lemma mem_Times_mset_iff: "x ∈# A ×# B ⟷ fst x ∈# A ∧ snd x ∈# B"
by (induct x) simp

lemma Sigma_mset_empty_iff: "(SIGMAMSET i∈#I. X i) = {#} ⟷ (∀i∈#I. X i = {#})"
by (auto simp: Sigma_mset_def)

lemma Times_mset_subset_mset_cancel1: "x ∈# A ⟹ (A ×# B ⊆# A ×# C) = (B ⊆# C)"
by (auto simp: subseteq_mset_def count_Sigma_mset)

lemma Times_mset_subset_mset_cancel2: "x ∈# C ⟹ (A ×# C ⊆# B ×# C) = (A ⊆# B)"
by (auto simp: subseteq_mset_def count_Sigma_mset)

lemma Times_mset_eq_cancel2: "x ∈# C ⟹ (A ×# C = B ×# C) = (A = B)"
by (auto simp: multiset_eq_iff count_Sigma_mset dest!: in_countE)

lemma split_paired_Ball_mset_Sigma_mset[simp]:
"(∀z∈#Sigma_mset A B. P z) ⟷ (∀x∈#A. ∀y∈#B x. P (x, y))"
by blast

lemma split_paired_Bex_mset_Sigma_mset[simp]:
"(∃z∈#Sigma_mset A B. P z) ⟷ (∃x∈#A. ∃y∈#B x. P (x, y))"
by blast

lemma sum_mset_if_eq_constant:
"(∑x∈#M. if a = x then (f x) else 0) = (((+) (f a)) ^^ (count M a)) 0"
by (induction M) (auto simp: ac_simps)

lemma iterate_op_plus: "(((+) k) ^^ m) 0 = k * m"
by (induction m) auto

lemma untion_image_mset_Pair_distribute:
"∑⇩#{#image_mset (Pair x) (C x). x ∈# J - I#} =
∑⇩# {#image_mset (Pair x) (C x). x ∈# J#} - ∑⇩#{#image_mset (Pair x) (C x). x ∈# I#}"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
iterate_op_plus diff_mult_distrib2)

lemma Sigma_mset_Un_distrib1: "Sigma_mset (I ∪# J) C = Sigma_mset I C ∪# Sigma_mset J C"
by (auto simp add: Sigma_mset_def union_mset_def untion_image_mset_Pair_distribute)

lemma Sigma_mset_Un_distrib2: "(SIGMAMSET i∈#I. A i ∪# B i) = Sigma_mset I A ∪# Sigma_mset I B"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def diff_mult_distrib2 iterate_op_plus max_def not_in_iff)

lemma Sigma_mset_Int_distrib1: "Sigma_mset (I ∩# J) C = Sigma_mset I C ∩# Sigma_mset J C"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def iterate_op_plus min_def not_in_iff)

lemma Sigma_mset_Int_distrib2: "(SIGMAMSET i∈#I. A i ∩# B i) = Sigma_mset I A ∩# Sigma_mset I B"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def iterate_op_plus min_def not_in_iff)

lemma Sigma_mset_Diff_distrib1: "Sigma_mset (I - J) C = Sigma_mset I C - Sigma_mset J C"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib2)

lemma Sigma_mset_Diff_distrib2: "(SIGMAMSET i∈#I. A i - B i) = Sigma_mset I A - Sigma_mset I B"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib)

lemma Sigma_mset_Union: "Sigma_mset (∑⇩#X) B = (∑⇩# (image_mset (λA. Sigma_mset A B) X))"
by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
Sigma_mset_def iterate_op_plus min_def not_in_iff sum_mset_distrib_left)

lemma Times_mset_Un_distrib1: "(A ∪# B) ×# C = A ×# C ∪# B ×# C"
by (fact Sigma_mset_Un_distrib1)

lemma Times_mset_Int_distrib1: "(A ∩# B) ×# C = A ×# C ∩# B ×# C"
by (fact Sigma_mset_Int_distrib1)

lemma Times_mset_Diff_distrib1: "(A - B) ×# C = A ×# C - B ×# C"
by (fact Sigma_mset_Diff_distrib1)

lemma Times_mset_empty[simp]: "A ×# B = {#} ⟷ A = {#} ∨ B = {#}"
by (auto simp: Sigma_mset_empty_iff)

lemma Times_insert_left: "A ×# add_mset x B = A ×# B + image_mset (λa. Pair a x) A"

lemma Times_insert_right: "add_mset a A ×# B = A ×# B + image_mset (Pair a) B"

lemma fst_image_mset_times_mset [simp]:
"image_mset fst (A ×# B) = (if B = {#} then {#} else repeat_mset (size B) A)"
by (induct B) (auto simp: Times_mset_single_right ac_simps Times_insert_left)

lemma snd_image_mset_times_mset [simp]:
"image_mset snd (A ×# B) = (if A = {#} then {#} else repeat_mset (size A) B)"
by (induct B) (auto simp add: Times_mset_single_right Times_insert_left image_mset_const_eq)

lemma product_swap_mset: "image_mset prod.swap (A ×# B) = B ×# A"
by (induction A) (auto simp add: Times_mset_single_left Times_mset_single_right
Times_insert_right Times_insert_left)

context
begin

qualified definition product_mset :: "'a multiset ⇒ 'b multiset ⇒ ('a × 'b) multiset" where
[code_abbrev]: "product_mset A B = A ×# B"

lemma member_product_mset: "x ∈# product_mset A B ⟷ x ∈# A ×# B"

end

lemma count_Sigma_mset_abs_def: "count (Sigma_mset A B) = (λ(a, b) ⇒ count A a * count (B a) b)"
by (auto simp: fun_eq_iff count_Sigma_mset)

lemma Times_mset_image_mset1: "image_mset f A ×# B = image_mset (λ(a, b). (f a, b)) (A ×# B)"
by (induct B) (auto simp: Times_insert_left)

lemma Times_mset_image_mset2: "A ×# image_mset f B = image_mset (λ(a, b). (a, f b)) (A ×# B)"
by (induct A) (auto simp: Times_insert_right)

lemma sum_le_singleton: "A ⊆ {x} ⟹ sum f A = (if x ∈ A then f x else 0)"
by (auto simp: subset_singleton_iff elim: finite_subset)

lemma Times_mset_assoc: "(A ×# B) ×# C = image_mset (λ(a, b, c). ((a, b), c)) (A ×# B ×# C)"
by (auto simp: multiset_eq_iff count_Sigma_mset count_image_mset vimage_def Times_mset_Times
Int_commute count_eq_zero_iff intro!: trans[OF _ sym[OF sum_le_singleton[of _ "(_, _, _)"]]]
cong: sum.cong if_cong)

subsection ‹Transfer Rules›

lemma plus_multiset_transfer[transfer_rule]:
"(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (+) (+)"
by (unfold rel_fun_def rel_mset_def)
(force dest: list_all2_appendI intro: exI[of _ "_ @ _"] conjI[rotated])

lemma minus_multiset_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique R"
shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (-) (-)"
proof (unfold rel_fun_def rel_mset_def, safe)
fix xs ys xs' ys'
assume [transfer_rule]: "list_all2 R xs ys" "list_all2 R xs' ys'"
have "list_all2 R (fold remove1 xs' xs) (fold remove1 ys' ys)"
by transfer_prover
moreover have "mset (fold remove1 xs' xs) = mset xs - mset xs'"
by (induct xs' arbitrary: xs) auto
moreover have "mset (fold remove1 ys' ys) = mset ys - mset ys'"
by (induct ys' arbitrary: ys) auto
ultimately show "∃xs'' ys''.
mset xs'' = mset xs - mset xs' ∧ mset ys'' = mset ys - mset ys' ∧ list_all2 R xs'' ys''"
by blast
qed

declare rel_mset_Zero[transfer_rule]

lemma count_transfer[transfer_rule]:
assumes "bi_unique R"
shows "(rel_fun (rel_mset R) (rel_fun R (=))) count count"
unfolding rel_fun_def rel_mset_def proof safe
fix x y xs ys
assume "list_all2 R xs ys" "R x y"
then show "count (mset xs) x = count (mset ys) y"
proof (induct xs ys rule: list.rel_induct)
case (Cons x' xs y' ys)
then show ?case
using assms unfolding bi_unique_alt_def2 by (auto simp: rel_fun_def)
qed simp
qed

lemma subseteq_multiset_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique R" "right_total R"
shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (=)))
(λM N. filter_mset (Domainp R) M ⊆# filter_mset (Domainp R) N) (⊆#)"
proof -
have count_filter_mset_less:
"(∀a. count (filter_mset (Domainp R) M) a ≤ count (filter_mset (Domainp R) N) a) ⟷
(∀a ∈ {x. Domainp R x}. count M a ≤ count N a)" for M and N by auto
show ?thesis unfolding subseteq_mset_def count_filter_mset_less
by transfer_prover
qed

lemma sum_mset_transfer[transfer_rule]:
"R 0 0 ⟹ rel_fun R (rel_fun R R) (+) (+) ⟹ (rel_fun (rel_mset R) R) sum_mset sum_mset"
using sum_list_transfer[of R] unfolding rel_fun_def rel_mset_def by auto

lemma Sigma_mset_transfer[transfer_rule]:
"(rel_fun (rel_mset R) (rel_fun (rel_fun R (rel_mset S)) (rel_mset (rel_prod R S))))
Sigma_mset Sigma_mset"
by (unfold Sigma_mset_def) transfer_prover

subsubsection ‹Multisets and Functions›

lemma range_image_mset:
assumes "set_mset Ds ⊆ range f"
shows "Ds ∈ range (image_mset f)"
proof -
have "∀D. D ∈# Ds ⟶ (∃C. f C = D)"
using assms by blast
then obtain f_i where
f_p: "∀D. D ∈# Ds ⟶ (f (f_i D) = D)"
by metis
define Cs where
"Cs ≡ image_mset f_i Ds"
from f_p Cs_def have "image_mset f Cs = Ds"
by auto
then show ?thesis
by blast
qed

subsubsection ‹Multisets and Lists›

lemma length_sorted_list_of_multiset[simp]: "length (sorted_list_of_multiset A) = size A"
by (metis mset_sorted_list_of_multiset size_mset)

definition list_of_mset :: "'a multiset ⇒ 'a list" where
"list_of_mset m = (SOME l. m = mset l)"

lemma list_of_mset_exi: "∃l. m = mset l"
using ex_mset by metis

lemma mset_list_of_mset[simp]: "mset (list_of_mset m) = m"
by (metis (mono_tags, lifting) ex_mset list_of_mset_def someI_ex)

lemma length_list_of_mset[simp]: "length (list_of_mset A) = size A"
unfolding list_of_mset_def by (metis (mono_tags) ex_mset size_mset someI_ex)

lemma range_mset_map:
assumes "set_mset Ds ⊆ range f"
shows "Ds ∈ range (λCl. mset (map f Cl))"
proof -
have "Ds ∈ range (image_mset f)"
then obtain Cs where Cs_p: "image_mset f Cs = Ds"
by auto
define Cl where "Cl = list_of_mset Cs"
then have "mset Cl = Cs"
by auto
then have "image_mset f (mset Cl) = Ds"
using Cs_p by auto
then have "mset (map f Cl) = Ds"
by auto
then show ?thesis
by auto
qed

lemma list_of_mset_empty[iff]: "list_of_mset m = [] ⟷ m = {#}"
by (metis (mono_tags, lifting) ex_mset list_of_mset_def mset_zero_iff_right someI_ex)

lemma in_mset_conv_nth: "(x ∈# mset xs) = (∃i<length xs. xs ! i = x)"
by (auto simp: in_set_conv_nth)

lemma in_mset_sum_list:
assumes "L ∈# LL"
assumes "LL ∈ set Ci"
shows "L ∈# sum_list Ci"
using assms by (induction Ci) auto

lemma in_mset_sum_list2:
assumes "L ∈# sum_list Ci"
obtains LL where
"LL ∈ set Ci"
"L ∈# LL"
using assms by (induction Ci) auto

(* TODO: Make [simp]. *)
lemma in_mset_sum_list_iff: "a ∈# sum_list 𝒜 ⟷ (∃A ∈ set 𝒜. a ∈# A)"
by (metis in_mset_sum_list in_mset_sum_list2)

lemma subseteq_list_Union_mset:
assumes "length Ci = n"
assumes "length CAi = n"
assumes "∀i<n.  Ci ! i ⊆# CAi ! i "
shows "∑⇩# (mset Ci) ⊆# ∑⇩# (mset CAi)"
using assms proof (induction n arbitrary: Ci CAi)
case 0
then show ?case by auto
next
case (Suc n)
from Suc have "∀i<n. tl Ci ! i ⊆# tl CAi ! i"
hence "∑⇩#(mset (tl Ci)) ⊆# ∑⇩#(mset (tl CAi))" using Suc by auto
moreover
have "hd Ci ⊆# hd CAi" using Suc
by (metis hd_conv_nth length_greater_0_conv zero_less_Suc)
ultimately
show "∑⇩#(mset Ci) ⊆# ∑⇩#(mset CAi)"
using Suc by (cases Ci; cases CAi) (auto intro: subset_mset.add_mono)
qed

lemma same_mset_distinct_iff:
‹mset M = mset M' ⟹ distinct M ⟷ distinct M'›
by (fact mset_eq_imp_distinct_iff)

subsubsection ‹More on Multisets and Functions›

lemma subseteq_mset_size_eql: "X ⊆# Y ⟹ size Y = size X ⟹ X = Y"
using mset_subset_size subset_mset_def by fastforce

lemma image_mset_of_subset_list:
assumes "image_mset η C' = mset lC"
shows "∃qC'. map η qC' = lC ∧ mset qC' = C'"
using assms apply (induction lC arbitrary: C')
subgoal by simp
subgoal by (fastforce dest!: msed_map_invR intro: exI[of _ ‹_ # _›])
done

lemma image_mset_of_subset:
assumes "A ⊆# image_mset η C'"
shows "∃A'. image_mset η A' = A ∧ A' ⊆# C'"
proof -
define C where "C = image_mset η C'"

define lA where "lA = list_of_mset A"
define lD where "lD = list_of_mset (C-A)"
define lC where "lC = lA @ lD"

have "mset lC = C"
using C_def assms unfolding lD_def lC_def lA_def by auto
then have "∃qC'. map η qC' = lC ∧ mset qC' = C'"
using assms image_mset_of_subset_list unfolding C_def by metis
then obtain qC' where qC'_p: "map η qC' = lC ∧ mset qC' = C'"
by auto
let ?lA' = "take (length lA) qC'"
have m: "map η ?lA' = lA"
using qC'_p lC_def
by (metis append_eq_conv_conj take_map)
let ?A' = "mset ?lA'"

have "image_mset η ?A' = A"
using m using lA_def
by (metis (full_types) ex_mset list_of_mset_def mset_map someI_ex)
moreover have "?A' ⊆# C'"
using qC'_p unfolding lA_def
using mset_take_subseteq by blast
ultimately show ?thesis by blast
qed

lemma all_the_same: "∀x ∈# X. x = y ⟹ card (set_mset X) ≤ Suc 0"
by (metis card.empty card.insert card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI)

lemma Melem_subseteq_Union_mset[simp]:
assumes "x ∈# T"
shows "x ⊆# ∑⇩#T"
using assms sum_mset.remove by force

lemma Melem_subset_eq_sum_list[simp]:
assumes "x ∈# mset T"
shows "x ⊆# sum_list T"
using assms by (metis mset_subset_eq_add_left sum_mset.remove sum_mset_sum_list)

lemma less_subset_eq_Union_mset[simp]:
assumes "i < length CAi"
shows "CAi ! i ⊆# ∑⇩#(mset CAi)"
proof -
from assms have "CAi ! i ∈# mset CAi"
by auto
then show ?thesis
by auto
qed

lemma less_subset_eq_sum_list[simp]:
assumes "i < length CAi"
shows "CAi ! i ⊆# sum_list CAi"
proof -
from assms have "CAi ! i ∈# mset CAi"
by auto
then show ?thesis
by auto
qed

subsubsection ‹More on Multiset Order›

lemma less_multiset_doubletons:
assumes
"y < t ∨ y < s"
"x < t ∨ x < s"
shows
"{#y, x#} < {#t, s#}"
unfolding less_multiset⇩D⇩M
proof (intro exI)
let ?X = "{#t, s#}"
let ?Y = "{#y, x#}"
show "?X ≠ {#} ∧ ?X ⊆# {#t, s#} ∧ {#y, x#} = {#t, s#} - ?X + ?Y
∧ (∀k. k ∈# ?Y ⟶ (∃a. a ∈# ?X ∧ k < a))"
qed

end


# Theory Signed_Multiset

(*  Title:       Signed (Finite) Multisets
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Signed (Finite) Multisets›

theory Signed_Multiset
imports Multiset_More
abbrevs
"!z" = "⇩z"
begin

subsection ‹Definition of Signed Multisets›

definition equiv_zmset :: "'a multiset × 'a multiset ⇒ 'a multiset × 'a multiset ⇒ bool" where
"equiv_zmset = (λ(Mp, Mn) (Np, Nn). Mp + Nn = Np + Mn)"

quotient_type 'a zmultiset = "'a multiset × 'a multiset" / equiv_zmset
by (rule equivpI, simp_all add: equiv_zmset_def reflp_def symp_def transp_def)
(metis multi_union_self_other_eq union_lcomm)

subsection ‹Basic Operations on Signed Multisets›

begin

lift_definition zero_zmultiset :: "'a zmultiset" is "({#}, {#})" .

abbreviation empty_zmset :: "'a zmultiset" ("{#}⇩z") where
"empty_zmset ≡ 0"

lift_definition minus_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ 'a zmultiset" is
"λ(Mp, Mn) (Np, Nn). (Mp + Nn, Mn + Np)"
by (auto simp: equiv_zmset_def union_commute union_lcomm)

lift_definition plus_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ 'a zmultiset" is
"λ(Mp, Mn) (Np, Nn). (Mp + Np, Mn + Nn)"
by (auto simp: equiv_zmset_def union_commute union_lcomm)

instance
by (intro_classes; transfer) (auto simp: equiv_zmset_def)

end

begin

lift_definition uminus_zmultiset :: "'a zmultiset ⇒ 'a zmultiset" is "λ(Mp, Mn). (Mn, Mp)"

instance
by (intro_classes; transfer) (auto simp: equiv_zmset_def)

end

lift_definition zcount :: "'a zmultiset ⇒ 'a ⇒ int" is
"λ(Mp, Mn) x. int (count Mp x) - int (count Mn x)"
by (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff diff_eq_eq

lemma zcount_inject: "zcount M = zcount N ⟷ M = N"
by transfer (auto simp del: of_nat_add simp: equiv_zmset_def fun_eq_iff multiset_eq_iff

lemma zmultiset_eq_iff: "M = N ⟷ (∀a. zcount M a = zcount N a)"
by (simp only: zcount_inject[symmetric] fun_eq_iff)

lemma zmultiset_eqI: "(⋀x. zcount A x = zcount B x) ⟹ A = B"
using zmultiset_eq_iff by auto

lemma zcount_uminus[simp]: "zcount (- A) x = - zcount A x"
by transfer auto

lift_definition add_zmset :: "'a ⇒ 'a zmultiset ⇒ 'a zmultiset" is
"λx (Mp, Mn). (add_mset x Mp, Mn)"
by (auto simp: equiv_zmset_def)

syntax
"_zmultiset" :: "args ⇒ 'a zmultiset" ("{#(_)#}⇩z")
translations
"{#x, xs#}⇩z" == "CONST add_zmset x {#xs#}⇩z"
"{#x#}⇩z" == "CONST add_zmset x {#}⇩z"

lemma zcount_empty[simp]: "zcount {#}⇩z a = 0"
by transfer auto

"zcount (add_zmset b A) a = (if b = a then zcount A a + 1 else zcount A a)"
by transfer auto

lemma zcount_single: "zcount {#b#}⇩z a = (if b = a then 1 else 0)"
by simp

by (auto simp: zmultiset_eq_iff)

by (auto simp: zmultiset_eq_iff)

lemma
singleton_ne_empty_zmset[simp]: "{#x#}⇩z ≠ {#}⇩z" and
empty_ne_singleton_zmset[simp]: "{#}⇩z ≠ {#x#}⇩z"
by (auto dest!: arg_cong2[of _ _ x _ zcount])

lemma
singleton_ne_uminus_singleton_zmset[simp]: "{#x#}⇩z ≠ - {#y#}⇩z" and
uminus_singleton_ne_singleton_zmset[simp]: "- {#x#}⇩z ≠ {#y#}⇩z"
by (auto dest!: arg_cong2[of _ _ x x zcount] split: if_splits)

subsubsection ‹Conversion to Set and Membership›

definition set_zmset :: "'a zmultiset ⇒ 'a set" where
"set_zmset M = {x. zcount M x ≠ 0}"

abbreviation elem_zmset :: "'a ⇒ 'a zmultiset ⇒ bool" where
"elem_zmset a M ≡ a ∈ set_zmset M"

notation
elem_zmset ("'(∈#⇩z')") and
elem_zmset ("(_/ ∈#⇩z _)" [51, 51] 50)

notation (ASCII)
elem_zmset ("'(:#z')") and
elem_zmset ("(_/ :#z _)" [51, 51] 50)

abbreviation not_elem_zmset :: "'a ⇒ 'a zmultiset ⇒ bool" where
"not_elem_zmset a M ≡ a ∉ set_zmset M"

notation
not_elem_zmset ("'(∉#⇩z')") and
not_elem_zmset ("(_/ ∉#⇩z _)" [51, 51] 50)

notation (ASCII)
not_elem_zmset ("'(~:#z')") and
not_elem_zmset ("(_/ ~:#z _)" [51, 51] 50)

context
begin

qualified abbreviation Ball :: "'a zmultiset ⇒ ('a ⇒ bool) ⇒ bool" where
"Ball M ≡ Set.Ball (set_zmset M)"

qualified abbreviation Bex :: "'a zmultiset ⇒ ('a ⇒ bool) ⇒ bool" where
"Bex M ≡ Set.Bex (set_zmset M)"

end

syntax
"_ZMBall" :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool" ("(3∀_∈#⇩z_./ _)" [0, 0, 10] 10)
"_ZMBex" :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool" ("(3∃_∈#⇩z_./ _)" [0, 0, 10] 10)

syntax (ASCII)
"_ZMBall" :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool" ("(3∀_:#⇩z_./ _)" [0, 0, 10] 10)
"_ZMBex" :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool" ("(3∃_:#⇩z_./ _)" [0, 0, 10] 10)

translations
"∀x∈#⇩zA. P" ⇌ "CONST Signed_Multiset.Ball A (λx. P)"
"∃x∈#⇩zA. P" ⇌ "CONST Signed_Multiset.Bex A (λx. P)"

lemma zcount_eq_zero_iff: "zcount M x = 0 ⟷ x ∉#⇩z M"

lemma not_in_iff_zmset: "x ∉#⇩z M ⟷ zcount M x = 0"

lemma zcount_ne_zero_iff[simp]: "zcount M x ≠ 0 ⟷ x ∈#⇩z M"

lemma zcount_inI:
assumes "zcount M x = 0 ⟹ False"
shows "x ∈#⇩z M"
proof (rule ccontr)
assume "x ∉#⇩z M"
with assms show False by (simp add: not_in_iff_zmset)
qed

lemma set_zmset_empty[simp]: "set_zmset {#}⇩z = {}"

lemma set_zmset_single: "set_zmset {#b#}⇩z = {b}"

lemma set_zmset_eq_empty_iff[simp]: "set_zmset M = {} ⟷ M = {#}⇩z"
by (auto simp add: zmultiset_eq_iff zcount_eq_zero_iff)

lemma finite_count_ne: "finite {x. count M x ≠ count N x}"
proof -
have "{x. count M x ≠ count N x} ⊆ set_mset M ∪ set_mset N"
by (auto simp: not_in_iff)
moreover have "finite (set_mset M ∪ set_mset N)"
by (rule finite_UnI[OF finite_set_mset finite_set_mset])
ultimately show ?thesis
by (rule finite_subset)
qed

lemma finite_set_zmset[iff]: "finite (set_zmset M)"
unfolding set_zmset_def by transfer (auto intro: finite_count_ne)

lemma zmultiset_nonemptyE[elim]:
assumes "A ≠ {#}⇩z"
obtains x where "x ∈#⇩z A"
proof -
have "∃x. x ∈#⇩z A"
by (rule ccontr) (insert assms, auto)
with that show ?thesis
by blast
qed

subsubsection ‹Union›

lemma zcount_union[simp]: "zcount (M + N) a = zcount M a + zcount N a"
by transfer auto

by (auto simp: zmultiset_eq_iff)

by (auto simp: zmultiset_eq_iff)

subsubsection ‹Difference›

lemma zcount_diff[simp]: "zcount (M - N) a = zcount M a - zcount N a"
by transfer auto

by (auto simp: zmultiset_eq_iff)

lemma in_diff_zcount: "a ∈#⇩z M - N ⟷ zcount N a ≠ zcount M a"
by (fastforce simp: set_zmset_def)

fixes M N Q :: "'a zmultiset"
shows "M - (N + Q) = M - N - Q"

lemma insert_Diff_zmset[simp]: "add_zmset x (M - {#x#}⇩z) = M"
by (clarsimp simp: zmultiset_eq_iff)

lemma diff_union_swap_zmset: "add_zmset b (M - {#a#}⇩z) = add_zmset b M - {#a#}⇩z"

lemma diff_diff_add_zmset[simp]: "(M :: 'a zmultiset) - N - P = M - (N + P)"

obtains B where "A = add_zmset a B"
proof -
have "A = add_zmset a (A - {#a#}⇩z)"
by simp
with that show thesis .
qed

subsubsection ‹Equality of Signed Multisets›

lemma single_eq_single_zmset[simp]: "{#a#}⇩z = {#b#}⇩z ⟷ a = b"

by simp

lemma diff_single_eq_union_zmset: "M - {#x#}⇩z = N ⟷ M = add_zmset x N"
by auto

lemma union_single_eq_diff_zmset: "add_zmset x M = N ⟹ M = N - {#x#}⇩z"

M = N ∧ a = b ∨ M = add_zmset b (N - {#a#}⇩z) ∧ N = add_zmset a (M - {#b#}⇩z)"

(M = N ∧ a = b ∨ (∃K. M = add_zmset b K ∧ N = add_zmset a K))"

lemma multi_member_split: "∃A. M = add_zmset x A"
by (rule exI[where x = "M - {#x#}⇩z"]) simp

subsection ‹Conversions from and to Multisets›

lift_definition zmset_of :: "'a multiset ⇒ 'a zmultiset" is "λf. (Abs_multiset f, {#})" .

lemma zmset_of_inject[simp]: "zmset_of M = zmset_of N ⟷ M = N"
by (simp add: zmset_of_def, transfer, auto simp: equiv_zmset_def)

lemma zmset_of_empty[simp]: "zmset_of {#} = {#}⇩z"

by transfer (auto simp: equiv_zmset_def add_mset_def cong: if_cong)

lemma zcount_of_mset[simp]: "zcount (zmset_of M) x = int (count M x)"
by (induct M) auto

lemma zmset_of_plus: "zmset_of (M + N) = zmset_of M + zmset_of N"
by (transfer, auto simp: equiv_zmset_def eq_onp_same_args plus_multiset.abs_eq)+

lift_definition mset_pos :: "'a zmultiset ⇒ 'a multiset" is "λ(Mp, Mn). count (Mp - Mn)"
by (auto simp add: equiv_zmset_def simp flip: set_mset_diff)

lift_definition mset_neg :: "'a zmultiset ⇒ 'a multiset" is "λ(Mp, Mn). count (Mn - Mp)"
by (auto simp add: equiv_zmset_def simp flip: set_mset_diff)

lemma
zmset_of_inverse[simp]: "mset_pos (zmset_of M) = M" and
minus_zmset_of_inverse[simp]: "mset_neg (- zmset_of M) = M"
by (transfer, simp)+

lemma neg_zmset_pos[simp]: "mset_neg (zmset_of M) = {#}"
by (rule zmset_of_inject[THEN iffD1], simp, transfer, auto simp: equiv_zmset_def)+

lemma
count_mset_pos[simp]: "count (mset_pos M) x = nat (zcount M x)" and
count_mset_neg[simp]: "count (mset_neg M) x = nat (- zcount M x)"
by (transfer; auto)+

lemma
mset_pos_empty[simp]: "mset_pos {#}⇩z = {#}" and
mset_neg_empty[simp]: "mset_neg {#}⇩z = {#}"
by (rule multiset_eqI, simp)+

lemma
mset_pos_singleton[simp]: "mset_pos {#x#}⇩z = {#x#}" and
mset_neg_singleton[simp]: "mset_neg {#x#}⇩z = {#}"
by (rule multiset_eqI, simp)+

lemma
mset_pos_neg_partition: "M = zmset_of (mset_pos M) - zmset_of (mset_neg M)" and
mset_pos_as_neg: "zmset_of (mset_pos M) = zmset_of (mset_neg M) + M" and
mset_neg_as_pos: "zmset_of (mset_neg M) = zmset_of (mset_pos M) - M"
by (rule zmultiset_eqI, simp)+

lemma mset_pos_uminus[simp]: "mset_pos (- A) = mset_neg A"
by (rule multiset_eqI) simp

lemma mset_neg_uminus[simp]: "mset_neg (- A) = mset_pos A"
by (rule multiset_eqI) simp

lemma mset_pos_plus[simp]:
"mset_pos (A + B) = (mset_pos A - mset_neg B) + (mset_pos B - mset_neg A)"
by (rule multiset_eqI) simp

lemma mset_neg_plus[simp]:
"mset_neg (A + B) = (mset_neg A - mset_pos B) + (mset_neg B - mset_pos A)"
by (rule multiset_eqI) simp

lemma mset_pos_diff[simp]:
"mset_pos (A - B) = (mset_pos A - mset_pos B) + (mset_neg B - mset_neg A)"
by (rule mset_pos_plus[of A "- B", simplified])

lemma mset_neg_diff[simp]:
"mset_neg (A - B) = (mset_neg A - mset_neg B) + (mset_pos B - mset_pos A)"
by (rule mset_neg_plus[of A "- B", simplified])

lemma mset_pos_neg_dual:
"mset_pos a + mset_pos b + (mset_neg a - mset_pos b) + (mset_neg b - mset_pos a) =
mset_neg a + mset_neg b + (mset_pos a - mset_neg b) + (mset_pos b - mset_neg a)"
using [[linarith_split_limit = 20]] by (rule multiset_eqI) simp

lemma decompose_zmset_of2:
obtains A B C where
"M = zmset_of A + C" and
"N = zmset_of B + C"
proof
let ?A = "zmset_of (mset_pos M + mset_neg N)"
let ?B = "zmset_of (mset_pos N + mset_neg M)"
let ?C = "- (zmset_of (mset_neg M) + zmset_of (mset_neg N))"

show "M = ?A + ?C"
show "N = ?B + ?C"
qed

subsubsection ‹Pointwise Ordering Induced by @{const zcount}›

definition subseteq_zmset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" (infix "⊆#⇩z" 50) where
"A ⊆#⇩z B ⟷ (∀a. zcount A a ≤ zcount B a)"

definition subset_zmset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" (infix "⊂#⇩z" 50) where
"A ⊂#⇩z B ⟷ A ⊆#⇩z B ∧ A ≠ B"

abbreviation (input)
supseteq_zmset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" (infix "⊇#⇩z" 50)
where
"supseteq_zmset A B ≡ B ⊆#⇩z A"

abbreviation (input)
supset_zmset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" (infix "⊃#⇩z" 50)
where
"supset_zmset A B ≡ B ⊂#⇩z A"

notation (input)
subseteq_zmset (infix "⊆#⇩z" 50) and
supseteq_zmset (infix "⊇#⇩z" 50)

notation (ASCII)
subseteq_zmset (infix "⊆#⇩z" 50) and
subset_zmset (infix "⊂#⇩z" 50) and
supseteq_zmset (infix "⊇#⇩z" 50) and
supset_zmset (infix ">#⇩z" 50)

interpretation subset_zmset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(⊆#⇩z)" "(⊂#⇩z)"
by unfold_locales (auto simp add: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff
intro: order_trans antisym)

interpretation subset_zmset:
ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(⊆#⇩z)" "(⊂#⇩z)"
by unfold_locales

lemma zmset_subset_eqI: "(⋀a. zcount A a ≤ zcount B a) ⟹ A ⊆#⇩z B"

lemma zmset_subset_eq_zcount: "A ⊆#⇩z B ⟹ zcount A a ≤ zcount B a"

lemma zmset_subset_eq_zmultiset_union_diff_commute:
"A - B + C = A + C - B" for A B C :: "'a zmultiset"

lemma zmset_subset_eq_insertD: "add_zmset x A ⊆#⇩z B ⟹ A ⊂#⇩z B"
unfolding subset_zmset_def subseteq_zmset_def
le_numeral_extra(2))

lemma zmset_subset_insertD: "add_zmset x A ⊂#⇩z B ⟹ A ⊂#⇩z B"
by (rule zmset_subset_eq_insertD) (rule subset_zmset.less_imp_le)

lemma subset_eq_diff_conv_zmset: "A - C ⊆#⇩z B ⟷ A ⊆#⇩z B + C"

by (auto simp: subset_zmset_def subseteq_zmset_def)

lemma multi_psub_self_zmset: "A ⊂#⇩z A = False"
by simp

lemma zmset_of_subseteq_iff[simp]: "zmset_of M ⊆#⇩z zmset_of N ⟷ M ⊆# N"

lemma zmset_of_subset_iff[simp]: "zmset_of M ⊂#⇩z zmset_of N ⟷ M ⊂# N"

lemma
mset_pos_supset: "A ⊆#⇩z zmset_of (mset_pos A)" and
mset_neg_supset: "- A ⊆#⇩z zmset_of (mset_neg A)"
by (auto intro: zmset_subset_eqI)

lemma subset_mset_zmsetE:
assumes "M ⊂#⇩z N"
obtains A B C where
"M = zmset_of A + C" and "N = zmset_of B + C" and "A ⊂# B"
by (metis assms decompose_zmset_of2 subset_zmset.add_less_cancel_right zmset_of_subset_iff)

lemma subseteq_mset_zmsetE:
assumes "M ⊆#⇩z N"
obtains A B C where
"M = zmset_of A + C" and "N = zmset_of B + C" and "A ⊆# B"
subset_mset_zmsetE subset_zmset_def zmset_of_empty)

subsubsection ‹Subset is an Order›

interpretation subset_zmset: order "(⊆#⇩z)" "(⊂#⇩z)"
by unfold_locales

subsection ‹Replicate and Repeat Operations›

definition replicate_zmset :: "nat ⇒ 'a ⇒ 'a zmultiset" where
"replicate_zmset n x = (add_zmset x ^^ n) {#}⇩z"

lemma replicate_zmset_0[simp]: "replicate_zmset 0 x = {#}⇩z"
unfolding replicate_zmset_def by simp

lemma replicate_zmset_Suc[simp]: "replicate_zmset (Suc n) x = add_zmset x (replicate_zmset n x)"
unfolding replicate_zmset_def by (induct n) (auto intro: add.commute)

lemma count_replicate_zmset[simp]:
"zcount (replicate_zmset n x) y = (if y = x then of_nat n else 0)"
unfolding replicate_zmset_def by (induct n) auto

fun repeat_zmset :: "nat ⇒ 'a zmultiset ⇒ 'a zmultiset" where
"repeat_zmset 0 _ = {#}⇩z" |
"repeat_zmset (Suc n) A = A + repeat_zmset n A"

lemma count_repeat_zmset[simp]: "zcount (repeat_zmset i A) a = of_nat i * zcount A a"
by (induct i) (auto simp: semiring_normalization_rules(3))

lemma repeat_zmset_right[simp]: "repeat_zmset a (repeat_zmset b A) = repeat_zmset (a * b) A"
by (auto simp: zmultiset_eq_iff left_diff_distrib')

lemma left_diff_repeat_zmset_distrib':
‹i ≥ j ⟹ repeat_zmset (i - j) u = repeat_zmset i u - repeat_zmset j u›
by (auto simp: zmultiset_eq_iff int_distrib(3) of_nat_diff)

"repeat_zmset i u + (repeat_zmset j u + k) = repeat_zmset (i+j) u + k"
by (auto simp: zmultiset_eq_iff add_mult_distrib int_distrib(1))

lemma repeat_zmset_distrib: "repeat_zmset (m + n) A = repeat_zmset m A + repeat_zmset n A"
by (auto simp: zmultiset_eq_iff Nat.add_mult_distrib int_distrib(1))

lemma repeat_zmset_distrib2[simp]:
"repeat_zmset n (A + B) = repeat_zmset n A + repeat_zmset n B"
by (auto simp: zmultiset_eq_iff add_mult_distrib2 int_distrib(2))

lemma repeat_zmset_replicate_zmset[simp]: "repeat_zmset n {#a#}⇩z = replicate_zmset n a"
by (auto simp: zmultiset_eq_iff)

"repeat_zmset n (add_zmset a A) = replicate_zmset n a + repeat_zmset n A"
by (auto simp: zmultiset_eq_iff int_distrib(2))

lemma repeat_zmset_empty[simp]: "repeat_zmset n {#}⇩z = {#}⇩z"
by (induct n) simp_all

subsubsection ‹Filter (with Comprehension Syntax)›

lift_definition filter_zmset :: "('a ⇒ bool) ⇒ 'a zmultiset ⇒ 'a zmultiset" is
"λP (Mp, Mn). (filter_mset P Mp, filter_mset P Mn)"
by (auto simp del: filter_union_mset simp: equiv_zmset_def filter_union_mset[symmetric])

syntax (ASCII)
"_ZMCollect" :: "pttrn ⇒ 'a zmultiset ⇒ bool ⇒ 'a zmultiset" ("(1{#_ :#z _./ _#})")
syntax
"_ZMCollect" :: "pttrn ⇒ 'a zmultiset ⇒ bool ⇒ 'a zmultiset" ("(1{#_ ∈#⇩z _./ _#})")
translations
"{#x ∈#⇩z M. P#}" == "CONST filter_zmset (λx. P) M"

lemma count_filter_zmset[simp]:
"zcount (filter_zmset P M) a = (if P a then zcount M a else 0)"
by transfer auto

lemma filter_empty_zmset[simp]: "filter_zmset P {#}⇩z = {#}⇩z"
by (rule zmultiset_eqI) simp

lemma filter_single_zmset: "filter_zmset P {#x#}⇩z = (if P x then {#x#}⇩z else {#}⇩z)"
by (rule zmultiset_eqI) simp

lemma filter_union_zmset[simp]: "filter_zmset P (M + N) = filter_zmset P M + filter_zmset P N"
by (rule zmultiset_eqI) simp

lemma filter_diff_zmset[simp]: "filter_zmset P (M - N) = filter_zmset P M - filter_zmset P N"
by (rule zmultiset_eqI) simp

"filter_zmset P (add_zmset x A) =
(if P x then add_zmset x (filter_zmset P A) else filter_zmset P A)"
by (auto simp: zmultiset_eq_iff)

lemma zmultiset_filter_mono:
assumes "A ⊆#⇩z B"
shows "filter_zmset f A ⊆#⇩z filter_zmset f B"
using assms by (simp add: subseteq_zmset_def)

lemma filter_filter_zmset: "filter_zmset P (filter_zmset Q M) = {#x ∈#⇩z M. Q x ∧ P x#}"
by (auto simp: zmultiset_eq_iff)

lemma
filter_zmset_True[simp]: "{#y ∈#⇩z M. True#} = M" and
filter_zmset_False[simp]: "{#y ∈#⇩z M. False#} = {#}⇩z"
by (auto simp: zmultiset_eq_iff)

subsection ‹Uncategorized›

lemma multi_drop_mem_not_eq_zmset: "B - {#c#}⇩z ≠ B"

lemma zmultiset_partition: "M = {#x ∈#⇩z M. P x #} + {#x ∈#⇩z M. ¬ P x#}"
by (subst zmultiset_eq_iff) auto

subsection ‹Image›

definition image_zmset :: "('a ⇒ 'b) ⇒ 'a zmultiset ⇒ 'b zmultiset" where
"image_zmset f M =
zmset_of (fold_mset (add_mset ∘ f) {#} (mset_pos M)) -
zmset_of (fold_mset (add_mset ∘ f) {#} (mset_neg M))"

subsection ‹Multiset Order›

instantiation zmultiset :: (preorder) order
begin

lift_definition less_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" is
"λ(Mp, Mn) (Np, Nn). Mp + Nn < Mn + Np"
proof (clarsimp simp: equiv_zmset_def)
fix A1 B2 B1 A2 C1 D2 D1 C2 :: "'a multiset"
assume
ab: "A1 + A2 = B1 + B2" and
cd: "C1 + C2 = D1 + D2"

have "A1 + D2 < B2 + C1 ⟷ A1 + A2 + D2 < A2 + B2 + C1"
by simp
also have "… ⟷ B1 + B2 + D2 < A2 + B2 + C1"
unfolding ab by (rule refl)
also have "… ⟷ B1 + D2 < A2 + C1"
by simp
also have "… ⟷ B1 + D1 + D2 < A2 + C1 + D1"
by simp
also have "… ⟷ B1 + C1 + C2 < A2 + C1 + D1"
also have "… ⟷ B1 + C2 < A2 + D1"
by simp
finally show "A1 + D2 < B2 + C1 ⟷ B1 + C2 < A2 + D1"
by assumption
qed

definition less_eq_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ bool" where
"less_eq_zmultiset M' M ⟷ M' < M ∨ M' = M"

instance
proof ((intro_classes; unfold less_eq_zmultiset_def; transfer),
auto simp: equiv_zmset_def union_commute)
fix A1 B1 D C B2 A2 :: "'a multiset"
assume ab: "A1 + A2 ≠ B1 + B2"

{
assume ab1: "A1 + C < B1 + D"

{
assume ab2: "D + A2 < C + B2"
show "A1 + A2 < B1 + B2"
proof -
have f1: "⋀m. D + A2 + m < C + B2 + m"
have "⋀m. C + (A1 + m) < D + (B1 + m)"
then have "D + (A2 + A1) < D + (B1 + B2)"
then show ?thesis
qed
}
{
assume ab2: "D + A2 = C + B2"
show "A1 + A2 < B1 + B2"
proof -
have "⋀m. C + A1 + m < D + B1 + m"
then have "D + (A2 + A1) < D + (B1 + B2)"
then show ?thesis
qed
}
}

{
assume ab1: "A1 + C = B1 + D"

{
assume ab2: "D + A2 < C + B2"
show "A1 + A2 < B1 + B2"
proof -
have "A1 + (D + A2) < B1 + (D + B2)"
then show ?thesis
by simp
qed
}
{
assume ab2: "D + A2 = C + B2"
have False
thus "A1 + A2 < B1 + B2"
by sat
}
}
qed

end

by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def)

by (intro_classes; transfer; auto simp: equiv_zmset_def)

instantiation zmultiset :: (linorder) distrib_lattice
begin

definition inf_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ 'a zmultiset" where
"inf_zmultiset A B = (if A < B then A else B)"

definition sup_zmultiset :: "'a zmultiset ⇒ 'a zmultiset ⇒ 'a zmultiset" where
"sup_zmultiset A B = (if B > A then B else A)"

lemma not_lt_iff_ge_zmset: "¬ x < y ⟷ x ≥ y" for x y :: "'a zmultiset"
by (unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def algebra_simps)

instance
by intro_classes (auto simp: less_eq_zmultiset_def inf_zmultiset_def sup_zmultiset_def
dest!: not_lt_iff_ge_zmset[THEN iffD1])

end

lemma zmset_of_less: "zmset_of M < zmset_of N ⟷ M < N"
by (clarsimp simp: zmset_of_def, transfer, simp)+

lemma zmset_of_le: "zmset_of M ≤ zmset_of N ⟷ M ≤ N"
by (simp_all add: less_eq_zmultiset_def zmset_of_def; transfer; auto simp: equiv_zmset_def)

by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def)

lemma uminus_add_conv_diff_mset[cancelation_simproc_pre]: ‹-a + b = b - a› for a :: ‹'a zmultiset›

lemma uminus_add_add_uminus[cancelation_simproc_pre]: ‹b -a + c = b + c - a› for a :: ‹'a zmultiset›

‹NO_MATCH {#}⇩z H ⟹ add_zmset a H = {#a#}⇩z + H›
by auto

unfolding iterate_add_def by (induction n) auto

simproc_setup zmseteq_cancel_numerals
("(l::'a zmultiset) + m = n" | "(l::'a zmultiset) = m + n" |
"add_zmset a m = n" | "m = add_zmset a n" |
"replicate_zmset p a = n" | "m = replicate_zmset p a" |
"repeat_zmset p m = n" | "m = repeat_zmset p m") =
‹fn phi => Cancel_Simprocs.eq_cancel›

‹j ≤ i ⟹ (repeat_zmset i u + m ⊆#⇩z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m ⊆#⇩z n)›

‹i ≤ j ⟹ (repeat_zmset i u + m ⊆#⇩z repeat_zmset j u + n) = (m ⊆#⇩z repeat_zmset (j - i) u + n)›
proof -
assume "i ≤ j"
then have "⋀z. repeat_zmset j (z::'a zmultiset) - repeat_zmset i z = repeat_zmset (j - i) z"
then show ?thesis
qed

‹j ≤ i ⟹ (repeat_zmset i u + m ⊂#⇩z repeat_zmset j u + n) = (repeat_zmset (i - j) u + m ⊂#⇩z n)›

‹i ≤ j ⟹ (repeat_zmset i u + m ⊂#⇩z repeat_zmset j u + n) = (m ⊂#⇩z repeat_zmset (j - i) u + n)›

ML_file ‹zmultiset_simprocs.ML›

simproc_setup zmsetsubset_cancel
("(l::'a zmultiset) + m ⊂#⇩z n" | "(l::'a zmultiset) ⊂#⇩z m + n" |
"add_zmset a m ⊂#⇩z n" | "m ⊂#⇩z add_zmset a n" |
"replicate_zmset p a ⊂#⇩z n" | "m ⊂#⇩z replicate_zmset p a" |
"repeat_zmset p m ⊂#⇩z n" | "m ⊂#⇩z repeat_zmset p m") =
‹fn phi => ZMultiset_Simprocs.subset_cancel_zmsets›

simproc_setup zmsetsubseteq_cancel
("(l::'a zmultiset) + m ⊆#⇩z n" | "(l::'a zmultiset) ⊆#⇩z m + n" |
"add_zmset a m ⊆#⇩z n" | "m ⊆#⇩z add_zmset a n" |
"replicate_zmset p a ⊆#⇩z n" | "m ⊆#⇩z replicate_zmset p a" |
"repeat_zmset p m ⊆#⇩z n" | "m ⊆#⇩z repeat_zmset p m") =
‹fn phi => ZMultiset_Simprocs.subseteq_cancel_zmsets›

by (intro_classes; unfold less_eq_zmultiset_def; transfer; auto)

simproc_setup zmsetless_cancel
("(l::'a::preorder zmultiset) + m < n" | "(l::'a zmultiset) < m + n" |
"add_zmset a m < n" | "m < add_zmset a n" |
"replicate_zmset p a < n" | "m < replicate_zmset p a" |
"repeat_zmset p m < n" | "m < repeat_zmset p m") =
‹fn phi => Cancel_Simprocs.less_cancel›

simproc_setup zmsetless_eq_cancel
("(l::'a::preorder zmultiset) + m ≤ n" | "(l::'a zmultiset) ≤ m + n" |
"add_zmset a m ≤ n" | "m ≤ add_zmset a n" |
"replicate_zmset p a ≤ n" | "m ≤ replicate_zmset p a" |
"repeat_zmset p m ≤ n" | "m ≤ repeat_zmset p m") =
‹fn phi => Cancel_Simprocs.less_eq_cancel›

simproc_setup zmsetdiff_cancel
("n + (l::'a zmultiset)" | "(l::'a zmultiset) - m" |
"add_zmset a m - n" | "m - add_zmset a n" |
"replicate_zmset p r - n" | "m - replicate_zmset p r" |
"repeat_zmset p m - n" | "m - repeat_zmset p m") =
‹fn phi => Cancel_Simprocs.diff_cancel›

by (intro_classes, unfold less_eq_zmultiset_def, transfer, auto simp: equiv_zmset_def add.commute)

lemma less_mset_zmsetE:
assumes "M < N"
obtains A B C where
"M = zmset_of A + C" and "N = zmset_of B + C" and "A < B"
by (metis add_less_imp_less_right assms decompose_zmset_of2 zmset_of_less)

lemma less_eq_mset_zmsetE:
assumes "M ≤ N"
obtains A B C where
"M = zmset_of A + C" and "N = zmset_of B + C" and "A ≤ B"
zmset_of_empty)

lemma subset_eq_imp_le_zmset: "M ⊆#⇩z N ⟹ M ≤ N"
subseteq_mset_zmsetE zmset_of_le)

lemma subset_imp_less_zmset: "M ⊂#⇩z N ⟹ M < N"
by (metis le_neq_trans subset_eq_imp_le_zmset subset_zmset_def)

lemma lt_imp_ex_zcount_lt:
assumes m_lt_n: "M < N"
shows "∃y. zcount M y < zcount N y"
proof (rule ccontr, clarsimp)
assume "∀y. ¬ zcount M y < zcount N y"
hence "∀y. zcount M y ≥ zcount N y"
hence "M ⊇#⇩z N"
hence "M ≥ N"
thus False
using m_lt_n by simp
qed

instance zmultiset :: (preorder) no_top
proof
fix M :: ‹'a zmultiset›
obtain a :: 'a where True by fast
let ?M = ‹zmset_of (mset_pos M) + zmset_of (mset_neg M)›
have ‹M < add_zmset a ?M + ?M›
by (subst mset_pos_neg_partition)
(auto simp: subset_zmset_def subseteq_zmset_def zmultiset_eq_iff
intro!: subset_imp_less_zmset)
then show ‹∃N. M < N›
by blast
qed

end


# File ‹zmultiset_simprocs.ML›

(*  Title:       \$AFP/Nested_Multisets_Ordinals/zmultiset_simprocs.ML
Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2017

Simprocs for zmultisets, based on Larry Paulson's simprocs for natural numbers
and numerals.
*)

signature ZMULTISET_SIMPROCS =
sig
val subset_cancel_zmsets: Proof.context -> cterm -> thm option
val subseteq_cancel_zmsets: Proof.context -> cterm -> thm option
end;

structure ZMultiset_Simprocs : ZMULTISET_SIMPROCS =
struct

structure Subset_Cancel_Multiset = Cancel_Fun
(open Cancel_Data
val mk_bal   = HOLogic.mk_binrel @{const_name subset_zmset}
val dest_bal = HOLogic.dest_bin @{const_name subset_zmset} dummyT
);

structure Subseteq_Cancel_Multiset = Cancel_Fun
(open Cancel_Data
val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_zmset}
val dest_bal = HOLogic.dest_bin @{const_name subseteq_zmset} dummyT
);

val subset_cancel_zmsets = Subset_Cancel_Multiset.proc;
val subseteq_cancel_zmsets = Subseteq_Cancel_Multiset.proc;

end


# Theory Nested_Multiset

(*  Title:       Nested Multisets
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Nested Multisets›

theory Nested_Multiset
imports "HOL-Library.Multiset_Order"
begin

declare multiset.map_comp [simp]
declare multiset.map_cong [cong]

subsection ‹Type Definition›

datatype 'a nmultiset =
Elem 'a
| MSet "'a nmultiset multiset"

inductive no_elem :: "'a nmultiset ⇒ bool" where
"(⋀X. X ∈# M ⟹ no_elem X) ⟹ no_elem (MSet M)"

inductive_set sub_nmset :: "('a nmultiset × 'a nmultiset) set" where
"X ∈# M ⟹ (X, MSet M) ∈ sub_nmset"

lemma wf_sub_nmset[simp]: "wf sub_nmset"
proof (rule wfUNIVI)
fix P :: "'a nmultiset ⇒ bool" and M :: "'a nmultiset"
assume IH: "∀M. (∀N. (N, M) ∈ sub_nmset ⟶ P N) ⟶ P M"
show "P M"
by (induct M; rule IH[rule_format]) (auto simp: sub_nmset.simps)
qed

primrec depth_nmset :: "'a nmultiset ⇒ nat" ("|_|") where
"|Elem a| = 0"
| "|MSet M| = (let X = set_mset (image_mset depth_nmset M) in if X = {} then 0 else Suc (Max X))"

lemma depth_nmset_MSet: "x ∈# M ⟹ |x| < |MSet M|"
by (auto simp: less_Suc_eq_le)

declare depth_nmset.simps(2)[simp del]

subsection ‹Dershowitz and Manna's Nested Multiset Order›

text ‹The Dershowitz--Manna extension:›

definition less_multiset_ext⇩D⇩M :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"less_multiset_ext⇩D⇩M R M N ⟷
(∃X Y. X ≠ {#} ∧ X ⊆# N ∧ M = (N - X) + Y ∧ (∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ R k a)))"

lemma less_multiset_ext⇩D⇩M_imp_mult:
assumes
N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and less: "less_multiset_ext⇩D⇩M R M N"
shows "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
proof -
from less obtain X Y where
"X ≠ {#}" and "X ⊆# N" and "M = N - X + Y" and "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ R k a)"
unfolding less_multiset_ext⇩D⇩M_def by blast
with N_A M_A have "(N - X + Y, N - X + X) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
by (intro one_step_implies_mult, blast,
metis (mono_tags, lifting) case_prodI mem_Collect_eq mset_subset_eqD mset_subset_eq_add_right
subsetCE)
with ‹M = N - X + Y› ‹X ⊆# N› show "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
qed

lemma mult_imp_less_multiset_ext⇩D⇩M:
assumes
N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and
trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. R x y ⟶ R y z ⟶ R x z" and
in_mult: "(M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
shows "less_multiset_ext⇩D⇩M R M N"
using in_mult N_A M_A unfolding mult_def less_multiset_ext⇩D⇩M_def
proof induct
case (base N)
then obtain y M0 X where "N = add_mset y M0" and "M = M0 + X" and "∀a. a ∈# X ⟶ R a y"
unfolding mult1_def by auto
thus ?case
by (auto intro: exI[of _ "{#y#}"])
next
case (step N N')
note N_N'_in_mult1 = this(2) and ih = this(3) and N'_A = this(4) and M_A = this(5)

have N_A: "set_mset N ⊆ A"
using N_N'_in_mult1 N'_A unfolding mult1_def by auto

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 ∧ R x y)"
using ih[OF N_A M_A] by blast

obtain z M0 Ya where N'_eq: "N' = M0 + {#z#}" and N_eq: "N = M0 + Ya" and
z_gt: "∀y. y ∈# Ya ⟶ y ∈ A ∧ z ∈ A ∧ R y z"
using N_N'_in_mult1[unfolded mult1_def] by auto

let ?Za = "Y - Ya + {#z#}"
let ?Xa = "X + Ya + (Y - Ya) - Y"

have xa_sub_x_ya: "set_mset ?Xa ⊆ set_mset (X + Ya)"
by (metis diff_subset_eq_self in_diffD subsetI subset_mset.diff_diff_right)

have x_A: "set_mset X ⊆ A"
using M_A M_eq by auto
have ya_A: "set_mset Ya ⊆ A"

have ex_y': "∃y. y ∈# Y - Ya + {#z#} ∧ R x y" if x_in: "x ∈# X + Ya" for x
proof (cases "x ∈# X")
case True
then obtain y where y_in: "y ∈# Y" and y_gt_x: "R x y"
using ex_y by blast
show ?thesis
proof (cases "y ∈# Ya")
case False
hence "y ∈# Y - Ya + {#z#}"
using y_in count_greater_zero_iff in_diff_count by fastforce
thus ?thesis
using y_gt_x by blast
next
case True
hence "y ∈ A" and "z ∈ A" and "R y z"
using z_gt by blast+
hence "R x z"
using trans y_gt_x x_A ya_A x_in by (meson subsetCE union_iff)
thus ?thesis
by auto
qed
next
case False
hence "x ∈# Ya"
using x_in by auto
hence "x ∈ A" and "z ∈ A" and "R x z"
using z_gt by blast+
thus ?thesis
by auto
qed

show ?case
proof (rule exI[of _ ?Za], rule exI[of _ ?Xa], intro conjI)
show "Y - Ya + {#z#} ⊆# N'"
using mset_subset_eq_mono_add subset_eq_diff_conv y_sub_N N_eq N'_eq
next
show "M = N' - (Y - Ya + {#z#}) + (X + Ya + (Y - Ya) - Y)"
unfolding M_eq N_eq N'_eq by (auto simp: multiset_eq_iff)
next
show "∀x. x ∈# X + Ya + (Y - Ya) - Y ⟶ (∃y. y ∈# Y - Ya + {#z#} ∧ R x y)"
using ex_y' xa_sub_x_ya by blast
qed auto
qed

lemma less_multiset_ext⇩D⇩M_iff_mult:
assumes
N_A: "set_mset N ⊆ A" and M_A: "set_mset M ⊆ A" and
trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. R x y ⟶ R y z ⟶ R x z"
shows "less_multiset_ext⇩D⇩M R M N ⟷ (M, N) ∈ mult {(x, y). x ∈ A ∧ y ∈ A ∧ R x y}"
using mult_imp_less_multiset_ext⇩D⇩M[OF assms] less_multiset_ext⇩D⇩M_imp_mult[OF N_A M_A] by blast

instantiation nmultiset :: (preorder) preorder
begin

lemma less_multiset_ext⇩D⇩M_cong[fundef_cong]:
"(⋀X Y k a. X ≠ {#} ⟹ X ⊆# N ⟹ M = (N - X) + Y ⟹ k ∈# Y ⟹ R k a = S k a) ⟹
less_multiset_ext⇩D⇩M R M N = less_multiset_ext⇩D⇩M S M N"
unfolding less_multiset_ext⇩D⇩M_def by metis

function less_nmultiset :: "'a nmultiset ⇒ 'a nmultiset ⇒ bool" where
"less_nmultiset (Elem a) (Elem b) ⟷ a < b"
| "less_nmultiset (Elem a) (MSet M) ⟷ True"
| "less_nmultiset (MSet M) (Elem a) ⟷ False"
| "less_nmultiset (MSet M) (MSet N) ⟷ less_multiset_ext⇩D⇩M less_nmultiset M N"
by pat_completeness auto
termination
by (relation "sub_nmset <*lex*> sub_nmset", fastforce,

lemmas less_nmultiset_induct =
less_nmultiset.induct[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet]

lemmas less_nmultiset_cases =
less_nmultiset.cases[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet]

lemma trans_less_nmultiset: "X < Y ⟹ Y < Z ⟹ X < Z" for X Y Z :: "'a nmultiset"
proof (induct "Max {|X|, |Y|, |Z|}" arbitrary: X Y Z
rule: less_induct)
case less
from less(2,3) show ?case
proof (cases X; cases Y; cases Z)
fix M N N' :: "'a nmultiset multiset"
define A where "A = set_mset M ∪ set_mset N ∪ set_mset N'"
assume XYZ: "X = MSet M" "Y = MSet N" "Z = MSet N'"
then have trans: "∀x ∈ A. ∀y ∈ A. ∀z ∈ A. x < y ⟶ y < z ⟶ x < z"
by (auto elim!: less(1)[rotated -1] dest!: depth_nmset_MSet simp add: A_def)
have "set_mset M ⊆ A" "set_mset N ⊆ A" "set_mset N' ⊆ A"
unfolding A_def by auto
with less(2,3) XYZ show "X < Z"
by (auto simp: less_multiset_ext⇩D⇩M_iff_mult[OF _ _ trans] mult_def)
qed (auto elim: less_trans)
qed

lemma irrefl_less_nmultiset:
fixes X :: "'a nmultiset"
shows "X < X ⟹ False"
proof (induct X)
case (MSet M)
from MSet(2) show ?case
unfolding less_nmultiset.simps less_multiset_ext⇩D⇩M_def
proof safe
fix X Y :: "'a nmultiset multiset"
define XY where "XY = {(x, y). x ∈# X ∧ y ∈# Y ∧ y < x}"
then have fin: "finite XY" and trans: "trans XY"
by (auto simp: trans_def intro: trans_less_nmultiset
finite_subset[OF _ finite_cartesian_product])
assume "X ≠ {#}" "X ⊆# M" "M = M - X + Y"
then have "X = Y"
by (auto simp: mset_subset_eq_exists_conv)
with MSet(1) ‹X ⊆# M› have "irrefl XY"
unfolding XY_def by (force dest: mset_subset_eqD simp: irrefl_def)
with trans have "acyclic XY"
moreover
assume "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)"
with ‹X = Y› ‹X ≠ {#}› have "¬ acyclic XY"
by (intro notI, elim finite_acyclic_wf[OF fin, elim_format])
(auto dest!: spec[of _ "set_mset Y"] simp: wf_eq_minimal XY_def)
ultimately show False by blast
qed
qed simp

lemma antisym_less_nmultiset:
fixes X Y :: "'a nmultiset"
shows "X < Y ⟹ Y < X ⟹ False"
using trans_less_nmultiset irrefl_less_nmultiset by blast

definition less_eq_nmultiset :: "'a nmultiset ⇒ 'a nmultiset ⇒ bool" where
"less_eq_nmultiset X Y = (X < Y ∨ X = Y)"

instance
proof (intro_classes, goal_cases less_def refl trans)
case (less_def x y)
then show ?case
unfolding less_eq_nmultiset_def by (metis irrefl_less_nmultiset antisym_less_nmultiset)
next
case (refl x)
then show ?case
unfolding less_eq_nmultiset_def by blast
next
case (trans x y z)
then show ?case
unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset)
qed

lemma less_multiset_ext⇩D⇩M_less: "less_multiset_ext⇩D⇩M (<) = (<)"
unfolding fun_eq_iff less_multiset_ext⇩D⇩M_def less_multiset⇩D⇩M by blast

end

instantiation nmultiset :: (order) order
begin

instance
proof (intro_classes, goal_cases antisym)
case (antisym x y)
then show ?case
unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset irrefl_less_nmultiset)
qed

end

instantiation nmultiset :: (linorder) linorder
begin

lemma total_less_nmultiset:
fixes X Y :: "'a nmultiset"
shows "¬ X < Y ⟹ Y ≠ X ⟹ Y < X"
proof (induct X Y rule: less_nmultiset_induct)
case (MSet_MSet M N)
then show ?case
unfolding nmultiset.inject less_nmultiset.simps less_multiset_ext⇩D⇩M_less less_multiset⇩H⇩O
mset_subset_eq_multiset_union_diff_commute subset_mset.refl)
qed auto

instance
proof (intro_classes, goal_cases total)
case (total x y)
then show ?case
unfolding less_eq_nmultiset_def by (metis total_less_nmultiset)
qed

end

lemma less_depth_nmset_imp_less_nmultiset: "|X| < |Y| ⟹ X < Y"
proof (induct X Y rule: less_nmultiset_induct)
case (MSet_MSet M N)
then show ?case
proof (cases "M = {#}")
case False
with MSet_MSet show ?thesis
by (auto 0 4 simp: depth_nmset.simps(2) less_multiset_ext⇩D⇩M_def not_le Max_gr_iff
intro: exI[of _ N] split: if_splits)
qed (auto simp: depth_nmset.simps(2) less_multiset_ext⇩D⇩M_less split: if_splits)
qed simp_all

lemma less_nmultiset_imp_le_depth_nmset: "X < Y ⟹ |X| ≤ |Y|"
proof (induct X Y rule: less_nmultiset_induct)
case (MSet_MSet M N)
then have "M < N" by (simp add: less_multiset_ext⇩D⇩M_less)
then show ?case
proof (cases "M = {#}" "N = {#}" rule: bool.exhaust[case_product bool.exhaust])
case [simp]: False_False
show ?thesis
unfolding depth_nmset.simps(2) Let_def False_False Suc_le_mono set_image_mset image_is_empty
set_mset_eq_empty_iff if_False
proof (intro iffD2[OF Max_le_iff] ballI iffD2[OF Max_ge_iff]; (elim imageE)?; simp)
fix X
assume [simp]: "X ∈# M"
with MSet_MSet(1)[of N M X, simplified] ‹M < N› show "∃Y∈#N. |X| ≤ |Y|"
by (meson ex_gt_imp_less_multiset less_asym' less_depth_nmset_imp_less_nmultiset
not_le_imp_less)
qed
qed (auto simp: depth_nmset.simps(2))
qed simp_all

lemma eq_mlex_I:
fixes f :: "'a ⇒ nat" and R :: "'a ⇒ 'a ⇒ bool"
assumes "⋀X Y. f X < f Y ⟹ R X Y" and "antisymp R"
shows "{(X, Y). R X Y} = f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
proof safe
fix X Y
assume "R X Y"
show "(X, Y) ∈ f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
proof (cases "f X" "f Y" rule: linorder_cases)
case less
with ‹R X Y› show ?thesis
by (elim mlex_less)
next
case equal
with ‹R X Y› show ?thesis
by (intro mlex_leq) auto
next
case greater
from ‹R X Y› assms(1)[OF greater] ‹antisymp R› greater show ?thesis
unfolding antisymp_def by auto
qed
next
fix X Y
assume "(X, Y) ∈ f <*mlex*> {(X, Y). f X = f Y ∧ R X Y}"
then show "R X Y"
unfolding mlex_prod_def by (auto simp: assms(1))
qed

instantiation nmultiset :: (wellorder) wellorder
begin

lemma depth_nmset_eq_0[simp]: "|X| = 0 ⟷ (X = MSet {#} ∨ (∃x. X = Elem x))"
by (cases X; simp add: depth_nmset.simps(2))

lemma depth_nmset_eq_Suc[simp]: "|X| = Suc n ⟷
(∃N. X = MSet N ∧ (∃Y ∈# N. |Y| = n) ∧ (∀Y ∈# N. |Y| ≤ n))"
by (cases X; auto simp add: depth_nmset.simps(2) intro!: Max_eqI)
(metis (no_types, lifting) Max_in finite_imageI finite_set_mset imageE image_is_empty
set_mset_eq_empty_iff)

lemma wf_less_nmultiset_depth:
"wf {(X :: 'a nmultiset, Y). |X| = i ∧ |Y| = i ∧ X < Y}"
proof (induct i rule: less_induct)
case (less i)
define A :: "'a nmultiset set" where "A = {X. |X| < i}"
from less have "wf ((depth_nmset :: 'a nmultiset ⇒ nat) <*mlex*>
(⋃j < i. {(X, Y). |X| = j ∧ |Y| = j ∧ X < Y}))"
by (intro wf_UN wf_mlex) auto
then have *: "wf (mult {(X :: 'a nmultiset, Y). X ∈ A ∧ Y ∈ A ∧ X < Y})"
by (intro wf_mult, elim wf_subset) (force simp: A_def mlex_prod_def not_less_iff_gr_or_eq
dest!: less_depth_nmset_imp_less_nmultiset)
show ?case
proof (cases i)
case 0
then show ?thesis
by (auto simp: inj_on_def intro!: wf_subset[OF
wf_Un[OF wf_map_prod_image[OF wf, of Elem] wf_UN[of "Elem  UNIV" "λx. {(x, MSet {#})}"]]])
next
case (Suc n)
then show ?thesis
by (intro wf_subset[OF wf_map_prod_image[OF *, of MSet]])
(auto 0 4 simp: map_prod_def image_iff inj_on_def A_def
dest!: less_multiset_ext⇩D⇩M_imp_mult[of _ A, rotated -1] split: prod.splits)
qed
qed

lemma wf_less_nmultiset: "wf {(X :: 'a nmultiset, Y :: 'a nmultiset). X < Y}" (is "wf ?R")
proof -
have "?R = depth_nmset <*mlex*> {(X, Y). |X| = |Y| ∧ X < Y}"
by (rule eq_mlex_I) (auto simp: antisymp_def less_depth_nmset_imp_less_nmultiset)
also have "{(X, Y). |X| = |Y| ∧ X < Y} = (⋃i. {(X, Y). |X| = i ∧ |Y| = i ∧ X < Y})"
by auto
finally show ?thesis
by (fastforce intro: wf_mlex wf_Union wf_less_nmultiset_depth)
qed

instance using wf_less_nmultiset unfolding wf_def mem_Collect_eq prod.case by intro_classes metis

end

end


# Theory Hereditary_Multiset

(*  Title:       Hereditar(il)y (Finite) Multisets
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Hereditar(il)y (Finite) Multisets›

theory Hereditary_Multiset
imports Multiset_More Nested_Multiset
begin

subsection ‹Type Definition›

datatype hmultiset =
HMSet (hmsetmset: "hmultiset multiset")

lemma hmsetmset_inject[simp]: "hmsetmset A = hmsetmset B ⟷ A = B"
by (blast intro: hmultiset.expand)

primrec Rep_hmultiset :: "hmultiset ⇒ unit nmultiset" where
"Rep_hmultiset (HMSet M) = MSet (image_mset Rep_hmultiset M)"

primrec (nonexhaustive) Abs_hmultiset :: "unit nmultiset ⇒ hmultiset" where
"Abs_hmultiset (MSet M) = HMSet (image_mset Abs_hmultiset M)"

lemma type_definition_hmultiset: "type_definition Rep_hmultiset Abs_hmultiset {X. no_elem X}"
proof (unfold_locales, unfold mem_Collect_eq)
fix X
show "no_elem (Rep_hmultiset X)"
by (induct X) (auto intro!: no_elem.intros)
show "Abs_hmultiset (Rep_hmultiset X) = X"
by (induct X) auto
next
fix Y :: "unit nmultiset"
assume "no_elem Y"
thus "Rep_hmultiset (Abs_hmultiset Y) = Y"
by (induct Y rule: no_elem.induct) auto
qed

setup_lifting type_definition_hmultiset

lemma HMSet_alt: "HMSet = Abs_hmultiset o MSet o image_mset Rep_hmultiset"
by (auto simp: type_definition.Rep_inverse[OF type_definition_hmultiset])

lemma HMSet_transfer[transfer_rule]: "rel_fun (rel_mset pcr_hmultiset) pcr_hmultiset MSet HMSet"
unfolding HMSet_alt by (force simp: rel_fun_def multiset.in_rel nmultiset.rel_eq
pcr_hmultiset_def cr_hmultiset_def
type_definition.Rep_inverse[OF type_definition_hmultiset] intro!: multiset.map_cong)

subsection ‹Restriction of Dershowitz and Manna's Nested Multiset Order›

instantiation hmultiset :: linorder
begin

lift_definition less_hmultiset :: "hmultiset ⇒ hmultiset ⇒ bool" is "(<)" .
lift_definition less_eq_hmultiset :: "hmultiset ⇒ hmultiset ⇒ bool" is "(≤)" .

instance
by (intro_classes; transfer) auto

end

lemma less_HMSet_iff_less_multiset_ext⇩D⇩M: "HMSet M < HMSet N ⟷ less_multiset_ext⇩D⇩M (<) M N"
unfolding less_multiset_ext⇩D⇩M_def
proof (transfer, unfold less_nmultiset.simps less_multiset_ext⇩D⇩M_def, safe)
fix M N :: "unit nmultiset multiset" and X Y
assume *: "pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "X ≠ {#}"
"X ⊆# N" "∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k < a)"
then have "X ∈ Collect (pred_mset no_elem)"
unfolding multiset.pred_set mem_Collect_eq by (metis rev_subsetD set_mset_mono)
from *(1) have "Y ∈ Collect (pred_mset no_elem)"
unfolding multiset.pred_set mem_Collect_eq by (metis add_diff_cancel_left' in_diffD)
show
"∃X'∈Collect (pred_mset no_elem). ∃Y'∈Collect (pred_mset no_elem).
X' ≠ {#} ∧ filter_mset no_elem X' ⊆# filter_mset no_elem N ∧ N - X + Y = N - X' + Y' ∧
(∀k∈Collect no_elem. k ∈# Y' ⟶ (∃a∈Collect no_elem. a ∈# X' ∧ k < a))"
by (rule bexI[OF _ ‹X ∈ Collect (pred_mset no_elem)›],
rule bexI[OF _ ‹Y ∈ Collect (pred_mset no_elem)›])
(insert *; force simp: set_mset_diff multiset.pred_set multiset_filter_mono)
next
fix M N :: "unit nmultiset multiset" and X Y
assume *:
"pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "pred_mset no_elem X" "pred_mset no_elem Y"
"X ≠ {#}" "filter_mset no_elem X ⊆# filter_mset no_elem N"
"∀k∈Collect no_elem.  k ∈# Y ⟶ (∃a∈Collect no_elem. a ∈# X ∧ k < a)"
then have [simp]: "filter_mset no_elem X = X" "filter_mset no_elem N = N"
unfolding filter_mset_eq_conv by (auto simp: multiset.pred_set)
show
"∃X' Y'. X' ≠ {#} ∧ X' ⊆# N ∧  N - X + Y = N - X' + Y' ∧
(∀k. k ∈# Y' ⟶ (∃a. a ∈# X' ∧ k < a))"
by (rule exI[of _ X], rule exI[of _ Y]) (insert *; auto simp: multiset.pred_set)
qed

lemma hmsetmset_less[simp]: "hmsetmset M < hmsetmset N ⟷ M < N"
by (cases M, cases N, simp add: less_multiset_ext⇩D⇩M_less less_HMSet_iff_less_multiset_ext⇩D⇩M)

lemma hmsetmset_le[simp]: "hmsetmset M ≤ hmsetmset N ⟷ M ≤ N"
unfolding le_less hmsetmset_less by (metis hmultiset.collapse)

lemma wf_less_hmultiset: "wf {(X :: hmultiset, Y :: hmultiset). X < Y}"
unfolding wf_eq_minimal by transfer (insert wf_less_nmultiset[unfolded wf_eq_minimal], fast)

instance hmultiset :: wellorder
using wf_less_hmultiset unfolding wf_def mem_Collect_eq prod.case by intro_classes metis

lemma HMSet_less[simp]: "HMSet M < HMSet N ⟷ M < N"

lemma HMSet_le[simp]: "HMSet M ≤ HMSet N ⟷ M ≤ N"

lemma mem_imp_less_HMSet: "k ∈# L ⟹ k < HMSet L"
by (induct k arbitrary: L) (auto intro: ex_gt_imp_less_multiset)

lemma mem_hmsetmset_imp_less: "M ∈# hmsetmset N ⟹ M < N"
using mem_imp_less_HMSet by force

subsection ‹Disjoint Union and Truncated Difference›

begin

definition zero_hmultiset :: hmultiset where
"0 = HMSet {#}"

lemma hmsetmset_empty_iff[simp]: "hmsetmset n = {#} ⟷ n = 0"
unfolding zero_hmultiset_def by (cases n) simp

lemma hmsetmset_0[simp]: "hmsetmset 0 = {#}"
by simp

lemma
HMSet_eq_0_iff[simp]: "HMSet m = 0 ⟷ m = {#}" and
zero_eq_HMSet[simp]: "0 = HMSet m ⟷ m = {#}"
by (cases m) (auto simp: zero_hmultiset_def)

definition plus_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
"A + B = HMSet (hmsetmset A + hmsetmset B)"

definition minus_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
"A - B = HMSet (hmsetmset A - hmsetmset B)"

instance
by intro_classes (auto simp: zero_hmultiset_def plus_hmultiset_def minus_hmultiset_def)

end

lemma HMSet_plus: "HMSet (A + B) = HMSet A + HMSet B"

lemma HMSet_diff: "HMSet (A - B) = HMSet A - HMSet B"

lemma hmsetmset_plus: "hmsetmset (M + N) = hmsetmset M + hmsetmset N"

lemma hmsetmset_diff: "hmsetmset (M - N) = hmsetmset M - hmsetmset N"

lemma diff_diff_add_hmset[simp]: "a - b - c = a - (b + c)" for a b c :: hmultiset

instance hmultiset :: comm_monoid_diff
by intro_classes (auto simp: zero_hmultiset_def minus_hmultiset_def)

simproc_setup hmseteq_cancel
("(l::hmultiset) + m = n" | "(l::hmultiset) = m + n") =
‹fn phi => Cancel_Simprocs.eq_cancel›

simproc_setup hmsetdiff_cancel
("((l::hmultiset) + m) - n" | "(l::hmultiset) - (m + n)") =
‹fn phi => Cancel_Simprocs.diff_cancel›

simproc_setup hmsetless_cancel
("(l::hmultiset) + m < n" | "(l::hmultiset) < m + n") =
‹fn phi => Cancel_Simprocs.less_cancel›

simproc_setup hmsetless_eq_cancel
("(l::hmultiset) + m ≤ n" | "(l::hmultiset) ≤ m + n") =
‹fn phi => Cancel_Simprocs.less_eq_cancel›

by intro_classes (simp del: hmsetmset_less add: plus_hmultiset_def order_le_less
hmsetmset_less[symmetric] less_multiset_ext⇩D⇩M_less)

by intro_classes (simp add: plus_hmultiset_def order_le_less less_multiset_ext⇩D⇩M_less)

instantiation hmultiset :: order_bot
begin

definition bot_hmultiset :: hmultiset where
"bot_hmultiset = 0"

instance
proof (intro_classes, unfold bot_hmultiset_def zero_hmultiset_def, transfer, goal_cases bot_least)
case (bot_least x)
thus ?case
by (induct x rule: no_elem.induct) (auto simp: less_eq_nmultiset_def less_multiset_ext⇩D⇩M_less)
qed

end

instance hmultiset :: no_top
proof (intro_classes, goal_cases gt_ex)
case (gt_ex a)
have "a < a + HMSet {#0#}"
thus ?case
by (rule exI)
qed

lemma le_minus_plus_same_hmset: "m ≤ m - n + n" for m n :: hmultiset
proof (cases m n rule: hmultiset.exhaust[case_product hmultiset.exhaust])
case (HMSet_HMSet m0 n0)
note m = this(1) and n = this(2)

{
assume "n0 ⊆# m0"
hence "m0 = m0 - n0 + n0"
by simp
}
moreover
{
assume "¬ n0 ⊆# m0"
hence "m0 ⊂# m0 - n0 + n0"
subset_mset_def)
hence "m0 < m0 - n0 + n0"
by (rule subset_imp_less_mset)
}
ultimately show ?thesis
by (simp (no_asm) add: m n order_le_less plus_hmultiset_def minus_hmultiset_def) blast
qed

subsection ‹Infimum and Supremum›

instantiation hmultiset :: distrib_lattice
begin

definition inf_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
"inf_hmultiset A B = (if A < B then A else B)"

definition sup_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset" where
"sup_hmultiset A B = (if B > A then B else A)"

instance
by intro_classes (auto simp: inf_hmultiset_def sup_hmultiset_def)

end

subsection ‹Inequalities›

lemma zero_le_hmset[simp]: "0 ≤ M" for M :: hmultiset
by (simp add: order_le_less) (metis hmsetmset_less le_multiset_empty_left hmsetmset_empty_iff)

lemma
le_add1_hmset: "n ≤ n + m" and
le_add2_hmset: "n ≤ m + n" for n :: hmultiset
by simp+

lemma le_zero_eq_hmset[simp]: "M ≤ 0 ⟷ M = 0" for M :: hmultiset

lemma not_less_zero_hmset[simp]: "¬ M < 0" for M :: hmultiset
using not_le zero_le_hmset by blast

lemma not_gr_zero_hmset[simp]: "¬ 0 < M ⟷ M = 0" for M :: hmultiset
using neqE not_less_zero_hmset by blast

lemma zero_less_iff_neq_zero_hmset: "0 < M ⟷ M ≠ 0" for M :: hmultiset
using not_gr_zero_hmset by blast

lemma zero_less_HMSet_iff[simp]: "0 < HMSet M ⟷ M ≠ {#}"
by (simp only: zero_less_iff_neq_zero_hmset HMSet_eq_0_iff)

lemma gr_zeroI_hmset: "(M = 0 ⟹ False) ⟹ 0 < M" for M :: hmultiset
using not_gr_zero_hmset by blast

lemma gr_implies_not_zero_hmset: "M < N ⟹ N ≠ 0" for M N :: hmultiset
by auto

lemma add_eq_0_iff_both_eq_0_hmset[simp]: "M + N = 0 ⟷ M = 0 ∧ N = 0" for M N :: hmultiset

lemma trans_less_add1_hmset: "i < j ⟹ i < j + m" for i j m :: hmultiset
by (metis add_increasing2 leD le_less not_gr_zero_hmset)

lemma trans_less_add2_hmset: "i < j ⟹ i < m + j" for i j m :: hmultiset

lemma trans_le_add1_hmset: "i ≤ j ⟹ i ≤ j + m" for i j m :: hmultiset

lemma trans_le_add2_hmset: "i ≤ j ⟹ i ≤ m + j" for i j m :: hmultiset

lemma diff_le_self_hmset: "m - n ≤ m" for m n :: hmultiset
le_minus_plus_same_hmset)

end


# Theory Signed_Hereditary_Multiset

(*  Title:       Signed Hereditar(il)y (Finite) Multisets
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Signed Hereditar(il)y (Finite) Multisets›

theory Signed_Hereditary_Multiset
imports Signed_Multiset Hereditary_Multiset
begin

subsection ‹Type Definition›

typedef zhmultiset = "UNIV :: hmultiset zmultiset set"
morphisms zhmsetmset ZHMSet
by simp

lemmas ZHMSet_inverse[simp] = ZHMSet_inverse[OF UNIV_I]
lemmas ZHMSet_inject[simp] = ZHMSet_inject[OF UNIV_I UNIV_I]

declare
zhmsetmset_inverse [simp]
zhmsetmset_inject [simp]

setup_lifting type_definition_zhmultiset

subsection ‹Multiset Order›

instantiation zhmultiset :: linorder
begin

lift_definition less_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ bool" is "(<)" .
lift_definition less_eq_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ bool" is "(≤)" .

instance
by (intro_classes; transfer) auto

end

lemmas ZHMSet_less[simp] = less_zhmultiset.abs_eq
lemmas ZHMSet_le[simp] = less_eq_zhmultiset.abs_eq
lemmas zhmsetmset_less[simp] = less_zhmultiset.rep_eq[symmetric]
lemmas zhmsetmset_le[simp] = less_eq_zhmultiset.rep_eq[symmetric]

subsection ‹Embedding and Projections of Syntactic Ordinals›

abbreviation zhmset_of :: "hmultiset ⇒ zhmultiset" where
"zhmset_of M ≡ ZHMSet (zmset_of (hmsetmset M))"

lemma zhmset_of_inject[simp]: "zhmset_of M = zhmset_of N ⟷ M = N"
by simp

lemma zhmset_of_less: "zhmset_of M < zhmset_of N ⟷ M < N"

lemma zhmset_of_le: "zhmset_of M ≤ zhmset_of N ⟷ M ≤ N"

abbreviation hmset_pos :: "zhmultiset ⇒ hmultiset" where
"hmset_pos M ≡ HMSet (mset_pos (zhmsetmset M))"

abbreviation hmset_neg :: "zhmultiset ⇒ hmultiset" where
"hmset_neg M ≡ HMSet (mset_neg (zhmsetmset M))"

subsection ‹Disjoint Union and Difference›

begin

lift_definition zero_zhmultiset :: zhmultiset is "{#}⇩z" .

lift_definition plus_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" is
"λA B. A + B" .

lift_definition minus_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" is
"λA B. A - B" .

lemmas ZHMSet_plus = plus_zhmultiset.abs_eq[symmetric]
lemmas ZHMSet_diff = minus_zhmultiset.abs_eq[symmetric]
lemmas zhmsetmset_plus = plus_zhmultiset.rep_eq
lemmas zhmsetmset_diff = minus_zhmultiset.rep_eq

lemma zhmset_of_plus: "zhmset_of (A + B) = zhmset_of A + zhmset_of B"
by (simp add: hmsetmset_plus ZHMSet_plus zmset_of_plus)

lemma hmsetmset_0: "hmsetmset 0 = {#}"
by (fact hmsetmset_0)

instance
by (intro_classes; transfer) (auto intro: mult.assoc add.commute)

end

lemma zhmset_of_0: "zhmset_of 0 = 0"

lemma hmset_pos_plus:
"hmset_pos (A + B) = (hmset_pos A - hmset_neg B) + (hmset_pos B - hmset_neg A)"
by (simp add: HMSet_diff HMSet_plus zhmsetmset_plus)

lemma hmset_neg_plus:
"hmset_neg (A + B) = (hmset_neg A - hmset_pos B) + (hmset_neg B - hmset_pos A)"
by (simp add: HMSet_diff HMSet_plus zhmsetmset_plus)

lemma zhmset_pos_neg_partition: "M = zhmset_of (hmset_pos M) - zhmset_of (hmset_neg M)"
by (cases M, simp add: ZHMSet_diff[symmetric], rule mset_pos_neg_partition)

lemma zhmset_pos_as_neg: "zhmset_of (hmset_pos M) = zhmset_of (hmset_neg M) + M"
using mset_pos_as_neg zhmsetmset_plus zhmsetmset_inject by fastforce

lemma zhmset_neg_as_pos: "zhmset_of (hmset_neg M) = zhmset_of (hmset_pos M) - M"
using zhmsetmset_diff mset_neg_as_pos zhmsetmset_inject by fastforce

lemma hmset_pos_neg_dual:
"hmset_pos a + hmset_pos b + (hmset_neg a - hmset_pos b) + (hmset_neg b - hmset_pos a) =
hmset_neg a + hmset_neg b + (hmset_pos a - hmset_neg b) + (hmset_pos b - hmset_neg a)"
by (simp add: HMSet_plus[symmetric] HMSet_diff[symmetric]) (rule mset_pos_neg_dual)

lemma zhmset_of_sum_list: "zhmset_of (sum_list Ms) = sum_list (map zhmset_of Ms)"
by (induct Ms) (auto simp: zero_zhmultiset_def zhmset_of_plus)

lemma less_hmset_zhmsetE:
assumes m_lt_n: "M < N"
obtains A B C where "M = zhmset_of A + C" and "N = zhmset_of B + C" and "A < B"
by (rule less_mset_zmsetE[OF m_lt_n[folded zhmsetmset_less]])
(metis hmsetmset_less hmultiset.sel ZHMSet_plus zhmsetmset_inverse)

lemma less_eq_hmset_zhmsetE:
assumes m_le_n: "M ≤ N"
obtains A B C where "M = zhmset_of A + C" and "N = zhmset_of B + C" and "A ≤ B"
by (rule less_eq_mset_zmsetE[OF m_le_n[folded zhmsetmset_le]])
(metis hmsetmset_le hmultiset.sel ZHMSet_plus zhmsetmset_inverse)

begin

lift_definition uminus_zhmultiset :: "zhmultiset ⇒ zhmultiset" is "λA. - A" .

lemmas ZHMSet_uminus = uminus_zhmultiset.abs_eq[symmetric]
lemmas zhmsetmset_uminus = uminus_zhmultiset.rep_eq

instance
by (intro_classes; transfer; simp)

end

subsection ‹Infimum and Supremum›

by (intro_classes; transfer) (auto simp: add_left_mono)

by (intro_classes; transfer; simp)

instantiation zhmultiset :: distrib_lattice
begin

definition inf_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" where
"inf_zhmultiset A B = (if A < B then A else B)"

definition sup_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" where
"sup_zhmultiset A B = (if B > A then B else A)"

instance
by intro_classes (auto simp: inf_zhmultiset_def sup_zhmultiset_def)

end

end


# Theory Syntactic_Ordinal

(*  Title:       Syntactic Ordinals in Cantor Normal Form
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Author:      Mathias Fleury <mfleury at mpi-inf.mpg.de>, 2016
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Syntactic Ordinals in Cantor Normal Form›

theory Syntactic_Ordinal
imports Hereditary_Multiset "HOL-Library.Product_Order" "HOL-Library.Extended_Nat"
begin

subsection ‹Natural (Hessenberg) Product›

instantiation hmultiset :: comm_semiring_1
begin

abbreviation ω_exp :: "hmultiset ⇒ hmultiset" ("ω^") where
"ω^ ≡ λm. HMSet {#m#}"

definition one_hmultiset :: hmultiset where
"1 = ω^0"

abbreviation ω :: hmultiset where
"ω ≡ ω^1"

definition times_hmultiset :: "hmultiset ⇒ hmultiset ⇒ hmultiset"  where
"A * B = HMSet (image_mset (case_prod (+)) (hmsetmset A ×# hmsetmset B))"

lemma hmsetmset_times:
"hmsetmset (m * n) = image_mset (case_prod (+)) (hmsetmset m ×# hmsetmset n)"
unfolding times_hmultiset_def by simp

instance
proof (intro_classes, goal_cases assoc comm one distrib_plus zeroL zeroR zero_one)
case (assoc a b c)
thus ?case
by (auto simp: times_hmultiset_def Times_mset_image_mset1 Times_mset_image_mset2
Times_mset_assoc ac_simps intro: multiset.map_cong)
next
case (comm a b)
thus ?case
unfolding times_hmultiset_def
by (subst product_swap_mset[symmetric]) (auto simp: ac_simps intro: multiset.map_cong)
next
case (one a)
thus ?case
by (auto simp: one_hmultiset_def times_hmultiset_def Times_mset_single_left)
next
case (distrib_plus a b c)
thus ?case
by (auto simp: plus_hmultiset_def times_hmultiset_def)
next
case (zeroL a)
thus ?case
by (auto simp: times_hmultiset_def)
next
case (zeroR a)
thus ?case
by (auto simp: times_hmultiset_def)
next
case zero_one
thus ?case
by (auto simp: one_hmultiset_def)
qed

end

lemma empty_times_left_hmset[simp]: "HMSet {#} * M = 0"

lemma empty_times_right_hmset[simp]: "M * HMSet {#} = 0"
by (metis mult_zero_right zero_hmultiset_def)

lemma singleton_times_left_hmset[simp]: "ω^M * N = HMSet (image_mset ((+) M) (hmsetmset N))"

lemma singleton_times_right_hmset[simp]: "N * ω^M = HMSet (image_mset ((+) M) (hmsetmset N))"
by (metis mult.commute singleton_times_left_hmset)

subsection ‹Inequalities›

definition plus_nmultiset :: "unit nmultiset ⇒ unit nmultiset ⇒ unit nmultiset"  where
"plus_nmultiset X Y = Rep_hmultiset (Abs_hmultiset X + Abs_hmultiset Y)"

lemma plus_nmultiset_mono:
assumes less: "(X, Y) < (X', Y')" and no_elem: "no_elem X" "no_elem Y" "no_elem X'" "no_elem Y'"
shows "plus_nmultiset X Y < plus_nmultiset X' Y'"
using less[unfolded less_le_not_le] no_elem
by (auto simp: plus_nmultiset_def plus_hmultiset_def less_multiset_ext⇩D⇩M_less less_eq_nmultiset_def
union_less_mono type_definition.Abs_inverse[OF type_definition_hmultiset, simplified]
elim!: no_elem.cases)

lemma plus_hmultiset_transfer[transfer_rule]:
"(rel_fun pcr_hmultiset (rel_fun pcr_hmultiset pcr_hmultiset)) plus_nmultiset (+)"
unfolding rel_fun_def plus_nmultiset_def pcr_hmultiset_def nmultiset.rel_eq eq_OO cr_hmultiset_def
by (auto simp: type_definition.Rep_inverse[OF type_definition_hmultiset])

lemma Times_mset_monoL:
assumes less: "M < N" and Z_nemp: "Z ≠ {#}"
shows "M ×# Z < N ×# Z"
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

let ?X = "X ×# Z"
let ?Y = "Y ×# Z"

show ?thesis
unfolding less_multiset⇩D⇩M
proof (intro exI conjI)
show "M ×# Z = N ×# Z - ?Y + ?X"
unfolding M_eq by (auto simp: Sigma_mset_Diff_distrib1)
next
obtain y where y: "∀x. x ∈# X ⟶ y x ∈# Y ∧ x < y x"
using ex_Y by moura

show "∀x. x ∈# ?X ⟶ (∃y. y ∈# ?Y ∧ x < y)"
proof (intro allI impI)
fix x
assume "x ∈# ?X"
thus "∃y. y ∈# ?Y ∧ x < y"
using y by (intro exI[of _ "(y (fst x), snd x)"]) (auto simp: less_le_not_le)
qed
qed (auto simp: Z_nemp Y_nemp Y_sub_N Sigma_mset_mono)
qed

lemma times_hmultiset_monoL:
"a < b ⟹ 0 < c ⟹ a * c < b * c" for a b c :: hmultiset
by (cases a, cases b, cases c, hypsubst_thin,
unfold times_hmultiset_def zero_hmultiset_def hmultiset.sel, transfer,
auto simp: less_multiset_ext⇩D⇩M_less multiset.pred_set
intro!: image_mset_strict_mono Times_mset_monoL elim!: plus_nmultiset_mono)

instance hmultiset :: linordered_semiring_strict
by intro_classes (subst (1 2) mult.commute, (fact times_hmultiset_monoL)+)

lemma mult_le_mono1_hmset: "i ≤ j ⟹ i * k ≤ j * k" for i j k :: hmultiset

lemma mult_le_mono2_hmset: "i ≤ j ⟹ k * i ≤ k * j" for i j k :: hmultiset

lemma mult_le_mono_hmset: "i ≤ j ⟹ k ≤ l ⟹ i * k ≤ j * l" for i j k l :: hmultiset

lemma less_iff_add1_le_hmset: "m < n ⟷ m + 1 ≤ n" for m n :: hmultiset
proof (cases m n rule: hmultiset.exhaust[case_product hmultiset.exhaust])
case (HMSet_HMSet m0 n0)
note m = this(1) and n = this(2)

show ?thesis
proof (simp add: m n one_hmultiset_def plus_hmultiset_def order.order_iff_strict
less_multiset_ext⇩D⇩M_less, intro iffI)
assume m0_lt_n0: "m0 < n0"
note
m0_ne_n0 = m0_lt_n0[unfolded less_multiset⇩H⇩O, THEN conjunct1] and
ex_n0_gt_m0 = m0_lt_n0[unfolded less_multiset⇩H⇩O, THEN conjunct2, rule_format]

{
assume zero_m0_gt_n0: "add_mset 0 m0 > n0"
note
n0_ne_0m0 = zero_m0_gt_n0[unfolded less_multiset⇩H⇩O, THEN conjunct1] and
ex_0m0_gt_n0 = zero_m0_gt_n0[unfolded less_multiset⇩H⇩O, THEN conjunct2, rule_format]

{
fix y
assume m0y_lt_n0y: "count m0 y < count n0 y"

have "∃x > y. count n0 x < count m0 x"
proof (cases "count (add_mset 0 m0) y < count n0 y")
case True
then obtain aa where
aa_gt_y: "aa > y" and
count_n0aa_lt_count_0m0aa: "count n0 aa < count (add_mset 0 m0) aa"
using ex_0m0_gt_n0 by blast
have "aa ≠ 0"
by (rule gr_implies_not_zero_hmset[OF aa_gt_y])
hence "count (add_mset 0 m0) aa = count m0 aa"
by simp
thus ?thesis
using count_n0aa_lt_count_0m0aa aa_gt_y by auto
next
case not_0m0_y_lt_n0y: False
hence y_eq_0: "y = 0"
have sm0y_eq_n0y: "Suc (count m0 y) = count n0 y"
using m0y_lt_n0y not_0m0_y_lt_n0y count_add_mset[of 0 _ 0] unfolding y_eq_0 by simp

obtain bb where "count n0 bb < count (add_mset 0 m0) bb"
using lt_imp_ex_count_lt[OF zero_m0_gt_n0] by blast
hence n0bb_lt_m0bb: "count n0 bb < count m0 bb"
unfolding count_add_mset by (metis (full_types) less_irrefl_nat sm0y_eq_n0y y_eq_0)
hence "bb ≠ 0"
using sm0y_eq_n0y y_eq_0 by auto
thus ?thesis
unfolding y_eq_0 using n0bb_lt_m0bb not_gr_zero_hmset by blast
qed
}
hence "n0 < m0"
unfolding less_multiset⇩H⇩O using m0_ne_n0 by blast
hence False
using m0_lt_n0 by simp
}
thus "add_mset 0 m0 < n0 ∨ add_mset 0 m0 = n0"
using antisym_conv3 by blast
next
assume "add_mset 0 m0 < n0 ∨ add_mset 0 m0 = n0"
thus "m0 < n0"
using dual_order.strict_trans le_multiset_right_total by blast
qed
qed

lemma zero_less_iff_1_le_hmset: "0 < n ⟷ 1 ≤ n" for n :: hmultiset

lemma less_add_1_iff_le_hmset: "m < n + 1 ⟷ m ≤ n" for m n :: hmultiset
by (rule less_iff_add1_le_hmset[of m "n + 1", simplified])

instance hmultiset :: ordered_cancel_comm_semiring

instance hmultiset :: zero_less_one

instance hmultiset :: linordered_semiring_1_strict
by intro_classes

instance hmultiset :: bounded_lattice_bot
by intro_classes

instance hmultiset :: linordered_nonzero_semiring
by intro_classes simp

instance hmultiset :: semiring_no_zero_divisors
by intro_classes (use mult_pos_pos not_gr_zero_hmset in blast)

lemma lt_1_iff_eq_0_hmset: "M < 1 ⟷ M = 0" for M :: hmultiset

lemma zero_less_mult_iff_hmset[simp]: "0 < m * n ⟷ 0 < m ∧ 0 < n" for m n :: hmultiset
using mult_eq_0_iff not_gr_zero_hmset by blast

lemma one_le_mult_iff_hmset[simp]: "1 ≤ m * n ⟷ 1 ≤ m ∧ 1 ≤ n" for m n :: hmultiset
by (metis lt_1_iff_eq_0_hmset mult_eq_0_iff not_le)

lemma mult_less_cancel2_hmset[simp]: "m * k < n * k ⟷ 0 < k ∧ m < n" for k m n :: hmultiset
by (metis gr_zeroI_hmset leD leI le_cases mult_right_mono mult_zero_right times_hmultiset_monoL)

lemma mult_less_cancel1_hmset[simp]: "k * m < k * n ⟷ 0 < k ∧ m < n" for k m n :: hmultiset

lemma mult_le_cancel1_hmset[simp]: "k * m ≤ k * n ⟷ (0 < k ⟶ m ≤ n)" for k m n :: hmultiset

lemma mult_le_cancel2_hmset[simp]: "m * k ≤ n * k ⟷ (0 < k ⟶ m ≤ n)" for k m n :: hmultiset

lemma mult_le_cancel_left1_hmset: "y > 0 ⟹ x ≤ x * y" for x y :: hmultiset
by (metis zero_less_iff_1_le_hmset mult.commute mult.left_neutral mult_le_cancel2_hmset)

lemma mult_le_cancel_left2_hmset: "y ≤ 1 ⟹ x * y ≤ x" for x y :: hmultiset
by (metis mult.commute mult.left_neutral mult_le_cancel2_hmset)

lemma mult_le_cancel_right1_hmset: "y > 0 ⟹ x ≤ y * x" for x y :: hmultiset
by (subst mult.commute) (fact mult_le_cancel_left1_hmset)

lemma mult_le_cancel_right2_hmset: "y ≤ 1 ⟹ y * x ≤ x" for x y :: hmultiset
by (subst mult.commute) (fact mult_le_cancel_left2_hmset)

lemma le_square_hmset: "m ≤ m * m" for m :: hmultiset
using mult_le_cancel_left1_hmset by force

lemma le_cube_hmset: "m ≤ m * (m * m)" for m :: hmultiset
using mult_le_cancel_left1_hmset by force

lemma
less_imp_minus_plus_hmset: "m < n ⟹ k < k - m + n" and
le_imp_minus_plus_hmset: "m ≤ n ⟹ k ≤ k - m + n" for k m n :: hmultiset
by (meson add_less_cancel_left leD le_minus_plus_same_hmset less_le_trans not_le_imp_less)+

lemma gt_0_lt_mult_gt_1_hmset:
fixes m n :: hmultiset
assumes "m > 0" and "n > 1"
shows "m < m * n"
using assms by (metis mult.right_neutral mult_less_cancel1_hmset)

instance hmultiset :: linordered_comm_semiring_strict
by intro_classes simp

subsection ‹Embedding of Natural Numbers›

lemma of_nat_hmset: "of_nat n = HMSet (replicate_mset n 0)"
by (induct n) (auto simp: zero_hmultiset_def one_hmultiset_def plus_hmultiset_def)

lemma of_nat_inject_hmset[simp]: "(of_nat m :: hmultiset) = of_nat n ⟷ m = n"
unfolding of_nat_hmset by simp

lemma of_nat_minus_hmset: "of_nat (m - n) = (of_nat m :: hmultiset) - of_nat n"
unfolding of_nat_hmset minus_hmultiset_def by simp

lemma plus_of_nat_plus_of_nat_hmset:
"k + of_nat m + of_nat n = k + of_nat (m + n)" for k :: hmultiset
by simp

lemma plus_of_nat_minus_of_nat_hmset:
fixes k :: hmultiset
assumes "n ≤ m"
shows "k + of_nat m - of_nat n = k + of_nat (m - n)"

lemma of_nat_lt_ω[simp]: "of_nat n < ω"
by (auto simp: of_nat_hmset zero_less_iff_neq_zero_hmset less_multiset_ext⇩D⇩M_less)

lemma of_nat_ne_ω[simp]: "of_nat n ≠ ω"

lemma of_nat_less_hmset[simp]: "(of_nat M :: hmultiset) < of_nat N ⟷ M < N"
unfolding of_nat_hmset less_multiset_ext⇩D⇩M_less by simp

lemma of_nat_le_hmset[simp]: "(of_nat M :: hmultiset) ≤ of_nat N ⟷ M ≤ N"
unfolding of_nat_hmset order_le_less less_multiset_ext⇩D⇩M_less by simp

lemma of_nat_times_ω_exp: "of_nat n * ω^m = HMSet (replicate_mset n m)"
by (induct n) (simp_all add: hmsetmset_plus one_hmultiset_def)

lemma ω_exp_times_of_nat: "ω^m * of_nat n = HMSet (replicate_mset n m)"
using of_nat_times_ω_exp by simp

subsection ‹Embedding of Extended Natural Numbers›

primrec hmset_of_enat :: "enat ⇒ hmultiset" where
"hmset_of_enat (enat n) = of_nat n"
| "hmset_of_enat ∞ = ω"

lemma hmset_of_enat_0[simp]: "hmset_of_enat 0 = 0"

lemma hmset_of_enat_1[simp]: "hmset_of_enat 1 = 1"
by (simp add: one_enat_def del: One_nat_def)

lemma hmset_of_enat_of_nat[simp]: "hmset_of_enat (of_nat n) = of_nat n"
using of_nat_eq_enat by auto

lemma hmset_of_enat_numeral[simp]: "hmset_of_enat (numeral n) = numeral n"

lemma hmset_of_enat_le_ω[simp]: "hmset_of_enat n ≤ ω"
using of_nat_lt_ω[THEN less_imp_le] by (cases n) auto

lemma hmset_of_enat_eq_ω_iff[simp]: "hmset_of_enat n = ω ⟷ n = ∞"
by (cases n) auto

definition head_ω :: "hmultiset ⇒ hmultiset" where
"head_ω M = (if M = 0 then 0 else ω^(Max (set_mset (hmsetmset M))))"

by simp

lemma head_ω_of_nat[simp]: "head_ω (of_nat n) = (if n = 0 then 0 else 1)"
unfolding head_ω_def one_hmultiset_def of_nat_hmset by simp

assumes m_le_n: "m ≤ n"
proof -
have le_in_le_max: "⋀a M N. M ≤ N ⟹ a ∈# M ⟹ a ≤ Max (set_mset N)"
by (metis (no_types) Max_ge finite_set_mset le_less less_eq_multiset⇩H⇩O linorder_not_less
mem_Collect_eq neq0_conv order_trans set_mset_def)
show ?thesis
by (cases m, cases n,
auto simp del: hmsetmset_le simp: head_ω_def hmsetmset_le[symmetric] zero_hmultiset_def,
metis Max_in dual_order.antisym finite_set_mset le_in_le_max le_less set_mset_eq_empty_iff)
qed

by (rule all_lt_Max_imp_lt_mset, auto simp: zero_hmultiset_def split: if_splits)

proof (cases m n rule: hmultiset.exhaust[case_product hmultiset.exhaust])
case m_n: (HMSet_HMSet M N)
show ?thesis
proof (cases "Max_mset M < Max_mset N")
case True
thus ?thesis
unfolding m_n head_ω_def sup_hmultiset_def zero_hmultiset_def plus_hmultiset_def
by (simp add: Max.union max_def dual_order.strict_implies_order)
next
case False
thus ?thesis
unfolding m_n head_ω_def sup_hmultiset_def zero_hmultiset_def plus_hmultiset_def
by simp (metis False Max.union finite_set_mset leI max_def set_mset_eq_empty_iff sup.commute)
qed
qed

proof (cases "m = 0 ∨ n = 0")
case False
hence m_nz: "m ≠ 0" and n_nz: "n ≠ 0"
by simp+

define δ where "δ = hmsetmset m"
define ε where "ε = hmsetmset n"

have δ_nemp: "δ ≠ {#}"
unfolding δ_def using m_nz by simp
have ε_nemp: "ε ≠ {#}"
unfolding ε_def using n_nz by simp

let ?D = "set_mset δ"
let ?E = "set_mset ε"
let ?DE = "{z. ∃x ∈ ?D. ∃y ∈ ?E. z = x + y}"

have max_D_in: "Max ?D ∈ ?D"
using δ_nemp by simp
have max_E_in: "Max ?E ∈ ?E"
using ε_nemp by simp

have "Max ?DE = Max ?D + Max ?E"
proof (rule order_antisym, goal_cases le ge)
case le
have "⋀x y. x ∈ ?D ⟹ y ∈ ?E ⟹ x + y ≤ Max ?D + Max ?E"
hence mem_imp_le: "⋀z. z ∈ ?DE ⟹ z ≤ Max ?D + Max ?E"
by auto
show ?case
by (intro mem_imp_le Max_in, simp, use δ_nemp ε_nemp in fast)
next
case ge
have "{z. ∃x ∈ {Max ?D}. ∃y ∈ {Max ?E}. z = x + y} ⊆ {z. ∃x ∈# δ. ∃y ∈# ε. z = x + y}"
using max_D_in max_E_in by fast
thus ?case
by simp
qed
thus ?thesis
unfolding δ_def ε_def by (auto simp: head_ω_def image_def times_hmultiset_def)
qed auto

subsection ‹More Inequalities and Some Equalities›

lemma zero_lt_ω[simp]: "0 < ω"
by (metis of_nat_lt_ω of_nat_0)

lemma one_lt_ω[simp]: "1 < ω"
by (metis enat_defs(2) hmset_of_enat.simps(1) hmset_of_enat_1 of_nat_lt_ω)

lemma numeral_lt_ω[simp]: "numeral n < ω"
using hmset_of_enat_numeral[symmetric] hmset_of_enat.simps(1) of_nat_lt_ω numeral_eq_enat
by presburger

lemma one_le_ω[simp]: "1 ≤ ω"

lemma of_nat_le_ω[simp]: "of_nat n ≤ ω"

lemma numeral_le_ω[simp]: "numeral n ≤ ω"

lemma not_ω_lt_1[simp]: "¬ ω < 1"

lemma not_ω_lt_of_nat[simp]: "¬ ω < of_nat n"

lemma not_ω_lt_numeral[simp]: "¬ ω < numeral n"

lemma not_ω_le_1[simp]: "¬ ω ≤ 1"

lemma not_ω_le_of_nat[simp]: "¬ ω ≤ of_nat n"

lemma not_ω_le_numeral[simp]: "¬ ω ≤ numeral n"

lemma zero_ne_ω[simp]: "0 ≠ ω"
by (metis not_ω_le_1 zero_le_hmset)

lemma one_ne_ω[simp]: "1 ≠ ω"
using not_ω_le_1 by force

lemma numeral_ne_ω[simp]: "numeral n ≠ ω"
by (metis not_ω_le_numeral numeral_le_ω)

lemma
ω_ne_0[simp]: "ω ≠ 0" and
ω_ne_1[simp]: "ω ≠ 1" and
ω_ne_of_nat[simp]: "ω ≠ of_nat m" and
ω_ne_numeral[simp]: "ω ≠ numeral n"
using zero_ne_ω one_ne_ω of_nat_ne_ω numeral_ne_ω by metis+

lemma
hmset_of_enat_inject[simp]: "hmset_of_enat m = hmset_of_enat n ⟷ m = n" and
hmset_of_enat_less[simp]: "hmset_of_enat m < hmset_of_enat n ⟷ m < n" and
hmset_of_enat_le[simp]: "hmset_of_enat m ≤ hmset_of_enat n ⟷ m ≤ n"
by (cases m; cases n; simp)+

lemma lt_ω_imp_ex_of_nat:
assumes M_lt_ω: "M < ω"
shows "∃n. M = of_nat n"
proof -
have M_lt_single_1: "hmsetmset M < {#1#}"
by (rule M_lt_ω[unfolded hmsetmset_less[symmetric] less_multiset_ext⇩D⇩M_less hmultiset.sel])

have "N = 0" if "N ∈# hmsetmset M" for N
proof -
have "0 < count (hmsetmset M) N"
using that by auto
hence "N < 1"
by (metis (no_types) M_lt_single_1 count_single gr_implies_not0 less_eq_multiset⇩H⇩O less_one
neq_iff not_le)
thus ?thesis
qed
then obtain n where hmmM: "M = HMSet (replicate_mset n 0)"
using ex_replicate_mset_if_all_elems_eq by (metis hmultiset.collapse)
show ?thesis
unfolding hmmM of_nat_hmset by blast
qed

lemma le_ω_imp_ex_hmset_of_enat:
assumes M_le_ω: "M ≤ ω"
shows "∃n. M = hmset_of_enat n"
proof (cases "M = ω")
case True
thus ?thesis
by (metis hmset_of_enat.simps(2))
next
case False
thus ?thesis
using M_le_ω lt_ω_imp_ex_of_nat by (metis hmset_of_enat.simps(1) le_less)
qed

lemma lt_ω_lt_ω_imp_times_lt_ω: "M < ω ⟹ N < ω ⟹ M * N < ω"
by (metis lt_ω_imp_ex_of_nat of_nat_lt_ω of_nat_mult)

lemma times_ω_minus_of_nat[simp]: "m * ω - of_nat n = m * ω"
by (auto intro!: Diff_triv_mset simp: times_hmultiset_def minus_hmultiset_def
Times_mset_single_right of_nat_hmset disjunct_not_in image_def)

lemma times_ω_minus_numeral[simp]: "m * ω - numeral n = m * ω"
by (metis of_nat_numeral times_ω_minus_of_nat)

lemma ω_minus_of_nat[simp]: "ω - of_nat n = ω"
using times_ω_minus_of_nat[of 1] by (metis mult.left_neutral)

lemma ω_minus_1[simp]: "ω - 1 = ω"
using ω_minus_of_nat[of 1] by simp

lemma ω_minus_numeral[simp]: "ω - numeral n = ω"
using times_ω_minus_numeral[of 1] by (metis mult.left_neutral)

lemma hmset_of_enat_minus_enat[simp]: "hmset_of_enat (m - enat n) = hmset_of_enat m - of_nat n"
by (cases m) (auto simp: of_nat_minus_hmset)

lemma of_nat_lt_hmset_of_enat_iff: "of_nat m < hmset_of_enat n ⟷ enat m < n"
by (metis hmset_of_enat.simps(1) hmset_of_enat_less)

lemma of_nat_le_hmset_of_enat_iff: "of_nat m ≤ hmset_of_enat n ⟷ enat m ≤ n"
by (metis hmset_of_enat.simps(1) hmset_of_enat_le)

lemma hmset_of_enat_lt_iff_ne_infinity: "hmset_of_enat x < ω ⟷ x ≠ ∞"
by (cases x; simp)

lemma minus_diff_sym_hmset: "m - (m - n) = n - (n - m)" for m n :: hmultiset
unfolding minus_hmultiset_def by (simp flip: inter_mset_def ac_simps)

lemma diff_plus_sym_hmset: "(c - b) + b = (b - c) + c" for b c :: hmultiset
proof -
have f1: "⋀h ha :: hmultiset. h - (ha + h) = 0"
have f2: "⋀h ha hb :: hmultiset. h + ha - (h - hb) = hb + ha - (hb - h)"
have "⋀h ha hb :: hmultiset. h + (ha + hb) - hb = h + ha"
then show ?thesis
qed

lemma times_diff_plus_sym_hmset: "a * (c - b) + a * b = a * (b - c) + a * c" for a b c :: hmultiset
by (metis distrib_left diff_plus_sym_hmset)

lemma times_of_nat_minus_left:
"(of_nat m - of_nat n) * l = of_nat m * l - of_nat n * l" for l :: hmultiset
by (induct n m rule: diff_induct) (auto simp: ring_distribs)

lemma times_of_nat_minus_right:
"l * (of_nat m - of_nat n) = l * of_nat m - l * of_nat n" for l :: hmultiset
by (metis times_of_nat_minus_left mult.commute)

lemma lt_ω_imp_times_minus_left: "m < ω ⟹ n < ω ⟹ (m - n) * l = m * l - n * l"
by (metis lt_ω_imp_ex_of_nat times_of_nat_minus_left)

lemma lt_ω_imp_times_minus_right: "m < ω ⟹ n < ω ⟹ l * (m - n) = l * m - l * n"
by (metis lt_ω_imp_ex_of_nat times_of_nat_minus_right)

lemma hmset_pair_decompose:
"∃k n1 n2. m1 = k + n1 ∧ m2 = k + n2 ∧ (head_ω n1 ≠ head_ω n2 ∨ n1 = 0 ∧ n2 = 0)"
proof -
define n1 where n1: "n1 = m1 - m2"
define n2 where n2: "n2 = m2 - m1"
define k where k1: "k = m1 - n1"

have k2: "k = m2 - n2"
using k1 unfolding n1 n2 by (simp add: minus_diff_sym_hmset)

have "m1 = k + n1"
unfolding k1
moreover have "m2 = k + n2"
unfolding k2
moreover have hd_n: "head_ω n1 ≠ head_ω n2" if n1_or_n2_nz: "n1 ≠ 0 ∨ n2 ≠ 0"
proof (cases "n1 = 0" "n2 = 0" rule: bool.exhaust[case_product bool.exhaust])
case False_False
note n1_nz = this(1)[simplified] and n2_nz = this(2)[simplified]

define δ1 where "δ1 = hmsetmset n1"
define δ2 where "δ2 = hmsetmset n2"

have δ1_inter_δ2: "δ1 ∩# δ2 = {#}"
unfolding δ1_def δ2_def n1 n2 minus_hmultiset_def by (simp add: diff_intersect_sym_diff)

have δ1_ne: "δ1 ≠ {#}"
unfolding δ1_def using n1_nz by simp
have δ2_ne: "δ2 ≠ {#}"
unfolding δ2_def using n2_nz by simp

have max_δ1: "Max (set_mset δ1) ∈# δ1"
using δ1_ne by simp
have max_δ2: "Max (set_mset δ2) ∈# δ2"
using δ2_ne by simp
have max_δ1_ne_δ2: "Max (set_mset δ1) ≠ Max (set_mset δ2)"
using δ1_inter_δ2 disjunct_not_in max_δ1 max_δ2 by force

show ?thesis
using n1_nz n2_nz
by (cases n1 rule: hmultiset.exhaust_sel, cases n2 rule: hmultiset.exhaust_sel,
auto simp: head_ω_def zero_hmultiset_def max_δ1_ne_δ2[unfolded δ1_def δ2_def])
qed (use n1_or_n2_nz in ‹auto simp: head_ω_def›)
ultimately show ?thesis
by blast
qed

lemma hmset_pair_decompose_less:
assumes m1_lt_m2: "m1 < m2"
shows "∃k n1 n2. m1 = k + n1 ∧ m2 = k + n2 ∧ head_ω n1 < head_ω n2"
proof -
obtain k n1 n2 where
m1: "m1 = k + n1" and
m2: "m2 = k + n2" and
hds: "head_ω n1 ≠ head_ω n2 ∨ n1 = 0 ∧ n2 = 0"
using hmset_pair_decompose[of m1 m2] by blast

{
assume "n1 = 0" and "n2 = 0"
hence "m1 = m2"
unfolding m1 m2 by simp
hence False
using m1_lt_m2 by simp
}
moreover
{
hence "n1 > n2"
hence "m1 > m2"
unfolding m1 m2 by simp
hence False
using m1_lt_m2 by simp
}
ultimately show ?thesis
using m1 m2 hds by (blast elim: neqE)
qed

lemma hmset_pair_decompose_less_eq:
assumes "m1 ≤ m2"
shows "∃k n1 n2. m1 = k + n1 ∧ m2 = k + n2 ∧ (head_ω n1 < head_ω n2 ∨ n1 = 0 ∧ n2 = 0)"
using assms

lemma mono_cross_mult_less_hmset:
fixes Aa A Ba B :: hmultiset
assumes A_lt: "A < Aa" and B_lt: "B < Ba"
shows "A * Ba + B * Aa < A * B + Aa * Ba"
proof -
obtain j m1 m2 where A: "A = j + m1" and Aa: "Aa = j + m2" and hd_m: "head_ω m1 < head_ω m2"
by (metis hmset_pair_decompose_less[OF A_lt])
obtain k n1 n2 where B: "B = k + n1" and Ba: "Ba = k + n2" and hd_n: "head_ω n1 < head_ω n2"
by (metis hmset_pair_decompose_less[OF B_lt])

have hd_lt: "head_ω (m1 * n2 + m2 * n1) < head_ω (m1 * n1 + m2 * n2)"
proof simp
have "⋀h ha :: hmultiset. 0 < h ∨ ¬ ha < h"
by force
using hd_m hd_n sup_hmultiset_def by auto
by (meson leI sup.bounded_iff)
qed
show ?thesis
unfolding A Aa B Ba ring_distribs by (simp add: algebra_simps head_ω_lt_imp_lt[OF hd_lt])
qed

lemma triple_cross_mult_hmset:
"An * (Bn * Cn + Bp * Cp - (Bn * Cp + Cn * Bp))
+ (Cn * (An * Bp + Bn * Ap - (An * Bn + Ap * Bp))
+ (Ap * (Bn * Cp + Cn * Bp - (Bn * Cn + Bp * Cp))
+ Cp * (An * Bn + Ap * Bp - (An * Bp + Bn * Ap)))) =
An * (Bn * Cp + Cn * Bp - (Bn * Cn + Bp * Cp))
+ (Cn * (An * Bn + Ap * Bp - (An * Bp + Bn * Ap))
+ (Ap * (Bn * Cn + Bp * Cp - (Bn * Cp + Cn * Bp))
+ Cp * (An * Bp + Bn * Ap - (An * Bn + Ap * Bp))))"
for Ap An Bp Bn Cp Cn Dp Dn :: hmultiset

apply (rule add_right_cancel[THEN iffD1, of _ "Cp * (An * Bp + Ap * Bn)"])
apply (subst times_diff_plus_sym_hmset)

apply (rule add_right_cancel[THEN iffD1, of _ "Cn * (An * Bn + Ap * Bp)"])
apply (subst times_diff_plus_sym_hmset)

apply (rule add_right_cancel[THEN iffD1, of _ "Ap * (Bn * Cn + Bp * Cp)"])
apply (subst times_diff_plus_sym_hmset)

apply (rule add_right_cancel[THEN iffD1, of _ "An * (Bn * Cp + Bp * Cn)"])
apply (subst times_diff_plus_sym_hmset)

subsection ‹Conversions to Natural Numbers›

definition offset_hmset :: "hmultiset ⇒ nat" where
"offset_hmset M = count (hmsetmset M) 0"

lemma offset_hmset_of_nat[simp]: "offset_hmset (of_nat n) = n"
unfolding offset_hmset_def of_nat_hmset by simp

lemma offset_hmset_numeral[simp]: "offset_hmset (numeral n) = numeral n"
unfolding offset_hmset_def by (metis offset_hmset_def offset_hmset_of_nat of_nat_numeral)

definition sum_coefs :: "hmultiset ⇒ nat" where
"sum_coefs M = size (hmsetmset M)"

lemma sum_coefs_distrib_plus[simp]: "sum_coefs (M + N) = sum_coefs M + sum_coefs N"
unfolding plus_hmultiset_def sum_coefs_def by simp

lemma sum_coefs_gt_0: "sum_coefs M > 0 ⟷ M > 0"
by (auto simp: sum_coefs_def zero_hmultiset_def hmsetmset_less[symmetric] less_multiset_ext⇩D⇩M_less
nonempty_has_size[symmetric])

subsection ‹An Example›

text ‹
The following proof is based on an informal proof by Uwe Waldmann, inspired by
a similar argument by Michel Ludwig.
›

lemma ludwig_waldmann_less:
fixes α1 α2 β1 β2 γ δ :: hmultiset
assumes
αβ2γ_lt_αβ1γ: "α2 + β2 * γ < α1 + β1 * γ" and
β2_le_β1: "β2 ≤ β1" and
γ_lt_δ: "γ < δ"
shows "α2 + β2 * δ < α1 + β1 * δ"
proof -
obtain β0 β2a β1a where
β1: "β1 = β0 + β1a" and
β2: "β2 = β0 + β2a" and
hd_β2a_vs_β1a: "head_ω β2a < head_ω β1a ∨ β2a = 0 ∧ β1a = 0"
using hmset_pair_decompose_less_eq[OF β2_le_β1] by blast

obtain η γa δa where
γ: "γ = η + γa" and
δ: "δ = η + δa" and
using hmset_pair_decompose_less[OF γ_lt_δ] by blast

have "α2 + β0 * γ + β2a * γ = α2 + β2 * γ"
also have "… < α1 + β1 * γ"
by (rule αβ2γ_lt_αβ1γ)
also have "… = α1 + β0 * γ + β1a * γ"
finally have *: "α2 + β2a * γ < α1 + β1a * γ"

have "α2 + β2 * δ = α2 + β0 * δ + β2a * δ"
also have "… = α2 + β0 * δ + β2a * η + β2a * δa"
unfolding δ by (simp add: distrib_left semiring_normalization_rules(25))
also have "… ≤ α2 + β0 * δ + β2a * η + β2a * δa + β2a * γa"
by simp
also have "… = α2 + β2a * γ + β0 * δ + β2a * δa"
also have "… < α1 + β1a * γ + β0 * δ + β2a * δa"
using * by simp
also have "… = α1 + β1a * η + β1a * γa + β0 * η + β0 * δa + β2a * δa"
unfolding γ δ distrib_left add.assoc[symmetric] by (rule refl)
also have "… ≤ α1 + β1a * η + β0 * η + β0 * δa + β1a * δa"
proof -
have "β1a * γa + β2a * δa ≤ β1a * δa"
proof (cases "β2a = 0 ∧ β1a = 0")
case False
using hd_β2a_vs_β1a by blast
hence "head_ω (β1a * γa + β2a * δa) < head_ω (β1a * δa)"
using hd_γa_lt_δa by (auto intro: gr_zeroI_hmset simp: sup_hmultiset_def)
hence "β1a * γa + β2a * δa < β1a * δa"
thus ?thesis
by simp
qed simp
thus ?thesis
by simp
qed
finally show ?thesis
unfolding β1 δ
qed

end


# Theory Signed_Syntactic_Ordinal

(*  Title:       Signed Syntactic Ordinals in Cantor Normal Form
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
Author:      Mathias Fleury <mfleury at mpi-inf.mpg.de>, 2016
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2016
Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Signed Syntactic Ordinals in Cantor Normal Form›

theory Signed_Syntactic_Ordinal
imports Signed_Hereditary_Multiset Syntactic_Ordinal
begin

subsection ‹Natural (Hessenberg) Product›

instantiation zhmultiset :: comm_ring_1
begin

abbreviation ω⇩z_exp :: "hmultiset ⇒ zhmultiset" ("ω⇩z^") where
"ω⇩z^ ≡ λm. ZHMSet {#m#}⇩z"

lift_definition one_zhmultiset :: zhmultiset is "{#0#}⇩z" .

abbreviation ω⇩z :: zhmultiset where
"ω⇩z ≡ ω⇩z^1"

lemma ω⇩z_as_ω: "ω⇩z = zhmset_of ω"
by simp

lift_definition times_zhmultiset :: "zhmultiset ⇒ zhmultiset ⇒ zhmultiset" is
"λM N.
zmset_of (hmsetmset (HMSet (mset_pos M) * HMSet (mset_pos N)))
- zmset_of (hmsetmset (HMSet (mset_pos M) * HMSet (mset_neg N)))
+ zmset_of (hmsetmset (HMSet (mset_neg M) * HMSet (mset_neg N)))
- zmset_of (hmsetmset (HMSet (mset_neg M) * HMSet (mset_pos N)))" .

lemmas zhmsetmset_times = times_zhmultiset.rep_eq

instance
proof (intro_classes, goal_cases mult_assoc mult_comm mult_1 distrib zero_neq_one)
case (mult_assoc a b c)
show ?case
by (transfer,
simp add: algebra_simps zmset_of_plus[symmetric] hmsetmset_plus[symmetric] HMSet_diff,
rule triple_cross_mult_hmset)
next
case (mult_comm a b)
show ?case
by transfer (auto simp: algebra_simps)
next
case (mult_1 a)
show ?case
by transfer (auto simp: algebra_simps mset_pos_neg_partition[symmetric])
next
case (distrib a b c)

show ?case
by (simp add: times_zhmultiset_def ZHMSet_plus[symmetric] zmset_of_plus[symmetric]
hmsetmset_plus[symmetric] algebra_simps hmset_pos_plus hmset_neg_plus)
(simp add: mult.commute[of _ "hmset_pos c"] mult.commute[of _ "hmset_neg c"]
add.commute[of "hmset_neg c * M" "hmset_pos c * N" for M N]
next
case zero_neq_one
show ?case
unfolding zero_zhmultiset_def one_zhmultiset_def by simp
qed

end

lemma zhmset_of_1: "zhmset_of 1 = 1"

lemma zhmset_of_times: "zhmset_of (A * B) = zhmset_of A * zhmset_of B"
by transfer simp

lemma zhmset_of_prod_list:
"zhmset_of (prod_list Ms) = prod_list (map zhmset_of Ms)"
by (induct Ms) (auto simp: one_hmultiset_def one_zhmultiset_def zhmset_of_times)

subsection ‹Embedding of Natural Numbers›

lemma of_nat_zhmset: "of_nat n = zhmset_of (of_nat n)"
by (induct n) (auto simp: zero_zhmultiset_def zhmset_of_plus zhmset_of_1)

lemma of_nat_inject_zhmset[simp]: "(of_nat m :: zhmultiset) = of_nat n ⟷ m = n"
unfolding of_nat_zhmset by simp

lemma plus_of_nat_plus_of_nat_zhmset:
"k + of_nat m + of_nat n = k + of_nat (m + n)" for k :: zhmultiset
by simp

lemma plus_of_nat_minus_of_nat_zhmset:
fixes k :: zhmultiset
assumes "n ≤ m"
shows "k + of_nat m - of_nat n = k + of_nat (m - n)"
using assms by (simp add: of_nat_diff)

lemma of_nat_lt_ω⇩z[simp]: "of_nat n < ω⇩z"
unfolding ω⇩z_as_ω using of_nat_lt_ω of_nat_zhmset zhmset_of_less by presburger

lemma of_nat_ne_ω⇩z[simp]: "of_nat n ≠ ω⇩z"
by (metis of_nat_lt_ω⇩z mset_le_asym mset_lt_single_iff)

subsection ‹Embedding of Extended Natural Numbers›

primrec zhmset_of_enat :: "enat ⇒ zhmultiset" where
"zhmset_of_enat (enat n) = of_nat n"
| "zhmset_of_enat ∞ = ω⇩z"

lemma zhmset_of_enat_0[simp]: "zhmset_of_enat 0 = 0"

lemma zhmset_of_enat_1[simp]: "zhmset_of_enat 1 = 1"
by (simp add: one_enat_def del: One_nat_def)

lemma zhmset_of_enat_of_nat[simp]: "zhmset_of_enat (of_nat n) = of_nat n"
using of_nat_eq_enat by auto

lemma zhmset_of_enat_numeral[simp]: "zhmset_of_enat (numeral n) = numeral n"

lemma zhmset_of_enat_le_ω⇩z[simp]: "zhmset_of_enat n ≤ ω⇩z"
using of_nat_lt_ω⇩z[THEN less_imp_le] by (cases n) auto

lemma zhmset_of_enat_eq_ω⇩z_iff[simp]: "zhmset_of_enat n = ω⇩z ⟷ n = ∞"
by (cases n) auto

subsection ‹Inequalities and Some (Dis)equalities›

instance zhmultiset :: zero_less_one
by (intro_classes, transfer, transfer, auto)

instantiation zhmultiset :: linordered_idom
begin

definition sgn_zhmultiset :: "zhmultiset ⇒ zhmultiset" where
"sgn_zhmultiset M = (if M = 0 then 0 else if M > 0 then 1 else -1)"

definition abs_zhmultiset :: "zhmultiset ⇒ zhmultiset" where
"abs_zhmultiset M = (if M < 0 then - M else M)"

lemma gt_0_times_gt_0_imp:
fixes a b :: zhmultiset
assumes a_gt0: "a > 0" and b_gt0: "b > 0"
shows "a * b > 0"
proof -
show ?thesis
using a_gt0 b_gt0
by (subst (asm) (2 4) zhmset_pos_neg_partition, simp, transfer,
simp del: HMSet_less add: algebra_simps zmset_of_plus[symmetric] hmsetmset_plus[symmetric]
zmset_of_less HMSet_less[symmetric])
(rule mono_cross_mult_less_hmset)
qed

instance
proof intro_classes
fix a b c :: zhmultiset

assume
a_lt_b: "a < b" and
zero_lt_c: "0 < c"

have "c * b < c * b + c * (b - a)"
using gt_0_times_gt_0_imp by (simp add: a_lt_b zero_lt_c)
hence "c * a + c * (b - a) < c * b + c * (b - a)"
thus "c * a < c * b"
by simp
qed (auto simp: sgn_zhmultiset_def abs_zhmultiset_def)

end

lemma le_zhmset_of_pos: "M ≤ zhmset_of (hmset_pos M)"
by (simp add: less_eq_zhmultiset.rep_eq mset_pos_supset subset_eq_imp_le_zmset)

lemma minus_zhmset_of_pos_le: "- zhmset_of (hmset_neg M) ≤ M"
by (metis le_zhmset_of_pos minus_le_iff mset_pos_uminus zhmsetmset_uminus)

lemma zhmset_of_nonneg[simp]: "zhmset_of M ≥ 0"
by (metis hmsetmset_0 zero_le_hmset zero_zhmultiset_def zhmset_of_le zmset_of_empty)

lemma
fixes n :: zhmultiset
assumes "0 ≤ m"
shows
le_add1_hmset: "n ≤ n + m" and
le_add2_hmset: "n ≤ m + n"
using assms by simp+

lemma less_iff_add1_le_zhmset: "m < n ⟷ m + 1 ≤ n" for m n :: zhmultiset
proof
assume m_lt_n: "m < n"
show "m + 1 ≤ n"
proof -
obtain hh :: hmultiset and zz :: zhmultiset and hha :: hmultiset where
f1: "m = zhmset_of hh + zz ∧ n = zhmset_of hha + zz ∧ hh < hha"
using less_hmset_zhmsetE[OF m_lt_n] by metis
hence "zhmset_of (hh + 1) ≤ zhmset_of hha"
thus ?thesis
using f1 by (simp add: zhmset_of_1 zhmset_of_plus)
qed
qed simp

lemma gt_0_lt_mult_gt_1_zhmset:
fixes m n :: zhmultiset
assumes "m > 0" and "n > 1"
shows "m < m * n"
using assms by simp

lemma zero_less_iff_1_le_zhmset: "0 < n ⟷ 1 ≤ n" for n :: zhmultiset

lemma less_add_1_iff_le_hmset: "m < n + 1 ⟷ m ≤ n" for m n :: zhmultiset
by (rule less_iff_add1_le_zhmset[of m "n + 1", simplified])

lemma nonneg_le_mult_right_mono_zhmset:
fixes x y z :: zhmultiset
assumes x: "0 ≤ x" and y: "0 < y" and z: "x ≤ z"
shows "x ≤ y * z"
using x zero_less_iff_1_le_zhmset[THEN iffD1, OF y] z
by (meson dual_order.trans leD mult_less_cancel_right2 not_le_imp_less)

instance hmultiset :: ordered_cancel_comm_semiring
by intro_classes

instance hmultiset :: linordered_semiring_1_strict
by intro_classes

instance hmultiset :: bounded_lattice_bot
by intro_classes

instance hmultiset :: zero_less_one
by intro_classes

instance hmultiset :: linordered_nonzero_semiring
by intro_classes

instance hmultiset :: semiring_no_zero_divisors
by intro_classes

lemma zero_lt_ω⇩z[simp]: "0 < ω⇩z"
by (metis of_nat_lt_ω⇩z of_nat_0)

lemma one_lt_ω[simp]: "1 < ω⇩z"
by (metis enat_defs(2) zhmset_of_enat.simps(1) zhmset_of_enat_1 of_nat_lt_ω⇩z)

lemma numeral_lt_ω⇩z[simp]: "numeral n < ω⇩z"
using zhmset_of_enat_numeral[symmetric] zhmset_of_enat.simps(1) of_nat_lt_ω⇩z numeral_eq_enat
by presburger

lemma one_le_ω⇩z[simp]: "1 ≤ ω⇩z"

lemma of_nat_le_ω⇩z[simp]: "of_nat n ≤ ω⇩z"

lemma numeral_le_ω⇩z[simp]: "numeral n ≤ ω⇩z"

lemma not_ω⇩z_lt_1[simp]: "¬ ω⇩z < 1"

lemma not_ω⇩z_lt_of_nat[simp]: "¬ ω⇩z < of_nat n"

lemma not_ω⇩z_lt_numeral[simp]: "¬ ω⇩z < numeral n"

lemma not_ω⇩z_le_1[simp]: "¬ ω⇩z ≤ 1"

lemma not_ω⇩z_le_of_nat[simp]: "¬ ω⇩z ≤ of_nat n"

lemma not_ω⇩z_le_numeral[simp]: "¬ ω⇩z ≤ numeral n"

lemma zero_ne_ω⇩z[simp]: "0 ≠ ω⇩z"
using zero_lt_ω⇩z by linarith

lemma one_ne_ω⇩z[simp]: "1 ≠ ω⇩z"
using not_ω⇩z_le_1 by force

lemma numeral_ne_ω⇩z[simp]: "numeral n ≠ ω⇩z"
by (metis not_ω⇩z_le_numeral numeral_le_ω⇩z)

lemma
ω⇩z_ne_0[simp]: "ω⇩z ≠ 0" and
ω⇩z_ne_1[simp]: "ω⇩z ≠ 1" and
ω⇩z_ne_of_nat[simp]: "ω⇩z ≠ of_nat m" and
ω⇩z_ne_numeral[simp]: "ω⇩z ≠ numeral n"
using zero_ne_ω⇩z one_ne_ω⇩z of_nat_ne_ω⇩z numeral_ne_ω⇩z by metis+

lemma
zhmset_of_enat_inject[simp]: "zhmset_of_enat m = zhmset_of_enat n ⟷ m = n" and
zhmset_of_enat_lt_iff_lt[simp]: "zhmset_of_enat m < zhmset_of_enat n ⟷ m < n" and
zhmset_of_enat_le_iff_le[simp]: "zhmset_of_enat m ≤ zhmset_of_enat n ⟷ m ≤ n"
by (cases m; cases n; simp)+

lemma of_nat_lt_zhmset_of_enat_iff: "of_nat m < zhmset_of_enat n ⟷ enat m < n"
by (metis zhmset_of_enat.simps(1) zhmset_of_enat_lt_iff_lt)

lemma of_nat_le_zhmset_of_enat_iff: "of_nat m ≤ zhmset_of_enat n ⟷ enat m ≤ n"
by (metis zhmset_of_enat.simps(1) zhmset_of_enat_le_iff_le)

lemma zhmset_of_enat_lt_iff_ne_infinity: "zhmset_of_enat x < ω⇩z ⟷ x ≠ ∞"
by (cases x; simp)

subsection ‹An Example›

text ‹
A new proof of @{thm ludwig_waldmann_less}:
›

lemma
fixes α1 α2 β1 β2 γ δ :: hmultiset
assumes
αβ2γ_lt_αβ1γ: "α2 + β2 * γ < α1 + β1 * γ" and
β2_le_β1: "β2 ≤ β1" and
γ_lt_δ: "γ < δ"
shows "α2 + β2 * δ < α1 + β1 * δ"
proof -
let ?z = zhmset_of

note αβ2γ_lt_αβ1γ' = αβ2γ_lt_αβ1γ[THEN zhmset_of_less[THEN iffD2],
simplified zhmset_of_plus zhmset_of_times]
note β2_le_β1' = β2_le_β1[THEN zhmset_of_le[THEN iffD2]]
note γ_lt_δ' = γ_lt_δ[THEN zhmset_of_less[THEN iffD2]]

have "?z α2 + ?z β2 * ?z δ < ?z α1 + ?z β1 * ?z γ + ?z β2 * (?z δ - ?z γ)"
using αβ2γ_lt_αβ1γ' by (simp add: algebra_simps)
also have "… ≤ ?z α1 + ?z β1 * ?z γ + ?z β1 * (?z δ - ?z γ)"
using β2_le_β1' γ_lt_δ' by simp
finally show ?thesis
by (simp add: zmset_of_less zhmset_of_times[symmetric] zhmset_of_plus[symmetric] algebra_simps)
qed

end


# Theory Syntactic_Ordinal_Bridge

(*  Title:       Syntactic Ordinals in Cantor Normal Form
Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2017
Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
*)

theory Syntactic_Ordinal_Bridge
imports "HOL-Library.Sublist" Ordinal.OrdinalOmega Syntactic_Ordinal
abbrevs
"!h" = "⇩h"
begin

section ‹Bridge between Huffman's Ordinal Library and the Syntactic Ordinals›

subsection ‹Missing Lemmas about Huffman's Ordinals›

instantiation ordinal :: order_bot
begin

definition bot_ordinal :: ordinal where
"bot_ordinal = 0"

instance

end

lemma insort_bot[simp]: "insort bot xs = bot # xs" for xs :: "'a::{order_bot,linorder} list"

lemmas insort_0_ordinal[simp] = insort_bot[of "xs :: ordinal list" for xs, unfolded bot_ordinal_def]

lemma from_cnf_less_ω_exp:
assumes "∀k ∈ set ks. k < l"
shows "from_cnf ks < ω ** l"

lemma from_cnf_0_iff[simp]: "from_cnf ks = 0 ⟷ ks = []"
by (induct ks) (auto simp: ordinal_plus_not_0)

lemma from_cnf_append[simp]: "from_cnf (ks @ ls) = from_cnf ks + from_cnf ls"
by (induct ks) (auto simp: ordinal_plus_assoc)

lemma subseq_from_cnf_less_eq: "Sublist.subseq ks ls ⟹ from_cnf ks ≤ from_cnf ls"
by (induct rule: list_emb.induct) (auto intro: ordinal_le_plusL order_trans)

subsection ‹Embedding of Syntactic Ordinals into Huffman's Ordinals›

abbreviation ω⇩h :: hmultiset where
"ω⇩h ≡ Syntactic_Ordinal.ω"

abbreviation ω⇩h_exp :: "hmultiset ⇒ hmultiset" ("ω⇩h^") where
"ω⇩h^ ≡ Syntactic_Ordinal.ω_exp"

primrec ordinal_of_hmset :: "hmultiset ⇒ ordinal" where
"ordinal_of_hmset (HMSet M) =
from_cnf (rev (sorted_list_of_multiset (image_mset ordinal_of_hmset M)))"

lemma ordinal_of_hmset_0[simp]: "ordinal_of_hmset 0 = 0"
unfolding zero_hmultiset_def by simp

lemma ordinal_of_hmset_suc[simp]: "ordinal_of_hmset (k + 1) = ordinal_of_hmset k + 1"
unfolding plus_hmultiset_def one_hmultiset_def by (cases k) simp

lemma ordinal_of_hmset_1[simp]: "ordinal_of_hmset 1 = 1"
using ordinal_of_hmset_suc[of 0] by simp

lemma ordinal_of_hmset_ω[simp]: "ordinal_of_hmset ω⇩h = ω"
by simp

lemma ordinal_of_hmset_singleton[simp]: "ordinal_of_hmset (ω^k) = ω ** ordinal_of_hmset k"
by simp

lemma ordinal_of_hmset_iff[simp]: "ordinal_of_hmset k = 0 ⟷ k = 0"
by (induct k) auto

lemma less_imp_ordinal_of_hmset_less: "k < l ⟹ ordinal_of_hmset k < ordinal_of_hmset l"
proof (simp only: atomize_imp,
rule measure_induct_rule[of "λ(k, l). {#k, l#}"
"λ(k, l). k < l ⟶ ordinal_of_hmset k < ordinal_of_hmset l" "(k, l)",
simplified prod.case],
simp only: split_paired_all prod.case atomize_imp[symmetric])
fix k l
assume
ih: "⋀ka la. {#ka, la#} < {#k, l#} ⟹ ka < la ⟹ ordinal_of_hmset ka < ordinal_of_hmset la" and
k_lt_l: "k < l"

show "ordinal_of_hmset k < ordinal_of_hmset l"
proof (cases "k = 0")
case True
thus ?thesis
using k_lt_l ordinal_neq_0 by fastforce
next
case k_nz: False

have l_nz: "l ≠ 0"
using k_lt_l by auto

define K where K: "K = hmsetmset k"
define L where L: "L = hmsetmset l"

have k: "k = HMSet K" and l: "l = HMSet L"

have K_lt_L: "K < L"
unfolding K L using k_lt_l by simp

define x where x: "x = Max_mset K"
define Ka where Ka: "Ka = K - {#x#}"

have k_eq_xKa: "k = HMSet (add_mset x Ka)"
using K x Ka k_nz by auto
have x_max: "∀a ∈# Ka. a ≤ x"
unfolding x Ka by (meson Max_ge finite_set_mset in_diffD)

have ord_x_max: "∀a ∈# Ka. ordinal_of_hmset a ≤ ordinal_of_hmset x"
proof
fix a
assume a_in: "a ∈# Ka"

have a_le_x: "a ≤ x"
moreover
{
assume a_lt_x: "a < x"
moreover have x_lt_k: "x < k"
unfolding k_eq_xKa by (rule mem_imp_less_HMSet) simp
ultimately have a_lt_k: "a < k"
by simp

have "{#a, x#} < {#k#}"
using x_lt_k a_lt_k by simp
also have "… < {#k, l#}"
unfolding k_eq_xKa using a_in
by simp
finally have "ordinal_of_hmset a < ordinal_of_hmset x"
by (rule ih[OF _ a_lt_x])
}
ultimately show "ordinal_of_hmset a ≤ ordinal_of_hmset x"
by force
qed

define y where y: "y = Max_mset L"
define La where La: "La = L - {#y#}"

have l_eq_yLa: "l = HMSet (add_mset y La)"
using L y La l_nz by auto
have y_max: "∀b ∈# La. b ≤ y"
unfolding y La by (meson Max_ge finite_set_mset in_diffD)

have ord_y_max: "∀b ∈# La. ordinal_of_hmset b ≤ ordinal_of_hmset y"
proof
fix b
assume b_in: "b ∈# La"

have b_le_y: "b ≤ y"
moreover
{
assume b_lt_y: "b < y"
moreover have y_lt_l: "y < l"
unfolding l_eq_yLa by (rule mem_imp_less_HMSet) simp
ultimately have b_lt_l: "b < l"
by simp

have "{#b, y#} < {#l#}"
using y_lt_l b_lt_l by simp
also have "… < {#k, l#}"
unfolding l_eq_yLa using b_in
by simp
finally have "ordinal_of_hmset b < ordinal_of_hmset y"
by (rule ih[OF _ b_lt_y])
}
ultimately show "ordinal_of_hmset b ≤ ordinal_of_hmset y"
by force
qed

{
assume x_eq_y: "x = y"

have "ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)"
proof (rule ih)
show "{#HMSet Ka, HMSet La#} < {#k, l#}"
unfolding k l
le_multiset_right_total mset_lt_single_iff union_less_mono)
next
have "ω^x + HMSet Ka < ω^y + HMSet La"
using k_lt_l[unfolded k_eq_xKa l_eq_yLa]
thus "HMSet Ka < HMSet La"
using x_eq_y by simp
qed
hence ?thesis
unfolding k_eq_xKa l_eq_yLa
by (simp, subst (1 2) sorted_insort_is_snoc, simp_all add: ord_x_max ord_y_max,
force simp: x_eq_y)
}
moreover
{
assume x_ne_y: "x ≠ y"

have x_lt_y: "x < y"
less_imp_not_less mset_lt_single_iff neqE x x_ne_y y)

have ord_y_smax_K: "ordinal_of_hmset a < ordinal_of_hmset y" if a_in_K: "a ∈# K" for a
proof (rule ih)
show "{#a, y#} < {#k, l#}"
unfolding k_eq_xKa l_eq_yLa using a_in_K k k_eq_xKa
union_single_eq_member)
next
show "a < y"
by (metis Max_ge finite_set_mset less_le_trans not_less_iff_gr_or_eq that x x_lt_y)
qed

have "ordinal_of_hmset k < ordinal_of_hmset (ω^y)"
proof (cases La)
case empty
show ?thesis
unfolding k by (auto intro!: from_cnf_less_ω_exp simp: ord_y_smax_K)
next
show "{#k, ω^y#}