equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Tree{\isadigit{2}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \noindent In Exercise~\ref{ex:Tree} we defined a function |
|
20 \isa{flatten} from trees to lists. The straightforward version of |
|
21 \isa{flatten} is based on \isa{{\isaliteral{40}{\isacharat}}} and is thus, like \isa{rev}, |
|
22 quadratic. A linear time version of \isa{flatten} again reqires an extra |
|
23 argument, the accumulator. Define% |
|
24 \end{isamarkuptext}% |
|
25 \isamarkuptrue% |
|
26 flatten{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}% |
|
27 \begin{isamarkuptext}% |
|
28 \noindent and prove% |
|
29 \end{isamarkuptext}% |
|
30 \isamarkuptrue% |
|
31 % |
|
32 \isadelimproof |
|
33 % |
|
34 \endisadelimproof |
|
35 % |
|
36 \isatagproof |
|
37 % |
|
38 \endisatagproof |
|
39 {\isafoldproof}% |
|
40 % |
|
41 \isadelimproof |
|
42 % |
|
43 \endisadelimproof |
|
44 \isacommand{lemma}\isamarkupfalse% |
|
45 \ {\isaliteral{22}{\isachardoublequoteopen}}flatten{\isadigit{2}}\ t\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ flatten\ t{\isaliteral{22}{\isachardoublequoteclose}}% |
|
46 \isadelimproof |
|
47 % |
|
48 \endisadelimproof |
|
49 % |
|
50 \isatagproof |
|
51 % |
|
52 \endisatagproof |
|
53 {\isafoldproof}% |
|
54 % |
|
55 \isadelimproof |
|
56 % |
|
57 \endisadelimproof |
|
58 % |
|
59 \isadelimtheory |
|
60 % |
|
61 \endisadelimtheory |
|
62 % |
|
63 \isatagtheory |
|
64 % |
|
65 \endisatagtheory |
|
66 {\isafoldtheory}% |
|
67 % |
|
68 \isadelimtheory |
|
69 % |
|
70 \endisadelimtheory |
|
71 \end{isabellebody}% |
|
72 %%% Local Variables: |
|
73 %%% mode: latex |
|
74 %%% TeX-master: "root" |
|
75 %%% End: |