header {* \isaheader{Map implementation via tries} *}
theory TrieMapImpl imports
Trie
"../gen_algo/MapGA"
begin
subsection {* Operations *}
type_synonym ('k, 'v) tm = "('k, 'v) trie"
definition tm_α :: "('k, 'v) tm => 'k list \<rightharpoonup> 'v"
where "tm_α = Trie.lookup"
abbreviation (input) tm_invar :: "('k, 'v) tm => bool"
where "tm_invar ≡ λ_. True"
definition tm_empty :: "unit => ('k, 'v) tm"
where "tm_empty == (λ_::unit. Trie.empty)"
definition tm_lookup :: "'k list => ('k, 'v) tm => 'v option"
where "tm_lookup k t = Trie.lookup t k"
definition tm_update :: "'k list => 'v => ('k, 'v) tm => ('k, 'v) tm"
where "tm_update = Trie.update"
definition "tm_update_dj == tm_update"
definition tm_delete :: "'k list => ('k, 'v) tm => ('k, 'v) tm"
where "tm_delete = Trie.delete"
definition tm_iteratei :: "('k, 'v) tm => ('k list × 'v, 'σ) set_iterator"
where
"tm_iteratei = Trie.iteratei"
definition "tm_add == it_add tm_update tm_iteratei"
definition "tm_add_dj == tm_add"
definition tm_isEmpty :: "('k, 'v) tm => bool"
where "tm_isEmpty = Trie.isEmpty"
definition "tm_sel == iti_sel tm_iteratei"
definition "tm_sel' == iti_sel_no_map tm_iteratei"
definition "tm_ball == sel_ball tm_sel"
definition "tm_to_list == it_map_to_list tm_iteratei"
definition "list_to_tm == gen_list_to_map tm_empty tm_update"
lemmas tm_defs =
tm_α_def
tm_empty_def
tm_lookup_def
tm_update_def
tm_update_dj_def
tm_delete_def
tm_iteratei_def
tm_add_def
tm_add_dj_def
tm_isEmpty_def
tm_sel_def
tm_sel'_def
tm_ball_def
tm_to_list_def
list_to_tm_def
subsection {* Correctness *}
lemma tm_empty_impl: "map_empty tm_α tm_invar tm_empty"
by(unfold_locales)(simp_all add: tm_defs fun_eq_iff)
lemma tm_lookup_impl: "map_lookup tm_α tm_invar tm_lookup"
by(unfold_locales)(auto simp add: tm_defs)
lemma tm_update_impl: "map_update tm_α tm_invar tm_update"
by(unfold_locales)(simp_all add: tm_defs)
lemma tm_update_dj_impl: "map_update_dj tm_α tm_invar tm_update_dj"
unfolding tm_update_dj_def
by(rule map_update.update_dj_by_update)(rule tm_update_impl)
lemma tm_delete_impl: "map_delete tm_α tm_invar tm_delete"
by(unfold_locales)(simp_all add: tm_defs)
lemma tm_α_finite [simp, intro!]:
"finite (dom (tm_α m))"
by(simp add: tm_defs finite_dom_lookup)
lemma tm_is_finite_map: "finite_map tm_α tm_invar"
by unfold_locales simp
lemma tm_iteratei_impl: "map_iteratei tm_α tm_invar tm_iteratei"
by(unfold_locales)(simp, unfold tm_defs, rule iteratei_correct)
lemma tm_add_impl: "map_add tm_α tm_invar tm_add"
unfolding tm_add_def
by(rule it_add_correct tm_iteratei_impl tm_update_impl)+
lemma tm_add_dj_impl: "map_add_dj tm_α tm_invar tm_add_dj"
unfolding tm_add_dj_def
by(rule map_add.add_dj_by_add tm_add_impl)+
lemma tm_isEmpty_impl: "map_isEmpty tm_α tm_invar tm_isEmpty"
by unfold_locales(simp add: tm_defs isEmpty_lookup)
lemma tm_sel_impl: "map_sel tm_α tm_invar tm_sel"
unfolding tm_sel_def
by(rule iti_sel_correct tm_iteratei_impl)+
lemma tm_sel'_impl: "map_sel' tm_α tm_invar tm_sel'"
unfolding tm_sel'_def
by(rule iti_sel'_correct tm_iteratei_impl)+
lemma tm_ball_impl: "map_ball tm_α tm_invar tm_ball"
unfolding tm_ball_def
by(rule sel_ball_correct tm_sel_impl)+
lemma tm_to_list_impl: "map_to_list tm_α tm_invar tm_to_list"
unfolding tm_to_list_def
by(rule it_map_to_list_correct tm_iteratei_impl)+
lemma list_to_tm_impl: "list_to_map tm_α tm_invar list_to_tm"
unfolding list_to_tm_def
by(rule gen_list_to_map_correct tm_empty_impl tm_update_impl)+
interpretation tm: map_empty tm_α tm_invar tm_empty
using tm_empty_impl .
interpretation tm: map_lookup tm_α tm_invar tm_lookup
using tm_lookup_impl .
interpretation tm: map_update tm_α tm_invar tm_update
using tm_update_impl .
interpretation tm: map_update_dj tm_α tm_invar tm_update_dj
using tm_update_dj_impl .
interpretation tm: map_delete tm_α tm_invar tm_delete
using tm_delete_impl .
interpretation tm: finite_map tm_α tm_invar
using tm_is_finite_map .
interpretation tm: map_iteratei tm_α tm_invar tm_iteratei
using tm_iteratei_impl .
interpretation tm: map_add tm_α tm_invar tm_add
using tm_add_impl .
interpretation tm: map_add_dj tm_α tm_invar tm_add_dj
using tm_add_dj_impl .
interpretation tm: map_isEmpty tm_α tm_invar tm_isEmpty
using tm_isEmpty_impl .
interpretation tm: map_sel tm_α tm_invar tm_sel
using tm_sel_impl .
interpretation tm: map_sel' tm_α tm_invar tm_sel'
using tm_sel'_impl .
interpretation tm: map_ball tm_α tm_invar tm_ball
using tm_ball_impl .
interpretation tm: map_to_list tm_α tm_invar tm_to_list
using tm_to_list_impl .
interpretation tm: list_to_map tm_α tm_invar list_to_tm
using list_to_tm_impl .
declare tm.finite[simp del, rule del]
lemmas tm_correct =
tm.empty_correct
tm.lookup_correct
tm.update_correct
tm.update_dj_correct
tm.delete_correct
tm.add_correct
tm.add_dj_correct
tm.isEmpty_correct
tm.ball_correct
tm.to_list_correct
tm.to_map_correct
subsection "Code Generation"
export_code
tm_empty
tm_lookup
tm_update
tm_update_dj
tm_delete
tm_iteratei
tm_add
tm_add_dj
tm_isEmpty
tm_sel
tm_sel'
tm_ball
tm_to_list
list_to_tm
in SML
module_name TrieMap
file -
end