1(* Title: HOL/Binomial.thy 2 Author: Jacques D. Fleuriot 3 Author: Lawrence C Paulson 4 Author: Jeremy Avigad 5 Author: Chaitanya Mangla 6 Author: Manuel Eberl 7*) 8 9section \<open>Binomial Coefficients and Binomial Theorem\<close> 10 11theory Binomial 12 imports Presburger Factorial 13begin 14 15subsection \<open>Binomial coefficients\<close> 16 17text \<open>This development is based on the work of Andy Gordon and Florian Kammueller.\<close> 18 19text \<open>Combinatorial definition\<close> 20 21definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) 22 where "n choose k = card {K\<in>Pow {0..<n}. card K = k}" 23 24theorem n_subsets: 25 assumes "finite A" 26 shows "card {B. B \<subseteq> A \<and> card B = k} = card A choose k" 27proof - 28 from assms obtain f where bij: "bij_betw f {0..<card A} A" 29 by (blast dest: ex_bij_betw_nat_finite) 30 then have [simp]: "card (f ` C) = card C" if "C \<subseteq> {0..<card A}" for C 31 by (meson bij_betw_imp_inj_on bij_betw_subset card_image that) 32 from bij have "bij_betw (image f) (Pow {0..<card A}) (Pow A)" 33 by (rule bij_betw_Pow) 34 then have "inj_on (image f) (Pow {0..<card A})" 35 by (rule bij_betw_imp_inj_on) 36 moreover have "{K. K \<subseteq> {0..<card A} \<and> card K = k} \<subseteq> Pow {0..<card A}" 37 by auto 38 ultimately have "inj_on (image f) {K. K \<subseteq> {0..<card A} \<and> card K = k}" 39 by (rule inj_on_subset) 40 then have "card {K. K \<subseteq> {0..<card A} \<and> card K = k} = 41 card (image f ` {K. K \<subseteq> {0..<card A} \<and> card K = k})" (is "_ = card ?C") 42 by (simp add: card_image) 43 also have "?C = {K. K \<subseteq> f ` {0..<card A} \<and> card K = k}" 44 by (auto elim!: subset_imageE) 45 also have "f ` {0..<card A} = A" 46 by (meson bij bij_betw_def) 47 finally show ?thesis 48 by (simp add: binomial_def) 49qed 50 51text \<open>Recursive characterization\<close> 52 53lemma binomial_n_0 [simp]: "n choose 0 = 1" 54proof - 55 have "{K \<in> Pow {0..<n}. card K = 0} = {{}}" 56 by (auto dest: finite_subset) 57 then show ?thesis 58 by (simp add: binomial_def) 59qed 60 61lemma binomial_0_Suc [simp]: "0 choose Suc k = 0" 62 by (simp add: binomial_def) 63 64lemma binomial_Suc_Suc [simp]: "Suc n choose Suc k = (n choose k) + (n choose Suc k)" 65proof - 66 let ?P = "\<lambda>n k. {K. K \<subseteq> {0..<n} \<and> card K = k}" 67 let ?Q = "?P (Suc n) (Suc k)" 68 have inj: "inj_on (insert n) (?P n k)" 69 by rule (auto; metis atLeastLessThan_iff insert_iff less_irrefl subsetCE) 70 have disjoint: "insert n ` ?P n k \<inter> ?P n (Suc k) = {}" 71 by auto 72 have "?Q = {K\<in>?Q. n \<in> K} \<union> {K\<in>?Q. n \<notin> K}" 73 by auto 74 also have "{K\<in>?Q. n \<in> K} = insert n ` ?P n k" (is "?A = ?B") 75 proof (rule set_eqI) 76 fix K 77 have K_finite: "finite K" if "K \<subseteq> insert n {0..<n}" 78 using that by (rule finite_subset) simp_all 79 have Suc_card_K: "Suc (card K - Suc 0) = card K" if "n \<in> K" 80 and "finite K" 81 proof - 82 from \<open>n \<in> K\<close> obtain L where "K = insert n L" and "n \<notin> L" 83 by (blast elim: Set.set_insert) 84 with that show ?thesis by (simp add: card_insert) 85 qed 86 show "K \<in> ?A \<longleftrightarrow> K \<in> ?B" 87 by (subst in_image_insert_iff) 88 (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite 89 Diff_subset_conv K_finite Suc_card_K) 90 qed 91 also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)" 92 by (auto simp add: atLeast0_lessThan_Suc) 93 finally show ?thesis using inj disjoint 94 by (simp add: binomial_def card_Un_disjoint card_image) 95qed 96 97lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0" 98 by (auto simp add: binomial_def dest: subset_eq_atLeast0_lessThan_card) 99 100lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0" 101 by (induct n k rule: diff_induct) simp_all 102 103lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k" 104 by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) 105 106lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n" 107 by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial) 108 109lemma binomial_n_n [simp]: "n choose n = 1" 110 by (induct n) (simp_all add: binomial_eq_0) 111 112lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n" 113 by (induct n) simp_all 114 115lemma binomial_1 [simp]: "n choose Suc 0 = n" 116 by (induct n) simp_all 117 118lemma choose_reduce_nat: 119 "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> 120 n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)" 121 using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp 122 123lemma Suc_times_binomial_eq: "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" 124 apply (induct n arbitrary: k) 125 apply simp 126 apply arith 127 apply (case_tac k) 128 apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) 129 done 130 131lemma binomial_le_pow2: "n choose k \<le> 2^n" 132 apply (induct n arbitrary: k) 133 apply (case_tac k) 134 apply simp_all 135 apply (case_tac k) 136 apply auto 137 apply (simp add: add_le_mono mult_2) 138 done 139 140text \<open>The absorption property.\<close> 141lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)" 142 using Suc_times_binomial_eq by auto 143 144text \<open>This is the well-known version of absorption, but it's harder to use 145 because of the need to reason about division.\<close> 146lemma binomial_Suc_Suc_eq_times: "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" 147 by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) 148 149text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close> 150lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))" 151 using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"] 152 by (auto split: nat_diff_split) 153 154 155subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close> 156 157text \<open>Avigad's version, generalized to any commutative ring\<close> 158theorem binomial_ring: "(a + b :: 'a::comm_semiring_1)^n = 159 (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))" 160proof (induct n) 161 case 0 162 then show ?case by simp 163next 164 case (Suc n) 165 have decomp: "{0..n+1} = {0} \<union> {n + 1} \<union> {1..n}" 166 by auto 167 have decomp2: "{0..n} = {0} \<union> {1..n}" 168 by auto 169 have "(a + b)^(n+1) = (a + b) * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k))" 170 using Suc.hyps by simp 171 also have "\<dots> = a * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k)) + 172 b * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n-k))" 173 by (rule distrib_right) 174 also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + 175 (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k + 1))" 176 by (auto simp add: sum_distrib_left ac_simps) 177 also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + 178 (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))" 179 by (simp add: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum.cl_ivl_Suc) 180 also have "\<dots> = b^(n + 1) + 181 (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (a^(n + 1) + 182 (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)))" 183 using sum.nat_ivl_Suc' [of 1 n "\<lambda>k. of_nat (n choose (k-1)) * a ^ k * b ^ (n + 1 - k)"] 184 by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0) 185 also have "\<dots> = a^(n + 1) + b^(n + 1) + 186 (\<Sum>k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" 187 by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat) 188 also have "\<dots> = (\<Sum>k\<le>n+1. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))" 189 using decomp by (simp add: atMost_atLeast0 field_simps) 190 finally show ?case 191 by simp 192qed 193 194text \<open>Original version for the naturals.\<close> 195corollary binomial: "(a + b :: nat)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n - k))" 196 using binomial_ring [of "int a" "int b" n] 197 by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric] 198 of_nat_sum [symmetric] of_nat_eq_iff of_nat_id) 199 200lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n" 201proof (induct n arbitrary: k rule: nat_less_induct) 202 fix n k 203 assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m - x) * (m choose x) = fact m" 204 assume kn: "k \<le> n" 205 let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" 206 consider "n = 0 \<or> k = 0 \<or> n = k" | m h where "n = Suc m" "k = Suc h" "h < m" 207 using kn by atomize_elim presburger 208 then show "fact k * fact (n - k) * (n choose k) = fact n" 209 proof cases 210 case 1 211 with kn show ?thesis by auto 212 next 213 case 2 214 note n = \<open>n = Suc m\<close> 215 note k = \<open>k = Suc h\<close> 216 note hm = \<open>h < m\<close> 217 have mn: "m < n" 218 using n by arith 219 have hm': "h \<le> m" 220 using hm by arith 221 have km: "k \<le> m" 222 using hm k n kn by arith 223 have "m - h = Suc (m - Suc h)" 224 using k km hm by arith 225 with km k have "fact (m - h) = (m - h) * fact (m - k)" 226 by simp 227 with n k have "fact k * fact (n - k) * (n choose k) = 228 k * (fact h * fact (m - h) * (m choose h)) + 229 (m - h) * (fact k * fact (m - k) * (m choose k))" 230 by (simp add: field_simps) 231 also have "\<dots> = (k + (m - h)) * fact m" 232 using H[rule_format, OF mn hm'] H[rule_format, OF mn km] 233 by (simp add: field_simps) 234 finally show ?thesis 235 using k n km by simp 236 qed 237qed 238 239lemma binomial_fact': 240 assumes "k \<le> n" 241 shows "n choose k = fact n div (fact k * fact (n - k))" 242 using binomial_fact_lemma [OF assms] 243 by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left) 244 245lemma binomial_fact: 246 assumes kn: "k \<le> n" 247 shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))" 248 using binomial_fact_lemma[OF kn] 249 apply (simp add: field_simps) 250 apply (metis mult.commute of_nat_fact of_nat_mult) 251 done 252 253lemma fact_binomial: 254 assumes "k \<le> n" 255 shows "fact k * of_nat (n choose k) = (fact n / fact (n - k) :: 'a::field_char_0)" 256 unfolding binomial_fact [OF assms] by (simp add: field_simps) 257 258lemma choose_two: "n choose 2 = n * (n - 1) div 2" 259proof (cases "n \<ge> 2") 260 case False 261 then have "n = 0 \<or> n = 1" 262 by auto 263 then show ?thesis by auto 264next 265 case True 266 define m where "m = n - 2" 267 with True have "n = m + 2" 268 by simp 269 then have "fact n = n * (n - 1) * fact (n - 2)" 270 by (simp add: fact_prod_Suc atLeast0_lessThan_Suc algebra_simps) 271 with True show ?thesis 272 by (simp add: binomial_fact') 273qed 274 275lemma choose_row_sum: "(\<Sum>k\<le>n. n choose k) = 2^n" 276 using binomial [of 1 "1" n] by (simp add: numeral_2_eq_2) 277 278lemma sum_choose_lower: "(\<Sum>k\<le>n. (r+k) choose k) = Suc (r+n) choose n" 279 by (induct n) auto 280 281lemma sum_choose_upper: "(\<Sum>k\<le>n. k choose m) = Suc n choose Suc m" 282 by (induct n) auto 283 284lemma choose_alternating_sum: 285 "n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a::comm_ring_1)" 286 using binomial_ring[of "-1 :: 'a" 1 n] 287 by (simp add: atLeast0AtMost mult_of_nat_commute zero_power) 288 289lemma choose_even_sum: 290 assumes "n > 0" 291 shows "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)" 292proof - 293 have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)" 294 using choose_row_sum[of n] 295 by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_sum[symmetric]) 296 also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))" 297 by (simp add: sum.distrib) 298 also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)" 299 by (subst sum_distrib_left, intro sum.cong) simp_all 300 finally show ?thesis .. 301qed 302 303lemma choose_odd_sum: 304 assumes "n > 0" 305 shows "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a::comm_ring_1)" 306proof - 307 have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)" 308 using choose_row_sum[of n] 309 by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_sum[symmetric]) 310 also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))" 311 by (simp add: sum_subtractf) 312 also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)" 313 by (subst sum_distrib_left, intro sum.cong) simp_all 314 finally show ?thesis .. 315qed 316 317text\<open>NW diagonal sum property\<close> 318lemma sum_choose_diagonal: 319 assumes "m \<le> n" 320 shows "(\<Sum>k\<le>m. (n - k) choose (m - k)) = Suc n choose m" 321proof - 322 have "(\<Sum>k\<le>m. (n-k) choose (m - k)) = (\<Sum>k\<le>m. (n - m + k) choose k)" 323 using sum.atLeastAtMost_rev [of "\<lambda>k. (n - k) choose (m - k)" 0 m] assms 324 by (simp add: atMost_atLeast0) 325 also have "\<dots> = Suc (n - m + m) choose m" 326 by (rule sum_choose_lower) 327 also have "\<dots> = Suc n choose m" 328 using assms by simp 329 finally show ?thesis . 330qed 331 332 333subsection \<open>Generalized binomial coefficients\<close> 334 335definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65) 336 where gbinomial_prod_rev: "a gchoose k = prod (\<lambda>i. a - of_nat i) {0..<k} div fact k" 337 338lemma gbinomial_0 [simp]: 339 "a gchoose 0 = 1" 340 "0 gchoose (Suc k) = 0" 341 by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc) 342 343lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)" 344 by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost) 345 346lemma gbinomial_1 [simp]: "a gchoose 1 = a" 347 by (simp add: gbinomial_prod_rev lessThan_Suc) 348 349lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a" 350 by (simp add: gbinomial_prod_rev lessThan_Suc) 351 352lemma gbinomial_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - of_nat i)" 353 for a :: "'a::field_char_0" 354 by (simp_all add: gbinomial_prod_rev field_simps) 355 356lemma gbinomial_mult_fact': "(a gchoose k) * fact k = (\<Prod>i = 0..<k. a - of_nat i)" 357 for a :: "'a::field_char_0" 358 using gbinomial_mult_fact [of k a] by (simp add: ac_simps) 359 360lemma gbinomial_pochhammer: "a gchoose k = (- 1) ^ k * pochhammer (- a) k / fact k" 361 for a :: "'a::field_char_0" 362proof (cases k) 363 case (Suc k') 364 then show ?thesis 365 apply (simp add: pochhammer_minus) 366 apply (simp add: gbinomial_prod_rev pochhammer_prod_rev power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost 367 prod.atLeast_Suc_atMost_Suc_shift of_nat_diff del: prod.cl_ivl_Suc) 368 done 369qed auto 370 371lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k" 372 for a :: "'a::field_char_0" 373proof - 374 have "a gchoose k = ((-1)^k * (-1)^k) * pochhammer (a - of_nat k + 1) k / fact k" 375 by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac) 376 also have "(-1 :: 'a)^k * (-1)^k = 1" 377 by (subst power_add [symmetric]) simp 378 finally show ?thesis 379 by simp 380qed 381 382lemma gbinomial_binomial: "n gchoose k = n choose k" 383proof (cases "k \<le> n") 384 case False 385 then have "n < k" 386 by (simp add: not_le) 387 then have "0 \<in> ((-) n) ` {0..<k}" 388 by auto 389 then have "prod ((-) n) {0..<k} = 0" 390 by (auto intro: prod_zero) 391 with \<open>n < k\<close> show ?thesis 392 by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero) 393next 394 case True 395 from True have *: "prod ((-) n) {0..<k} = \<Prod>{Suc (n - k)..n}" 396 by (intro prod.reindex_bij_witness[of _ "\<lambda>i. n - i" "\<lambda>i. n - i"]) auto 397 from True have "n choose k = fact n div (fact k * fact (n - k))" 398 by (rule binomial_fact') 399 with * show ?thesis 400 by (simp add: gbinomial_prod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact) 401qed 402 403lemma of_nat_gbinomial: "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)" 404proof (cases "k \<le> n") 405 case False 406 then show ?thesis 407 by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_prod_rev) 408next 409 case True 410 define m where "m = n - k" 411 with True have n: "n = m + k" 412 by arith 413 from n have "fact n = ((\<Prod>i = 0..<m + k. of_nat (m + k - i) ):: 'a)" 414 by (simp add: fact_prod_rev) 415 also have "\<dots> = ((\<Prod>i\<in>{0..<k} \<union> {k..<m + k}. of_nat (m + k - i)) :: 'a)" 416 by (simp add: ivl_disj_un) 417 finally have "fact n = (fact m * (\<Prod>i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)" 418 using prod.shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m] 419 by (simp add: fact_prod_rev [of m] prod.union_disjoint of_nat_diff) 420 then have "fact n / fact (n - k) = ((\<Prod>i = 0..<k. of_nat n - of_nat i) :: 'a)" 421 by (simp add: n) 422 with True have "fact k * of_nat (n gchoose k) = (fact k * (of_nat n gchoose k) :: 'a)" 423 by (simp only: gbinomial_mult_fact [of k "of_nat n"] gbinomial_binomial [of n k] fact_binomial) 424 then show ?thesis 425 by simp 426qed 427 428lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)" 429 by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial) 430 431setup 432 \<open>Sign.add_const_constraint (\<^const_name>\<open>gbinomial\<close>, SOME \<^typ>\<open>'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a\<close>)\<close> 433 434lemma gbinomial_mult_1: 435 fixes a :: "'a::field_char_0" 436 shows "a * (a gchoose k) = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))" 437 (is "?l = ?r") 438proof - 439 have "?r = ((- 1) ^k * pochhammer (- a) k / fact k) * (of_nat k - (- a + of_nat k))" 440 apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc) 441 apply (simp del: of_nat_Suc fact_Suc) 442 apply (auto simp add: field_simps simp del: of_nat_Suc) 443 done 444 also have "\<dots> = ?l" 445 by (simp add: field_simps gbinomial_pochhammer) 446 finally show ?thesis .. 447qed 448 449lemma gbinomial_mult_1': 450 "(a gchoose k) * a = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))" 451 for a :: "'a::field_char_0" 452 by (simp add: mult.commute gbinomial_mult_1) 453 454lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" 455 for a :: "'a::field_char_0" 456proof (cases k) 457 case 0 458 then show ?thesis by simp 459next 460 case (Suc h) 461 have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)" 462 apply (rule prod.reindex_cong [where l = Suc]) 463 using Suc 464 apply (auto simp add: image_Suc_atMost) 465 done 466 have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) = 467 (a gchoose Suc h) * (fact (Suc (Suc h))) + 468 (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))" 469 by (simp add: Suc field_simps del: fact_Suc) 470 also have "\<dots> = 471 (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)" 472 apply (simp del: fact_Suc prod.op_ivl_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"]) 473 apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact 474 mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost) 475 done 476 also have "\<dots> = 477 (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)" 478 by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult) 479 also have "\<dots> = 480 of_nat (Suc (Suc h)) * (\<Prod>i=0..h. a - of_nat i) + (\<Prod>i=0..Suc h. a - of_nat i)" 481 unfolding gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost by auto 482 also have "\<dots> = 483 (\<Prod>i=0..Suc h. a - of_nat i) + (of_nat h * (\<Prod>i=0..h. a - of_nat i) + 2 * (\<Prod>i=0..h. a - of_nat i))" 484 by (simp add: field_simps) 485 also have "\<dots> = 486 ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0..Suc h}. a - of_nat i)" 487 unfolding gbinomial_mult_fact' 488 by (simp add: comm_semiring_class.distrib field_simps Suc atLeastLessThanSuc_atLeastAtMost) 489 also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)" 490 unfolding gbinomial_mult_fact' atLeast0_atMost_Suc 491 by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost) 492 also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)" 493 using eq0 494 by (simp add: Suc prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc) 495 also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))" 496 by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost) 497 finally show ?thesis 498 using fact_nonzero [of "Suc k"] by auto 499qed 500 501lemma gbinomial_reduce_nat: "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)" 502 for a :: "'a::field_char_0" 503 by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc) 504 505lemma gchoose_row_sum_weighted: 506 "(\<Sum>k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))" 507 for r :: "'a::field_char_0" 508 by (induct m) (simp_all add: field_simps distrib gbinomial_mult_1) 509 510lemma binomial_symmetric: 511 assumes kn: "k \<le> n" 512 shows "n choose k = n choose (n - k)" 513proof - 514 have kn': "n - k \<le> n" 515 using kn by arith 516 from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] 517 have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" 518 by simp 519 then show ?thesis 520 using kn by simp 521qed 522 523lemma choose_rising_sum: 524 "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" 525 "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" 526proof - 527 show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" 528 by (induct m) simp_all 529 also have "\<dots> = (n + m + 1) choose m" 530 by (subst binomial_symmetric) simp_all 531 finally show "(\<Sum>j\<le>m. ((n + j) choose n)) = (n + m + 1) choose m" . 532qed 533 534lemma choose_linear_sum: "(\<Sum>i\<le>n. i * (n choose i)) = n * 2 ^ (n - 1)" 535proof (cases n) 536 case 0 537 then show ?thesis by simp 538next 539 case (Suc m) 540 have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" 541 by (simp add: Suc) 542 also have "\<dots> = Suc m * 2 ^ m" 543 unfolding sum.atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric] 544 by (simp add: choose_row_sum) 545 finally show ?thesis 546 using Suc by simp 547qed 548 549lemma choose_alternating_linear_sum: 550 assumes "n \<noteq> 1" 551 shows "(\<Sum>i\<le>n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a::comm_ring_1) = 0" 552proof (cases n) 553 case 0 554 then show ?thesis by simp 555next 556 case (Suc m) 557 with assms have "m > 0" 558 by simp 559 have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = 560 (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" 561 by (simp add: Suc) 562 also have "\<dots> = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))" 563 by (simp only: sum.atMost_Suc_shift sum_distrib_left[symmetric] mult_ac of_nat_mult) simp 564 also have "\<dots> = - of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat (m choose i))" 565 by (subst sum_distrib_left, rule sum.cong[OF refl], subst Suc_times_binomial) 566 (simp add: algebra_simps) 567 also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0" 568 using choose_alternating_sum[OF \<open>m > 0\<close>] by simp 569 finally show ?thesis 570 by simp 571qed 572 573lemma vandermonde: "(\<Sum>k\<le>r. (m choose k) * (n choose (r - k))) = (m + n) choose r" 574proof (induct n arbitrary: r) 575 case 0 576 have "(\<Sum>k\<le>r. (m choose k) * (0 choose (r - k))) = (\<Sum>k\<le>r. if k = r then (m choose k) else 0)" 577 by (intro sum.cong) simp_all 578 also have "\<dots> = m choose r" 579 by simp 580 finally show ?case 581 by simp 582next 583 case (Suc n r) 584 show ?case 585 by (cases r) (simp_all add: Suc [symmetric] algebra_simps sum.distrib Suc_diff_le) 586qed 587 588lemma choose_square_sum: "(\<Sum>k\<le>n. (n choose k)^2) = ((2*n) choose n)" 589 using vandermonde[of n n n] 590 by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric]) 591 592lemma pochhammer_binomial_sum: 593 fixes a b :: "'a::comm_ring_1" 594 shows "pochhammer (a + b) n = (\<Sum>k\<le>n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))" 595proof (induction n arbitrary: a b) 596 case 0 597 then show ?case by simp 598next 599 case (Suc n a b) 600 have "(\<Sum>k\<le>Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) = 601 (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) + 602 ((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + 603 pochhammer b (Suc n))" 604 by (subst sum.atMost_Suc_shift) (simp add: ring_distribs sum.distrib) 605 also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) = 606 a * pochhammer ((a + 1) + b) n" 607 by (subst Suc) (simp add: sum_distrib_left pochhammer_rec mult_ac) 608 also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + 609 pochhammer b (Suc n) = 610 (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" 611 apply (subst sum.atLeast_Suc_atMost) 612 apply simp 613 apply (subst sum.shift_bounds_cl_Suc_ivl) 614 apply (simp add: atLeast0AtMost) 615 done 616 also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" 617 using Suc by (intro sum.mono_neutral_right) (auto simp: not_le binomial_eq_0) 618 also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))" 619 by (intro sum.cong) (simp_all add: Suc_diff_le) 620 also have "\<dots> = b * pochhammer (a + (b + 1)) n" 621 by (subst Suc) (simp add: sum_distrib_left mult_ac pochhammer_rec) 622 also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n = 623 pochhammer (a + b) (Suc n)" 624 by (simp add: pochhammer_rec algebra_simps) 625 finally show ?case .. 626qed 627 628text \<open>Contributed by Manuel Eberl, generalised by LCP. 629 Alternative definition of the binomial coefficient as \<^term>\<open>\<Prod>i<k. (n - i) / (k - i)\<close>.\<close> 630lemma gbinomial_altdef_of_nat: "a gchoose k = (\<Prod>i = 0..<k. (a - of_nat i) / of_nat (k - i) :: 'a)" 631 for k :: nat and a :: "'a::field_char_0" 632 by (simp add: prod_dividef gbinomial_prod_rev fact_prod_rev) 633 634lemma gbinomial_ge_n_over_k_pow_k: 635 fixes k :: nat 636 and a :: "'a::linordered_field" 637 assumes "of_nat k \<le> a" 638 shows "(a / of_nat k :: 'a) ^ k \<le> a gchoose k" 639proof - 640 have x: "0 \<le> a" 641 using assms of_nat_0_le_iff order_trans by blast 642 have "(a / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. a / of_nat k :: 'a)" 643 by simp 644 also have "\<dots> \<le> a gchoose k" (* FIXME *) 645 unfolding gbinomial_altdef_of_nat 646 apply (safe intro!: prod_mono) 647 apply simp_all 648 prefer 2 649 subgoal premises for i 650 proof - 651 from assms have "a * of_nat i \<ge> of_nat (i * k)" 652 by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult) 653 then have "a * of_nat k - a * of_nat i \<le> a * of_nat k - of_nat (i * k)" 654 by arith 655 then have "a * of_nat (k - i) \<le> (a - of_nat i) * of_nat k" 656 using \<open>i < k\<close> by (simp add: algebra_simps zero_less_mult_iff of_nat_diff) 657 then have "a * of_nat (k - i) \<le> (a - of_nat i) * (of_nat k :: 'a)" 658 by (simp only: of_nat_mult[symmetric] of_nat_le_iff) 659 with assms show ?thesis 660 using \<open>i < k\<close> by (simp add: field_simps) 661 qed 662 apply (simp add: x zero_le_divide_iff) 663 done 664 finally show ?thesis . 665qed 666 667lemma gbinomial_negated_upper: "(a gchoose k) = (-1) ^ k * ((of_nat k - a - 1) gchoose k)" 668 by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps) 669 670lemma gbinomial_minus: "((-a) gchoose k) = (-1) ^ k * ((a + of_nat k - 1) gchoose k)" 671 by (subst gbinomial_negated_upper) (simp add: add_ac) 672 673lemma Suc_times_gbinomial: "of_nat (Suc k) * ((a + 1) gchoose (Suc k)) = (a + 1) * (a gchoose k)" 674proof (cases k) 675 case 0 676 then show ?thesis by simp 677next 678 case (Suc b) 679 then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)" 680 by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost) 681 also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)" 682 by (simp add: prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc) 683 also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" 684 by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost) 685 finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc) 686qed 687 688lemma gbinomial_factors: "((a + 1) gchoose (Suc k)) = (a + 1) / of_nat (Suc k) * (a gchoose k)" 689proof (cases k) 690 case 0 691 then show ?thesis by simp 692next 693 case (Suc b) 694 then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)" 695 by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost) 696 also have "(\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)" 697 by (simp add: prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc) 698 also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)" 699 by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) 700 finally show ?thesis 701 by (simp add: Suc) 702qed 703 704lemma gbinomial_rec: "((a + 1) gchoose (Suc k)) = (a gchoose k) * ((a + 1) / of_nat (Suc k))" 705 using gbinomial_mult_1[of a k] 706 by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps) 707 708lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n - k)" 709 using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric]) 710 711 712text \<open>The absorption identity (equation 5.5 @{cite \<open>p.~157\<close> GKP_CM}): 713\[ 714{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0. 715\]\<close> 716lemma gbinomial_absorption': "k > 0 \<Longrightarrow> a gchoose k = (a / of_nat k) * (a - 1 gchoose (k - 1))" 717 using gbinomial_rec[of "a - 1" "k - 1"] 718 by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc) 719 720text \<open>The absorption identity is written in the following form to avoid 721division by $k$ (the lower index) and therefore remove the $k \neq 0$ 722restriction @{cite \<open>p.~157\<close> GKP_CM}: 723\[ 724k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k. 725\]\<close> 726lemma gbinomial_absorption: "of_nat (Suc k) * (a gchoose Suc k) = a * ((a - 1) gchoose k)" 727 using gbinomial_absorption'[of "Suc k" a] by (simp add: field_simps del: of_nat_Suc) 728 729text \<open>The absorption identity for natural number binomial coefficients:\<close> 730lemma binomial_absorption: "Suc k * (n choose Suc k) = n * ((n - 1) choose k)" 731 by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc) 732 733text \<open>The absorption companion identity for natural number coefficients, 734 following the proof by GKP @{cite \<open>p.~157\<close> GKP_CM}:\<close> 735lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)" 736 (is "?lhs = ?rhs") 737proof (cases "n \<le> k") 738 case True 739 then show ?thesis by auto 740next 741 case False 742 then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))" 743 using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n] 744 by simp 745 also have "Suc ((n - 1) - k) = n - k" 746 using False by simp 747 also have "n choose \<dots> = n choose k" 748 using False by (intro binomial_symmetric [symmetric]) simp_all 749 finally show ?thesis .. 750qed 751 752text \<open>The generalised absorption companion identity:\<close> 753lemma gbinomial_absorb_comp: "(a - of_nat k) * (a gchoose k) = a * ((a - 1) gchoose k)" 754 using pochhammer_absorb_comp[of a k] by (simp add: gbinomial_pochhammer) 755 756lemma gbinomial_addition_formula: 757 "a gchoose (Suc k) = ((a - 1) gchoose (Suc k)) + ((a - 1) gchoose k)" 758 using gbinomial_Suc_Suc[of "a - 1" k] by (simp add: algebra_simps) 759 760lemma binomial_addition_formula: 761 "0 < n \<Longrightarrow> n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)" 762 by (subst choose_reduce_nat) simp_all 763 764text \<open> 765 Equation 5.9 of the reference material @{cite \<open>p.~159\<close> GKP_CM} is a useful 766 summation formula, operating on both indices: 767 \[ 768 \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n}, 769 \quad \textnormal{integer } n. 770 \] 771\<close> 772lemma gbinomial_parallel_sum: "(\<Sum>k\<le>n. (a + of_nat k) gchoose k) = (a + of_nat n + 1) gchoose n" 773proof (induct n) 774 case 0 775 then show ?case by simp 776next 777 case (Suc m) 778 then show ?case 779 using gbinomial_Suc_Suc[of "(a + of_nat m + 1)" m] 780 by (simp add: add_ac) 781qed 782 783 784subsubsection \<open>Summation on the upper index\<close> 785 786text \<open> 787 Another summation formula is equation 5.10 of the reference material @{cite \<open>p.~160\<close> GKP_CM}, 788 aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 789 {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\] 790\<close> 791lemma gbinomial_sum_up_index: 792 "(\<Sum>j = 0..n. (of_nat j gchoose k) :: 'a::field_char_0) = (of_nat n + 1) gchoose (k + 1)" 793proof (induct n) 794 case 0 795 show ?case 796 using gbinomial_Suc_Suc[of 0 k] 797 by (cases k) auto 798next 799 case (Suc n) 800 then show ?case 801 using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" k] 802 by (simp add: add_ac) 803qed 804 805lemma gbinomial_index_swap: 806 "((-1) ^ k) * ((- (of_nat n) - 1) gchoose k) = ((-1) ^ n) * ((- (of_nat k) - 1) gchoose n)" 807 (is "?lhs = ?rhs") 808proof - 809 have "?lhs = (of_nat (k + n) gchoose k)" 810 by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric]) 811 also have "\<dots> = (of_nat (k + n) gchoose n)" 812 by (subst gbinomial_of_nat_symmetric) simp_all 813 also have "\<dots> = ?rhs" 814 by (subst gbinomial_negated_upper) simp 815 finally show ?thesis . 816qed 817 818lemma gbinomial_sum_lower_neg: "(\<Sum>k\<le>m. (a gchoose k) * (- 1) ^ k) = (- 1) ^ m * (a - 1 gchoose m)" 819 (is "?lhs = ?rhs") 820proof - 821 have "?lhs = (\<Sum>k\<le>m. -(a + 1) + of_nat k gchoose k)" 822 by (intro sum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib) 823 also have "\<dots> = - a + of_nat m gchoose m" 824 by (subst gbinomial_parallel_sum) simp 825 also have "\<dots> = ?rhs" 826 by (subst gbinomial_negated_upper) (simp add: power_mult_distrib) 827 finally show ?thesis . 828qed 829 830lemma gbinomial_partial_row_sum: 831 "(\<Sum>k\<le>m. (a gchoose k) * ((a / 2) - of_nat k)) = ((of_nat m + 1)/2) * (a gchoose (m + 1))" 832proof (induct m) 833 case 0 834 then show ?case by simp 835next 836 case (Suc mm) 837 then have "(\<Sum>k\<le>Suc mm. (a gchoose k) * (a / 2 - of_nat k)) = 838 (a - of_nat (Suc mm)) * (a gchoose Suc mm) / 2" 839 by (simp add: field_simps) 840 also have "\<dots> = a * (a - 1 gchoose Suc mm) / 2" 841 by (subst gbinomial_absorb_comp) (rule refl) 842 also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (a gchoose (Suc mm + 1))" 843 by (subst gbinomial_absorption [symmetric]) simp 844 finally show ?case . 845qed 846 847lemma sum_bounds_lt_plus1: "(\<Sum>k<mm. f (Suc k)) = (\<Sum>k=1..mm. f k)" 848 by (induct mm) simp_all 849 850lemma gbinomial_partial_sum_poly: 851 "(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) = 852 (\<Sum>k\<le>m. (-a gchoose k) * (-x)^k * (x + y)^(m-k))" 853 (is "?lhs m = ?rhs m") 854proof (induction m) 855 case 0 856 then show ?case by simp 857next 858 case (Suc mm) 859 define G where "G i k = (of_nat i + a gchoose k) * x^k * y^(i - k)" for i k 860 define S where "S = ?lhs" 861 have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))" 862 unfolding S_def G_def .. 863 864 have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)" 865 using SG_def by (simp add: sum.atLeast_Suc_atMost atLeast0AtMost [symmetric]) 866 also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))" 867 by (subst sum.shift_bounds_cl_Suc_ivl) simp 868 also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + a gchoose (Suc k)) + 869 (of_nat mm + a gchoose k)) * x^(Suc k) * y^(mm - k))" 870 unfolding G_def by (subst gbinomial_addition_formula) simp 871 also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) + 872 (\<Sum>k=0..mm. (of_nat mm + a gchoose k) * x^(Suc k) * y^(mm - k))" 873 by (subst sum.distrib [symmetric]) (simp add: algebra_simps) 874 also have "(\<Sum>k=0..mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = 875 (\<Sum>k<Suc mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k))" 876 by (simp only: atLeast0AtMost lessThan_Suc_atMost) 877 also have "\<dots> = (\<Sum>k<mm. (of_nat mm + a gchoose Suc k) * x^(Suc k) * y^(mm-k)) + 878 (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)" 879 (is "_ = ?A + ?B") 880 by (subst sum.lessThan_Suc) simp 881 also have "?A = (\<Sum>k=1..mm. (of_nat mm + a gchoose k) * x^k * y^(mm - k + 1))" 882 proof (subst sum_bounds_lt_plus1 [symmetric], intro sum.cong[OF refl], clarify) 883 fix k 884 assume "k < mm" 885 then have "mm - k = mm - Suc k + 1" 886 by linarith 887 then show "(of_nat mm + a gchoose Suc k) * x ^ Suc k * y ^ (mm - k) = 888 (of_nat mm + a gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" 889 by (simp only:) 890 qed 891 also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)" 892 unfolding G_def by (subst sum_distrib_left) (simp add: algebra_simps) 893 also have "(\<Sum>k=0..mm. (of_nat mm + a gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)" 894 unfolding S_def by (subst sum_distrib_left) (simp add: atLeast0AtMost algebra_simps) 895 also have "(G (Suc mm) 0) = y * (G mm 0)" 896 by (simp add: G_def) 897 finally have "S (Suc mm) = 898 y * (G mm 0 + (\<Sum>k=1..mm. (G mm k))) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)" 899 by (simp add: ring_distribs) 900 also have "G mm 0 + (\<Sum>k=1..mm. (G mm k)) = S mm" 901 by (simp add: sum.atLeast_Suc_atMost[symmetric] SG_def atLeast0AtMost) 902 finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)" 903 by (simp add: algebra_simps) 904 also have "(of_nat mm + a gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- a gchoose (Suc mm))" 905 by (subst gbinomial_negated_upper) simp 906 also have "(-1) ^ Suc mm * (- a gchoose Suc mm) * x ^ Suc mm = 907 (- a gchoose (Suc mm)) * (-x) ^ Suc mm" 908 by (simp add: power_minus[of x]) 909 also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (- a gchoose (Suc mm)) * (- x)^Suc mm" 910 unfolding S_def by (subst Suc.IH) simp 911 also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))" 912 by (subst sum_distrib_left, rule sum.cong) (simp_all add: Suc_diff_le) 913 also have "\<dots> + (-a gchoose (Suc mm)) * (-x)^Suc mm = 914 (\<Sum>n\<le>Suc mm. (- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" 915 by simp 916 finally show ?case 917 by (simp only: S_def) 918qed 919 920lemma gbinomial_partial_sum_poly_xpos: 921 "(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) = 922 (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))" 923 apply (subst gbinomial_partial_sum_poly) 924 apply (subst gbinomial_negated_upper) 925 apply (intro sum.cong, rule refl) 926 apply (simp add: power_mult_distrib [symmetric]) 927 done 928 929lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)" 930proof - 931 have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))" 932 using choose_row_sum[where n="2 * m + 1"] by (simp add: atMost_atLeast0) 933 also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) = 934 (\<Sum>k = 0..m. (2 * m + 1 choose k)) + 935 (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))" 936 using sum.ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"] 937 by (simp add: mult_2) 938 also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) = 939 (\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))" 940 by (subst sum.shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2) 941 also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))" 942 by (intro sum.cong[OF refl], subst binomial_symmetric) simp_all 943 also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))" 944 using sum.atLeastAtMost_rev [of "\<lambda>k. 2 * m + 1 choose (m - k)" 0 m] 945 by simp 946 also have "\<dots> + \<dots> = 2 * \<dots>" 947 by simp 948 finally show ?thesis 949 by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost) 950qed 951 952lemma gbinomial_r_part_sum: "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" 953 (is "?lhs = ?rhs") 954proof - 955 have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)" 956 by (simp add: binomial_gbinomial add_ac) 957 also have "\<dots> = of_nat (2 ^ (2 * m))" 958 by (subst binomial_r_part_sum) (rule refl) 959 finally show ?thesis by simp 960qed 961 962lemma gbinomial_sum_nat_pow2: 963 "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a::field_char_0) / 2 ^ k) = 2 ^ m" 964 (is "?lhs = ?rhs") 965proof - 966 have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" 967 by (induct m) simp_all 968 also have "\<dots> = (\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k))" 969 using gbinomial_r_part_sum .. 970 also have "\<dots> = (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))" 971 using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and a="of_nat m + 1" and m="m"] 972 by (simp add: add_ac) 973 also have "\<dots> = 2 ^ m * (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) / 2 ^ k)" 974 by (subst sum_distrib_left) (simp add: algebra_simps power_diff) 975 finally show ?thesis 976 by (subst (asm) mult_left_cancel) simp_all 977qed 978 979lemma gbinomial_trinomial_revision: 980 assumes "k \<le> m" 981 shows "(a gchoose m) * (of_nat m gchoose k) = (a gchoose k) * (a - of_nat k gchoose (m - k))" 982proof - 983 have "(a gchoose m) * (of_nat m gchoose k) = (a gchoose m) * fact m / (fact k * fact (m - k))" 984 using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact) 985 also have "\<dots> = (a gchoose k) * (a - of_nat k gchoose (m - k))" 986 using assms by (simp add: gbinomial_pochhammer power_diff pochhammer_product) 987 finally show ?thesis . 988qed 989 990text \<open>Versions of the theorems above for the natural-number version of "choose"\<close> 991lemma binomial_altdef_of_nat: 992 "k \<le> n \<Longrightarrow> of_nat (n choose k) = (\<Prod>i = 0..<k. of_nat (n - i) / of_nat (k - i) :: 'a)" 993 for n k :: nat and x :: "'a::field_char_0" 994 by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff) 995 996lemma binomial_ge_n_over_k_pow_k: "k \<le> n \<Longrightarrow> (of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)" 997 for k n :: nat and x :: "'a::linordered_field" 998 by (simp add: gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff) 999 1000lemma binomial_le_pow: 1001 assumes "r \<le> n" 1002 shows "n choose r \<le> n ^ r" 1003proof - 1004 have "n choose r \<le> fact n div fact (n - r)" 1005 using assms by (subst binomial_fact_lemma[symmetric]) auto 1006 with fact_div_fact_le_pow [OF assms] show ?thesis 1007 by auto 1008qed 1009 1010lemma binomial_altdef_nat: "k \<le> n \<Longrightarrow> n choose k = fact n div (fact k * fact (n - k))" 1011 for k n :: nat 1012 by (subst binomial_fact_lemma [symmetric]) auto 1013 1014lemma choose_dvd: 1015 "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)" 1016 unfolding dvd_def 1017 apply (rule exI [where x="of_nat (n choose k)"]) 1018 using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]] 1019 apply auto 1020 done 1021 1022lemma fact_fact_dvd_fact: 1023 "fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)" 1024 by (metis add.commute add_diff_cancel_left' choose_dvd le_add2) 1025 1026lemma choose_mult_lemma: 1027 "((m + r + k) choose (m + k)) * ((m + k) choose k) = ((m + r + k) choose k) * ((m + r) choose m)" 1028 (is "?lhs = _") 1029proof - 1030 have "?lhs = 1031 fact (m + r + k) div (fact (m + k) * fact (m + r - m)) * (fact (m + k) div (fact k * fact m))" 1032 by (simp add: binomial_altdef_nat) 1033 also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))" 1034 apply (subst div_mult_div_if_dvd) 1035 apply (auto simp: algebra_simps fact_fact_dvd_fact) 1036 apply (metis add.assoc add.commute fact_fact_dvd_fact) 1037 done 1038 also have "\<dots> = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))" 1039 apply (subst div_mult_div_if_dvd [symmetric]) 1040 apply (auto simp add: algebra_simps) 1041 apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj) 1042 done 1043 also have "\<dots> = 1044 (fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))" 1045 apply (subst div_mult_div_if_dvd) 1046 apply (auto simp: fact_fact_dvd_fact algebra_simps) 1047 done 1048 finally show ?thesis 1049 by (simp add: binomial_altdef_nat mult.commute) 1050qed 1051 1052text \<open>The "Subset of a Subset" identity.\<close> 1053lemma choose_mult: 1054 "k \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))" 1055 using choose_mult_lemma [of "m-k" "n-m" k] by simp 1056 1057 1058subsection \<open>More on Binomial Coefficients\<close> 1059 1060lemma choose_one: "n choose 1 = n" for n :: nat 1061 by simp 1062 1063lemma card_UNION: 1064 assumes "finite A" 1065 and "\<forall>k \<in> A. finite k" 1066 shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))" 1067 (is "?lhs = ?rhs") 1068proof - 1069 have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" 1070 by simp 1071 also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" 1072 (is "_ = nat ?rhs") 1073 by (subst sum_distrib_left) simp 1074 also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))" 1075 using assms by (subst sum.Sigma) auto 1076 also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))" 1077 by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI) 1078 also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))" 1079 using assms 1080 by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"]) 1081 also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))" 1082 using assms by (subst sum.Sigma) auto 1083 also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "sum ?lhs _ = _") 1084 proof (rule sum.cong[OF refl]) 1085 fix x 1086 assume x: "x \<in> \<Union>A" 1087 define K where "K = {X \<in> A. x \<in> X}" 1088 with \<open>finite A\<close> have K: "finite K" 1089 by auto 1090 let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}" 1091 have "inj_on snd (SIGMA i:{1..card A}. ?I i)" 1092 using assms by (auto intro!: inj_onI) 1093 moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}" 1094 using assms 1095 by (auto intro!: rev_image_eqI[where x="(card a, a)" for a] 1096 simp add: card_gt_0_iff[folded Suc_le_eq] 1097 dest: finite_subset intro: card_mono) 1098 ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))" 1099 by (rule sum.reindex_cong [where l = snd]) fastforce 1100 also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))" 1101 using assms by (subst sum.Sigma) auto 1102 also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))" 1103 by (subst sum_distrib_left) simp 1104 also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" 1105 (is "_ = ?rhs") 1106 proof (rule sum.mono_neutral_cong_right[rule_format]) 1107 show "finite {1..card A}" 1108 by simp 1109 show "{1..card K} \<subseteq> {1..card A}" 1110 using \<open>finite A\<close> by (auto simp add: K_def intro: card_mono) 1111 next 1112 fix i 1113 assume "i \<in> {1..card A} - {1..card K}" 1114 then have i: "i \<le> card A" "card K < i" 1115 by auto 1116 have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" 1117 by (auto simp add: K_def) 1118 also have "\<dots> = {}" 1119 using \<open>finite A\<close> i by (auto simp add: K_def dest: card_mono[rotated 1]) 1120 finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0" 1121 by (simp only:) simp 1122 next 1123 fix i 1124 have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)" 1125 (is "?lhs = ?rhs") 1126 by (rule sum.cong) (auto simp add: K_def) 1127 then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" 1128 by simp 1129 qed 1130 also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" 1131 using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset) 1132 then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1" 1133 by (subst (2) sum.atLeast_Suc_atMost) simp_all 1134 also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1" 1135 using K by (subst n_subsets[symmetric]) simp_all 1136 also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1" 1137 by (subst sum_distrib_left[symmetric]) simp 1138 also have "\<dots> = - ((-1 + 1) ^ card K) + 1" 1139 by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0) 1140 also have "\<dots> = 1" 1141 using x K by (auto simp add: K_def card_gt_0_iff) 1142 finally show "?lhs x = 1" . 1143 qed 1144 also have "nat \<dots> = card (\<Union>A)" 1145 by simp 1146 finally show ?thesis .. 1147qed 1148 1149text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is \<^term>\<open>(N + m - 1) choose N\<close>:\<close> 1150lemma card_length_sum_list_rec: 1151 assumes "m \<ge> 1" 1152 shows "card {l::nat list. length l = m \<and> sum_list l = N} = 1153 card {l. length l = (m - 1) \<and> sum_list l = N} + 1154 card {l. length l = m \<and> sum_list l + 1 = N}" 1155 (is "card ?C = card ?A + card ?B") 1156proof - 1157 let ?A' = "{l. length l = m \<and> sum_list l = N \<and> hd l = 0}" 1158 let ?B' = "{l. length l = m \<and> sum_list l = N \<and> hd l \<noteq> 0}" 1159 let ?f = "\<lambda>l. 0 # l" 1160 let ?g = "\<lambda>l. (hd l + 1) # tl l" 1161 have 1: "xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" for x :: nat and xs 1162 by simp 1163 have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list" 1164 by (auto simp add: neq_Nil_conv) 1165 have f: "bij_betw ?f ?A ?A'" 1166 apply (rule bij_betw_byWitness[where f' = tl]) 1167 using assms 1168 apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv) 1169 done 1170 have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list" 1171 by (metis 1 sum_list_simps(2) 2) 1172 have g: "bij_betw ?g ?B ?B'" 1173 apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"]) 1174 using assms 1175 by (auto simp: 2 length_0_conv[symmetric] intro!: 3 1176 simp del: length_greater_0_conv length_0_conv) 1177 have fin: "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" for M N :: nat 1178 using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto 1179 have fin_A: "finite ?A" using fin[of _ "N+1"] 1180 by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"]) 1181 (auto simp: member_le_sum_list less_Suc_eq_le) 1182 have fin_B: "finite ?B" 1183 by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"]) 1184 (auto simp: member_le_sum_list less_Suc_eq_le fin) 1185 have uni: "?C = ?A' \<union> ?B'" 1186 by auto 1187 have disj: "?A' \<inter> ?B' = {}" by blast 1188 have "card ?C = card(?A' \<union> ?B')" 1189 using uni by simp 1190 also have "\<dots> = card ?A + card ?B" 1191 using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g] 1192 bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B 1193 by presburger 1194 finally show ?thesis . 1195qed 1196 1197lemma card_length_sum_list: "card {l::nat list. size l = m \<and> sum_list l = N} = (N + m - 1) choose N" 1198 \<comment> \<open>by Holden Lee, tidied by Tobias Nipkow\<close> 1199proof (cases m) 1200 case 0 1201 then show ?thesis 1202 by (cases N) (auto cong: conj_cong) 1203next 1204 case (Suc m') 1205 have m: "m \<ge> 1" 1206 by (simp add: Suc) 1207 then show ?thesis 1208 proof (induct "N + m - 1" arbitrary: N m) 1209 case 0 \<comment> \<open>In the base case, the only solution is [0].\<close> 1210 have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}" 1211 by (auto simp: length_Suc_conv) 1212 have "m = 1 \<and> N = 0" 1213 using 0 by linarith 1214 then show ?case 1215 by simp 1216 next 1217 case (Suc k) 1218 have c1: "card {l::nat list. size l = (m - 1) \<and> sum_list l = N} = (N + (m - 1) - 1) choose N" 1219 proof (cases "m = 1") 1220 case True 1221 with Suc.hyps have "N \<ge> 1" 1222 by auto 1223 with True show ?thesis 1224 by (simp add: binomial_eq_0) 1225 next 1226 case False 1227 then show ?thesis 1228 using Suc by fastforce 1229 qed 1230 from Suc have c2: "card {l::nat list. size l = m \<and> sum_list l + 1 = N} = 1231 (if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)" 1232 proof - 1233 have *: "n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" for m n 1234 by arith 1235 from Suc have "N > 0 \<Longrightarrow> 1236 card {l::nat list. size l = m \<and> sum_list l + 1 = N} = 1237 ((N - 1) + m - 1) choose (N - 1)" 1238 by (simp add: *) 1239 then show ?thesis 1240 by auto 1241 qed 1242 from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> sum_list l = N} + 1243 card {l::nat list. size l = m \<and> sum_list l + 1 = N}) = (N + m - 1) choose N" 1244 by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def) 1245 then show ?case 1246 using card_length_sum_list_rec[OF Suc.prems] by auto 1247 qed 1248qed 1249 1250lemma card_disjoint_shuffles: 1251 assumes "set xs \<inter> set ys = {}" 1252 shows "card (shuffles xs ys) = (length xs + length ys) choose length xs" 1253using assms 1254proof (induction xs ys rule: shuffles.induct) 1255 case (3 x xs y ys) 1256 have "shuffles (x # xs) (y # ys) = (#) x ` shuffles xs (y # ys) \<union> (#) y ` shuffles (x # xs) ys" 1257 by (rule shuffles.simps) 1258 also have "card \<dots> = card ((#) x ` shuffles xs (y # ys)) + card ((#) y ` shuffles (x # xs) ys)" 1259 by (rule card_Un_disjoint) (insert "3.prems", auto) 1260 also have "card ((#) x ` shuffles xs (y # ys)) = card (shuffles xs (y # ys))" 1261 by (rule card_image) auto 1262 also have "\<dots> = (length xs + length (y # ys)) choose length xs" 1263 using "3.prems" by (intro "3.IH") auto 1264 also have "card ((#) y ` shuffles (x # xs) ys) = card (shuffles (x # xs) ys)" 1265 by (rule card_image) auto 1266 also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)" 1267 using "3.prems" by (intro "3.IH") auto 1268 also have "length xs + length (y # ys) choose length xs + \<dots> = 1269 (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp 1270 finally show ?case . 1271qed auto 1272 1273lemma Suc_times_binomial_add: "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)" 1274 \<comment> \<open>by Lukas Bulwahn\<close> 1275proof - 1276 have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b 1277 using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat] 1278 by (simp only: fact_Suc add_Suc[symmetric] of_nat_id mult.assoc) 1279 have "Suc a * (fact (Suc (a + b)) div (Suc a * fact a * fact b)) = 1280 Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))" 1281 by (subst div_mult_swap[symmetric]; simp only: mult.assoc dvd) 1282 also have "\<dots> = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))" 1283 by (simp only: div_mult_mult1) 1284 also have "\<dots> = Suc b * (fact (Suc (a + b)) div (Suc b * (fact a * fact b)))" 1285 using dvd[of b a] by (subst div_mult_swap[symmetric]; simp only: ac_simps dvd) 1286 finally show ?thesis 1287 by (subst (1 2) binomial_altdef_nat) 1288 (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id) 1289qed 1290 1291 1292subsection \<open>Executable code\<close> 1293 1294lemma gbinomial_code [code]: 1295 "a gchoose k = 1296 (if k = 0 then 1 1297 else fold_atLeastAtMost_nat (\<lambda>k acc. (a - of_nat k) * acc) 0 (k - 1) 1 / fact k)" 1298 by (cases k) 1299 (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric] 1300 atLeastLessThanSuc_atLeastAtMost) 1301 1302lemma binomial_code [code]: 1303 "n choose k = 1304 (if k > n then 0 1305 else if 2 * k > n then n choose (n - k) 1306 else (fold_atLeastAtMost_nat (*) (n - k + 1) n 1 div fact k))" 1307proof - 1308 { 1309 assume "k \<le> n" 1310 then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto 1311 then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}" 1312 by (simp add: prod.union_disjoint fact_prod) 1313 } 1314 then show ?thesis by (auto simp: binomial_altdef_nat mult_ac prod_atLeastAtMost_code) 1315qed 1316 1317end 1318