Theory PAC_Assoc_Map_Rel

theory PAC_Assoc_Map_Rel
  imports PAC_Map_Rel
begin

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 Heap›where
  ‹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
      br_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+
    done

  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
           hassoc_map_of_filter_all
         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
             hassoc_map_of_filter_all
           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
        map_le_iff_map_add_commute)
  then show ?thesis
    by auto
qed

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_internal_def:
  ‹hassoc_map_rel K V = hassoc_map_rel_raw O ⟨K,V⟩map_rel›

lemma hassoc_map_rel_def:
  ‹⟨K,V⟩ hassoc_map_rel = hassoc_map_rel_raw O ⟨K,V⟩map_rel›
  unfolding relAPP_def hassoc_map_rel_internal_def
  by auto


end