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