header {* Binary Search Trees *}
(*<*)theory Tree_ex imports Main
begin
(*>*)
subsection {* Preliminaries *}
text{*
We begin by declaring a binary tree with labelled nodes.
*}
datatype tree = Lf | Br int tree tree
text{*
A \emph{binary search tree} is a binary tree
with an ordering constraint: at every node, the label is
greater than every label in the left subtree, and smaller than
every label in the right subtree (both inequalities strict).
*}
text{*
The @{term"update"} operation for a binary search tree can be declared as follows.
Note the use of the ordering constraint to recursively update the correct
subtree.
*}
fun update :: "tree => int => tree"
where
"update Lf v = Br v Lf Lf"
| "update (Br w t1 t2) v =
(if v int => bool"
labels :: "tree => int set"
ordered :: "tree => bool"
(*>*)
text {*\begin{task}
Define an Isabelle function @{term"lookup"} of type @{typ"tree => int => bool"},
so as to return @{term True} if a given label occurs in a binary search tree.
It should take advantage of the ordering constraint analogously to @{term"update"}.
\marks{4}
\end{task}
*}
text {*\begin{task}
Define an Isabelle function @{term"labels"} of type @{typ"tree => int set"},
to return the set of labels in a binary tree.
Also define an Isabelle function @{term"ordered"} of type @{typ"tree => bool"},
specifying the ordering constraint for binary search trees.
\marks{6}
\end{task}
*}
text {*\begin{task}
Prove the following theorems.\marks{15}
\end{task}
*}
lemma labels_update: "labels (update t v) = {v} \ labels t"
(*<*) oops (*>*)
lemma ordered_update: "ordered (update t v) \ ordered t"
(*<*) oops (*>*)
lemma ordered_lookup: "ordered t \ lookup t v \ v \ labels t"
(*<*) oops (*>*)
lemma lookup_update:
"ordered t \ lookup (update t v) w = (v=w \ lookup t w)"
(*<*) oops (*>*)
subsection {* Additional Functions on Trees *}
text {*
The remainder of this exercise involves the function @{term"gax"}:
*}
fun gax :: "tree => tree => tree"
where
"gax Lf t = t"
| "gax (Br v t1 t2) t = gax t1 (gax t2 (update t v))"
text {*\begin{task}
Prove the following theorems, first replacing the function @{term f} in the first
one by something more appropriate. Thus explain what @{term"gax"} actually does.
\marks{10}
\end{task}
*}
lemma labels_gax: "labels (gax t1 t2) = f (labels t1, labels t2)"
(*<*) oops (*>*)
lemma ordered_gax: "ordered (gax t1 t2) = ordered t2"
(*<*) oops (*>*)
text {*\begin{task}
Define an Isabelle function @{term"delete"} of type @{typ"tree => int => tree"},
to delete a label from a binary tree. (\emph{Hint}: you may find the function @{term"gax"} helpful.)
Then, prove the following theorems.
\marks{15}
\end{task}
*}
lemma labels_delete:
"ordered t \ labels (delete t v) = labels t - {v}"
(*<*) oops (*>*)
lemma ordered_delete: "ordered t \ ordered (delete t v)"
(*<*) oops (*>*)
text{*
\emph{Note}: If your solution generalises the type of trees to be polymorphic,
rather than having integer labels, then you will gain 5--10 marks in the
category of ``expertise''. This generalisation requires the use of an appropriate axiomatic type class.
*}
text {*
\newpage*}
(*<*) end (*>*)