1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Trie{\isadigit{1}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Tries% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Section~3.4.4 of \cite{isabelle-tutorial} is a case study |
|
12 about so-called \emph{tries}, a data structure for fast indexing with |
|
13 strings. Read that section. |
|
14 |
|
15 The data type of tries over the alphabet type \isa{{\isacharprime}a} und the value |
|
16 type \isa{{\isacharprime}v} is defined as follows:% |
|
17 \end{isamarkuptext}% |
|
18 \isamarkuptrue% |
|
19 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse% |
|
20 % |
|
21 \begin{isamarkuptext}% |
|
22 A trie consists of an optional value and an association list |
|
23 that maps letters of the alphabet to subtrees. Type \isa{{\isacharprime}a\ option} is |
|
24 defined in section~2.5.3 of \cite{isabelle-tutorial}. |
|
25 |
|
26 There are also two selector functions \isa{value} and \isa{alist}:% |
|
27 \end{isamarkuptext}% |
|
28 \isamarkuptrue% |
|
29 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline |
|
30 \isamarkupfalse% |
|
31 \isacommand{primrec}\ {\isachardoublequote}value\ {\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequote}\ \isanewline |
|
32 \isanewline |
|
33 \isamarkupfalse% |
|
34 \isacommand{consts}\ alist\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list{\isachardoublequote}\isanewline |
|
35 \isamarkupfalse% |
|
36 \isacommand{primrec}\ {\isachardoublequote}alist\ {\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequote}\isamarkupfalse% |
|
37 % |
|
38 \begin{isamarkuptext}% |
|
39 Furthermore there is a function \isa{lookup} on tries |
|
40 defined with the help of the generic search function \isa{assoc} on |
|
41 association lists:% |
|
42 \end{isamarkuptext}% |
|
43 \isamarkuptrue% |
|
44 \isacommand{consts}\ assoc\ {\isacharcolon}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequote}\isanewline |
|
45 \isamarkupfalse% |
|
46 \isacommand{primrec}\ {\isachardoublequote}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequote}\isanewline |
|
47 \ \ \ \ \ \ \ \ {\isachardoublequote}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline |
|
48 \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a\ {\isacharequal}\ x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequote}\isanewline |
|
49 \isanewline |
|
50 \isamarkupfalse% |
|
51 \isacommand{consts}\ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline |
|
52 \isamarkupfalse% |
|
53 \isacommand{primrec}\ {\isachardoublequote}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequote}\isanewline |
|
54 \ \ \ \ \ \ \ \ {\isachardoublequote}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline |
|
55 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline |
|
56 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
57 % |
|
58 \begin{isamarkuptext}% |
|
59 Finally, \isa{update} updates the value associated with some |
|
60 string with a new value, overwriting the old one:% |
|
61 \end{isamarkuptext}% |
|
62 \isamarkuptrue% |
|
63 \isacommand{consts}\ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isachardoublequote}\isanewline |
|
64 \isamarkupfalse% |
|
65 \isacommand{primrec}\isanewline |
|
66 \ \ {\isachardoublequote}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequote}\isanewline |
|
67 \ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline |
|
68 \ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline |
|
69 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ \isanewline |
|
70 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline |
|
71 \ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}\ update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
72 % |
|
73 \begin{isamarkuptext}% |
|
74 The following theorem tells us that \isa{update} behaves as |
|
75 expected:% |
|
76 \end{isamarkuptext}% |
|
77 \isamarkuptrue% |
|
78 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline |
|
79 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as\ {\isacharequal}\ bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
80 \isamarkupfalse% |
|
81 % |
|
82 \begin{isamarkuptext}% |
|
83 As a warming up exercise, define a function% |
|
84 \end{isamarkuptext}% |
|
85 \isamarkuptrue% |
|
86 \isacommand{consts}\ modify\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isachardoublequote}\isamarkupfalse% |
|
87 % |
|
88 \begin{isamarkuptext}% |
|
89 for inserting as well as deleting elements from a trie. Show |
|
90 that \isa{modify} satisfies a suitably modified version of the |
|
91 correctness theorem for \isa{update}.% |
|
92 \end{isamarkuptext}% |
|
93 \isamarkuptrue% |
|
94 \isamarkupfalse% |
|
95 \end{isabellebody}% |
|
96 %%% Local Variables: |
|
97 %%% mode: latex |
|
98 %%% TeX-master: "root" |
|
99 %%% End: |
|