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 ‹('key, 'value) alist››
typedef ('key, 'value) alist = "{xs :: ('key × 'value) list. (distinct ∘ 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"
by (simp add: impl_of_inject)
lemma alist_eq_iff: "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 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
by (simp add: distinct_update)
lift_definition delete :: "'key ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
is AList.delete
by (simp add: distinct_delete)
lift_definition map_entry ::
"'key ⇒ ('value ⇒ 'value) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
is AList.map_entry
by (simp add: distinct_map_entry)
lift_definition filter :: "('key × 'value ⇒ bool) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
is List.filter
by (simp add: distinct_map_fst_filter)
lift_definition map_default ::
"'key ⇒ 'value ⇒ ('value ⇒ 'value) ⇒ ('key, 'value) alist ⇒ ('key, 'value) alist"
is AList.map_default
by (simp add: distinct_map_default)
subsection ‹Abstract operation properties›
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 standard (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 "∘>" 60)
notation scomp (infixl "∘→" 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 ∘→ (λk. Quickcheck_Random.random j ∘→
(λv. random_aux_alist (i - 1) j ∘→ (λ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 "∘>" 60)
no_notation scomp (infixl "∘→" 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_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k × 'v) list"] for map: map rel: rel
by auto
hide_const valterm_empty valterm_update random_aux_alist
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
end