theory hw01_tmpl
imports Main
begin
***
First, rename this file to FirstnameLastname.thy (insert your name!),
and replace the "theory hw01_tmpl" header by "theory FirstnameLastname"!
Then, comment out/erase this lines to make the theory compile!
***
(* This is an informal comment. It may contain everything. *)
text \This is a formal text comment. It should be valid LaTeX.\
-- \This is a formal text comment bound to the command before it.
It should be valid LaTeX.\
fun snoc :: "'a list \ 'a \ 'a list" where
"snoc [] x = [x]" |
"snoc (y # ys) x = y # (snoc ys x)"
fun reverse :: "'a list \ 'a list" where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x"
text \
Mail a theory file named FirstnameLastname01.thy (replace with your name!) which runs in Isabelle-2015 {\bfseries without errors} to \emph{lammichatindottumdotde}.
General hints:
\begin{itemize}
\item If you cannot prove a lemma, that you need for a subsequent
proof, assume this lemma by using sorry.
\item Define the functions as simple as possible.
In particular, do not try to make them tail recursive by
introducing extra accumulator parameters --- this will
complicate the proofs!
\item Nitpick, Quickcheck, and Sledgehammer are your friends!
\item All proofs should be straightforward, and take only a few
lines.
\end{itemize}
Define a function that adds up the elements of a list:
\
fun lsum :: "nat list \ nat" where
"lsum [] = undefined"
| "lsum (x#xs) = undefined"
-- \Replace undefined by your definition!\
text \Prove that reversing the list does not affect its sum.\
lemma "lsum (reverse xs) = lsum xs" oops
-- \Replace oops by your proof!\
text \Hint: Induction. You may need an auxiliary lemma about
@{const lsum} and @{const snoc}.\
text \Write a function that, for argument $n$
generates the list $[1..n]$:\
fun nlist :: "nat \ nat list" where
"nlist 0 = undefined"
| "nlist (Suc n) = undefined"
-- \Replace undefined by your definition!\
text \Prove the well-known Gauss-formula: \
lemma "lsum (nlist n) = n * (n+1) div 2" oops
-- \Replace oops by your proof!\
end