add lemmas
authornoschinl
Mon Dec 19 14:41:08 2011 +0100 (2011-12-19)
changeset 45933ee70da42e08a
parent 45932 6f08f8fe9752
child 45934 9321cd2572fe
add lemmas
src/HOL/Nat.thy
src/HOL/Number_Theory/Binomial.thy
     1.1 --- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -1615,6 +1615,9 @@
     1.4  lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
     1.5  by arith
     1.6  
     1.7 +lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
     1.8 +by simp
     1.9 +
    1.10  text{*Lemmas for ex/Factorization*}
    1.11  
    1.12  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
     2.1 --- a/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
     2.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Dec 19 14:41:08 2011 +0100
     2.3 @@ -349,4 +349,17 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +lemma choose_le_pow:
     2.8 +  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
     2.9 +proof -
    2.10 +  have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
    2.11 +    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
    2.12 +  have "n choose r \<le> fact n div fact (n - r)"
    2.13 +    using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2)
    2.14 +  also have "\<dots> \<le> n ^ r" using `r \<le> n`
    2.15 +    by (induct r rule: nat.induct)
    2.16 +     (auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono)
    2.17 + finally show ?thesis .
    2.18 +qed
    2.19 +
    2.20  end