header {* Assessed Exercise II: \\ Properties of Binomial Coefficients*}

(*<*)
theory Binomial_ex
imports "~~/src/HOL/Library/Binomial"
begin

declare binomial_eq_0_iff [simp]
declare zero_less_binomial_iff [simp]
(*>*)

text{*The binomial coefficients arise in the binomial theorem. 
They are the elements of Pascal's triangle and satisfy a great many mathematical identities. 
Below, we examine some of these. The theory @{text "HOL/Library/Binomial"}
contains basic definitions and proofs, including the binomial theorem itself: 

@{thm[display]binomial[no_vars]} 

Many textbooks on discrete mathematics cover binomial coefficients.
Information about them is widely available on the Internet, 
including Wikipedia and the lecture course notes available here:

@{text "http://www.cs.columbia.edu/~cs4205/files/CM4.pdf"}

\begin{task} Prove the following theorem. 
Hint: it follows from the binomial theorem, 
which is available under the name @{thm[source]binomial}.
\marks{4}
\end{task} 
*}
lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
(*<*)oops(*>*)  

text{*\begin{task} Prove the following two theorems, which concern 
sums of binomial coefficients. 
\marks{4}
\end{task} 
*}
lemma sum_choose_lower: 
    "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
(*<*)oops(*>*)  

lemma sum_choose_upper: 
    "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
(*<*)oops(*>*)  

text{*The built-in theorem @{thm[source]setsum_reindex_cong} allows a summation to be re-indexed
by any injective function. (The notion of set image is also used.)
@{thm[display]setsum_reindex_cong[no_vars]} 

\begin{task} Prove the following corollary of @{thm[source]setsum_reindex_cong}, 
which allows the indexes of a summation to be reversed.\marks{5}
\end{task} 
*}
corollary natsum_reverse_index:
  fixes m::nat
  assumes "\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)"
  shows "(\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
(*<*)oops(*>*)  

text{*\begin{task} Prove the following identity. In addition to the re-indexing result just proved, 
you will need another of the identities proved above.\marks{10}
\end{task} 
*}
lemma sum_choose_diagonal:
  assumes "m\<le>n" 
    shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
(*<*)oops(*>*)  

text{*The identity $\binom{n}{m} \binom{m}{k} = \binom{n}{k} \binom{n-k}{m-k}$ is straightforward. 
But the need to show the necessary divisibility properties complicates the Isabelle proof.
The key result we need is already available as @{thm[source]binomial_fact_lemma}:
@{thm[display]binomial_fact_lemma[no_vars]} 
\begin{task} 
Using it, prove the following divisibility property.\marks{5}
\end{task} 
*}
lemma fact_fact_dvd_fact: 
    fixes k::nat 
    shows "fact k * fact n dvd fact (n + k)"
(*<*)oops(*>*)  

text{*Now the identity $\binom{n}{m} \binom{m}{k} = \binom{n}{k} \binom{n-k}{m-k}$ can be
proved by expressing binomial coefficients in terms of factorials:
@{thm[display]binomial_altdef_nat[no_vars]} 
Common factors are then cancelled using the result just proved
along with the lemma  @{thm[source]div_mult_div_if_dvd}:
@{thm[display]div_mult_div_if_dvd[no_vars]} 
The equational calculation is still short, but each step requires some justification.
\begin{task} 
Prove the identity, expressed as shown below.\marks{18}
\end{task} 
*}
lemma choose_mult_p1:
     "((m+r+k) choose (m+k)) * ((m+k) choose k) = 
      ((m+r+k) choose k) * ((m+r) choose m)"
(*<*)oops(*>*)  

text{*\begin{task} 
The formulation given above uses addition instead of subtraction, 
which tends to complicate proofs about the natural numbers. 
Now that the hard work has been done, establish the identity in its conventional form.\marks{4}
\end{task} 
*}
lemma choose_mult:
  assumes "k\<le>m" "m\<le>n"
    shows "(n choose m) * (m choose k) = 
           (n choose k) * ((n-k) choose (m-k))"
(*<*)oops(*>*)  

text{*\checkmarks*}
(*<*)
end
(*>*)