# Theory Binomial

theory Binomial
imports Factorial
(*  Title:      HOL/Binomial.thy
Author:     Jacques D. Fleuriot
Author:     Lawrence C Paulson
Author:     Chaitanya Mangla
Author:     Manuel Eberl
*)

section ‹Binomial Coefficients and Binomial Theorem›

theory Binomial
imports Presburger Factorial
begin

subsection ‹Binomial coefficients›

text ‹This development is based on the work of Andy Gordon and Florian Kammueller.›

text ‹Combinatorial definition›

definition binomial :: "nat ⇒ nat ⇒ nat"  (infixl "choose" 65)
where "n choose k = card {K∈Pow {0..<n}. card K = k}"

theorem n_subsets:
assumes "finite A"
shows "card {B. B ⊆ A ∧ card B = k} = card A choose k"
proof -
from assms obtain f where bij: "bij_betw f {0..<card A} A"
by (blast dest: ex_bij_betw_nat_finite)
then have [simp]: "card (f  C) = card C" if "C ⊆ {0..<card A}" for C
by (meson bij_betw_imp_inj_on bij_betw_subset card_image that)
from bij have "bij_betw (image f) (Pow {0..<card A}) (Pow A)"
by (rule bij_betw_Pow)
then have "inj_on (image f) (Pow {0..<card A})"
by (rule bij_betw_imp_inj_on)
moreover have "{K. K ⊆ {0..<card A} ∧ card K = k} ⊆ Pow {0..<card A}"
by auto
ultimately have "inj_on (image f) {K. K ⊆ {0..<card A} ∧ card K = k}"
by (rule inj_on_subset)
then have "card {K. K ⊆ {0..<card A} ∧ card K = k} =
card (image f  {K. K ⊆ {0..<card A} ∧ card K = k})" (is "_ = card ?C")
also have "?C = {K. K ⊆ f  {0..<card A} ∧ card K = k}"
by (auto elim!: subset_imageE)
also have "f  {0..<card A} = A"
by (meson bij bij_betw_def)
finally show ?thesis
qed

text ‹Recursive characterization›

lemma binomial_n_0 [simp, code]: "n choose 0 = 1"
proof -
have "{K ∈ Pow {0..<n}. card K = 0} = {{}}"
by (auto dest: finite_subset)
then show ?thesis
qed

lemma binomial_0_Suc [simp, code]: "0 choose Suc k = 0"

lemma binomial_Suc_Suc [simp, code]: "Suc n choose Suc k = (n choose k) + (n choose Suc k)"
proof -
let ?P = "λn k. {K. K ⊆ {0..<n} ∧ card K = k}"
let ?Q = "?P (Suc n) (Suc k)"
have inj: "inj_on (insert n) (?P n k)"
by rule (auto; metis atLeastLessThan_iff insert_iff less_irrefl subsetCE)
have disjoint: "insert n  ?P n k ∩ ?P n (Suc k) = {}"
by auto
have "?Q = {K∈?Q. n ∈ K} ∪ {K∈?Q. n ∉ K}"
by auto
also have "{K∈?Q. n ∈ K} = insert n  ?P n k" (is "?A = ?B")
proof (rule set_eqI)
fix K
have K_finite: "finite K" if "K ⊆ insert n {0..<n}"
using that by (rule finite_subset) simp_all
have Suc_card_K: "Suc (card K - Suc 0) = card K" if "n ∈ K"
and "finite K"
proof -
from ‹n ∈ K› obtain L where "K = insert n L" and "n ∉ L"
by (blast elim: Set.set_insert)
with that show ?thesis by (simp add: card_insert)
qed
show "K ∈ ?A ⟷ K ∈ ?B"
by (subst in_image_insert_iff)
Diff_subset_conv K_finite Suc_card_K)
qed
also have "{K∈?Q. n ∉ K} = ?P n (Suc k)"
finally show ?thesis using inj disjoint
by (simp add: binomial_def card_Un_disjoint card_image)
qed

lemma binomial_eq_0: "n < k ⟹ n choose k = 0"
by (auto simp add: binomial_def dest: subset_eq_atLeast0_lessThan_card)

lemma zero_less_binomial: "k ≤ n ⟹ n choose k > 0"
by (induct n k rule: diff_induct) simp_all

lemma binomial_eq_0_iff [simp]: "n choose k = 0 ⟷ n < k"
by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)

lemma zero_less_binomial_iff [simp]: "n choose k > 0 ⟷ k ≤ n"
by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)

lemma binomial_n_n [simp]: "n choose n = 1"
by (induct n) (simp_all add: binomial_eq_0)

lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"
by (induct n) simp_all

lemma binomial_1 [simp]: "n choose Suc 0 = n"
by (induct n) simp_all

lemma choose_reduce_nat:
"0 < n ⟹ 0 < k ⟹
n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp

lemma Suc_times_binomial_eq: "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
apply (induct n arbitrary: k)
apply simp
apply arith
apply (case_tac k)
done

lemma binomial_le_pow2: "n choose k ≤ 2^n"
apply (induct n arbitrary: k)
apply (case_tac k)
apply simp_all
apply (case_tac k)
apply auto
done

text ‹The absorption property.›
lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
using Suc_times_binomial_eq by auto

text ‹This is the well-known version of absorption, but it's harder to use
because of the need to reason about division.›
lemma binomial_Suc_Suc_eq_times: "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)

text ‹Another version of absorption, with ‹-1› instead of ‹Suc›.›
lemma times_binomial_minus1_eq: "0 < k ⟹ k * (n choose k) = n * ((n - 1) choose (k - 1))"
using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
by (auto split: nat_diff_split)

subsection ‹The binomial theorem (courtesy of Tobias Nipkow):›

text ‹Avigad's version, generalized to any commutative ring›
theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n =
(∑k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have decomp: "{0..n+1} = {0} ∪ {n + 1} ∪ {1..n}"
by auto
have decomp2: "{0..n} = {0} ∪ {1..n}"
by auto
have "(a + b)^(n+1) = (a + b) * (∑k=0..n. of_nat (n choose k) * a^k * b^(n - k))"
using Suc.hyps by simp
also have "… = a * (∑k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
b * (∑k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
by (rule distrib_right)
also have "… = (∑k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
(∑k=0..n. of_nat (n choose k) * a^k * b^(n - k + 1))"
by (auto simp add: sum_distrib_left ac_simps)
also have "… = (∑k=0..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
(∑k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))"
by (simp add:sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
also have "… = a^(n + 1) + b^(n + 1) +
(∑k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
(∑k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
also have "… = a^(n + 1) + b^(n + 1) +
(∑k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat)
also have "… = (∑k=0..n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
using decomp by (simp add: field_simps)
finally show ?case
by simp
qed

text ‹Original version for the naturals.›
corollary binomial: "(a + b :: nat)^n = (∑k=0..n. (of_nat (n choose k)) * a^k * b^(n - k))"
using binomial_ring [of "int a" "int b" n]
by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]
of_nat_sum [symmetric] of_nat_eq_iff of_nat_id)

lemma binomial_fact_lemma: "k ≤ n ⟹ fact k * fact (n - k) * (n choose k) = fact n"
proof (induct n arbitrary: k rule: nat_less_induct)
fix n k
assume H: "∀m<n. ∀x≤m. fact x * fact (m - x) * (m choose x) = fact m"
assume kn: "k ≤ n"
let ?ths = "fact k * fact (n - k) * (n choose k) = fact n"
consider "n = 0 ∨ k = 0 ∨ n = k" | m h where "n = Suc m" "k = Suc h" "h < m"
using kn by atomize_elim presburger
then show "fact k * fact (n - k) * (n choose k) = fact n"
proof cases
case 1
with kn show ?thesis by auto
next
case 2
note n = ‹n = Suc m›
note k = ‹k = Suc h›
note hm = ‹h < m›
have mn: "m < n"
using n by arith
have hm': "h ≤ m"
using hm by arith
have km: "k ≤ m"
using hm k n kn by arith
have "m - h = Suc (m - Suc h)"
using  k km hm by arith
with km k have "fact (m - h) = (m - h) * fact (m - k)"
by simp
with n k have "fact k * fact (n - k) * (n choose k) =
k * (fact h * fact (m - h) * (m choose h)) +
(m - h) * (fact k * fact (m - k) * (m choose k))"
also have "… = (k + (m - h)) * fact m"
using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
finally show ?thesis
using k n km by simp
qed
qed

lemma binomial_fact':
assumes "k ≤ n"
shows "n choose k = fact n div (fact k * fact (n - k))"
using binomial_fact_lemma [OF assms]
by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left)

lemma binomial_fact:
assumes kn: "k ≤ n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))"
using binomial_fact_lemma[OF kn]
apply (metis mult.commute of_nat_fact of_nat_mult)
done

lemma fact_binomial:
assumes "k ≤ n"
shows "fact k * of_nat (n choose k) = (fact n / fact (n - k) :: 'a::field_char_0)"
unfolding binomial_fact [OF assms] by (simp add: field_simps)

lemma choose_two: "n choose 2 = n * (n - 1) div 2"
proof (cases "n ≥ 2")
case False
then have "n = 0 ∨ n = 1"
by auto
then show ?thesis by auto
next
case True
define m where "m = n - 2"
with True have "n = m + 2"
by simp
then have "fact n = n * (n - 1) * fact (n - 2)"
by (simp add: fact_prod_Suc atLeast0_lessThan_Suc algebra_simps)
with True show ?thesis
qed

lemma choose_row_sum: "(∑k=0..n. n choose k) = 2^n"
using binomial [of 1 "1" n] by (simp add: numeral_2_eq_2)

lemma sum_choose_lower: "(∑k=0..n. (r+k) choose k) = Suc (r+n) choose n"
by (induct n) auto

lemma sum_choose_upper: "(∑k=0..n. k choose m) = Suc n choose Suc m"
by (induct n) auto

lemma choose_alternating_sum:
"n > 0 ⟹ (∑i≤n. (-1)^i * of_nat (n choose i)) = (0 :: 'a::comm_ring_1)"
using binomial_ring[of "-1 :: 'a" 1 n]
by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)

lemma choose_even_sum:
assumes "n > 0"
shows "2 * (∑i≤n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)"
proof -
have "2 ^ n = (∑i≤n. of_nat (n choose i)) + (∑i≤n. (-1) ^ i * of_nat (n choose i) :: 'a)"
using choose_row_sum[of n]
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_sum[symmetric])
also have "… = (∑i≤n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
also have "… = 2 * (∑i≤n. if even i then of_nat (n choose i) else 0)"
by (subst sum_distrib_left, intro sum.cong) simp_all
finally show ?thesis ..
qed

lemma choose_odd_sum:
assumes "n > 0"
shows "2 * (∑i≤n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)"
proof -
have "2 ^ n = (∑i≤n. of_nat (n choose i)) - (∑i≤n. (-1) ^ i * of_nat (n choose i) :: 'a)"
using choose_row_sum[of n]
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_sum[symmetric])
also have "… = (∑i≤n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
also have "… = 2 * (∑i≤n. if odd i then of_nat (n choose i) else 0)"
by (subst sum_distrib_left, intro sum.cong) simp_all
finally show ?thesis ..
qed

lemma choose_row_sum': "(∑k≤n. (n choose k)) = 2 ^ n"
using choose_row_sum[of n] by (simp add: atLeast0AtMost)

text‹NW diagonal sum property›
lemma sum_choose_diagonal:
assumes "m ≤ n"
shows "(∑k=0..m. (n - k) choose (m - k)) = Suc n choose m"
proof -
have "(∑k=0..m. (n-k) choose (m - k)) = (∑k=0..m. (n - m + k) choose k)"
using sum.atLeast_atMost_rev [of "λk. (n - k) choose (m - k)" 0 m] assms
by simp
also have "… = Suc (n - m + m) choose m"
by (rule sum_choose_lower)
also have "… = Suc n choose m"
using assms by simp
finally show ?thesis .
qed

subsection ‹Generalized binomial coefficients›

definition gbinomial :: "'a::{semidom_divide,semiring_char_0} ⇒ nat ⇒ 'a"  (infixl "gchoose" 65)
where gbinomial_prod_rev: "a gchoose n = prod (λi. a - of_nat i) {0..<n} div fact n"

lemma gbinomial_0 [simp]:
"a gchoose 0 = 1"
"0 gchoose (Suc n) = 0"

lemma gbinomial_Suc: "a gchoose (Suc k) = prod (λi. a - of_nat i) {0..k} div fact (Suc k)"

lemma gbinomial_mult_fact: "fact n * (a gchoose n) = (∏i = 0..<n. a - of_nat i)"
for a :: "'a::field_char_0"

lemma gbinomial_mult_fact': "(a gchoose n) * fact n = (∏i = 0..<n. a - of_nat i)"
for a :: "'a::field_char_0"
using gbinomial_mult_fact [of n a] by (simp add: ac_simps)

lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / fact n"
for a :: "'a::field_char_0"
by (cases n)
power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
prod.atLeast_Suc_atMost_Suc_shift of_nat_diff)

lemma gbinomial_pochhammer': "s gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
for s :: "'a::field_char_0"
proof -
have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"
by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
also have "(-1 :: 'a)^n * (-1)^n = 1"
finally show ?thesis
by simp
qed

lemma gbinomial_binomial: "n gchoose k = n choose k"
proof (cases "k ≤ n")
case False
then have "n < k"
then have "0 ∈ (op - n)  {0..<k}"
by auto
then have "prod (op - n) {0..<k} = 0"
by (auto intro: prod_zero)
with ‹n < k› show ?thesis
by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero)
next
case True
from True have *: "prod (op - n) {0..<k} = ∏{Suc (n - k)..n}"
by (intro prod.reindex_bij_witness[of _ "λi. n - i" "λi. n - i"]) auto
from True have "n choose k = fact n div (fact k * fact (n - k))"
by (rule binomial_fact')
with * show ?thesis
by (simp add: gbinomial_prod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
qed

lemma of_nat_gbinomial: "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof (cases "k ≤ n")
case False
then show ?thesis
by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_prod_rev)
next
case True
define m where "m = n - k"
with True have n: "n = m + k"
by arith
from n have "fact n = ((∏i = 0..<m + k. of_nat (m + k - i) ):: 'a)"
also have "… = ((∏i∈{0..<k} ∪ {k..<m + k}. of_nat (m + k - i)) :: 'a)"
finally have "fact n = (fact m * (∏i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)"
using prod_shift_bounds_nat_ivl [of "λi. of_nat (m + k - i) :: 'a" 0 k m]
by (simp add: fact_prod_rev [of m] prod.union_disjoint of_nat_diff)
then have "fact n / fact (n - k) = ((∏i = 0..<k. of_nat n - of_nat i) :: 'a)"
with True have "fact k * of_nat (n gchoose k) = (fact k * (of_nat n gchoose k) :: 'a)"
by (simp only: gbinomial_mult_fact [of k "of_nat n"] gbinomial_binomial [of n k] fact_binomial)
then show ?thesis
by simp
qed

lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial)

setup
‹Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 ⇒ nat ⇒ 'a"})›

lemma gbinomial_1[simp]: "a gchoose 1 = a"

lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"

lemma gbinomial_mult_1:
fixes a :: "'a::field_char_0"
shows "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
(is "?l = ?r")
proof -
have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc)
apply (simp del: of_nat_Suc fact_Suc)
apply (auto simp add: field_simps simp del: of_nat_Suc)
done
also have "… = ?l"
finally show ?thesis ..
qed

lemma gbinomial_mult_1':
"(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
for a :: "'a::field_char_0"

lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
for a :: "'a::field_char_0"
proof (cases k)
case 0
then show ?thesis by simp
next
case (Suc h)
have eq0: "(∏i∈{1..k}. (a + 1) - of_nat i) = (∏i∈{0..h}. a - of_nat i)"
apply (rule prod.reindex_cong [where l = Suc])
using Suc
done
have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
(a gchoose Suc h) * (fact (Suc (Suc h))) +
(a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
by (simp add: Suc field_simps del: fact_Suc)
also have "… =
(a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (∏i=0..Suc h. a - of_nat i)"
apply (simp del: fact_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
done
also have "… =
(fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + (∏i=0..Suc h. a - of_nat i)"
by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
also have "… =
of_nat (Suc (Suc h)) * (∏i=0..h. a - of_nat i) + (∏i=0..Suc h. a - of_nat i)"
unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost by auto
also have "… =
(∏i=0..Suc h. a - of_nat i) + (of_nat h * (∏i=0..h. a - of_nat i) + 2 * (∏i=0..h. a - of_nat i))"
also have "… =
((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (∏i∈{0..Suc h}. a - of_nat i)"
unfolding gbinomial_mult_fact'
by (simp add: comm_semiring_class.distrib field_simps Suc atLeastLessThanSuc_atLeastAtMost)
also have "… = (∏i∈{0..h}. a - of_nat i) * (a + 1)"
unfolding gbinomial_mult_fact' atLeast0_atMost_Suc
by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost)
also have "… = (∏i∈{0..k}. (a + 1) - of_nat i)"
using eq0
also have "… = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost)
finally show ?thesis
using fact_nonzero [of "Suc k"] by auto
qed

lemma gbinomial_reduce_nat: "0 < k ⟹ a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
for a :: "'a::field_char_0"

lemma gchoose_row_sum_weighted:
"(∑k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))"
for r :: "'a::field_char_0"
by (induct m) (simp_all add: field_simps distrib gbinomial_mult_1)

lemma binomial_symmetric:
assumes kn: "k ≤ n"
shows "n choose k = n choose (n - k)"
proof -
have kn': "n - k ≤ n"
using kn by arith
from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))"
by simp
then show ?thesis
using kn by simp
qed

lemma choose_rising_sum:
"(∑j≤m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"
"(∑j≤m. ((n + j) choose n)) = ((n + m + 1) choose m)"
proof -
show "(∑j≤m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"
by (induct m) simp_all
also have "… = (n + m + 1) choose m"
by (subst binomial_symmetric) simp_all
finally show "(∑j≤m. ((n + j) choose n)) = (n + m + 1) choose m" .
qed

lemma choose_linear_sum: "(∑i≤n. i * (n choose i)) = n * 2 ^ (n - 1)"
proof (cases n)
case 0
then show ?thesis by simp
next
case (Suc m)
have "(∑i≤n. i * (n choose i)) = (∑i≤Suc m. i * (Suc m choose i))"
also have "… = Suc m * 2 ^ m"
by (simp only: sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric])
finally show ?thesis
using Suc by simp
qed

lemma choose_alternating_linear_sum:
assumes "n ≠ 1"
shows "(∑i≤n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a::comm_ring_1) = 0"
proof (cases n)
case 0
then show ?thesis by simp
next
case (Suc m)
with assms have "m > 0"
by simp
have "(∑i≤n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =
(∑i≤Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))"
also have "… = (∑i≤m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
by (simp only: sum_atMost_Suc_shift sum_distrib_left[symmetric] mult_ac of_nat_mult) simp
also have "… = - of_nat (Suc m) * (∑i≤m. (-1) ^ i * of_nat (m choose i))"
by (subst sum_distrib_left, rule sum.cong[OF refl], subst Suc_times_binomial)
also have "(∑i≤m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"
using choose_alternating_sum[OF ‹m > 0›] by simp
finally show ?thesis
by simp
qed

lemma vandermonde: "(∑k≤r. (m choose k) * (n choose (r - k))) = (m + n) choose r"
proof (induct n arbitrary: r)
case 0
have "(∑k≤r. (m choose k) * (0 choose (r - k))) = (∑k≤r. if k = r then (m choose k) else 0)"
by (intro sum.cong) simp_all
also have "… = m choose r"
finally show ?case
by simp
next
case (Suc n r)
show ?case
by (cases r) (simp_all add: Suc [symmetric] algebra_simps sum.distrib Suc_diff_le)
qed

lemma choose_square_sum: "(∑k≤n. (n choose k)^2) = ((2*n) choose n)"
using vandermonde[of n n n]
by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric])

lemma pochhammer_binomial_sum:
fixes a b :: "'a::comm_ring_1"
shows "pochhammer (a + b) n = (∑k≤n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))"
proof (induction n arbitrary: a b)
case 0
then show ?case by simp
next
case (Suc n a b)
have "(∑k≤Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) =
(∑i≤n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
((∑i≤n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
pochhammer b (Suc n))"
by (subst sum_atMost_Suc_shift) (simp add: ring_distribs sum.distrib)
also have "(∑i≤n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
a * pochhammer ((a + 1) + b) n"
by (subst Suc) (simp add: sum_distrib_left pochhammer_rec mult_ac)
also have "(∑i≤n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
pochhammer b (Suc n) =
(∑i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
apply simp
apply (subst sum_shift_bounds_cl_Suc_ivl)
done
also have "… = (∑i≤n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
using Suc by (intro sum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
also have "… = (∑i≤n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))"
by (intro sum.cong) (simp_all add: Suc_diff_le)
also have "… = b * pochhammer (a + (b + 1)) n"
by (subst Suc) (simp add: sum_distrib_left mult_ac pochhammer_rec)
also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n =
pochhammer (a + b) (Suc n)"
finally show ?case ..
qed

text ‹Contributed by Manuel Eberl, generalised by LCP.
Alternative definition of the binomial coefficient as @{term "∏i<k. (n - i) / (k - i)"}.›
lemma gbinomial_altdef_of_nat: "x gchoose k = (∏i = 0..<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
for k :: nat and x :: "'a::field_char_0"
by (simp add: prod_dividef gbinomial_prod_rev fact_prod_rev)

lemma gbinomial_ge_n_over_k_pow_k:
fixes k :: nat
and x :: "'a::linordered_field"
assumes "of_nat k ≤ x"
shows "(x / of_nat k :: 'a) ^ k ≤ x gchoose k"
proof -
have x: "0 ≤ x"
using assms of_nat_0_le_iff order_trans by blast
have "(x / of_nat k :: 'a) ^ k = (∏i = 0..<k. x / of_nat k :: 'a)"
also have "… ≤ x gchoose k" (* FIXME *)
unfolding gbinomial_altdef_of_nat
apply (safe intro!: prod_mono)
apply simp_all
prefer 2
subgoal premises for i
proof -
from assms have "x * of_nat i ≥ of_nat (i * k)"
by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
then have "x * of_nat k - x * of_nat i ≤ x * of_nat k - of_nat (i * k)"
by arith
then have "x * of_nat (k - i) ≤ (x - of_nat i) * of_nat k"
using ‹i < k› by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)
then have "x * of_nat (k - i) ≤ (x - of_nat i) * (of_nat k :: 'a)"
by (simp only: of_nat_mult[symmetric] of_nat_le_iff)
with assms show ?thesis
using ‹i < k› by (simp add: field_simps)
qed
done
finally show ?thesis .
qed

lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"
by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)

lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"

lemma Suc_times_gbinomial: "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
proof (cases b)
case 0
then show ?thesis by simp
next
case (Suc b)
then have "((a + 1) gchoose (Suc (Suc b))) = (∏i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(∏i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (∏i = 0..b. a - of_nat i)"
also have "… / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
qed

lemma gbinomial_factors: "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
proof (cases b)
case 0
then show ?thesis by simp
next
case (Suc b)
then have "((a + 1) gchoose (Suc (Suc b))) = (∏i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(∏i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (∏i = 0..b. a - of_nat i)"
also have "… / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
finally show ?thesis
qed

lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"
using gbinomial_mult_1[of r k]

lemma gbinomial_of_nat_symmetric: "k ≤ n ⟹ (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])

text ‹The absorption identity (equation 5.5 \cite[p.~157]{GKP}):
${r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.$›
lemma gbinomial_absorption': "k > 0 ⟹ r gchoose k = (r / of_nat k) * (r - 1 gchoose (k - 1))"
using gbinomial_rec[of "r - 1" "k - 1"]
by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)

text ‹The absorption identity is written in the following form to avoid
division by $k$ (the lower index) and therefore remove the $k \neq 0$
restriction\cite[p.~157]{GKP}:
$k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.$›
lemma gbinomial_absorption: "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"
using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)

text ‹The absorption identity for natural number binomial coefficients:›
lemma binomial_absorption: "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)

text ‹The absorption companion identity for natural number coefficients,
following the proof by GKP \cite[p.~157]{GKP}:›
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
(is "?lhs = ?rhs")
proof (cases "n ≤ k")
case True
then show ?thesis by auto
next
case False
then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"
using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]
by simp
also have "Suc ((n - 1) - k) = n - k"
using False by simp
also have "n choose … = n choose k"
using False by (intro binomial_symmetric [symmetric]) simp_all
finally show ?thesis ..
qed

text ‹The generalised absorption companion identity:›
lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"
using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)

"r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"
using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)

"0 < n ⟹ n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
by (subst choose_reduce_nat) simp_all

text ‹
Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
summation formula, operating on both indices:
$\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, \quad \textnormal{integer } n.$
›
lemma gbinomial_parallel_sum: "(∑k≤n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc m)
then show ?case
using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m]
qed

subsubsection ‹Summation on the upper index›

text ‹
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
aptly named \emph{summation on the upper index}:$\sum_{0 \leq k \leq n} {k \choose m} = {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.$
›
lemma gbinomial_sum_up_index:
"(∑k = 0..n. (of_nat k gchoose m) :: 'a::field_char_0) = (of_nat n + 1) gchoose (m + 1)"
proof (induct n)
case 0
show ?case
using gbinomial_Suc_Suc[of 0 m]
by (cases m) auto
next
case (Suc n)
then show ?case
using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m]
qed

lemma gbinomial_index_swap:
"((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (of_nat (m + n) gchoose m)"
by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])
also have "… = (of_nat (m + n) gchoose n)"
by (subst gbinomial_of_nat_symmetric) simp_all
also have "… = ?rhs"
by (subst gbinomial_negated_upper) simp
finally show ?thesis .
qed

lemma gbinomial_sum_lower_neg: "(∑k≤m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∑k≤m. -(r + 1) + of_nat k gchoose k)"
by (intro sum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)
also have "…  = - r + of_nat m gchoose m"
by (subst gbinomial_parallel_sum) simp
also have "… = ?rhs"
by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)
finally show ?thesis .
qed

lemma gbinomial_partial_row_sum:
"(∑k≤m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
proof (induct m)
case 0
then show ?case by simp
next
case (Suc mm)
then have "(∑k≤Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
(r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2"
also have "… = r * (r - 1 gchoose Suc mm) / 2"
by (subst gbinomial_absorb_comp) (rule refl)
also have "… = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
by (subst gbinomial_absorption [symmetric]) simp
finally show ?case .
qed

lemma sum_bounds_lt_plus1: "(∑k<mm. f (Suc k)) = (∑k=1..mm. f k)"
by (induct mm) simp_all

lemma gbinomial_partial_sum_poly:
"(∑k≤m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
(∑k≤m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))"
(is "?lhs m = ?rhs m")
proof (induction m)
case 0
then show ?case by simp
next
case (Suc mm)
define G where "G i k = (of_nat i + r gchoose k) * x^k * y^(i - k)" for i k
define S where "S = ?lhs"
have SG_def: "S = (λi. (∑k≤i. (G i k)))"
unfolding S_def G_def ..

have "S (Suc mm) = G (Suc mm) 0 + (∑k=Suc 0..Suc mm. G (Suc mm) k)"
also have "(∑k=Suc 0..Suc mm. G (Suc mm) k) = (∑k=0..mm. G (Suc mm) (Suc k))"
by (subst sum_shift_bounds_cl_Suc_ivl) simp
also have "… = (∑k=0..mm. ((of_nat mm + r gchoose (Suc k)) +
(of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"
unfolding G_def by (subst gbinomial_addition_formula) simp
also have "… = (∑k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) +
(∑k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
by (subst sum.distrib [symmetric]) (simp add: algebra_simps)
also have "(∑k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
(∑k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
by (simp only: atLeast0AtMost lessThan_Suc_atMost)
also have "… = (∑k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k)) +
(of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
(is "_ = ?A + ?B")
by (subst sum_lessThan_Suc) simp
also have "?A = (∑k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
proof (subst sum_bounds_lt_plus1 [symmetric], intro sum.cong[OF refl], clarify)
fix k
assume "k < mm"
then have "mm - k = mm - Suc k + 1"
by linarith
then show "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)"
by (simp only:)
qed
also have "… + ?B = y * (∑k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
unfolding G_def by (subst sum_distrib_left) (simp add: algebra_simps)
also have "(∑k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
unfolding S_def by (subst sum_distrib_left) (simp add: atLeast0AtMost algebra_simps)
also have "(G (Suc mm) 0) = y * (G mm 0)"
finally have "S (Suc mm) =
y * (G mm 0 + (∑k=1..mm. (G mm k))) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
also have "G mm 0 + (∑k=1..mm. (G mm k)) = S mm"
finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- r gchoose (Suc mm))"
by (subst gbinomial_negated_upper) simp
also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =
(- r gchoose (Suc mm)) * (-x) ^ Suc mm"
also have "(x + y) * S mm + … = (x + y) * ?rhs mm + (- r gchoose (Suc mm)) * (- x)^Suc mm"
unfolding S_def by (subst Suc.IH) simp
also have "(x + y) * ?rhs mm = (∑n≤mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
by (subst sum_distrib_left, rule sum.cong) (simp_all add: Suc_diff_le)
also have "… + (-r gchoose (Suc mm)) * (-x)^Suc mm =
(∑n≤Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))"
by simp
finally show ?case
by (simp only: S_def)
qed

lemma gbinomial_partial_sum_poly_xpos:
"(∑k≤m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
(∑k≤m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
apply (subst gbinomial_partial_sum_poly)
apply (subst gbinomial_negated_upper)
apply (intro sum.cong, rule refl)
done

lemma binomial_r_part_sum: "(∑k≤m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
proof -
have "2 * 2^(2*m) = (∑k = 0..(2 * m + 1). (2 * m + 1 choose k))"
using choose_row_sum[where n="2 * m + 1"] by simp
also have "(∑k = 0..(2 * m + 1). (2 * m + 1 choose k)) =
(∑k = 0..m. (2 * m + 1 choose k)) +
(∑k = m+1..2*m+1. (2 * m + 1 choose k))"
using sum_ub_add_nat[of 0 m "λk. 2 * m + 1 choose k" "m+1"]
also have "(∑k = m+1..2*m+1. (2 * m + 1 choose k)) =
(∑k = 0..m. (2 * m + 1 choose (k + (m + 1))))"
by (subst sum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
also have "… = (∑k = 0..m. (2 * m + 1 choose (m - k)))"
by (intro sum.cong[OF refl], subst binomial_symmetric) simp_all
also have "… = (∑k = 0..m. (2 * m + 1 choose k))"
using sum.atLeast_atMost_rev [of "λk. 2 * m + 1 choose (m - k)" 0 m]
by simp
also have "… + … = 2 * …"
by simp
finally show ?thesis
by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)
qed

lemma gbinomial_r_part_sum: "(∑k≤m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)"
(is "?lhs = ?rhs")
proof -
have "?lhs = of_nat (∑k≤m. (2 * m + 1) choose k)"
also have "… = of_nat (2 ^ (2 * m))"
by (subst binomial_r_part_sum) (rule refl)
finally show ?thesis by simp
qed

lemma gbinomial_sum_nat_pow2:
"(∑k≤m. (of_nat (m + k) gchoose k :: 'a::field_char_0) / 2 ^ k) = 2 ^ m"
(is "?lhs = ?rhs")
proof -
have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)"
by (induct m) simp_all
also have "… = (∑k≤m. (2 * (of_nat m) + 1 gchoose k))"
using gbinomial_r_part_sum ..
also have "… = (∑k≤m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"
using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]
also have "… = 2 ^ m * (∑k≤m. (of_nat (m + k) gchoose k) / 2 ^ k)"
by (subst sum_distrib_left) (simp add: algebra_simps power_diff)
finally show ?thesis
by (subst (asm) mult_left_cancel) simp_all
qed

lemma gbinomial_trinomial_revision:
assumes "k ≤ m"
shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
proof -
have "(r gchoose m) * (of_nat m gchoose k) = (r gchoose m) * fact m / (fact k * fact (m - k))"
using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
also have "… = (r gchoose k) * (r - of_nat k gchoose (m - k))"
using assms by (simp add: gbinomial_pochhammer power_diff pochhammer_product)
finally show ?thesis .
qed

text ‹Versions of the theorems above for the natural-number version of "choose"›
lemma binomial_altdef_of_nat:
"k ≤ n ⟹ of_nat (n choose k) = (∏i = 0..<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
for n k :: nat and x :: "'a::field_char_0"
by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)

lemma binomial_ge_n_over_k_pow_k: "k ≤ n ⟹ (of_nat n / of_nat k :: 'a) ^ k ≤ of_nat (n choose k)"
for k n :: nat and x :: "'a::linordered_field"
by (simp add: gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)

lemma binomial_le_pow:
assumes "r ≤ n"
shows "n choose r ≤ n ^ r"
proof -
have "n choose r ≤ fact n div fact (n - r)"
using assms by (subst binomial_fact_lemma[symmetric]) auto
with fact_div_fact_le_pow [OF assms] show ?thesis
by auto
qed

lemma binomial_altdef_nat: "k ≤ n ⟹ n choose k = fact n div (fact k * fact (n - k))"
for k n :: nat
by (subst binomial_fact_lemma [symmetric]) auto

lemma choose_dvd:
"k ≤ n ⟹ fact k * fact (n - k) dvd (fact n :: 'a::{semiring_div,linordered_semidom})"
unfolding dvd_def
apply (rule exI [where x="of_nat (n choose k)"])
using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
apply auto
done

lemma fact_fact_dvd_fact:
"fact k * fact n dvd (fact (k + n) :: 'a::{semiring_div,linordered_semidom})"

lemma choose_mult_lemma:
"((m + r + k) choose (m + k)) * ((m + k) choose k) = ((m + r + k) choose k) * ((m + r) choose m)"
(is "?lhs = _")
proof -
have "?lhs =
fact (m + r + k) div (fact (m + k) * fact (m + r - m)) * (fact (m + k) div (fact k * fact m))"
also have "… = fact (m + r + k) div (fact r * (fact k * fact m))"
apply (subst div_mult_div_if_dvd)
apply (auto simp: algebra_simps fact_fact_dvd_fact)
done
also have "… = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
apply (subst div_mult_div_if_dvd [symmetric])
apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)
done
also have "… =
(fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
apply (subst div_mult_div_if_dvd)
apply (auto simp: fact_fact_dvd_fact algebra_simps)
done
finally show ?thesis
qed

text ‹The "Subset of a Subset" identity.›
lemma choose_mult:
"k ≤ m ⟹ m ≤ n ⟹ (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))"
using choose_mult_lemma [of "m-k" "n-m" k] by simp

subsection ‹More on Binomial Coefficients›

lemma choose_one: "n choose 1 = n" for n :: nat
by simp

lemma card_UNION:
assumes "finite A"
and "∀k ∈ A. finite k"
shows "card (⋃A) = nat (∑I | I ⊆ A ∧ I ≠ {}. (- 1) ^ (card I + 1) * int (card (⋂I)))"
(is "?lhs = ?rhs")
proof -
have "?rhs = nat (∑I | I ⊆ A ∧ I ≠ {}. (- 1) ^ (card I + 1) * (∑_∈⋂I. 1))"
by simp
also have "… = nat (∑I | I ⊆ A ∧ I ≠ {}. (∑_∈⋂I. (- 1) ^ (card I + 1)))"
(is "_ = nat ?rhs")
by (subst sum_distrib_left) simp
also have "?rhs = (∑(I, _)∈Sigma {I. I ⊆ A ∧ I ≠ {}} Inter. (- 1) ^ (card I + 1))"
using assms by (subst sum.Sigma) auto
also have "… = (∑(x, I)∈(SIGMA x:UNIV. {I. I ⊆ A ∧ I ≠ {} ∧ x ∈ ⋂I}). (- 1) ^ (card I + 1))"
by (rule sum.reindex_cong [where l = "λ(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
also have "… = (∑(x, I)∈(SIGMA x:⋃A. {I. I ⊆ A ∧ I ≠ {} ∧ x ∈ ⋂I}). (- 1) ^ (card I + 1))"
using assms
by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="⋃A"])
also have "… = (∑x∈⋃A. (∑I|I ⊆ A ∧ I ≠ {} ∧ x ∈ ⋂I. (- 1) ^ (card I + 1)))"
using assms by (subst sum.Sigma) auto
also have "… = (∑_∈⋃A. 1)" (is "sum ?lhs _ = _")
proof (rule sum.cong[OF refl])
fix x
assume x: "x ∈ ⋃A"
define K where "K = {X ∈ A. x ∈ X}"
with ‹finite A› have K: "finite K"
by auto
let ?I = "λi. {I. I ⊆ A ∧ card I = i ∧ x ∈ ⋂I}"
have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
using assms by (auto intro!: inj_onI)
moreover have [symmetric]: "snd  (SIGMA i:{1..card A}. ?I i) = {I. I ⊆ A ∧ I ≠ {} ∧ x ∈ ⋂I}"
using assms
by (auto intro!: rev_image_eqI[where x="(card a, a)" for a]
dest: finite_subset intro: card_mono)
ultimately have "?lhs x = (∑(i, I)∈(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
by (rule sum.reindex_cong [where l = snd]) fastforce
also have "… = (∑i=1..card A. (∑I|I ⊆ A ∧ card I = i ∧ x ∈ ⋂I. (- 1) ^ (i + 1)))"
using assms by (subst sum.Sigma) auto
also have "… = (∑i=1..card A. (- 1) ^ (i + 1) * (∑I|I ⊆ A ∧ card I = i ∧ x ∈ ⋂I. 1))"
by (subst sum_distrib_left) simp
also have "… = (∑i=1..card K. (- 1) ^ (i + 1) * (∑I|I ⊆ K ∧ card I = i. 1))"
(is "_ = ?rhs")
proof (rule sum.mono_neutral_cong_right[rule_format])
show "finite {1..card A}"
by simp
show "{1..card K} ⊆ {1..card A}"
using ‹finite A› by (auto simp add: K_def intro: card_mono)
next
fix i
assume "i ∈ {1..card A} - {1..card K}"
then have i: "i ≤ card A" "card K < i"
by auto
have "{I. I ⊆ A ∧ card I = i ∧ x ∈ ⋂I} = {I. I ⊆ K ∧ card I = i}"
also have "… = {}"
using ‹finite A› i by (auto simp add: K_def dest: card_mono[rotated 1])
finally show "(- 1) ^ (i + 1) * (∑I | I ⊆ A ∧ card I = i ∧ x ∈ ⋂I. 1 :: int) = 0"
by (simp only:) simp
next
fix i
have "(∑I | I ⊆ A ∧ card I = i ∧ x ∈ ⋂I. 1) = (∑I | I ⊆ K ∧ card I = i. 1 :: int)"
(is "?lhs = ?rhs")
by (rule sum.cong) (auto simp add: K_def)
then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs"
by simp
qed
also have "{I. I ⊆ K ∧ card I = 0} = {{}}"
using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
then have "?rhs = (∑i = 0..card K. (- 1) ^ (i + 1) * (∑I | I ⊆ K ∧ card I = i. 1 :: int)) + 1"
also have "… = (∑i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
using K by (subst n_subsets[symmetric]) simp_all
also have "… = - (∑i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
by (subst sum_distrib_left[symmetric]) simp
also have "… =  - ((-1 + 1) ^ card K) + 1"
by (subst binomial_ring) (simp add: ac_simps)
also have "… = 1"
using x K by (auto simp add: K_def card_gt_0_iff)
finally show "?lhs x = 1" .
qed
also have "nat … = card (⋃A)"
by simp
finally show ?thesis ..
qed

text ‹The number of nat lists of length ‹m› summing to ‹N› is @{term "(N + m - 1) choose N"}:›
lemma card_length_sum_list_rec:
assumes "m ≥ 1"
shows "card {l::nat list. length l = m ∧ sum_list l = N} =
card {l. length l = (m - 1) ∧ sum_list l = N} +
card {l. length l = m ∧ sum_list l + 1 = N}"
(is "card ?C = card ?A + card ?B")
proof -
let ?A' = "{l. length l = m ∧ sum_list l = N ∧ hd l = 0}"
let ?B' = "{l. length l = m ∧ sum_list l = N ∧ hd l ≠ 0}"
let ?f = "λl. 0 # l"
let ?g = "λl. (hd l + 1) # tl l"
have 1: "xs ≠ [] ⟹ x = hd xs ⟹ x # tl xs = xs" for x :: nat and xs
by simp
have 2: "xs ≠ [] ⟹ sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
have f: "bij_betw ?f ?A ?A'"
apply (rule bij_betw_byWitness[where f' = tl])
using assms
apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
done
have 3: "xs ≠ [] ⟹ hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "λl. (hd l - 1) # tl l"])
using assms
by (auto simp: 2 length_0_conv[symmetric] intro!: 3
simp del: length_greater_0_conv length_0_conv)
have fin: "finite {xs. size xs = M ∧ set xs ⊆ {0..<N}}" for M N :: nat
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]
by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 ∧ set xs ⊆ {0..<N+1}}"])
(auto simp: member_le_sum_list less_Suc_eq_le)
have fin_B: "finite ?B"
by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m ∧ set xs ⊆ {0..<N}}"])
(auto simp: member_le_sum_list less_Suc_eq_le fin)
have uni: "?C = ?A' ∪ ?B'"
by auto
have disj: "?A' ∩ ?B' = {}" by blast
have "card ?C = card(?A' ∪ ?B')"
using uni by simp
also have "… = card ?A + card ?B"
using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
by presburger
finally show ?thesis .
qed

lemma card_length_sum_list: "card {l::nat list. size l = m ∧ sum_list l = N} = (N + m - 1) choose N"
― "by Holden Lee, tidied by Tobias Nipkow"
proof (cases m)
case 0
then show ?thesis
by (cases N) (auto cong: conj_cong)
next
case (Suc m')
have m: "m ≥ 1"
then show ?thesis
proof (induct "N + m - 1" arbitrary: N m)
case 0  ― "In the base case, the only solution is [0]."
have [simp]: "{l::nat list. length l = Suc 0 ∧ (∀n∈set l. n = 0)} = {[0]}"
by (auto simp: length_Suc_conv)
have "m = 1 ∧ N = 0"
using 0 by linarith
then show ?case
by simp
next
case (Suc k)
have c1: "card {l::nat list. size l = (m - 1) ∧ sum_list l =  N} = (N + (m - 1) - 1) choose N"
proof (cases "m = 1")
case True
with Suc.hyps have "N ≥ 1"
by auto
with True show ?thesis
next
case False
then show ?thesis
using Suc by fastforce
qed
from Suc have c2: "card {l::nat list. size l = m ∧ sum_list l + 1 = N} =
(if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
proof -
have *: "n > 0 ⟹ Suc m = n ⟷ m = n - 1" for m n
by arith
from Suc have "N > 0 ⟹
card {l::nat list. size l = m ∧ sum_list l + 1 = N} =
((N - 1) + m - 1) choose (N - 1)"
then show ?thesis
by auto
qed
from Suc.prems have "(card {l::nat list. size l = (m - 1) ∧ sum_list l = N} +
card {l::nat list. size l = m ∧ sum_list l + 1 = N}) = (N + m - 1) choose N"
by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
then show ?case
using card_length_sum_list_rec[OF Suc.prems] by auto
qed
qed

lemma card_disjoint_shuffle:
assumes "set xs ∩ set ys = {}"
shows   "card (shuffle xs ys) = (length xs + length ys) choose length xs"
using assms
proof (induction xs ys rule: shuffle.induct)
case (3 x xs y ys)
have "shuffle (x # xs) (y # ys) = op # x  shuffle xs (y # ys) ∪ op # y  shuffle (x # xs) ys"
by (rule shuffle.simps)
also have "card … = card (op # x  shuffle xs (y # ys)) + card (op # y  shuffle (x # xs) ys)"
by (rule card_Un_disjoint) (insert "3.prems", auto)
also have "card (op # x  shuffle xs (y # ys)) = card (shuffle xs (y # ys))"
by (rule card_image) auto
also have "… = (length xs + length (y # ys)) choose length xs"
using "3.prems" by (intro "3.IH") auto
also have "card (op # y  shuffle (x # xs) ys) = card (shuffle (x # xs) ys)"
by (rule card_image) auto
also have "… = (length (x # xs) + length ys) choose length (x # xs)"
using "3.prems" by (intro "3.IH") auto
also have "length xs + length (y # ys) choose length xs + … =
(length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
finally show ?case .
qed auto

lemma Suc_times_binomial_add: "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
― ‹by Lukas Bulwahn›
proof -
have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b
using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat]
by (simp only: fact_Suc add_Suc[symmetric] of_nat_id mult.assoc)
have "Suc a * (fact (Suc (a + b)) div (Suc a * fact a * fact b)) =
Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))"
by (subst div_mult_swap[symmetric]; simp only: mult.assoc dvd)
also have "… = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))"
by (simp only: div_mult_mult1)
also have "… = Suc b * (fact (Suc (a + b)) div (Suc b * (fact a * fact b)))"
using dvd[of b a] by (subst div_mult_swap[symmetric]; simp only: ac_simps dvd)
finally show ?thesis
by (subst (1 2) binomial_altdef_nat)
(simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
qed

subsection ‹Misc›

lemma gbinomial_code [code]:
"a gchoose n =
(if n = 0 then 1
else fold_atLeastAtMost_nat (λn acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
by (cases n)
atLeastLessThanSuc_atLeastAtMost)

declare [[code drop: binomial]]

lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op * ) (n-k+1) n 1 div fact k))"
proof -
{
assume "k ≤ n"
then have "{1..n} = {1..n-k} ∪ {n-k+1..n}" by auto
then have "(fact n :: nat) = fact (n-k) * ∏{n-k+1..n}"