Theory PAC_Assoc_Map_Rel

theory PAC_Assoc_Map_Rel
  imports PAC_Map_Rel

section ‹Hash Map as association list›

type_synonym ('k, 'v) hash_assoc = ('k × 'v) list

definition hassoc_map_rel_raw :: (('k, 'v) hash_assoc × _) set where
  hassoc_map_rel_raw = br map_of (λ_. True)

abbreviation hassoc_map_assn :: ('k  'v option)  ('k, 'v) hash_assoc  assn where
  hassoc_map_assn  pure (hassoc_map_rel_raw)

lemma hassoc_map_rel_raw_empty[simp]:
  ([], m)  hassoc_map_rel_raw  m = Map.empty
  (p, Map.empty)  hassoc_map_rel_raw  p = []
  hassoc_map_assn Map.empty [] = emp
  by (auto simp: hassoc_map_rel_raw_def br_def pure_def)

definition hassoc_new :: ('k, 'v) hash_assoc Heapwhere
  hassoc_new = return []

  lemma precise_hassoc_map_assn: precise hassoc_map_assn
    by (auto intro!: precise_pure)
     (auto simp: single_valued_def hassoc_map_rel_raw_def

  definition hassoc_isEmpty :: "('k × 'v) list  bool Heap" where
   "hassoc_isEmpty ht  return (length ht = 0)"

 interpretation hassoc: bind_map_empty hassoc_map_assn hassoc_new
    by unfold_locales
     (auto intro: precise_hassoc_map_assn
         simp: ent_refl_true hassoc_new_def
       intro!: return_cons_rule)

  interpretation hassoc: bind_map_is_empty hassoc_map_assn hassoc_isEmpty
    by unfold_locales
      (auto simp: precise_hassoc_map_assn hassoc_isEmpty_def ent_refl_true
       intro!: precise_pure return_cons_rule)

  definition "op_assoc_empty  IICF_Map.op_map_empty"

  interpretation hassoc: map_custom_empty op_assoc_empty
    by unfold_locales (simp add: op_assoc_empty_def)

  lemmas [sepref_fr_rules] = hassoc.empty_hnr[folded op_assoc_empty_def]

  definition hassoc_update :: "'k  'v  ('k, 'v) hash_assoc  ('k, 'v) hash_assoc Heap" where
   "hassoc_update k v ht = return ((k, v ) # ht)"

  lemma hassoc_map_assn_Cons:
     hassoc_map_assn (m) (p) A hassoc_map_assn (m(k  v)) ((k, v) # p) * true
     by (auto simp: hassoc_map_rel_raw_def pure_def br_def)

  interpretation hassoc: bind_map_update hassoc_map_assn hassoc_update
    by unfold_locales
     (auto intro!: return_cons_rule
      simp: hassoc_update_def hassoc_map_assn_Cons)

  definition hassoc_delete :: 'k  ('k, 'v) hash_assoc  ('k, 'v) hash_assoc Heap where
    hassoc_delete k ht = return (filter (λ(a, b). a  k) ht)

  lemma hassoc_map_of_filter_all:
    map_of p |` (- {k}) = map_of (filter (λ(a, b). a  k) p)
    apply (induction p)
    apply (auto simp: restrict_map_def fun_eq_iff split: if_split)
    apply presburger+

  lemma hassoc_map_assn_hassoc_delete: <hassoc_map_assn m p> hassoc_delete k p <hassoc_map_assn (m |` (- {k}))>t
   by (auto simp: hassoc_delete_def hassoc_map_rel_raw_def pure_def br_def
         intro!: return_cons_rule)

  interpretation hassoc: bind_map_delete hassoc_map_assn hassoc_delete
    by unfold_locales
     (auto intro: hassoc_map_assn_hassoc_delete)

  definition hassoc_lookup :: 'k  ('k, 'v) hash_assoc  'v option Heap where
    hassoc_lookup k ht = return (map_of ht k)

  lemma hassoc_map_assn_hassoc_lookup:
    <hassoc_map_assn m p> hassoc_lookup k p <λr. hassoc_map_assn m p *  (r = m k)>t
     by (auto simp: hassoc_lookup_def hassoc_map_rel_raw_def pure_def br_def
           intro!: return_cons_rule)

  interpretation hassoc: bind_map_lookup hassoc_map_assn hassoc_lookup
    by unfold_locales
     (rule hassoc_map_assn_hassoc_lookup)

  setup Locale_Code.open_block
  interpretation hassoc: gen_contains_key_by_lookup hassoc_map_assn hassoc_lookup
    by unfold_locales
  setup Locale_Code.close_block

  interpretation hassoc: bind_map_contains_key hassoc_map_assn hassoc.contains_key
    by unfold_locales

subsection ‹Conversion from assoc to other map›

definition hash_of_assoc_map where
hash_of_assoc_map xs = fold (λ(k, v) m. if m k  None then m else m(k  v)) xs Map.empty

lemma map_upd_map_add_left:
  m(a   b) ++ m' = m ++ (if a  dom m' then m'(a   b) else m')
proof -
  have m' a = Some y  m(a  b) ++ m' = m ++ m' for y
    by (metis (no_types) fun_upd_triv fun_upd_upd map_add_assoc map_add_empty map_add_upd
  then show ?thesis
    by auto

lemma fold_map_of_alt:
  fold (λ(k, v) m. if m k  None then m else m(k  v)) xs m' = map_of xs ++ m'
  by (induction xs arbitrary: m')
    (auto simp: map_upd_map_add_left)

lemma map_of_alt_def:
  map_of xs = hash_of_assoc_map xs
  using fold_map_of_alt[of xs Map.empty]
  unfolding hash_of_assoc_map_def
  by auto

definition hashmap_conv where
  [simp]: hashmap_conv x = x

lemma hash_of_assoc_map_id:
  (hash_of_assoc_map, hashmap_conv)  hassoc_map_rel_raw  Id
  by (auto intro!: fun_relI simp: hassoc_map_rel_raw_def br_def map_of_alt_def)

definition hassoc_map_rel where
  hassoc_map_rel K V = hassoc_map_rel_raw O K,Vmap_rel

lemma hassoc_map_rel_def:
  K,V hassoc_map_rel = hassoc_map_rel_raw O K,Vmap_rel
  unfolding relAPP_def hassoc_map_rel_internal_def
  by auto