src/HOL/Number_Theory/Binomial.thy
changeset 56178 2a6f58938573
parent 55143 04448228381d
child 57129 7edb7550663e
     1.1 --- a/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 14:40:59 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 15:48:30 2014 +0000
     1.3 @@ -186,6 +186,37 @@
     1.4             of_nat_setsum [symmetric]
     1.5             of_nat_eq_iff of_nat_id)
     1.6  
     1.7 +lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
     1.8 +  using binomial [of 1 "1" n]
     1.9 +  by (simp add: numeral_2_eq_2)
    1.10 +
    1.11 +lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
    1.12 +  by (induct n) auto
    1.13 +
    1.14 +lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
    1.15 +  by (induct n) auto
    1.16 +
    1.17 +lemma natsum_reverse_index:
    1.18 +  fixes m::nat
    1.19 +  assumes "\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)"
    1.20 +  shows "(\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
    1.21 +apply (rule setsum_reindex_cong [where f = "\<lambda>k. m+n-k"])
    1.22 +apply (auto simp add: inj_on_def image_def)
    1.23 +apply (rule_tac x="m+n-x" in bexI, auto simp: assms)
    1.24 +done
    1.25 +
    1.26 +lemma sum_choose_diagonal:
    1.27 +  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
    1.28 +proof -
    1.29 +  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
    1.30 +    by (rule natsum_reverse_index) (simp add: assms)
    1.31 +  also have "... = Suc (n-m+m) choose m"
    1.32 +    by (rule sum_choose_lower)
    1.33 +  also have "... = Suc n choose m" using assms
    1.34 +    by simp
    1.35 +  finally show ?thesis .
    1.36 +qed
    1.37 +
    1.38  subsection{* Pochhammer's symbol : generalized rising factorial *}
    1.39  
    1.40  text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
    1.41 @@ -605,6 +636,42 @@
    1.42      n choose k = fact n div (fact k * fact (n - k))"
    1.43   by (subst binomial_fact_lemma [symmetric]) auto
    1.44  
    1.45 +lemma fact_fact_dvd_fact_m: fixes k::nat shows "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
    1.46 +  by (metis binomial_fact_lemma dvd_def)
    1.47 +
    1.48 +lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
    1.49 +  by (metis fact_fact_dvd_fact_m diff_add_inverse2 le_add2)
    1.50 +
    1.51 +lemma choose_mult_lemma:
    1.52 +     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
    1.53 +proof -
    1.54 +  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
    1.55 +        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
    1.56 +    by (simp add: assms binomial_altdef_nat)
    1.57 +  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
    1.58 +    apply (subst div_mult_div_if_dvd)
    1.59 +    apply (auto simp: fact_fact_dvd_fact)
    1.60 +    apply (metis ab_semigroup_add_class.add_ac(1) add_commute fact_fact_dvd_fact)
    1.61 +    done
    1.62 +  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
    1.63 +    apply (subst div_mult_div_if_dvd [symmetric])
    1.64 +    apply (auto simp: fact_fact_dvd_fact)
    1.65 +    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult_left_commute)
    1.66 +    done
    1.67 +  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
    1.68 +    apply (subst div_mult_div_if_dvd)
    1.69 +    apply (auto simp: fact_fact_dvd_fact)
    1.70 +    apply(metis mult_left_commute)
    1.71 +    done
    1.72 +  finally show ?thesis
    1.73 +    by (simp add: binomial_altdef_nat mult_commute)
    1.74 +qed
    1.75 +
    1.76 +lemma choose_mult:
    1.77 +  assumes "k\<le>m" "m\<le>n"
    1.78 +    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
    1.79 +using assms choose_mult_lemma [of "m-k" "n-m" k]
    1.80 +by simp
    1.81  
    1.82  
    1.83  subsection {* Binomial coefficients *}