--- a/src/HOL/Binomial.thy Mon Jul 04 19:46:19 2016 +0200
+++ b/src/HOL/Binomial.thy Mon Jul 04 19:46:19 2016 +0200
@@ -6,7 +6,7 @@
Additional binomial identities by Chaitanya Mangla and Manuel Eberl
*)
-section\<open>Factorial Function, Binomial Coefficients and Binomial Theorem\<close>
+section \<open>Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\<close>
theory Binomial
imports Main
@@ -170,7 +170,8 @@
text \<open>This development is based on the work of Andy Gordon and
Florian Kammueller.\<close>
-subsection \<open>Basic definitions and lemmas\<close>
+
+subsection \<open>Binomial coefficients\<close>
text \<open>Combinatorial definition\<close>
@@ -471,7 +472,8 @@
finally show ?thesis .
qed
-subsection\<open>Pochhammer's symbol : generalized rising factorial\<close>
+
+subsection \<open>Pochhammer's symbol : generalized rising factorial\<close>
text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
@@ -1136,7 +1138,7 @@
thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)
qed auto
-subsection \<open>Summation on the upper index\<close>
+subsubsection \<open>Summation on the upper index\<close>
text \<open>
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
@@ -1383,7 +1385,7 @@
by simp
-subsection \<open>Binomial coefficients\<close>
+subsection \<open>More on Binomial Coefficients\<close>
lemma choose_one: "(n::nat) choose 1 = n"
by simp
@@ -1585,6 +1587,9 @@
(simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
qed
+
+subsection \<open>Misc\<close>
+
lemma fact_code [code]:
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a :: semiring_char_0)"
proof -
@@ -1600,7 +1605,6 @@
"setprod f {..<Suc n} = fold_atLeastAtMost_nat (times \<circ> f) 0 n 1"
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setprod_atLeastAtMost_code comp_def)
-
lemma pochhammer_code [code]:
"pochhammer a n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"