header {* B\"aume *}

theory Aufgabe2 = Main:

text{*Wir arbeiten im Folgenden mit einer sehr einfachen Form der
Bin\"arb\"aume, deren Bl\"attern (``tip'') und Knoten (``node'')
keine Information enthalten:*}

datatype tree = Tp | Nd tree tree

text{* \emph{Definieren Sie eine Funktion @{term tips}, die die Anzahl der
Bl\"atter in einem Baum z\"ahlt, und eine Funktion @{term height}, die die
H\"ohe eines Baumes berechnet.}

Vollst\"andigen Bin\"arb\"aume (``complete binary trees'')
einer gewissen H\"ohe werden wie folgt erzeugt:
*}

consts cbt :: "nat \<Rightarrow> tree"
primrec
"cbt 0 = Tp"
"cbt(Suc n) = Nd (cbt n) (cbt n)"

text{*
Um diese speziellen B\"aume wird es im Folgenden gehen.

Die Funktion @{term cbt} erzeugt vollst\"andige Bin\"arb\"aume.  Man kann
aber auch testen, ob ein gegebener Baum vollst\"andig ist. Definieren sie eine
allgemeine Testfunktion @{term iscbt} (bzgl.\ einer Funktion auf B\"aumen),
die folgende verbale Beschreibung implementiert: @{term Tp} ist vollst\"andig
(bzgl.\ jeder Funktion auf B\"aumen), und @{term"Nd l r"} ist vollst\"andig
(bzgl.\ einer Funktion @{term f}) gdw @{term l} und @{term r} vollst\"andig
sind (bzgl.\ @{term f}) und @{prop"f l = f r"} gilt.

Wir haben nun 3 Funktionen auf B\"aumen, n\"amlich @{term tips}, @{term
height} und @{term size}. Letztere wird automatisch definiert --- lesen sie
im Tutorial nach, wie sie sich verh\"alt. Damit haben wir auch 3 Versionen
des Begriffs \emph{Vollst\"andig}: vollst\"andig bzgl.\ @{term tips},
vollst\"andig bzgl.\ @{term height} und vollst\"andig bzgl.\ @{term
size}. Zeigen Sie nun,
\begin{itemize}
\item \emph{dass alle 3 Begriffe das gleiche bedeuten}
      (z.B. @{prop"iscbt tips t = iscbt size t"}), und
\item \emph{dass alle 3 Begriffe genau die von @{term cbt} erzeugten B\"aume
beschreiben}: Das Resultat von @{term cbt} ist vollst\"andig im Sinne von
@{term iscbt} (bzgl.\ jeder Funktion auf B\"aumen), und wenn ein Baum im
Sinne von @{term iscbt} vollst\"andig ist, so ist er das Ergebnis von @{term
cbt} (angewandt auf eine passende, von Ihnen zu findende Zahl).
\end{itemize}
\emph{Geben Sie eine Funktion @{term f} an, so dass @{prop"iscbt f"}
verschieden von @{term"iscbt size"} etc ist.}

Hinweise:
\begin{itemize}
\item \"Uberlegen Sie Sich (und beweisen Sie!) geeignete Beziehungen zwischen
den Funktionen @{term tips}, @{term height} und @{term size}.
\item Eventuell ben\"otigen Sie Lemmas, in denen es nur um die arithmetischen
Grundfunktionen (@{text"+"}, @{text"*"}, @{text"^"} etc) geht.
Diese k\"onnen Sie einfach mit \isacommand{sorry}
,,beweisen'', falls weder die Methode @{text arith} noch Sie selbst einen
Beweis finden. Nicht @{text"apply sorry"} sondern nur @{text sorry}.
\item
Sie brauchen nicht explizit zu beweisen, dass jeder
Begriff gleich jedem anderen ist. So gen\"ugt es z.B.\ zu zeigen, dass
$A = C$ und $B = C$ --- $A = B$ ist eine triviale Konsequenz.
Die Schwierigkeit der Beweise wird aber davon abh\"angen, welche der
\"Aquivalenzen sie beweisen.
\item Es gibt @{text"\<and>"} und @{text"\<longrightarrow>"}.
\end{itemize}
*}

end;