header {* \isaheader{Tries without invariants} *}
theory Trie imports
Trie_Impl
begin
lemma rev_rev_image: "rev ` rev ` A = A"
by(auto intro: rev_image_eqI[where x="rev y", standard])
subsection {* Abstract type definition *}
typedef ('key, 'val) trie =
"{t :: ('key, 'val) Trie_Impl.trie. trie_invar t}"
morphisms impl_of Trie
proof
show "Trie_Impl.empty ∈ ?trie" by(simp)
qed
lemma trie_invar_impl_of [simp, intro]: "trie_invar (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 (Trie_Impl.empty)"
definition update :: "'key list => 'val => ('key, 'val) trie => ('key, 'val) trie"
where "update ks v t = Trie (Trie_Impl.update (impl_of t) ks v)"
definition delete :: "'key list => ('key, 'val) trie => ('key, 'val) trie"
where "delete ks t = Trie (Trie_Impl.delete (impl_of t) ks)"
definition lookup :: "('key, 'val) trie => 'key list => 'val option"
where "lookup t = Trie_Impl.lookup (impl_of t)"
definition isEmpty :: "('key, 'val) trie => bool"
where "isEmpty t = Trie_Impl.isEmpty (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))")
apply (auto simp add: trie_reverse_key_def)
done
lemma impl_of_empty [code abstract]: "impl_of empty = Trie_Impl.empty"
by(simp add: empty_def Trie_inverse)
lemma impl_of_update [code abstract]: "impl_of (update ks v t) = Trie_Impl.update (impl_of t) ks v"
by(simp add: update_def Trie_inverse trie_invar_update)
lemma impl_of_delete [code abstract]: "impl_of (delete ks t) = Trie_Impl.delete (impl_of t) ks"
by(simp add: delete_def Trie_inverse trie_invar_delete)
subsection {* Correctness of primitive operations *}
lemma lookup_empty [simp]: "lookup empty = Map.empty"
by(simp add: lookup_def empty_def Trie_inverse)
lemma lookup_update [simp]: "lookup (update ks v t) = (lookup t)(ks \<mapsto> v)"
by(simp add: lookup_def update_def Trie_inverse trie_invar_update lookup_update')
lemma lookup_delete [simp]: "lookup (delete ks t) = (lookup t)(ks := None)"
by(simp add: lookup_def delete_def Trie_inverse trie_invar_delete lookup_delete')
lemma isEmpty_lookup: "isEmpty t <-> lookup t = Map.empty"
by(simp add: isEmpty_def lookup_def isEmpty_lookup_empty)
lemma finite_dom_lookup: "finite (dom (lookup t))"
by(simp add: lookup_def finite_dom_trie_lookup)
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
qed(simp add: equal_trie_def impl_of_inject)
end
hide_const (open) empty lookup update delete iteratei isEmpty
end