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<w then  Br w (update t1 v)  t2
       else
       if w<v then  Br w  t1  (update t2 v)
       else  Br v t1 t2)"
       
(*<*)
consts lookup :: "tree => 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} \<union> labels t"
(*<*) oops (*>*)

lemma ordered_update: "ordered (update t v) \<longleftrightarrow> ordered t"
(*<*) oops (*>*)

lemma ordered_lookup: "ordered t \<Longrightarrow> lookup t v \<longleftrightarrow> v \<in> labels t"
(*<*) oops (*>*)

lemma lookup_update:
      "ordered t \<Longrightarrow> lookup (update t v) w = (v=w \<or> 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 \<Longrightarrow> labels (delete t v) = labels t - {v}"
(*<*) oops (*>*)

lemma ordered_delete: "ordered t \<Longrightarrow> 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 (*>*)