more exercises
Tue, 29 Oct 2013 08:06:08 +0100
changeset 54214 6d0688ce4ee2
parent 54213 cd5ef8bb9d59
child 54215 ab0595cb9fe9
more exercises
--- 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}.
+Start from the data type of binary trees defined earlier:
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
+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)"}.
 \section{Proof Automation}
 So far we have only seen @{text simp} and @{text auto}: Both perform