equal
deleted
inserted
replaced
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Tree}% |
3 \def\isabellecontext{Tree}% |
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \noindent |
6 \noindent |
7 Define the datatype of binary trees% |
7 Define the datatype of \rmindex{binary trees}:% |
8 \end{isamarkuptext}% |
8 \end{isamarkuptext}% |
9 \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}% |
9 \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}% |
10 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
11 \noindent |
11 \noindent |
12 and a function \isa{mirror} that mirrors a binary tree |
12 Define a function \isa{mirror} that mirrors a binary tree |
13 by swapping subtrees recursively. Prove% |
13 by swapping subtrees recursively. Prove% |
14 \end{isamarkuptext}% |
14 \end{isamarkuptext}% |
15 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}% |
15 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}% |
16 \begin{isamarkuptext}% |
16 \begin{isamarkuptext}% |
17 \noindent |
17 \noindent |