src/HOL/Binomial.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 62347 2230b7047376 child 62481 b5d8e57826df permissions -rw-r--r--
generalize more theorems to support enat and ennreal
 lp15@59669  1 (* Title : Binomial.thy  paulson@12196  2  Author : Jacques D. Fleuriot  paulson@12196  3  Copyright : 1998 University of Cambridge  paulson@15094  4  Conversion to Isar and new proofs by Lawrence C Paulson, 2004  avigad@32036  5  The integer version of factorial and other additions by Jeremy Avigad.  eberlm@61554  6  Additional binomial identities by Chaitanya Mangla and Manuel Eberl  paulson@12196  7 *)  paulson@12196  8 wenzelm@60758  9 section\Factorial Function, Binomial Coefficients and Binomial Theorem\  paulson@15094  10 lp15@59669  11 theory Binomial  haftmann@33319  12 imports Main  nipkow@15131  13 begin  paulson@15094  14 wenzelm@60758  15 subsection \Factorial\  lp15@59730  16 eberlm@61552  17 fun (in semiring_char_0) fact :: "nat \ 'a"  lp15@59730  18  where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"  avigad@32036  19 lp15@59730  20 lemmas fact_Suc = fact.simps(2)  lp15@59730  21 lp15@59730  22 lemma fact_1 [simp]: "fact 1 = 1"  lp15@59730  23  by simp  lp15@59730  24 lp15@59730  25 lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"  lp15@59730  26  by simp  avigad@32036  27 haftmann@62347  28 lemma of_nat_fact [simp]:  haftmann@62347  29  "of_nat (fact n) = fact n"  lp15@59730  30  by (induct n) (auto simp add: algebra_simps of_nat_mult)  hoelzl@62378  31 haftmann@62347  32 lemma of_int_fact [simp]:  haftmann@62347  33  "of_int (fact n) = fact n"  haftmann@62347  34 proof -  haftmann@62347  35  have "of_int (of_nat (fact n)) = fact n"  haftmann@62347  36  unfolding of_int_of_nat_eq by simp  haftmann@62347  37  then show ?thesis  haftmann@62347  38  by simp  haftmann@62347  39 qed  haftmann@62347  40 lp15@59730  41 lemma fact_reduce: "n > 0 \ fact n = of_nat n * fact (n - 1)"  lp15@59730  42  by (cases n) auto  avigad@32036  43 lp15@59733  44 lemma fact_nonzero [simp]: "fact n \ (0::'a::{semiring_char_0,semiring_no_zero_divisors})"  lp15@59730  45  apply (induct n)  lp15@59730  46  apply auto  lp15@59730  47  using of_nat_eq_0_iff by fastforce  lp15@59730  48 lp15@59730  49 lemma fact_mono_nat: "m \ n \ fact m \ (fact n :: nat)"  lp15@59730  50  by (induct n) (auto simp: le_Suc_eq)  avigad@32036  51 eberlm@61531  52 lemma fact_in_Nats: "fact n \ \" by (induction n) auto  eberlm@61531  53 eberlm@61531  54 lemma fact_in_Ints: "fact n \ \" by (induction n) auto  eberlm@61531  55 lp15@59730  56 context  wenzelm@60241  57  assumes "SORT_CONSTRAINT('a::linordered_semidom)"  lp15@59667  58 begin  hoelzl@62378  59 lp15@59730  60  lemma fact_mono: "m \ n \ fact m \ (fact n :: 'a)"  lp15@59730  61  by (metis of_nat_fact of_nat_le_iff fact_mono_nat)  hoelzl@62378  62 lp15@59730  63  lemma fact_ge_1 [simp]: "fact n \ (1 :: 'a)"  lp15@59730  64  by (metis le0 fact.simps(1) fact_mono)  hoelzl@62378  65 lp15@59730  66  lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"  lp15@59730  67  using fact_ge_1 less_le_trans zero_less_one by blast  hoelzl@62378  68 lp15@59730  69  lemma fact_ge_zero [simp]: "fact n \ (0 :: 'a)"  lp15@59730  70  by (simp add: less_imp_le)  avigad@32036  71 lp15@59730  72  lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))"  lp15@59730  73  by (simp add: not_less_iff_gr_or_eq)  hoelzl@62378  74 lp15@59730  75  lemma fact_le_power:  lp15@59730  76  "fact n \ (of_nat (n^n) ::'a)"  lp15@59730  77  proof (induct n)  lp15@59730  78  case (Suc n)  lp15@59730  79  then have *: "fact n \ (of_nat (Suc n ^ n) ::'a)"  lp15@61649  80  by (rule order_trans) (simp add: power_mono del: of_nat_power)  lp15@59730  81  have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"  lp15@59730  82  by (simp add: algebra_simps)  lp15@59730  83  also have "... \ (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)"  lp15@61649  84  by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)  lp15@59730  85  also have "... \ (of_nat (Suc n ^ Suc n) ::'a)"  lp15@59730  86  by (metis of_nat_mult order_refl power_Suc)  lp15@59730  87  finally show ?case .  lp15@59730  88  qed simp  hoelzl@62378  89 avigad@32036  90 end  avigad@32036  91 wenzelm@60758  92 text\Note that @{term "fact 0 = fact 1"}\  lp15@59730  93 lemma fact_less_mono_nat: "\0 < m; m < n\ \ fact m < (fact n :: nat)"  lp15@59730  94  by (induct n) (auto simp: less_Suc_eq)  avigad@32036  95 lp15@59730  96 lemma fact_less_mono:  wenzelm@60241  97  "\0 < m; m < n\ \ fact m < (fact n :: 'a::linordered_semidom)"  lp15@59730  98  by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)  avigad@32036  99 lp15@59730  100 lemma fact_ge_Suc_0_nat [simp]: "fact n \ Suc 0"  lp15@59730  101  by (metis One_nat_def fact_ge_1)  avigad@32036  102 hoelzl@62378  103 lemma dvd_fact:  lp15@59730  104  shows "1 \ m \ m \ n \ m dvd fact n"  lp15@59730  105  by (induct n) (auto simp: dvdI le_Suc_eq)  avigad@32036  106 eberlm@62128  107 lemma fact_ge_self: "fact n \ n"  eberlm@62128  108  by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)  eberlm@62128  109 lp15@59730  110 lemma fact_altdef_nat: "fact n = \{1..n}"  lp15@59730  111  by (induct n) (auto simp: atLeastAtMostSuc_conv)  avigad@32036  112 eberlm@62128  113 lemma fact_altdef: "fact n = (\i=1..n. of_nat i)"  lp15@59730  114  by (induct n) (auto simp: atLeastAtMostSuc_conv)  hoelzl@62378  115 eberlm@62128  116 lemma fact_altdef': "fact n = of_nat (\{1..n})"  eberlm@62128  117  by (subst fact_altdef_nat [symmetric]) simp  paulson@15094  118 lp15@59730  119 lemma fact_dvd: "n \ m \ fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"  lp15@59730  120  by (induct m) (auto simp: le_Suc_eq)  avigad@32036  121 lp15@59730  122 lemma fact_mod: "m \ n \ fact n mod (fact m :: 'a :: {semiring_div,linordered_semidom}) = 0"  lp15@59730  123  by (auto simp add: fact_dvd)  bulwahn@40033  124 bulwahn@40033  125 lemma fact_div_fact:  lp15@59730  126  assumes "m \ n"  bulwahn@40033  127  shows "(fact m) div (fact n) = \{n + 1..m}"  bulwahn@40033  128 proof -  bulwahn@40033  129  obtain d where "d = m - n" by auto  bulwahn@40033  130  from assms this have "m = n + d" by auto  bulwahn@40033  131  have "fact (n + d) div (fact n) = \{n + 1..n + d}"  bulwahn@40033  132  proof (induct d)  bulwahn@40033  133  case 0  bulwahn@40033  134  show ?case by simp  bulwahn@40033  135  next  bulwahn@40033  136  case (Suc d')  bulwahn@40033  137  have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"  bulwahn@40033  138  by simp  lp15@59667  139  also from Suc.hyps have "... = Suc (n + d') * \{n + 1..n + d'}"  bulwahn@40033  140  unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)  bulwahn@40033  141  also have "... = \{n + 1..n + Suc d'}"  lp15@59730  142  by (simp add: atLeastAtMostSuc_conv)  bulwahn@40033  143  finally show ?case .  bulwahn@40033  144  qed  wenzelm@60758  145  from this \m = n + d\ show ?thesis by simp  bulwahn@40033  146 qed  bulwahn@40033  147 hoelzl@62378  148 lemma fact_num_eq_if:  lp15@59730  149  "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))"  avigad@32036  150 by (cases m) auto  avigad@32036  151 lp15@59730  152 lemma fact_eq_rev_setprod_nat: "fact k = (\i n" shows "fact n div fact (n - r) \ n ^ r"  hoelzl@50240  158 proof -  hoelzl@50240  159  have "\r. r \ n \ \{n - r..n} = (n - r) * \{Suc (n - r)..n}"  haftmann@57418  160  by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)  hoelzl@50240  161  with assms show ?thesis  hoelzl@50240  162  by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)  hoelzl@50240  163 qed  hoelzl@50240  164 wenzelm@61799  165 lemma fact_numeral: \\Evaluation for specific numerals\  lp15@57113  166  "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"  lp15@59730  167  by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)  lp15@57113  168 lp15@59658  169 wenzelm@60758  170 text \This development is based on the work of Andy Gordon and  wenzelm@60758  171  Florian Kammueller.\  lp15@59658  172 wenzelm@60758  173 subsection \Basic definitions and lemmas\  lp15@59658  174 lp15@59658  175 primrec binomial :: "nat \ nat \ nat" (infixl "choose" 65)  lp15@59658  176 where  lp15@59658  177  "0 choose k = (if k = 0 then 1 else 0)"  lp15@59658  178 | "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"  lp15@59658  179 lp15@59658  180 lemma binomial_n_0 [simp]: "(n choose 0) = 1"  lp15@59658  181  by (cases n) simp_all  lp15@59658  182 lp15@59658  183 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"  lp15@59658  184  by simp  lp15@59658  185 lp15@59658  186 lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"  lp15@59658  187  by simp  lp15@59658  188 lp15@59667  189 lemma choose_reduce_nat:  lp15@59658  190  "0 < (n::nat) \ 0 < k \  lp15@59658  191  (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"  lp15@59658  192  by (metis Suc_diff_1 binomial.simps(2) neq0_conv)  lp15@59658  193 lp15@59658  194 lemma binomial_eq_0: "n < k \ n choose k = 0"  lp15@59658  195  by (induct n arbitrary: k) auto  lp15@59658  196 lp15@59658  197 declare binomial.simps [simp del]  lp15@59658  198 lp15@59658  199 lemma binomial_n_n [simp]: "n choose n = 1"  lp15@59658  200  by (induct n) (simp_all add: binomial_eq_0)  lp15@59658  201 lp15@59658  202 lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"  lp15@59658  203  by (induct n) simp_all  lp15@59658  204 lp15@59658  205 lemma binomial_1 [simp]: "n choose Suc 0 = n"  lp15@59658  206  by (induct n) simp_all  lp15@59658  207 lp15@59658  208 lemma zero_less_binomial: "k \ n \ n choose k > 0"  lp15@59658  209  by (induct n k rule: diff_induct) simp_all  lp15@59658  210 lp15@59658  211 lemma binomial_eq_0_iff [simp]: "n choose k = 0 \ n < k"  lp15@59658  212  by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)  lp15@59658  213 lp15@59658  214 lemma zero_less_binomial_iff [simp]: "n choose k > 0 \ k \ n"  lp15@59658  215  by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)  lp15@59658  216 lp15@59658  217 lemma Suc_times_binomial_eq:  lp15@59658  218  "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"  lp15@59658  219  apply (induct n arbitrary: k, simp add: binomial.simps)  lp15@59658  220  apply (case_tac k)  lp15@59658  221  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)  lp15@59658  222  done  lp15@59658  223 lp15@60141  224 lemma binomial_le_pow2: "n choose k \ 2^n"  lp15@60141  225  apply (induction n arbitrary: k)  lp15@60141  226  apply (simp add: binomial.simps)  lp15@60141  227  apply (case_tac k)  lp15@60141  228  apply (auto simp: power_Suc)  lp15@60141  229  by (simp add: add_le_mono mult_2)  lp15@60141  230 wenzelm@60758  231 text\The absorption property\  lp15@59658  232 lemma Suc_times_binomial:  lp15@59658  233  "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"  lp15@59658  234  using Suc_times_binomial_eq by auto  lp15@59658  235 wenzelm@60758  236 text\This is the well-known version of absorption, but it's harder to use because of the  wenzelm@60758  237  need to reason about division.\  lp15@59658  238 lemma binomial_Suc_Suc_eq_times:  lp15@59658  239  "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"  lp15@59658  240  by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)  lp15@59658  241 wenzelm@60758  242 text\Another version of absorption, with -1 instead of Suc.\  lp15@59658  243 lemma times_binomial_minus1_eq:  lp15@59658  244  "0 < k \ k * (n choose k) = n * ((n - 1) choose (k - 1))"  lp15@59658  245  using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]  lp15@59658  246  by (auto split add: nat_diff_split)  lp15@59658  247 lp15@59658  248 wenzelm@61799  249 subsection \Combinatorial theorems involving \choose\\  lp15@59658  250 wenzelm@60758  251 text \By Florian Kamm\"uller, tidied by LCP.\  lp15@59658  252 lp15@59658  253 lemma card_s_0_eq_empty: "finite A \ card {B. B \ A & card B = 0} = 1"  lp15@59658  254  by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])  lp15@59658  255 lp15@59658  256 lemma choose_deconstruct: "finite M \ x \ M \  lp15@59658  257  {s. s \ insert x M \ card s = Suc k} =  lp15@59658  258  {s. s \ M \ card s = Suc k} \ {s. \t. t \ M \ card t = k \ s = insert x t}"  lp15@59658  259  apply safe  lp15@59658  260  apply (auto intro: finite_subset [THEN card_insert_disjoint])  lp15@59667  261  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if  lp15@59658  262  card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)  lp15@59658  263 lp15@59658  264 lemma finite_bex_subset [simp]:  lp15@59658  265  assumes "finite B"  lp15@59658  266  and "\A. A \ B \ finite {x. P x A}"  lp15@59658  267  shows "finite {x. \A \ B. P x A}"  lp15@59658  268  by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)  lp15@59658  269 wenzelm@60758  270 text\There are as many subsets of @{term A} having cardinality @{term k}  lp15@59658  271  as there are sets obtained from the former by inserting a fixed element  wenzelm@60758  272  @{term x} into each.\  lp15@59658  273 lemma constr_bij:  lp15@59658  274  "finite A \ x \ A \  lp15@59658  275  card {B. \C. C \ A \ card C = k \ B = insert x C} =  lp15@59658  276  card {B. B \ A & card(B) = k}"  lp15@59658  277  apply (rule card_bij_eq [where f = "\s. s - {x}" and g = "insert x"])  lp15@59658  278  apply (auto elim!: equalityE simp add: inj_on_def)  lp15@59658  279  apply (metis card_Diff_singleton_if finite_subset in_mono)  lp15@59658  280  done  lp15@59658  281 wenzelm@60758  282 text \  lp15@59658  283  Main theorem: combinatorial statement about number of subsets of a set.  wenzelm@60758  284 \  lp15@59658  285 lp15@59658  286 theorem n_subsets: "finite A \ card {B. B \ A \ card B = k} = (card A choose k)"  lp15@59658  287 proof (induct k arbitrary: A)  lp15@59658  288  case 0 then show ?case by (simp add: card_s_0_eq_empty)  lp15@59658  289 next  lp15@59658  290  case (Suc k)  wenzelm@60758  291  show ?case using \finite A\  lp15@59658  292  proof (induct A)  lp15@59658  293  case empty show ?case by (simp add: card_s_0_eq_empty)  lp15@59658  294  next  lp15@59658  295  case (insert x A)  lp15@59658  296  then show ?case using Suc.hyps  lp15@59658  297  apply (simp add: card_s_0_eq_empty choose_deconstruct)  lp15@59658  298  apply (subst card_Un_disjoint)  lp15@59658  299  prefer 4 apply (force simp add: constr_bij)  lp15@59658  300  prefer 3 apply force  lp15@59658  301  prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]  lp15@59658  302  finite_subset [of _ "Pow (insert x F)" for F])  lp15@59658  303  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])  lp15@59658  304  done  lp15@59658  305  qed  lp15@59658  306 qed  lp15@59658  307 lp15@59658  308 wenzelm@60758  309 subsection \The binomial theorem (courtesy of Tobias Nipkow):\  lp15@59658  310 wenzelm@60758  311 text\Avigad's version, generalized to any commutative ring\  lp15@59667  312 theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n =  lp15@59658  313  (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")  lp15@59658  314 proof (induct n)  lp15@59658  315  case 0 then show "?P 0" by simp  lp15@59658  316 next  lp15@59658  317  case (Suc n)  lp15@59658  318  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"  lp15@59658  319  by auto  lp15@59658  320  have decomp2: "{0..n} = {0} Un {1..n}"  lp15@59658  321  by auto  lp15@59667  322  have "(a+b)^(n+1) =  lp15@59658  323  (a+b) * (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))"  lp15@59658  324  using Suc.hyps by simp  lp15@59658  325  also have "\ = a*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +  lp15@59658  326  b*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k))"  lp15@59658  327  by (rule distrib_right)  lp15@59658  328  also have "\ = (\k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +  lp15@59658  329  (\k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"  lp15@59658  330  by (auto simp add: setsum_right_distrib ac_simps)  lp15@59658  331  also have "\ = (\k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +  lp15@59658  332  (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"  lp15@59667  333  by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps  lp15@59658  334  del:setsum_cl_ivl_Suc)  lp15@59658  335  also have "\ = a^(n+1) + b^(n+1) +  lp15@59658  336  (\k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +  lp15@59658  337  (\k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"  lp15@59658  338  by (simp add: decomp2)  lp15@59658  339  also have  lp15@59667  340  "\ = a^(n+1) + b^(n+1) +  lp15@59658  341  (\k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"  lp15@59658  342  by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat)  lp15@59658  343  also have "\ = (\k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"  lp15@59658  344  using decomp by (simp add: field_simps)  lp15@59658  345  finally show "?P (Suc n)" by simp  lp15@59658  346 qed  lp15@59658  347 wenzelm@60758  348 text\Original version for the naturals\  lp15@59658  349 corollary binomial: "(a+b::nat)^n = (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"  lp15@59658  350  using binomial_ring [of "int a" "int b" n]  lp15@59658  351  by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]  lp15@59658  352  of_nat_setsum [symmetric]  lp15@59658  353  of_nat_eq_iff of_nat_id)  lp15@59658  354 lp15@59658  355 lemma binomial_fact_lemma: "k \ n \ fact k * fact (n - k) * (n choose k) = fact n"  lp15@59658  356 proof (induct n arbitrary: k rule: nat_less_induct)  lp15@59658  357  fix n k assume H: "\mx\m. fact x * fact (m - x) * (m choose x) =  lp15@59658  358  fact m" and kn: "k \ n"  lp15@59658  359  let ?ths = "fact k * fact (n - k) * (n choose k) = fact n"  lp15@59658  360  { assume "n=0" then have ?ths using kn by simp }  lp15@59658  361  moreover  lp15@59658  362  { assume "k=0" then have ?ths using kn by simp }  lp15@59658  363  moreover  lp15@59658  364  { assume nk: "n=k" then have ?ths by simp }  lp15@59658  365  moreover  lp15@59658  366  { fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m"  lp15@59658  367  from n have mn: "m < n" by arith  lp15@59658  368  from hm have hm': "h \ m" by arith  lp15@59658  369  from hm h n kn have km: "k \ m" by arith  lp15@59658  370  have "m - h = Suc (m - Suc h)" using h km hm by arith  lp15@59658  371  with km h have th0: "fact (m - h) = (m - h) * fact (m - k)"  lp15@59658  372  by simp  lp15@59658  373  from n h th0  lp15@59658  374  have "fact k * fact (n - k) * (n choose k) =  lp15@59667  375  k * (fact h * fact (m - h) * (m choose h)) +  lp15@59658  376  (m - h) * (fact k * fact (m - k) * (m choose k))"  lp15@59658  377  by (simp add: field_simps)  lp15@59658  378  also have "\ = (k + (m - h)) * fact m"  lp15@59658  379  using H[rule_format, OF mn hm'] H[rule_format, OF mn km]  lp15@59658  380  by (simp add: field_simps)  lp15@59658  381  finally have ?ths using h n km by simp }  lp15@59658  382  moreover have "n=0 \ k = 0 \ k = n \ (\m h. n = Suc m \ k = Suc h \ h < m)"  lp15@59658  383  using kn by presburger  lp15@59658  384  ultimately show ?ths by blast  lp15@59658  385 qed  lp15@59658  386 lp15@59658  387 lemma binomial_fact:  lp15@59658  388  assumes kn: "k \ n"  lp15@59730  389  shows "(of_nat (n choose k) :: 'a::field_char_0) =  lp15@59730  390  (fact n) / (fact k * fact(n - k))"  lp15@59658  391  using binomial_fact_lemma[OF kn]  lp15@59730  392  apply (simp add: field_simps)  lp15@59730  393  by (metis mult.commute of_nat_fact of_nat_mult)  lp15@59658  394 lp15@59667  395 lemma choose_row_sum: "(\k=0..n. n choose k) = 2^n"  lp15@59667  396  using binomial [of 1 "1" n]  lp15@59667  397  by (simp add: numeral_2_eq_2)  lp15@59667  398 lp15@59667  399 lemma sum_choose_lower: "(\k=0..n. (r+k) choose k) = Suc (r+n) choose n"  lp15@59667  400  by (induct n) auto  lp15@59667  401 lp15@59667  402 lemma sum_choose_upper: "(\k=0..n. k choose m) = Suc n choose Suc m"  lp15@59667  403  by (induct n) auto  lp15@59667  404 hoelzl@62378  405 lemma choose_alternating_sum:  eberlm@61531  406  "n > 0 \ (\i\n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"  eberlm@61531  407  using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)  eberlm@61531  408 eberlm@61531  409 lemma choose_even_sum:  eberlm@61531  410  assumes "n > 0"  eberlm@61531  411  shows "2 * (\i\n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"  hoelzl@62378  412 proof -  eberlm@61531  413  have "2 ^ n = (\i\n. of_nat (n choose i)) + (\i\n. (-1) ^ i * of_nat (n choose i) :: 'a)"  eberlm@61531  414  using choose_row_sum[of n]  eberlm@61531  415  by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)  eberlm@61531  416  also have "\ = (\i\n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"  eberlm@61531  417  by (simp add: setsum.distrib)  hoelzl@62378  418  also have "\ = 2 * (\i\n. if even i then of_nat (n choose i) else 0)"  eberlm@61531  419  by (subst setsum_right_distrib, intro setsum.cong) simp_all  eberlm@61531  420  finally show ?thesis ..  eberlm@61531  421 qed  eberlm@61531  422 eberlm@61531  423 lemma choose_odd_sum:  eberlm@61531  424  assumes "n > 0"  eberlm@61531  425  shows "2 * (\i\n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"  hoelzl@62378  426 proof -  eberlm@61531  427  have "2 ^ n = (\i\n. of_nat (n choose i)) - (\i\n. (-1) ^ i * of_nat (n choose i) :: 'a)"  eberlm@61531  428  using choose_row_sum[of n]  eberlm@61531  429  by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)  eberlm@61531  430  also have "\ = (\i\n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"  eberlm@61531  431  by (simp add: setsum_subtractf)  hoelzl@62378  432  also have "\ = 2 * (\i\n. if odd i then of_nat (n choose i) else 0)"  eberlm@61531  433  by (subst setsum_right_distrib, intro setsum.cong) simp_all  eberlm@61531  434  finally show ?thesis ..  eberlm@61531  435 qed  eberlm@61531  436 eberlm@61531  437 lemma choose_row_sum': "(\k\n. (n choose k)) = 2 ^ n"  eberlm@61531  438  using choose_row_sum[of n] by (simp add: atLeast0AtMost)  eberlm@61531  439 lp15@59667  440 lemma natsum_reverse_index:  lp15@59667  441  fixes m::nat  lp15@59667  442  shows "(\k. m \ k \ k \ n \ g k = f (m + n - k)) \ (\k=m..n. f k) = (\k=m..n. g k)"  lp15@59667  443  by (rule setsum.reindex_bij_witness[where i="\k. m+n-k" and j="\k. m+n-k"]) auto  lp15@59667  444 wenzelm@60758  445 text\NW diagonal sum property\  lp15@59667  446 lemma sum_choose_diagonal:  lp15@59667  447  assumes "m\n" shows "(\k=0..m. (n-k) choose (m-k)) = Suc n choose m"  lp15@59667  448 proof -  lp15@59667  449  have "(\k=0..m. (n-k) choose (m-k)) = (\k=0..m. (n-m+k) choose k)"  lp15@59667  450  by (rule natsum_reverse_index) (simp add: assms)  lp15@59667  451  also have "... = Suc (n-m+m) choose m"  lp15@59667  452  by (rule sum_choose_lower)  lp15@59667  453  also have "... = Suc n choose m" using assms  lp15@59667  454  by simp  lp15@59667  455  finally show ?thesis .  lp15@59667  456 qed  lp15@59667  457 wenzelm@60758  458 subsection\Pochhammer's symbol : generalized rising factorial\  lp15@59667  459 wenzelm@60758  460 text \See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\  lp15@59667  461 eberlm@61552  462 definition (in comm_semiring_1) "pochhammer (a :: 'a) n =  lp15@59667  463  (if n = 0 then 1 else setprod (\n. a + of_nat n) {0 .. n - 1})"  lp15@59667  464 lp15@59667  465 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"  lp15@59667  466  by (simp add: pochhammer_def)  lp15@59667  467 lp15@59667  468 lemma pochhammer_1 [simp]: "pochhammer a 1 = a"  lp15@59667  469  by (simp add: pochhammer_def)  lp15@59667  470 lp15@59667  471 lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"  lp15@59667  472  by (simp add: pochhammer_def)  lp15@59667  473 lp15@59667  474 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\n. a + of_nat n) {0 .. n}"  lp15@59667  475  by (simp add: pochhammer_def)  hoelzl@62378  476 eberlm@61531  477 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"  eberlm@61531  478  by (simp add: pochhammer_def of_nat_setprod)  eberlm@61531  479 eberlm@61531  480 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"  eberlm@61531  481  by (simp add: pochhammer_def of_int_setprod)  lp15@59667  482 lp15@59667  483 lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"  lp15@59667  484 proof -  lp15@59667  485  have "{0..Suc n} = {0..n} \ {Suc n}" by auto  lp15@59667  486  then show ?thesis by (simp add: field_simps)  lp15@59667  487 qed  lp15@59667  488 lp15@59667  489 lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"  lp15@59667  490 proof -  lp15@59667  491  have "{0..Suc n} = {0} \ {1 .. Suc n}" by auto  lp15@59667  492  then show ?thesis by simp  lp15@59667  493 qed  lp15@59667  494 lp15@59667  495 lp15@59667  496 lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"  lp15@59667  497 proof (cases n)  lp15@59667  498  case 0  lp15@59667  499  then show ?thesis by simp  lp15@59667  500 next  lp15@59667  501  case (Suc n)  lp15@59667  502  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..  lp15@59667  503 qed  lp15@59667  504 lp15@59667  505 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"  lp15@59667  506 proof (cases "n = 0")  lp15@59667  507  case True  lp15@59667  508  then show ?thesis by (simp add: pochhammer_Suc_setprod)  lp15@59667  509 next  lp15@59667  510  case False  lp15@59667  511  have *: "finite {1 .. n}" "0 \ {1 .. n}" by auto  lp15@59667  512  have eq: "insert 0 {1 .. n} = {0..n}" by auto  wenzelm@61076  513  have **: "(\n\{1::nat..n}. a + of_nat n) = (\n\{0::nat..n - 1}. a + 1 + of_nat n)"  lp15@59667  514  apply (rule setprod.reindex_cong [where l = Suc])  lp15@59667  515  using False  lp15@59667  516  apply (auto simp add: fun_eq_iff field_simps)  lp15@59667  517  done  lp15@59667  518  show ?thesis  lp15@59667  519  apply (simp add: pochhammer_def)  lp15@59667  520  unfolding setprod.insert [OF *, unfolded eq]  lp15@59667  521  using ** apply (simp add: field_simps)  lp15@59667  522  done  lp15@59667  523 qed  lp15@59667  524 eberlm@61531  525 lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"  eberlm@61531  526 proof (induction n arbitrary: z)  eberlm@61531  527  case (Suc n z)  hoelzl@62378  528  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"  eberlm@61531  529  by (simp add: pochhammer_rec)  eberlm@61531  530  also note Suc  hoelzl@62378  531  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =  eberlm@61531  532  (z + of_nat (Suc n)) * pochhammer z (Suc n)"  eberlm@61531  533  by (simp_all add: pochhammer_rec algebra_simps)  eberlm@61531  534  finally show ?case .  eberlm@61531  535 qed simp_all  eberlm@61531  536 lp15@59730  537 lemma pochhammer_fact: "fact n = pochhammer 1 n"  lp15@59730  538  unfolding fact_altdef  lp15@59667  539  apply (cases n)  lp15@59667  540  apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)  lp15@59667  541  apply (rule setprod.reindex_cong [where l = Suc])  lp15@59667  542  apply (auto simp add: fun_eq_iff)  lp15@59667  543  done  lp15@59667  544 lp15@59667  545 lemma pochhammer_of_nat_eq_0_lemma:  lp15@59667  546  assumes "k > n"  lp15@59667  547  shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"  lp15@59667  548 proof (cases "n = 0")  lp15@59667  549  case True  lp15@59667  550  then show ?thesis  lp15@59667  551  using assms by (cases k) (simp_all add: pochhammer_rec)  lp15@59667  552 next  lp15@59667  553  case False  lp15@59667  554  from assms obtain h where "k = Suc h" by (cases k) auto  lp15@59667  555  then show ?thesis  lp15@59667  556  by (simp add: pochhammer_Suc_setprod)  lp15@59667  557  (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))  lp15@59667  558 qed  lp15@59667  559 lp15@59667  560 lemma pochhammer_of_nat_eq_0_lemma':  lp15@59667  561  assumes kn: "k \ n"  lp15@59667  562  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \ 0"  lp15@59667  563 proof (cases k)  lp15@59667  564  case 0  lp15@59667  565  then show ?thesis by simp  lp15@59667  566 next  lp15@59667  567  case (Suc h)  lp15@59667  568  then show ?thesis  lp15@59667  569  apply (simp add: pochhammer_Suc_setprod)  lp15@59667  570  using Suc kn apply (auto simp add: algebra_simps)  lp15@59667  571  done  lp15@59667  572 qed  lp15@59667  573 lp15@59667  574 lemma pochhammer_of_nat_eq_0_iff:  lp15@59667  575  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \ k > n"  lp15@59667  576  (is "?l = ?r")  lp15@59667  577  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]  lp15@59667  578  pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]  lp15@59667  579  by (auto simp add: not_le[symmetric])  lp15@59667  580 lp15@59667  581 lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \ (\k < n. a = - of_nat k)"  lp15@59667  582  apply (auto simp add: pochhammer_of_nat_eq_0_iff)  lp15@59667  583  apply (cases n)  lp15@59667  584  apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)  lp15@59667  585  apply (metis leD not_less_eq)  lp15@59667  586  done  lp15@59667  587 lp15@59667  588 lemma pochhammer_eq_0_mono:  lp15@59667  589  "pochhammer a n = (0::'a::field_char_0) \ m \ n \ pochhammer a m = 0"  lp15@59667  590  unfolding pochhammer_eq_0_iff by auto  lp15@59667  591 lp15@59667  592 lemma pochhammer_neq_0_mono:  lp15@59667  593  "pochhammer a m \ (0::'a::field_char_0) \ m \ n \ pochhammer a n \ 0"  lp15@59667  594  unfolding pochhammer_eq_0_iff by auto  lp15@59667  595 lp15@59667  596 lemma pochhammer_minus:  lp15@59862  597  "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"  lp15@59667  598 proof (cases k)  lp15@59667  599  case 0  lp15@59667  600  then show ?thesis by simp  lp15@59667  601 next  lp15@59667  602  case (Suc h)  lp15@59667  603  have eq: "((- 1) ^ Suc h :: 'a) = (\i=0..h. - 1)"  lp15@59667  604  using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]  lp15@59667  605  by auto  lp15@59667  606  show ?thesis  lp15@59667  607  unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]  lp15@59667  608  by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])  lp15@59667  609  (auto simp: of_nat_diff)  lp15@59667  610 qed  lp15@59667  611 lp15@59667  612 lemma pochhammer_minus':  lp15@59862  613  "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"  lp15@59862  614  unfolding pochhammer_minus[where b=b]  lp15@59667  615  unfolding mult.assoc[symmetric]  lp15@59667  616  unfolding power_add[symmetric]  lp15@59667  617  by simp  lp15@59667  618 lp15@59667  619 lemma pochhammer_same: "pochhammer (- of_nat n) n =  lp15@59730  620  ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)"  lp15@59862  621  unfolding pochhammer_minus  lp15@59667  622  by (simp add: of_nat_diff pochhammer_fact)  lp15@59667  623 hoelzl@62378  624 lemma pochhammer_product':  eberlm@61531  625  "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"  eberlm@61531  626 proof (induction n arbitrary: z)  eberlm@61531  627  case (Suc n z)  hoelzl@62378  628  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =  eberlm@61531  629  z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"  eberlm@61531  630  by (simp add: pochhammer_rec ac_simps)  eberlm@61531  631  also note Suc[symmetric]  eberlm@61531  632  also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"  eberlm@61531  633  by (subst pochhammer_rec) simp  eberlm@61531  634  finally show ?case by simp  eberlm@61531  635 qed simp  eberlm@61531  636 hoelzl@62378  637 lemma pochhammer_product:  eberlm@61531  638  "m \ n \ pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"  eberlm@61531  639  using pochhammer_product'[of z m "n - m"] by simp  eberlm@61531  640 eberlm@61552  641 lemma pochhammer_times_pochhammer_half:  eberlm@61552  642  fixes z :: "'a :: field_char_0"  eberlm@61552  643  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\k=0..2*n+1. z + of_nat k / 2)"  eberlm@61552  644 proof (induction n)  eberlm@61552  645  case (Suc n)  eberlm@61552  646  def n' \ "Suc n"  eberlm@61552  647  have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =  hoelzl@62378  648  (pochhammer z n' * pochhammer (z + 1 / 2) n') *  eberlm@61552  649  ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")  eberlm@61552  650  by (simp_all add: pochhammer_rec' mult_ac)  eberlm@61552  651  also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"  eberlm@61552  652  (is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult)  eberlm@61552  653  also note Suc[folded n'_def]  eberlm@61552  654  also have "(\k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\k = 0..2 * Suc n + 1. z + of_nat k / 2)"  eberlm@61552  655  by (simp add: setprod_nat_ivl_Suc)  eberlm@61552  656  finally show ?case by (simp add: n'_def)  eberlm@61552  657 qed (simp add: setprod_nat_ivl_Suc)  eberlm@61552  658 eberlm@61552  659 lemma pochhammer_double:  eberlm@61552  660  fixes z :: "'a :: field_char_0"  eberlm@61552  661  shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"  eberlm@61552  662 proof (induction n)  eberlm@61552  663  case (Suc n)  hoelzl@62378  664  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *  eberlm@61552  665  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"  eberlm@61552  666  by (simp add: pochhammer_rec' ac_simps of_nat_mult)  eberlm@61552  667  also note Suc  eberlm@61552  668  also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *  eberlm@61552  669  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =  eberlm@61552  670  of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"  eberlm@61552  671  by (simp add: of_nat_mult field_simps pochhammer_rec')  eberlm@61552  672  finally show ?case .  eberlm@61552  673 qed simp  eberlm@61552  674 eberlm@61531  675 lemma pochhammer_absorb_comp:  hoelzl@62378  676  "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"  eberlm@61531  677  (is "?lhs = ?rhs")  eberlm@61531  678 proof -  eberlm@61531  679  have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)  eberlm@61531  680  also have "\ = ?rhs" by (subst pochhammer_rec) simp  eberlm@61531  681  finally show ?thesis .  eberlm@61531  682 qed  eberlm@61531  683 lp15@59667  684 wenzelm@60758  685 subsection\Generalized binomial coefficients\  lp15@59667  686 eberlm@61552  687 definition (in field_char_0) gbinomial :: "'a \ nat \ 'a" (infixl "gchoose" 65)  lp15@59667  688  where "a gchoose n =  lp15@59730  689  (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / (fact n))"  lp15@59667  690 lp15@59667  691 lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"  haftmann@59867  692  by (simp_all add: gbinomial_def)  lp15@59667  693 lp15@59730  694 lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"  lp15@59667  695 proof (cases "n = 0")  lp15@59667  696  case True  lp15@59667  697  then show ?thesis by simp  lp15@59667  698 next  lp15@59667  699  case False  lp15@59667  700  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]  wenzelm@61076  701  have eq: "(- (1::'a)) ^ n = setprod (\i. - 1) {0 .. n - 1}"  lp15@59667  702  by auto  lp15@59667  703  from False show ?thesis  lp15@59667  704  by (simp add: pochhammer_def gbinomial_def field_simps  lp15@59667  705  eq setprod.distrib[symmetric])  lp15@59667  706 qed  lp15@59667  707 eberlm@61552  708 lemma gbinomial_pochhammer':  eberlm@61552  709  "(s :: 'a :: field_char_0) gchoose n = pochhammer (s - of_nat n + 1) n / fact n"  eberlm@61552  710 proof -  eberlm@61552  711  have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"  eberlm@61552  712  by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)  eberlm@61552  713  also have "(-1 :: 'a)^n * (-1)^n = 1" by (subst power_add [symmetric]) simp  eberlm@61552  714  finally show ?thesis by simp  eberlm@61552  715 qed  eberlm@61552  716 hoelzl@62378  717 lemma binomial_gbinomial:  lp15@59730  718  "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"  lp15@59667  719 proof -  lp15@59667  720  { assume kn: "k > n"  lp15@59667  721  then have ?thesis  lp15@59667  722  by (subst binomial_eq_0[OF kn])  lp15@59667  723  (simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff) }  lp15@59667  724  moreover  lp15@59667  725  { assume "k=0" then have ?thesis by simp }  lp15@59667  726  moreover  lp15@59667  727  { assume kn: "k \ n" and k0: "k\ 0"  lp15@59667  728  from k0 obtain h where h: "k = Suc h" by (cases k) auto  lp15@59667  729  from h  lp15@59667  730  have eq:"(- 1 :: 'a) ^ k = setprod (\i. - 1) {0..h}"  lp15@59667  731  by (subst setprod_constant) auto  lp15@59667  732  have eq': "(\i\{0..h}. of_nat n + - (of_nat i :: 'a)) = (\i\{n - h..n}. of_nat i)"  lp15@59667  733  using h kn  lp15@59667  734  by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])  lp15@59667  735  (auto simp: of_nat_diff)  lp15@59667  736  have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"  lp15@59667  737  "{1..n - Suc h} \ {n - h .. n} = {}" and  lp15@59667  738  eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}"  lp15@59667  739  using h kn by auto  lp15@59667  740  from eq[symmetric]  lp15@59667  741  have ?thesis using kn  lp15@59667  742  apply (simp add: binomial_fact[OF kn, where ?'a = 'a]  lp15@59667  743  gbinomial_pochhammer field_simps pochhammer_Suc_setprod)  hoelzl@62378  744  apply (simp add: pochhammer_Suc_setprod fact_altdef h  lp15@59667  745  of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)  lp15@59667  746  unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h]  lp15@59730  747  unfolding mult.assoc  lp15@59667  748  unfolding setprod.distrib[symmetric]  lp15@59667  749  apply simp  lp15@59667  750  apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])  lp15@59667  751  apply (auto simp: of_nat_diff)  lp15@59667  752  done  lp15@59667  753  }  lp15@59667  754  moreover  lp15@59667  755  have "k > n \ k = 0 \ (k \ n \ k \ 0)" by arith  lp15@59667  756  ultimately show ?thesis by blast  lp15@59667  757 qed  lp15@59667  758 lp15@59667  759 lemma gbinomial_1[simp]: "a gchoose 1 = a"  lp15@59667  760  by (simp add: gbinomial_def)  lp15@59667  761 lp15@59667  762 lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"  lp15@59667  763  by (simp add: gbinomial_def)  lp15@59667  764 lp15@59667  765 lemma gbinomial_mult_1:  lp15@59730  766  fixes a :: "'a :: field_char_0"  lp15@59730  767  shows "a * (a gchoose n) =  lp15@59667  768  of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r")  lp15@59667  769 proof -  lp15@59730  770  have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"  lp15@59667  771  unfolding gbinomial_pochhammer  lp15@59730  772  pochhammer_Suc of_nat_mult right_diff_distrib power_Suc  lp15@59730  773  apply (simp del: of_nat_Suc fact.simps)  lp15@59730  774  apply (auto simp add: field_simps simp del: of_nat_Suc)  lp15@59730  775  done  lp15@59667  776  also have "\ = ?l" unfolding gbinomial_pochhammer  lp15@59667  777  by (simp add: field_simps)  lp15@59667  778  finally show ?thesis ..  lp15@59667  779 qed  lp15@59667  780 lp15@59667  781 lemma gbinomial_mult_1':  lp15@59730  782  fixes a :: "'a :: field_char_0"  lp15@59730  783  shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  lp15@59667  784  by (simp add: mult.commute gbinomial_mult_1)  lp15@59667  785 lp15@59667  786 lemma gbinomial_Suc:  lp15@59730  787  "a gchoose (Suc k) = (setprod (\i. a - of_nat i) {0 .. k}) / (fact (Suc k))"  lp15@59667  788  by (simp add: gbinomial_def)  lp15@59667  789 lp15@59667  790 lemma gbinomial_mult_fact:  lp15@59730  791  fixes a :: "'a::field_char_0"  lp15@59730  792  shows  lp15@59730  793  "fact (Suc k) * (a gchoose (Suc k)) =  lp15@59667  794  (setprod (\i. a - of_nat i) {0 .. k})"  lp15@59730  795  by (simp_all add: gbinomial_Suc field_simps del: fact.simps)  lp15@59667  796 lp15@59667  797 lemma gbinomial_mult_fact':  lp15@59730  798  fixes a :: "'a::field_char_0"  lp15@59730  799  shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\i. a - of_nat i) {0 .. k})"  lp15@59667  800  using gbinomial_mult_fact[of k a]  lp15@59667  801  by (subst mult.commute)  lp15@59667  802 lp15@59667  803 lemma gbinomial_Suc_Suc:  lp15@59730  804  fixes a :: "'a :: field_char_0"  lp15@59730  805  shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"  lp15@59667  806 proof (cases k)  lp15@59667  807  case 0  lp15@59667  808  then show ?thesis by simp  lp15@59667  809 next  lp15@59667  810  case (Suc h)  lp15@59667  811  have eq0: "(\i\{1..k}. (a + 1) - of_nat i) = (\i\{0..h}. a - of_nat i)"  lp15@59667  812  apply (rule setprod.reindex_cong [where l = Suc])  lp15@59667  813  using Suc  lp15@59667  814  apply auto  lp15@59667  815  done  lp15@59730  816  have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =  lp15@59730  817  (a gchoose Suc h) * (fact (Suc (Suc h))) +  lp15@59730  818  (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"  lp15@59730  819  by (simp add: Suc field_simps del: fact.simps)  hoelzl@62378  820  also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +  lp15@59730  821  (\i = 0..Suc h. a - of_nat i)"  lp15@59730  822  by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)  hoelzl@62378  823  also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +  lp15@59730  824  (\i = 0..Suc h. a - of_nat i)"  lp15@59730  825  by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)  hoelzl@62378  826  also have "... = of_nat (Suc (Suc h)) * (\i = 0..h. a - of_nat i) +  lp15@59730  827  (\i = 0..Suc h. a - of_nat i)"  lp15@59730  828  by (metis gbinomial_mult_fact mult.commute)  lp15@59730  829  also have "... = (\i = 0..Suc h. a - of_nat i) +  lp15@59730  830  (of_nat h * (\i = 0..h. a - of_nat i) + 2 * (\i = 0..h. a - of_nat i))"  lp15@59730  831  by (simp add: field_simps)  hoelzl@62378  832  also have "... =  wenzelm@61076  833  ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\i\{0::nat..Suc h}. a - of_nat i)"  lp15@59667  834  unfolding gbinomial_mult_fact'  lp15@59730  835  by (simp add: comm_semiring_class.distrib field_simps Suc)  lp15@59667  836  also have "\ = (\i\{0..h}. a - of_nat i) * (a + 1)"  lp15@59667  837  unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc  lp15@59667  838  by (simp add: field_simps Suc)  lp15@59667  839  also have "\ = (\i\{0..k}. (a + 1) - of_nat i)"  lp15@59667  840  using eq0  lp15@59667  841  by (simp add: Suc setprod_nat_ivl_1_Suc)  lp15@59730  842  also have "\ = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"  lp15@59667  843  unfolding gbinomial_mult_fact ..  lp15@59730  844  finally show ?thesis  hoelzl@62378  845  by (metis fact_nonzero mult_cancel_left)  lp15@59667  846 qed  lp15@59667  847 lp15@59667  848 lemma gbinomial_reduce_nat:  lp15@59730  849  fixes a :: "'a :: field_char_0"  lp15@59730  850  shows "0 < k \ a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"  lp15@59730  851  by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)  lp15@59667  852 lp15@60141  853 lemma gchoose_row_sum_weighted:  lp15@60141  854  fixes r :: "'a::field_char_0"  lp15@60141  855  shows "(\k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))"  lp15@60141  856 proof (induct m)  lp15@60141  857  case 0 show ?case by simp  lp15@60141  858 next  lp15@60141  859  case (Suc m)  lp15@60141  860  from Suc show ?case  lp15@61738  861  by (simp add: field_simps distrib gbinomial_mult_1)  lp15@60141  862 qed  lp15@59667  863 lp15@59667  864 lemma binomial_symmetric:  lp15@59667  865  assumes kn: "k \ n"  lp15@59667  866  shows "n choose k = n choose (n - k)"  lp15@59667  867 proof-  lp15@59667  868  from kn have kn': "n - k \ n" by arith  lp15@59667  869  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']  lp15@59667  870  have "fact k * fact (n - k) * (n choose k) =  lp15@59667  871  fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp  lp15@59667  872  then show ?thesis using kn by simp  lp15@59667  873 qed  lp15@59667  874 eberlm@61531  875 lemma choose_rising_sum:  eberlm@61531  876  "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"  eberlm@61531  877  "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose m)"  eberlm@61531  878 proof -  eberlm@61531  879  show "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all  eberlm@61531  880  also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all  eberlm@61531  881  finally show "(\j\m. ((n + j) choose n)) = ((n + m + 1) choose m)" .  eberlm@61531  882 qed  eberlm@61531  883 eberlm@61531  884 lemma choose_linear_sum:  eberlm@61531  885  "(\i\n. i * (n choose i)) = n * 2 ^ (n - 1)"  eberlm@61531  886 proof (cases n)  eberlm@61531  887  case (Suc m)  eberlm@61531  888  have "(\i\n. i * (n choose i)) = (\i\Suc m. i * (Suc m choose i))" by (simp add: Suc)  eberlm@61531  889  also have "... = Suc m * 2 ^ m"  hoelzl@62378  890  by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric])  eberlm@61531  891  (simp add: choose_row_sum')  eberlm@61531  892  finally show ?thesis using Suc by simp  eberlm@61531  893 qed simp_all  eberlm@61531  894 eberlm@61531  895 lemma choose_alternating_linear_sum:  eberlm@61531  896  assumes "n \ 1"  eberlm@61531  897  shows "(\i\n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0"  eberlm@61531  898 proof (cases n)  eberlm@61531  899  case (Suc m)  eberlm@61531  900  with assms have "m > 0" by simp  hoelzl@62378  901  have "(\i\n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =  eberlm@61531  902  (\i\Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)  eberlm@61531  903  also have "... = (\i\m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"  eberlm@61531  904  by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp  eberlm@61531  905  also have "... = -of_nat (Suc m) * (\i\m. (-1) ^ i * of_nat ((m choose i)))"  eberlm@61531  906  by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)  eberlm@61531  907  (simp add: algebra_simps of_nat_mult)  eberlm@61531  908  also have "(\i\m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"  wenzelm@61799  909  using choose_alternating_sum[OF \m > 0\] by simp  eberlm@61531  910  finally show ?thesis by simp  eberlm@61531  911 qed simp  eberlm@61531  912 eberlm@61531  913 lemma vandermonde:  eberlm@61531  914  "(\k\r. (m choose k) * (n choose (r - k))) = (m + n) choose r"  eberlm@61531  915 proof (induction n arbitrary: r)  eberlm@61531  916  case 0  eberlm@61531  917  have "(\k\r. (m choose k) * (0 choose (r - k))) = (\k\r. if k = r then (m choose k) else 0)"  eberlm@61531  918  by (intro setsum.cong) simp_all  eberlm@61531  919  also have "... = m choose r" by (simp add: setsum.delta)  eberlm@61531  920  finally show ?case by simp  eberlm@61531  921 next  eberlm@61531  922  case (Suc n r)  eberlm@61531  923  show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le)  eberlm@61531  924 qed  eberlm@61531  925 eberlm@61531  926 lemma choose_square_sum:  eberlm@61531  927  "(\k\n. (n choose k)^2) = ((2*n) choose n)"  eberlm@61531  928  using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric])  eberlm@61531  929 eberlm@61531  930 lemma pochhammer_binomial_sum:  eberlm@61531  931  fixes a b :: "'a :: comm_ring_1"  eberlm@61531  932  shows "pochhammer (a + b) n = (\k\n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))"  eberlm@61531  933 proof (induction n arbitrary: a b)  eberlm@61531  934  case (Suc n a b)  eberlm@61531  935  have "(\k\Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) =  eberlm@61531  936  (\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +  eberlm@61531  937  ((\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +  eberlm@61531  938  pochhammer b (Suc n))"  eberlm@61531  939  by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib)  eberlm@61531  940  also have "(\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =  eberlm@61531  941  a * pochhammer ((a + 1) + b) n"  eberlm@61531  942  by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)  hoelzl@62378  943  also have "(\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) =  eberlm@61531  944  (\i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"  eberlm@61531  945  by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)  eberlm@61531  946  also have "... = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"  eberlm@61531  947  using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0)  eberlm@61531  948  also have "... = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))"  eberlm@61531  949  by (intro setsum.cong) (simp_all add: Suc_diff_le)  eberlm@61531  950  also have "... = b * pochhammer (a + (b + 1)) n"  eberlm@61531  951  by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec)  eberlm@61531  952  also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n =  eberlm@61531  953  pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps)  eberlm@61531  954  finally show ?case ..  eberlm@61531  955 qed simp_all  eberlm@61531  956 eberlm@61531  957 wenzelm@60758  958 text\Contributed by Manuel Eberl, generalised by LCP.  wenzelm@60758  959  Alternative definition of the binomial coefficient as @{term "\i  lp15@59667  960 lemma gbinomial_altdef_of_nat:  lp15@59667  961  fixes k :: nat  haftmann@59867  962  and x :: "'a :: {field_char_0,field}"  lp15@59667  963  shows "x gchoose k = (\ii = (\i x"  lp15@59667  978  shows "(x / of_nat k :: 'a) ^ k \ x gchoose k"  lp15@59667  979 proof -  lp15@59667  980  have x: "0 \ x"  lp15@59667  981  using assms of_nat_0_le_iff order_trans by blast  lp15@59667  982  have "(x / of_nat k :: 'a) ^ k = (\i \ x gchoose k"  lp15@59667  985  unfolding gbinomial_altdef_of_nat  lp15@59667  986  proof (safe intro!: setprod_mono)  lp15@59667  987  fix i :: nat  lp15@59667  988  assume ik: "i < k"  lp15@59667  989  from assms have "x * of_nat i \ of_nat (i * k)"  lp15@59667  990  by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)  lp15@59667  991  then have "x * of_nat k - x * of_nat i \ x * of_nat k - of_nat (i * k)" by arith  lp15@59667  992  then have "x * of_nat (k - i) \ (x - of_nat i) * of_nat k"  lp15@59667  993  using ik  lp15@59667  994  by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)  lp15@59667  995  then have "x * of_nat (k - i) \ (x - of_nat i) * (of_nat k :: 'a)"  lp15@59667  996  unfolding of_nat_mult[symmetric] of_nat_le_iff .  lp15@59667  997  with assms show "x / of_nat k \ (x - of_nat i) / (of_nat (k - i) :: 'a)"  wenzelm@60758  998  using \i < k\ by (simp add: field_simps)  lp15@59667  999  qed (simp add: x zero_le_divide_iff)  lp15@59667  1000  finally show ?thesis .  lp15@59667  1001 qed  lp15@59667  1002 eberlm@61531  1003 lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"  eberlm@61531  1004  by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)  eberlm@61531  1005 eberlm@61531  1006 lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"  eberlm@61531  1007  by (subst gbinomial_negated_upper) (simp add: add_ac)  eberlm@61531  1008 eberlm@61531  1009 lemma Suc_times_gbinomial:  eberlm@61531  1010  "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"  eberlm@61531  1011 proof (cases b)  eberlm@61531  1012  case (Suc b)  hoelzl@62378  1013  hence "((a + 1) gchoose (Suc (Suc b))) =  eberlm@61531  1014  (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"  eberlm@61531  1015  by (simp add: field_simps gbinomial_def)  eberlm@61531  1016  also have "(\i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)"  eberlm@61531  1017  by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)  eberlm@61531  1018  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"  eberlm@61531  1019  by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)  eberlm@61531  1020  finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)  eberlm@61531  1021 qed simp  eberlm@61531  1022 eberlm@61531  1023 lemma gbinomial_factors:  eberlm@61531  1024  "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"  eberlm@61531  1025 proof (cases b)  eberlm@61531  1026  case (Suc b)  hoelzl@62378  1027  hence "((a + 1) gchoose (Suc (Suc b))) =  eberlm@61531  1028  (\i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"  eberlm@61531  1029  by (simp add: field_simps gbinomial_def)  eberlm@61531  1030  also have "(\i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\i = 0..b. a - of_nat i)"  eberlm@61531  1031  by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)  eberlm@61531  1032  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"  eberlm@61531  1033  by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)  eberlm@61531  1034  finally show ?thesis by (simp add: Suc)  eberlm@61531  1035 qed simp  eberlm@61531  1036 eberlm@61531  1037 lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"  eberlm@61531  1038  using gbinomial_mult_1[of r k]  eberlm@61531  1039  by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps)  eberlm@61531  1040 eberlm@61531  1041 lemma gbinomial_of_nat_symmetric: "k \ n \ (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"  eberlm@61531  1042  using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])  eberlm@61531  1043 eberlm@61531  1044 eberlm@61531  1045 text \The absorption identity (equation 5.5 \cite[p.~157]{GKP}):$ eberlm@61531  1046 {r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.  eberlm@61531  1047 $\  hoelzl@62378  1048 lemma gbinomial_absorption':  eberlm@61531  1049  "k > 0 \ (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"  hoelzl@62378  1050  using gbinomial_rec[of "r - 1" "k - 1"]  eberlm@61531  1051  by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)  eberlm@61531  1052 eberlm@61531  1053 text \The absorption identity is written in the following form to avoid  eberlm@61531  1054 division by $k$ (the lower index) and therefore remove the $k \neq 0$  eberlm@61531  1055 restriction\cite[p.~157]{GKP}:$ eberlm@61531  1056 k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.  eberlm@61531  1057 $\  eberlm@61531  1058 lemma gbinomial_absorption:  eberlm@61531  1059  "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"  eberlm@61531  1060  using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)  eberlm@61531  1061 eberlm@61531  1062 text \The absorption identity for natural number binomial coefficients:\  eberlm@61531  1063 lemma binomial_absorption:  eberlm@61531  1064  "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"  eberlm@61531  1065  by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)  eberlm@61531  1066 eberlm@61531  1067 text \The absorption companion identity for natural number coefficients,  eberlm@61531  1068 following the proof by GKP \cite[p.~157]{GKP}:\  eberlm@61531  1069 lemma binomial_absorb_comp:  eberlm@61531  1070  "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs")  eberlm@61531  1071 proof (cases "n \ k")  eberlm@61531  1072  case False  eberlm@61531  1073  then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"  eberlm@61531  1074  using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]  eberlm@61531  1075  by simp  eberlm@61531  1076  also from False have "Suc ((n - 1) - k) = n - k" by simp  eberlm@61531  1077  also from False have "n choose \ = n choose k" by (intro binomial_symmetric [symmetric]) simp_all  eberlm@61531  1078  finally show ?thesis ..  eberlm@61531  1079 qed auto  eberlm@61531  1080 eberlm@61531  1081 text \The generalised absorption companion identity:\  eberlm@61531  1082 lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"  eberlm@61531  1083  using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)  eberlm@61531  1084 eberlm@61531  1085 lemma gbinomial_addition_formula:  eberlm@61531  1086  "r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"  eberlm@61531  1087  using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)  eberlm@61531  1088 eberlm@61531  1089 lemma binomial_addition_formula:  eberlm@61531  1090  "0 < n \ n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"  eberlm@61531  1091  by (subst choose_reduce_nat) simp_all  eberlm@61531  1092 eberlm@61531  1093 eberlm@61531  1094 text \  eberlm@61531  1095  Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful  eberlm@61531  1096  summation formula, operating on both indices:$ eberlm@61531  1097  \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},  eberlm@61531  1098  \quad \textnormal{integer } n.  hoelzl@62378  1099 $  eberlm@61531  1100 \  eberlm@61531  1101 lemma gbinomial_parallel_sum:  eberlm@61531  1102 "(\k\n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"  eberlm@61531  1103 proof (induction n)  eberlm@61531  1104  case (Suc m)  eberlm@61531  1105  thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)  eberlm@61531  1106 qed auto  eberlm@61531  1107 eberlm@61531  1108 subsection \Summation on the upper index\  eberlm@61531  1109 text \  eberlm@61531  1110  Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},  hoelzl@62378  1111  aptly named \emph{summation on the upper index}:$\sum_{0 \leq k \leq n} {k \choose m} =  eberlm@61531  1112  {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.$  eberlm@61531  1113 \  eberlm@61531  1114 lemma gbinomial_sum_up_index:  eberlm@61531  1115  "(\k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)"  eberlm@61531  1116 proof (induction n)  eberlm@61531  1117  case 0  eberlm@61531  1118  show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto  eberlm@61531  1119 next  eberlm@61531  1120  case (Suc n)  eberlm@61531  1121  thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)  eberlm@61531  1122 qed  eberlm@61531  1123 hoelzl@62378  1124 lemma gbinomial_index_swap:  eberlm@61531  1125  "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"  eberlm@61531  1126  (is "?lhs = ?rhs")  eberlm@61531  1127 proof -  eberlm@61531  1128  have "?lhs = (of_nat (m + n) gchoose m)"  eberlm@61531  1129  by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])  eberlm@61531  1130  also have "\ = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all  eberlm@61531  1131  also have "\ = ?rhs" by (subst gbinomial_negated_upper) simp  eberlm@61531  1132  finally show ?thesis .  eberlm@61531  1133 qed  eberlm@61531  1134 hoelzl@62378  1135 lemma gbinomial_sum_lower_neg:  eberlm@61531  1136  "(\k\m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")  eberlm@61531  1137 proof -  eberlm@61531  1138  have "?lhs = (\k\m. -(r + 1) + of_nat k gchoose k)"  eberlm@61531  1139  by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)  eberlm@61531  1140  also have "\ = -r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp  eberlm@61531  1141  also have "\ = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)  eberlm@61531  1142  finally show ?thesis .  eberlm@61531  1143 qed  eberlm@61531  1144 eberlm@61531  1145 lemma gbinomial_partial_row_sum:  eberlm@61531  1146 "(\k\m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"  eberlm@61531  1147 proof (induction m)  eberlm@61531  1148  case (Suc mm)  hoelzl@62378  1149  hence "(\k\Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =  lp15@61738  1150  (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps)  eberlm@61531  1151  also have "\ = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)  eberlm@61531  1152  also have "\ = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"  eberlm@61531  1153  by (subst gbinomial_absorption [symmetric]) simp  eberlm@61531  1154  finally show ?case .  eberlm@61531  1155 qed simp_all  eberlm@61531  1156 eberlm@61531  1157 lemma setsum_bounds_lt_plus1: "(\kk=1..mm. f k)"  eberlm@61531  1158  by (induction mm) simp_all  eberlm@61531  1159 eberlm@61531  1160 lemma gbinomial_partial_sum_poly:  eberlm@61531  1161  "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =  eberlm@61531  1162  (\k\m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" (is "?lhs m = ?rhs m")  eberlm@61531  1163 proof (induction m)  eberlm@61531  1164  case (Suc mm)  eberlm@61531  1165  def G \ "\i k. (of_nat i + r gchoose k) * x^k * y^(i-k)" and S \ ?lhs  eberlm@61531  1166  have SG_def: "S = (\i. (\k\i. (G i k)))" unfolding S_def G_def ..  eberlm@61531  1167 eberlm@61531  1168  have "S (Suc mm) = G (Suc mm) 0 + (\k=Suc 0..Suc mm. G (Suc mm) k)"  eberlm@61531  1169  using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric])  eberlm@61531  1170  also have "(\k=Suc 0..Suc mm. G (Suc mm) k) = (\k=0..mm. G (Suc mm) (Suc k))"  eberlm@61531  1171  by (subst setsum_shift_bounds_cl_Suc_ivl) simp  eberlm@61531  1172  also have "\ = (\k=0..mm. ((of_nat mm + r gchoose (Suc k))  eberlm@61531  1173  + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"  eberlm@61531  1174  unfolding G_def by (subst gbinomial_addition_formula) simp  eberlm@61531  1175  also have "\ = (\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))  eberlm@61531  1176  + (\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"  eberlm@61531  1177  by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)  hoelzl@62378  1178  also have "(\k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =  eberlm@61531  1179  (\k = (\kk=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"  eberlm@61531  1185  proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify)  eberlm@61531  1186  fix k assume "k < mm"  eberlm@61531  1187  hence "mm - k = mm - Suc k + 1" by linarith  eberlm@61531  1188  thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =  eberlm@61531  1189  (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)  eberlm@61531  1190  qed  hoelzl@62378  1191  also have "\ + ?B = y * (\k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"  eberlm@61531  1192  unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)  eberlm@61531  1193  also have "(\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"  eberlm@61531  1194  unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)  eberlm@61531  1195  also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)  hoelzl@62378  1196  finally have "S (Suc mm) = y * ((G mm 0) + (\k=1..mm. (G mm k)))  eberlm@61531  1197  + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"  eberlm@61531  1198  by (simp add: ring_distribs)  hoelzl@62378  1199  also have "(G mm 0) + (\k=1..mm. (G mm k)) = S mm"  eberlm@61531  1200  by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)  hoelzl@62378  1201  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"  eberlm@61531  1202  by (simp add: algebra_simps)  eberlm@61531  1203  also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"  eberlm@61531  1204  by (subst gbinomial_negated_upper) simp  eberlm@61531  1205  also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =  eberlm@61531  1206  (-r gchoose (Suc mm)) * (-x) ^ Suc mm" by (simp add: power_minus[of x])  eberlm@61531  1207  also have "(x + y) * S mm + \ = (x + y) * ?rhs mm + (-r gchoose (Suc mm)) * (-x)^Suc mm"  eberlm@61531  1208  unfolding S_def by (subst Suc.IH) simp  eberlm@61531  1209  also have "(x + y) * ?rhs mm = (\n\mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"  eberlm@61531  1210  by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)  hoelzl@62378  1211  also have "\ + (-r gchoose (Suc mm)) * (-x)^Suc mm =  eberlm@61531  1212  (\n\Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp  eberlm@61531  1213  finally show ?case unfolding S_def .  eberlm@61531  1214 qed simp_all  eberlm@61531  1215 eberlm@61531  1216 lemma gbinomial_partial_sum_poly_xpos:  hoelzl@62378  1217  "(\k\m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =  eberlm@61531  1218  (\k\m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"  eberlm@61531  1219  apply (subst gbinomial_partial_sum_poly)  eberlm@61531  1220  apply (subst gbinomial_negated_upper)  eberlm@61531  1221  apply (intro setsum.cong, rule refl)  eberlm@61531  1222  apply (simp add: power_mult_distrib [symmetric])  eberlm@61531  1223  done  eberlm@61531  1224 hoelzl@62378  1225 lemma setsum_nat_symmetry:  eberlm@61531  1226  "(\k = 0..(m::nat). f k) = (\k = 0..m. f (m - k))"  eberlm@61531  1227  by (rule setsum.reindex_bij_witness[where i="\i. m - i" and j="\i. m - i"]) auto  eberlm@61531  1228 eberlm@61531  1229 lemma binomial_r_part_sum: "(\k\m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"  eberlm@61531  1230 proof -  eberlm@61531  1231  have "2 * 2^(2*m) = (\k = 0..(2 * m + 1). (2 * m + 1 choose k))"  eberlm@61531  1232  using choose_row_sum[where n="2 * m + 1"] by simp  eberlm@61531  1233  also have "(\k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\k = 0..m. (2 * m + 1 choose k))  eberlm@61531  1234  + (\k = m+1..2*m+1. (2 * m + 1 choose k))"  eberlm@61531  1235  using setsum_ub_add_nat[of 0 m "\k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2)  eberlm@61531  1236  also have "(\k = m+1..2*m+1. (2 * m + 1 choose k)) =  eberlm@61531  1237  (\k = 0..m. (2 * m + 1 choose (k + (m + 1))))"  eberlm@61531  1238  by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)  eberlm@61531  1239  also have "\ = (\k = 0..m. (2 * m + 1 choose (m - k)))"  eberlm@61531  1240  by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all  eberlm@61531  1241  also have "\ = (\k = 0..m. (2 * m + 1 choose k))"  eberlm@61531  1242  by (subst (2) setsum_nat_symmetry) (rule refl)  eberlm@61531  1243  also have "\ + \ = 2 * \" by simp  eberlm@61531  1244  finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)  eberlm@61531  1245 qed  eberlm@61531  1246 eberlm@61531  1247 lemma gbinomial_r_part_sum:  eberlm@61531  1248  "(\k\m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")  eberlm@61531  1249 proof -  hoelzl@62378  1250  have "?lhs = of_nat (\k\m. (2 * m + 1) choose k)"  eberlm@61531  1251  by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)  eberlm@61531  1252  also have "\ = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)  eberlm@61531  1253  finally show ?thesis by (simp add: of_nat_power)  eberlm@61531  1254 qed  eberlm@61531  1255 eberlm@61531  1256 lemma gbinomial_sum_nat_pow2:  eberlm@61531  1257  "(\k\m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")  eberlm@61531  1258 proof -  eberlm@61531  1259  have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" by (induction m) simp_all  eberlm@61531  1260  also have "\ = (\k\m. (2 * (of_nat m) + 1 gchoose k))" using gbinomial_r_part_sum ..  eberlm@61531  1261  also have "\ = (\k\m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"  eberlm@61531  1262  using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]  eberlm@61531  1263  by (simp add: add_ac)  eberlm@61531  1264  also have "\ = 2 ^ m * (\k\m. (of_nat (m + k) gchoose k) / 2 ^ k)"  eberlm@61531  1265  by (subst setsum_right_distrib) (simp add: algebra_simps power_diff)  eberlm@61531  1266  finally show ?thesis by (subst (asm) mult_left_cancel) simp_all  eberlm@61531  1267 qed  eberlm@61531  1268 eberlm@61531  1269 lemma gbinomial_trinomial_revision:  eberlm@61531  1270  assumes "k \ m"  eberlm@61531  1271  shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"  eberlm@61531  1272 proof -  hoelzl@62378  1273  have "(r gchoose m) * (of_nat m gchoose k) =  eberlm@61531  1274  (r gchoose m) * fact m / (fact k * fact (m - k))"  eberlm@61531  1275  using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)  eberlm@61531  1276  also have "\ = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms  eberlm@61531  1277  by (simp add: gbinomial_pochhammer power_diff pochhammer_product)  eberlm@61531  1278  finally show ?thesis .  eberlm@61531  1279 qed  eberlm@61531  1280 eberlm@61531  1281 wenzelm@60758  1282 text\Versions of the theorems above for the natural-number version of "choose"\  lp15@59667  1283 lemma binomial_altdef_of_nat:  lp15@59667  1284  fixes n k :: nat  wenzelm@61799  1285  and x :: "'a :: {field_char_0,field}" \\the point is to constrain @{typ 'a}\  lp15@59667  1286  assumes "k \ n"  lp15@59667  1287  shows "of_nat (n choose k) = (\i n"  lp15@59667  1295  shows "(of_nat n / of_nat k :: 'a) ^ k \ of_nat (n choose k)"  lp15@59667  1296 by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)  lp15@59667  1297 lp15@59667  1298 lemma binomial_le_pow:  lp15@59667  1299  assumes "r \ n"  lp15@59667  1300  shows "n choose r \ n ^ r"  lp15@59667  1301 proof -  lp15@59667  1302  have "n choose r \ fact n div fact (n - r)"  wenzelm@60758  1303  using \r \ n\ by (subst binomial_fact_lemma[symmetric]) auto  lp15@59667  1304  with fact_div_fact_le_pow [OF assms] show ?thesis by auto  lp15@59667  1305 qed  lp15@59667  1306 lp15@59667  1307 lemma binomial_altdef_nat: "(k::nat) \ n \  lp15@59667  1308  n choose k = fact n div (fact k * fact (n - k))"  lp15@59667  1309  by (subst binomial_fact_lemma [symmetric]) auto  lp15@59667  1310 lp15@59730  1311 lemma choose_dvd: "k \ n \ fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})"  lp15@59730  1312  unfolding dvd_def  lp15@59730  1313  apply (rule exI [where x="of_nat (n choose k)"])  lp15@59730  1314  using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]  lp15@59730  1315  apply (auto simp: of_nat_mult)  lp15@59667  1316  done  lp15@59667  1317 hoelzl@62378  1318 lemma fact_fact_dvd_fact:  lp15@59730  1319  "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"  lp15@59730  1320 by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)  lp15@59667  1321 lp15@59667  1322 lemma choose_mult_lemma:  lp15@59667  1323  "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"  lp15@59667  1324 proof -  lp15@59667  1325  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =  lp15@59667  1326  fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"  lp15@59667  1327  by (simp add: assms binomial_altdef_nat)  lp15@59667  1328  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"  lp15@59667  1329  apply (subst div_mult_div_if_dvd)  lp15@59730  1330  apply (auto simp: algebra_simps fact_fact_dvd_fact)  lp15@59667  1331  apply (metis add.assoc add.commute fact_fact_dvd_fact)  lp15@59667  1332  done  lp15@59667  1333  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"  lp15@59667  1334  apply (subst div_mult_div_if_dvd [symmetric])  lp15@59730  1335  apply (auto simp add: algebra_simps)  haftmann@62344  1336  apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)  lp15@59667  1337  done  lp15@59667  1338  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"  lp15@59667  1339  apply (subst div_mult_div_if_dvd)  lp15@59730  1340  apply (auto simp: fact_fact_dvd_fact algebra_simps)  lp15@59667  1341  done  lp15@59667  1342  finally show ?thesis  lp15@59667  1343  by (simp add: binomial_altdef_nat mult.commute)  lp15@59667  1344 qed  lp15@59667  1345 wenzelm@60758  1346 text\The "Subset of a Subset" identity\  lp15@59667  1347 lemma choose_mult:  lp15@59667  1348  assumes "k\m" "m\n"  lp15@59667  1349  shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"  lp15@59667  1350 using assms choose_mult_lemma [of "m-k" "n-m" k]  lp15@59667  1351 by simp  lp15@59667  1352 lp15@59667  1353 wenzelm@60758  1354 subsection \Binomial coefficients\  lp15@59667  1355 lp15@59667  1356 lemma choose_one: "(n::nat) choose 1 = n"  lp15@59667  1357  by simp  lp15@59667  1358 lp15@59667  1359 (*FIXME: messy and apparently unused*)  lp15@59667  1360 lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \  lp15@59667  1361  (ALL n. P (Suc n) 0) \ (ALL n. (ALL k < n. P n k \ P n (Suc k) \  lp15@59667  1362  P (Suc n) (Suc k))) \ (ALL k <= n. P n k)"  lp15@59667  1363  apply (induct n)  lp15@59667  1364  apply auto  lp15@59667  1365  apply (case_tac "k = 0")  lp15@59667  1366  apply auto  lp15@59667  1367  apply (case_tac "k = Suc n")  lp15@59667  1368  apply auto  lp15@59730  1369  apply (metis Suc_le_eq fact.cases le_Suc_eq le_eq_less_or_eq)  lp15@59667  1370  done  lp15@59667  1371 lp15@59667  1372 lemma card_UNION:  lp15@59667  1373  assumes "finite A" and "\k \ A. finite k"  lp15@59667  1374  shows "card (\A) = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * int (card (\I)))"  lp15@59667  1375  (is "?lhs = ?rhs")  lp15@59667  1376 proof -  lp15@59667  1377  have "?rhs = nat (\I | I \ A \ I \ {}. (- 1) ^ (card I + 1) * (\_\\I. 1))" by simp  lp15@59667  1378  also have "\ = nat (\I | I \ A \ I \ {}. (\_\\I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")  lp15@59667  1379  by(subst setsum_right_distrib) simp  lp15@59667  1380  also have "?rhs = (\(I, _)\Sigma {I. I \ A \ I \ {}} Inter. (- 1) ^ (card I + 1))"  lp15@59667  1381  using assms by(subst setsum.Sigma)(auto)  lp15@59667  1382  also have "\ = (\(x, I)\(SIGMA x:UNIV. {I. I \ A \ I \ {} \ x \ \I}). (- 1) ^ (card I + 1))"  lp15@59667  1383  by (rule setsum.reindex_cong [where l = "\(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)  lp15@59667  1384  also have "\ = (\(x, I)\(SIGMA x:\A. {I. I \ A \ I \ {} \ x \ \I}). (- 1) ^ (card I + 1))"  lp15@59667  1385  using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\A"])  lp15@59667  1386  also have "\ = (\x\\A. (\I|I \ A \ I \ {} \ x \ \I. (- 1) ^ (card I + 1)))"  lp15@59667  1387  using assms by(subst setsum.Sigma) auto  lp15@59667  1388  also have "\ = (\_\\A. 1)" (is "setsum ?lhs _ = _")  lp15@59667  1389  proof(rule setsum.cong[OF refl])  lp15@59667  1390  fix x  lp15@59667  1391  assume x: "x \ \A"  lp15@59667  1392  def K \ "{X \ A. x \ X}"  wenzelm@60758  1393  with \finite A\ have K: "finite K" by auto  lp15@59667  1394  let ?I = "\i. {I. I \ A \ card I = i \ x \ \I}"  lp15@59667  1395  have "inj_on snd (SIGMA i:{1..card A}. ?I i)"  lp15@59667  1396  using assms by(auto intro!: inj_onI)  lp15@59667  1397  moreover have [symmetric]: "snd  (SIGMA i:{1..card A}. ?I i) = {I. I \ A \ I \ {} \ x \ \I}"  lp15@59667  1398  using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]  lp15@59667  1399  simp add: card_gt_0_iff[folded Suc_le_eq]  lp15@59667  1400  dest: finite_subset intro: card_mono)  lp15@59667  1401  ultimately have "?lhs x = (\(i, I)\(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"  lp15@59667  1402  by (rule setsum.reindex_cong [where l = snd]) fastforce  lp15@59667  1403  also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. (- 1) ^ (i + 1)))"  lp15@59667  1404  using assms by(subst setsum.Sigma) auto  lp15@59667  1405  also have "\ = (\i=1..card A. (- 1) ^ (i + 1) * (\I|I \ A \ card I = i \ x \ \I. 1))"  lp15@59667  1406  by(subst setsum_right_distrib) simp  lp15@59667  1407  also have "\ = (\i=1..card K. (- 1) ^ (i + 1) * (\I|I \ K \ card I = i. 1))" (is "_ = ?rhs")  lp15@59667  1408  proof(rule setsum.mono_neutral_cong_right[rule_format])  wenzelm@60758  1409  show "{1..card K} \ {1..card A}" using \finite A\  lp15@59667  1410  by(auto simp add: K_def intro: card_mono)  lp15@59667  1411  next  lp15@59667  1412  fix i  lp15@59667  1413  assume "i \ {1..card A} - {1..card K}"  lp15@59667  1414  hence i: "i \ card A" "card K < i" by auto  lp15@59667  1415  have "{I. I \ A \ card I = i \ x \ \I} = {I. I \ K \ card I = i}"  lp15@59667  1416  by(auto simp add: K_def)  wenzelm@60758  1417  also have "\ = {}" using \finite A\ i  lp15@59667  1418  by(auto simp add: K_def dest: card_mono[rotated 1])  lp15@59667  1419  finally show "(- 1) ^ (i + 1) * (\I | I \ A \ card I = i \ x \ \I. 1 :: int) = 0"  lp15@59667  1420  by(simp only:) simp  lp15@59667  1421  next  lp15@59667  1422  fix i  lp15@59667  1423  have "(\I | I \ A \ card I = i \ x \ \I. 1) = (\I | I \ K \ card I = i. 1 :: int)"  lp15@59667  1424  (is "?lhs = ?rhs")  lp15@59667  1425  by(rule setsum.cong)(auto simp add: K_def)  lp15@59667  1426  thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp  lp15@59667  1427  qed simp  lp15@59667  1428  also have "{I. I \ K \ card I = 0} = {{}}" using assms  lp15@59667  1429  by(auto simp add: card_eq_0_iff K_def dest: finite_subset)  lp15@59667  1430  hence "?rhs = (\i = 0..card K. (- 1) ^ (i + 1) * (\I | I \ K \ card I = i. 1 :: int)) + 1"  lp15@59667  1431  by(subst (2) setsum_head_Suc)(simp_all )  lp15@59667  1432  also have "\ = (\i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"  lp15@59667  1433  using K by(subst n_subsets[symmetric]) simp_all  lp15@59667  1434  also have "\ = - (\i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"  lp15@59667  1435  by(subst setsum_right_distrib[symmetric]) simp  lp15@59667  1436  also have "\ = - ((-1 + 1) ^ card K) + 1"  lp15@59667  1437  by(subst binomial_ring)(simp add: ac_simps)  lp15@59667  1438  also have "\ = 1" using x K by(auto simp add: K_def card_gt_0_iff)  lp15@59667  1439  finally show "?lhs x = 1" .  lp15@59667  1440  qed  lp15@59667  1441  also have "nat \ = card (\A)" by simp  lp15@59667  1442  finally show ?thesis ..  lp15@59667  1443 qed  lp15@59667  1444 wenzelm@61799  1445 text\The number of nat lists of length \m\ summing to \N\ is  wenzelm@60758  1446 @{term "(N + m - 1) choose N"}:\  lp15@59667  1447 lp15@59667  1448 lemma card_length_listsum_rec:  lp15@59667  1449  assumes "m\1"  lp15@59667  1450  shows "card {l::nat list. length l = m \ listsum l = N} =  lp15@59667  1451  (card {l. length l = (m - 1) \ listsum l = N} +  lp15@59667  1452  card {l. length l = m \ listsum l + 1 = N})"  lp15@59667  1453  (is "card ?C = (card ?A + card ?B)")  lp15@59667  1454 proof -  lp15@59667  1455  let ?A'="{l. length l = m \ listsum l = N \ hd l = 0}"  lp15@59667  1456  let ?B'="{l. length l = m \ listsum l = N \ hd l \ 0}"  lp15@59667  1457  let ?f ="\ l. 0#l"  lp15@59667  1458  let ?g ="\ l. (hd l + 1) # tl l"  lp15@59667  1459  have 1: "\xs x. xs \ [] \ x = hd xs \ x # tl xs = xs" by simp  lp15@59667  1460  have 2: "\xs. (xs::nat list) \ [] \ listsum(tl xs) = listsum xs - hd xs"  lp15@59667  1461  by(auto simp add: neq_Nil_conv)  lp15@59667  1462  have f: "bij_betw ?f ?A ?A'"  lp15@59667  1463  apply(rule bij_betw_byWitness[where f' = tl])  lp15@59667  1464  using assms  lp15@59667  1465  by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)  lp15@59667  1466  have 3: "\xs:: nat list. xs \ [] \ hd xs + (listsum xs - hd xs) = listsum xs"  lp15@59667  1467  by (metis 1 listsum_simps(2) 2)  lp15@59667  1468  have g: "bij_betw ?g ?B ?B'"  lp15@59667  1469  apply(rule bij_betw_byWitness[where f' = "\ l. (hd l - 1) # tl l"])  lp15@59667  1470  using assms  lp15@59667  1471  by (auto simp: 2 length_0_conv[symmetric] intro!: 3  lp15@59667  1472  simp del: length_greater_0_conv length_0_conv)  lp15@59667  1473  { fix M N :: nat have "finite {xs. size xs = M \ set xs \ {0.. ?B'" by auto  lp15@59667  1483  have disj: "?A' \ ?B' = {}" by auto  lp15@59667  1484  have "card ?C = card(?A' \ ?B')" using uni by simp  lp15@59667  1485  also have "\ = card ?A + card ?B"  lp15@59667  1486  using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]  lp15@59667  1487  bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B  lp15@59667  1488  by presburger  lp15@59667  1489  finally show ?thesis .  lp15@59667  1490 qed  lp15@59667  1491 wenzelm@61799  1492 lemma card_length_listsum: \"By Holden Lee, tidied by Tobias Nipkow"  lp15@59667  1493  "card {l::nat list. size l = m \ listsum l = N} = (N + m - 1) choose N"  lp15@59667  1494 proof (cases m)  lp15@59667  1495  case 0 then show ?thesis  lp15@59667  1496  by (cases N) (auto simp: cong: conj_cong)  lp15@59667  1497 next  lp15@59667  1498  case (Suc m')  lp15@59667  1499  have m: "m\1" by (simp add: Suc)  lp15@59667  1500  then show ?thesis  lp15@59667  1501  proof (induct "N + m - 1" arbitrary: N m)  wenzelm@61799  1502  case 0 \ "In the base case, the only solution is [0]."  lp15@59667  1503  have [simp]: "{l::nat list. length l = Suc 0 \ (\n\set l. n = 0)} = {[0]}"  lp15@59667  1504  by (auto simp: length_Suc_conv)  lp15@59667  1505  have "m=1 \ N=0" using 0 by linarith  lp15@59667  1506  then show ?case by simp  lp15@59667  1507  next  lp15@59667  1508  case (Suc k)  lp15@59667  1509 lp15@59667  1510  have c1: "card {l::nat list. size l = (m - 1) \ listsum l = N} =  lp15@59667  1511  (N + (m - 1) - 1) choose N"  lp15@59667  1512  proof cases  lp15@59667  1513  assume "m = 1"  lp15@59667  1514  with Suc.hyps have "N\1" by auto  wenzelm@60758  1515  with \m = 1\ show ?thesis by (simp add: binomial_eq_0)  lp15@59667  1516  next  lp15@59667  1517  assume "m \ 1" thus ?thesis using Suc by fastforce  lp15@59667  1518  qed  lp15@59667  1519 lp15@59667  1520  from Suc have c2: "card {l::nat list. size l = m \ listsum l + 1 = N} =  lp15@59667  1521  (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"  lp15@59667  1522  proof -  lp15@59667  1523  have aux: "\m n. n > 0 \ Suc m = n \ m = n - 1" by arith  lp15@59667  1524  from Suc have "N>0 \  lp15@59667  1525  card {l::nat list. size l = m \ listsum l + 1 = N} =  lp15@59667  1526  ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)  lp15@59667  1527  thus ?thesis by auto  lp15@59667  1528  qed  lp15@59667  1529 lp15@59667  1530  from Suc.prems have "(card {l::nat list. size l = (m - 1) \ listsum l = N} +  lp15@59667  1531  card {l::nat list. size l = m \ listsum l + 1 = N}) = (N + m - 1) choose N"  lp15@59667  1532  by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)  lp15@59667  1533  thus ?case using card_length_listsum_rec[OF Suc.prems] by auto  lp15@59667  1534  qed  lp15@59667  1535 qed  lp15@59667  1536 hoelzl@60604  1537 wenzelm@61799  1538 lemma Suc_times_binomial_add: \ \by Lukas Bulwahn\  hoelzl@60604  1539  "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"  hoelzl@60604  1540 proof -  hoelzl@60604  1541  have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b  hoelzl@60604  1542  using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat]  hoelzl@60604  1543  by (simp only: fact_Suc add_Suc[symmetric] of_nat_id mult.assoc)  hoelzl@60604  1544 hoelzl@60604  1545  have "Suc a * (fact (Suc (a + b)) div (Suc a * fact a * fact b)) =  hoelzl@60604  1546  Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))"  hoelzl@60604  1547  by (subst div_mult_swap[symmetric]; simp only: mult.assoc dvd)  hoelzl@60604  1548  also have "\ = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))"  hoelzl@60604  1549  by (simp only: div_mult_mult1)  hoelzl@60604  1550  also have "\ = Suc b * (fact (Suc (a + b)) div (Suc b * (fact a * fact b)))"  hoelzl@60604  1551  using dvd[of b a] by (subst div_mult_swap[symmetric]; simp only: ac_simps dvd)  hoelzl@60604  1552  finally show ?thesis  hoelzl@60604  1553  by (subst (1 2) binomial_altdef_nat)  hoelzl@60604  1554  (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)  hoelzl@60604  1555 qed  hoelzl@60604  1556 eberlm@62128  1557 eberlm@62128  1558 eberlm@62128  1559 lemma fact_code [code]:  eberlm@62128  1560  "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"  eberlm@62128  1561 proof -  eberlm@62128  1562  have "fact n = (of_nat (\{1..n}) :: 'a)" by (simp add: fact_altdef')  eberlm@62128  1563  also have "\{1..n} = \{2..n}"  eberlm@62128  1564  by (intro setprod.mono_neutral_right) auto  eberlm@62128  1565  also have "\ = fold_atLeastAtMost_nat (op *) 2 n 1"  eberlm@62128  1566  by (simp add: setprod_atLeastAtMost_code)  eberlm@62128  1567  finally show ?thesis .  eberlm@62128  1568 qed  eberlm@62128  1569 eberlm@62128  1570 lemma pochhammer_code [code]:  hoelzl@62378  1571  "pochhammer a n = (if n = 0 then 1 else  eberlm@62128  1572  fold_atLeastAtMost_nat (\n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"  eberlm@62128  1573  by (simp add: setprod_atLeastAtMost_code pochhammer_def)  eberlm@62128  1574 eberlm@62128  1575 lemma gbinomial_code [code]:  hoelzl@62378  1576  "a gchoose n = (if n = 0 then 1 else  eberlm@62128  1577  fold_atLeastAtMost_nat (\n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"  eberlm@62128  1578  by (simp add: setprod_atLeastAtMost_code gbinomial_def)  eberlm@62128  1579 eberlm@62142  1580 (*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)  eberlm@62142  1581 eberlm@62142  1582 (*  eberlm@62128  1583 lemma binomial_code [code]:  eberlm@62128  1584  "(n choose k) =  eberlm@62128  1585  (if k > n then 0  eberlm@62128  1586  else if 2 * k > n then (n choose (n - k))  eberlm@62142  1587  else (fold_atLeastAtMost_nat (op * ) (n-k+1) n 1 div fact k))"  eberlm@62128  1588 proof -  eberlm@62128  1589  {  eberlm@62128  1590  assume "k \ n"  eberlm@62128  1591  hence "{1..n} = {1..n-k} \ {n-k+1..n}" by auto  eberlm@62128  1592  hence "(fact n :: nat) = fact (n-k) * \{n-k+1..n}"  eberlm@62128  1593  by (simp add: setprod.union_disjoint fact_altdef_nat)  eberlm@62128  1594  }  eberlm@62128  1595  thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)  hoelzl@62378  1596 qed  eberlm@62142  1597 *)  eberlm@62128  1598 nipkow@15131  1599 end `