--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/Trie.thy Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,23 @@
+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