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 (*>*)