(*
$Id: ex.thy,v 1.3 2008/07/04 15:37:39 nipkow Exp $
Author: Tobias Nipkow
*)
header {* Complete Binary Trees *}
(*<*) theory ex imports Main begin (*>*)
text {* Let's work with skeletons of binary trees where neither the leaves
(``tip'') nor the nodes contain any information: *}
datatype tree = Tp | Nd tree tree
text {* Define a function @{term tips} that counts the tips of a tree, and a
function @{term height} that computes the height of a tree. *}
text {* Complete binary trees of a given height are generated as follows: *}
primrec cbt :: "nat \ tree" where
"cbt 0 = Tp" |
"cbt (Suc n) = Nd (cbt n) (cbt n)"
text {* We will now focus on these complete binary trees.
Instead of generating complete binary trees, we can also \emph{test} if a
binary tree is complete. Define a function @{term "iscbt f"} (where @{term f}
is a function on trees) that checks for completeness: @{term Tp} is complete,
and @{term"Nd l r"} is complete iff @{term l} and @{term r} are complete and
@{prop"f l = f r"}. *}
text {* We now have 3 functions on trees, namely @{term tips}, @{term height}
and @{term size}. The latter is defined automatically -- look it up in the
tutorial. Thus we also have 3 kinds of completeness: complete wrt.\ @{term
tips}, complete wrt.\ @{term height} and complete wrt.\ @{term size}. Show
that
\begin{itemize}
\item the 3 notions are the same (e.g.\ @{prop "iscbt tips t = iscbt size t"}),
and
\item the 3 notions describe exactly the trees generated by @{term cbt}: the
result of @{term cbt} is complete (in the sense of @{term iscbt}, wrt.\
any function on trees), and if a tree is complete in the sense of @{term
iscbt}, it is the result of @{term cbt} (applied to a suitable number~--
which one?).
\end{itemize}
Hints:
\begin{itemize}
\item Work out and prove suitable relationships between @{term tips}, @{term
height} und @{term size}.
\item If you need lemmas dealing only with the basic arithmetic operations
(@{text"+"}, @{text"*"}, @{text"^"} etc), you may ``prove'' them with the
command @{text sorry}, if neither @{text arith} nor you can find a proof.
Not @{text "apply sorry"}, just @{text sorry}.
\item You do not need to show that every notion is equal to every other notion.
It suffices to show that $A = C$ und $B = C$ -- $A = B$ is a trivial
consequence. However, the difficulty of the proof will depend on which
of the equivalences you prove.
\item There is @{text"\"} and @{text"\"}.
\end{itemize} *}
text {* Find a function @{term f} such that @{term "iscbt f"} is different from
@{term "iscbt size"}. *}
(*<*) end (*>*)