# HG changeset patch
# User nipkow
# Date 1382544283 -7200
# Node ID 12c9ad3142beb174e0728d2654820dfd2d69d792
# Parent  bc07627c5dcdfc4a72ddb7c48262b04430210bee
added exercises

diff -r bc07627c5dcd -r 12c9ad3142be src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Wed Oct 23 14:53:36 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Wed Oct 23 18:04:43 2013 +0200
@@ -204,6 +204,25 @@
 \subsection{Exercises}
 
 \begin{exercise}
+Starting from the type @{text "'a tree"} defined in the text, define
+a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}
+that collects all values in a tree in a list, in any order,
+without removing duplicates.
+Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}
+that sums up all values in a tree of natural numbers
+and prove @{prop "treesum t = listsum(contents t)"}.
+\end{exercise}
+
+\begin{exercise}
+Define a new type @{text "'a tree2"} of binary trees where values are also
+stored in the leaves of the tree.  Also reformulate the
+@{const mirror} function accordingly. Define two functions
+@{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"}
+that traverse a tree and collect all stored values in the respective order in
+a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}.
+\end{exercise}
+
+\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}