|
1 (*<*) |
|
2 theory Aufgabe2 = Main: |
|
3 (*>*) |
|
4 |
|
5 subsection {* Trees *} |
|
6 |
|
7 text{* In the sequel we work with skeletons of binary trees where |
|
8 neither the leaves (``tip'') nor the nodes contain any information: *} |
|
9 |
|
10 datatype tree = Tp | Nd tree tree |
|
11 |
|
12 text{* Define a function @{term tips} that counts the tips of a |
|
13 tree, and a function @{term height} that computes the height of a |
|
14 tree. |
|
15 |
|
16 Complete binary trees of a given height are generated as follows: |
|
17 *} |
|
18 |
|
19 consts cbt :: "nat \<Rightarrow> tree" |
|
20 primrec |
|
21 "cbt 0 = Tp" |
|
22 "cbt(Suc n) = Nd (cbt n) (cbt n)" |
|
23 |
|
24 text{* |
|
25 We will now focus on these complete binary trees. |
|
26 |
|
27 Instead of generating complete binary trees, we can also \emph{test} |
|
28 if a binary tree is complete. Define a function @{term "iscbt f"} |
|
29 (where @{term f} is a function on trees) that checks for completeness: |
|
30 @{term Tp} is complete and @{term"Nd l r"} ist complete iff @{term l} and |
|
31 @{term r} are complete and @{prop"f l = f r"}. |
|
32 |
|
33 We now have 3 functions on trees, namely @{term tips}, @{term height} |
|
34 und @{term size}. The latter is defined automatically --- look it up |
|
35 in the tutorial. Thus we also have 3 kinds of completeness: complete |
|
36 wrt.\ @{term tips}, complete wrt.\ @{term height} and complete wrt.\ |
|
37 @{term size}. Show that |
|
38 \begin{itemize} |
|
39 \item the 3 notions are the same (e.g.\ @{prop"iscbt tips t = iscbt size t"}), |
|
40 and |
|
41 \item the 3 notions describe exactly the trees generated by @{term cbt}: |
|
42 the result of @{term cbt} is complete (in the sense of @{term iscbt}, |
|
43 wrt.\ any function on trees), and if a tree is complete in the sense of |
|
44 @{term iscbt}, it is the result of @{term cbt} (applied to a suitable number |
|
45 --- which one?) |
|
46 \end{itemize} |
|
47 Find a function @{term f} such that @{prop"iscbt f"} is different from |
|
48 @{term"iscbt size"}. |
|
49 |
|
50 Hints: |
|
51 \begin{itemize} |
|
52 \item Work out and prove suitable relationships between @{term tips}, |
|
53 @{term height} und @{term size}. |
|
54 |
|
55 \item If you need lemmas dealing only with the basic arithmetic operations |
|
56 (@{text"+"}, @{text"*"}, @{text"^"} etc), you can ``prove'' them |
|
57 with the command @{text sorry}, if neither @{text arith} nor you can |
|
58 find a proof. Not @{text"apply sorry"}, just @{text sorry}. |
|
59 |
|
60 \item |
|
61 You do not need to show that every notion is equal to every other |
|
62 notion. It suffices to show that $A = C$ und $B = C$ --- $A = B$ is a |
|
63 trivial consequence. However, the difficulty of the proof will depend |
|
64 on which of the equivalences you prove. |
|
65 |
|
66 \item There is @{text"\<and>"} and @{text"\<longrightarrow>"}. |
|
67 \end{itemize} |
|
68 *} |
|
69 |
|
70 (*<*) |
|
71 end; |
|
72 (*>*) |