header {* Assessed Exercise II: Binomial Coefficients*}
(*<*)
theory Binomial_ex
imports "~~/src/HOL/Number_Theory/Fib"
begin
(*>*)
text{*The binomial coefficients arise in the binomial theorem.
They are the elements of Pascal's triangle and satisfy a great many mathematical identities.
The theory @{text "HOL/Number_Theory/Binomial"}
contains basic definitions and proofs.
Information about binomial coefficients. is widely available on the Internet,
including the lecture course notes available here:
@{text "http://www.cs.columbia.edu/~cs4205/files/CM4.pdf"}
\begin{task}
Prove the following theorem about binomial coefficients.
(Note that @{text"0 - 1 = 0"} on the natural numbers.)\marks{5}
\end{task}
*}
lemma times_binomial:
"Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
(*<*) oops (*>*)
text {*\begin{task}
Prove the following theorem, which relates to a weighted sum of a row of Pascal's triangle.
(It involves arithmetic on type @{typ real} as well as @{typ nat}, so the function @{const real}
is implicitly inserted at multiple points.)\marks{15}
\end{task}
*}
lemma choose_row_sum:
"(\k = 0..m. (r choose k) * (r/2 - k)) =
(Suc m) /2 * (r choose (Suc m))"
(*<*) oops (*>*)
text {*\begin{task}
Prove the following lemma, which will be useful below.\marks{10}
\end{task}
*}
lemma setsum_choose_drop_zero:
"(\k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) =
(\j = 0..n. (n-j) choose j)"
(*<*) oops (*>*)
text {*\begin{task}
Prove the following theorem, which relates binomial coefficients with Fibonacci numbers.\marks{20}
\end{task}
*}
lemma ne_diagonal_fib:
"(\k = 0..n. (n-k) choose k) = fib (Suc n)"
(*<*) oops (*>*)
text {*
\bigskip\emph{Remark}: as in Assessed Exercise I, choose your induction rule with care in each proof.
The precise statement of the induction formula is also important.
Some of the proofs are best done using calculational reasoning.
*}
text{*\checkmarks*}
(*<*)
end
(*>*)