--- a/doc-src/Exercises/2001/a2/Aufgabe2.thy Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*<*)
-theory Aufgabe2 = Main:
-(*>*)
-
-subsection {* Trees *}
-
-text{* In the sequel we 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.
-
-Complete binary trees of a given height are generated as follows:
-*}
-
-consts cbt :: "nat \<Rightarrow> tree"
-primrec
-"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"} ist complete iff @{term l} and
-@{term r} are complete and @{prop"f l = f r"}.
-
-We now have 3 functions on trees, namely @{term tips}, @{term height}
-und @{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}
-Find a function @{term f} such that @{prop"iscbt f"} is different from
-@{term"iscbt size"}.
-
-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 can ``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>"} and @{text"\<longrightarrow>"}.
-\end{itemize}
-*}
-
-(*<*)
-end;
-(*>*)