header {* Sums of Powers, Polynomials *}
(*<*)theory Solution3 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"}.
*}
definition S :: "nat \ nat \ nat" where
"S p n \ \k=1..n. k^p"
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"
by (simp add: S_def)
lemma(*<*)gauss:(*>*) "2 * S 1 n = n^2 + n"
by (induct n) (auto simp add: S_def power2_eq_square)
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 "6 * S 2 n = 2*n^3 + 3*n^2 + n" -- {* replace @{term k} and @{term poly} *}
by (induct n) (auto simp add: S_def algebra_simps power2_eq_square power3_eq_cube)
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.
*}
lemma l1: "4 * S 3 n = (n^2 + n)^2"
by (induct n) (auto simp add: S_def algebra_simps power2_eq_square power3_eq_cube)
lemma l2: "4 * (m::nat) = (2 * n)^2 \ m = n^2"
by (simp add: power2_eq_square)
theorem "S 3 n = (S 1 n)^2"
by (simp only: l1 l2 gauss)
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$.
*}
fun poly :: "'a\comm_ring list \ 'a\comm_ring \ 'a\comm_ring" where
"poly [] _ = 0"
| "poly (c#cs) x = c + x * poly cs x"
text {*
$\rhd$ Define a function @{term "poly_plus p q"} that computes the sum
of two polynomials.
*}
fun poly_plus :: "'a\comm_ring list \ 'a\comm_ring list \ 'a\comm_ring list" where
"poly_plus p [] = p"
| "poly_plus [] q = q"
| "poly_plus (p#ps) (q#qs) = (p + q) # poly_plus ps qs"
text {*
$\rhd$ Prove correctness of @{term poly_plus}.
*}
lemma poly_plus_correct: "poly (poly_plus p q) x = poly p x + poly q x"
by (induct p q rule: poly_plus.induct) (auto simp add: algebra_simps)
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.
*}
fun poly_times :: "'a\comm_ring list \ 'a\comm_ring list \ 'a\comm_ring list" where
"poly_times [] _ = []"
| "poly_times (p#ps) q = poly_plus (map (op * p) q) (poly_times ps (0 # q))"
text {*
$\rhd$ Prove correctness of @{term poly_times}.
*}
lemma poly_map_times: "poly (map (op * c) p) x = c * poly p x"
by (induct p) (auto simp add: algebra_simps)
lemma "poly (poly_times p q) x = poly p x * poly q x"
by (induct p q rule: poly_times.induct) (auto simp add: algebra_simps poly_plus_correct poly_map_times)
(*<*)end(*>*)