Theory Expander_Graphs.Expander_Graphs_Multiset_Extras

subsection ‹Multisets›

text ‹Some preliminary results about multisets.›

theory Expander_Graphs_Multiset_Extras
  imports
    "HOL-Library.Multiset"
    Extra_Congruence_Method
begin

unbundle intro_cong_syntax

text ‹This is an induction scheme over the distinct elements of a multisets:
We can represent each multiset as a sum like:
@{text "replicate_mset n⇩1 x⇩1 + replicate_mset n⇩2 x⇩2 + ... + replicate_mset n⇩k x⇩k"} where the
@{term "x⇩i"} are distinct.›

lemma disj_induct_mset:
  assumes "P {#}"
  assumes "⋀n M x. P M ⟹ ¬(x ∈# M) ⟹ n > 0 ⟹ P (M + replicate_mset n x)"
  shows "P M"
proof (induction "size M" arbitrary: M rule:nat_less_induct)
  case 1
  show ?case
  proof (cases "M = {#}")
    case True
    then show ?thesis using assms by simp
  next
    case False
    then obtain x where x_def: "x ∈# M" using multiset_nonemptyE by auto
    define M1 where "M1 = M - replicate_mset (count M x) x"
    then have M_def: "M = M1 + replicate_mset (count M x) x"
      by (metis count_le_replicate_mset_subset_eq dual_order.refl subset_mset.diff_add)
    have "size M1 < size M"
      by (metis M_def x_def count_greater_zero_iff less_add_same_cancel1 size_replicate_mset size_union)
    hence "P M1" using 1 by blast
    then show "P M"
      apply (subst M_def, rule assms(2), simp)
      by (simp add:M1_def x_def count_eq_zero_iff[symmetric])+
  qed
qed

lemma sum_mset_conv:
  fixes f :: "'a ⇒ 'b::{semiring_1}"
  shows "sum_mset (image_mset f A) = sum (λx. of_nat (count A x) * f x) (set_mset A)"
proof (induction A rule: disj_induct_mset)
  case 1
  then show ?case by simp
next
  case (2 n M x)
  moreover have "count M x = 0" using 2 by (simp add: count_eq_zero_iff)
  moreover have "⋀y. y ∈ set_mset M ⟹ y ≠ x" using 2 by blast
  ultimately show ?case by (simp add:algebra_simps)
qed

lemma sum_mset_conv_2:
  fixes f :: "'a ⇒ 'b::{semiring_1}"
  assumes "set_mset A ⊆ B" "finite B"
  shows "sum_mset (image_mset f A) = sum (λx. of_nat (count A x) * f x) B" (is "?L = ?R")
proof -
  have "?L = sum (λx. of_nat (count A x) * f x) (set_mset A)"
    unfolding sum_mset_conv by simp
  also have "... = ?R"
    by (intro sum.mono_neutral_left assms) (simp_all add: iffD2[OF count_eq_zero_iff])
  finally show ?thesis by simp
qed

lemma count_mset_exp: "count A x = size (filter_mset (λy. y = x) A)"
  by (induction A, simp, simp)

lemma mset_repl: "mset (replicate k x) = replicate_mset k x"
  by (induction k, auto)

lemma count_image_mset_inj:
  assumes "inj f"
  shows "count (image_mset f A) (f x) = count A x"
proof (cases "x ∈ set_mset A")
  case True
  hence "f -` {f x} ∩ set_mset A = {x}"
    using assms by (auto simp add:vimage_def inj_def)
  then show ?thesis by (simp add:count_image_mset)
next
  case False
  hence "f -` {f x} ∩ set_mset A = {}"
    using assms by (auto simp add:vimage_def inj_def)
  thus ?thesis  using False by (simp add:count_image_mset count_eq_zero_iff)
qed

lemma count_image_mset_0_triv:
  assumes "x ∉ range f"
  shows "count (image_mset f A) x = 0"
proof -
  have "x ∉ set_mset (image_mset f A)"
    using assms by auto
  thus ?thesis
    by (meson count_inI)
qed

lemma filter_mset_ex_predicates:
  assumes "⋀x. ¬ P x ∨ ¬ Q x"
  shows "filter_mset P M + filter_mset Q M = filter_mset (λx. P x ∨ Q x) M"
  using assms by (induction M, auto)

lemma sum_count_2:
  assumes "finite F"
  shows "sum (count M) F = size (filter_mset (λx. x ∈ F) M)"
  using assms
proof (induction F rule:finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F)
  have "sum (count M) (insert x F) = size ({#y ∈# M. y = x#} + {#x ∈# M. x ∈ F#})"
    using insert(1,2,3) by (simp add:count_mset_exp)
  also have "... = size ({#y ∈# M. y = x ∨ y ∈ F#})"
    using insert(2)
    by (intro arg_cong[where f="size"] filter_mset_ex_predicates) simp
  also have "... = size (filter_mset (λy. y ∈ insert x F) M)"
    by simp
  finally show ?case by simp
qed

definition concat_mset :: "('a multiset) multiset ⇒ 'a multiset"
  where "concat_mset xss = fold_mset (λxs ys. xs + ys) {#} xss"

lemma image_concat_mset:
  "image_mset f (concat_mset xss) = concat_mset (image_mset (image_mset f) xss)"
  unfolding concat_mset_def by (induction xss, auto)

lemma concat_add_mset:
  "concat_mset (image_mset (λx. f x + g x) xs) = concat_mset (image_mset f xs) + concat_mset (image_mset g xs)"
  unfolding concat_mset_def by (induction xs) auto

lemma concat_add_mset_2:
  "concat_mset (xs + ys) = concat_mset xs + concat_mset ys"
  unfolding concat_mset_def by (induction xs, auto)

lemma size_concat_mset:
  "size (concat_mset xss) = sum_mset (image_mset size xss)"
  unfolding concat_mset_def by (induction xss, auto)

lemma filter_concat_mset:
  "filter_mset P (concat_mset xss) = concat_mset (image_mset (filter_mset P) xss)"
  unfolding concat_mset_def by (induction xss, auto)

lemma count_concat_mset:
  "count (concat_mset xss) xs = sum_mset (image_mset (λx. count x xs) xss)"
  unfolding concat_mset_def by (induction xss, auto)

lemma set_mset_concat_mset:
  "set_mset (concat_mset xss) = ⋃ (set_mset ` (set_mset xss))"
  unfolding concat_mset_def by (induction xss, auto)

lemma concat_mset_empty: "concat_mset {#} = {#}"
  unfolding concat_mset_def by simp

lemma concat_mset_single: "concat_mset {#x#} = x"
  unfolding concat_mset_def by simp

lemma concat_disjoint_union_mset:
  assumes "finite I"
  assumes "⋀i. i ∈ I ⟹ finite (A i)"
  assumes "⋀i j. i ∈ I ⟹ j ∈ I ⟹ i ≠ j ⟹ A i ∩ A j = {}"
  shows  "mset_set (⋃ (A ` I)) = concat_mset (image_mset (mset_set ∘ A) (mset_set I))"
  using assms
proof (induction I rule:finite_induct)
  case empty
  then show ?case by (simp add:concat_mset_empty)
next
  case (insert x F)
  have "mset_set (⋃ (A ` insert x F)) = mset_set (A x ∪ (⋃ (A ` F)))"
    by simp
  also have "... = mset_set (A x) + mset_set (⋃ (A ` F))"
    using insert by (intro mset_set_Union) auto
  also have "... = mset_set (A x) + concat_mset (image_mset (mset_set ∘ A) (mset_set F))"
    using insert by (intro arg_cong2[where f="(+)"] insert(3)) auto
  also have "... = concat_mset (image_mset (mset_set ∘ A) ({#x#} + mset_set F))"
    by (simp add:concat_mset_def)
  also have "... = concat_mset (image_mset (mset_set ∘ A) (mset_set (insert x F)))"
    using insert by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset]") auto
  finally show ?case by blast
qed

lemma size_filter_mset_conv:
  "size (filter_mset f A) = sum_mset (image_mset (λx. of_bool (f x) :: nat) A)"
  by (induction A, auto)

lemma filter_mset_const: "filter_mset (λ_. c) xs = (if c then xs else {#})"
  by simp

lemma repeat_image_concat_mset:
  "repeat_mset n (image_mset f A) = concat_mset (image_mset (λx. replicate_mset n (f x)) A)"
  unfolding concat_mset_def by (induction A, auto)

lemma mset_prod_eq:
  assumes "finite A" "finite B"
  shows
    "mset_set (A × B) = concat_mset {# {# (x,y). y ∈# mset_set B #} .x ∈# mset_set A #}"
  using assms(1)
proof (induction rule:finite_induct)
  case empty
  then show ?case unfolding concat_mset_def by simp
next
  case (insert x F)
  have "mset_set (insert x F × B) = mset_set (F × B ∪ (λy. (x,y)) ` B)"
    by (intro arg_cong[where f="mset_set"]) auto
  also have "... = mset_set (F × B) + mset_set ((λy. (x,y)) ` B)"
    using insert(1,2) assms(2) by (intro mset_set_Union finite_cartesian_product) auto
  also have "... = mset_set (F × B) + {# (x,y). y ∈# mset_set B #}"
    by (intro arg_cong2[where f="(+)"] image_mset_mset_set[symmetric] inj_onI) auto
  also have "... = concat_mset {#image_mset (Pair x) (mset_set B). x ∈# {#x#} + (mset_set F)#}"
    unfolding insert image_mset_union concat_add_mset_2 by (simp add:concat_mset_single)
  also have "... = concat_mset {#image_mset (Pair x) (mset_set B). x ∈# mset_set (insert x F)#}"
    using insert(1,2) by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset]") auto
  finally show ?case by simp
qed

lemma sum_mset_repeat:
  fixes f :: "'a ⇒ 'b :: {comm_monoid_add,semiring_1}"
  shows "sum_mset (image_mset f (repeat_mset n A)) = of_nat n * sum_mset (image_mset f A)"
  by (induction n, auto simp add:sum_mset.distrib algebra_simps)

unbundle no_intro_cong_syntax

end