equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Trie{\isadigit{3}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \begin{isamarkuptext}% |
|
7 Instead of association lists we can also use partial functions |
|
8 that map letters to subtrees. Partiality can be modelled with the help |
|
9 of type \isa{{\isacharprime}a\ option}: if \isa{f} is a function of type |
|
10 \mbox{\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option}}, set \isa{f\ a\ {\isacharequal}\ Some\ b} |
|
11 if \isa{a} should be mapped to some \isa{b} and set \isa{f\ a\ {\isacharequal}\ None} otherwise.% |
|
12 \end{isamarkuptext}% |
|
13 \isamarkuptrue% |
|
14 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie\ option{\isachardoublequote}\isamarkupfalse% |
|
15 % |
|
16 \begin{isamarkuptext}% |
|
17 Modify the definitions of \isa{lookup} and \isa{modify} |
|
18 accordingly and show the same correctness theorem as above.% |
|
19 \end{isamarkuptext}% |
|
20 \isamarkuptrue% |
|
21 \isamarkupfalse% |
|
22 \end{isabellebody}% |
|
23 %%% Local Variables: |
|
24 %%% mode: latex |
|
25 %%% TeX-master: "root" |
|
26 %%% End: |
|