doc-src/Exercises/2001/a2/generated/Aufgabe2.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2001/a2/generated/Aufgabe2.tex	Sat Mar 01 16:57:32 2003 +0100
@@ -0,0 +1,82 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Aufgabe{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In the sequel we work with skeletons of binary trees where
+neither the leaves (``tip'') nor the nodes contain any information:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ tree\ {\isacharequal}\ Tp\ {\isacharbar}\ Nd\ tree\ tree\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{tips} that counts the tips of a
+tree, and a function \isa{height} that computes the height of a
+tree.
+
+Complete binary trees of a given height are generated as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ cbt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ tree{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+{\isachardoublequote}cbt\ {\isadigit{0}}\ {\isacharequal}\ Tp{\isachardoublequote}\isanewline
+{\isachardoublequote}cbt{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Nd\ {\isacharparenleft}cbt\ n{\isacharparenright}\ {\isacharparenleft}cbt\ n{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+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 \isa{iscbt\ f}
+(where \isa{f} is a function on trees) that checks for completeness:
+\isa{Tp} is complete and \isa{Nd\ l\ r} ist complete iff \isa{l} and
+\isa{r} are complete and \isa{f\ l\ {\isacharequal}\ f\ r}.
+
+We now have 3 functions on trees, namely \isa{tips}, \isa{height}
+und \isa{size}. The latter is defined automatically --- look it up
+in the tutorial.  Thus we also have 3 kinds of completeness: complete
+wrt.\ \isa{tips}, complete wrt.\ \isa{height} and complete wrt.\
+\isa{size}. Show that
+\begin{itemize}
+\item the 3 notions are the same (e.g.\ \isa{iscbt\ tips\ t\ {\isacharequal}\ iscbt\ size\ t}),
+      and
+\item the 3 notions describe exactly the trees generated by \isa{cbt}:
+the result of \isa{cbt} is complete (in the sense of \isa{iscbt},
+wrt.\ any function on trees), and if a tree is complete in the sense of
+\isa{iscbt}, it is the result of \isa{cbt} (applied to a suitable number
+--- which one?)
+\end{itemize}
+Find a function \isa{f} such that \isa{iscbt\ f} is different from
+\isa{iscbt\ size}.
+
+Hints:
+\begin{itemize}
+\item Work out and prove suitable relationships between \isa{tips},
+      \isa{height} und \isa{size}.
+
+\item If you need lemmas dealing only with the basic arithmetic operations
+(\isa{{\isacharplus}}, \isa{{\isacharasterisk}}, \isa{{\isacharcircum}} etc), you can ``prove'' them
+with the command \isa{sorry}, if neither \isa{arith} nor you can
+find a proof. Not \isa{apply\ sorry}, just \isa{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 \isa{{\isasymand}} and \isa{{\isasymlongrightarrow}}.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: