src/HOL/Binomial.thy

--- 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)"