(* 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" by (simp add: size_multiset_overloaded_eq) 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" by (simp add: size_mset_mono) 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))" by (simp add: filter_mset_image_mset) 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" by (simp add: nth_eq_iff_index_eq) 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)" by (simp add: xseq) 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 by (metis Suc_diff_Suc add_Suc_shift add_diff_inverse_nat assms(4) length_drop less_imp_not_less) 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" by (metis True Suc_eq_plus1 count_add_mset) 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" by (simp add: nth_append xse) 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" by (simp add: xse) then have "count (mset xs) x = count (mset xs1) x + count (mset xs2) x" by simp thus ?thesis using xs1in xs2in by (metis add_mono assms(2) assms(3) count_greater_eq_one_iff nat_1_add_1) 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 › context comm_monoid_add 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))" by (simp add: local.sum.distrib) 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