Theory HashMap_Impl

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
header {* \isaheader{Hash maps implementation} *}
theory HashMap_Impl
imports 
  "../common/Misc" 
  ListMapImpl
  RBTMapImpl 
  "../common/HashCode"
begin

text {*
  We use a red-black tree instead of an indexed array. This
  has the disadvantage of being more complex, however we need not bother
  about a fixed-size array and rehashing if the array becomes too full.

  The entries of the red-black tree are lists of (key,value) pairs.
*}

subsection {* Abstract Hashmap *}
text {*
  We first specify the behavior of our hashmap on the level of maps.
  We will then show that our implementation based on hashcode-map and bucket-map 
  is a correct implementation of this specification.
*}
type_synonym 
  ('k,'v) abs_hashmap = "hashcode \<rightharpoonup> ('k \<rightharpoonup> 'v)"

  -- "Map entry of map by function"
abbreviation "map_entry k f m == m(k := f (m k))"


  -- "Invariant: Buckets only contain entries with the right hashcode and there are no empty buckets"
definition ahm_invar:: "('k::hashable,'v) abs_hashmap => bool" 
  where "ahm_invar m == 
    (∀hc cm k. m hc = Some cm ∧ k∈dom cm --> hashcode k = hc) ∧ 
    (∀hc cm. m hc = Some cm --> cm ≠ empty)"



  -- "Abstract a hashmap to the corresponding map"
definition ahm_α where
  "ahm_α m k == case m (hashcode k) of 
    None => None |
    Some cm => cm k"

  -- "Lookup an entry"
definition ahm_lookup :: "'k::hashable => ('k,'v) abs_hashmap => 'v option" 
  where "ahm_lookup k m == (ahm_α m) k"

  -- "The empty hashmap"
definition ahm_empty :: "('k::hashable,'v) abs_hashmap" 
  where "ahm_empty = empty"

  -- "Update/insert an entry"
definition ahm_update where
  "ahm_update k v m ==
    case m (hashcode k) of
      None => m (hashcode k \<mapsto> [k \<mapsto> v]) |
      Some cm => m (hashcode k \<mapsto> cm (k \<mapsto> v))
  "

  -- "Delete an entry"
definition ahm_delete where 
  "ahm_delete k m == map_entry (hashcode k) 
    (λv. case v of 
      None => None | 
      Some bm => (
        if bm |` (- {k}) = empty then
          None
        else
          Some ( bm |` (- {k}))
      )
    ) m
  "

definition ahm_isEmpty where
  "ahm_isEmpty m == m=Map.empty"

text {*
  Now follow correctness lemmas, that relate the hashmap operations to
  operations on the corresponding map. Those lemmas are named op\_correct, where
  op is the operation.
*}

lemma ahm_invarI: "[| 
  !!hc cm k. [|m hc = Some cm; k∈dom cm|] ==> hashcode k = hc;
  !!hc cm. [| m hc = Some cm |] ==> cm ≠ empty
  |] ==> ahm_invar m"
  by (unfold ahm_invar_def) blast

lemma ahm_invarD: "[| ahm_invar m; m hc = Some cm; k∈dom cm |] ==> hashcode k = hc"
  by (unfold ahm_invar_def) blast

lemma ahm_invarDne: "[| ahm_invar m; m hc = Some cm |] ==> cm ≠ empty"
  by (unfold ahm_invar_def) blast

lemma ahm_invar_bucket_not_empty[simp]: 
  "ahm_invar m ==> m hc ≠ Some Map.empty"
  by (auto dest: ahm_invarDne)

lemmas ahm_lookup_correct = ahm_lookup_def

lemma ahm_empty_correct: 
  "ahm_α ahm_empty = empty"
  "ahm_invar ahm_empty"
  apply (rule ext)
  apply (unfold ahm_empty_def) 
  apply (auto simp add: ahm_α_def intro: ahm_invarI split: option.split)
  done


lemma ahm_update_correct: 
  "ahm_α (ahm_update k v m) = ahm_α m (k \<mapsto> v)"
  "ahm_invar m ==> ahm_invar (ahm_update k v m)"
  apply (rule ext)
  apply (unfold ahm_update_def)
  apply (auto simp add: ahm_α_def split: option.split)
  apply (rule ahm_invarI)
  apply (auto dest: ahm_invarD ahm_invarDne split: split_if_asm)
  apply (rule ahm_invarI)
  apply (auto dest: ahm_invarD split: split_if_asm)
  apply (drule (1) ahm_invarD)
  apply auto
  done

lemma fun_upd_apply_ne: "x≠y ==> (f(x:=v)) y = f y"
  by simp

lemma cancel_one_empty_simp: "m |` (-{k}) = Map.empty <-> dom m ⊆ {k}"
proof
  assume "m |` (- {k}) = Map.empty"
  hence "{} = dom (m |` (-{k}))" by auto
  also have "… = dom m - {k}" by auto
  finally show "dom m ⊆ {k}" by blast
next
  assume "dom m ⊆ {k}"
  hence "dom m - {k} = {}" by auto
  hence "dom (m |` (-{k})) = {}" by auto
  thus "m |` (-{k}) = Map.empty" by (simp only: dom_empty_simp)
qed
  
lemma ahm_delete_correct: 
  "ahm_α (ahm_delete k m) = (ahm_α m) |` (-{k})"
  "ahm_invar m ==> ahm_invar (ahm_delete k m)"
  apply (rule ext)
  apply (unfold ahm_delete_def)
  apply (auto simp add: ahm_α_def Let_def Map.restrict_map_def 
              split: option.split)[1]
  apply (drule_tac x=x in fun_cong)
  apply (auto)[1]
  apply (rule ahm_invarI)
  apply (auto split: split_if_asm option.split_asm dest: ahm_invarD)
  apply (drule (1) ahm_invarD)
  apply (auto simp add: restrict_map_def split: split_if_asm option.split_asm)
  done

lemma ahm_isEmpty_correct: "ahm_invar m ==> ahm_isEmpty m <-> ahm_α m = Map.empty"
proof
  assume "ahm_invar m" "ahm_isEmpty m"
  thus "ahm_α m = Map.empty"
    by (auto simp add: ahm_isEmpty_def ahm_α_def intro: ext)
next
  assume I: "ahm_invar m" 
    and E: "ahm_α m = Map.empty"

  show "ahm_isEmpty m"
  proof (rule ccontr)
    assume "¬ahm_isEmpty m"
    then obtain hc bm where MHC: "m hc = Some bm"
      by (unfold ahm_isEmpty_def)
         (blast elim: nempty_dom dest: domD)
    from ahm_invarDne[OF I, OF MHC] obtain k v where
      BMK: "bm k = Some v"
      by (blast elim: nempty_dom dest: domD)
    from ahm_invarD[OF I, OF MHC] BMK have [simp]: "hashcode k = hc"
      by auto
    hence "ahm_α m k = Some v"
      by (simp add: ahm_α_def MHC BMK)
    with E show False by simp
  qed
qed

lemmas ahm_correct = ahm_empty_correct ahm_lookup_correct ahm_update_correct 
                     ahm_delete_correct ahm_isEmpty_correct

  -- "Bucket entries correspond to map entries"
lemma ahm_be_is_e:
  assumes I: "ahm_invar m"
  assumes A: "m hc = Some bm" "bm k = Some v"
  shows "ahm_α m k = Some v"
  using A
  apply (auto simp add: ahm_α_def split: option.split dest: ahm_invarD[OF I])
  apply (frule ahm_invarD[OF I, where k=k])
  apply auto
  done

  -- "Map entries correspond to bucket entries"
lemma ahm_e_is_be: "[|
  ahm_α m k = Some v; 
  !!bm. [|m (hashcode k) = Some bm; bm k = Some v |] ==> P
  |] ==> P"
  by (unfold ahm_α_def)
     (auto split: option.split_asm)

subsection {* Concrete Hashmap *}
text {*
  In this section, we define the concrete hashmap that is made from the 
  hashcode map and the bucket map.

  We then show the correctness of the operations w.r.t. the abstract hashmap, and
  thus, indirectly, w.r.t. the corresponding map.
*}

type_synonym
  ('k,'v) hm_impl = "(hashcode, ('k,'v) lm) rm"

subsubsection "Operations"

  -- "Auxiliary function: Apply function to value of an entry"
definition rm_map_entry 
  :: "hashcode => ('v option => 'v option) => (hashcode, 'v) rm => (hashcode,'v) rm" 
  where 
  "rm_map_entry k f m ==
      case rm_lookup k m of
        None => (
          case f None of 
            None => m |
            Some v => rm_update k v m
        ) |
        Some v => (
          case f (Some v) of
            None => rm_delete k m |
            Some v' => rm_update k v' m
        )
    "

  -- "Empty hashmap"
definition empty :: "unit => ('k :: hashable, 'v) hm_impl" where "empty == rm_empty"

  -- "Update/insert entry"
definition update :: "'k::hashable => 'v => ('k,'v) hm_impl => ('k,'v) hm_impl"
  where 
  "update k v m == 
   let hc = hashcode k in
     case rm_lookup hc m of
       None => rm_update hc (lm_update k v (lm_empty ())) m |
       Some bm => rm_update hc (lm_update k v bm) m" 

  -- "Lookup value by key"
definition lookup :: "'k::hashable => ('k,'v) hm_impl => 'v option" where
  "lookup k m ==
   case rm_lookup (hashcode k) m of
     None => None |
     Some lm => lm_lookup k lm"

  -- "Delete entry by key"
definition delete :: "'k::hashable => ('k,'v) hm_impl => ('k,'v) hm_impl" where
  "delete k m ==
   rm_map_entry (hashcode k) 
     (λv. case v of 
       None => None | 
       Some lm => (
         let lm' = lm_delete k lm 
         in  if lm_isEmpty lm' then None else Some lm'
       )
     ) m"

  -- "Select arbitrary entry"
definition sel :: "('k::hashable,'v) hm_impl => ('k × 'v => 'r option) => 'r option" 
  where "sel m f == rm_sel m (λ(hc, lm). lm_sel lm f)"

  -- "Emptiness check"
definition "isEmpty == rm_isEmpty"

  -- "Interruptible iterator"
definition "iteratei m c f σ0 ==
  rm_iteratei m c (λ(hc, lm) σ. 
    lm_iteratei lm c f σ
  ) σ0"

lemma iteratei_alt_def :
  "iteratei m = set_iterator_image snd (
     set_iterator_product (rm_iteratei m) (λhclm. lm_iteratei (snd hclm)))"
proof -
  have aux: "!!c f. (λ(hc, lm). lm_iteratei lm c f) = (λm. lm_iteratei (snd m) c f)"
    by auto
  show ?thesis
    unfolding set_iterator_product_def set_iterator_image_alt_def 
      iteratei_def[abs_def] aux
    by (simp add: split_beta)
qed


subsubsection "Correctness w.r.t. Abstract HashMap"
text {*
  The following lemmas establish the correctness of the operations w.r.t. the 
  abstract hashmap.

  They have the naming scheme op\_correct', where op is the name of the 
  operation.
*}

  -- "Abstract concrete hashmap to abstract hashmap"
definition hm_α' where "hm_α' m == λhc. case rm_α m hc of
  None => None |
  Some lm => Some (lm_α lm)"

  -- "Invariant for concrete hashmap: 
    The hashcode-map and bucket-maps satisfy their invariants and
    the invariant of the corresponding abstract hashmap is satisfied.
  "

definition "invar m == ahm_invar (hm_α' m)"

lemma rm_map_entry_correct:
  "rm_α (rm_map_entry k f m) = (rm_α m)(k := f (rm_α m k))"
  apply (auto 
    simp add: rm_map_entry_def rm.delete_correct rm.lookup_correct rm.update_correct
    split: option.split)
  apply (auto simp add: Map.restrict_map_def fun_upd_def intro: ext)
  done

lemma empty_correct': 
  "hm_α' (empty ()) = ahm_empty"
  "invar (empty ())"
by(simp_all add: hm_α'_def empty_def ahm_empty_def rm_correct invar_def ahm_invar_def)

lemma lookup_correct': 
  "invar m ==> lookup k m = ahm_lookup k (hm_α' m)"
  apply (unfold lookup_def invar_def)
  apply (auto split: option.split 
              simp add: ahm_lookup_def ahm_α_def hm_α'_def 
                        rm_correct lm_correct)
  done

lemma update_correct': 
  "invar m ==> hm_α' (update k v m) = ahm_update k v (hm_α' m)"
  "invar m ==> invar (update k v m)"
proof -
  assume "invar m"
  thus "hm_α' (update k v m) = ahm_update k v (hm_α' m)"
    apply (unfold invar_def)
    apply (rule ext)
    apply (auto simp add: update_def ahm_update_def hm_α'_def Let_def 
                          rm_correct lm_correct 
                split: option.split)
    done
  thus "invar m ==> invar (update k v m)"
    by (simp add: invar_def ahm_update_correct)
qed

lemma delete_correct':
  "invar m ==> hm_α' (delete k m) = ahm_delete k (hm_α' m)"
  "invar m ==> invar (delete k m)"
proof -
  assume "invar m"
  thus "hm_α' (delete k m) = ahm_delete k (hm_α' m)"
    apply (unfold invar_def)
    apply (rule ext)
    apply (auto simp add: delete_def ahm_delete_def hm_α'_def rm_map_entry_correct
                          rm_correct lm_correct Let_def 
                split: option.split option.split_asm)
    done
  thus "invar (delete k m)" using `invar m`
    by (simp add: ahm_delete_correct invar_def)
qed

lemma isEmpty_correct':
  "invar hm ==> isEmpty hm <-> ahm_α (hm_α' hm) = Map.empty"
apply (simp add: isEmpty_def rm.isEmpty_correct invar_def
                 ahm_isEmpty_correct[unfolded ahm_isEmpty_def, symmetric])
by (auto simp add: hm_α'_def ahm_α_def fun_eq_iff split: option.split_asm)

lemma sel_correct':
  assumes "invar hm"
  shows "[| sel hm f = Some r; !!u v. [| ahm_α (hm_α' hm) u = Some v; f (u, v) = Some r |] ==> P |] ==> P"
  and "[| sel hm f = None; ahm_α (hm_α' hm) u = Some v |] ==> f (u, v) = None"
proof -
  assume sel: "sel hm f = Some r"
    and P: "!!u v. [|ahm_α (hm_α' hm) u = Some v; f (u, v) = Some r|] ==> P"
  from `invar hm` have IA: "ahm_invar (hm_α' hm)" by(simp add: invar_def)
  from TrueI sel obtain hc lm where "rm_α hm hc = Some lm"
    and "lm_sel lm f = Some r"
    unfolding sel_def by (rule rm.sel_someE) simp
  from TrueI `lm_sel lm f = Some r`
  obtain k v where "lm_α lm k = Some v" "f (k, v) = Some r"
    by(rule lm.sel_someE)
  from `rm_α hm hc = Some lm` have "hm_α' hm hc = Some (lm_α lm)"
    by(simp add: hm_α'_def)
  with IA have "ahm_α (hm_α' hm) k = Some v" using `lm_α lm k = Some v`
    by(rule ahm_be_is_e)
  thus P using `f (k, v) = Some r` by(rule P)
next
  assume sel: "sel hm f = None" 
    and α: "ahm_α (hm_α' hm) u = Some v"
  from `invar hm` have IA: "ahm_invar (hm_α' hm)" by(simp add: invar_def)
  from α obtain lm where α_u: "hm_α' hm (hashcode u) = Some lm"
    and "lm u = Some v" by (rule ahm_e_is_be)
  from α_u obtain lmc where "rm_α hm (hashcode u) = Some lmc" "lm = lm_α lmc" 
    by(auto simp add: hm_α'_def split: option.split_asm)
  with `lm u = Some v` have "lm_α lmc u = Some v" by simp
  from sel rm.sel_noneD [OF TrueI _ `rm_α hm (hashcode u) = Some lmc`, 
         of "(λ(hc, lm). lm_sel lm f)"]
  have "lm_sel lmc f = None" unfolding sel_def by simp  
  with TrueI show "f (u, v) = None" using `lm_α lmc u = Some v` by(rule lm.sel_noneD)
qed

lemma iteratei_correct':
  assumes invar: "invar hm"
  shows "map_iterator (iteratei hm) (ahm_α (hm_α' hm))"
proof -
  from map_iteratei.iteratei_rule[OF rm_iteratei_impl]
  have it_rm: "map_iterator (rm_iteratei hm) (rm_α hm)" by simp

  from map_iteratei.iteratei_rule[OF lm_iteratei_impl]
  have it_lm: "!!lm. map_iterator (lm_iteratei lm) (lm_α lm)" by simp
 
  from set_iterator_product_correct [OF it_rm, of "λhclm. lm_iteratei (snd hclm)"
     "λhclm. map_to_set (lm_α (snd hclm))", OF it_lm]
  have it_prod: "set_iterator
         (set_iterator_product (rm_iteratei hm) (λhclm. lm_iteratei (snd hclm)))
         (SIGMA hclm:map_to_set (rm_α hm). map_to_set (lm_α (snd hclm)))" by simp
 
  show ?thesis unfolding iteratei_alt_def
  proof (rule set_iterator_image_correct[OF it_prod])
    from invar
    show "inj_on snd
       (SIGMA hclm:map_to_set (rm_α hm). map_to_set (lm_α (snd hclm)))"
      apply (simp add: inj_on_def invar_def ahm_invar_def hm_α'_def Ball_def 
                       map_to_set_def split: option.splits)
      apply (metis domI option.inject)
    done
  next
    from invar
    show "map_to_set (ahm_α (hm_α' hm)) =
          snd ` (SIGMA hclm:map_to_set (rm_α hm). map_to_set (lm_α (snd hclm)))" 
      apply (simp add: inj_on_def invar_def ahm_invar_def hm_α'_def Ball_def 
                       map_to_set_def set_eq_iff image_iff split: option.splits)
      apply (auto simp add: dom_def ahm_α_def split: option.splits)
    done
  qed
qed


lemmas hm_correct' = empty_correct' lookup_correct' update_correct' 
                     delete_correct' isEmpty_correct' 
                     sel_correct' iteratei_correct'
lemmas hm_invars = empty_correct'(2) update_correct'(2) 
                   delete_correct'(2)

hide_const (open) empty invar lookup update delete sel isEmpty iteratei

end