Theory Fishers_Inequality.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"
    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