Theory Containers.AssocList

(*  Title:      Containers/AssocList.thy
    Author:     Andreas Lochbihler, KIT *)

theory AssocList imports
  "HOL-Library.DAList" 
begin

section ‹Additional operations for associative lists›

subsection ‹Operations on the raw type›

primrec update_with_aux :: "'val ⇒ 'key ⇒ ('val ⇒ 'val) ⇒ ('key × 'val) list ⇒ ('key × 'val) list"
where
  "update_with_aux v k f [] = [(k, f v)]"
| "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"

text ‹
  Do not use @{term "AList.delete"} because this traverses all the list even if it has found the key.
  We do not have to keep going because we use the invariant that keys are distinct.
›
fun delete_aux :: "'key ⇒ ('key × 'val) list ⇒ ('key × 'val) list"
where
  "delete_aux k [] = []"
| "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"

definition zip_with_index_from :: "nat ⇒ 'a list ⇒ (nat × 'a) list" where
  "zip_with_index_from n xs = zip [n..<n + length xs] xs"

abbreviation zip_with_index :: "'a list ⇒ (nat × 'a) list" where
  "zip_with_index ≡ zip_with_index_from 0"

lemma update_conv_update_with_aux:
  "AList.update k v xs = update_with_aux v k (λ_. v) xs"
by(induct xs) simp_all

lemma map_of_update_with_aux':
  "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k ↦ (case map_of ps k of None ⇒ f v | Some v ⇒ f v))) k'"
by(induct ps) auto

lemma map_of_update_with_aux:
  "map_of (update_with_aux v k f ps) = (map_of ps)(k ↦ (case map_of ps k of None ⇒ f v | Some v ⇒ f v))"
by(simp add: fun_eq_iff map_of_update_with_aux')

lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} ∪ fst ` set ps"
  by (induct ps) auto

lemma distinct_update_with_aux [simp]:
  "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
by(induct ps)(auto simp add: dom_update_with_aux)

lemma set_update_with_aux:
  "distinct (map fst xs) 
  ⟹ set (update_with_aux v k f xs) = (set xs - {k} × UNIV ∪ {(k, f (case map_of xs k of None ⇒ v | Some v ⇒ v))})"
by(induct xs)(auto intro: rev_image_eqI)

lemma set_delete_aux: "distinct (map fst xs) ⟹ set (delete_aux k xs) = set xs - {k} × UNIV"
apply(induct xs)
apply simp_all
apply clarsimp
apply(fastforce intro: rev_image_eqI)
done

lemma dom_delete_aux: "distinct (map fst ps) ⟹ fst ` set (delete_aux k ps) = fst ` set ps - {k}"
by(auto simp add: set_delete_aux)

lemma distinct_delete_aux [simp]:
  "distinct (map fst ps) ⟹ distinct (map fst (delete_aux k ps))"
proof(induct ps)
  case Nil thus ?case by simp
next
  case (Cons a ps)
  obtain k' v where a: "a = (k', v)" by(cases a)
  show ?case
  proof(cases "k' = k")
    case True with Cons a show ?thesis by simp
  next
    case False
    with Cons a have "k' ∉ fst ` set ps" "distinct (map fst ps)" by simp_all
    with False a have "k' ∉ fst ` set (delete_aux k ps)"
      by(auto dest!: dom_delete_aux[where k=k])
    with Cons a show ?thesis by simp
  qed
qed

lemma map_of_delete_aux':
  "distinct (map fst xs) ⟹ map_of (delete_aux k xs) = (map_of xs)(k := None)"
by(induct xs)(fastforce simp add: map_of_eq_None_iff fun_upd_twist)+

lemma map_of_delete_aux:
  "distinct (map fst xs) ⟹ map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
by(simp add: map_of_delete_aux')

lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] ⟷ ts = [] ∨ (∃v. ts = [(k, v)])"
by(cases ts)(auto split: if_split_asm)

lemma zip_with_index_from_simps [simp, code]:
  "zip_with_index_from n [] = []"
  "zip_with_index_from n (x # xs) = (n, x) # zip_with_index_from (Suc n) xs"
  by(simp_all add: zip_with_index_from_def upt_rec del: upt.upt_Suc)

lemma zip_with_index_from_append [simp]:
  "zip_with_index_from n (xs @ ys) = zip_with_index_from n xs @ zip_with_index_from (n + length xs) ys"
  by(simp add: zip_with_index_from_def zip_append[symmetric] upt_add_eq_append[symmetric] del: zip_append)
    (simp add: add.assoc)

lemma zip_with_index_from_conv_nth:
  "zip_with_index_from n xs = map (λi. (n + i, xs ! i)) [0..<length xs]"
  by(induction xs rule: rev_induct)(auto simp add: nth_append)

lemma map_of_zip_with_index_from [simp]:
  "map_of (zip_with_index_from n xs) i = (if i ≥ n ∧ i < n + length xs then Some (xs ! (i - n)) else None)"
  by(auto simp add: zip_with_index_from_def set_zip intro: exI[where x="i - n"])

lemma map_of_map': "map_of (map (λ(k, v). (k, f k v)) xs) x = map_option (f x) (map_of xs x)"
  by (induct xs)(auto)


subsection ‹Operations on the abstract type @{typ "('a, 'b) alist"}›

lift_definition update_with :: "'v ⇒ 'k ⇒ ('v ⇒ 'v) ⇒ ('k, 'v) alist ⇒ ('k, 'v) alist"
  is "update_with_aux" by simp

lift_definition delete :: "'k ⇒ ('k, 'v) alist ⇒ ('k, 'v) alist" is "delete_aux"
by simp

lift_definition keys :: "('k, 'v) alist ⇒ 'k set" is "set ∘ map fst" .

lift_definition set :: "('key, 'val) alist ⇒ ('key × 'val) set"
is "List.set" .

lift_definition map_values :: "('key ⇒ 'val ⇒ 'val') ⇒ ('key, 'val) alist ⇒ ('key, 'val') alist" is
  "λf. map (λ(x,y). (x, f x y))"
  by(simp add: o_def split_def)

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

lemma lookup_delete [simp]: "DAList.lookup (delete k al) = (DAList.lookup al)(k := None)"
by transfer(simp add: map_of_delete_aux')

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

lemma update_conv_update_with: "DAList.update k v = update_with v k (λ_. v)"
by(rule ext)(transfer, simp add: update_conv_update_with_aux)

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

lemma dom_lookup_keys: "dom (DAList.lookup al) = keys al"
by transfer(simp add: dom_map_of_conv_image_fst)

lemma keys_empty [simp]: "keys DAList.empty = {}"
by transfer simp

lemma keys_update_with [simp]: "keys (update_with v k f al) = insert k (keys al)"
by(simp add: dom_lookup_keys[symmetric])

lemma keys_update [simp]: "keys (DAList.update k v al) = insert k (keys al)"
by(simp add: update_conv_update_with)

lemma keys_delete [simp]: "keys (delete k al) = keys al - {k}"
by(simp add: dom_lookup_keys[symmetric])

lemma set_empty [simp]: "set DAList.empty = {}"
by transfer simp

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

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

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

lemma size_dalist_transfer [transfer_rule]:
  includes lifting_syntax
  shows "(pcr_alist (=) (=) ===> (=)) length size"
unfolding size_alist_def[abs_def]
by transfer_prover

lemma size_eq_card_dom_lookup: "size al = card (dom (DAList.lookup al))"
by transfer (metis comp_apply distinct_card dom_map_of_conv_image_fst image_set length_map)

hide_const (open) update_with keys set delete

end