27 |
51 |
28 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |
52 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |
29 "keys m = dom (lookup m)" |
53 "keys m = dom (lookup m)" |
30 |
54 |
31 definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where |
55 definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where |
32 "ordered_keys m = sorted_list_of_set (keys m)" |
56 "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])" |
33 |
57 |
34 definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where |
58 definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where |
35 "is_empty m \<longleftrightarrow> dom (lookup m) = {}" |
59 "is_empty m \<longleftrightarrow> keys m = {}" |
36 |
60 |
37 definition size :: "('a, 'b) mapping \<Rightarrow> nat" where |
61 definition size :: "('a, 'b) mapping \<Rightarrow> nat" where |
38 "size m = (if finite (dom (lookup m)) then card (dom (lookup m)) else 0)" |
62 "size m = (if finite (keys m) then card (keys m) else 0)" |
39 |
63 |
40 definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
64 definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
41 "replace k v m = (if lookup m k = None then m else update k v m)" |
65 "replace k v m = (if k \<in> keys m then update k v m else m)" |
42 |
66 |
43 definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
67 definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
44 "default k v m = (if lookup m k = None then update k v m else m)" |
68 "default k v m = (if k \<in> keys m then m else update k v m)" |
45 |
69 |
46 definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
70 definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
47 "map_entry k f m = (case lookup m k of None \<Rightarrow> m |
71 "map_entry k f m = (case lookup m k of None \<Rightarrow> m |
48 | Some v \<Rightarrow> update k (f v) m)" |
72 | Some v \<Rightarrow> update k (f v) m)" |
49 |
73 |
109 lemma delete_empty [simp]: |
137 lemma delete_empty [simp]: |
110 "delete k empty = empty" |
138 "delete k empty = empty" |
111 by (rule mapping_eqI) simp |
139 by (rule mapping_eqI) simp |
112 |
140 |
113 lemma replace_update: |
141 lemma replace_update: |
114 "k \<notin> dom (lookup m) \<Longrightarrow> replace k v m = m" |
142 "k \<notin> keys m \<Longrightarrow> replace k v m = m" |
115 "k \<in> dom (lookup m) \<Longrightarrow> replace k v m = update k v m" |
143 "k \<in> keys m \<Longrightarrow> replace k v m = update k v m" |
116 by (rule mapping_eqI, auto simp add: replace_def fun_upd_twist)+ |
144 by (rule mapping_eqI) (auto simp add: replace_def fun_upd_twist)+ |
117 |
145 |
118 lemma size_empty [simp]: |
146 lemma size_empty [simp]: |
119 "size empty = 0" |
147 "size empty = 0" |
120 by (simp add: size_def) |
148 by (simp add: size_def keys_def) |
121 |
149 |
122 lemma size_update: |
150 lemma size_update: |
123 "finite (dom (lookup m)) \<Longrightarrow> size (update k v m) = |
151 "finite (keys m) \<Longrightarrow> size (update k v m) = |
124 (if k \<in> dom (lookup m) then size m else Suc (size m))" |
152 (if k \<in> keys m then size m else Suc (size m))" |
125 by (auto simp add: size_def insert_dom) |
153 by (auto simp add: size_def insert_dom keys_def) |
126 |
154 |
127 lemma size_delete: |
155 lemma size_delete: |
128 "size (delete k m) = (if k \<in> dom (lookup m) then size m - 1 else size m)" |
156 "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)" |
129 by (simp add: size_def) |
157 by (simp add: size_def keys_def) |
130 |
158 |
131 lemma size_tabulate: |
159 lemma size_tabulate [simp]: |
132 "size (tabulate ks f) = length (remdups ks)" |
160 "size (tabulate ks f) = length (remdups ks)" |
133 by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def) |
161 by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def keys_def) |
134 |
162 |
135 lemma bulkload_tabulate: |
163 lemma bulkload_tabulate: |
136 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
164 "bulkload xs = tabulate [0..<length xs] (nth xs)" |
137 by (rule mapping_eqI) (simp add: expand_fun_eq) |
165 by (rule mapping_eqI) (simp add: expand_fun_eq) |
138 |
166 |
139 lemma keys_tabulate: |
167 lemma is_empty_empty: (*FIXME*) |
|
168 "is_empty m \<longleftrightarrow> m = Mapping Map.empty" |
|
169 by (cases m) (simp add: is_empty_def keys_def) |
|
170 |
|
171 lemma is_empty_empty' [simp]: |
|
172 "is_empty empty" |
|
173 by (simp add: is_empty_empty empty_def) |
|
174 |
|
175 lemma is_empty_update [simp]: |
|
176 "\<not> is_empty (update k v m)" |
|
177 by (cases m) (simp add: is_empty_empty) |
|
178 |
|
179 lemma is_empty_delete: |
|
180 "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}" |
|
181 by (cases m) (auto simp add: is_empty_empty keys_def dom_eq_empty_conv [symmetric] simp del: dom_eq_empty_conv) |
|
182 |
|
183 lemma is_empty_replace [simp]: |
|
184 "is_empty (replace k v m) \<longleftrightarrow> is_empty m" |
|
185 by (auto simp add: replace_def) (simp add: is_empty_def) |
|
186 |
|
187 lemma is_empty_default [simp]: |
|
188 "\<not> is_empty (default k v m)" |
|
189 by (auto simp add: default_def) (simp add: is_empty_def) |
|
190 |
|
191 lemma is_empty_map_entry [simp]: |
|
192 "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m" |
|
193 by (cases "lookup m k") |
|
194 (auto simp add: map_entry_def, simp add: is_empty_empty) |
|
195 |
|
196 lemma is_empty_map_default [simp]: |
|
197 "\<not> is_empty (map_default k v f m)" |
|
198 by (simp add: map_default_def) |
|
199 |
|
200 lemma keys_empty [simp]: |
|
201 "keys empty = {}" |
|
202 by (simp add: keys_def) |
|
203 |
|
204 lemma keys_update [simp]: |
|
205 "keys (update k v m) = insert k (keys m)" |
|
206 by (simp add: keys_def) |
|
207 |
|
208 lemma keys_delete [simp]: |
|
209 "keys (delete k m) = keys m - {k}" |
|
210 by (simp add: keys_def) |
|
211 |
|
212 lemma keys_replace [simp]: |
|
213 "keys (replace k v m) = keys m" |
|
214 by (auto simp add: keys_def replace_def) |
|
215 |
|
216 lemma keys_default [simp]: |
|
217 "keys (default k v m) = insert k (keys m)" |
|
218 by (auto simp add: keys_def default_def) |
|
219 |
|
220 lemma keys_map_entry [simp]: |
|
221 "keys (map_entry k f m) = keys m" |
|
222 by (auto simp add: keys_def) |
|
223 |
|
224 lemma keys_map_default [simp]: |
|
225 "keys (map_default k v f m) = insert k (keys m)" |
|
226 by (simp add: map_default_def) |
|
227 |
|
228 lemma keys_tabulate [simp]: |
140 "keys (tabulate ks f) = set ks" |
229 "keys (tabulate ks f) = set ks" |
141 by (simp add: tabulate_def keys_def map_of_map_restrict o_def) |
230 by (simp add: tabulate_def keys_def map_of_map_restrict o_def) |
142 |
231 |
143 lemma keys_bulkload: |
232 lemma keys_bulkload [simp]: |
144 "keys (bulkload xs) = {0..<length xs}" |
233 "keys (bulkload xs) = {0..<length xs}" |
145 by (simp add: keys_tabulate bulkload_tabulate) |
234 by (simp add: keys_tabulate bulkload_tabulate) |
146 |
235 |
147 lemma is_empty_empty: |
236 lemma distinct_ordered_keys [simp]: |
148 "is_empty m \<longleftrightarrow> m = Mapping Map.empty" |
237 "distinct (ordered_keys m)" |
149 by (cases m) (simp add: is_empty_def) |
238 by (simp add: ordered_keys_def) |
|
239 |
|
240 lemma ordered_keys_infinite [simp]: |
|
241 "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []" |
|
242 by (simp add: ordered_keys_def) |
|
243 |
|
244 lemma ordered_keys_empty [simp]: |
|
245 "ordered_keys empty = []" |
|
246 by (simp add: ordered_keys_def) |
|
247 |
|
248 lemma ordered_keys_update [simp]: |
|
249 "k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m" |
|
250 "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)" |
|
251 by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb) |
|
252 |
|
253 lemma ordered_keys_delete [simp]: |
|
254 "ordered_keys (delete k m) = remove1 k (ordered_keys m)" |
|
255 proof (cases "finite (keys m)") |
|
256 case False then show ?thesis by simp |
|
257 next |
|
258 case True note fin = True |
|
259 show ?thesis |
|
260 proof (cases "k \<in> keys m") |
|
261 case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp |
|
262 with False show ?thesis by (simp add: ordered_keys_def remove1_idem) |
|
263 next |
|
264 case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove) |
|
265 qed |
|
266 qed |
|
267 |
|
268 lemma ordered_keys_replace [simp]: |
|
269 "ordered_keys (replace k v m) = ordered_keys m" |
|
270 by (simp add: replace_def) |
|
271 |
|
272 lemma ordered_keys_default [simp]: |
|
273 "k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m" |
|
274 "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)" |
|
275 by (simp_all add: default_def) |
|
276 |
|
277 lemma ordered_keys_map_entry [simp]: |
|
278 "ordered_keys (map_entry k f m) = ordered_keys m" |
|
279 by (simp add: ordered_keys_def) |
|
280 |
|
281 lemma ordered_keys_map_default [simp]: |
|
282 "k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m" |
|
283 "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)" |
|
284 by (simp_all add: map_default_def) |
|
285 |
|
286 lemma ordered_keys_tabulate [simp]: |
|
287 "ordered_keys (tabulate ks f) = sort (remdups ks)" |
|
288 by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) |
|
289 |
|
290 lemma ordered_keys_bulkload [simp]: |
|
291 "ordered_keys (bulkload ks) = [0..<length ks]" |
|
292 by (simp add: ordered_keys_def) |
150 |
293 |
151 |
294 |
152 subsection {* Some technical code lemmas *} |
295 subsection {* Some technical code lemmas *} |
153 |
296 |
154 lemma [code]: |
297 lemma [code]: |