# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1424451565 0
# Node ID efd44495ecf8555936184c63722f8b31968ee6b5
# Parent  35da1bbf234ee84903a3b73e30103f1d6549e48c
generalised the results by Eberl

diff -r 35da1bbf234e -r efd44495ecf8 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Thu Feb 19 16:32:53 2015 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Fri Feb 20 16:59:25 2015 +0000
@@ -566,53 +566,67 @@
   then show ?thesis using kn by simp
 qed
 
-(* Contributed by Manuel Eberl *)
-(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *)
+text{*Contributed by Manuel Eberl, generalised by LCP.
+  Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
+lemma gbinomial_altdef_of_nat:
+  fixes k :: nat
+    and x :: "'a :: {field_char_0,field_inverse_zero}"
+  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
+proof -
+  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
+    unfolding gbinomial_def
+    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
+  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
+    unfolding fact_eq_rev_setprod_nat of_nat_setprod
+    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
+  finally show ?thesis .
+qed
+
+lemma gbinomial_ge_n_over_k_pow_k:
+  fixes k :: nat
+    and x :: "'a :: linordered_field_inverse_zero"
+  assumes "of_nat k \<le> x"
+  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
+proof -
+  have x: "0 \<le> x"
+    using assms of_nat_0_le_iff order_trans by blast
+  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
+    by (simp add: setprod_constant)
+  also have "\<dots> \<le> x gchoose k"
+    unfolding gbinomial_altdef_of_nat
+  proof (safe intro!: setprod_mono)
+    fix i :: nat
+    assume ik: "i < k"
+    from assms have "x * of_nat i \<ge> of_nat (i * k)"
+      by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
+    then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith
+    then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
+      using ik 
+      by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)
+    then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
+      unfolding of_nat_mult[symmetric] of_nat_le_iff .
+    with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"
+      using `i < k` by (simp add: field_simps)
+  qed (simp add: x zero_le_divide_iff)
+  finally show ?thesis .
+qed
+
+text{*Versions of the theorems above for the natural-number version of "choose"*}
 lemma binomial_altdef_of_nat:
   fixes n k :: nat
-    and x :: "'a :: {field_char_0,field_inverse_zero}"
+    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}}*}
   assumes "k \<le> n"
   shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
-proof (cases "0 < k")
-  case True
-  then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n - of_nat i) / of_nat (fact k)"
-    unfolding binomial_gbinomial gbinomial_def
-    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
-  also have "\<dots> = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
-    using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod
-    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
-  finally show ?thesis .
-next
-  case False
-  then show ?thesis by simp
-qed
+using assms
+by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
 
 lemma binomial_ge_n_over_k_pow_k:
   fixes k n :: nat
     and x :: "'a :: linordered_field_inverse_zero"
-  assumes "0 < k"
-    and "k \<le> n"
+  assumes "k \<le> n"
   shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
-proof -
-  have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)"
-    by (simp add: setprod_constant)
-  also have "\<dots> \<le> of_nat (n choose k)"
-    unfolding binomial_altdef_of_nat[OF `k\<le>n`]
-  proof (safe intro!: setprod_mono)
-    fix i :: nat
-    assume  "i < k"
-    from assms have "n * i \<ge> i * k" by simp
-    then have "n * k - n * i \<le> n * k - i * k" by arith
-    then have "n * (k - i) \<le> (n - i) * k"
-      by (simp add: diff_mult_distrib2 mult.commute)
-    then have "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)"
-      unfolding of_nat_mult[symmetric] of_nat_le_iff .
-    with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)"
-      using `i < k` by (simp add: field_simps)
-  qed (simp add: zero_le_divide_iff)
-  finally show ?thesis .
-qed
-
+by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)  
+  
 lemma binomial_le_pow:
   assumes "r \<le> n"
   shows "n choose r \<le> n ^ r"