# HG changeset patch
# User nipkow
# Date 1382555540 -7200
# Node ID 1e685123926d8be15a3b1e11fde6552854dfdd93
# Parent  12c9ad3142beb174e0728d2654820dfd2d69d792
more exercises

diff -r 12c9ad3142be -r 1e685123926d src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Wed Oct 23 18:04:43 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Wed Oct 23 21:12:20 2013 +0200
@@ -525,6 +525,31 @@
 
 \subsection{Exercises}
 
+\exercise\label{exe:tree0}
+Define a datatype @{text tree0} of binary tree skeletons which do not store
+any information, neither in the inner nodes nor in the leaves.
+Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the total number
+all nodes (inner nodes and leaves) in such a tree.
+Consider the following recursive function:
+*}
+(*<*)
+datatype tree0 = Tip | Node tree0 tree0
+(*>*)
+fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where
+"explode 0 t = t" |
+"explode (Suc n) t = explode n (Node t t)"
+
+text {*
+Find an equation expressing the size of a tree after exploding it
+(\noquotes{@{term [source] "nodes (explode n t)"}}) as a function
+of @{term "nodes t"} and @{text n}. Prove your equation.
+You may use the usual arithmetic operators including the exponentiation
+operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}.
+
+Hint: simplifying with the list of theorems @{thm[source] algebra_simps}
+takes care of common algebraic properties of the arithmetic operators.
+\endexercise
+
 \exercise
 Define arithmetic expressions in one variable over integers (type @{typ int})
 as a data type:
@@ -546,8 +571,7 @@
 that transforms an expression into a polynomial. This may require auxiliary
 functions. Prove that @{text coeffs} preserves the value of the expression:
 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.}
-Hint: simplifying with @{thm[source] algebra_simps} takes care of
-common algebraic properties of @{text "+"} and @{text "*"}.
+Hint: consider the hint in \autoref{exe:tree0}.
 \endexercise
 *}
 (*<*)