Theory Assoc_List

section ‹\isaheader{The type of associative lists}›
theory Assoc_List 
  imports 
  "HOL-Library.AList" 
  "../Iterator/SetIteratorOperations"
begin

subsection ‹Type ‹('a, 'b) assoc_list››

typedef ('k, 'v) assoc_list = "{xs :: ('k × 'v) list. distinct (map fst xs)}"
morphisms impl_of Assoc_List
by(rule exI[where x="[]"]) simp

lemma assoc_list_ext: "impl_of xs = impl_of ys ⟹ xs = ys"
by(simp add: impl_of_inject)

lemma expand_assoc_list_eq: "xs = ys ⟷ impl_of xs = impl_of ys"
by(simp add: impl_of_inject)

lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of al))"
using impl_of[of al] by simp

lemma impl_of_distinct_full [simp, intro]: "distinct (impl_of al)"
using impl_of_distinct[of al] 
unfolding distinct_map by simp

lemma Assoc_List_impl_of [code abstype]: "Assoc_List (impl_of al) = al"
by(rule impl_of_inverse)

subsection ‹Primitive operations›

definition empty :: "('k, 'v) assoc_list"
where [code del]: "empty = Assoc_List []"

definition lookup :: "('k, 'v) assoc_list ⇒ 'k ⇒ 'v option"
where [code]: "lookup al = map_of (impl_of al)" 

definition update_with :: "'v ⇒ 'k ⇒ ('v ⇒ 'v) ⇒ ('k, 'v) assoc_list ⇒ ('k, 'v) assoc_list"
where [code del]: "update_with v k f al = Assoc_List (AList.update_with_aux v k f (impl_of al))"

definition delete :: "'k ⇒ ('k, 'v) assoc_list ⇒ ('k, 'v) assoc_list"
where [code del]: "delete k al = Assoc_List (AList.delete_aux k (impl_of al))"

definition iteratei :: "('k, 'v) assoc_list ⇒ ('s⇒bool) ⇒ ('k × 'v ⇒ 's ⇒ 's) ⇒ 's ⇒ 's" 
where [code]: "iteratei al c f = foldli (impl_of al) c f"

lemma impl_of_empty [code abstract]: "impl_of empty = []"
by(simp add: empty_def Assoc_List_inverse)

lemma impl_of_update_with [code abstract]:
  "impl_of (update_with v k f al) = AList.update_with_aux v k f (impl_of al)"
by(simp add: update_with_def Assoc_List_inverse)

lemma impl_of_delete [code abstract]:
  "impl_of (delete k al) = AList.delete_aux k (impl_of al)"
by(simp add: delete_def Assoc_List_inverse)

subsection ‹Abstract operation properties›

lemma lookup_empty [simp]: "lookup empty k = None"
by(simp add: empty_def lookup_def Assoc_List_inverse)

lemma lookup_empty': "lookup empty = Map.empty"
by(rule ext) simp

lemma lookup_update_with [simp]: 
  "lookup (update_with v k f al) = (lookup al)(k ↦ case lookup al k of None ⇒ f v | Some v ⇒ f v)"
by(simp add: lookup_def update_with_def Assoc_List_inverse map_of_update_with_aux)

lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
by(simp add: lookup_def delete_def Assoc_List_inverse distinct_delete map_of_delete_aux')

lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup m))"
by(simp add: lookup_def finite_dom_map_of)

lemma iteratei_correct:
  "map_iterator (iteratei m) (lookup m)"
unfolding iteratei_def[abs_def] lookup_def map_to_set_def
by (simp add: set_iterator_foldli_correct)


subsection ‹Derived operations›

definition update :: "'key ⇒ 'val ⇒ ('key, 'val) assoc_list ⇒ ('key, 'val) assoc_list"
where "update k v = update_with v k (λ_. v)"

definition set :: "('key, 'val) assoc_list ⇒ ('key × 'val) set"
where "set al = List.set (impl_of al)"


lemma lookup_update [simp]: "lookup (update k v al) = (lookup al)(k ↦ v)"
by(simp add: update_def split: option.split)

lemma set_empty [simp]: "set empty = {}"
by(simp add: set_def empty_def Assoc_List_inverse)

lemma set_update_with:
  "set (update_with v k f al) = 
  (set al - {k} × UNIV ∪ {(k, f (case lookup al k of None ⇒ v | Some v ⇒ v))})"
by(simp add: set_def update_with_def Assoc_List_inverse set_update_with_aux lookup_def)

lemma set_update: "set (update k v al) = (set al - {k} × UNIV ∪ {(k, v)})"
by(simp add: update_def set_update_with)

lemma set_delete: "set (delete k al) = set al - {k} × UNIV"
by(simp add: set_def delete_def Assoc_List_inverse set_delete_aux)

subsection ‹Type classes›

instantiation assoc_list :: (equal, equal) equal begin

definition "equal_class.equal (al :: ('a, 'b) assoc_list) al' == impl_of al = impl_of al'"

instance
proof
qed (simp add: equal_assoc_list_def impl_of_inject)

end

instantiation assoc_list :: (type, type) size begin

definition "size (al :: ('a, 'b) assoc_list) = length (impl_of al)"

instance ..
end

hide_const (open) impl_of empty lookup update_with set update delete iteratei 

subsection ‹@{const map_ran}›

text ‹@{term map_ran} with more general type - lemmas replicated from AList in HOL/Library›

hide_const (open) map_ran

primrec
  map_ran :: "('key ⇒ 'val ⇒ 'val') ⇒ ('key × 'val) list ⇒ ('key × 'val') list"
where
    "map_ran f [] = []"
  | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"

lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
  by (induct al) auto

lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
  by (induct al) auto

lemma distinct_map_ran: "distinct (map fst al) ⟹ distinct (map fst (map_ran f al))"
  by (induct al) (auto simp add: dom_map_ran)

lemma map_ran_filter: "map_ran f [(a, _)←ps. fst p ≠ a] = [(a, _)←map_ran f ps. fst p ≠ a]"
  by (induct ps) auto

lemma clearjunk_map_ran: "AList.clearjunk (map_ran f al) 
  = map_ran f (AList.clearjunk al)"
  by (induct al rule: clearjunk.induct) (simp_all add: AList.delete_eq map_ran_filter)

text ‹new lemmas and definitions›

lemma map_ran_cong [fundef_cong]:
  "⟦ al = al'; ⋀k v. (k, v) ∈ set al ⟹ f k v = g k v ⟧ ⟹ map_ran f al = map_ran g al'"
by hypsubst_thin (induct al', auto)

lemma size_list_delete: "size_list f (AList.delete a al) ≤ size_list f al"
by(induct al) simp_all

lemma size_list_clearjunk: "size_list f (AList.clearjunk al) ≤ size_list f al"
by(induct al)(auto simp add: clearjunk_delete intro: le_trans[OF size_list_delete])

lemma set_delete_conv: "set (AList.delete a al) = set al - ({a} × UNIV)"
proof(induct al)
  case (Cons kv al)
  thus ?case by(cases kv) auto
qed simp

lemma set_clearjunk_subset: "set (AList.clearjunk al) ⊆ set al"
by(induct al)(auto simp add: clearjunk_delete set_delete_conv)

lemma map_ran_conv_map:
  "map_ran f xs = map (λ(k, v). (k, f k v)) xs"
by(induct xs) auto

lemma card_dom_map_of: "distinct (map fst al) ⟹ card (dom (map_of al)) = length al"
by(induct al)(auto simp add: card_insert_if finite_dom_map_of dom_map_of_conv_image_fst)

lemma map_of_map_inj_fst:
  assumes "inj f"
  shows "map_of (map (λ(k, v). (f k, v)) xs) (f x) = map_of xs x"
by(induct xs)(auto dest: injD[OF ‹inj f›])

lemma length_map_ran [simp]: "length (map_ran f xs) = length xs"
by(induct xs) simp_all

lemma length_update: 
  "length (AList.update k v xs) 
  = (if k ∈ fst ` set xs then length xs else Suc (length xs))"
by(induct xs) simp_all

lemma length_distinct: 
  "distinct (map fst xs) ⟹ length (AList.delete k xs) 
  = (if k ∈ fst ` set xs then length xs - 1 else length xs)"
  by(induct xs)(auto split: if_split_asm simp add: in_set_conv_nth)

lemma finite_Assoc_List_set_image:
  assumes "finite (Assoc_List.set ` A)"
  shows "finite A"
proof -
  have "Assoc_List.set ` A = set ` Assoc_List.impl_of ` A"
    by (auto simp add: Assoc_List.set_def)
  with assms finite_set_image have "finite (Assoc_List.impl_of ` A)" by auto
  with assoc_list_ext show ?thesis by (metis inj_onI finite_imageD)
qed

end