section \Tries\
text \
Tries are a data structure for fast indexing with strings.
In this project you will implement and verify several functions on and
variations of tries.
(Adapted from \<^url>\http://isabelle.in.tum.de/exercises/advanced/tries/ex.pdf\)
\
theory Project_Tries
imports Main
begin
text \
Section 3.4.4 of the Isabelle/HOL \<^doc>\tutorial\ is a case study about tries. Read that section.
The data type of tries over the alphabet type @{typ 'a} and the value type @{typ 'v}
is defined as follows:
\
datatype ('a, 'v) trie = Trie ("value" : "'v option") (alist : "('a * ('a, 'v) trie) list")
text \
A trie consists of an optional value and an association list that maps letters of the alphabet
to subtrees. It comes with the two selector functions @{const value} and @{const alist}.
Furthermore, there is a function \lookup\ on tries defined with the help of the generic search
function \assoc\ on association lists:
\
fun assoc :: "('k * 'v) list \ 'k \ 'v option"
where
"assoc [] x = None"
| "assoc ((a, b) # ps) x = (if a = x then Some b else assoc ps x)"
fun lookup :: "('a, 'v) trie \ 'a list \ 'v option"
where
"lookup t [] = value t"
| "lookup t (a # as) =
(case assoc (alist t) a of
None \ None
| Some at \ lookup at as)"
text \
Finally, the function \update\ replaces the value associated with some string by a
new value:
\
fun update :: "('a, 'v) trie \ 'a list \ 'v \ ('a, 'v) trie"
where
"update t [] v = Trie (Some v) (alist t)"
| "update t (a # as) v =
(let t' = (case assoc (alist t) a of
None \ Trie None []
| Some at \ at)
in Trie (value t) ((a, update t' as v) # alist t))"
text \
The following result tells us that @{const update} behaves as expected:
\
lemma lookup_empty [simp]: "lookup (Trie None []) xs = None"
by (induction xs) auto
lemma "lookup (update t as v) bs = (if as = bs then Some v else lookup t bs)"
proof (induction t as v arbitrary: bs rule: update.induct)
case (1 t v)
then show ?case by (cases bs) auto
next
case (2 t a as v)
then show ?case by (cases bs) (auto split: option.split)
qed
subsection \Modifying Tries\
text \
As a warm-up exercise, define a function \modify\ for inserting as well as deleting elements
from a trie.
Show that \modify\ satisfies a suitably modified version of the correctness theorem for
@{const update} above.
\
fun modify :: "('a, 'v) trie \ 'a list \ 'v option \ ('a, 'v) trie"
where
"modify t as v = undefined"
lemma "lookup (modify t as v) bs = (if as = bs then v else lookup t bs)"
sorry
text \
The above definition of @{const update} has the disadvantage that it often
creates junk: each association list it passes through is extended at the left
end with a new (letter, value) pair without removing any old association of
that letter which may already be present.
Logically, such cleaning up is unnecessary because @{const assoc} always searches
the list from the left.
However, it constitutes a space leak: the old associations cannot be garbage
collected because physically they are still reachable. This problem can be
solved by means of a function \overwrite\ that does not just add new pairs at the
front but replaces old associations by new pairs if possible.
Define \overwrite\, modify @{const modify} to employ @{term overwrite},
and show the same relationship between @{const modify} and @{const lookup} as
before.
\
fun overwrite :: "'a \ 'b \ ('a * 'b) list \ ('a * 'b) list"
where
"overwrite k v as = undefined"
fun modify' :: "('a, 'v) trie \ 'a list \ 'v option \ ('a, 'v) trie"
where
"modify' t as v = undefined"
lemma "lookup (modify' t as v) bs = (if as = bs then v else lookup t bs)"
sorry
subsection \Time Complexity\
text \
Prove that @{const lookup} takes at most a linear number of recursive calls.
\
fun lookup_t :: "('a, 'v) trie \ 'a list \ nat"
where
"lookup_t t as = undefined"
fun sz :: "('a, 'v) trie \ nat"
where
"sz t = undefined"
lemma "lookup_t t as \ sz t"
sorry
subsection \Tries via Partial Functions\
text \
Instead of association lists we can also use partial functions that map
letters to subtrees.
Partiality can be modelled with the help of type @{typ "'a option"}:
if @{term f} is a function of type @{typ "'a \ 'b option"}, let \f a = Some b\ if \a\ should be
mapped to some @{term b}, and let \f a = None\ otherwise.
\
datatype ('a, 'v) trieP = TrieP "'v option" "'a \ ('a, 'v) trieP option"
text \
Modify the definitions of @{const lookup} and @{const modify'} accordingly and
show the same correctness theorem as above.
\
fun lookup2 :: "('a, 'v) trieP \ 'a list \ 'v option"
where
"lookup2 t as = undefined"
fun modify2 :: "('a, 'v) trieP \ 'a list \ 'v option \ ('a, 'v) trieP"
where
"modify2 t as w = undefined"
lemma "lookup2 (modify2 t as v) bs = (if as = bs then v else lookup2 t bs)"
sorry
end