Theory Collections.HashMap

(*  Title:       Isabelle Collections Library
    Author:      Andreas Lochbihler <andreas dot lochbihler at kit.edu>
    Maintainer:  Andreas Lochbihler <andreas dot lochbihler at kit.edu>
*)
section ‹\isaheader{Hash Maps}›
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}"
    by(simp add: HashMap_Impl.empty_correct')
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 ()"
by(simp add: hm_empty_const_def empty_correct' RBT_HM_inverse)

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)"
by(simp add: hm_update_def update_correct' RBT_HM_inverse)

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)"
by(simp add: hm_delete_def delete_correct' RBT_HM_inverse)

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 
  by unfold_locales (simp add: icf_rec_unf)
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.add ,
  hm.add_dj ,
  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