1(*  Title:      HOL/Library/DAList.thy
2    Author:     Lukas Bulwahn, TU Muenchen
3*)
4
5section \<open>Abstract type of association lists with unique keys\<close>
6
7theory DAList
8imports AList
9begin
10
11text \<open>This was based on some existing fragments in the AFP-Collection framework.\<close>
12
13subsection \<open>Preliminaries\<close>
14
15lemma distinct_map_fst_filter:
16  "distinct (map fst xs) \<Longrightarrow> distinct (map fst (List.filter P xs))"
17  by (induct xs) auto
18
19
20subsection \<open>Type \<open>('key, 'value) alist\<close>\<close>
21
22typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
23  morphisms impl_of Alist
24proof
25  show "[] \<in> {xs. (distinct \<circ> map fst) xs}"
26    by simp
27qed
28
29setup_lifting type_definition_alist
30
31lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
32  by (simp add: impl_of_inject)
33
34lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
35  by (simp add: impl_of_inject)
36
37lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
38  using impl_of[of xs] by simp
39
40lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
41  by (rule impl_of_inverse)
42
43
44subsection \<open>Primitive operations\<close>
45
46lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  .
47
48lift_definition empty :: "('key, 'value) alist" is "[]"
49  by simp
50
51lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
52  is AList.update
53  by (simp add: distinct_update)
54
55(* FIXME: we use an unoptimised delete operation. *)
56lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
57  is AList.delete
58  by (simp add: distinct_delete)
59
60lift_definition map_entry ::
61    "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
62  is AList.map_entry
63  by (simp add: distinct_map_entry)
64
65lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
66  is List.filter
67  by (simp add: distinct_map_fst_filter)
68
69lift_definition map_default ::
70    "'key \<Rightarrow> 'value \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
71  is AList.map_default
72  by (simp add: distinct_map_default)
73
74
75subsection \<open>Abstract operation properties\<close>
76
77(* FIXME: to be completed *)
78
79lemma lookup_empty [simp]: "lookup empty k = None"
80by (simp add: empty_def lookup_def Alist_inverse)
81
82lemma lookup_update:
83  "lookup (update k1 v xs) k2 = (if k1 = k2 then Some v else lookup xs k2)"
84by(transfer)(simp add: update_conv')
85
86lemma lookup_update_eq [simp]:
87  "k1 = k2 \<Longrightarrow> lookup (update k1 v xs) k2 = Some v"
88by(simp add: lookup_update)
89
90lemma lookup_update_neq [simp]:
91  "k1 \<noteq> k2 \<Longrightarrow> lookup (update k1 v xs) k2 = lookup xs k2"
92by(simp add: lookup_update)
93
94lemma update_update_eq [simp]:
95  "k1 = k2 \<Longrightarrow> update k2 v2 (update k1 v1 xs) = update k2 v2 xs"
96by(transfer)(simp add: update_conv')
97
98lemma 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')
100
101
102subsection \<open>Further operations\<close>
103
104subsubsection \<open>Equality\<close>
105
106instantiation alist :: (equal, equal) equal
107begin
108
109definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
110
111instance
112  by standard (simp add: equal_alist_def impl_of_inject)
113
114end
115
116
117subsubsection \<open>Size\<close>
118
119instantiation alist :: (type, type) size
120begin
121
122definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
123
124instance ..
125
126end
127
128
129subsection \<open>Quickcheck generators\<close>
130
131notation fcomp (infixl "\<circ>>" 60)
132notation scomp (infixl "\<circ>\<rightarrow>" 60)
133
134definition (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"
137
138definition (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"
144
145fun (in term_syntax) random_aux_alist
146where
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)]))"
154
155instantiation alist :: (random, random) random
156begin
157
158definition random_alist
159where
160  "random_alist i = random_aux_alist i i"
161
162instance ..
163
164end
165
166no_notation fcomp (infixl "\<circ>>" 60)
167no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
168
169instantiation alist :: (exhaustive, exhaustive) exhaustive
170begin
171
172fun exhaustive_alist ::
173  "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
174where
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))"
185
186instance ..
187
188end
189
190instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
191begin
192
193fun 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"
196where
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))"
209
210instance ..
211
212end
213
214
215section \<open>alist is a BNF\<close>
216
217lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel
218  by auto
219
220hide_const valterm_empty valterm_update random_aux_alist
221
222hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
223hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
224
225end
226