# Theory DAList

theory DAList
imports AList
```(*  Title:      HOL/Library/DAList.thy
Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹Abstract type of association lists with unique keys›

theory DAList
imports AList
begin

text ‹This was based on some existing fragments in the AFP-Collection framework.›

subsection ‹Preliminaries›

lemma distinct_map_fst_filter:
"distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
by (induct xs) auto

subsection ‹Type @{text "('key, 'value) alist" }›

typedef ('key, 'value) alist = "{xs :: ('key × 'value) list. (distinct o map fst) xs}"
morphisms impl_of Alist
proof
show "[] ∈ {xs. (distinct o map fst) xs}"
by simp
qed

setup_lifting type_definition_alist

lemma alist_ext: "impl_of xs = impl_of ys ==> xs = ys"

lemma alist_eq_iff: "xs = ys <-> impl_of xs = impl_of ys"

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

lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
by (rule impl_of_inverse)

subsection ‹Primitive operations›

lift_definition lookup :: "('key, 'value) alist => 'key => 'value option" is map_of  .

lift_definition empty :: "('key, 'value) alist" is "[]"
by simp

lift_definition update :: "'key => 'value => ('key, 'value) alist => ('key, 'value) alist"
is AList.update

(* FIXME: we use an unoptimised delete operation. *)
lift_definition delete :: "'key => ('key, 'value) alist => ('key, 'value) alist"
is AList.delete

lift_definition map_entry ::
"'key => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
is AList.map_entry

lift_definition filter :: "('key × 'value => bool) => ('key, 'value) alist => ('key, 'value) alist"
is List.filter

lift_definition map_default ::
"'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
is AList.map_default

subsection ‹Abstract operation properties›

(* FIXME: to be completed *)

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

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

subsection ‹Further operations›

subsubsection ‹Equality›

instantiation alist :: (equal, equal) equal
begin

definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"

instance
by default (simp add: equal_alist_def impl_of_inject)

end

subsubsection ‹Size›

instantiation alist :: (type, type) size
begin

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

instance ..

end

subsection ‹Quickcheck generators›

notation fcomp (infixl "o>" 60)
notation scomp (infixl "o->" 60)

definition (in term_syntax)
valterm_empty :: "('key :: typerep, 'value :: typerep) alist × (unit => Code_Evaluation.term)"
where "valterm_empty = Code_Evaluation.valtermify empty"

definition (in term_syntax)
valterm_update :: "'key :: typerep × (unit => Code_Evaluation.term) =>
'value :: typerep × (unit => Code_Evaluation.term) =>
('key, 'value) alist × (unit => Code_Evaluation.term) =>
('key, 'value) alist × (unit => Code_Evaluation.term)" where
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {·} k {·} v {·}a"

fun (in term_syntax) random_aux_alist
where
"random_aux_alist i j =
(if i = 0 then Pair valterm_empty
else Quickcheck_Random.collapse
(Random.select_weight
[(i, Quickcheck_Random.random j o-> (λk. Quickcheck_Random.random j o->
(λv. random_aux_alist (i - 1) j o-> (λa. Pair (valterm_update k v a))))),
(1, Pair valterm_empty)]))"

instantiation alist :: (random, random) random
begin

definition random_alist
where
"random_alist i = random_aux_alist i i"

instance ..

end

no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o->" 60)

instantiation alist :: (exhaustive, exhaustive) exhaustive
begin

fun exhaustive_alist ::
"(('a, 'b) alist => (bool × term list) option) => natural => (bool × term list) option"
where
"exhaustive_alist f i =
(if i = 0 then None
else
case f empty of
Some ts => Some ts
| None =>
exhaustive_alist
(λa. Quickcheck_Exhaustive.exhaustive
(λk. Quickcheck_Exhaustive.exhaustive (λv. f (update k v a)) (i - 1)) (i - 1))
(i - 1))"

instance ..

end

instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
begin

fun full_exhaustive_alist ::
"(('a, 'b) alist × (unit => term) => (bool × term list) option) => natural =>
(bool × term list) option"
where
"full_exhaustive_alist f i =
(if i = 0 then None
else
case f valterm_empty of
Some ts => Some ts
| None =>
full_exhaustive_alist
(λa.
Quickcheck_Exhaustive.full_exhaustive
(λk. Quickcheck_Exhaustive.full_exhaustive (λv. f (valterm_update k v a)) (i - 1))
(i - 1))
(i - 1))"

instance ..

end

section ‹alist is a BNF›

lift_definition map :: "('a => 'b) => ('k, 'a) alist => ('k, 'b) alist"
is "λf xs. List.map (map_prod id f) xs" by simp

lift_definition set :: "('k, 'v) alist => 'v set"
is "λxs. snd ` List.set xs" .

lift_definition rel :: "('a => 'b => bool) => ('k, 'a) alist => ('k, 'b) alist => bool"
is "λR xs ys. list_all2 (rel_prod op = R) xs ys" .

bnf "('k, 'v) alist"
map: map
sets: set
bd: natLeq
wits: empty
rel: rel
proof (unfold OO_Grp_alt)
show "map id = id" by (rule ext, transfer) (simp add: prod.map_id0)
next
fix f g
show "map (g o f) = map g o map f"
by (rule ext, transfer) (simp add: prod.map_comp)
next
fix x f g
assume "(!!z. z ∈ set x ==> f z = g z)"
then show "map f x = map g x" by transfer force
next
fix f
show "set o map f = op ` f o set"
by (rule ext, transfer) (simp add: image_image)
next
fix x
show "ordLeq3 (card_of (set x)) natLeq"
by transfer (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
next
fix R S
show "rel R OO rel S ≤ rel (R OO S)"
by (rule predicate2I, transfer)
(auto simp: list.rel_compp prod.rel_compp[of "op =", unfolded eq_OO])
next
fix R
show "rel R = (λx y. ∃z. z ∈ {x. set x ⊆ {(x, y). R x y}} ∧ map fst z = x ∧ map snd z = y)"
unfolding fun_eq_iff by transfer (fastforce simp: list.in_rel o_def intro:
exI[of _ "List.map (λp. ((fst p, fst (snd p)), (fst p, snd (snd p)))) z" for z]
exI[of _ "List.map (λp. (fst (fst p), snd (fst p), snd (snd p))) z" for z])
next
fix z assume "z ∈ set empty"
then show False by transfer simp