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

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

%
\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: