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