doc-src/Tutorial/Datatype/Trie.thy

tuned;

Trie = Main +
consts   assoc :: "('key * 'val)list => 'key => 'val option"
primrec "assoc [] x = None"
        "assoc (p#ps) x =
           (let (a,b) = p in if a=x then Some b else assoc ps x)"
datatype ('a,'v)trie = Trie ('v option) "('a * ('a,'v)trie)list"
consts value :: ('a,'v)trie => 'v option
       alist :: "('a,'v)trie => ('a * ('a,'v)trie)list"
primrec "value(Trie ov al) = ov"
primrec "alist(Trie ov al) = al"
consts   lookup :: ('a,'v)trie => 'a list => 'v option
primrec "lookup t [] = value t"
        "lookup t (a#as) = (case assoc (alist t) a of
                              None => None
                            | Some at => lookup at as)"
consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie

primrec
  "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))"
end