(* $Id: ex.thy,v 1.4 2011/06/28 18:11:37 webertj Exp$ Author: Tobias Nipkow *) header {* Tries *} (*<*) theory ex imports Main begin (*>*) text {* Section~3.4.4 of the Isabelle/HOL tutorial is a case study about so-called \emph{tries}, a data structure for fast indexing with strings. Read that section. The data type of tries over the alphabet type @{typ 'a} und the value type @{typ 'v} is defined as follows: *} datatype ('a, 'v) trie = Trie "'v option" "('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. Type @{typ "'a option"} is defined in Section~2.5.3 of the Isabelle/HOL tutorial. There are also two selector functions @{term value} and @{term alist}: *} primrec "value" :: "('a, 'v) trie \ 'v option" where "value (Trie ov al) = ov" primrec alist :: "('a, 'v) trie \ ('a * ('a,'v) trie) list" where "alist (Trie ov al) = al" text {* Furthermore there is a function @{term lookup} on tries defined with the help of the generic search function @{term assoc} on association lists: *} primrec assoc :: "('key * 'val)list \ 'key \ 'val option" where "assoc [] x = None" | "assoc (p#ps) x = (let (a, b) = p in if a = x then Some b else assoc ps x)" primrec 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, @{term update} updates the value associated with some string with a new value, overwriting the old one: *} primrec 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 tt = (case assoc (alist t) a of None \ Trie None [] | Some at \ at) in Trie (value t) ((a, update tt as v) # alist t))" text {* The following theorem tells us that @{term update} behaves as expected: *} theorem "\t v bs. lookup (update t as v) bs = (if as = bs then Some v else lookup t bs)" (*<*) oops (*>*) text {* As a warm-up exercise, define a function *} consts modify :: "('a, 'v) trie \ 'a list \ 'v option \ ('a, 'v) trie" text{* for inserting as well as deleting elements from a trie. Show that @{term modify} satisfies a suitably modified version of the correctness theorem for @{term update}. *} text {* The above definition of @{term 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 @{term 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 *} consts overwrite :: "'a \ 'b \ ('a * 'b) list \ ('a * 'b) list" text {* that does not just add new pairs at the front but replaces old associations by new pairs if possible. Define @{term overwrite}, modify @{term modify} to employ @{term overwrite}, and show the same relationship between @{term modify} and @{term lookup} as before. *} 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 \mbox{@{typ "'a \ 'b option"}}, let @{term "f a = Some b"} if @{term a} should be mapped to some @{term b}, and let @{term "f a = None"} otherwise. *} datatype ('a, 'v) trieP = Trie "'v option" "'a \ ('a,'v) trieP option" text {* Modify the definitions of @{term lookup} and @{term modify} accordingly and show the same correctness theorem as above. *} (*<*) end (*>*)