Theory Collections.Trie2

```(*  Title:       Isabelle Collections Library
Author:      Andreas Lochbihler <andreas dot lochbihler at kit.edu>
Maintainer:  Andreas Lochbihler <andreas dot lochbihler at kit.edu>
*)
theory Trie2 imports
Trie_Impl
begin

(*<*)
lemma rev_rev_image: "rev ` rev ` A = A"
by(auto intro: rev_image_eqI[where x="rev y" for y])
(*>*)

subsection ‹Abstract type definition›

typedef ('key, 'val) trie =
"{t :: ('key, 'val) Trie.trie. invar_trie t}"
morphisms impl_of Trie
proof
show "empty_trie ∈ ?trie" by(simp)
qed

lemma invar_trie_impl_of [simp, intro]: "invar_trie (impl_of t)"
using impl_of[of t] by simp

lemma Trie_impl_of [code abstype]: "Trie (impl_of t) = t"
by(rule impl_of_inverse)

subsection ‹Primitive operations›

definition empty :: "('key, 'val) trie"
where "empty = Trie (empty_trie)"

definition update :: "'key list ⇒ 'val ⇒ ('key, 'val) trie ⇒ ('key, 'val) trie"
where "update ks v t = Trie (update_trie ks v (impl_of t))"

definition delete :: "'key list ⇒ ('key, 'val) trie ⇒ ('key, 'val) trie"
where "delete ks t = Trie (delete_trie ks (impl_of t))"

definition lookup :: "('key, 'val) trie ⇒ 'key list ⇒ 'val option"
where "lookup t = lookup_trie (impl_of t)"

definition isEmpty :: "('key, 'val) trie ⇒ bool"
where "isEmpty t = is_empty_trie (impl_of t)"

definition iteratei :: "('key, 'val) trie ⇒ ('key list × 'val, 'σ) set_iterator"
where "iteratei t = set_iterator_image trie_reverse_key (Trie_Impl.iteratei (impl_of t))"

lemma iteratei_code[code] :
"iteratei t c f = Trie_Impl.iteratei (impl_of t) c (λ(ks, v). f (rev ks, v))"
unfolding iteratei_def set_iterator_image_alt_def
apply (subgoal_tac "(λx. f (trie_reverse_key x)) = (λ(ks, v). f (rev ks, v))")
done

lemma impl_of_empty [code abstract]: "impl_of empty = empty_trie"

lemma impl_of_update [code abstract]: "impl_of (update ks v t) = update_trie ks v (impl_of t)"

lemma impl_of_delete [code abstract]: "impl_of (delete ks t) = delete_trie ks (impl_of t)"

subsection ‹Correctness of primitive operations›

lemma lookup_empty [simp]: "lookup empty = Map.empty"

lemma lookup_update [simp]: "lookup (update ks v t) = (lookup t)(ks ↦ v)"
by(simp add: lookup_def update_def Trie_inverse invar_trie_update lookup_update')

lemma lookup_delete [simp]: "lookup (delete ks t) = (lookup t)(ks := None)"
by(simp add: lookup_def delete_def Trie_inverse invar_trie_delete lookup_delete')

lemma isEmpty_lookup: "isEmpty t ⟷ lookup t = Map.empty"

lemma finite_dom_lookup: "finite (dom (lookup t))"

lemma iteratei_correct:
"map_iterator (iteratei m) (lookup m)"
proof -
note it_base = Trie_Impl.trie_iteratei_correct [of "impl_of m"]
show ?thesis
unfolding iteratei_def lookup_def
apply (rule set_iterator_image_correct [OF it_base])
apply (simp_all add: set_eq_iff image_iff inj_on_def)
done
qed

subsection ‹Type classes›

instantiation trie :: (equal, equal) equal begin

definition "equal_class.equal (t :: ('a, 'b) trie) t' = (impl_of t = impl_of t')"

instance
proof