# Theory HashMap

(*  Title:       Isabelle Collections Library
Author:      Andreas Lochbihler <andreas dot lochbihler at kit.edu>
Maintainer:  Andreas Lochbihler <andreas dot lochbihler at kit.edu>
*)
theory HashMap
imports HashMap_Impl
begin
text_raw ‹\label{thy:HashMap}›

(*@impl Map
@type 'a::hashable hm
@abbrv hm,h
Hash maps based on red-black trees.
*)

subsection "Type definition"

typedef (overloaded) ('k, 'v) hashmap = "{hm :: ('k :: hashable, 'v) hm_impl. HashMap_Impl.invar hm}"
morphisms impl_of_RBT_HM RBT_HM
proof
show "HashMap_Impl.empty () ∈ {hm. HashMap_Impl.invar hm}"
qed

lemma impl_of_RBT_HM_invar [simp, intro!]: "HashMap_Impl.invar (impl_of_RBT_HM hm)"
using impl_of_RBT_HM[of hm] by simp

lemma RBT_HM_imp_of_RBT_HM [code abstype]:
"RBT_HM (impl_of_RBT_HM hm) = hm"
by(fact impl_of_RBT_HM_inverse)

definition hm_empty_const :: "('k :: hashable, 'v) hashmap"
where "hm_empty_const = RBT_HM (HashMap_Impl.empty ())"

definition hm_empty :: "unit ⇒ ('k :: hashable, 'v) hashmap"
where "hm_empty = (λ_. hm_empty_const)"

definition "hm_lookup k hm == HashMap_Impl.lookup k (impl_of_RBT_HM hm)"

definition hm_update :: "('k :: hashable) ⇒ 'v ⇒ ('k, 'v) hashmap ⇒ ('k, 'v) hashmap"
where "hm_update k v hm = RBT_HM (HashMap_Impl.update k v (impl_of_RBT_HM hm))"

definition hm_update_dj :: "('k :: hashable) ⇒ 'v ⇒ ('k, 'v) hashmap ⇒ ('k, 'v) hashmap"
where "hm_update_dj = hm_update"

definition hm_delete :: "('k :: hashable) ⇒ ('k, 'v) hashmap ⇒ ('k, 'v) hashmap"
where "hm_delete k hm = RBT_HM (HashMap_Impl.delete k (impl_of_RBT_HM hm))"

definition hm_isEmpty :: "('k :: hashable, 'v) hashmap ⇒ bool"
where "hm_isEmpty hm = HashMap_Impl.isEmpty (impl_of_RBT_HM hm)"

(*definition hm_sel :: "('k :: hashable, 'v) hashmap ⇒ ('k × 'v ⇀ 'a) ⇀ 'a"
where "hm_sel hm = HashMap_Impl.sel (impl_of_RBT_HM hm)"*)

(*definition "hm_sel' = MapGA.sel_sel' hm_sel"*)

definition "hm_iteratei hm == HashMap_Impl.iteratei (impl_of_RBT_HM hm)"

lemma impl_of_hm_empty [simp, code abstract]:
"impl_of_RBT_HM (hm_empty_const) = HashMap_Impl.empty ()"

lemma impl_of_hm_update [simp, code abstract]:
"impl_of_RBT_HM (hm_update k v hm) = HashMap_Impl.update k v (impl_of_RBT_HM hm)"

lemma impl_of_hm_delete [simp, code abstract]:
"impl_of_RBT_HM (hm_delete k hm) = HashMap_Impl.delete k (impl_of_RBT_HM hm)"

subsection "Correctness w.r.t. Map"
text ‹
The next lemmas establish the correctness of the hashmap operations w.r.t. the
associated map. This is achieved by chaining the correctness lemmas of the
concrete hashmap w.r.t. the abstract hashmap and the correctness lemmas of the
abstract hashmap w.r.t. maps.
›

type_synonym ('k, 'v) hm = "('k, 'v) hashmap"

― ‹Abstract concrete hashmap to map›
definition "hm_α == ahm_α ∘ hm_α' ∘ impl_of_RBT_HM"

abbreviation (input) hm_invar :: "('k :: hashable, 'v) hashmap ⇒ bool"
where "hm_invar == λ_. True"

lemma hm_aux_correct:
"hm_α (hm_empty ()) = Map.empty "
"hm_lookup k m = hm_α m k"
"hm_α (hm_update k v m) = (hm_α m)(k↦v)"
"hm_α (hm_delete k m) = (hm_α m) | (-{k})"
by(auto simp add: hm_α_def hm_correct' hm_empty_def ahm_correct hm_lookup_def)

lemma hm_finite[simp, intro!]:
"finite (dom (hm_α m))"
proof(cases m)
case (RBT_HM m')
hence SS: "dom (hm_α m) ⊆ ⋃{ dom (lm.α lm) | lm hc. rm.α m' hc = Some lm }"
apply(clarsimp simp add: RBT_HM_inverse hm_α_def hm_α'_def [abs_def] ahm_α_def [abs_def])
apply(auto split: option.split_asm option.split)
done
moreover have "finite …" (is "finite (⋃?A)")
proof
have "{ dom (lm.α lm) | lm hc. rm.α m' hc = Some lm }
⊆ (λhc. dom (lm.α (the (rm.α m' hc)) ))  (dom (rm.α m'))"
(is "?S ⊆ _")
by force
thus "finite ?A" by(rule finite_subset) auto
next
fix M
assume "M ∈ ?A"
thus "finite M" by auto
qed
ultimately show ?thesis unfolding RBT_HM by(rule finite_subset)
qed

lemma hm_iteratei_impl:
"map_iterator (hm_iteratei m) (hm_α m)"
apply (unfold hm_α_def hm_iteratei_def o_def)
apply(rule iteratei_correct'[OF impl_of_RBT_HM_invar])
done

subsection "Integration in Isabelle Collections Framework"
text ‹
In this section, we integrate hashmaps into the Isabelle Collections Framework.
›

definition [icf_rec_def]: "hm_basic_ops ≡ ⦇
bmap_op_α = hm_α,
bmap_op_invar = λ_. True,
bmap_op_empty = hm_empty,
bmap_op_lookup = hm_lookup,
bmap_op_update = hm_update,
bmap_op_update_dj = hm_update, ― ‹TODO: Optimize bucket-ins here›
bmap_op_delete = hm_delete,
bmap_op_list_it = hm_iteratei
⦈"

setup Locale_Code.open_block
interpretation hm_basic: StdBasicMap hm_basic_ops
apply unfold_locales
apply (simp_all add: icf_rec_unf hm_aux_correct hm_iteratei_impl)
done
setup Locale_Code.close_block

definition [icf_rec_def]: "hm_ops ≡ hm_basic.dflt_ops"

setup Locale_Code.open_block
interpretation hm: StdMapDefs hm_ops .
interpretation hm: StdMap hm_ops
unfolding hm_ops_def
by (rule hm_basic.dflt_ops_impl)
interpretation hm: StdMap_no_invar hm_ops
setup Locale_Code.close_block

setup ‹ICF_Tools.revert_abbrevs "hm"›

lemma pi_hm[proper_it]:
shows "proper_it' hm_iteratei hm_iteratei"
apply (rule proper_it'I)
unfolding hm_iteratei_def HashMap_Impl.iteratei_alt_def
by (intro icf_proper_iteratorI)

interpretation pi_hm: proper_it_loc hm_iteratei hm_iteratei
apply unfold_locales
apply (rule pi_hm)
done

text ‹Code generator test›

definition test_codegen where "test_codegen ≡ (
hm.ball ,
hm.bex ,
hm.delete ,
hm.empty ,
hm.isEmpty ,
hm.isSng ,
hm.iterate ,
hm.iteratei ,
hm.list_it ,
hm.lookup ,
hm.restrict ,
hm.sel ,
hm.size ,
hm.size_abort ,
hm.sng ,
hm.to_list ,
hm.to_map ,
hm.update ,
hm.update_dj)"

export_code test_codegen checking SML

end