author haftmann Mon, 04 Jul 2016 19:46:19 +0200 changeset 63373 487d764fca4a parent 63372 492b49535094 child 63374 1a474286f315
tuned sections
 src/HOL/Binomial.thy file | annotate | diff | comparison | revisions
--- 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)"