relating gbinomial and binomial, still using distinct definitions

--- a/src/HOL/Binomial.thy	Mon Jul 04 19:08:54 2016 +0200
+++ b/src/HOL/Binomial.thy	Mon Jul 04 19:46:19 2016 +0200
@@ -394,6 +394,12 @@
   ultimately show ?ths by blast
 qed
 
+lemma binomial_fact':
+  assumes "k \<le> n"
+  shows "n choose k = fact n div (fact k * fact (n - k))"
+  using binomial_fact_lemma [OF assms]
+  by (metis fact_nonzero mult_eq_0_iff nonzero_mult_divide_cancel_left)
+
 lemma binomial_fact:
   assumes kn: "k \<le> n"
   shows "(of_nat (n choose k) :: 'a::field_char_0) =
@@ -675,20 +681,24 @@
 qed
 
 
-subsection\<open>Generalized binomial coefficients\<close>
+subsection \<open>Generalized binomial coefficients\<close>
 
-definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a :: {semidom_divide, semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
 where
-  "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} / fact n"
+  "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} div fact n"
 
 lemma gbinomial_Suc:
   "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {..k} / fact (Suc k)"
   by (simp add: gbinomial_def lessThan_Suc_atMost)
 
-lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
+lemma gbinomial_0 [simp]:
+  fixes a :: "'a::field_char_0"
+  shows "a gchoose 0 = 1" "(0::'a) gchoose (Suc n) = 0"
   by (simp_all add: gbinomial_def)
 
-lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
+lemma gbinomial_pochhammer:
+  fixes a :: "'a::field_char_0"
+  shows "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
 proof (cases "n = 0")
   case True
   then show ?thesis by simp
@@ -710,6 +720,32 @@
   finally show ?thesis by simp
 qed
 
+lemma gbinomial_binomial:
+  "n gchoose k = n choose k"
+proof (cases "k \<le> n")
+  case False
+  then have "n < k" by (simp add: not_le)
+  then have "0 \<in> (op - n) ` {..<k}"
+    by auto
+  then have "setprod (op - n) {..<k} = 0"
+    by (auto intro: setprod_zero)
+  with \<open>n < k\<close> show ?thesis
+    by (simp add: binomial_eq_0 gbinomial_def setprod_zero)
+next
+  case True
+  then have "inj_on (op - n) {..<k}"
+    by (auto intro: inj_onI)
+  then have "\<Prod>(op - n ` {..<k}) = setprod (op - n) {..<k}"
+    by (auto dest: setprod.reindex)
+  also have "op - n ` {..<k} = {Suc (n - k)..n}"
+    using True by (auto simp add: image_def Bex_def) arith
+  finally have *: "setprod (\<lambda>q. n - q) {..<k} = \<Prod>{Suc (n - k)..n}" ..
+  from True have "(n choose k) = fact n div (fact k * fact (n - k))"
+    by (rule binomial_fact')
+  with * show ?thesis
+    by (simp add: gbinomial_def mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+qed
+
 lemma binomial_gbinomial:
     "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
 proof -
@@ -752,6 +788,8 @@
   ultimately show ?thesis by blast
 qed
 
+setup \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
+
 lemma gbinomial_1[simp]: "a gchoose 1 = a"
   by (simp add: gbinomial_def lessThan_Suc)