| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 27015 | f8537d69f514 |
| child 40685 | 313a24b66a8d |
| permissions | -rw-r--r-- |
| nipkow@9722 | 1 |
% |
| nipkow@9722 | 2 |
\begin{isabellebody}%
|
| wenzelm@10267 | 3 |
\def\isabellecontext{Tree{\isadigit{2}}}%
|
| wenzelm@17056 | 4 |
% |
| wenzelm@17056 | 5 |
\isadelimtheory |
| wenzelm@17056 | 6 |
% |
| wenzelm@17056 | 7 |
\endisadelimtheory |
| wenzelm@17056 | 8 |
% |
| wenzelm@17056 | 9 |
\isatagtheory |
| wenzelm@17056 | 10 |
% |
| wenzelm@17056 | 11 |
\endisatagtheory |
| wenzelm@17056 | 12 |
{\isafoldtheory}%
|
| wenzelm@17056 | 13 |
% |
| wenzelm@17056 | 14 |
\isadelimtheory |
| wenzelm@17056 | 15 |
% |
| wenzelm@17056 | 16 |
\endisadelimtheory |
| nipkow@9493 | 17 |
% |
| nipkow@9493 | 18 |
\begin{isamarkuptext}%
|
| nipkow@9493 | 19 |
\noindent In Exercise~\ref{ex:Tree} we defined a function
|
| nipkow@9493 | 20 |
\isa{flatten} from trees to lists. The straightforward version of
|
| nipkow@9792 | 21 |
\isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev},
|
| nipkow@9792 | 22 |
quadratic. A linear time version of \isa{flatten} again reqires an extra
|
| nipkow@27015 | 23 |
argument, the accumulator. Define% |
| nipkow@9493 | 24 |
\end{isamarkuptext}%
|
| wenzelm@17175 | 25 |
\isamarkuptrue% |
| nipkow@27015 | 26 |
flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
|
| nipkow@9493 | 27 |
\begin{isamarkuptext}%
|
| nipkow@27015 | 28 |
\noindent and prove% |
| nipkow@9493 | 29 |
\end{isamarkuptext}%
|
| wenzelm@17175 | 30 |
\isamarkuptrue% |
| wenzelm@17056 | 31 |
% |
| wenzelm@17056 | 32 |
\isadelimproof |
| wenzelm@17056 | 33 |
% |
| wenzelm@17056 | 34 |
\endisadelimproof |
| wenzelm@17056 | 35 |
% |
| wenzelm@17056 | 36 |
\isatagproof |
| wenzelm@17056 | 37 |
% |
| wenzelm@17056 | 38 |
\endisatagproof |
| wenzelm@17056 | 39 |
{\isafoldproof}%
|
| wenzelm@17056 | 40 |
% |
| wenzelm@17056 | 41 |
\isadelimproof |
| wenzelm@17056 | 42 |
% |
| wenzelm@17056 | 43 |
\endisadelimproof |
| wenzelm@17175 | 44 |
\isacommand{lemma}\isamarkupfalse%
|
| wenzelm@17175 | 45 |
\ {\isachardoublequoteopen}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequoteclose}%
|
| wenzelm@17056 | 46 |
\isadelimproof |
| wenzelm@17056 | 47 |
% |
| wenzelm@17056 | 48 |
\endisadelimproof |
| wenzelm@17056 | 49 |
% |
| wenzelm@17056 | 50 |
\isatagproof |
| wenzelm@17056 | 51 |
% |
| wenzelm@17056 | 52 |
\endisatagproof |
| wenzelm@17056 | 53 |
{\isafoldproof}%
|
| wenzelm@17056 | 54 |
% |
| wenzelm@17056 | 55 |
\isadelimproof |
| wenzelm@17056 | 56 |
% |
| wenzelm@17056 | 57 |
\endisadelimproof |
| wenzelm@17056 | 58 |
% |
| wenzelm@17056 | 59 |
\isadelimtheory |
| wenzelm@17056 | 60 |
% |
| wenzelm@17056 | 61 |
\endisadelimtheory |
| wenzelm@17056 | 62 |
% |
| wenzelm@17056 | 63 |
\isatagtheory |
| wenzelm@17056 | 64 |
% |
| wenzelm@17056 | 65 |
\endisatagtheory |
| wenzelm@17056 | 66 |
{\isafoldtheory}%
|
| wenzelm@17056 | 67 |
% |
| wenzelm@17056 | 68 |
\isadelimtheory |
| wenzelm@17056 | 69 |
% |
| wenzelm@17056 | 70 |
\endisadelimtheory |
| wenzelm@11866 | 71 |
\end{isabellebody}%
|
| nipkow@9493 | 72 |
%%% Local Variables: |
| nipkow@9493 | 73 |
%%% mode: latex |
| nipkow@9493 | 74 |
%%% TeX-master: "root" |
| nipkow@9493 | 75 |
%%% End: |