summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 17 Oct 2013 16:45:54 +0200 | |

changeset 54136 | c206cb2a3afe |

parent 54135 | 0d5ed72c4c60 |

child 54137 | e475d86ab2ca |

more exercises

--- 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