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

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

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

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

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"

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

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

lemma lookup_delete [simp]: "DAList.lookup (delete k al) = (DAList.lookup al)(k := None)"

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

lemma update_conv_update_with: "DAList.update k v = update_with v k (λ_. v)"

lemma lookup_update [simp]: "DAList.lookup (DAList.update k v al) = (DAList.lookup al)(k ↦ v)"

lemma dom_lookup_keys: "dom (DAList.lookup al) = keys al"

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

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

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

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

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

lemma set_delete: "set (delete k al) = set al - {k} × UNIV"

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