src/HOL/Binomial.thy
 changeset 63366 209c4cbbc4cd parent 63363 bd483ddb17f2 child 63367 6c731c8b7f03
equal inserted replaced
63365:5340fb6633d0 63366:209c4cbbc4cd
`    25 lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"`
`    25 lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"`
`    26   by simp`
`    26   by simp`
`    27 `
`    27 `
`    28 lemma of_nat_fact [simp]:`
`    28 lemma of_nat_fact [simp]:`
`    29   "of_nat (fact n) = fact n"`
`    29   "of_nat (fact n) = fact n"`
`    30   by (induct n) (auto simp add: algebra_simps of_nat_mult)`
`    30   by (induct n) (auto simp add: algebra_simps)`
`    31 `
`    31 `
`    32 lemma of_int_fact [simp]:`
`    32 lemma of_int_fact [simp]:`
`    33   "of_int (fact n) = fact n"`
`    33   "of_int (fact n) = fact n"`
`    34 proof -`
`    34 proof -`
`    35   have "of_int (of_nat (fact n)) = fact n"`
`    35   have "of_int (of_nat (fact n)) = fact n"`
`   170 text \<open>This development is based on the work of Andy Gordon and`
`   170 text \<open>This development is based on the work of Andy Gordon and`
`   171   Florian Kammueller.\<close>`
`   171   Florian Kammueller.\<close>`
`   172 `
`   172 `
`   173 subsection \<open>Basic definitions and lemmas\<close>`
`   173 subsection \<open>Basic definitions and lemmas\<close>`
`   174 `
`   174 `
`   175 primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)`
`   175 text \<open>Combinatorial definition\<close>`
`       `
`   176 `
`       `
`   177 definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)`
`   176 where`
`   178 where`
`   177   "0 choose k = (if k = 0 then 1 else 0)"`
`   179   "n choose k = card {K\<in>Pow {..<n}. card K = k}"`
`   178 | "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"`
`   180 `
`   179 `
`   181 theorem n_subsets:`
`   180 lemma binomial_n_0 [simp]: "(n choose 0) = 1"`
`   182   assumes "finite A"`
`   181   by (cases n) simp_all`
`   183   shows "card {B. B \<subseteq> A \<and> card B = k} = card A choose k"`
`   182 `
`   184 proof -`
`   183 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"`
`   185   from assms obtain f where bij: "bij_betw f {..<card A} A"`
`   184   by simp`
`   186     by (blast elim: bij_betw_nat_finite)`
`   185 `
`   187   then have [simp]: "card (f ` C) = card C" if "C \<subseteq> {..<card A}" for C`
`   186 lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"`
`   188     by (meson bij_betw_imp_inj_on bij_betw_subset card_image that)`
`   187   by simp`
`   189   from bij have "bij_betw (image f) (Pow {..<card A}) (Pow A)"`
`       `
`   190     by (rule bij_betw_Pow)`
`       `
`   191   then have "inj_on (image f) (Pow {..<card A})"`
`       `
`   192     by (rule bij_betw_imp_inj_on)`
`       `
`   193   moreover have "{K. K \<subseteq> {..<card A} \<and> card K = k} \<subseteq> Pow {..<card A}"`
`       `
`   194     by auto`
`       `
`   195   ultimately have "inj_on (image f) {K. K \<subseteq> {..<card A} \<and> card K = k}"`
`       `
`   196     by (rule inj_on_subset)`
`       `
`   197   then have "card {K. K \<subseteq> {..<card A} \<and> card K = k} =`
`       `
`   198     card (image f ` {K. K \<subseteq> {..<card A} \<and> card K = k})" (is "_ = card ?C")`
`       `
`   199     by (simp add: card_image)`
`       `
`   200   also have "?C = {K. K \<subseteq> f ` {..<card A} \<and> card K = k}"`
`       `
`   201     by (auto elim!: subset_imageE)`
`       `
`   202   also have "f ` {..<card A} = A"`
`       `
`   203     by (meson bij bij_betw_def)`
`       `
`   204   finally show ?thesis`
`       `
`   205     by (simp add: binomial_def)`
`       `
`   206 qed`
`       `
`   207     `
`       `
`   208 text \<open>Recursive characterization\<close>`
`       `
`   209 `
`       `
`   210 lemma binomial_n_0 [simp, code]:`
`       `
`   211   "n choose 0 = 1"`
`       `
`   212 proof -`
`       `
`   213   have "{K \<in> Pow {..<n}. card K = 0} = {{}}"`
`       `
`   214     by (auto dest: subset_eq_range_finite) `
`       `
`   215   then show ?thesis`
`       `
`   216     by (simp add: binomial_def)`
`       `
`   217 qed`
`       `
`   218 `
`       `
`   219 lemma binomial_0_Suc [simp, code]:`
`       `
`   220   "0 choose Suc k = 0"`
`       `
`   221   by (simp add: binomial_def)`
`       `
`   222 `
`       `
`   223 lemma binomial_Suc_Suc [simp, code]:`
`       `
`   224   "Suc n choose Suc k = (n choose k) + (n choose Suc k)"`
`       `
`   225 proof -`
`       `
`   226   let ?P = "\<lambda>n k. {K. K \<subseteq> {..<n} \<and> card K = k}"`
`       `
`   227   let ?Q = "?P (Suc n) (Suc k)"`
`       `
`   228   have inj: "inj_on (insert n) (?P n k)"`
`       `
`   229     by rule auto`
`       `
`   230   have disjoint: "insert n ` ?P n k \<inter> ?P n (Suc k) = {}"`
`       `
`   231     by auto`
`       `
`   232   have "?Q = {K\<in>?Q. n \<in> K} \<union> {K\<in>?Q. n \<notin> K}"`
`       `
`   233     by auto`
`       `
`   234   also have "{K\<in>?Q. n \<in> K} = insert n ` ?P n k" (is "?A = ?B")`
`       `
`   235   proof (rule set_eqI)`
`       `
`   236     fix K`
`       `
`   237     have K_finite: "finite K" if "K \<subseteq> insert n {..<n}"`
`       `
`   238       using that by (rule finite_subset) simp_all`
`       `
`   239     have Suc_card_K: "Suc (card K - Suc 0) = card K" if "n \<in> K"`
`       `
`   240       and "finite K"`
`       `
`   241     proof -`
`       `
`   242       from \<open>n \<in> K\<close> obtain L where "K = insert n L" and "n \<notin> L"`
`       `
`   243         by (blast elim: Set.set_insert)`
`       `
`   244       with that show ?thesis by (simp add: card_insert)`
`       `
`   245     qed`
`       `
`   246     show "K \<in> ?A \<longleftrightarrow> K \<in> ?B"`
`       `
`   247       by (subst in_image_insert_iff)`
`       `
`   248         (auto simp add: card_insert subset_eq_range_finite Diff_subset_conv K_finite Suc_card_K)`
`       `
`   249   qed    `
`       `
`   250   also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)"`
`       `
`   251     by (auto simp add: lessThan_Suc)`
`       `
`   252   finally show ?thesis using inj disjoint`
`       `
`   253     by (simp add: binomial_def card_Un_disjoint card_image)`
`       `
`   254 qed`
`       `
`   255 `
`       `
`   256 lemma binomial_eq_0:`
`       `
`   257   "n < k \<Longrightarrow> n choose k = 0"`
`       `
`   258   by (auto simp add: binomial_def dest: subset_eq_range_card)`
`       `
`   259 `
`       `
`   260 lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"`
`       `
`   261   by (induct n k rule: diff_induct) simp_all`
`       `
`   262 `
`       `
`   263 lemma binomial_eq_0_iff [simp]:`
`       `
`   264   "n choose k = 0 \<longleftrightarrow> n < k"`
`       `
`   265   by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)`
`       `
`   266 `
`       `
`   267 lemma zero_less_binomial_iff [simp]:`
`       `
`   268   "n choose k > 0 \<longleftrightarrow> k \<le> n"`
`       `
`   269   by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)`
`       `
`   270 `
`       `
`   271 lemma binomial_n_n [simp]: "n choose n = 1"`
`       `
`   272   by (induct n) (simp_all add: binomial_eq_0)`
`       `
`   273 `
`       `
`   274 lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"`
`       `
`   275   by (induct n) simp_all`
`       `
`   276 `
`       `
`   277 lemma binomial_1 [simp]: "n choose Suc 0 = n"`
`       `
`   278   by (induct n) simp_all`
`   188 `
`   279 `
`   189 lemma choose_reduce_nat:`
`   280 lemma choose_reduce_nat:`
`   190   "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>`
`   281   "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>`
`   191     (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"`
`   282     (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"`
`   192   by (metis Suc_diff_1 binomial.simps(2) neq0_conv)`
`   283   using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp`
`   193 `
`       `
`   194 lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"`
`       `
`   195   by (induct n arbitrary: k) auto`
`       `
`   196 `
`       `
`   197 declare binomial.simps [simp del]`
`       `
`   198 `
`       `
`   199 lemma binomial_n_n [simp]: "n choose n = 1"`
`       `
`   200   by (induct n) (simp_all add: binomial_eq_0)`
`       `
`   201 `
`       `
`   202 lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"`
`       `
`   203   by (induct n) simp_all`
`       `
`   204 `
`       `
`   205 lemma binomial_1 [simp]: "n choose Suc 0 = n"`
`       `
`   206   by (induct n) simp_all`
`       `
`   207 `
`       `
`   208 lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"`
`       `
`   209   by (induct n k rule: diff_induct) simp_all`
`       `
`   210 `
`       `
`   211 lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k"`
`       `
`   212   by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)`
`       `
`   213 `
`       `
`   214 lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n"`
`       `
`   215   by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)`
`       `
`   216 `
`   284 `
`   217 lemma Suc_times_binomial_eq:`
`   285 lemma Suc_times_binomial_eq:`
`   218   "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"`
`   286   "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"`
`   219   apply (induct n arbitrary: k, simp add: binomial.simps)`
`   287   apply (induct n arbitrary: k)`
`       `
`   288   apply simp apply arith`
`   220   apply (case_tac k)`
`   289   apply (case_tac k)`
`   221    apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)`
`   290    apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)`
`   222   done`
`   291   done`
`   223 `
`   292 `
`   224 lemma binomial_le_pow2: "n choose k \<le> 2^n"`
`   293 lemma binomial_le_pow2: "n choose k \<le> 2^n"`
`   225   apply (induction n arbitrary: k)`
`   294   apply (induct n arbitrary: k)`
`   226   apply (simp add: binomial.simps)`
`   295   apply (case_tac k) apply simp_all`
`   227   apply (case_tac k)`
`   296   apply (case_tac k)`
`   228   apply (auto simp: power_Suc)`
`   297   apply auto`
`   229   by (simp add: add_le_mono mult_2)`
`   298   apply (simp add: add_le_mono mult_2)`
`       `
`   299   done`
`   230 `
`   300 `
`   231 text\<open>The absorption property\<close>`
`   301 text\<open>The absorption property\<close>`
`   232 lemma Suc_times_binomial:`
`   302 lemma Suc_times_binomial:`
`   233   "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"`
`   303   "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"`
`   234   using Suc_times_binomial_eq by auto`
`   304   using Suc_times_binomial_eq by auto`
`   242 text\<open>Another version of absorption, with -1 instead of Suc.\<close>`
`   312 text\<open>Another version of absorption, with -1 instead of Suc.\<close>`
`   243 lemma times_binomial_minus1_eq:`
`   313 lemma times_binomial_minus1_eq:`
`   244   "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"`
`   314   "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"`
`   245   using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]`
`   315   using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]`
`   246   by (auto split add: nat_diff_split)`
`   316   by (auto split add: nat_diff_split)`
`   307 `
`   317 `
`   308 `
`   318 `
`   309 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>`
`   319 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>`
`   310 `
`   320 `
`   311 text\<open>Avigad's version, generalized to any commutative ring\<close>`
`   321 text\<open>Avigad's version, generalized to any commutative ring\<close>`
`   410   assumes "n > 0"`
`   420   assumes "n > 0"`
`   411   shows   "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"`
`   421   shows   "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"`
`   412 proof -`
`   422 proof -`
`   413   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"`
`   423   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"`
`   414     using choose_row_sum[of n]`
`   424     using choose_row_sum[of n]`
`   415     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)`
`   425     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric])`
`   416   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"`
`   426   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"`
`   417     by (simp add: setsum.distrib)`
`   427     by (simp add: setsum.distrib)`
`   418   also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"`
`   428   also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"`
`   419     by (subst setsum_right_distrib, intro setsum.cong) simp_all`
`   429     by (subst setsum_right_distrib, intro setsum.cong) simp_all`
`   420   finally show ?thesis ..`
`   430   finally show ?thesis ..`
`   424   assumes "n > 0"`
`   434   assumes "n > 0"`
`   425   shows   "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"`
`   435   shows   "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"`
`   426 proof -`
`   436 proof -`
`   427   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"`
`   437   have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"`
`   428     using choose_row_sum[of n]`
`   438     using choose_row_sum[of n]`
`   429     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)`
`   439     by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric])`
`   430   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"`
`   440   also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"`
`   431     by (simp add: setsum_subtractf)`
`   441     by (simp add: setsum_subtractf)`
`   432   also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"`
`   442   also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"`
`   433     by (subst setsum_right_distrib, intro setsum.cong) simp_all`
`   443     by (subst setsum_right_distrib, intro setsum.cong) simp_all`
`   434   finally show ?thesis ..`
`   444   finally show ?thesis ..`
`   473 `
`   483 `
`   474 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"`
`   484 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"`
`   475   by (simp add: pochhammer_def)`
`   485   by (simp add: pochhammer_def)`
`   476 `
`   486 `
`   477 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"`
`   487 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"`
`   478   by (simp add: pochhammer_def of_nat_setprod)`
`   488   by (simp add: pochhammer_def)`
`   479 `
`   489 `
`   480 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"`
`   490 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"`
`   481   by (simp add: pochhammer_def of_int_setprod)`
`   491   by (simp add: pochhammer_def)`
`   482 `
`   492 `
`   483 lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"`
`   493 lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"`
`   484 proof -`
`   494 proof -`
`   485   have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto`
`   495   have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto`
`   486   then show ?thesis by (simp add: field_simps)`
`   496   then show ?thesis by (simp add: field_simps)`
`   535 qed simp_all`
`   545 qed simp_all`
`   536 `
`   546 `
`   537 lemma pochhammer_fact: "fact n = pochhammer 1 n"`
`   547 lemma pochhammer_fact: "fact n = pochhammer 1 n"`
`   538   unfolding fact_altdef`
`   548   unfolding fact_altdef`
`   539   apply (cases n)`
`   549   apply (cases n)`
`   540    apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)`
`   550    apply (simp_all add: pochhammer_Suc_setprod)`
`   541   apply (rule setprod.reindex_cong [where l = Suc])`
`   551   apply (rule setprod.reindex_cong [where l = Suc])`
`   542     apply (auto simp add: fun_eq_iff)`
`   552     apply (auto simp add: fun_eq_iff)`
`   543   done`
`   553   done`
`   544 `
`   554 `
`   545 lemma pochhammer_of_nat_eq_0_lemma:`
`   555 lemma pochhammer_of_nat_eq_0_lemma:`
`   647   have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =`
`   657   have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =`
`   648           (pochhammer z n' * pochhammer (z + 1 / 2) n') *`
`   658           (pochhammer z n' * pochhammer (z + 1 / 2) n') *`
`   649           ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")`
`   659           ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")`
`   650      by (simp_all add: pochhammer_rec' mult_ac)`
`   660      by (simp_all add: pochhammer_rec' mult_ac)`
`   651   also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"`
`   661   also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"`
`   652     (is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult)`
`   662     (is "_ = ?A") by (simp add: field_simps n'_def)`
`   653   also note Suc[folded n'_def]`
`   663   also note Suc[folded n'_def]`
`   654   also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"`
`   664   also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"`
`   655     by (simp add: setprod_nat_ivl_Suc)`
`   665     by (simp add: setprod_nat_ivl_Suc)`
`   656   finally show ?case by (simp add: n'_def)`
`   666   finally show ?case by (simp add: n'_def)`
`   657 qed (simp add: setprod_nat_ivl_Suc)`
`   667 qed (simp add: setprod_nat_ivl_Suc)`
`   661   shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"`
`   671   shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"`
`   662 proof (induction n)`
`   672 proof (induction n)`
`   663   case (Suc n)`
`   673   case (Suc n)`
`   664   have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *`
`   674   have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *`
`   665           (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"`
`   675           (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"`
`   666     by (simp add: pochhammer_rec' ac_simps of_nat_mult)`
`   676     by (simp add: pochhammer_rec' ac_simps)`
`   667   also note Suc`
`   677   also note Suc`
`   668   also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *`
`   678   also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *`
`   669                  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =`
`   679                  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =`
`   670              of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"`
`   680              of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"`
`   671     by (simp add: of_nat_mult field_simps pochhammer_rec')`
`   681     by (simp add: field_simps pochhammer_rec')`
`   672   finally show ?case .`
`   682   finally show ?case .`
`   673 qed simp`
`   683 qed simp`
`   674 `
`   684 `
`   675 lemma fact_double:`
`   685 lemma fact_double:`
`   676   "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"`
`   686   "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"`
`   743     from eq[symmetric]`
`   753     from eq[symmetric]`
`   744     have ?thesis using kn`
`   754     have ?thesis using kn`
`   745       apply (simp add: binomial_fact[OF kn, where ?'a = 'a]`
`   755       apply (simp add: binomial_fact[OF kn, where ?'a = 'a]`
`   746         gbinomial_pochhammer field_simps pochhammer_Suc_setprod)`
`   756         gbinomial_pochhammer field_simps pochhammer_Suc_setprod)`
`   747       apply (simp add: pochhammer_Suc_setprod fact_altdef h`
`   757       apply (simp add: pochhammer_Suc_setprod fact_altdef h`
`   748         of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)`
`   758         setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)`
`   749       unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]`
`   759       unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]`
`   750       unfolding mult.assoc`
`   760       unfolding mult.assoc`
`   751       unfolding setprod.distrib[symmetric]`
`   761       unfolding setprod.distrib[symmetric]`
`   752       apply simp`
`   762       apply simp`
`   753       apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])`
`   763       apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])`
`   770   shows "a * (a gchoose n) =`
`   780   shows "a * (a gchoose n) =`
`   771     of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")`
`   781     of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")`
`   772 proof -`
`   782 proof -`
`   773   have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"`
`   783   have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"`
`   774     unfolding gbinomial_pochhammer`
`   784     unfolding gbinomial_pochhammer`
`   775       pochhammer_Suc of_nat_mult right_diff_distrib power_Suc`
`   785       pochhammer_Suc right_diff_distrib power_Suc`
`   776     apply (simp del: of_nat_Suc fact.simps)`
`   786     apply (simp del: of_nat_Suc fact.simps)`
`   777     apply (auto simp add: field_simps simp del: of_nat_Suc)`
`   787     apply (auto simp add: field_simps simp del: of_nat_Suc)`
`   778     done`
`   788     done`
`   779   also have "\<dots> = ?l" unfolding gbinomial_pochhammer`
`   789   also have "\<dots> = ?l" unfolding gbinomial_pochhammer`
`   780     by (simp add: field_simps)`
`   790     by (simp add: field_simps)`
`   902   case (Suc m)`
`   912   case (Suc m)`
`   903   with assms have "m > 0" by simp`
`   913   with assms have "m > 0" by simp`
`   904   have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =`
`   914   have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =`
`   905             (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)`
`   915             (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)`
`   906   also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"`
`   916   also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"`
`   907     by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp`
`   917     by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] mult_ac of_nat_mult) simp`
`   908   also have "... = -of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat ((m choose i)))"`
`   918   also have "... = -of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat ((m choose i)))"`
`   909     by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)`
`   919     by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)`
`   910        (simp add: algebra_simps of_nat_mult)`
`   920        (simp add: algebra_simps)`
`   911   also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"`
`   921   also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"`
`   912     using choose_alternating_sum[OF \<open>m > 0\<close>] by simp`
`   922     using choose_alternating_sum[OF \<open>m > 0\<close>] by simp`
`   913   finally show ?thesis by simp`
`   923   finally show ?thesis by simp`
`   914 qed simp`
`   924 qed simp`
`   915 `
`   925 `
`   992     from assms have "x * of_nat i \<ge> of_nat (i * k)"`
`  1002     from assms have "x * of_nat i \<ge> of_nat (i * k)"`
`   993       by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)`
`  1003       by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)`
`   994     then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith`
`  1004     then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith`
`   995     then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"`
`  1005     then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"`
`   996       using ik`
`  1006       using ik`
`   997       by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)`
`  1007       by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)`
`   998     then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"`
`  1008     then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"`
`   999       unfolding of_nat_mult[symmetric] of_nat_le_iff .`
`  1009       unfolding of_nat_mult[symmetric] of_nat_le_iff .`
`  1000     with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"`
`  1010     with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"`
`  1001       using \<open>i < k\<close> by (simp add: field_simps)`
`  1011       using \<open>i < k\<close> by (simp add: field_simps)`
`  1002   qed (simp add: x zero_le_divide_iff)`
`  1012   qed (simp add: x zero_le_divide_iff)`
`  1250 `
`  1260 `
`  1251 lemma gbinomial_r_part_sum:`
`  1261 lemma gbinomial_r_part_sum:`
`  1252   "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")`
`  1262   "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")`
`  1253 proof -`
`  1263 proof -`
`  1254   have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"`
`  1264   have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"`
`  1255     by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)`
`  1265     by (simp add: binomial_gbinomial add_ac)`
`  1256   also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)`
`  1266   also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)`
`  1257   finally show ?thesis by (simp add: of_nat_power)`
`  1267   finally show ?thesis by simp`
`  1258 qed`
`  1268 qed`
`  1259 `
`  1269 `
`  1260 lemma gbinomial_sum_nat_pow2:`
`  1270 lemma gbinomial_sum_nat_pow2:`
`  1261    "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")`
`  1271    "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")`
`  1262 proof -`
`  1272 proof -`
`  1314 `
`  1324 `
`  1315 lemma choose_dvd: "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})"`
`  1325 lemma choose_dvd: "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})"`
`  1316   unfolding dvd_def`
`  1326   unfolding dvd_def`
`  1317   apply (rule exI [where x="of_nat (n choose k)"])`
`  1327   apply (rule exI [where x="of_nat (n choose k)"])`
`  1318   using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]`
`  1328   using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]`
`  1319   apply (auto simp: of_nat_mult)`
`  1329   apply auto`
`  1320   done`
`  1330   done`
`  1321 `
`  1331 `
`  1322 lemma fact_fact_dvd_fact:`
`  1332 lemma fact_fact_dvd_fact:`
`  1323     "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"`
`  1333     "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"`
`  1324 by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)`
`  1334 by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)`
`  1556   finally show ?thesis`
`  1566   finally show ?thesis`
`  1557     by (subst (1 2) binomial_altdef_nat)`
`  1567     by (subst (1 2) binomial_altdef_nat)`
`  1558        (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)`
`  1568        (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)`
`  1559 qed`
`  1569 qed`
`  1560 `
`  1570 `
`  1563 lemma fact_code [code]:`
`  1571 lemma fact_code [code]:`
`  1564   "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"`
`  1572   "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"`
`  1565 proof -`
`  1573 proof -`
`  1566   have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)" by (simp add: fact_altdef')`
`  1574   have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)" by (simp add: fact_altdef')`
`  1567   also have "\<Prod>{1..n} = \<Prod>{2..n}"`
`  1575   also have "\<Prod>{1..n} = \<Prod>{2..n}"`