add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
authorhoelzl
Tue Nov 27 10:56:31 2012 +0100 (2012-11-27)
changeset 50240019d642d422d
parent 50239 fb579401dc26
child 50241 8b0fdeeefef7
child 50243 0d97ef1d6de9
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
src/HOL/Fact.thy
src/HOL/Library/Binomial.thy
     1.1 --- a/src/HOL/Fact.thy	Mon Nov 26 21:46:04 2012 +0100
     1.2 +++ b/src/HOL/Fact.thy	Tue Nov 27 10:56:31 2012 +0100
     1.3 @@ -315,4 +315,13 @@
     1.4      by (auto simp: image_iff)
     1.5  qed (auto intro: inj_onI)
     1.6  
     1.7 +lemma fact_div_fact_le_pow:
     1.8 +  assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
     1.9 +proof -
    1.10 +  have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
    1.11 +    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
    1.12 +  with assms show ?thesis
    1.13 +    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
    1.14 +qed
    1.15 +
    1.16  end
     2.1 --- a/src/HOL/Library/Binomial.thy	Mon Nov 26 21:46:04 2012 +0100
     2.2 +++ b/src/HOL/Library/Binomial.thy	Tue Nov 27 10:56:31 2012 +0100
     2.3 @@ -575,4 +575,16 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma binomial_le_pow:
     2.8 +  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
     2.9 +proof -
    2.10 +  have "n choose r \<le> fact n div fact (n - r)"
    2.11 +    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
    2.12 +  with fact_div_fact_le_pow[OF assms] show ?thesis by auto
    2.13 +qed
    2.14 +
    2.15 +lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
    2.16 +    n choose k = fact n div (fact k * fact (n - k))"
    2.17 + by (subst binomial_fact_lemma[symmetric]) auto
    2.18 +
    2.19  end