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