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_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def |
|
177 hide_const (open) impl_of lookup empty update delete map_entry filter map_default |
|
178 |
|
179 end |
|