46167
|
1 |
(* Title: HOL/Library/AList.thy
|
|
2 |
Author: Lukas Bulwahn, TU Muenchen *)
|
|
3 |
|
|
4 |
header {* Abstract type of association lists with unique keys *}
|
|
5 |
|
|
6 |
theory AList
|
|
7 |
imports AList_Impl
|
|
8 |
begin
|
|
9 |
|
|
10 |
text {* This was based on some existing fragments in the AFP-Collection framework. *}
|
|
11 |
|
|
12 |
subsection {* Type @{text "('key, 'value) alist" } *}
|
|
13 |
|
|
14 |
typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
|
|
15 |
morphisms impl_of Alist
|
|
16 |
by(rule exI[where x="[]"]) simp
|
|
17 |
|
|
18 |
lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
|
|
19 |
by(simp add: impl_of_inject)
|
|
20 |
|
|
21 |
lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
|
|
22 |
by(simp add: impl_of_inject)
|
|
23 |
|
|
24 |
lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
|
|
25 |
using impl_of[of xs] by simp
|
|
26 |
|
|
27 |
lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
|
|
28 |
by(rule impl_of_inverse)
|
|
29 |
|
|
30 |
subsection {* Primitive operations *}
|
|
31 |
|
|
32 |
definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
|
|
33 |
where [code]: "lookup xs = map_of (impl_of xs)"
|
|
34 |
|
|
35 |
definition empty :: "('key, 'value) alist"
|
|
36 |
where [code del]: "empty = Alist []"
|
|
37 |
|
|
38 |
definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
|
|
39 |
where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))"
|
|
40 |
|
|
41 |
(* FIXME: we use an unoptimised delete operation. *)
|
|
42 |
definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
|
|
43 |
where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
|
|
44 |
|
|
45 |
definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
|
|
46 |
where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))"
|
|
47 |
|
|
48 |
definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
|
|
49 |
where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
|
|
50 |
|
|
51 |
definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
|
|
52 |
where
|
|
53 |
"map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))"
|
|
54 |
|
|
55 |
lemma impl_of_empty [code abstract]: "impl_of empty = []"
|
|
56 |
by (simp add: empty_def Alist_inverse)
|
|
57 |
|
|
58 |
lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)"
|
|
59 |
by (simp add: update_def Alist_inverse distinct_update)
|
|
60 |
|
|
61 |
lemma impl_of_delete [code abstract]:
|
|
62 |
"impl_of (delete k al) = AList_Impl.delete k (impl_of al)"
|
|
63 |
unfolding delete_def by (simp add: Alist_inverse distinct_delete)
|
|
64 |
|
|
65 |
lemma impl_of_map_entry [code abstract]:
|
|
66 |
"impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)"
|
|
67 |
unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
|
|
68 |
|
|
69 |
lemma distinct_map_fst_filter:
|
|
70 |
"distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
|
|
71 |
by (induct xs) auto
|
|
72 |
|
|
73 |
lemma impl_of_filter [code abstract]:
|
|
74 |
"impl_of (filter P xs) = List.filter P (impl_of xs)"
|
|
75 |
unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
|
|
76 |
|
|
77 |
lemma impl_of_map_default [code abstract]:
|
|
78 |
"impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)"
|
|
79 |
by (auto simp add: map_default_def Alist_inverse distinct_map_default)
|
|
80 |
|
|
81 |
subsection {* Abstract operation properties *}
|
|
82 |
|
|
83 |
(* FIXME: to be completed *)
|
|
84 |
|
|
85 |
lemma lookup_empty [simp]: "lookup empty k = None"
|
|
86 |
by(simp add: empty_def lookup_def Alist_inverse)
|
|
87 |
|
|
88 |
lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
|
|
89 |
by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
|
|
90 |
|
|
91 |
subsection {* Further operations *}
|
|
92 |
|
|
93 |
subsubsection {* Equality *}
|
|
94 |
|
|
95 |
instantiation alist :: (equal, equal) equal begin
|
|
96 |
|
|
97 |
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
|
|
98 |
|
|
99 |
instance
|
|
100 |
proof
|
|
101 |
qed (simp add: equal_alist_def impl_of_inject)
|
|
102 |
|
|
103 |
end
|
|
104 |
|
|
105 |
subsubsection {* Size *}
|
|
106 |
|
|
107 |
instantiation alist :: (type, type) size begin
|
|
108 |
|
|
109 |
definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
|
|
110 |
|
|
111 |
instance ..
|
|
112 |
|
|
113 |
end
|
|
114 |
|
|
115 |
subsection {* Quickcheck generators *}
|
|
116 |
|
|
117 |
notation fcomp (infixl "\<circ>>" 60)
|
|
118 |
notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
119 |
|
|
120 |
definition (in term_syntax)
|
|
121 |
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
|
|
122 |
where
|
|
123 |
"valterm_empty = Code_Evaluation.valtermify empty"
|
|
124 |
|
|
125 |
definition (in term_syntax)
|
|
126 |
valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
|
|
127 |
'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
|
|
128 |
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
|
|
129 |
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
|
|
130 |
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
|
|
131 |
|
|
132 |
fun (in term_syntax) random_aux_alist
|
|
133 |
where
|
|
134 |
"random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
|
|
135 |
|
|
136 |
instantiation alist :: (random, random) random
|
|
137 |
begin
|
|
138 |
|
|
139 |
definition random_alist
|
|
140 |
where
|
|
141 |
"random_alist i = random_aux_alist i i"
|
|
142 |
|
|
143 |
instance ..
|
|
144 |
|
|
145 |
end
|
|
146 |
|
|
147 |
no_notation fcomp (infixl "\<circ>>" 60)
|
|
148 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
149 |
|
|
150 |
instantiation alist :: (exhaustive, exhaustive) exhaustive
|
|
151 |
begin
|
|
152 |
|
|
153 |
fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
|
|
154 |
where
|
|
155 |
"exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
|
|
156 |
exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
|
|
157 |
|
|
158 |
instance ..
|
|
159 |
|
|
160 |
end
|
|
161 |
|
|
162 |
instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
|
|
163 |
begin
|
|
164 |
|
|
165 |
fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
|
|
166 |
where
|
|
167 |
"full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
|
|
168 |
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))"
|
|
169 |
|
|
170 |
instance ..
|
|
171 |
|
|
172 |
end
|
|
173 |
|
|
174 |
hide_const valterm_empty valterm_update random_aux_alist
|
|
175 |
|
|
176 |
hide_const (open) impl_of lookup empty update delete map_entry filter map_default
|
|
177 |
|
|
178 |
end |