lemma multinomial:
  "card {f∈A →⇩E B. ∀x∈B. card (f -` {x} ∩ A) = h x} * (∏x∈B. fact (h x)) =
     fact (card A)"

lemma finite_card_fixed_length_lists:
  assumes "finite X"
  shows
    "finite {ls. length ls = n ∧ set ls ⊆ X}"
    "card {ls. length ls = n ∧ set ls ⊆ X} = card X ^ n"
proof -
  obtain xs where "X = set xs"
    using assms finite_list by blast
  show "finite {ls. length ls = n ∧ set ls ⊆ X}"
    by (smt (verit) Collect_mono_iff assms finite_lists_length_eq rev_finite_subset)
  show "card {ls. length ls = n ∧ set ls ⊆ X} = card X ^ n"
    by (metis (no_types, lifting) Collect_cong assms card_lists_length_eq)
qed

(* Multinomial coefficient:
  this definition makes it slightly easier to prove the
  multinomial theorem
*)
definition multinomial :: "nat ⇒ nat list ⇒ nat"  (infixl "mchoose" 65)
  where "n mchoose ks =
  fact n div prod_list (map fact ks)"

lemma prod_list_dvd_fact_sum_list:
  shows "prod_list (map fact ks) dvd fact (sum_list ks)"
proof (induction ks)
  case Nil
  then show ?case
    by (auto simp add: dvd_def)
next
  case (Cons k ks)
  then show ?case
    apply auto
    by (smt (verit) add_diff_cancel_left' binomial_fact_lemma dvd_def le_add1 mult.assoc of_nat_fact of_nat_mult)
qed

lemma multinomial_dvd:
  assumes "sum_list ks ≤ n"
  shows "prod_list (map fact ks) dvd fact n"
  by (metis assms binomial_fact_lemma dvd_def mult.assoc of_nat_fact of_nat_mult prod_list_dvd_fact_sum_list)

lemma finite_sum_list_eq:
  "finite {ks. length ks = x ∧ sum_list ks = (y::nat)}"
proof -
  have *: "{ks. length ks = x ∧ sum_list ks = (y::nat)} ⊆
    {ks. length ks = x ∧ set ks ⊆ {0..y}}"
    apply auto
    by (simp add: member_le_sum_list)
  have "finite  {ks. length ks = x ∧ set ks ⊆ {0..y}}"
    using finite_card_fixed_length_lists
    by blast
  thus ?thesis using *
    by (meson rev_finite_subset)
qed

lemma sum_split_k:
  shows "sum f {ks. length ks = Suc x ∧ sum_list ks = n} =
    (∑k≤n. sum (λks. f ((k::nat) # ks)) {ks. length ks = x ∧ sum_list ks = n - k})"
proof -
  have *: "{ks. length ks = Suc x ∧ sum_list ks = n} =
    (⋃k≤n.
    (λks. k # ks) `
    {ks. length ks = x ∧ sum_list ks = n - k})"
    apply auto
  proof -
    fix ys
    assume ys: "length ys = Suc x" "n = sum_list ys"
    then obtain y yss where y: "ys = y # yss"
      by (metis Suc_length_conv)
    have "y + sum_list yss = n" using ys y by auto
    then have 1:"y ∈ {..sum_list ys}"
      by (simp add: ys(2))
    have 2:"ys ∈ (#) y ` {ks. length ks = x ∧ sum_list ks = sum_list ys - y}"
      apply (auto simp add: image_def)
      using y ys(1) by fastforce
    thus "∃xb∈{..sum_list ys}.
             ys ∈ (#) xb `
                   {ks.
                    length ks = x ∧
                    sum_list ks = sum_list ys - xb}"
      using 1 2 by blast
  qed
  have f: "finite {ks. length ks = x ∧ sum_list ks = (y::nat)}" for y
    using finite_sum_list_eq by auto
  show ?thesis
    unfolding *
    apply (subst sum.UNION_disjoint)
       apply (auto simp add: f)
    apply (subst sum.reindex)
    by auto
qed

lemma cross_multiply:
  assumes "a dvd c"
  assumes "d dvd (a::nat)"
  shows "a div d * c div a = c div d"
  using assms(1) assms(2) by fastforce

lemma mchoose_cons:
  assumes "sum_list (k # ks) ≤ n"
  shows "(n mchoose (k # ks)) =
    (n-k mchoose ks) * (n choose k)"
proof -
  have *: "fact n div fact k = fact (n - k) * (n choose k)"
    by (metis (no_types, lifting) assms binomial_fact_lemma fact_nonzero le_add1 le_eq_less_or_eq mult.assoc nonzero_mult_div_cancel_left order_le_less_trans sum_list_simps(2))
  have "n mchoose (k # ks) =
    fact n div prod_list (map fact (k # ks))"
    unfolding multinomial_def by auto
  moreover have "... = (fact n div fact k) div prod_list (map fact ks)"
    apply simp
    by (metis div_mult2_eq)
  moreover have "... = (fact (n - k) * (n choose k)) div prod_list (map fact ks)"
    using * by auto
  moreover have "... = (fact (n - k) div prod_list (map fact ks)) * (n choose k)"
    by (metis add_le_cancel_left assms binomial_eq_0 bits_div_0 div_mult_swap le_add_diff_inverse linorder_not_less mult.commute mult_zero_left multinomial_dvd sum_list.Cons)
  ultimately show ?thesis
    using multinomial_def by presburger
qed

theorem multinomial_theorem:
  shows "(sum_list (xs::nat list)) ^ n =
    sum (λks. (n mchoose ks) * prod_list (map2 (^) xs ks))
    {ks. length ks = length xs ∧ sum_list ks = n}"
proof (induction xs arbitrary: n)
  case Nil
  have *: "{ks. ks = [] ∧ (∀n∈set ks. n = 0)} = {[]}"
    by auto
  show ?case
    apply (cases n)
     by (auto simp add:multinomial_def *)
next
  case (Cons x xs)

  (* rhs *)
  have "(∑ks | length ks = Suc (length xs) ∧
            sum_list ks = n.
       (n mchoose ks) *
       prod_list (map2 (^) (x # xs) ks)) =
    (∑k≤n.
        ∑ks | length ks = length xs ∧
               sum_list ks = n - k.
          (n mchoose (k # ks)) *
          prod_list (map2 (^) (x # xs) (k # ks)))"
    unfolding sum_split_k by auto
  moreover have "... =
     (∑k≤n.
        sum (λks.
          ((n-k mchoose ks) * (n choose k)) *
          (x ^ k * prod_list (map2 (^) xs ks)))
        {ks. length ks = length xs ∧ sum_list ks = n - k})"
    by (auto intro!: sum.cong simp add: mchoose_cons)
  moreover have "... =
     (∑k≤n.
        (n choose k) * x ^ k *
        sum (λks.
          (n-k mchoose ks) *
          prod_list (map2 (^) xs ks))
        {ks. length ks = length xs ∧ sum_list ks = n - k})"
    by (smt (z3) mult.assoc mult.left_commute sum.cong sum_distrib_left)
  moreover have "... =
    (∑k≤n.
        of_nat (n choose k) * x ^ k *
        sum_list xs ^ (n - k))"
    using Cons
    using of_nat_id by presburger
  moreover
  have "... = (x + sum_list xs) ^ n "
    unfolding binomial by auto
  ultimately show ?case
    by auto
qed