# Theory Multisets_Extras

```(* Title: Multisets_Extras
Author: Chelsea Edmonds
*)

section ‹Micellanious Helper Functions on Sets and Multisets›

theory Multisets_Extras imports
"HOL-Library.Multiset"
Card_Partitions.Set_Partition
Nested_Multisets_Ordinals.Multiset_More
Nested_Multisets_Ordinals.Duplicate_Free_Multiset
"HOL-Library.Disjoint_Sets"
begin

subsection ‹Set Theory Extras›

text ‹A number of extra helper lemmas for reasoning on sets (finite) required for Design Theory
proofs›

lemma card_Pow_filter_one:
assumes "finite A"
shows "card {x ∈ Pow A . card x = 1}  = card (A)"
using assms
proof (induct rule: finite_induct)
case empty
then show ?case by auto
next
case (insert x F)
have "Pow (insert x F) = Pow F ∪ insert x ` Pow F"
then have split: "{y ∈ Pow (insert x F) . card y = 1} =
{y ∈ (Pow F) . card y = 1} ∪ {y ∈ (insert x ` Pow F) . card y = 1}"
by blast
have "⋀ y . y ∈ (insert x ` Pow F) ⟹ finite y"
using finite_subset insert.hyps(1) by fastforce
then have single: "⋀ y . y ∈ (insert x ` Pow F) ⟹ card y = 1 ⟹ y = {x}"
by (metis card_1_singletonE empty_iff image_iff insertCI insertE)
then have "card {y ∈ (insert x ` Pow F) . card y = 1} = 1"
using empty_iff imageI is_singletonI is_singletonI' is_singleton_altdef (* LONG *)
by (metis (full_types, lifting) Collect_empty_eq_bot Pow_bottom bot_empty_eq  mem_Collect_eq)
then have " {y ∈ (insert x ` Pow F) . card y = 1} = {{x}}"
using single card_1_singletonE card_eq_0_iff
by (smt empty_Collect_eq mem_Collect_eq singletonD zero_neq_one)
then have split2:"{y ∈ Pow (insert x F) . card y = 1} = {y ∈ (Pow F) . card y = 1} ∪ {{x}}"
using split by simp
then show ?case
proof (cases "x ∈ F")
case True
then show ?thesis using insert.hyps(2) by auto
next
case False
then have "{y ∈ (Pow F) . card y = 1} ∩ {{x}} = {}" by blast
then have fact:"card {y ∈ Pow (insert x F) . card y = 1} =
card {y ∈ (Pow F) . card y = 1} + card {{x}}"
using split2 card_Un_disjoint insert.hyps(1) by auto
have "card (insert x F) = card F + 1"
using False card_insert_disjoint by (metis Suc_eq_plus1 insert.hyps(1))
then show ?thesis using fact insert.hyps(3) by auto
qed
qed

lemma elem_exists_non_empty_set:
assumes "card A > 0"
obtains x where "x ∈ A"
using assms card_gt_0_iff by fastforce

lemma set_self_img_compr: "{a | a . a ∈ A} = A"
by blast

lemma card_subset_not_gt_card: "finite A ⟹ card ps > card A ⟹ ¬ (ps ⊆ A)"
using card_mono leD by auto

lemma card_inter_lt_single: "finite A ⟹ finite B ⟹ card (A ∩ B) ≤ card A"

lemma set_diff_non_empty_not_subset:
assumes "A ⊆ (B - C)"
assumes "C ≠ {}"
assumes "A ≠ {}"
assumes "B ≠ {}"
shows " ¬ (A ⊆ C)"
proof (rule ccontr)
assume " ¬ ¬ (A ⊆ C)"
then have a: "⋀ x . x ∈ A ⟹ x ∈ C" by blast
thus False using a assms by blast
qed

lemma set_card_diff_ge_zero: "finite A ⟹ finite B ⟹ A ≠ B ⟹ card A = card B ⟹
card (A - B) > 0"
by (meson Diff_eq_empty_iff card_0_eq card_subset_eq finite_Diff neq0_conv)

lemma set_filter_diff: "{a ∈ A . P a } - {x} = {a ∈ (A - {x}) . (P a )}"
by (auto)

lemma set_filter_diff_card: "card ({a ∈ A . P a } - {x}) = card {a ∈ (A - {x}) . (P a )}"

lemma obtain_subset_with_card_int_n:
assumes "(n ::int) ≤ of_nat (card S)"
assumes "(n ::int) ≥ 0"
obtains T where "T ⊆ S" "of_nat (card T) = (n ::int)" "finite T"
using obtain_subset_with_card_n assms
by (metis nonneg_int_cases of_nat_le_iff)

lemma transform_filter_img_empty_rm:
assumes "⋀ g . g ∈ G ⟹ g ≠ {}"
shows "{g - {x} | g. g ∈ G ∧ g ≠ {x}} = {g - {x} | g. g ∈ G } - {{}}"
proof -
let ?f = "λ g . g - {x}"
have "⋀ g . g ∈ G ⟹ g ≠ {x} ⟷ ?f g ≠ {}" using assms
by (metis Diff_cancel Diff_empty Diff_insert0 insert_Diff)
thus ?thesis by auto
qed

lemma bij_betw_inter_subsets: "bij_betw f A B ⟹ a1 ⊆ A ⟹ a2 ⊆ A
⟹ f ` (a1 ∩ a2) = (f ` a1) ∩ (f ` a2)"
by (meson bij_betw_imp_inj_on inj_on_image_Int)

text‹Partition related set theory lemmas›

lemma partition_on_remove_pt:
assumes "partition_on A G"
shows "partition_on (A - {x}) {g - {x} | g. g ∈ G ∧ g ≠ {x}}"
proof (intro partition_onI)
show "⋀p. p ∈ {g - {x} |g. g ∈ G ∧ g ≠ {x}} ⟹ p ≠ {}"
using assms partition_onD3 subset_singletonD by force
let ?f =  "(λ g . g - {x})"
have un_img: "⋃({?f g | g. g ∈ G }) = ?f (⋃ G)" by blast
have empty: "⋃ {g - {x} |g. g ∈ G ∧ g ≠ {x}} = ⋃({g - {x} | g. g ∈ G } - {{}})"
by blast
then have "⋃({g - {x} | g. g ∈ G } - {{}}) = ⋃({g - {x} | g. g ∈ G })" by blast
then show " ⋃ {g - {x} |g. g ∈ G ∧ g ≠ {x}} = A - {x}" using partition_onD1 assms un_img
by (metis empty)
then show "⋀p p'.
p ∈ {g - {x} |g. g ∈ G ∧ g ≠ {x}} ⟹
p' ∈ {g - {x} |g. g ∈ G ∧ g ≠ {x}} ⟹ p ≠ p' ⟹ p ∩ p' = {}"
proof -
fix p1 p2
assume p1: "p1 ∈ {g - {x} |g. g ∈ G ∧ g ≠ {x}}"
and p2: "p2 ∈ {g - {x} |g. g ∈ G ∧ g ≠ {x}}"
and ne: "p1 ≠ p2"
obtain p1' p2' where orig1: "p1 = p1' - {x}" and orig2: "p2 = p2' - {x}"
and origne: "p1' ≠ p2'" and ne1: "p1' ≠ {x}" and ne2:"p2' ≠ {x}" and ing1: "p1' ∈ G"
and ing2: "p2' ∈ G"
using p1 p2 using mem_Collect_eq ne by blast
then have "p1' ∩ p2' = {}" using assms partition_onD2 ing1 ing2 origne disjointD by blast
thus "p1 ∩ p2 = {}" using orig1 orig2 by blast
qed
qed

lemma partition_on_cart_prod:
assumes "card I > 0"
assumes "A ≠ {}"
assumes "G ≠ {}"
assumes "partition_on A G"
shows "partition_on (A × I) {g × I |g. g ∈ G}"
proof (intro partition_onI)
show "⋀p. p ∈ {g × I |g. g ∈ G} ⟹ p ≠ {}"
using assms(1) assms(4) partition_onD3 by fastforce
show "⋃ {g × I |g. g ∈ G} = A × I"
by (metis Setcompr_eq_image Sigma_Union assms(4) partition_onD1)
show "⋀p p'. p ∈ {g × I |g. g ∈ G} ⟹ p' ∈ {g × I |g. g ∈ G} ⟹ p ≠ p' ⟹ p ∩ p' = {}"
by (smt (verit, best) Sigma_Int_distrib1 Sigma_empty1 assms(4) mem_Collect_eq partition_onE)
qed

subsection ‹Multiset Helpers›

text ‹Generic Size, count and card helpers›

lemma count_size_set_repr: "size {# x ∈# A . x = g#} = count A g"

lemma mset_nempty_set_nempty: "A ≠ {#} ⟷ (set_mset A) ≠ {}"
by simp

lemma mset_size_ne0_set_card: "size A > 0 ⟹ card (set_mset A) > 0"
using mset_nempty_set_nempty by fastforce

lemma set_count_size_min: "count A a ≥ n ⟹ size A ≥ n"
by (metis (full_types) count_le_replicate_mset_subset_eq size_mset_mono size_replicate_mset)

lemma card_size_filter_eq: "finite A ⟹  card {a ∈ A . P a} = size {#a ∈# mset_set A . P a#}"
by simp

lemma size_multiset_set_mset_const_count:
assumes "card (set_mset A) = ca"
assumes "⋀p. p ∈# A ⟹ count A p = ca2"
shows "size A =  (ca * ca2)"
proof -
have "size A = (∑ p ∈ (set_mset A) . count A p)" using size_multiset_overloaded_eq by auto
then have "size A = (∑ p ∈ (set_mset A) . ca2)" using assms by simp
thus ?thesis using assms(1) by auto
qed

lemma size_multiset_int_count:
assumes "of_nat (card (set_mset A)) = (ca :: int)"
assumes "⋀p. p ∈# A ⟹ of_nat (count A p) = (ca2 :: int)"
shows "of_nat (size A) =  ((ca :: int) * ca2)"
proof -
have "size A = (∑ p ∈ (set_mset A) . count A p)" using size_multiset_overloaded_eq by auto
then have "of_nat (size A) = (∑ p ∈ (set_mset A) . ca2)" using assms by simp
thus ?thesis using assms(1) by auto
qed

lemma mset_union_size: "size (A ∪# B) = size (A) + size (B - A)"

lemma mset_union_size_inter: "size (A ∪# B) = size (A) + size B - size (A ∩# B)"

text ‹Lemmas for repeat\_mset›

lemma repeat_mset_size [simp]: "size (repeat_mset n A) = n * size A"
by (induction n) auto

lemma repeat_mset_subset_in:
assumes "⋀ a . a ∈# A ⟹ a ⊆ B"
assumes "X ∈# repeat_mset n A"
assumes "x ∈ X"
shows " x ∈ B"
using assms by (induction n) auto

lemma repeat_mset_not_empty: "n > 0 ⟹ A ≠ {#} ⟹ repeat_mset n A ≠ {#}"
by (induction n) auto

lemma elem_in_repeat_in_original: "a ∈# repeat_mset n A ⟹ a ∈# A"
by (metis count_inI count_repeat_mset in_countE mult.commute mult_zero_left nat.distinct(1))

lemma elem_in_original_in_repeat: "n > 0 ⟹ a ∈# A ⟹ a ∈# repeat_mset n A"
by (metis count_greater_zero_iff count_repeat_mset nat_0_less_mult_iff)

text ‹Lemmas on image and filter for multisets›

lemma multiset_add_filter_size: "size {# a ∈# (A1 + A2) . P a #} = size {# a ∈# A1 . P a #} +
size {# a ∈# A2 . P a #}"
by simp

lemma size_filter_neg: "size {#a ∈# A . P a #} = size A - size {# a ∈# A . ¬ P a #}"
using size_filter_mset_lesseq size_union union_filter_mset_complement

lemma filter_filter_mset_cond_simp:
assumes "⋀ a . P a ⟹ Q a"
shows "filter_mset P A = filter_mset P (filter_mset Q A)"
proof -
have "filter_mset P (filter_mset Q A) = filter_mset (λ a. Q a ∧ P a) A"
thus ?thesis using assms
by (metis (mono_tags, lifting) filter_mset_cong)
qed

lemma filter_filter_mset_ss_member: "filter_mset (λ a . {x, y} ⊆ a) A =
filter_mset (λ a . {x, y} ⊆ a) (filter_mset (λ a . x ∈ a) A)"
proof -
have filter: "filter_mset (λ a . {x, y} ⊆ a) (filter_mset (λ a . x ∈ a) A) =
filter_mset (λ a . x ∈ a ∧ {x, y} ⊆ a) A" by (simp add: filter_filter_mset)
have "⋀ a. {x, y} ⊆ a ⟹ x ∈ a" by simp
thus ?thesis using filter by auto
qed

lemma multiset_image_do_nothing: "(⋀ x .x ∈# A ⟹ f x = x) ⟹ image_mset f A = A"
by (induct A) auto

lemma set_mset_filter: "set_mset {# f a . a ∈# A #} = {f a | a. a ∈# A}"

lemma mset_exists_imply: "x ∈# {# f a . a ∈# A #} ⟹ ∃ y ∈# A . x = f y"
by auto

lemma filter_mset_image_mset:
"filter_mset P (image_mset f A) = image_mset f (filter_mset (λx. P (f x)) A)"
by (induction A) auto

lemma mset_bunion_filter: "{# a ∈# A . P a ∨ Q a #} = {# a ∈# A . P a #} ∪# {# a ∈# A . Q a #}"
by (rule multiset_eqI) simp

lemma mset_inter_filter: "{# a ∈# A . P a ∧ Q a #} = {# a ∈# A . P a #} ∩# {# a ∈# A . Q a #}"
by (rule multiset_eqI) simp

lemma image_image_mset: "image_mset (λ x . f x) (image_mset (λ y . g y) A) =
image_mset (λ x. f (g x)) A"
by simp

text ‹Big Union over multiset helpers›

lemma mset_big_union_obtain:
assumes "x ∈# ∑⇩# A"
obtains a where "a ∈# A" and "x ∈# a"
using assms by blast

lemma size_big_union_sum: "size (∑⇩# (M :: 'a multiset multiset)) = (∑x ∈#M . size x)"
by (induct M) auto

text ‹Cartesian Product on Multisets›

lemma size_cartesian_product_singleton [simp]: "size ({#a#} ×# B) = size B"

lemma size_cartesian_product_singleton_right [simp]: "size (A ×# {#b#}) = size A"

lemma size_cartesian_product_empty [simp]: "size (A ×# {#}) = 0"
by simp

assumes "size (A ×# B) = size A * size B"
shows "size (add_mset x A ×# B) = size (add_mset x A) * size B"
proof -
have "(add_mset x A ×# B) = A ×# B + {#x#} ×# B"
then have "size (add_mset x A ×# B) = size (A ×# B) + size B" by auto
also have "... = size A * size B + size B"
finally have "size (add_mset x A ×# B) = (size A + 1) * size B"
by auto
thus ?thesis by simp
qed

lemma size_cartesian_product: "size (A ×# B) = size A * size B"

lemma cart_prod_distinct_mset:
assumes assm1: "distinct_mset A"
assumes assm2: "distinct_mset B"
shows "distinct_mset (A ×# B)"
unfolding distinct_mset_count_less_1
proof (rule allI)
fix x
have count_mult: "count (A ×# B) x = count A (fst x) * count B (snd x)"
using count_Sigma_mset by (metis prod.exhaust_sel)
then have "count A (fst x) * count B (snd x) ≤ 1" using assm1 assm2
unfolding distinct_mset_count_less_1 using mult_le_one by blast
thus "count (A ×# B) x ≤ 1" using count_mult by simp
qed

lemma cart_product_single_intersect: "x1 ≠ x2 ⟹ ({#x1#} ×# A) ∩# ({#x2#} ×# B) = {#}"
using multiset_inter_single by fastforce

lemma size_union_distinct_cart_prod: "x1 ≠ x2 ⟹ size (({#x1#} ×# A) ∪# ({#x2#} ×# B)) =
size ({#x1#} ×# A) + size ({#x2#} ×# B)"

lemma size_Union_distinct_cart_prod: "distinct_mset M ⟹
size (∑p∈#M. ({#p#} ×# B)) = size (M) * size (B)"
by (induction M) auto

lemma size_Union_distinct_cart_prod_filter: "distinct_mset M ⟹
(⋀ p . p ∈# M ⟹ size ({# b ∈# B . P p b #}) = c) ⟹
size (∑p∈#M. ({#p#} ×# {# b ∈# B . P p b #})) = size (M) * c"
by (induction M) auto

lemma size_Union_distinct_cart_prod_filter2: "distinct_mset V ⟹
(⋀ b . b ∈# B ⟹ size ({# v ∈# V . P v b #}) = c) ⟹
size (∑b∈#B. ( {# v ∈# V . P v b #} ×# {#b#})) = size (B) * c"
by (induction B) auto

lemma cart_product_add_1: "(add_mset a A) ×# B = ({#a#} ×# B) + (A ×# B)"

lemma cart_product_add_1_filter: "{#m ∈# ((add_mset a M) ×# N) . P m #} =
{#m ∈# (M ×# N) . P m #} + {#m ∈# ({#a#} ×#  N) . P m #}"

lemma cart_product_add_1_filter2: "{#m ∈# (M ×# (add_mset b N)) . P m #} =
{#m ∈# (M ×# N) . P m #} + {#m ∈# (M ×#  {#b#}) . P m #}"

lemma cart_prod_singleton_right_gen:
assumes "⋀ x . x ∈# (A ×# {#b#}) ⟹ P x ⟷ Q (fst x)"
shows "{#x ∈# (A ×# {#b#}). P x#} = {# a ∈# A . Q a#} ×# {#b#}"
using assms
proof (induction A)
case empty
then show ?case by simp
next
have "add_mset x A ×# {#b#} = add_mset (x, b) (A ×# {#b#})"
then have lhs: "filter_mset P (add_mset x A ×# {#b#}) = filter_mset P (A ×# {#b#}) +
filter_mset P {#(x, b)#}" by simp
have rhs: "filter_mset Q (add_mset x A) ×# {#b#} = filter_mset Q A ×# {#b#} +
filter_mset Q {#x#} ×# {#b#}"
have "filter_mset P {#(x, b)#} = filter_mset Q {#x#} ×# {#b#}"
qed

lemma cart_prod_singleton_left_gen:
assumes "⋀ x . x ∈# ({#a#} ×# B) ⟹ P x ⟷ Q (snd x)"
shows "{#x ∈# ({#a#} ×# B). P x#} = {#a#} ×# {#b ∈# B . Q b#}"
using assms
proof (induction B)
case empty
then show ?case by simp
next
have lhs: "filter_mset P ({#a#} ×# add_mset x B) = filter_mset P ({#a#} ×# B) +
filter_mset P {#(a, x)#}"
have rhs: "{#a#} ×# filter_mset Q (add_mset x B) = {#a#} ×# filter_mset Q B +
{#a#} ×# filter_mset Q {#x#}"
have "filter_mset P {#(a, x)#} = {#a#} ×# filter_mset Q {#x#}"
qed

lemma cart_product_singleton_left: "{#m ∈# ({#a#} ×#  N) . fst m ∈ snd m #} =
({#a#} ×# {# n ∈# N . a ∈ n #})" (is "?A = ?B")
proof -
have stmt: "⋀m. m ∈# ({#a#} ×# N) ⟹ fst m ∈ snd m ⟷ a ∈ snd m"
thus ?thesis by (metis (no_types, lifting) Sigma_mset_cong stmt cart_prod_singleton_left_gen)
qed

lemma cart_product_singleton_right: "{#m ∈# (N ×# {#b#}) . fst m ∈ snd m #} =
({# n ∈# N . n ∈ b #} ×# {# b #})" (is "?A = ?B")
proof -
have stmt: "⋀m. m ∈# (N ×# {#b#}) ⟹ fst m ∈ snd m ⟷ fst m ∈b"
thus ?thesis by (metis (no_types, lifting) Sigma_mset_cong stmt cart_prod_singleton_right_gen)
qed

lemma cart_product_add_1_filter_eq: "{#m ∈# ((add_mset a M) ×# N) . (fst m ∈ snd m) #} =
{#m ∈# (M ×# N) . (fst m ∈ snd m) #} + ({#a#} ×# {# n ∈# N . a ∈ n #})"

lemma cart_product_add_1_filter_eq_mirror: "{#m ∈# M ×# (add_mset b N) . (fst m ∈ snd m) #} =
{#m ∈# (M ×# N) . (fst m ∈ snd m) #} + ({# n ∈# M . n ∈ b #} ×# {#b#})"

lemma set_break_down_left:
shows "{# m ∈# (M ×# N) . (fst m) ∈ (snd m)  #} = (∑m∈#M. ({#m#} ×# {#n ∈# N. m ∈ n#}))"

lemma set_break_down_right:
shows "{# x ∈# M ×# N . (fst x) ∈ (snd x)  #} = (∑n∈#N. ({#m ∈# M. m ∈ n#} ×# {#n#}))"

text ‹Reasoning on sums of elements over multisets›

lemma sum_over_fun_eq:
assumes "⋀ x . x ∈# A ⟹ f x = g x"
shows "(∑x ∈# A . f(x)) = (∑ x ∈# A . g (x))"
using assms by auto

fixes x:: 'a and  f g :: "'a ⇒ nat"
assumes "⋀x . x ∈# A ⟹ f x ≥ g x"
shows "(∑ x ∈# A. f x - g x) = (∑ x ∈# A . f x) -  (∑ x ∈# A . g x)"
using assms by (induction A) (simp_all add: sum_mset_mono)

fixes x:: 'a and  f g :: "'a ⇒ int"
shows "(∑ x ∈# A. f x - g x) = (∑ x ∈# A . f x) -  (∑ x ∈# A . g x)"
by (induction A) (simp_all add: sum_mset_mono)

context ring_1
begin

lemma sum_mset_add_diff: "(∑ x ∈# A. f x - g x) = (∑ x ∈# A . f x) -  (∑ x ∈# A . g x)"
by (induction A) (auto simp add: algebra_simps)

end

context ordered_semiring
begin

lemma sum_mset_ge0:"(⋀ x . f x ≥ 0) ⟹ (∑ x ∈# A. f x ) ≥ 0"
proof (induction A)
case empty
then show ?case by simp
next
then have hyp2: "0 ≤ sum_mset (image_mset f A)" by blast
then have " sum_mset (image_mset f (add_mset x A)) =  sum_mset (image_mset f  A) + f x"
then show ?case
qed

lemma sum_order_add_mset: "(⋀ x . f x ≥ 0) ⟹ (∑ x ∈# A. f x ) ≤ (∑ x ∈# add_mset a A. f x )"

lemma sum_mset_0_left: "(⋀ x . f x ≥ 0) ⟹ (∑ x ∈# A. f x ) = 0 ⟹ (∀ x ∈# A .f x = 0)"
apply (induction A)
apply auto

lemma sum_mset_0_iff_ge_0:
assumes "(⋀ x . f x ≥ 0)"
shows "(∑ x ∈# A. f x ) = 0 ⟷ (∀ x ∈ set_mset A .f x = 0)"
using sum_mset_0_left assms by auto

end

lemma mset_set_size_card_count: "(∑x ∈# A. x) = (∑x ∈ set_mset A . x * (count A x))"
proof (induction A)
case empty
then show ?case by simp
next
have lhs: "(∑x∈#add_mset y A. x) = (∑x∈# A. x) + y" by simp
have rhs: "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
(∑x∈(insert y (set_mset A)) . x * count (add_mset y A) x)"
by simp
then show ?case
proof (cases "y ∈# A")
case True
have x_val: "⋀ x . x ∈ (insert y (set_mset A)) ⟹ x ≠ y ⟹
x* count (add_mset y A) x = x * (count A x)"
by auto
have y_count: "count (add_mset y A) y = 1 + count A y"
using True count_inI by fastforce
then have "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
(y * (count (add_mset y A) y)) + (∑x∈(set_mset A) - {y}. x * count A x)"
using x_val finite_set_mset sum.cong sum.insert rhs
by (smt DiffD1 Diff_insert_absorb insert_absorb mk_disjoint_insert sum.insert_remove)
then have s1: "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
y + y * (count A y) + (∑x∈(set_mset A) - {y}. x * count A x)"
using y_count by simp
then have "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
y + (∑x∈insert y ((set_mset A) - {y} ) . x * count A x)"
then have "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
y + (∑x∈(set_mset A) . x * count A x)"
then show ?thesis using lhs add.IH
by linarith
next
case False
have x_val: "⋀ x . x ∈ set_mset A ⟹ x* count (add_mset y A) x = x * (count A x)"
using False by auto
have y_count: "count (add_mset y A) y = 1" using False count_inI by fastforce
have lhs: "(∑x∈#add_mset y A. x) = (∑x∈# A. x) + y" by simp
have "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
(y * count (add_mset y A) y) + (∑x∈set_mset A. x * count A x)"
using x_val rhs by (metis (no_types, lifting) False finite_set_mset sum.cong sum.insert)
then have "(∑x∈set_mset (add_mset y A). x * count (add_mset y A) x) =
y + (∑x∈set_mset A. x * count A x)"
using y_count by simp
then show ?thesis using lhs add.IH by linarith
qed
qed

subsection ‹Partitions on Multisets›

text ‹A partition on a multiset A is a multiset of multisets, where the sum over P equals A and the
empty multiset is not in the partition. Based off set partition definition.
We note that unlike set partitions, there is no requirement for elements in the multisets to be
distinct due to the definition of union on multisets \<^cite>‹"benderPartitionsMultisets1974"››

lemma mset_size_partition_dep: "size {# a ∈# A . P a ∨ Q a #} =
size {# a ∈# A . P a #} +  size {# a ∈# A . Q a #} -  size {# a ∈# A . P a ∧ Q a #}"
by (simp add: mset_bunion_filter mset_inter_filter mset_union_size_inter)

definition partition_on_mset :: "'a multiset ⇒ 'a multiset multiset ⇒ bool" where
"partition_on_mset A P ⟷ ∑⇩#P = A ∧ {#} ∉# P"

lemma partition_on_msetI [intro]: "∑⇩#P = A ⟹ {#} ∉# P ⟹ partition_on_mset A P"

lemma partition_on_msetD1: "partition_on_mset A P ⟹ ∑⇩#P = A"

lemma partition_on_msetD2: "partition_on_mset A P ⟹ {#} ∉#  P"

lemma partition_on_mset_empty: "partition_on_mset {#} P ⟷ P = {#}"
unfolding partition_on_mset_def
using multiset_nonemptyE by fastforce

lemma partition_on_mset_all: "A ≠ {#} ⟹ partition_on_mset A {#A #}"

lemma partition_on_mset_singletons: "partition_on_mset A (image_mset (λ x . {#x#}) A)"
by (auto simp: partition_on_mset_def)

lemma partition_on_mset_not_empty: "A ≠ {#} ⟹ partition_on_mset A P ⟹ P ≠ {#}"
by (auto simp: partition_on_mset_def)

lemma partition_on_msetI2: "∑⇩#P = A ⟹ (⋀ p . p ∈# P ⟹ p ≠ {#}) ⟹ partition_on_mset A P"
by (auto simp: partition_on_mset_def)

lemma partition_on_mset_elems: "partition_on_mset A P ⟹ p1 ∈# P ⟹ x ∈# p1 ⟹ x ∈# A"
by (auto simp: partition_on_mset_def)

lemma partition_on_mset_sum_size_eq: "partition_on_mset A P ⟹ (∑x ∈# P. size x) = size A"
by (metis partition_on_msetD1 size_big_union_sum)

lemma partition_on_mset_card: assumes "partition_on_mset A P" shows " size P ≤ size A"
proof (rule ccontr)
assume "¬ size P ≤ size A"
then have a: "size P > size A" by simp
have "⋀ x . x ∈# P ⟹ size x > 0" using partition_on_msetD2
using assms nonempty_has_size by auto
then have " (∑x ∈# P. size x) ≥ size P"
by (metis leI less_one not_less_zero size_eq_sum_mset sum_mset_mono)
thus False using a partition_on_mset_sum_size_eq
using assms by fastforce
qed

lemma partition_on_mset_count_eq: "partition_on_mset A P ⟹ a ∈# A ⟹
(∑x ∈# P. count x a) = count A a"
by (metis count_sum_mset partition_on_msetD1)

lemma partition_on_mset_subsets: "partition_on_mset A P ⟹ x ∈# P ⟹ x ⊆# A"

lemma partition_on_mset_distinct:
assumes "partition_on_mset A P"
assumes "distinct_mset A"
shows "distinct_mset P"
proof (rule ccontr)
assume "¬ distinct_mset P"
then obtain p1 where count: "count P p1 ≥ 2"
by (metis Suc_1 distinct_mset_count_less_1 less_Suc_eq_le not_less_eq)
then have cge: "⋀ x . x ∈# p1 ⟹ (∑p ∈# P. count p x ) ≥ 2"
by (smt count_greater_eq_one_iff count_sum_mset_if_1_0 dual_order.trans sum_mset_mono zero_le)
have elem_in: "⋀ x . x ∈# p1 ⟹ x ∈# A" using partition_on_mset_elems
by (metis count assms(1) count_eq_zero_iff not_numeral_le_zero)
have "⋀ x . x ∈# A ⟹ count A x = 1" using assms
thus False
using assms partition_on_mset_count_eq cge elem_in count_inI local.count multiset_nonemptyE
by (metis (mono_tags) not_numeral_le_zero numeral_One numeral_le_iff partition_on_mset_def semiring_norm(69))
qed

lemma partition_on_mset_distinct_disjoint:
assumes "partition_on_mset A P"
assumes "distinct_mset A"
assumes "p1 ∈# P"
assumes "p2 ∈# P - {#p1#}"
shows "p1 ∩# p2 = {#}"
by (smt partition_on_msetD1 subset_mset.inf.absorb_iff2 subset_mset.le_add_same_cancel1 subset_mset.le_iff_inf)

lemma partition_on_mset_diff:
assumes "partition_on_mset A P"
assumes "Q ⊆#P"
shows "partition_on_mset (A - ∑⇩#Q) (P - Q)"
using assms partition_on_mset_def
by (smt diff_union_cancelL subset_mset.add_diff_inverse sum_mset.union union_iff)

lemma sigma_over_set_partition_count:
assumes "finite A"
assumes "partition_on A P"
assumes "x ∈# ∑⇩# (mset_set (mset_set ` P))"
shows "count (∑⇩# (mset_set (mset_set ` P))) x = 1"
proof -
have disj: "disjoint P" using assms partition_onD2 by auto
then obtain p where  pin: "p ∈# mset_set (mset_set ` P)" and xin: "x ∈# p"
using assms by blast
then have "count (mset_set (mset_set ` P)) p = 1"
by (meson count_eq_zero_iff count_mset_set')
then have filter: "⋀ p' . p' ∈# ((mset_set (mset_set` P)) - {#p#}) ⟹ p ≠ p'"
using count_eq_zero_iff count_single by fastforce
have zero: "⋀ p'. p' ∈# mset_set (mset_set ` P) ⟹ p' ≠ p ⟹ count p' x = 0"
proof (rule ccontr)
fix p'
assume assm: "p' ∈# mset_set (mset_set ` P)" and ne: "p' ≠ p"  and n0: "count p' x ≠ 0"
then have xin2: "x ∈# p'"  by auto
obtain p1 p2 where p1in: "p1 ∈ P" and p2in: "p2 ∈ P" and  p1eq: "mset_set p1 = p"
and p2eq: "mset_set p2 = p'" using assm assms(1) assms(2) pin
by (metis (no_types, lifting) elem_mset_set finite_elements finite_imageI image_iff)
have origne: "p1 ≠ p2" using ne p1eq p2eq by auto
have "p1 = p2" using partition_onD4 xin xin2
by (metis assms(2) count_eq_zero_iff count_mset_set' p1eq p1in p2eq p2in)
then show False using origne by simp
qed
have one: "count p x = 1" using pin xin assms count_eq_zero_iff count_greater_eq_one_iff
by (metis count_mset_set(3) count_mset_set_le_one image_iff le_antisym)
then have "count (∑⇩# (mset_set (mset_set ` P))) x =
(∑p' ∈# (mset_set (mset_set ` P)) . count p' x)"
using count_sum_mset by auto
also have "... = (count p x) + (∑p' ∈# ((mset_set (mset_set ` P)) - {#p#}) . count p' x)"
by (metis (mono_tags, lifting) insert_DiffM pin sum_mset.insert)
also have "... = 1 + (∑p' ∈# ((mset_set (mset_set ` P)) - {#p#}) . count p' x)"
using one by presburger
finally have "count (∑⇩# (mset_set (mset_set ` P))) x =
1 + (∑p' ∈# ((mset_set (mset_set ` P)) - {#p#}) . 0)"
using zero filter by (metis (mono_tags, lifting) in_diffD sum_over_fun_eq)
then show "count (∑⇩# (mset_set (mset_set ` P))) x = 1" by simp
qed

lemma partition_on_mset_set:
assumes "finite A"
assumes "partition_on A P"
shows "partition_on_mset (mset_set A) (mset_set (image (λ x. mset_set x) P))"
proof (intro partition_on_msetI)
have partd1: "⋃P = A" using assms partition_onD1 by auto
have imp: "⋀x. x ∈# ∑⇩# (mset_set (mset_set ` P)) ⟹ x ∈# mset_set A"
proof -
fix x
assume "x ∈# ∑⇩# (mset_set (mset_set ` P))"
then obtain p where "p ∈ (mset_set ` P)" and xin: "x ∈# p"
by (metis elem_mset_set equals0D infinite_set_mset_mset_set mset_big_union_obtain)
then have "set_mset p ∈ P"
by (metis empty_iff finite_set_mset_mset_set image_iff infinite_set_mset_mset_set)
then show "x ∈# mset_set A"
using partd1 xin assms(1) by auto
qed
have imp2: "⋀x . x ∈# mset_set A ⟹ x ∈# ∑⇩# (mset_set (mset_set ` P))"
proof -
fix x
assume "x ∈# mset_set A"
then have "x ∈ A" by (simp add: assms(1))
then obtain p where "p ∈ P" and "x ∈ p" using assms(2) using partd1 by blast
then obtain p' where "p' ∈ (mset_set ` P)" and "p' = mset_set p" by blast
thus "x ∈# ∑⇩# (mset_set (mset_set ` P))" using assms ‹p ∈ P› ‹x ∈ p› finite_elements partd1
by (metis Sup_upper finite_imageI finite_set_mset_mset_set in_Union_mset_iff rev_finite_subset)
qed
have a1: "⋀ x . x ∈# mset_set A ⟹ count (mset_set A) x = 1"
using assms(1) by fastforce
then show "∑⇩# (mset_set (mset_set ` P)) = mset_set A"  using imp imp2 a1
by (metis assms(1) assms(2) count_eq_zero_iff multiset_eqI sigma_over_set_partition_count)
have "⋀ p. p ∈ P ⟹  p ≠ {} " using assms partition_onD3 by auto
then have "⋀ p. p ∈ P ⟹  mset_set p ≠ {#}" using mset_set_empty_iff
by (metis Union_upper assms(1) partd1 rev_finite_subset)
then show "{#} ∉# mset_set (mset_set ` P)"
by (metis elem_mset_set equals0D image_iff infinite_set_mset_mset_set)
qed

lemma partition_on_mset_distinct_inter:
assumes "partition_on_mset A P"
assumes "distinct_mset A"
assumes "p1 ∈# P" and "p2 ∈# P" and "p1 ≠ p2"
shows "p1 ∩# p2 = {#}"
by (metis assms in_remove1_mset_neq partition_on_mset_distinct_disjoint)

lemma partition_on_set_mset_distinct:
assumes "partition_on_mset A P"
assumes "distinct_mset A"
assumes "p ∈# image_mset set_mset P"
assumes "p' ∈# image_mset set_mset P"
assumes "p ≠ p'"
shows "p ∩ p' = {}"
proof -
obtain p1 where p1in: "p1 ∈# P" and p1eq: "set_mset p1 = p" using assms(3)
by blast
obtain p2 where p2in: "p2 ∈# P" and p2eq: "set_mset p2 = p'" using assms(4) by blast
have "distinct_mset P" using assms partition_on_mset_distinct by blast
then have "p1 ≠ p2" using assms using p1eq p2eq by fastforce
then have "p1 ∩# p2 = {#}" using partition_on_mset_distinct_inter
using assms(1) assms(2) p1in p2in by auto
thus ?thesis using p1eq p2eq
by (metis set_mset_empty set_mset_inter)
qed

lemma partition_on_set_mset:
assumes "partition_on_mset A P"
assumes "distinct_mset A"
shows "partition_on (set_mset A) (set_mset (image_mset set_mset P))"
proof (intro partition_onI)
show "⋀p. p ∈# image_mset set_mset P ⟹ p ≠ {}"
using assms(1) partition_on_msetD2 by fastforce
next
have "⋀ x . x ∈ set_mset A ⟹ x ∈ ⋃ (set_mset (image_mset set_mset P))"
by (metis Union_iff assms(1) image_eqI mset_big_union_obtain partition_on_msetD1 set_image_mset)
then show "⋃ (set_mset (image_mset set_mset P)) = set_mset A"
using set_eqI' partition_on_mset_elems assms by auto
show "⋀p p'. p ∈# image_mset set_mset P ⟹ p' ∈# image_mset set_mset P ⟹
p ≠ p' ⟹ p ∩ p' = {}"
using partition_on_set_mset_distinct assms by blast
qed

lemma partition_on_mset_eq_imp_eq_carrier:
assumes "partition_on_mset A P"
assumes "partition_on_mset B P"
shows "A = B"
using assms partition_on_msetD1 by auto

assumes "partition_on_mset A P"
using assms by (auto simp: partition_on_mset_def)

assumes "partition_on_mset A P"
assumes "X ≠ {#}"
assumes "A + X = A'"
shows "partition_on_mset A' (add_mset X P)"
using assms by (auto simp: partition_on_mset_def)

assumes "partition_on_mset A P"
assumes "X ∈# P"
assumes "add_mset a X = X'"

lemma partition_on_mset_elem_exists_part:
assumes "partition_on_mset A P"
assumes "x ∈# A"
obtains p where "p ∈# P" and "x ∈# p"
using assms in_Union_mset_iff partition_on_msetD2 partition_on_msetI
by (metis partition_on_mset_eq_imp_eq_carrier)

lemma partition_on_mset_combine:
assumes "partition_on_mset A P"
assumes "partition_on_mset B Q"
shows "partition_on_mset (A + B) (P + Q)"
unfolding partition_on_mset_def
using assms partition_on_msetD1 partition_on_msetD2 by auto

lemma partition_on_mset_split:
assumes "partition_on_mset A (P + Q)"
shows "partition_on_mset (∑⇩#P) P"
using  partition_on_mset_def partition_on_msetD2 assms by fastforce
end```