src/HOL/Library/Binomial.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 31287 6c593b431f04 child 32042 df28ead1cf19 child 32158 4dc119d4fc8b permissions -rw-r--r--
cleaned up some proofs
 wenzelm@21256 ` 1` ```(* Title: HOL/Binomial.thy ``` chaieb@29694 ` 2` ``` Author: Lawrence C Paulson, Amine Chaieb ``` wenzelm@21256 ` 3` ``` Copyright 1997 University of Cambridge ``` wenzelm@21256 ` 4` ```*) ``` wenzelm@21256 ` 5` wenzelm@21263 ` 6` ```header {* Binomial Coefficients *} ``` wenzelm@21256 ` 7` wenzelm@21256 ` 8` ```theory Binomial ``` huffman@31287 ` 9` ```imports Fact SetInterval Presburger Main Rational ``` wenzelm@21256 ` 10` ```begin ``` wenzelm@21256 ` 11` wenzelm@21263 ` 12` ```text {* This development is based on the work of Andy Gordon and ``` wenzelm@21263 ` 13` ``` Florian Kammueller. *} ``` wenzelm@21256 ` 14` haftmann@29931 ` 15` ```primrec binomial :: "nat \ nat \ nat" (infixl "choose" 65) where ``` wenzelm@21263 ` 16` ``` binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" ``` haftmann@29931 ` 17` ``` | binomial_Suc: "(Suc n choose k) = ``` wenzelm@21256 ` 18` ``` (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" ``` wenzelm@21256 ` 19` wenzelm@21256 ` 20` ```lemma binomial_n_0 [simp]: "(n choose 0) = 1" ``` nipkow@25134 ` 21` ```by (cases n) simp_all ``` wenzelm@21256 ` 22` wenzelm@21256 ` 23` ```lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" ``` nipkow@25134 ` 24` ```by simp ``` wenzelm@21256 ` 25` wenzelm@21256 ` 26` ```lemma binomial_Suc_Suc [simp]: ``` nipkow@25134 ` 27` ``` "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" ``` nipkow@25134 ` 28` ```by simp ``` wenzelm@21256 ` 29` wenzelm@21263 ` 30` ```lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0" ``` nipkow@25134 ` 31` ```by (induct n) auto ``` wenzelm@21256 ` 32` wenzelm@21256 ` 33` ```declare binomial_0 [simp del] binomial_Suc [simp del] ``` wenzelm@21256 ` 34` wenzelm@21256 ` 35` ```lemma binomial_n_n [simp]: "(n choose n) = 1" ``` nipkow@25134 ` 36` ```by (induct n) (simp_all add: binomial_eq_0) ``` wenzelm@21256 ` 37` wenzelm@21256 ` 38` ```lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" ``` nipkow@25134 ` 39` ```by (induct n) simp_all ``` wenzelm@21256 ` 40` wenzelm@21256 ` 41` ```lemma binomial_1 [simp]: "(n choose Suc 0) = n" ``` nipkow@25134 ` 42` ```by (induct n) simp_all ``` wenzelm@21256 ` 43` nipkow@25162 ` 44` ```lemma zero_less_binomial: "k \ n ==> (n choose k) > 0" ``` nipkow@25134 ` 45` ```by (induct n k rule: diff_induct) simp_all ``` wenzelm@21256 ` 46` wenzelm@21256 ` 47` ```lemma binomial_eq_0_iff: "(n choose k = 0) = (n 0) = (k\n)" ``` nipkow@25162 ` 54` ```by(simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] ``` nipkow@25162 ` 55` ``` del:neq0_conv) ``` wenzelm@21256 ` 56` wenzelm@21256 ` 57` ```(*Might be more useful if re-oriented*) ``` wenzelm@21263 ` 58` ```lemma Suc_times_binomial_eq: ``` nipkow@25134 ` 59` ``` "!!k. k \ n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" ``` nipkow@25134 ` 60` ```apply (induct n) ``` nipkow@25134 ` 61` ```apply (simp add: binomial_0) ``` nipkow@25134 ` 62` ```apply (case_tac k) ``` nipkow@25134 ` 63` ```apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq ``` wenzelm@21263 ` 64` ``` binomial_eq_0) ``` nipkow@25134 ` 65` ```done ``` wenzelm@21256 ` 66` wenzelm@21256 ` 67` ```text{*This is the well-known version, but it's harder to use because of the ``` wenzelm@21256 ` 68` ``` need to reason about division.*} ``` wenzelm@21256 ` 69` ```lemma binomial_Suc_Suc_eq_times: ``` wenzelm@21263 ` 70` ``` "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" ``` wenzelm@21263 ` 71` ``` by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc ``` wenzelm@21263 ` 72` ``` del: mult_Suc mult_Suc_right) ``` wenzelm@21256 ` 73` wenzelm@21256 ` 74` ```text{*Another version, with -1 instead of Suc.*} ``` wenzelm@21256 ` 75` ```lemma times_binomial_minus1_eq: ``` wenzelm@21263 ` 76` ``` "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" ``` wenzelm@21263 ` 77` ``` apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) ``` wenzelm@21263 ` 78` ``` apply (simp split add: nat_diff_split, auto) ``` wenzelm@21263 ` 79` ``` done ``` wenzelm@21263 ` 80` wenzelm@21256 ` 81` wenzelm@25378 ` 82` ```subsection {* Theorems about @{text "choose"} *} ``` wenzelm@21256 ` 83` wenzelm@21256 ` 84` ```text {* ``` wenzelm@21256 ` 85` ``` \medskip Basic theorem about @{text "choose"}. By Florian ``` wenzelm@21256 ` 86` ``` Kamm\"uller, tidied by LCP. ``` wenzelm@21256 ` 87` ```*} ``` wenzelm@21256 ` 88` wenzelm@21256 ` 89` ```lemma card_s_0_eq_empty: ``` wenzelm@21256 ` 90` ``` "finite A ==> card {B. B \ A & card B = 0} = 1" ``` nipkow@31166 ` 91` ```by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) ``` wenzelm@21256 ` 92` wenzelm@21256 ` 93` ```lemma choose_deconstruct: "finite M ==> x \ M ``` wenzelm@21256 ` 94` ``` ==> {s. s <= insert x M & card(s) = Suc k} ``` wenzelm@21256 ` 95` ``` = {s. s <= M & card(s) = Suc k} Un ``` wenzelm@21256 ` 96` ``` {s. EX t. t <= M & card(t) = k & s = insert x t}" ``` wenzelm@21256 ` 97` ``` apply safe ``` wenzelm@21256 ` 98` ``` apply (auto intro: finite_subset [THEN card_insert_disjoint]) ``` wenzelm@21256 ` 99` ``` apply (drule_tac x = "xa - {x}" in spec) ``` wenzelm@21256 ` 100` ``` apply (subgoal_tac "x \ xa", auto) ``` wenzelm@21256 ` 101` ``` apply (erule rev_mp, subst card_Diff_singleton) ``` wenzelm@21256 ` 102` ``` apply (auto intro: finite_subset) ``` wenzelm@21256 ` 103` ``` done ``` nipkow@29918 ` 104` ```(* ``` nipkow@29918 ` 105` ```lemma "finite(UN y. {x. P x y})" ``` nipkow@29918 ` 106` ```apply simp ``` nipkow@29918 ` 107` ```lemma Collect_ex_eq ``` nipkow@29918 ` 108` nipkow@29918 ` 109` ```lemma "{x. EX y. P x y} = (UN y. {x. P x y})" ``` nipkow@29918 ` 110` ```apply blast ``` nipkow@29918 ` 111` ```*) ``` nipkow@29918 ` 112` nipkow@29918 ` 113` ```lemma finite_bex_subset[simp]: ``` nipkow@29918 ` 114` ``` "finite B \ (!!A. A<=B \ finite{x. P x A}) \ finite{x. EX A<=B. P x A}" ``` nipkow@29918 ` 115` ```apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})") ``` nipkow@29918 ` 116` ``` apply simp ``` nipkow@29918 ` 117` ```apply blast ``` nipkow@29918 ` 118` ```done ``` wenzelm@21256 ` 119` wenzelm@21256 ` 120` ```text{*There are as many subsets of @{term A} having cardinality @{term k} ``` wenzelm@21256 ` 121` ``` as there are sets obtained from the former by inserting a fixed element ``` wenzelm@21256 ` 122` ``` @{term x} into each.*} ``` wenzelm@21256 ` 123` ```lemma constr_bij: ``` wenzelm@21256 ` 124` ``` "[|finite A; x \ A|] ==> ``` wenzelm@21256 ` 125` ``` card {B. EX C. C <= A & card(C) = k & B = insert x C} = ``` wenzelm@21256 ` 126` ``` card {B. B <= A & card(B) = k}" ``` nipkow@29918 ` 127` ```apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) ``` nipkow@29918 ` 128` ``` apply (auto elim!: equalityE simp add: inj_on_def) ``` nipkow@29918 ` 129` ```apply (subst Diff_insert0, auto) ``` nipkow@29918 ` 130` ```done ``` wenzelm@21256 ` 131` wenzelm@21256 ` 132` ```text {* ``` wenzelm@21256 ` 133` ``` Main theorem: combinatorial statement about number of subsets of a set. ``` wenzelm@21256 ` 134` ```*} ``` wenzelm@21256 ` 135` wenzelm@21256 ` 136` ```lemma n_sub_lemma: ``` wenzelm@21263 ` 137` ``` "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" ``` wenzelm@21256 ` 138` ``` apply (induct k) ``` wenzelm@21256 ` 139` ``` apply (simp add: card_s_0_eq_empty, atomize) ``` wenzelm@21256 ` 140` ``` apply (rotate_tac -1, erule finite_induct) ``` wenzelm@21256 ` 141` ``` apply (simp_all (no_asm_simp) cong add: conj_cong ``` wenzelm@21256 ` 142` ``` add: card_s_0_eq_empty choose_deconstruct) ``` wenzelm@21256 ` 143` ``` apply (subst card_Un_disjoint) ``` wenzelm@21256 ` 144` ``` prefer 4 apply (force simp add: constr_bij) ``` wenzelm@21256 ` 145` ``` prefer 3 apply force ``` wenzelm@21256 ` 146` ``` prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] ``` wenzelm@21256 ` 147` ``` finite_subset [of _ "Pow (insert x F)", standard]) ``` wenzelm@21256 ` 148` ``` apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) ``` wenzelm@21256 ` 149` ``` done ``` wenzelm@21256 ` 150` wenzelm@21256 ` 151` ```theorem n_subsets: ``` wenzelm@21256 ` 152` ``` "finite A ==> card {B. B <= A & card B = k} = (card A choose k)" ``` wenzelm@21256 ` 153` ``` by (simp add: n_sub_lemma) ``` wenzelm@21256 ` 154` wenzelm@21256 ` 155` wenzelm@21256 ` 156` ```text{* The binomial theorem (courtesy of Tobias Nipkow): *} ``` wenzelm@21256 ` 157` wenzelm@21256 ` 158` ```theorem binomial: "(a+b::nat)^n = (\k=0..n. (n choose k) * a^k * b^(n-k))" ``` wenzelm@21256 ` 159` ```proof (induct n) ``` wenzelm@21256 ` 160` ``` case 0 thus ?case by simp ``` wenzelm@21256 ` 161` ```next ``` wenzelm@21256 ` 162` ``` case (Suc n) ``` wenzelm@21256 ` 163` ``` have decomp: "{0..n+1} = {0} \ {n+1} \ {1..n}" ``` wenzelm@21256 ` 164` ``` by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) ``` wenzelm@21256 ` 165` ``` have decomp2: "{0..n} = {0} \ {1..n}" ``` wenzelm@21256 ` 166` ``` by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) ``` wenzelm@21256 ` 167` ``` have "(a+b::nat)^(n+1) = (a+b) * (\k=0..n. (n choose k) * a^k * b^(n-k))" ``` wenzelm@21256 ` 168` ``` using Suc by simp ``` wenzelm@21256 ` 169` ``` also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + ``` wenzelm@21256 ` 170` ``` b*(\k=0..n. (n choose k) * a^k * b^(n-k))" ``` wenzelm@21263 ` 171` ``` by (rule nat_distrib) ``` wenzelm@21256 ` 172` ``` also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + ``` wenzelm@21256 ` 173` ``` (\k=0..n. (n choose k) * a^k * b^(n-k+1))" ``` wenzelm@21263 ` 174` ``` by (simp add: setsum_right_distrib mult_ac) ``` wenzelm@21256 ` 175` ``` also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + ``` wenzelm@21256 ` 176` ``` (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" ``` wenzelm@21256 ` 177` ``` by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le ``` wenzelm@21256 ` 178` ``` del:setsum_cl_ivl_Suc) ``` wenzelm@21256 ` 179` ``` also have "\ = a^(n+1) + b^(n+1) + ``` wenzelm@21256 ` 180` ``` (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + ``` wenzelm@21256 ` 181` ``` (\k=1..n. (n choose k) * a^k * b^(n+1-k))" ``` wenzelm@21263 ` 182` ``` by (simp add: decomp2) ``` wenzelm@21256 ` 183` ``` also have ``` wenzelm@21263 ` 184` ``` "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" ``` wenzelm@21263 ` 185` ``` by (simp add: nat_distrib setsum_addf binomial.simps) ``` wenzelm@21256 ` 186` ``` also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" ``` wenzelm@21256 ` 187` ``` using decomp by simp ``` wenzelm@21256 ` 188` ``` finally show ?case by simp ``` wenzelm@21256 ` 189` ```qed ``` wenzelm@21256 ` 190` huffman@29906 ` 191` ```subsection{* Pochhammer's symbol : generalized raising factorial*} ``` chaieb@29694 ` 192` chaieb@29694 ` 193` ```definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\n. a + of_nat n) {0 .. n - 1})" ``` chaieb@29694 ` 194` chaieb@29694 ` 195` ```lemma pochhammer_0[simp]: "pochhammer a 0 = 1" ``` chaieb@29694 ` 196` ``` by (simp add: pochhammer_def) ``` chaieb@29694 ` 197` chaieb@29694 ` 198` ```lemma pochhammer_1[simp]: "pochhammer a 1 = a" by (simp add: pochhammer_def) ``` chaieb@29694 ` 199` ```lemma pochhammer_Suc0[simp]: "pochhammer a (Suc 0) = a" ``` chaieb@29694 ` 200` ``` by (simp add: pochhammer_def) ``` chaieb@29694 ` 201` chaieb@29694 ` 202` ```lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\n. a + of_nat n) {0 .. n}" ``` chaieb@29694 ` 203` ``` by (simp add: pochhammer_def) ``` chaieb@29694 ` 204` chaieb@29694 ` 205` ```lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)" ``` chaieb@29694 ` 206` ```proof- ``` chaieb@29694 ` 207` ``` have th: "finite {0..n}" "finite {Suc n}" "{0..n} \ {Suc n} = {}" by auto ``` chaieb@29694 ` 208` ``` have eq: "{0..Suc n} = {0..n} \ {Suc n}" by auto ``` chaieb@29694 ` 209` ``` show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp ``` chaieb@29694 ` 210` ```qed ``` chaieb@29694 ` 211` chaieb@29694 ` 212` ```lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}" ``` chaieb@29694 ` 213` ```proof- ``` chaieb@29694 ` 214` ``` have th: "finite {0}" "finite {1..Suc n}" "{0} \ {1.. Suc n} = {}" by auto ``` chaieb@29694 ` 215` ``` have eq: "{0..Suc n} = {0} \ {1 .. Suc n}" by auto ``` chaieb@29694 ` 216` ``` show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp ``` chaieb@29694 ` 217` ```qed ``` chaieb@29694 ` 218` chaieb@29694 ` 219` chaieb@29694 ` 220` ```lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" ``` chaieb@29694 ` 221` ```proof- ``` chaieb@29694 ` 222` ``` {assume "n=0" then have ?thesis by simp} ``` chaieb@29694 ` 223` ``` moreover ``` chaieb@29694 ` 224` ``` {fix m assume m: "n = Suc m" ``` chaieb@29694 ` 225` ``` have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..} ``` chaieb@29694 ` 226` ``` ultimately show ?thesis by (cases n, auto) ``` chaieb@29694 ` 227` ```qed ``` chaieb@29694 ` 228` chaieb@29694 ` 229` ```lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" ``` chaieb@29694 ` 230` ```proof- ``` chaieb@29694 ` 231` ``` {assume "n=0" then have ?thesis by (simp add: pochhammer_Suc_setprod)} ``` chaieb@29694 ` 232` ``` moreover ``` chaieb@29694 ` 233` ``` {assume n0: "n \ 0" ``` chaieb@29694 ` 234` ``` have th0: "finite {1 .. n}" "0 \ {1 .. n}" by auto ``` chaieb@29694 ` 235` ``` have eq: "insert 0 {1 .. n} = {0..n}" by auto ``` chaieb@29694 ` 236` ``` have th1: "(\n\{1\nat..n}. a + of_nat n) = ``` chaieb@29694 ` 237` ``` (\n\{0\nat..n - 1}. a + 1 + of_nat n)" ``` chaieb@29694 ` 238` ``` apply (rule setprod_reindex_cong[where f = "Suc"]) ``` chaieb@29694 ` 239` ``` using n0 by (auto simp add: expand_fun_eq ring_simps) ``` chaieb@29694 ` 240` ``` have ?thesis apply (simp add: pochhammer_def) ``` chaieb@29694 ` 241` ``` unfolding setprod_insert[OF th0, unfolded eq] ``` chaieb@29694 ` 242` ``` using th1 by (simp add: ring_simps)} ``` chaieb@29694 ` 243` ```ultimately show ?thesis by blast ``` chaieb@29694 ` 244` ```qed ``` chaieb@29694 ` 245` chaieb@29694 ` 246` ```lemma fact_setprod: "fact n = setprod id {1 .. n}" ``` chaieb@29694 ` 247` ``` apply (induct n, simp) ``` chaieb@29694 ` 248` ``` apply (simp only: fact_Suc atLeastAtMostSuc_conv) ``` chaieb@29694 ` 249` ``` apply (subst setprod_insert) ``` chaieb@29694 ` 250` ``` by simp_all ``` chaieb@29694 ` 251` chaieb@29694 ` 252` ```lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n" ``` chaieb@29694 ` 253` ``` unfolding fact_setprod ``` chaieb@29694 ` 254` ``` ``` chaieb@29694 ` 255` ``` apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod) ``` chaieb@29694 ` 256` ``` apply (rule setprod_reindex_cong[where f=Suc]) ``` chaieb@29694 ` 257` ``` by (auto simp add: expand_fun_eq) ``` chaieb@29694 ` 258` chaieb@29694 ` 259` ```lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n" ``` chaieb@29694 ` 260` ``` shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0" ``` chaieb@29694 ` 261` ```proof- ``` chaieb@29694 ` 262` ``` from kn obtain h where h: "k = Suc h" by (cases k, auto) ``` chaieb@29694 ` 263` ``` {assume n0: "n=0" then have ?thesis using kn ``` chaieb@29694 ` 264` ``` by (cases k, simp_all add: pochhammer_rec del: pochhammer_Suc)} ``` chaieb@29694 ` 265` ``` moreover ``` chaieb@29694 ` 266` ``` {assume n0: "n \ 0" ``` chaieb@29694 ` 267` ``` then have ?thesis apply (simp add: h pochhammer_Suc_setprod) ``` chaieb@29694 ` 268` ``` apply (rule_tac x="n" in bexI) ``` chaieb@29694 ` 269` ``` using h kn by auto} ``` chaieb@29694 ` 270` ```ultimately show ?thesis by blast ``` chaieb@29694 ` 271` ```qed ``` chaieb@29694 ` 272` chaieb@29694 ` 273` ```lemma pochhammer_of_nat_eq_0_lemma': assumes kn: "k \ n" ``` chaieb@29694 ` 274` ``` shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k \ 0" ``` chaieb@29694 ` 275` ```proof- ``` chaieb@29694 ` 276` ``` {assume "k=0" then have ?thesis by simp} ``` chaieb@29694 ` 277` ``` moreover ``` chaieb@29694 ` 278` ``` {fix h assume h: "k = Suc h" ``` chaieb@29694 ` 279` ``` then have ?thesis apply (simp add: pochhammer_Suc_setprod) ``` nipkow@30843 ` 280` ``` using h kn by (auto simp add: algebra_simps)} ``` chaieb@29694 ` 281` ``` ultimately show ?thesis by (cases k, auto) ``` chaieb@29694 ` 282` ```qed ``` chaieb@29694 ` 283` chaieb@29694 ` 284` ```lemma pochhammer_of_nat_eq_0_iff: ``` chaieb@29694 ` 285` ``` shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k = 0 \ k > n" ``` chaieb@29694 ` 286` ``` (is "?l = ?r") ``` chaieb@29694 ` 287` ``` using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] ``` chaieb@29694 ` 288` ``` pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] ``` chaieb@29694 ` 289` ``` by (auto simp add: not_le[symmetric]) ``` chaieb@29694 ` 290` huffman@29906 ` 291` ```subsection{* Generalized binomial coefficients *} ``` chaieb@29694 ` 292` huffman@31287 ` 293` ```definition gbinomial :: "'a::field_char_0 \ nat \ 'a" (infixl "gchoose" 65) ``` chaieb@29694 ` 294` ``` where "a gchoose n = (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))" ``` chaieb@29694 ` 295` chaieb@29694 ` 296` ```lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" ``` nipkow@30843 ` 297` ```apply (simp_all add: gbinomial_def) ``` nipkow@30843 ` 298` ```apply (subgoal_tac "(\i\nat\{0\nat..n}. - of_nat i) = (0::'b)") ``` nipkow@30843 ` 299` ``` apply (simp del:setprod_zero_iff) ``` nipkow@30843 ` 300` ```apply simp ``` nipkow@30843 ` 301` ```done ``` chaieb@29694 ` 302` chaieb@29694 ` 303` ```lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)" ``` chaieb@29694 ` 304` ```proof- ``` chaieb@29694 ` 305` ``` {assume "n=0" then have ?thesis by simp} ``` chaieb@29694 ` 306` ``` moreover ``` chaieb@29694 ` 307` ``` {assume n0: "n\0" ``` chaieb@29694 ` 308` ``` from n0 setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"] ``` chaieb@29694 ` 309` ``` have eq: "(- (1\'a)) ^ n = setprod (\i. - 1) {0 .. n - 1}" ``` chaieb@29694 ` 310` ``` by auto ``` chaieb@29694 ` 311` ``` from n0 have ?thesis ``` chaieb@29694 ` 312` ``` by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric])} ``` chaieb@29694 ` 313` ``` ultimately show ?thesis by blast ``` chaieb@29694 ` 314` ```qed ``` chaieb@29694 ` 315` chaieb@29694 ` 316` ```lemma binomial_fact_lemma: ``` chaieb@29694 ` 317` ``` "k \ n \ fact k * fact (n - k) * (n choose k) = fact n" ``` chaieb@29694 ` 318` ```proof(induct n arbitrary: k rule: nat_less_induct) ``` chaieb@29694 ` 319` ``` fix n k assume H: "\mx\m. fact x * fact (m - x) * (m choose x) = ``` chaieb@29694 ` 320` ``` fact m" and kn: "k \ n" ``` chaieb@29694 ` 321` ``` let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" ``` chaieb@29694 ` 322` ``` {assume "n=0" then have ?ths using kn by simp} ``` chaieb@29694 ` 323` ``` moreover ``` chaieb@29694 ` 324` ``` {assume "k=0" then have ?ths using kn by simp} ``` chaieb@29694 ` 325` ``` moreover ``` chaieb@29694 ` 326` ``` {assume nk: "n=k" then have ?ths by simp} ``` chaieb@29694 ` 327` ``` moreover ``` chaieb@29694 ` 328` ``` {fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" ``` chaieb@29694 ` 329` ``` from n have mn: "m < n" by arith ``` chaieb@29694 ` 330` ``` from hm have hm': "h \ m" by arith ``` chaieb@29694 ` 331` ``` from hm h n kn have km: "k \ m" by arith ``` chaieb@29694 ` 332` ``` have "m - h = Suc (m - Suc h)" using h km hm by arith ``` chaieb@29694 ` 333` ``` with km h have th0: "fact (m - h) = (m - h) * fact (m - k)" ``` chaieb@29694 ` 334` ``` by simp ``` chaieb@29694 ` 335` ``` from n h th0 ``` chaieb@29694 ` 336` ``` have "fact k * fact (n - k) * (n choose k) = k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" ``` chaieb@29694 ` 337` ``` by (simp add: ring_simps) ``` chaieb@29694 ` 338` ``` also have "\ = (k + (m - h)) * fact m" ``` chaieb@29694 ` 339` ``` using H[rule_format, OF mn hm'] H[rule_format, OF mn km] ``` chaieb@29694 ` 340` ``` by (simp add: ring_simps) ``` chaieb@29694 ` 341` ``` finally have ?ths using h n km by simp} ``` chaieb@29694 ` 342` ``` moreover have "n=0 \ k = 0 \ k = n \ (EX m h. n=Suc m \ k = Suc h \ h < m)" using kn by presburger ``` chaieb@29694 ` 343` ``` ultimately show ?ths by blast ``` chaieb@29694 ` 344` ```qed ``` chaieb@29694 ` 345` ``` ``` chaieb@29694 ` 346` ```lemma binomial_fact: ``` chaieb@29694 ` 347` ``` assumes kn: "k \ n" ``` huffman@31287 ` 348` ``` shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" ``` chaieb@29694 ` 349` ``` using binomial_fact_lemma[OF kn] ``` chaieb@29694 ` 350` ``` by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric]) ``` chaieb@29694 ` 351` chaieb@29694 ` 352` ```lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" ``` chaieb@29694 ` 353` ```proof- ``` chaieb@29694 ` 354` ``` {assume kn: "k > n" ``` chaieb@29694 ` 355` ``` from kn binomial_eq_0[OF kn] have ?thesis ``` chaieb@29694 ` 356` ``` by (simp add: gbinomial_pochhammer field_simps ``` chaieb@29694 ` 357` ``` pochhammer_of_nat_eq_0_iff)} ``` chaieb@29694 ` 358` ``` moreover ``` chaieb@29694 ` 359` ``` {assume "k=0" then have ?thesis by simp} ``` chaieb@29694 ` 360` ``` moreover ``` chaieb@29694 ` 361` ``` {assume kn: "k \ n" and k0: "k\ 0" ``` chaieb@29694 ` 362` ``` from k0 obtain h where h: "k = Suc h" by (cases k, auto) ``` chaieb@29694 ` 363` ``` from h ``` chaieb@29694 ` 364` ``` have eq:"(- 1 :: 'a) ^ k = setprod (\i. - 1) {0..h}" ``` chaieb@29694 ` 365` ``` by (subst setprod_constant, auto) ``` chaieb@29694 ` 366` ``` have eq': "(\i\{0..h}. of_nat n + - (of_nat i :: 'a)) = (\i\{n - h..n}. of_nat i)" ``` chaieb@29694 ` 367` ``` apply (rule strong_setprod_reindex_cong[where f="op - n"]) ``` chaieb@29694 ` 368` ``` using h kn ``` chaieb@29694 ` 369` ``` apply (simp_all add: inj_on_def image_iff Bex_def expand_set_eq) ``` chaieb@29694 ` 370` ``` apply clarsimp ``` chaieb@29694 ` 371` ``` apply (presburger) ``` chaieb@29694 ` 372` ``` apply presburger ``` chaieb@29694 ` 373` ``` by (simp add: expand_fun_eq ring_simps of_nat_add[symmetric] del: of_nat_add) ``` chaieb@29694 ` 374` ``` have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" ``` chaieb@29694 ` 375` ```"{1..n - Suc h} \ {n - h .. n} = {}" and eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}" using h kn by auto ``` chaieb@29694 ` 376` ``` from eq[symmetric] ``` chaieb@29694 ` 377` ``` have ?thesis using kn ``` chaieb@29694 ` 378` ``` apply (simp add: binomial_fact[OF kn, where ?'a = 'a] ``` chaieb@29694 ` 379` ``` gbinomial_pochhammer field_simps pochhammer_Suc_setprod) ``` huffman@30273 ` 380` ``` apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) ``` chaieb@29694 ` 381` ``` unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] ``` chaieb@29694 ` 382` ``` unfolding mult_assoc[symmetric] ``` chaieb@29694 ` 383` ``` unfolding setprod_timesf[symmetric] ``` chaieb@29694 ` 384` ``` apply simp ``` chaieb@29694 ` 385` ``` apply (rule strong_setprod_reindex_cong[where f= "op - n"]) ``` chaieb@29694 ` 386` ``` apply (auto simp add: inj_on_def image_iff Bex_def) ``` chaieb@29694 ` 387` ``` apply presburger ``` chaieb@29694 ` 388` ``` apply (subgoal_tac "(of_nat (n - x) :: 'a) = of_nat n - of_nat x") ``` chaieb@29694 ` 389` ``` apply simp ``` chaieb@29694 ` 390` ``` by (rule of_nat_diff, simp) ``` chaieb@29694 ` 391` ``` } ``` chaieb@29694 ` 392` ``` moreover ``` chaieb@29694 ` 393` ``` have "k > n \ k = 0 \ (k \ n \ k \ 0)" by arith ``` chaieb@29694 ` 394` ``` ultimately show ?thesis by blast ``` chaieb@29694 ` 395` ```qed ``` chaieb@29694 ` 396` chaieb@29694 ` 397` ```lemma gbinomial_1[simp]: "a gchoose 1 = a" ``` chaieb@29694 ` 398` ``` by (simp add: gbinomial_def) ``` chaieb@29694 ` 399` chaieb@29694 ` 400` ```lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a" ``` chaieb@29694 ` 401` ``` by (simp add: gbinomial_def) ``` chaieb@29694 ` 402` chaieb@29694 ` 403` ```lemma gbinomial_mult_1: "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") ``` chaieb@29694 ` 404` ```proof- ``` chaieb@29694 ` 405` ``` have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" ``` chaieb@29694 ` 406` ``` unfolding gbinomial_pochhammer ``` chaieb@29694 ` 407` ``` pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc ``` chaieb@29694 ` 408` ``` by (simp add: field_simps del: of_nat_Suc) ``` chaieb@29694 ` 409` ``` also have "\ = ?l" unfolding gbinomial_pochhammer ``` chaieb@29694 ` 410` ``` by (simp add: ring_simps) ``` chaieb@29694 ` 411` ``` finally show ?thesis .. ``` chaieb@29694 ` 412` ```qed ``` chaieb@29694 ` 413` chaieb@29694 ` 414` ```lemma gbinomial_mult_1': "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" ``` chaieb@29694 ` 415` ``` by (simp add: mult_commute gbinomial_mult_1) ``` chaieb@29694 ` 416` chaieb@29694 ` 417` ```lemma gbinomial_Suc: "a gchoose (Suc k) = (setprod (\i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))" ``` chaieb@29694 ` 418` ``` by (simp add: gbinomial_def) ``` chaieb@29694 ` 419` ``` ``` chaieb@29694 ` 420` ```lemma gbinomial_mult_fact: ``` huffman@31287 ` 421` ``` "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\i. a - of_nat i) {0 .. k})" ``` chaieb@29694 ` 422` ``` unfolding gbinomial_Suc ``` chaieb@29694 ` 423` ``` by (simp_all add: field_simps del: fact_Suc) ``` chaieb@29694 ` 424` chaieb@29694 ` 425` ```lemma gbinomial_mult_fact': ``` huffman@31287 ` 426` ``` "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\i. a - of_nat i) {0 .. k})" ``` chaieb@29694 ` 427` ``` using gbinomial_mult_fact[of k a] ``` chaieb@29694 ` 428` ``` apply (subst mult_commute) . ``` chaieb@29694 ` 429` huffman@31287 ` 430` ```lemma gbinomial_Suc_Suc: "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" ``` chaieb@29694 ` 431` ```proof- ``` chaieb@29694 ` 432` ``` {assume "k = 0" then have ?thesis by simp} ``` chaieb@29694 ` 433` ``` moreover ``` chaieb@29694 ` 434` ``` {fix h assume h: "k = Suc h" ``` chaieb@29694 ` 435` ``` have eq0: "(\i\{1..k}. (a + 1) - of_nat i) = (\i\{0..h}. a - of_nat i)" ``` chaieb@29694 ` 436` ``` apply (rule strong_setprod_reindex_cong[where f = Suc]) ``` chaieb@29694 ` 437` ``` using h by auto ``` chaieb@29694 ` 438` chaieb@29694 ` 439` ``` have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\i\{0\nat..Suc h}. a - of_nat i)" ``` chaieb@29694 ` 440` ``` unfolding h ``` chaieb@29694 ` 441` ``` apply (simp add: ring_simps del: fact_Suc) ``` chaieb@29694 ` 442` ``` unfolding gbinomial_mult_fact' ``` chaieb@29694 ` 443` ``` apply (subst fact_Suc) ``` chaieb@29694 ` 444` ``` unfolding of_nat_mult ``` chaieb@29694 ` 445` ``` apply (subst mult_commute) ``` chaieb@29694 ` 446` ``` unfolding mult_assoc ``` chaieb@29694 ` 447` ``` unfolding gbinomial_mult_fact ``` chaieb@29694 ` 448` ``` by (simp add: ring_simps) ``` chaieb@29694 ` 449` ``` also have "\ = (\i\{0..h}. a - of_nat i) * (a + 1)" ``` chaieb@29694 ` 450` ``` unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc ``` chaieb@29694 ` 451` ``` by (simp add: ring_simps h) ``` chaieb@29694 ` 452` ``` also have "\ = (\i\{0..k}. (a + 1) - of_nat i)" ``` chaieb@29694 ` 453` ``` using eq0 ``` chaieb@29694 ` 454` ``` unfolding h setprod_nat_ivl_1_Suc ``` chaieb@29694 ` 455` ``` by simp ``` chaieb@29694 ` 456` ``` also have "\ = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" ``` chaieb@29694 ` 457` ``` unfolding gbinomial_mult_fact .. ``` chaieb@29694 ` 458` ``` finally have ?thesis by (simp del: fact_Suc) } ``` chaieb@29694 ` 459` ``` ultimately show ?thesis by (cases k, auto) ``` chaieb@29694 ` 460` ```qed ``` chaieb@29694 ` 461` wenzelm@21256 ` 462` ```end ```