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(*>*)