Quelle Binomial.thy Sprache: Isabelle

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

section ‹Binomial Coefficients, Binomial Theorem, Inclusion-exclusion Principle›

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"
  where "binomial n k = card {K\Pow {0..

open_bundle binomial_syntax
begin
notation binomial  (infix ‹choose› 64)
end

lemma binomial_right_mono:
  assumes "m \ n" shows "m choose k \ n choose k"
proof -
  have "{K. K \ {0.. card K = k} \ {K. K \ {0.. card K = k}"
    using assms by auto
  then show ?thesis
    by (simp add: binomial_def card_mono)
qed

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..
    by (blast dest: ex_bij_betw_nat_finite)
  then have [simp]: "card (f ` C) = card C" if "C \ {0.. for C
    by (meson bij_betw_imp_inj_on bij_betw_subset card_image that)
  from bij have "bij_betw (image f) (Pow {0..
    by (rule bij_betw_Pow)
  then have "inj_on (image f) (Pow {0..
    by (rule bij_betw_imp_inj_on)
  moreover have "{K. K \ {0.. card K = k} \ Pow {0..
    by auto
  ultimately have "inj_on (image f) {K. K \ {0.. card K = k}"
    by (rule inj_on_subset)
  then have "card {K. K \ {0.. card K = k} =
      card (image f ` {K. K ⊆ {0..<card A} ∧ card K = k})" (is "_ = card ?C")
    by (simp add: card_image)
  also have "?C = {K. K \ f ` {0.. card K = k}"
    by (auto elim!: subset_imageE)
  also have "f ` {0..
    by (meson bij bij_betw_def)
  finally show ?thesis
    by (simp add: binomial_def)
qed

text ‹Recursive characterization›

lemma binomial_n_0 [simp]: "n choose 0 = 1"
proof -
  have "{K \ Pow {0..
    by (auto dest: finite_subset)
  then show ?thesis
    by (simp add: binomial_def)
qed

lemma binomial_0_Suc [simp]: "0 choose Suc k = 0"
  by (simp add: binomial_def)

lemma binomial_Suc_Suc [simp]: "Suc n choose Suc k = (n choose k) + (n choose Suc k)"
proof -
  let ?P = "\n k. {K. K \ {0.. 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..
      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_remove)
    qed
    show "K \ ?A \ K \ ?B"
      by (subst in_image_insert_iff)
        (auto simp add: card.insert_remove subset_eq_atLeast0_lessThan_finite
          Diff_subset_conv K_finite Suc_card_K)
  qed
  also have "{K\?Q. n \ K} = ?P n (Suc k)"
    by (auto simp add: atLeast0_lessThan_Suc)
  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_one: "n choose 1 = n" for n :: nat
  by simp

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"
proof (induction n arbitrary: k)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  show ?case
  proof (cases k)
    case (Suc k')
    then show ?thesis
      using Suc.IH
      by (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
  qed auto
qed

lemma binomial_le_pow2: "n choose k \ 2^n"
proof (induction n arbitrary: k)
  case 0
  then show ?case
    using le_less less_le_trans by fastforce
next
  case (Suc n)
  show ?case
  proof (cases k)
    case (Suc k')
    then show ?thesis
      using Suc.IH by (simp add: add_le_mono mult_2)
  qed auto
qed

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 (in comm_semiring_1) binomial_ring:
  "(a + b :: 'a)^n = (\k\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}" and decomp2: "{0..n} = {0} \ {1..n}"
    by auto
  have "(a + b)^(n+1) = (a + b) * (\k\n. of_nat (n choose k) * a^k * b^(n - k))"
    using Suc.hyps by simp
  also have "\ = a * (\k\n. of_nat (n choose k) * a^k * b^(n-k)) +
      b * (∑k≤n. of_nat (n choose k) * a^k * b^(n-k))"
    by (rule distrib_right)
  also have "\ = (\k\n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
      (∑k≤n. of_nat (n choose k) * a^k * b^(n - k + 1))"
    by (auto simp add: sum_distrib_left ac_simps)
  also have "\ = (\k\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: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum.cl_ivl_Suc)
  also have "\ = b^(n + 1) +
      (∑k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (a^(n + 1) +
      (∑k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)))"
      using sum.nat_ivl_Suc' [of 1 n "\k. of_nat (n choose (k-1)) * a ^ k * b ^ (n + 1 - k)"]
    by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0)
  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\n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
    using decomp by (simp add: atMost_atLeast0 field_simps)
  finally show ?case
    by simp
qed

text ‹Original version for the naturals.›
corollary binomial: "(a + b :: nat)^n = (\k\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: "\mx\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))"
      by (simp add: field_simps)
    also have "\ = (k + (m - h)) * fact m"
      using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
      by (simp add: field_simps)
    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]
  by (metis (mono_tags, lifting) fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left of_nat_fact of_nat_mult)

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 binomial_fact_pow: "(n choose s) * fact s \ n^s"
proof (cases "s \ n")
  case True
  then show ?thesis
    by (smt (verit) binomial_fact_lemma mult.assoc mult.commute fact_div_fact_le_pow fact_nonzero nonzero_mult_div_cancel_right)
qed (simp add: binomial_eq_0)

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
    by (simp add: binomial_fact')
qed

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

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

lemma sum_choose_upper: "(\k\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))"
    by (simp add: sum.distrib)
  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))"
    by (simp add: sum_subtractf)
  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

text‹NW diagonal sum property›
lemma sum_choose_diagonal:
  assumes "m \ n"
  shows "(\k\m. (n - k) choose (m - k)) = Suc n choose m"
proof -
  have "(\k\m. (n-k) choose (m - k)) = (\k\m. (n - m + k) choose k)"
    using sum.atLeastAtMost_rev [of "\k. (n - k) choose (m - k)" 0 m] assms
    by (simp add: atMost_atLeast0)
  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"  (infix ‹gchoose› 64)
  where gbinomial_prod_rev: "a gchoose k = (\i=0..

lemma gbinomial_0 [simp]:
  "a gchoose 0 = 1"
  "0 gchoose (Suc k) = 0"
  by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)

lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\i. a - of_nat i) {0..k} div fact (Suc k)"
  by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)

lemma gbinomial_1 [simp]: "a gchoose 1 = a"
  by (simp add: gbinomial_prod_rev lessThan_Suc)

lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a"
  by (simp add: gbinomial_prod_rev lessThan_Suc)

lemma gbinomial_0_left: "0 gchoose k = (if k = 0 then 1 else 0)"
  by (cases k) simp_all

lemma gbinomial_mult_fact: "fact k * (a gchoose k) = (\i = 0..
  for a :: "'a::field_char_0"
  by (simp_all add: gbinomial_prod_rev field_simps)

lemma gbinomial_mult_fact': "(a gchoose k) * fact k = (\i = 0..
  for a :: "'a::field_char_0"
  using gbinomial_mult_fact [of k a] by (simp add: ac_simps)

lemma gbinomial_pochhammer: "a gchoose k = (- 1) ^ k * pochhammer (- a) k / fact k"
  for a :: "'a::field_char_0"
proof (cases k)
  case (Suc k')
  then have "a gchoose k = pochhammer (a - of_nat k') (Suc k') / ((1 + of_nat k') * fact k')"
    by (simp add: gbinomial_prod_rev pochhammer_prod_rev atLeastLessThanSuc_atLeastAtMost
        prod.atLeast_Suc_atMost_Suc_shift of_nat_diff flip: power_mult_distrib prod.cl_ivl_Suc)
  then show ?thesis
    by (simp add: pochhammer_minus Suc)
qed auto

lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k"
  for a :: "'a::field_char_0"
proof -
  have "a gchoose k = ((-1)^k * (-1)^k) * pochhammer (a - of_nat k + 1) k / fact k"
    by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
  also have "(-1 :: 'a)^k * (-1)^k = 1"
    by (subst power_add [symmetric]) simp
  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"
    by (simp add: not_le)
  then have "0 \ ((-) n) ` {0..
    by auto
  then have "prod ((-) n) {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 ((-) n) {0..{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..
    by (simp add: fact_prod_rev)
  also have "\ = ((\i\{0.. {k..
    by (simp add: ivl_disj_un)
  finally have "fact n = (fact m * (\i = 0..
    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..
    by (simp add: n)
  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)"
  using gbinomial_binomial of_nat_gbinomial by auto

setup
  ‹Sign.add_const_constraint (🍋‹gbinomial›, SOME 🍋‹'a::field_char_0 \ nat \ 'a›)›

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

lemma gbinomial_mult_1':
  "(a gchoose k) * a = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))"
  for a :: "'a::field_char_0"
  by (simp add: mult.commute gbinomial_mult_1)

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)"
  proof (rule prod.reindex_cong)
    show "{1..k} = Suc ` {0..h}"
      using Suc by (auto simp add: image_Suc_atMost)
  qed auto
  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)"
    by (metis atLeastLessThanSuc_atLeastAtMost fact_Suc gbinomial_mult_fact mult.commute of_nat_fact of_nat_mult)
  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))"
    by (simp add: field_simps)
  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
    by (simp add: Suc prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc)
  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"
  by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)

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))"
    by (simp add: Suc)
  also have "\ = Suc m * 2 ^ m"
    unfolding sum.atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric]
    by (simp add: choose_row_sum)
  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))"
    by (simp add: Suc)
  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))"
    proof (subst sum_distrib_left, rule sum.cong[OF refl], subst Suc_times_binomial)
    qed (simp add: algebra_simps)
  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"
    by simp
  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)
           = of_nat (n choose 0) * pochhammer a 0 * pochhammer b (Suc n - 0)
           + (∑i = Suc 0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
    unfolding sum.shift_bounds_cl_Suc_ivl by (simp add: atLeast0AtMost)
  also have "\ = (\i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
    by (simp add: sum.atLeast_Suc_atMost)
  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 (simp 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)"
    by (simp add: pochhammer_rec algebra_simps)
  finally show ?case ..
qed

text ‹Contributed by Manuel Eberl, generalised by LCP.
  Alternative definition of the binomial coefficient as 🍋‹∏i<k. (n - i) / (k - i)›.›
lemma gbinomial_altdef_of_nat: "a gchoose k = (\i = 0..
  for k :: nat and a :: "'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 a :: "'a::linordered_field"
  assumes "of_nat k \ a"
  shows "(a / of_nat k :: 'a) ^ k \ a gchoose k"
proof -
  have x: "0 \ a"
    using assms of_nat_0_le_iff order_trans by blast
  have "(a / of_nat k :: 'a) ^ k = (\i = 0..
    by simp
  also have "\ \ a gchoose k"
  proof -
    have "\i. i < k \ 0 \ a / of_nat k"
      by (simp add: x zero_le_divide_iff)
    moreover have "a / of_nat k \ (a - of_nat i) / of_nat (k - i)" if "i < k" for i
    proof -
      from assms have "a * 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 "a * of_nat k - a * of_nat i \ a * of_nat k - of_nat (i * k)"
        by arith
      then have "a * of_nat (k - i) \ (a - of_nat i) * of_nat k"
        using ‹i < k› by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)
      then have "a * of_nat (k - i) \ (a - of_nat i) * (of_nat k :: 'a)"
        by blast
      with assms show ?thesis
        using ‹i < k› by (simp add: field_simps)
    qed
    ultimately show ?thesis
      unfolding gbinomial_altdef_of_nat
      by (intro prod_mono) auto
  qed
  finally show ?thesis .
qed

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

lemma gbinomial_minus: "((-a) gchoose k) = (-1) ^ k * ((a + of_nat k - 1) gchoose k)"
  by (metis add.commute diff_minus_eq_add gbinomial_negated_upper)

lemma Suc_times_gbinomial: "of_nat (Suc k) * ((a + 1) gchoose (Suc k)) = (a + 1) * (a gchoose k)"
proof (cases k)
  case 0
  then show ?thesis by simp
next
  case Suc
  have "((a + 1) gchoose (Suc k)) = (\i = 0..k. a + (1 - of_nat i)) / fact (Suc k)"
    by (simp add: add_diff_eq gbinomial_Suc)
  also have "(\i = 0..k. a + (1 - of_nat i)) = (a + 1) * (\i = 0..k-1. a - of_nat i)"
    by (simp add: Suc prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc)
  also have "\ / fact (Suc k) = (a + 1) / of_nat (Suc k) * (a gchoose k)"
    by (simp_all add: Suc gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
  finally show ?thesis
    using of_nat_neq_0 by auto
qed

lemma gbinomial_factors: "((a + 1) gchoose (Suc k)) = (a + 1) / of_nat (Suc k) * (a gchoose k)"
  by (metis Suc_times_gbinomial nonzero_mult_div_cancel_left of_nat_neq_0 times_divide_eq_left)

lemma gbinomial_rec: "((a + 1) gchoose (Suc k)) = (a gchoose k) * ((a + 1) / of_nat (Suc k))"
  by (simp add: gbinomial_factors mult.commute plus_1_eq_Suc)

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 🍋‹‹p.~157› in GKP_CM›):
\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]›
lemma gbinomial_absorption': "k > 0 \ a gchoose k = (a / of_nat k) * (a - 1 gchoose (k - 1))"
  using gbinomial_rec[of "a - 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 🍋‹‹p.~157› in GKP_CM›:
\[
k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
\]›
lemma gbinomial_absorption: "of_nat (Suc k) * (a gchoose Suc k) = a * ((a - 1) gchoose k)"
  by (metis Suc_times_gbinomial diff_eq_eq)

text ‹The absorption identity for natural number binomial coefficients:›
lemma binomial_absorption: "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
  using times_binomial_minus1_eq by fastforce

text ‹The absorption companion identity for natural number coefficients,
  following the proof by GKP 🍋‹‹p.~157› in GKP_CM›:›
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: "(a - of_nat k) * (a gchoose k) = a * ((a - 1) gchoose k)"
  using pochhammer_absorb_comp[of a k] by (simp add: gbinomial_pochhammer)

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

lemma binomial_addition_formula:
  "0 < n \ n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
  by (metis Suc_diff_1 add.commute binomial_Suc_Suc)

text ‹
  Equation 5.9 of the reference material 🍋‹‹p.~159› in GKP_CM› 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. (a + of_nat k) gchoose k) = (a + 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 "(a + of_nat m + 1)" m]
    by (simp add: add_ac)
qed

subsection ‹Summation on the upper index›

text ‹
  Another summation formula is equation 5.10 of the reference material 🍋‹‹p.~160› in GKP_CM›,
  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:
  "(\j = 0..n. (of_nat j gchoose k) :: 'a::field_char_0) = (of_nat n + 1) gchoose (k + 1)"
proof (induct n)
  case 0
  show ?case
    using gbinomial_Suc_Suc[of 0 k]
    by (cases k) auto
next
  case (Suc n)
  then show ?case
    using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" k]
    by (simp add: add_ac)
qed

lemma gbinomial_index_swap:
  "((-1) ^ k) * ((- (of_nat n) - 1) gchoose k) = ((-1) ^ n) * ((- (of_nat k) - 1) gchoose n)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (of_nat (k + n) gchoose k)"
    by (simp add: gbinomial_negated_upper [of "- of_nat n - 1"])
  also have "\ = (of_nat (k + n) gchoose n)"
    by (subst gbinomial_of_nat_symmetric; simp)
  also have "\ = ?rhs"
    by (subst gbinomial_negated_upper; simp)
  finally show ?thesis .
qed

lemma gbinomial_sum_lower_neg: "(\k\m. (a gchoose k) * (- 1) ^ k) = (- 1) ^ m * (a - 1 gchoose m)"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = (\k\m. -(a + 1) + of_nat k gchoose k)"
    by (simp add: gbinomial_negated_upper [of a] power_mult_distrib diff_add_eq mult.commute)
  also have "\ = - a + of_nat m gchoose m"
    by (simp add: gbinomial_parallel_sum)
  also have "\ = ?rhs"
    by (simp add: gbinomial_negated_upper [of "a-1"] power_mult_distrib)
  finally show ?thesis .
qed

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

lemma sum_bounds_lt_plus1: "(\kk=1..mm. f k)"
  by (induct mm) simp_all

lemma gbinomial_partial_sum_poly:
  "(\k\m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
    (∑k≤m. (-a 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 m)
  define G where "G i k = (of_nat i + a 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 m) = G (Suc m) 0 + (\k=Suc 0..Suc m. G (Suc m) k)"
    using SG_def by (simp add: sum.atLeast_Suc_atMost atLeast0AtMost [symmetric])
  also have "(\k=Suc 0..Suc m. G (Suc m) k) = (\k=0..m. G (Suc m) (Suc k))"
    by (subst sum.shift_bounds_cl_Suc_ivl) simp
  also have "\ = (\k=0..m. ((of_nat m + a gchoose (Suc k)) +
      (of_nat m + a gchoose k)) * x^(Suc k) * y^(m - k))"
    unfolding G_def by (subst gbinomial_addition_formula) simp
  also have "\ = (\k=0..m. (of_nat m + a gchoose (Suc k)) * x^(Suc k) * y^(m - k)) +
      (∑k=0..m. (of_nat m + a gchoose k) * x^(Suc k) * y^(m - k))"
    by (subst sum.distrib [symmetric]) (simp add: algebra_simps)
  also have "(\k=0..m. (of_nat m + a gchoose (Suc k)) * x^(Suc k) * y^(m - k)) =
      (∑k<Suc m. (of_nat m + a gchoose (Suc k)) * x^(Suc k) * y^(m - k))"
    by (simp only: atLeast0AtMost lessThan_Suc_atMost)
  also have "\ = (\k
      (of_nat m + a gchoose (Suc m)) * x^(Suc m)"
    (is "_ = ?A + ?B")
    by (subst sum.lessThan_Suc) simp
  also have "?A = (\k=1..m. (of_nat m + a gchoose k) * x^k * y^(m - k + 1))"
  proof (subst sum_bounds_lt_plus1 [symmetric], intro sum.cong[OF refl], clarify)
    fix k
    assume "k < m"
    then have "m - k = m - Suc k + 1"
      by linarith
    then show "(of_nat m + a gchoose Suc k) * x ^ Suc k * y ^ (m - k) =
        (of_nat m + a gchoose Suc k) * x ^ Suc k * y ^ (m - Suc k + 1)"
      by (simp only:)
  qed
  also have "\ + ?B = y * (\k=1..m. (G m k)) + (of_nat m + a gchoose (Suc m)) * x^(Suc m)"
    unfolding G_def by (simp add: sum_distrib_left algebra_simps)
  also have "(\k=0..m. (of_nat m + a gchoose k) * x^(Suc k) * y^(m - k)) = x * (S m)"
    unfolding S_def by (simp add: sum_distrib_left atLeast0AtMost algebra_simps)
  also have "(G (Suc m) 0) = y * (G m 0)"
    by (simp add: G_def)
  finally have "S (Suc m) =
      y * (G m 0 + (∑k=1..m. (G m k))) + (of_nat m + a gchoose (Suc m)) * x^(Suc m) + x * (S m)"
    by (simp add: ring_distribs)
  also have "G m 0 + (\k=1..m. (G m k)) = S m"
    by (simp add: SG_def atLeast0AtMost flip: sum.atLeast_Suc_atMost)
  finally have "S (Suc m) = (x + y) * (S m) + (of_nat m + a gchoose (Suc m)) * x^(Suc m)"
    by (simp add: algebra_simps)
  also have "(of_nat m + a gchoose (Suc m)) = (-1) ^ (Suc m) * (- a gchoose (Suc m))"
    by (subst gbinomial_negated_upper) simp
  also have "(-1) ^ Suc m * (- a gchoose Suc m) * x ^ Suc m = (- a gchoose (Suc m)) * (-x) ^ Suc m"
    by (simp add: power_minus[of x])
  also have "(x + y) * S m + \ = (x + y) * ?rhs m + (- a gchoose (Suc m)) * (- x)^Suc m"
    unfolding S_def by (simp add: Suc.IH)
  also have "(x + y) * ?rhs m = (\n\m. ((- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc m - n)))"
    by (auto simp: Suc_diff_le sum_distrib_left intro!: sum.cong)
  also have "\ + (-a gchoose (Suc m)) * (-x)^Suc m =
      (∑n≤Suc m. (- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc m - n))"
    by simp
  finally show ?case
    by (simp only: S_def)
qed

lemma gbinomial_partial_sum_poly_xpos:
    "(\k\m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
     (∑k≤m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))" (is "?lhs = ?rhs")
proof -
  have "?lhs = (\k\m. (- a gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
    by (simp add: gbinomial_partial_sum_poly)
  also have "\ = (\k\m. (-1) ^ k * (of_nat k - - a - 1 gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
    by (metis (no_types, opaque_lifting) gbinomial_negated_upper)
  also have "\ = ?rhs"
    by (auto simp flip: power_mult_distrib intro: sum.cong)
  finally show ?thesis .
qed

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 add: atMost_atLeast0)
  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"]
    by (simp add: mult_2)
  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.atLeastAtMost_rev [of "\k. 2 * m + 1 choose (m - k)" 0 m]
    by simp
  also have "\ + \ = 2 * \"
    by simp
  finally show ?thesis
    by (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)"
    by (simp add: binomial_gbinomial add_ac)
  also have "\ = of_nat (2 ^ (2 * m))"
    using binomial_r_part_sum by presburger
  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 a="of_nat m + 1" and m="m"]
    by (simp add: add_ac)
  also have "\ = 2 ^ m * (\k\m. (of_nat (m + k) gchoose k) / 2 ^ k)"
    by (simp add: sum_distrib_left algebra_simps power_diff)
  finally show ?thesis
    by (subst (asm) mult_left_cancel) simp_all
qed

lemma gbinomial_trinomial_revision:
  assumes "k \ m"
  shows "(a gchoose m) * (of_nat m gchoose k) = (a gchoose k) * (a - of_nat k gchoose (m - k))"
proof -
  have "(a gchoose m) * (of_nat m gchoose k) = (a gchoose m) * fact m / (fact k * fact (m - k))"
    using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
  also have "\ = (a gchoose k) * (a - 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..
  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: binomial_gbinomial gbinomial_ge_n_over_k_pow_k)

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 choose_dvd:
  assumes "k \ n" shows "fact k * fact (n - k) dvd (fact n)"
  by (metis assms binomial_fact_lemma dvd_def of_nat_fact of_nat_mult)

lemma fact_fact_dvd_fact:
  "fact k * fact n dvd (fact (k + n))"
  by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)

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))"
    by (simp add: binomial_fact')
  also have "\ = fact (m + r + k) * fact (m + k) div
                 (fact (m + k) * fact (m + r - m) * (fact k * fact m))"
    by (metis add_implies_diff add_le_mono1 choose_dvd diff_cancel2 div_mult_div_if_dvd le_add1 le_add2)
  also have "\ = fact (m + r + k) div (fact r * (fact k * fact m))"
    by (auto simp: algebra_simps fact_fact_dvd_fact)
  also have "\ = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
    by simp
  also have "\ =
      (fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
    by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
  finally show ?thesis
    by (simp add: binomial_fact' mult.commute)
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

lemma of_nat_binomial_eq_mult_binomial_Suc:
  assumes "k \ n"
  shows "(of_nat :: (nat \ ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
proof (cases k)
  case 0 then show ?thesis
    using of_nat_neq_0 by auto
next
  case (Suc l)
  have "of_nat (n + 1) * (\i=0.. 'a)) (n + 1 - k) * (\i=0..
    using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\i. of_nat (Suc n - i)" k]
    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
  also have "\ = (of_nat :: (nat \ 'a)) (Suc n - k) * (\i=0..
    by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
  also have "\ = (of_nat :: (nat \ 'a)) (n + 1 - k) * (\i=0..
    by (simp only: Suc_eq_plus1)
  finally have "(\i=0.. 'a)) (n + 1 - k) / of_nat (n + 1) * (\i=0..
    using of_nat_neq_0 by (auto simp: mult.commute divide_simps)
  with assms show ?thesis
    by (simp add: binomial_altdef_of_nat prod_dividef)
qed

subsection ‹More on Binomial Coefficients›

text ‹The number of nat lists of length ‹m› summing to ‹N› is 🍋‹(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"
    by (auto simp add: neq_Nil_conv)
  have f: "bij_betw ?f ?A ?A'"
    by (rule bij_betw_byWitness[where f' = tl]) (use assms in \auto simp: 2 1 simp flip: length_0_conv\)
  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 simp flip: length_0_conv intro!: 3)
  have fin: "finite {xs. size xs = M \ set xs \ {0.. 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..])
      (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..])
      (auto simp: member_le_sum_list less_Suc_eq_le fin)
  have disj: "?A' \ ?B' = {}" by blast
  have "?C = ?A' \ ?B'"
    by auto
  then have "card ?C = card(?A' \ ?B')"
    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"
    by (simp add: Suc)
  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
        by (simp add: binomial_eq_0)
    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)"
        by (simp add: *)
      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_shuffles:
  assumes "set xs \ set ys = {}"
  shows   "card (shuffles xs ys) = (length xs + length ys) choose length xs"
using assms
proof (induction xs ys rule: shuffles.induct)
  case (3 x xs y ys)
  have "shuffles (x # xs) (y # ys) = (#) x ` shuffles xs (y # ys) \ (#) y ` shuffles (x # xs) ys"
    by (rule shuffles.simps)
  also have "card \ = card ((#) x ` shuffles xs (y # ys)) + card ((#) y ` shuffles (x # xs) ys)"
    by (rule card_Un_disjoint) (use 3 in auto)
  also have "card ((#) x ` shuffles xs (y # ys)) = card (shuffles 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 ((#) y ` shuffles (x # xs) ys) = card (shuffles (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"]
    by (metis add.commute add_Suc_right fact_Suc id_apply mult.assoc of_nat_eq_id)
  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 (metis mult.assoc div_mult_swap 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)))"
    by (metis add.commute div_mult_swap dvd mult.commute)
  finally show ?thesis
    by (metis Suc_diff_le Suc_eq_plus1 Suc_times_binomial add.commute binomial_absorb_comp diff_add_inverse le_add1)
qed

subsection ‹Inclusion-exclusion principle›

text ‹Ported from HOL Light by lcp›

lemma Inter_over_Union:
  "\ {\ (\ x) |x. x \ S} = \ {\ (G ` S) |G. \x\S. G x \ \ x}"
proof -
  have "\x. \s\S. \X \ \ s. x \ X \ \G. (\x\S. G x \ \ x) \ (\s\S. x \ G s)"
    by metis
  then show ?thesis
    by (auto simp flip: all_simps ex_simps)
qed

lemma subset_insert_lemma:
  "{T. T \ (insert a S) \ P T} = {T. T \ S \ P T} \ {insert a T |T. T \ S \ P(insert a T)}" (is "?L=?R")
proof
  show "?L \ ?R"
    by (smt (verit) UnI1 UnI2 insert_Diff mem_Collect_eq subsetI subset_insert_iff)
qed blast

text‹Versions for additive real functions, where the additivity applies only to some
specific subsets (e.g. cardinality of finite sets, measurable sets with bounded measure.
(From HOL Light)›

locale Incl_Excl =
  fixes P :: "'a set \ bool" and f :: "'a set \ 'b::ring_1"
  assumes disj_add: "\P S; P T; disjnt S T\ \ f(S \ T) = f S + f T"
    and empty: "P{}"
    and Int: "\P S; P T\ \ P(S \ T)"
    and Un: "\P S; P T\ \ P(S \ T)"
    and Diff: "\P S; P T\ \ P(S - T)"

begin

lemma f_empty [simp]: "f{} = 0"
  using disj_add empty by fastforce

lemma f_Un_Int: "\P S; P T\ \ f(S \ T) + f(S \ T) = f S + f T"
  by (smt (verit, ccfv_threshold) Groups.add_ac(2) Incl_Excl.Diff Incl_Excl.Int Incl_Excl_axioms Int_Diff_Un Int_Diff_disjoint Int_absorb Un_Diff Un_Int_eq(2) disj_add disjnt_def group_cancel.add2 sup_bot.right_neutral)

lemma restricted_indexed:
  assumes "finite A" and X: "\a. a \ A \ P(X a)"
  shows "f(\(X ` A)) = (\B | B \ A \ B \ {}. (- 1) ^ (card B + 1) * f (\ (X ` B)))"
proof -
  have "\finite A; card A = n; \a \ A. P (X a)\
              ==> f(∪(X ` A)) = (∑B | B ⊆ A ∧ B ≠ {}. (- 1) ^ (card B + 1) * f (∩ (X ` B)))" for n X and A :: "'c set"
  proof (induction n arbitrary: A X rule: less_induct)
    case (less n0 A0 X)
    show ?case
    proof (cases "n0=0")
      case True
      with less show ?thesis
       by fastforce
    next
      case False
      with less.prems obtain A n a where *: "n0 = Suc n" "A0 = insert a A" "a \ A" "card A = n" "finite A"
        by (metis card_Suc_eq_finite not0_implies_Suc)
      with less have "P (X a)" by blast
      have APX: "\a \ A. P (X a)"
        by (simp add: "*" less.prems)
      have PUXA: "P (\ (X ` A))"
        using ‹finite A› APX
        by (induction) (auto simp: empty Un)
      have "f (\ (X ` A0)) = f (X a \ \ (X ` A))"
        by (simp add: *)
      also have "\ = f (X a) + f (\ (X ` A)) - f (X a \ \ (X ` A))"
        using f_Un_Int add_diff_cancel PUXA ‹P (X a)› by metis
      also have "\ = f (X a) - (\B | B \ A \ B \ {}. (- 1) ^ card B * f (\ (X ` B))) +
                       (∑B | B ⊆ A ∧ B ≠ {}. (- 1) ^ card B * f (X a ∩ ∩ (X ` B)))"
      proof -
        have 1: "f (\i\A. X a \ X i) = (\B | B \ A \ B \ {}. (- 1) ^ (card B + 1) * f (\b\B. X a \ X b))"
          using less.IH [of n A "\i. X a \ X i"] APX Int ‹P (X a)›  by (simp add: *)
        have 2: "X a \ \ (X ` A) = (\i\A. X a \ X i)"
          by auto
        have 3: "f (\ (X ` A)) = (\B | B \ A \ B \ {}. (- 1) ^ (card B + 1) * f (\ (X ` B)))"
          using less.IH [of n A X] APX Int ‹P (X a)›  by (simp add: *)
        show ?thesis
          unfolding 3 2 1
          by (simp add: sum_negf)
      qed
      also have "\ = (\B | B \ A0 \ B \ {}. (- 1) ^ (card B + 1) * f (\ (X ` B)))"
      proof -
         have F: "{insert a B |B. B \ A} = insert a ` Pow A \ {B. B \ A \ B \ {}} = Pow A - {{}}"
          by auto
        have G: "(\B\Pow A. (- 1) ^ card (insert a B) * f (X a \ \ (X ` B))) = (\B\Pow A. - ((- 1) ^ card B * f (X a \ \ (X ` B))))"
        proof (rule sum.cong [OF refl])
          fix B
          assume B: "B \ Pow A"
          then have "finite B"
            using ‹finite A› finite_subset by auto
          show "(- 1) ^ card (insert a B) * f (X a \ \ (X ` B)) = - ((- 1) ^ card B * f (X a \ \ (X ` B)))"
            using B * by (auto simp add: card_insert_if ‹finite B›)
        qed
        have disj: "{B. B \ A \ B \ {}} \ {insert a B |B. B \ A} = {}"
          using * by blast
        have inj: "inj_on (insert a) (Pow A)"
          using "*" inj_on_def by fastforce
        show ?thesis
          apply (simp add: * subset_insert_lemma sum.union_disjoint disj sum_negf)
          apply (simp add: F G sum_negf sum.reindex [OF inj] o_def sum_diff *)
          done
      qed
      finally show ?thesis .
    qed
  qed
  then show ?thesis
    by (meson assms)
qed

lemma restricted:
  assumes "finite A" "\a. a \ A \ P a"
  shows  "f(\ A) = (\B | B \ A \ B \ {}. (- 1) ^ (card B + 1) * f (\ B))"
  using restricted_indexed [of A "\x. x"] assms by auto

end

subsection‹Versions for unrestrictedly additive functions›

lemma Incl_Excl_UN:
  fixes f :: "'a set \ 'b::ring_1"
  assumes "\S T. disjnt S T \ f(S \ T) = f S + f T" "finite A"
  shows "f(\(G ` A)) = (\B | B \ A \ B \ {}. (-1) ^ (card B + 1) * f (\ (G ` B)))"
proof -
  interpret Incl_Excl "\x. True" f
    by (simp add: Incl_Excl.intro assms(1))
  show ?thesis
    using restricted_indexed assms by blast
qed

lemma Incl_Excl_Union:
  fixes f :: "'a set \ 'b::ring_1"
  assumes "\S T. disjnt S T \ f(S \ T) = f S + f T" "finite A"
  shows "f(\ A) = (\B | B \ A \ B \ {}. (- 1) ^ (card B + 1) * f (\ B))"
  using Incl_Excl_UN[of f A "\X. X"] assms by simp

text ‹The famous inclusion-exclusion formula for the cardinality of a union›
lemma int_card_UNION:
  assumes "finite A" "\K. K \ A \ finite K"
  shows "int (card (\A)) = (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * int (card (\I)))"
proof -
  interpret Incl_Excl finite "int o card"
  proof qed (auto simp add: card_Un_disjnt)
  show ?thesis
    using restricted assms by auto
qed

text‹A more conventional form›
lemma inclusion_exclusion:
  assumes "finite A" "\K. K \ A \ finite K"
  shows "int(card(\ A)) =
         (∑n=1..card A. (-1) ^ (Suc n) * (∑B | B ⊆ A ∧ card B = n. int (card (∩ B))))" (is "_=?R")
proof -
  have fin: "finite {I. I \ A \ I \ {}}"
    by (simp add: assms)
  have "\k. \Suc 0 \ k; k \ card A\ \ \B\A. B \ {} \ k = card B"
    by (metis (mono_tags, lifting) Suc_le_D Zero_neq_Suc card_eq_0_iff obtain_subset_with_card_n)
  with ‹finite A› finite_subset
  have card_eq: "card ` {I. I \ A \ I \ {}} = {1..card A}"
    using not_less_eq_eq card_mono by (fastforce simp: image_iff)
  have "int(card(\ A))
      = (∑y = 1..card A. ∑I∈{x. x ⊆ A ∧ x ≠ {} ∧ card x = y}. - ((- 1) ^ y * int (card (∩ I))))"
    by (simp add: int_card_UNION assms sum.image_gen [OF fin, where g=card] card_eq)
  also have "\ = ?R"
  proof -
    have "{B. B \ A \ B \ {} \ card B = k} = {B. B \ A \ card B = k}"
      if "Suc 0 \ k" and "k \ card A" for k
      using that by auto
    then show ?thesis
      by (clarsimp simp add: sum_negf simp flip: sum_distrib_left)
  qed
  finally show ?thesis .
qed

lemma card_UNION:
  assumes "finite A" and "\K. K \ A \ finite K"
  shows "card (\A) = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * int (card (\I)))"
  by (simp only: flip: int_card_UNION [OF assms])

lemma card_UNION_nonneg:
  assumes "finite A" and "\K. K \ A \ finite K"
  shows "(\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * int (card (\I))) \ 0"
  using int_card_UNION [OF assms] by presburger

subsection ‹General "Moebius inversion" inclusion-exclusion principle›

text ‹This "symmetric" form is from Ira Gessel: "Symmetric Inclusion-Exclusion" ›

lemma sum_Un_eq:
   "\S \ T = {}; S \ T = U; finite U\
           ==> (sum f S + sum f T = sum f U)"
  by (metis finite_Un sum.union_disjoint)

lemma card_adjust_lemma: "\inj_on f S; x = y + card (f ` S)\ \ x = y + card S"
  by (simp add: card_image)

lemma card_subsets_step:
  assumes "finite S" "x \ S" "U \ S"
  shows "card {T. T \ (insert x S) \ U \ T \ odd(card T)}
       = card {T. T ⊆ S ∧ U ⊆ T ∧ odd(card T)} + card {T. T ⊆ S ∧ U ⊆ T ∧ even(card T)} ∧
         card {T. T ⊆ (insert x S) ∧ U ⊆ T ∧ even(card T)}
       = card {T. T ⊆ S ∧ U ⊆ T ∧ even(card T)} + card {T. T ⊆ S ∧ U ⊆ T ∧ odd(card T)}"
proof -
  have inj: "inj_on (insert x) {T. T \ S \ P T}" for P
    using assms by (auto simp: inj_on_def)
  have [simp]: "finite {T. T \ S \ P T}"  "finite (insert x ` {T. T \ S \ P T})" for P
    using ‹finite S› by auto
  have [simp]: "disjnt {T. T \ S \ P T} (insert x ` {T. T \ S \ Q T})" for P Q
    using assms by (auto simp: disjnt_iff)
  have eq: "{T. T \ S \ U \ T \ P T} \ insert x ` {T. T \ S \ U \ T \ Q T}
          = {T. T ⊆ insert x S ∧ U ⊆ T ∧ P T}" (is "?L = ?R")
    if "\A. A \ S \ Q (insert x A) \ P A" "\A. \ Q A \ P A" for P Q
  proof
    show "?L \ ?R"
      by (clarsimp simp: image_iff subset_iff) (meson subsetI that)
    show "?R \ ?L"
      using ‹U ⊆ S›
      by (clarsimp simp: image_iff) (smt (verit) insert_iff mk_disjoint_insert subset_iff that)
  qed
  have [simp]: "\A. A \ S \ even (card (insert x A)) \ odd (card A)"
    by (metis ‹finite S› ‹x ∉ S› card_insert_disjoint even_Suc finite_subset subsetD)
  show ?thesis
    by (intro conjI card_adjust_lemma [OF inj]; simp add: eq flip: card_Un_disjnt)
qed

lemma card_subsupersets_even_odd:
  assumes "finite S" "U \ S"
  shows "card {T. T \ S \ U \ T \ even(card T)}
       = card {T. T ⊆ S ∧ U ⊆ T ∧ odd(card T)}"
  using assms
proof (induction "card S" arbitrary: S rule: less_induct)
  case (less S)
  then obtain x where "x \ U" "x \ S"
    by blast
  then have U: "U \ S - {x}"
    using less.prems(2) by blast
  let ?V = "S - {x}"
  show ?case
    using card_subsets_step [of ?V x U] less.prems U
    by (simp add: insert_absorb ‹x ∈ S›)
qed

lemma sum_alternating_cancels:
  assumes "finite S" "card {x. x \ S \ even(f x)} = card {x. x \ S \ odd(f x)}"
  shows "(\x\S. (-1) ^ f x) = (0::'b::ring_1)"
proof -
  have "(\x\S. (-1) ^ f x)
      = (∑x | x ∈ S ∧ even (f x). (-1) ^ f x) + (∑x | x ∈ S ∧ odd (f x). (-1) ^ f x)"
    by (rule sum_Un_eq [symmetric]; force simp: ‹finite S›)
  also have "\ = (0::'b::ring_1)"
    by (simp add: minus_one_power_iff assms cong: conj_cong)
  finally show ?thesis .
qed

lemma inclusion_exclusion_symmetric:
  fixes f :: "'a set \ 'b::ring_1"
--> --------------------

--> maximum size reached

--> --------------------

Messung V0.5

¤ Dauer der Verarbeitung: 0.40 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.