# Theory TrieList

Up to index of Isabelle/HOL/Tame

theory TrieList
imports Main
begin

```(*  ID:         \$Id: TrieList.thy,v 1.1 2006/01/04 13:44:14 nipkow Exp \$
Author:     Tobias Nipkow
*)

theory TrieList
imports Main
begin

(* FIXME move alist to List *)

subsection {* Association lists *}

consts
assoc :: "('key * 'val)list => 'key => 'val option"
rem_alist :: "'key => ('key * 'val)list =>  ('key * 'val)list"
upd_alist :: "'key => 'val => ('key * 'val)list =>  ('key * 'val)list"

primrec
"assoc [] x = None"
"assoc (p#ps) x = (let (a,b) = p in if a=x then Some b else assoc ps x)";
primrec
"rem_alist k [] = []"
"rem_alist k (p#ps) = (if fst p = k then ps else p # rem_alist k ps)"
primrec
"upd_alist k v [] = [(k,v)]"
"upd_alist k v (p#ps) = (if fst p = k then (k,v)#ps else p # upd_alist k v ps)"

lemma assoc_conv: "assoc al x = map_of al x"
by(induct al, auto)

lemma map_of_upd_alist: "map_of(upd_alist k v al) = (map_of al)(k \<mapsto> v)"
apply(induct al)
apply simp
apply(rule ext)
apply auto
done

lemma rem_alist_id[simp]: "k ∉ fst ` set al ==> rem_alist k al = al"
by(induct al, auto)

lemma map_of_rem_distinct_alist: "distinct(map fst al) ==>
map_of(rem_alist k al) = (map_of al)(k := None)"
apply(induct al)
apply simp
apply clarify
apply(rule ext)
apply auto
apply(erule ssubst)
apply simp
done

lemma map_of_rem_alist[simp]:
"k' ≠ k ==> map_of (rem_alist k al) k' = map_of al k'"
by(induct al, auto)

subsection {* Trie *}

datatype ('a,'v)trie = Trie  "'v list"  "('a * ('a,'v)trie)list"

consts values :: "('a,'v)trie => 'v list"
alist :: "('a,'v)trie => ('a * ('a,'v)trie)list"
primrec "values(Trie vs al) = vs"
primrec "alist(Trie vs al) = al"

consts
lookup_trie :: "('a,'v)trie => 'a list => 'v list"
update_trie :: "('a,'v)trie => 'a list => 'v list => ('a,'v)trie"
insert_trie :: "('a,'v)trie => 'a list => 'v      => ('a,'v)trie"

primrec
"lookup_trie t [] = values t"
"lookup_trie t (a#as) = (case assoc (alist t) a of
None => []
| Some at => lookup_trie at as)"
primrec
"update_trie t []     vs = Trie vs (alist t)"
"update_trie t (a#as) vs =
(let tt = (case assoc (alist t) a of
None => Trie [] [] | Some at => at)
in Trie (values t) ((a,update_trie tt as vs) # rem_alist a (alist t)))"

primrec
"insert_trie t []     v = Trie (v # values t) (alist t)"
"insert_trie t (a#as) vs =
(let tt = (case assoc (alist t) a of
None => Trie [] [] | Some at => at)
in Trie (values t) ((a,insert_trie tt as vs) # rem_alist a (alist t)))";

lemma lookup_empty[simp]: "lookup_trie (Trie [] []) as = []"
by(case_tac as, simp_all)

theorem lookup_update_trie: "!t v bs.
lookup_trie (update_trie t as vs) bs = (if as=bs then vs else lookup_trie t bs)"
apply(induct as)
apply clarsimp
apply(case_tac bs)
apply simp
apply simp
apply clarsimp
apply(case_tac bs)
apply (auto simp add:Let_def assoc_conv split:option.split)
done

theorem insert_trie_conv:
"!!t. insert_trie t as v = update_trie t as (v#lookup_trie t as)"
apply(induct as)
apply (auto simp:Let_def assoc_conv split:option.split)
done

constdefs
trie_of_list :: "('b => 'a list) => 'b list => ('a,'b)trie"
"trie_of_list key == foldl (%t v. insert_trie t (key v) v) (Trie [] [])"

lemma in_set_lookup_trie_of_list:
"v ∈ set(lookup_trie (trie_of_list key vs) (key v)) = (v ∈ set vs)"
proof -
have "!!t.
v ∈ set(lookup_trie (foldl (%t v. insert_trie t (key v) v) t vs) (key v)) =
(v ∈ set vs ∪ set(lookup_trie t (key v)))"
apply(induct vs)
apply blast
done
qed

lemma in_set_lookup_trie_of_listD:
assumes "v ∈ set(lookup_trie (trie_of_list f vs) xs)" shows "v ∈ set vs"
proof -
have "!!t.
v ∈ set(lookup_trie (foldl (%t v. insert_trie t (f v) v) t vs) xs) ==>
v ∈ set vs ∪ set(lookup_trie t xs)"
apply(induct vs)
apply(force simp:insert_trie_conv lookup_update_trie split:split_if_asm)
done
thus ?thesis using prems by(force simp add:trie_of_list_def)
qed

end```

### Association lists

lemma assoc_conv:

`  assoc al x = map_of al x`

lemma map_of_upd_alist:

`  map_of (upd_alist k v al) = map_of al(k |-> v)`

lemma rem_alist_id:

`  k ∉ fst ` set al ==> rem_alist k al = al`

lemma map_of_rem_distinct_alist:

`  distinct (map fst al) ==> map_of (rem_alist k al) = (map_of al)(k := None)`

lemma map_of_rem_alist:

`  k' ≠ k ==> map_of (rem_alist k al) k' = map_of al k'`

### Trie

lemma lookup_empty:

`  lookup_trie (Trie [] []) as = []`

theorem lookup_update_trie:

```  ∀t v bs.
lookup_trie (update_trie t as vs) bs =
(if as = bs then vs else lookup_trie t bs)```

theorem insert_trie_conv:

`  insert_trie t as v = update_trie t as (v # lookup_trie t as)`

lemma in_set_lookup_trie_of_list:

`  (v ∈ set (lookup_trie (trie_of_list key vs) (key v))) = (v ∈ set vs)`

lemma in_set_lookup_trie_of_listD:

`  v ∈ set (lookup_trie (trie_of_list f vs) xs) ==> v ∈ set vs`