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 \<Rightarrow> nat \<Rightarrow> nat" where
  "S p n \<equiv> \<Sum>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 \<Longrightarrow> 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\<Colon>comm_ring list \<Rightarrow> 'a\<Colon>comm_ring \<Rightarrow> 'a\<Colon>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\<Colon>comm_ring list \<Rightarrow> 'a\<Colon>comm_ring list \<Rightarrow> 'a\<Colon>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\<Colon>comm_ring list \<Rightarrow> 'a\<Colon>comm_ring list \<Rightarrow> 'a\<Colon>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(*>*)