header {* Sums of Powers, Polynomials *}
(*<*)theory Exercises3 imports Main begin(*>*)
text {*
This assignment \emph{will be assessed} to determine 50\% of your
final mark. Please complete the indicated tasks and write a brief
document explaining your work. You may prepare this document using
Isabelle's theory presentation facility, but this is not required. (A
very simple way to print a theory file legibly is to use the Proof
General command Isabelle~$>$ Commands~$>$ Display draft. You can
combine the resulting output with a document produced using your
favourite word processing package.) A clear write-up describing
elegant, clearly structured proofs of all tasks will receive maximum
credit.
You must work on this assignment as an individual. Collaboration is
not permitted.
*}
subsection {* Sums of Powers *}
text {*
We consider sums of consecutive powers: $S_p(n) = \sum_{k=1}^n{k^p}$.
$\rhd$ Define a corresponding function @{term "S p n"}.
*}
(*<*)consts(*>*) S :: "nat \ nat \ nat"
text {*
Hint: exponentiation and summation functions are already available in
Isabelle/HOL.
\medskip
Clearly, $S_0(n) = n$. It is also well-known that $S_1(n) = \frac{n^2
+ n}{2}$.
$\rhd$ Prove these identities.
*}
lemma "S 0 n = n"
(*<*)oops(*>*)
lemma(*<*)gauss:(*>*) "2 * S 1 n = n^2 + n"
(*<*)oops(*>*)
text {*
At this point, we might suspect that $S_p(n)$ is a polynomial in~$n$
with rational coefficients.
$\rhd$ Verify this conjecture for $p=2$, i.e., find $k > 0$ and a
polynomial $\mathit{poly}$ in~$n$ so that $k \cdot S_2(n) =
\mathit{poly}$. Prove the resulting identity.
*}
lemma "k * S 2 n = poly" -- {* replace @{term k} and @{term poly} *}
(*<*)oops(*>*)
text {*
Hint: useful simplification rules for addition and multiplication are
available as @{text "algebra_simps"}. The \emph{Find theorems} command
can be used to discover further lemmas.
\medskip
\begin{figure}[t]
\includegraphics[width=\textwidth]{CubeSquare_600}
\caption{Visualization of Nicomachus's theorem}
\end{figure}
For $p=3$, our conjecture follows from the astonishing identity
$\sum_{k=1}^n{k^3} = (\sum_{k=1}^n{k})^2$, which is known as
\emph{Nicomachus's theorem}.
$\rhd$ Prove Nicomachus's theorem.
*}
theorem "S 3 n = (S 1 n)^2"
(*<*)oops(*>*)
text {*
Before we could prove our conjecture for arbitrary~$p$ (which we will
not do as part of this assignment, but search for \emph{Faulhaber's
formula} if you want to know more), we need to define polynomials.
*}
subsection {* Polynomials *}
text {*
A polynomial in one variable can be given by the list of its
coefficients: e.g., $[0, \frac{1}{6}, \frac{1}{3}, \frac{1}{2}]$
represents the polynomial $\frac{1}{2}x^3 + \frac{1}{3}x^2 +
\frac{1}{6}x + 0$. (We list coefficients in reverse order, i.e., from
lower to higher degree.)
Coefficients may be integers, rationals, reals, etc. In general, we
require coefficients to be elements of a commutative ring (cf.\ @{text
Rings.thy}).
To every polynomial in one variable we can associate a
\emph{polynomial function} on the ring of coefficients. This
function's value is obtained by substituting its argument for the
polynomial's variable, i.e., by evaluating the polynomial.
$\rhd$ Define a function @{term "poly cs x"} so that $\mathit{poly}\
[c_0, c_1, \dots, c_n]\ x = c_n\underbrace{x\cdot\dots\cdot
x}_{\small \mbox{$n$ factors}} + \dots + c_1x + c_0$.
*}
(*<*)consts(*>*) poly :: "'a\comm_ring list \ 'a\comm_ring \ 'a\comm_ring"
text {*
$\rhd$ Define a function @{term "poly_plus p q"} that computes the sum
of two polynomials.
*}
(*<*)consts(*>*) poly_plus :: "'a\comm_ring list \ 'a\comm_ring list \ 'a\comm_ring list"
text {*
$\rhd$ Prove correctness of @{term poly_plus}.
*}
lemma "poly (poly_plus p q) x = poly p x + poly q x"
(*<*)oops(*>*)
text {*
Hint: Isabelle provides customized induction rules for recursive
functions, e.g., @{text poly_plus.induct}. See the \emph{Tutorial on
Function Definitions} for details.
\medskip
$\rhd$ Define a function @{term "poly_times p q"} that computes the
product of two polynomials.
*}
(*<*)consts(*>*) poly_times :: "'a\comm_ring list \ 'a\comm_ring list \ 'a\comm_ring list"
text {*
$\rhd$ Prove correctness of @{term poly_times}.
*}
lemma "poly (poly_times p q) x = poly p x * poly q x"
(*<*)oops(*>*)
(*<*)end(*>*)