author | haftmann |
Sun, 06 Sep 2015 22:14:51 +0200 | |
changeset 61127 | 76cd7f1ec257 |
parent 60919 | b0ba7799d05a |
child 61585 | a9599d3d7610 |
permissions | -rw-r--r-- |
46237 | 1 |
(* Title: HOL/Library/DAList.thy |
58806 | 2 |
Author: Lukas Bulwahn, TU Muenchen |
3 |
*) |
|
46167 | 4 |
|
58881 | 5 |
section \<open>Abstract type of association lists with unique keys\<close> |
46167 | 6 |
|
46237 | 7 |
theory DAList |
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
8 |
imports AList |
46167 | 9 |
begin |
10 |
||
58806 | 11 |
text \<open>This was based on some existing fragments in the AFP-Collection framework.\<close> |
46167 | 12 |
|
58806 | 13 |
subsection \<open>Preliminaries\<close> |
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
14 |
|
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
15 |
lemma distinct_map_fst_filter: |
58806 | 16 |
"distinct (map fst xs) \<Longrightarrow> distinct (map fst (List.filter P xs))" |
17 |
by (induct xs) auto |
|
18 |
||
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
19 |
|
58806 | 20 |
subsection \<open>Type @{text "('key, 'value) alist" }\<close> |
46167 | 21 |
|
58806 | 22 |
typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}" |
46507 | 23 |
morphisms impl_of Alist |
24 |
proof |
|
58806 | 25 |
show "[] \<in> {xs. (distinct o map fst) xs}" |
26 |
by simp |
|
46507 | 27 |
qed |
46167 | 28 |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
29 |
setup_lifting type_definition_alist |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
30 |
|
46167 | 31 |
lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys" |
58806 | 32 |
by (simp add: impl_of_inject) |
46167 | 33 |
|
34 |
lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys" |
|
58806 | 35 |
by (simp add: impl_of_inject) |
46167 | 36 |
|
37 |
lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))" |
|
58806 | 38 |
using impl_of[of xs] by simp |
46167 | 39 |
|
40 |
lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs" |
|
58806 | 41 |
by (rule impl_of_inverse) |
46167 | 42 |
|
58806 | 43 |
|
44 |
subsection \<open>Primitive operations\<close> |
|
46167 | 45 |
|
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
51143
diff
changeset
|
46 |
lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of . |
46167 | 47 |
|
58806 | 48 |
lift_definition empty :: "('key, 'value) alist" is "[]" |
49 |
by simp |
|
46167 | 50 |
|
47308 | 51 |
lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
52 |
is AList.update |
|
58806 | 53 |
by (simp add: distinct_update) |
46167 | 54 |
|
55 |
(* FIXME: we use an unoptimised delete operation. *) |
|
47308 | 56 |
lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
57 |
is AList.delete |
|
58806 | 58 |
by (simp add: distinct_delete) |
46167 | 59 |
|
58806 | 60 |
lift_definition map_entry :: |
61 |
"'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
|
47308 | 62 |
is AList.map_entry |
58806 | 63 |
by (simp add: distinct_map_entry) |
46167 | 64 |
|
47308 | 65 |
lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
66 |
is List.filter |
|
58806 | 67 |
by (simp add: distinct_map_fst_filter) |
46167 | 68 |
|
58806 | 69 |
lift_definition map_default :: |
70 |
"'key \<Rightarrow> 'value \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
|
47308 | 71 |
is AList.map_default |
58806 | 72 |
by (simp add: distinct_map_default) |
46167 | 73 |
|
58806 | 74 |
|
75 |
subsection \<open>Abstract operation properties\<close> |
|
46167 | 76 |
|
77 |
(* FIXME: to be completed *) |
|
78 |
||
79 |
lemma lookup_empty [simp]: "lookup empty k = None" |
|
58806 | 80 |
by (simp add: empty_def lookup_def Alist_inverse) |
46167 | 81 |
|
82 |
lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)" |
|
58806 | 83 |
by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv') |
46167 | 84 |
|
58806 | 85 |
|
86 |
subsection \<open>Further operations\<close> |
|
46167 | 87 |
|
58806 | 88 |
subsubsection \<open>Equality\<close> |
46167 | 89 |
|
58806 | 90 |
instantiation alist :: (equal, equal) equal |
91 |
begin |
|
46167 | 92 |
|
93 |
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys" |
|
94 |
||
95 |
instance |
|
60679 | 96 |
by standard (simp add: equal_alist_def impl_of_inject) |
46167 | 97 |
|
98 |
end |
|
99 |
||
58806 | 100 |
|
101 |
subsubsection \<open>Size\<close> |
|
46167 | 102 |
|
58806 | 103 |
instantiation alist :: (type, type) size |
104 |
begin |
|
46167 | 105 |
|
106 |
definition "size (al :: ('a, 'b) alist) = length (impl_of al)" |
|
107 |
||
108 |
instance .. |
|
109 |
||
110 |
end |
|
111 |
||
58806 | 112 |
|
113 |
subsection \<open>Quickcheck generators\<close> |
|
46167 | 114 |
|
115 |
notation fcomp (infixl "\<circ>>" 60) |
|
116 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
117 |
||
118 |
definition (in term_syntax) |
|
119 |
valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" |
|
58806 | 120 |
where "valterm_empty = Code_Evaluation.valtermify empty" |
46167 | 121 |
|
122 |
definition (in term_syntax) |
|
123 |
valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> |
|
124 |
'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> |
|
125 |
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> |
|
126 |
('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
|
127 |
[code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a" |
|
128 |
||
58806 | 129 |
fun (in term_syntax) random_aux_alist |
46167 | 130 |
where |
58806 | 131 |
"random_aux_alist i j = |
132 |
(if i = 0 then Pair valterm_empty |
|
133 |
else Quickcheck_Random.collapse |
|
134 |
(Random.select_weight |
|
135 |
[(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow> |
|
136 |
(\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))), |
|
137 |
(1, Pair valterm_empty)]))" |
|
46167 | 138 |
|
139 |
instantiation alist :: (random, random) random |
|
140 |
begin |
|
141 |
||
142 |
definition random_alist |
|
143 |
where |
|
144 |
"random_alist i = random_aux_alist i i" |
|
58806 | 145 |
|
46167 | 146 |
instance .. |
147 |
||
148 |
end |
|
149 |
||
150 |
no_notation fcomp (infixl "\<circ>>" 60) |
|
151 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
152 |
||
153 |
instantiation alist :: (exhaustive, exhaustive) exhaustive |
|
154 |
begin |
|
155 |
||
58806 | 156 |
fun exhaustive_alist :: |
157 |
"(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
46167 | 158 |
where |
58806 | 159 |
"exhaustive_alist f i = |
160 |
(if i = 0 then None |
|
161 |
else |
|
162 |
case f empty of |
|
163 |
Some ts \<Rightarrow> Some ts |
|
164 |
| None \<Rightarrow> |
|
165 |
exhaustive_alist |
|
166 |
(\<lambda>a. Quickcheck_Exhaustive.exhaustive |
|
167 |
(\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1)) |
|
168 |
(i - 1))" |
|
46167 | 169 |
|
170 |
instance .. |
|
171 |
||
172 |
end |
|
173 |
||
174 |
instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive |
|
175 |
begin |
|
176 |
||
58806 | 177 |
fun full_exhaustive_alist :: |
178 |
"(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> |
|
179 |
(bool \<times> term list) option" |
|
46167 | 180 |
where |
58806 | 181 |
"full_exhaustive_alist f i = |
182 |
(if i = 0 then None |
|
183 |
else |
|
184 |
case f valterm_empty of |
|
185 |
Some ts \<Rightarrow> Some ts |
|
186 |
| None \<Rightarrow> |
|
187 |
full_exhaustive_alist |
|
188 |
(\<lambda>a. |
|
189 |
Quickcheck_Exhaustive.full_exhaustive |
|
190 |
(\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1)) |
|
191 |
(i - 1)) |
|
192 |
(i - 1))" |
|
46167 | 193 |
|
194 |
instance .. |
|
195 |
||
196 |
end |
|
197 |
||
59581 | 198 |
|
199 |
section \<open>alist is a BNF\<close> |
|
200 |
||
60919 | 201 |
lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel |
202 |
by auto |
|
59581 | 203 |
|
46167 | 204 |
hide_const valterm_empty valterm_update random_aux_alist |
205 |
||
46171
19f68d7671f0
proper hiding of facts and constants in AList_Impl and AList theory
bulwahn
parents:
46167
diff
changeset
|
206 |
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def |
59581 | 207 |
hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel |
46167 | 208 |
|
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
209 |
end |