1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Tree}% |
3 \def\isabellecontext{Tree}% |
4 \isamarkupfalse% |
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 \isamarkuptrue% |
5 % |
18 % |
6 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
7 \noindent |
20 \noindent |
8 Define the datatype of \rmindex{binary trees}:% |
21 Define the datatype of \rmindex{binary trees}:% |
9 \end{isamarkuptext}% |
22 \end{isamarkuptext}% |
10 \isamarkuptrue% |
|
11 \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\isamarkupfalse% |
|
12 \isamarkupfalse% |
23 \isamarkupfalse% |
13 \isamarkupfalse% |
24 \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\isamarkuptrue% |
14 % |
25 % |
15 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
16 \noindent |
27 \noindent |
17 Define a function \isa{mirror} that mirrors a binary tree |
28 Define a function \isa{mirror} that mirrors a binary tree |
18 by swapping subtrees recursively. Prove% |
29 by swapping subtrees recursively. Prove% |
19 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
|
31 \isamarkupfalse% |
|
32 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}% |
|
33 \isadelimproof |
|
34 % |
|
35 \endisadelimproof |
|
36 % |
|
37 \isatagproof |
|
38 % |
|
39 \endisatagproof |
|
40 {\isafoldproof}% |
|
41 % |
|
42 \isadelimproof |
|
43 % |
|
44 \endisadelimproof |
20 \isamarkuptrue% |
45 \isamarkuptrue% |
21 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse% |
|
22 \isamarkupfalse% |
|
23 \isamarkupfalse% |
|
24 \isamarkupfalse% |
|
25 \isamarkupfalse% |
|
26 % |
46 % |
27 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
28 \noindent |
48 \noindent |
29 Define a function \isa{flatten} that flattens a tree into a list |
49 Define a function \isa{flatten} that flattens a tree into a list |
30 by traversing it in infix order. Prove% |
50 by traversing it in infix order. Prove% |
31 \end{isamarkuptext}% |
51 \end{isamarkuptext}% |
32 \isamarkuptrue% |
|
33 \isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
34 \isamarkupfalse% |
52 \isamarkupfalse% |
35 \isamarkupfalse% |
53 \isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}% |
36 \isamarkupfalse% |
54 \isadelimproof |
|
55 % |
|
56 \endisadelimproof |
|
57 % |
|
58 \isatagproof |
|
59 % |
|
60 \endisatagproof |
|
61 {\isafoldproof}% |
|
62 % |
|
63 \isadelimproof |
|
64 % |
|
65 \endisadelimproof |
|
66 % |
|
67 \isadelimtheory |
|
68 % |
|
69 \endisadelimtheory |
|
70 % |
|
71 \isatagtheory |
|
72 % |
|
73 \endisatagtheory |
|
74 {\isafoldtheory}% |
|
75 % |
|
76 \isadelimtheory |
|
77 % |
|
78 \endisadelimtheory |
37 \end{isabellebody}% |
79 \end{isabellebody}% |
38 %%% Local Variables: |
80 %%% Local Variables: |
39 %%% mode: latex |
81 %%% mode: latex |
40 %%% TeX-master: "root" |
82 %%% TeX-master: "root" |
41 %%% End: |
83 %%% End: |