src/HOL/Library/DAList.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 67091 1393c2340eec permissions -rw-r--r--
improved code equations taken over from AFP
1 (*  Title:      HOL/Library/DAList.thy
2     Author:     Lukas Bulwahn, TU Muenchen
3 *)
5 section \<open>Abstract type of association lists with unique keys\<close>
7 theory DAList
8 imports AList
9 begin
11 text \<open>This was based on some existing fragments in the AFP-Collection framework.\<close>
13 subsection \<open>Preliminaries\<close>
15 lemma distinct_map_fst_filter:
16   "distinct (map fst xs) \<Longrightarrow> distinct (map fst (List.filter P xs))"
17   by (induct xs) auto
20 subsection \<open>Type \<open>('key, 'value) alist\<close>\<close>
22 typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
23   morphisms impl_of Alist
24 proof
25   show "[] \<in> {xs. (distinct \<circ> map fst) xs}"
26     by simp
27 qed
29 setup_lifting type_definition_alist
31 lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
34 lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
37 lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
38   using impl_of[of xs] by simp
40 lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
41   by (rule impl_of_inverse)
44 subsection \<open>Primitive operations\<close>
46 lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  .
48 lift_definition empty :: "('key, 'value) alist" is "[]"
49   by simp
51 lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
52   is AList.update
55 (* FIXME: we use an unoptimised delete operation. *)
56 lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
57   is AList.delete
60 lift_definition map_entry ::
61     "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
62   is AList.map_entry
65 lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
66   is List.filter
69 lift_definition map_default ::
70     "'key \<Rightarrow> 'value \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
71   is AList.map_default
75 subsection \<open>Abstract operation properties\<close>
77 (* FIXME: to be completed *)
79 lemma lookup_empty [simp]: "lookup empty k = None"
80 by (simp add: empty_def lookup_def Alist_inverse)
82 lemma lookup_update:
83   "lookup (update k1 v xs) k2 = (if k1 = k2 then Some v else lookup xs k2)"
86 lemma lookup_update_eq [simp]:
87   "k1 = k2 \<Longrightarrow> lookup (update k1 v xs) k2 = Some v"
90 lemma lookup_update_neq [simp]:
91   "k1 \<noteq> k2 \<Longrightarrow> lookup (update k1 v xs) k2 = lookup xs k2"
94 lemma update_update_eq [simp]:
95   "k1 = k2 \<Longrightarrow> update k2 v2 (update k1 v1 xs) = update k2 v2 xs"
98 lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
99   by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
102 subsection \<open>Further operations\<close>
104 subsubsection \<open>Equality\<close>
106 instantiation alist :: (equal, equal) equal
107 begin
109 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
111 instance
112   by standard (simp add: equal_alist_def impl_of_inject)
114 end
117 subsubsection \<open>Size\<close>
119 instantiation alist :: (type, type) size
120 begin
122 definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
124 instance ..
126 end
129 subsection \<open>Quickcheck generators\<close>
131 notation fcomp (infixl "\<circ>>" 60)
132 notation scomp (infixl "\<circ>\<rightarrow>" 60)
134 definition (in term_syntax)
135   valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
136   where "valterm_empty = Code_Evaluation.valtermify empty"
138 definition (in term_syntax)
139   valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
140   'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
141   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
142   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
143   [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
145 fun (in term_syntax) random_aux_alist
146 where
147   "random_aux_alist i j =
148     (if i = 0 then Pair valterm_empty
149      else Quickcheck_Random.collapse
150        (Random.select_weight
151          [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow>
152            (\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
153           (1, Pair valterm_empty)]))"
155 instantiation alist :: (random, random) random
156 begin
158 definition random_alist
159 where
160   "random_alist i = random_aux_alist i i"
162 instance ..
164 end
166 no_notation fcomp (infixl "\<circ>>" 60)
167 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
169 instantiation alist :: (exhaustive, exhaustive) exhaustive
170 begin
172 fun exhaustive_alist ::
173   "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
174 where
175   "exhaustive_alist f i =
176     (if i = 0 then None
177      else
178       case f empty of
179         Some ts \<Rightarrow> Some ts
180       | None \<Rightarrow>
181           exhaustive_alist
182             (\<lambda>a. Quickcheck_Exhaustive.exhaustive
183               (\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1))
184             (i - 1))"
186 instance ..
188 end
190 instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
191 begin
193 fun full_exhaustive_alist ::
194   "(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow>
195     (bool \<times> term list) option"
196 where
197   "full_exhaustive_alist f i =
198     (if i = 0 then None
199      else
200       case f valterm_empty of
201         Some ts \<Rightarrow> Some ts
202       | None \<Rightarrow>
203           full_exhaustive_alist
204             (\<lambda>a.
205               Quickcheck_Exhaustive.full_exhaustive
206                 (\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1))
207               (i - 1))
208             (i - 1))"
210 instance ..
212 end
215 section \<open>alist is a BNF\<close>
217 lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel
218   by auto
220 hide_const valterm_empty valterm_update random_aux_alist
222 hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
223 hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
225 end