# Theory Set_Multiset_Extras

```(* Title: Set_Multiset_Extras.thy
Author: Chelsea Edmonds
*)

section ‹Micellaneous Multset/Set Extras ›

theory Set_Multiset_Extras imports Design_Theory.Multisets_Extras "HOL-Combinatorics.Multiset_Permutations"
begin

subsection ‹ Set extras ›
text ‹ Minor set extras on cardinality and filtering ›
lemma equal_card_inter_fin_eq_sets: "finite A ⟹ finite B ⟹ card A = card B ⟹
card (A ∩ B) = card A ⟹ A = B"
by (metis Int_lower1 Int_lower2 card_subset_eq)

lemma insert_filter_set_true: "P x ⟹ {a ∈ (insert x A) . P a} = insert x {a ∈ A . P a}"
by auto

lemma insert_filter_set_false: "¬ P x ⟹ {a ∈ (insert x A) . P a} = {a ∈ A . P a}"
by auto

subsection ‹Multiset Extras ›
text ‹ Minor multiset extras on size and element reasoning ›

lemma obtain_two_items_mset:
assumes "size A > 1"
obtains x y where "x ∈# A" and "y ∈# A - {#x#}"
proof -
obtain x where "x ∈# A"
by (metis assms gr_implies_not_zero multiset_nonemptyE size_empty)
have "size (A - {#x#}) > 0"
by (metis ‹x ∈# A› assms insert_DiffM less_irrefl_nat nonempty_has_size size_single)
then obtain bl2 where "bl2 ∈# A - {#x#}"
by (metis less_not_refl multiset_nonemptyE size_empty)
thus ?thesis
using ‹x ∈# A› that by blast
qed

lemma obtain_two_items_mset_filter:
assumes "size {#a ∈# A . P a #} > 1"
obtains x y where "x ∈# A" and "y ∈# A - {#x#}" and "P x" and "P y"
proof -
obtain x y where xin: "x ∈# {#a ∈# A . P a #}" and yin: "y ∈# {#a ∈# A . P a #} - {#x#}"
using obtain_two_items_mset assms by blast
then have xdets: "x ∈# A" "P x" by auto
then have yin2: "y ∈# {#a ∈# (A - {#x#}) . P a #}" using yin
by force
then have "y ∈# (A - {#x#})" "P y"
by (metis multiset_partition union_iff) (meson yin2 filter_mset_eq_conv)
thus ?thesis using xdets that by blast
qed

lemma size_count_mset_ss:
assumes "finite B"
assumes "(set_mset A) ⊆ B"
shows "size A = (∑ x ∈ B . count A x)"
proof -
obtain C where cdef: "B - (set_mset A) = C" using assms
by simp
have fin: "finite (set_mset A)" using assms by auto
have un: "C ∪ (set_mset A) = B"
using Diff_partition ‹B - set_mset A = C› assms by blast
have disj: "C ∩ (set_mset A) = {}"
using ‹B - set_mset A = C› by auto
have zero: "⋀ x . x∈ C ⟹ count A x = 0"
by (meson count_eq_zero_iff disj disjoint_iff_not_equal)
then have "(∑ x ∈ B . count A x) = (∑ x ∈ (C ∪ set_mset A) . count A x)" using un by simp
also have "... = (∑ x ∈ C . count A x) + (∑ x ∈ (set_mset A) . count A x) "
using disj fin assms cdef sum.subset_diff by (metis un)
also have "... = (∑ x ∈ (set_mset A) . count A x)" using zero by auto
finally have "(∑ x ∈ B . count A x) = size A"
thus ?thesis by simp
qed

lemma mset_list_by_index: "mset (xs) = image_mset (λ i . (xs ! i)) (mset_set {..<length xs})"
by (metis map_nth mset_map mset_set_upto_eq_mset_upto)

lemma count_mset_split_image_filter:
assumes "⋀ x. x ∈#A ⟹ a ≠ g x"
shows "count (image_mset (λx. if P x then a else g x) A ) a = size (filter_mset P A)"
using image_mset_If image_mset_filter_swap size_image_mset
by (smt (verit) assms count_size_set_repr filter_mset_cong)

lemma count_mset_split_image_filter_not:
assumes "⋀ x. x ∈#A ⟹ b ≠ f x"
shows "count (image_mset (λx. if P x then f x else b) A ) b = size (filter_mset (λ x. ¬ P x) A)"
using image_mset_If image_mset_filter_swap size_image_mset
by (smt (verit) assms count_size_set_repr filter_mset_cong)

lemma removeAll_size_lt: "size (removeAll_mset C M) ≤ size M"

lemma mset_image_eq_filter_eq: "A = image_mset f B ⟹
filter_mset P A = (image_mset f (filter_mset (λ x. P (f x)) B))"

subsection ‹Permutation on Sets and Multisets ›

lemma elem_permutation_of_set_empty_iff: "finite A ⟹ xs ∈ permutations_of_set A ⟹
xs = [] ⟷ A = {}"
using permutations_of_setD(1) by fastforce

lemma elem_permutation_of_mset_empty_iff: "xs ∈ permutations_of_multiset A ⟹ xs = [] ⟷ A = {#}"
using permutations_of_multisetD by fastforce

subsection ‹ Lists ›
text ‹Further lemmas on the relationship between lists and multisets ›

lemma count_distinct_mset_list_index: "i1 < length xs ⟹ i2 < length xs ⟹ i1 ≠ i2 ⟹
distinct_mset (mset xs) ⟹ xs ! i1 ≠ xs ! i2"

lemma index_remove1_mset_ne:
assumes "x ∈# (mset xs)"
assumes "y ∈# remove1_mset x (mset xs)"
assumes "xs ! j1 = x"
assumes "j1 < length xs"
obtains j2 where "xs ! j2 = y" and "j2 < length xs" and "j1 ≠ j2"
proof (cases "x = y")
case True
then have "count (mset xs) x ≥ 2"
using assms(2) count_eq_zero_iff by fastforce
then have crm: "count (remove1_mset x (mset xs)) x ≥ 1"
by (metis True assms(2) count_greater_eq_one_iff)
obtain ys zs where xseq: "xs = ys @ (x # zs)" and yseq: "ys = take j1 xs" and zseq: "zs = drop (Suc j1) xs"
using  assms(1) assms(3) id_take_nth_drop in_mset_conv_nth assms(4) by blast
have "mset xs = mset ys + mset (x # zs)"
then have "remove1_mset x (mset xs) = mset (ys) + mset (zs)"
using assms by simp
then have "y ∈# (mset ys + mset zs)" using crm
using True ‹remove1_mset x (mset xs) = mset ys + mset zs› assms(2) by presburger
then have yinor: "y ∈# mset ys ∨ y ∈# mset zs" by simp
then show ?thesis proof (cases "y ∈# mset ys")
case True
then obtain j2 where yeq: "ys ! j2 = y" and j2lt: "j2 < length ys"
by (meson in_mset_conv_nth)
then have 1: "xs ! j2 = y" using yseq by simp
have "j2 < j1" using yseq j2lt by simp
then show ?thesis using that 1 j2lt xseq by simp
next
case False
then have "y ∈# mset zs" using yinor by simp
then obtain j2 where zsy: "zs ! j2 = y" and j2lt: "j2 < length zs"
by (meson in_mset_conv_nth)
then have 1: "xs ! ((Suc j1) + j2) = y" using zseq zsy assms(4) by simp
have "length xs = (Suc j1) + length zs" using zseq xseq
then have 2: "(Suc j1) + j2 < length xs" using j2lt by simp
then show ?thesis using 1 that by simp
qed
next
case False
then show ?thesis
by (metis that assms(2) assms(3) in_diffD in_mset_conv_nth)
qed

lemma count_list_mset: "count_list xs x = count (mset xs) x"
proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case proof (cases "a = x")
case True
have mset_add_split: "count (mset (a # xs)) x = count (add_mset a (mset xs)) x"
by simp
then have "count (mset (a # xs)) x = count (mset xs) x + 1"
then show ?thesis using True Cons.hyps by simp
next
case False
then show ?thesis using Cons.hyps by simp
qed
qed

lemma count_min_2_indices_lt:
assumes "i1 < i2"
assumes "xs ! i1 = x"
assumes "xs ! i2 = x"
assumes "i1 < length xs" "i2 < length xs"
shows "count (mset xs) x ≥ 2"
proof -
obtain xs1 xs2 where xse: "xs = xs1 @ xs2" and xs1: "xs1 = take i2 xs" and xs2: "xs2 = drop i2 xs"
by simp
have "i1 < length xs1" using assms length_take
by (simp add: assms(4) ‹xs1 = take i2 xs›)
then have xs1in:  "xs ! i1 ∈# mset xs1"
have "i2 ≥ length xs1" using assms length_take xs1 by simp
then have xs2in: "xs ! i2 ∈# mset xs2" using xse nth_append
by (metis (no_types, lifting) assms(5) in_mset_conv_nth leD leI take_all_iff take_append)
have "count (mset xs) x = count ((mset xs1) + (mset xs2)) x"
then have "count (mset xs) x = count (mset xs1) x + count (mset xs2) x" by simp
thus ?thesis using xs1in xs2in
qed

lemma count_min_2_indices: "i1 ≠ i2 ⟹ xs ! i1 = x ⟹ xs ! i2 = x ⟹ i1 < length xs ⟹
i2 < length xs ⟹ count (mset xs) x ≥ 2"
apply (cases "i1 < i2", simp add: count_min_2_indices_lt)
by (metis count_min_2_indices_lt linorder_cases)

lemma obtain_set_list_item:
assumes "x ∈ set xs"
obtains i where "i < length xs" and "xs ! i = x"
by (meson assms in_set_conv_nth)

subsection ‹Summation Rules›

text ‹ Some lemmas to make it simpler to work with double and triple summations ›
begin

lemma sum_reorder_triple: "(∑ l ∈ A . (∑ i ∈ B . (∑ j ∈ C . g l i j))) =
(∑ i ∈ B . (∑ j ∈ C . (∑ l ∈ A . g l i j)))"
proof -
have "(∑ l ∈ A . (∑ i ∈ B . (∑ j ∈ C . g l i j))) = (∑i ∈ B . (∑ l ∈ A  . (∑ j ∈ C . g l i j)))"
using sum.swap[of "(λ l i . (∑ j ∈ C . g l i j))" "B" "A"] by simp
also have "...  = (∑i ∈ B . (∑ j ∈ C . (∑l ∈ A . g l i j)))" using sum.swap by metis
finally show ?thesis by simp
qed

lemma double_sum_mult_hom:
fixes k :: "'b :: {comm_ring_1}"
shows "(∑ i ∈ A . (∑ j ∈ g i . k * (f i j))) = k* (∑ i ∈ A . (∑ j ∈ g i . f i j))"
by (metis (mono_tags, lifting) comm_monoid_add_class.sum.cong sum_distrib_left)

lemma double_sum_split_case:
assumes "finite A"
shows "(∑ i ∈ A . (∑ j ∈ A . f i j)) = (∑ i ∈ A . (f i i)) + (∑ i ∈ A . (∑ j ∈ (A - {i}) . f i j))"
proof -
have "⋀ i. i ∈ A ⟹ (∑ j ∈ A . f i j) = f i i + (∑ j ∈ (A - {i}) . f i j)"
using sum.remove assms by metis
then show ?thesis by (simp add: sum.distrib)
qed

lemma double_sum_split_case2: "(∑ i ∈ A . (∑ j ∈ A . g i j)) =
(∑ i ∈ A . (g i i)) + (∑ i ∈ A . (∑ j ∈ {a ∈ A . a ≠ i} . g i j)) "
proof -
have "⋀ i. A = {a ∈ A . a = i} ∪ {a ∈ A . a ≠ i}" by auto
then have part: "⋀ i. i ∈ A ⟹ A = {i} ∪ {a ∈ A . a ≠ i}" by auto
have empt:"⋀ i. {i} ∩ {a ∈ A . a ≠ i} = {}"
by simp
then have "(∑ i ∈ A . (∑ j ∈ A . g i j)) =
(∑ i ∈ A . ((∑ j ∈ {i} . g i j) + (∑ j ∈ {a ∈ A . a ≠ i} . g i j)))" using part
by (smt (verit) finite_Un local.sum.cong local.sum.infinite local.sum.union_disjoint)
also have "... = (∑ i ∈ A . ((∑ j ∈ {i} . g i j))) + (∑ i ∈ A . (∑ j ∈ {a ∈ A . a ≠ i} . g i j))"
finally show ?thesis by simp
qed

end

context comm_ring_1
begin

lemma double_sum_split_case_square:
assumes "finite A"
shows "(∑ i ∈ A . f i )^2 = (∑ i ∈ A . (f i * f i)) + (∑ i ∈ A . (∑ j ∈ (A - {i}) . f i * f j))"
proof -
have "(∑ i ∈ A . f i )^2 = (∑ i ∈ A . f i) * (∑ i ∈ A . f i)"
using power2_eq_square by blast
then have "(∑ i ∈ A . f i) * (∑ i ∈ A . f i) = (∑ i ∈ A . f i) * (∑ j ∈ A . f j)" by simp
also have 1: "... = (∑ i ∈ A . f i * (∑ j ∈ A . f j))" using sum_distrib_right by simp
also have 2: "... = (∑ i ∈ A .  (∑ j ∈ A . f i * f j))" using sum_distrib_left by metis
finally have "(∑ i ∈ A . f i) * (∑ i ∈ A . f i) =
(∑ i ∈ A . (f i * f i)) + (∑ i ∈ A . (∑ j ∈ (A - {i}) . f i * f j))"
using assms double_sum_split_case[of "A" "λ i j . f i * f j"] 1 2 by presburger
then show ?thesis
using power2_eq_square by presburger
qed

lemma double_sum_split_square_diff:  "finite {0..<x} ⟹
(∑ i ∈ {0..<x} . (∑ j ∈ ({0..< x} - {i}) . c i * c j)) =
(∑ i ∈ {0..<x} . c i)^2 - (∑ i ∈ {0..<x} . c i * c i)"
using double_sum_split_case_square[of "{0..<x}" "λ i. c i"] by fastforce

end
end```