# Theory Signed_Multiset

theory Signed_Multiset
imports Multiset_More
```(*  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 (clarsimp simp: equiv_zmset_def intro!: arg_cong[of _ _ count])

lift_definition mset_neg :: "'a zmultiset ⇒ 'a multiset" is "λ(Mp, Mn). count (Mn - Mp)"
by (clarsimp simp: equiv_zmset_def intro!: arg_cong[of _ _ count])

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
```