Theory AssocList

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

theory AssocList imports

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"
  "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"
  "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)

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
  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
    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

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