# HG changeset patch
# User nipkow
# Date 1383030368 -3600
# Node ID 6d0688ce4ee2d106861c792e4ed66def6992d7e1
# Parent  cd5ef8bb9d5932347dc5e0a270c5c0bb282beb45
more exercises

diff -r cd5ef8bb9d59 -r 6d0688ce4ee2 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Mon Oct 28 10:29:56 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Tue Oct 29 08:06:08 2013 +0100
@@ -141,6 +141,28 @@
 See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
 @{theory Main}.
 
+
+\subsection{Exercises}
+
+\exercise
+Start from the data type of binary trees defined earlier:
+*}
+
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
+
+text{*
+Define a function @{text "set ::"} @{typ "'a tree \<Rightarrow> 'a set"}
+that returns the elements in a tree and a function
+@{text "ord ::"} @{typ "int tree \<Rightarrow> bool"}
+the tests if an @{typ "int tree"} is ordered.
+
+Define a function @{text ins} that inserts an element into an ordered @{typ "int tree"}
+while maintaining the order of the tree. If the element is already in the tree, the
+same tree should be returned. Prove correctness of @{text ins}:
+@{prop "set(ins x t) = {x} \<union> set t"} and @{prop "ord t \<Longrightarrow> ord(ins i t)"}.
+\endexercise
+
+
 \section{Proof Automation}
 
 So far we have only seen @{text simp} and @{text auto}: Both perform