--- a/src/Doc/ProgProve/Types_and_funs.thy Thu Oct 17 13:37:13 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy Thu Oct 17 16:45:54 2013 +0200
@@ -156,7 +156,7 @@
fun div2 :: "nat \<Rightarrow> nat" where
"div2 0 = 0" |
-"div2 (Suc 0) = Suc 0" |
+"div2 (Suc 0) = 0" |
"div2 (Suc(Suc n)) = Suc(div2 n)"
text{* does not just define @{const div2} but also proves a
@@ -200,6 +200,15 @@
But note that the induction rule does not mention @{text f} at all,
except in its name, and is applicable independently of @{text f}.
+
+\subsection{Exercises}
+
+\begin{exercise}
+Prove that @{const div2} defined above divides every number by @{text 2},
+not just those of the form @{text"n+n"}: @{prop "div2 n = n div 2"}.
+\end{exercise}
+
+
\section{Induction Heuristics}
We have already noted that theorems about recursive functions are proved by
@@ -307,6 +316,18 @@
matters in some cases. The variables that need to be quantified are typically
those that change in recursive calls.
+
+\subsection{Exercises}
+
+\begin{exercise}
+Write a tail-recursive variant of the @{text add} function on @{typ nat}:
+@{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}.
+Tail-recursive means that in the recursive case, @{text itadd} needs to call
+itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}.
+Prove @{prop "itadd m n = add m n"}.
+\end{exercise}
+
+
\section{Simplification}
So far we have talked a lot about simplifying terms without explaining the concept. \concept{Simplification} means