# HG changeset patch
# User hoelzl
# Date 1354010191 -3600
# Node ID 019d642d422d2bc796bb373d2c72e44235948516
# Parent  fb579401dc261b167da4d8585bae219d457c97e1
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)

diff -r fb579401dc26 -r 019d642d422d src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Mon Nov 26 21:46:04 2012 +0100
+++ b/src/HOL/Fact.thy	Tue Nov 27 10:56:31 2012 +0100
@@ -315,4 +315,13 @@
     by (auto simp: image_iff)
 qed (auto intro: inj_onI)
 
+lemma fact_div_fact_le_pow:
+  assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
+proof -
+  have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
+    by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
+  with assms show ?thesis
+    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
+qed
+
 end
diff -r fb579401dc26 -r 019d642d422d src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Nov 26 21:46:04 2012 +0100
+++ b/src/HOL/Library/Binomial.thy	Tue Nov 27 10:56:31 2012 +0100
@@ -575,4 +575,16 @@
   finally show ?thesis .
 qed
 
+lemma binomial_le_pow:
+  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
+proof -
+  have "n choose r \<le> fact n div fact (n - r)"
+    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
+  with fact_div_fact_le_pow[OF assms] show ?thesis by auto
+qed
+
+lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
+    n choose k = fact n div (fact k * fact (n - k))"
+ by (subst binomial_fact_lemma[symmetric]) auto
+
 end