src/HOL/Binomial.thy
 author haftmann Mon Aug 14 13:46:06 2006 +0200 (2006-08-14) changeset 20380 14f9f2a1caa6 parent 20217 25b068a99d2b permissions -rw-r--r--
simplified code generator setup
 nipkow@16732 ` 1` ```(* Title: HOL/Binomial.thy ``` nipkow@16732 ` 2` ``` ID: \$Id\$ ``` nipkow@16732 ` 3` ``` Author: Lawrence C Paulson ``` nipkow@16732 ` 4` ``` Copyright 1997 University of Cambridge ``` nipkow@16732 ` 5` ```*) ``` nipkow@16732 ` 6` nipkow@16732 ` 7` ```header{*Binomial Coefficients*} ``` nipkow@16732 ` 8` nipkow@16732 ` 9` ```theory Binomial ``` wenzelm@17508 ` 10` ```imports GCD ``` nipkow@16732 ` 11` ```begin ``` nipkow@16732 ` 12` nipkow@16732 ` 13` ```text{*This development is based on the work of Andy Gordon and ``` nipkow@16732 ` 14` ```Florian Kammueller*} ``` nipkow@16732 ` 15` nipkow@16732 ` 16` ```consts ``` nipkow@16732 ` 17` ``` binomial :: "nat \ nat \ nat" (infixl "choose" 65) ``` nipkow@16732 ` 18` nipkow@16732 ` 19` ```primrec ``` nipkow@16732 ` 20` ``` binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" ``` nipkow@16732 ` 21` nipkow@16732 ` 22` ``` binomial_Suc: "(Suc n choose k) = ``` nipkow@16732 ` 23` ``` (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" ``` nipkow@16732 ` 24` nipkow@16732 ` 25` ```lemma binomial_n_0 [simp]: "(n choose 0) = 1" ``` wenzelm@17508 ` 26` ```by (cases n) simp_all ``` nipkow@16732 ` 27` nipkow@16732 ` 28` ```lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" ``` nipkow@16732 ` 29` ```by simp ``` nipkow@16732 ` 30` nipkow@16732 ` 31` ```lemma binomial_Suc_Suc [simp]: ``` nipkow@16732 ` 32` ``` "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" ``` nipkow@16732 ` 33` ```by simp ``` nipkow@16732 ` 34` nipkow@16732 ` 35` ```lemma binomial_eq_0 [rule_format]: "\k. n < k --> (n choose k) = 0" ``` webertj@20217 ` 36` ```apply (induct "n") ``` webertj@20217 ` 37` ```apply auto ``` nipkow@16732 ` 38` ```done ``` nipkow@16732 ` 39` nipkow@16732 ` 40` ```declare binomial_0 [simp del] binomial_Suc [simp del] ``` nipkow@16732 ` 41` nipkow@16732 ` 42` ```lemma binomial_n_n [simp]: "(n choose n) = 1" ``` nipkow@16732 ` 43` ```apply (induct "n") ``` nipkow@16732 ` 44` ```apply (simp_all add: binomial_eq_0) ``` nipkow@16732 ` 45` ```done ``` nipkow@16732 ` 46` nipkow@16732 ` 47` ```lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" ``` nipkow@16732 ` 48` ```by (induct "n", simp_all) ``` nipkow@16732 ` 49` nipkow@16732 ` 50` ```lemma binomial_1 [simp]: "(n choose Suc 0) = n" ``` nipkow@16732 ` 51` ```by (induct "n", simp_all) ``` nipkow@16732 ` 52` nipkow@16732 ` 53` ```lemma zero_less_binomial [rule_format]: "k \ n --> 0 < (n choose k)" ``` nipkow@16732 ` 54` ```by (rule_tac m = n and n = k in diff_induct, simp_all) ``` nipkow@16732 ` 55` nipkow@16732 ` 56` ```lemma binomial_eq_0_iff: "(n choose k = 0) = (nn)" ``` nipkow@16732 ` 63` ```by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) ``` nipkow@16732 ` 64` nipkow@16732 ` 65` ```(*Might be more useful if re-oriented*) ``` nipkow@16732 ` 66` ```lemma Suc_times_binomial_eq [rule_format]: ``` nipkow@16732 ` 67` ``` "\k. k \ n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" ``` nipkow@16732 ` 68` ```apply (induct "n") ``` nipkow@16732 ` 69` ```apply (simp add: binomial_0, clarify) ``` nipkow@16732 ` 70` ```apply (case_tac "k") ``` nipkow@16732 ` 71` ```apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq ``` nipkow@16732 ` 72` ``` binomial_eq_0) ``` nipkow@16732 ` 73` ```done ``` nipkow@16732 ` 74` nipkow@16732 ` 75` ```text{*This is the well-known version, but it's harder to use because of the ``` nipkow@16732 ` 76` ``` need to reason about division.*} ``` nipkow@16732 ` 77` ```lemma binomial_Suc_Suc_eq_times: ``` nipkow@16732 ` 78` ``` "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" ``` nipkow@16732 ` 79` ```by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc ``` nipkow@16732 ` 80` ``` del: mult_Suc mult_Suc_right) ``` nipkow@16732 ` 81` nipkow@16732 ` 82` ```text{*Another version, with -1 instead of Suc.*} ``` nipkow@16732 ` 83` ```lemma times_binomial_minus1_eq: ``` nipkow@16732 ` 84` ``` "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" ``` nipkow@16732 ` 85` ```apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) ``` nipkow@16732 ` 86` ```apply (simp split add: nat_diff_split, auto) ``` nipkow@16732 ` 87` ```done ``` nipkow@16732 ` 88` nipkow@16732 ` 89` ```subsubsection {* Theorems about @{text "choose"} *} ``` nipkow@16732 ` 90` nipkow@16732 ` 91` ```text {* ``` nipkow@16732 ` 92` ``` \medskip Basic theorem about @{text "choose"}. By Florian ``` nipkow@16732 ` 93` ``` Kamm\"uller, tidied by LCP. ``` nipkow@16732 ` 94` ```*} ``` nipkow@16732 ` 95` nipkow@16732 ` 96` ```lemma card_s_0_eq_empty: ``` nipkow@16732 ` 97` ``` "finite A ==> card {B. B \ A & card B = 0} = 1" ``` nipkow@16732 ` 98` ``` apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) ``` nipkow@16732 ` 99` ``` apply (simp cong add: rev_conj_cong) ``` nipkow@16732 ` 100` ``` done ``` nipkow@16732 ` 101` nipkow@16732 ` 102` ```lemma choose_deconstruct: "finite M ==> x \ M ``` nipkow@16732 ` 103` ``` ==> {s. s <= insert x M & card(s) = Suc k} ``` nipkow@16732 ` 104` ``` = {s. s <= M & card(s) = Suc k} Un ``` nipkow@16732 ` 105` ``` {s. EX t. t <= M & card(t) = k & s = insert x t}" ``` nipkow@16732 ` 106` ``` apply safe ``` nipkow@16732 ` 107` ``` apply (auto intro: finite_subset [THEN card_insert_disjoint]) ``` nipkow@16732 ` 108` ``` apply (drule_tac x = "xa - {x}" in spec) ``` nipkow@16732 ` 109` ``` apply (subgoal_tac "x \ xa", auto) ``` nipkow@16732 ` 110` ``` apply (erule rev_mp, subst card_Diff_singleton) ``` nipkow@16732 ` 111` ``` apply (auto intro: finite_subset) ``` nipkow@16732 ` 112` ``` done ``` nipkow@16732 ` 113` nipkow@16732 ` 114` ```text{*There are as many subsets of @{term A} having cardinality @{term k} ``` nipkow@16732 ` 115` ``` as there are sets obtained from the former by inserting a fixed element ``` nipkow@16732 ` 116` ``` @{term x} into each.*} ``` nipkow@16732 ` 117` ```lemma constr_bij: ``` nipkow@16732 ` 118` ``` "[|finite A; x \ A|] ==> ``` nipkow@16732 ` 119` ``` card {B. EX C. C <= A & card(C) = k & B = insert x C} = ``` nipkow@16732 ` 120` ``` card {B. B <= A & card(B) = k}" ``` nipkow@16732 ` 121` ``` apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) ``` nipkow@16732 ` 122` ``` apply (auto elim!: equalityE simp add: inj_on_def) ``` nipkow@16732 ` 123` ``` apply (subst Diff_insert0, auto) ``` nipkow@16732 ` 124` ``` txt {* finiteness of the two sets *} ``` nipkow@16732 ` 125` ``` apply (rule_tac [2] B = "Pow (A)" in finite_subset) ``` nipkow@16732 ` 126` ``` apply (rule_tac B = "Pow (insert x A)" in finite_subset) ``` nipkow@16732 ` 127` ``` apply fast+ ``` nipkow@16732 ` 128` ``` done ``` nipkow@16732 ` 129` nipkow@16732 ` 130` ```text {* ``` nipkow@16732 ` 131` ``` Main theorem: combinatorial statement about number of subsets of a set. ``` nipkow@16732 ` 132` ```*} ``` nipkow@16732 ` 133` nipkow@16732 ` 134` ```lemma n_sub_lemma: ``` nipkow@16732 ` 135` ``` "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" ``` nipkow@16732 ` 136` ``` apply (induct k) ``` nipkow@16732 ` 137` ``` apply (simp add: card_s_0_eq_empty, atomize) ``` nipkow@16732 ` 138` ``` apply (rotate_tac -1, erule finite_induct) ``` nipkow@16732 ` 139` ``` apply (simp_all (no_asm_simp) cong add: conj_cong ``` nipkow@16732 ` 140` ``` add: card_s_0_eq_empty choose_deconstruct) ``` nipkow@16732 ` 141` ``` apply (subst card_Un_disjoint) ``` nipkow@16732 ` 142` ``` prefer 4 apply (force simp add: constr_bij) ``` nipkow@16732 ` 143` ``` prefer 3 apply force ``` nipkow@16732 ` 144` ``` prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] ``` nipkow@16732 ` 145` ``` finite_subset [of _ "Pow (insert x F)", standard]) ``` nipkow@16732 ` 146` ``` apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) ``` nipkow@16732 ` 147` ``` done ``` nipkow@16732 ` 148` nipkow@16732 ` 149` ```theorem n_subsets: ``` nipkow@16732 ` 150` ``` "finite A ==> card {B. B <= A & card B = k} = (card A choose k)" ``` nipkow@16732 ` 151` ``` by (simp add: n_sub_lemma) ``` nipkow@16732 ` 152` nipkow@16732 ` 153` nipkow@16732 ` 154` ```text{* The binomial theorem (courtesy of Tobias Nipkow): *} ``` nipkow@16732 ` 155` nipkow@16732 ` 156` ```theorem binomial: "(a+b::nat)^n = (\k=0..n. (n choose k) * a^k * b^(n-k))" ``` nipkow@16732 ` 157` ```proof (induct n) ``` nipkow@16732 ` 158` ``` case 0 thus ?case by simp ``` nipkow@16732 ` 159` ```next ``` nipkow@16732 ` 160` ``` case (Suc n) ``` nipkow@16732 ` 161` ``` have decomp: "{0..n+1} = {0} \ {n+1} \ {1..n}" ``` nipkow@16732 ` 162` ``` by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) ``` nipkow@16732 ` 163` ``` have decomp2: "{0..n} = {0} \ {1..n}" ``` nipkow@16732 ` 164` ``` by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) ``` nipkow@16732 ` 165` ``` have "(a+b::nat)^(n+1) = (a+b) * (\k=0..n. (n choose k) * a^k * b^(n-k))" ``` nipkow@16732 ` 166` ``` using Suc by simp ``` nipkow@16732 ` 167` ``` also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + ``` nipkow@16732 ` 168` ``` b*(\k=0..n. (n choose k) * a^k * b^(n-k))" ``` nipkow@16732 ` 169` ``` by(rule nat_distrib) ``` nipkow@16732 ` 170` ``` also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + ``` nipkow@16732 ` 171` ``` (\k=0..n. (n choose k) * a^k * b^(n-k+1))" ``` ballarin@19279 ` 172` ``` by(simp add: setsum_right_distrib mult_ac) ``` nipkow@16732 ` 173` ``` also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + ``` nipkow@16732 ` 174` ``` (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" ``` nipkow@16732 ` 175` ``` by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le ``` nipkow@16732 ` 176` ``` del:setsum_cl_ivl_Suc) ``` nipkow@16732 ` 177` ``` also have "\ = a^(n+1) + b^(n+1) + ``` nipkow@16732 ` 178` ``` (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + ``` nipkow@16732 ` 179` ``` (\k=1..n. (n choose k) * a^k * b^(n+1-k))" ``` nipkow@16732 ` 180` ``` by(simp add: decomp2) ``` nipkow@16732 ` 181` ``` also have ``` nipkow@16732 ` 182` ``` "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" ``` nipkow@16732 ` 183` ``` by(simp add: nat_distrib setsum_addf binomial.simps) ``` nipkow@16732 ` 184` ``` also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" ``` nipkow@16732 ` 185` ``` using decomp by simp ``` nipkow@16732 ` 186` ``` finally show ?case by simp ``` nipkow@16732 ` 187` ```qed ``` nipkow@16732 ` 188` nipkow@16732 ` 189` ```end ```