|
13739
|
1 |
(*<*)
|
|
|
2 |
theory Trie3 = Main:
|
|
|
3 |
(*>*)
|
|
|
4 |
|
|
|
5 |
text {* Instead of association lists we can also use partial functions
|
|
|
6 |
that map letters to subtrees. Partiality can be modelled with the help
|
|
|
7 |
of type @{typ "'a option"}: if @{term f} is a function of type
|
|
|
8 |
\mbox{@{typ "'a \<Rightarrow> 'b option"}}, set @{term "f a = Some b"}
|
|
|
9 |
if @{term a} should be mapped to some @{term b} and set @{term "f a =
|
|
|
10 |
None"} otherwise. *}
|
|
|
11 |
|
|
|
12 |
datatype ('a, 'v) trie = Trie "'v option" "'a \<Rightarrow> ('a,'v) trie option";
|
|
|
13 |
|
|
|
14 |
text{* Modify the definitions of @{term lookup} and @{term modify}
|
|
|
15 |
accordingly and show the same correctness theorem as above. *}
|
|
|
16 |
|
|
|
17 |
(*<*)
|
|
|
18 |
end;
|
|
|
19 |
(*>*)
|