(* ID: $Id: TrieList.thy,v 1.1 2006/01/04 13:44:14 nipkow Exp $ Author: Tobias Nipkow *) header "Trie (List Version)" 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 (simp add:trie_of_list_def) apply (simp add:trie_of_list_def) apply(simp add:insert_trie_conv lookup_update_trie) apply blast done thus ?thesis by(simp add:trie_of_list_def) 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 (simp add:trie_of_list_def) apply (simp add:trie_of_list_def) 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
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'
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