src/HOL/Library/AList.thy
 author nipkow Tue Sep 22 14:31:22 2015 +0200 (2015-09-22) changeset 61225 1a690dce8cfc parent 60500 903bb1495239 child 61585 a9599d3d7610 permissions -rw-r--r--
tuned references
1 (*  Title:      HOL/Library/AList.thy
2     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
3 *)
5 section \<open>Implementation of Association Lists\<close>
7 theory AList
8 imports Main
9 begin
11 context
12 begin
14 text \<open>
15   The operations preserve distinctness of keys and
16   function @{term "clearjunk"} distributes over them. Since
17   @{term clearjunk} enforces distinctness of keys it can be used
18   to establish the invariant, e.g. for inductive proofs.
19 \<close>
21 subsection \<open>@{text update} and @{text updates}\<close>
23 qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
24 where
25   "update k v [] = [(k, v)]"
26 | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
28 lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
29   by (induct al) (auto simp add: fun_eq_iff)
31 corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
34 lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
35   by (induct al) auto
37 lemma update_keys:
38   "map fst (update k v al) =
39     (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
40   by (induct al) simp_all
42 lemma distinct_update:
43   assumes "distinct (map fst al)"
44   shows "distinct (map fst (update k v al))"
45   using assms by (simp add: update_keys)
47 lemma update_filter:
48   "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
49   by (induct ps) auto
51 lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
52   by (induct al) auto
54 lemma update_nonempty [simp]: "update k v al \<noteq> []"
55   by (induct al) auto
57 lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
58 proof (induct al arbitrary: al')
59   case Nil
60   then show ?case
61     by (cases al') (auto split: split_if_asm)
62 next
63   case Cons
64   then show ?case
65     by (cases al') (auto split: split_if_asm)
66 qed
68 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
69   by (induct al) auto
71 text \<open>Note that the lists are not necessarily the same:
72         @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and
73         @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.\<close>
75 lemma update_swap:
76   "k \<noteq> k' \<Longrightarrow>
77     map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
78   by (simp add: update_conv' fun_eq_iff)
80 lemma update_Some_unfold:
81   "map_of (update k v al) x = Some y \<longleftrightarrow>
82     x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
83   by (simp add: update_conv' map_upd_Some_unfold)
85 lemma image_update [simp]:
86   "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
89 qualified definition
90     updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
91   where "updates ks vs = fold (case_prod update) (zip ks vs)"
94   "updates [] vs ps = ps"
95   "updates ks [] ps = ps"
96   "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
100   "updates (k # ks) vs ps =
101     (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
102   by (cases vs) simp_all
105 proof -
106   have "map_of \<circ> fold (case_prod update) (zip ks vs) =
107       fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
108     by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
109   then show ?thesis
111 qed
113 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
117   assumes "distinct (map fst al)"
118   shows "distinct (map fst (updates ks vs al))"
119 proof -
120   have "distinct (fold
121        (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
122        (zip ks vs) (map fst al))"
123     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
124   moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
125       fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
126     by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
127   ultimately show ?thesis
129 qed
131 lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
132     updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
133   by (induct ks arbitrary: vs al) (auto split: list.splits)
136   "size ks \<le> i \<Longrightarrow> i < size vs \<Longrightarrow>
138   by (induct ks arbitrary: al vs i) (auto split: list.splits nat.splits)
141   "map_of (updates xs ys (update x y al)) =
142     map_of
143      (if x \<in> set (take (length ys) xs)
144       then updates xs ys al
145       else (update x y (updates xs ys al)))"
149   "k \<notin> set ks \<Longrightarrow>
150     map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
154   "k \<notin> set ks \<Longrightarrow> map_of (updates ks vs al) k = map_of al k"
158   "size xs = size ys \<Longrightarrow> updates (xs @ zs) ys al = updates xs ys al"
159   by (induct xs arbitrary: ys al) (auto split: list.splits)
162   "size xs = size ys \<Longrightarrow> updates xs (ys @ zs) al = updates xs ys al"
163   by (induct xs arbitrary: ys al) (auto split: list.splits)
166 subsection \<open>@{text delete}\<close>
168 qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
169   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
171 lemma delete_simps [simp]:
172   "delete k [] = []"
173   "delete k (p # ps) = (if fst p = k then delete k ps else p # delete k ps)"
174   by (auto simp add: delete_eq)
176 lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
177   by (induct al) (auto simp add: fun_eq_iff)
179 corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
182 lemma delete_keys: "map fst (delete k al) = removeAll k (map fst al)"
183   by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
185 lemma distinct_delete:
186   assumes "distinct (map fst al)"
187   shows "distinct (map fst (delete k al))"
188   using assms by (simp add: delete_keys distinct_removeAll)
190 lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
191   by (auto simp add: image_iff delete_eq filter_id_conv)
193 lemma delete_idem: "delete k (delete k al) = delete k al"
196 lemma map_of_delete [simp]: "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
199 lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
200   by (auto simp add: delete_eq)
202 lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
203   by (auto simp add: delete_eq)
205 lemma delete_update_same: "delete k (update k v al) = delete k al"
206   by (induct al) simp_all
208 lemma delete_update: "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
209   by (induct al) simp_all
211 lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
212   by (simp add: delete_eq conj_commute)
214 lemma length_delete_le: "length (delete k al) \<le> length al"
218 subsection \<open>@{text update_with_aux} and @{text delete_aux}\<close>
220 qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
221 where
222   "update_with_aux v k f [] = [(k, f v)]"
223 | "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
225 text \<open>
226   The above @{term "delete"} traverses all the list even if it has found the key.
227   This one does not have to keep going because is assumes the invariant that keys are distinct.
228 \<close>
229 qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
230 where
231   "delete_aux k [] = []"
232 | "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
234 lemma map_of_update_with_aux':
235   "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
236 by(induct ps) auto
238 lemma map_of_update_with_aux:
239   "map_of (update_with_aux v k f ps) = (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
242 lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
243   by (induct ps) auto
245 lemma distinct_update_with_aux [simp]:
246   "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
247 by(induct ps)(auto simp add: dom_update_with_aux)
249 lemma set_update_with_aux:
250   "distinct (map fst xs)
251   \<Longrightarrow> set (update_with_aux v k f xs) = (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
252 by(induct xs)(auto intro: rev_image_eqI)
254 lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
255 apply(induct xs)
256 apply simp_all
257 apply clarsimp
258 apply(fastforce intro: rev_image_eqI)
259 done
261 lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
264 lemma distinct_delete_aux [simp]:
265   "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
266 proof(induct ps)
267   case Nil thus ?case by simp
268 next
269   case (Cons a ps)
270   obtain k' v where a: "a = (k', v)" by(cases a)
271   show ?case
272   proof(cases "k' = k")
273     case True with Cons a show ?thesis by simp
274   next
275     case False
276     with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
277     with False a have "k' \<notin> fst ` set (delete_aux k ps)"
278       by(auto dest!: dom_delete_aux[where k=k])
279     with Cons a show ?thesis by simp
280   qed
281 qed
283 lemma map_of_delete_aux':
284   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
285   apply (induct xs)
286   apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
287   apply (auto intro!: ext)
289   done
291 lemma map_of_delete_aux:
292   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
295 lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
296 by(cases ts)(auto split: split_if_asm)
299 subsection \<open>@{text restrict}\<close>
301 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
302   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
304 lemma restr_simps [simp]:
305   "restrict A [] = []"
306   "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
307   by (auto simp add: restrict_eq)
309 lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
310 proof
311   fix k
312   show "map_of (restrict A al) k = ((map_of al)|` A) k"
313     by (induct al) (simp, cases "k \<in> A", auto)
314 qed
316 corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
319 lemma distinct_restr:
320   "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
321   by (induct al) (auto simp add: restrict_eq)
323 lemma restr_empty [simp]:
324   "restrict {} al = []"
325   "restrict A [] = []"
326   by (induct al) (auto simp add: restrict_eq)
328 lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
331 lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
334 lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
335   by (induct al) (auto simp add: restrict_eq)
337 lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
338   by (induct al) (auto simp add: restrict_eq)
340 lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
341   by (induct al) (auto simp add: restrict_eq)
343 lemma restr_update[simp]:
344  "map_of (restrict D (update x y al)) =
345   map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
346   by (simp add: restr_conv' update_conv')
348 lemma restr_delete [simp]:
349   "delete x (restrict D al) = (if x \<in> D then restrict (D - {x}) al else restrict D al)"
350   apply (simp add: delete_eq restrict_eq)
351   apply (auto simp add: split_def)
352 proof -
353   have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y"
354     by auto
355   then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
356     by simp
357   assume "x \<notin> D"
358   then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y"
359     by auto
360   then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
361     by simp
362 qed
364 lemma update_restr:
365   "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
366   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
368 lemma update_restr_conv [simp]:
369   "x \<in> D \<Longrightarrow>
370     map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
371   by (simp add: update_conv' restr_conv')
374   "length xs = length ys \<Longrightarrow> set xs \<subseteq> D \<Longrightarrow>
375     map_of (restrict D (updates xs ys al)) =
376       map_of (updates xs ys (restrict (D - set xs) al))"
379 lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
380   by (induct ps) auto
383 subsection \<open>@{text clearjunk}\<close>
385 qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
386 where
387   "clearjunk [] = []"
388 | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
389   by pat_completeness auto
390 termination
391   by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le)
393 lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
394   by (induct al rule: clearjunk.induct) (simp_all add: fun_eq_iff)
396 lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)"
397   by (induct al rule: clearjunk.induct) (simp_all add: delete_keys)
399 lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
400   using clearjunk_keys_set by simp
402 lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
403   by (induct al rule: clearjunk.induct) (simp_all del: set_map add: clearjunk_keys_set delete_keys)
405 lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)"
408 lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)"
409 proof -
410   have "ran (map_of al) = ran (map_of (clearjunk al))"
412   also have "\<dots> = snd ` set (clearjunk al)"
414   finally show ?thesis .
415 qed
417 lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
418   by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
421 proof -
422   have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
423     fold (case_prod update) (zip ks vs) \<circ> clearjunk"
424     by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
425   then show ?thesis
427 qed
429 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
430   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
432 lemma clearjunk_restrict: "clearjunk (restrict A al) = restrict A (clearjunk al)"
433   by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
435 lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
436   by (induct al rule: clearjunk.induct) auto
438 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
439   by simp
441 lemma length_clearjunk: "length (clearjunk al) \<le> length al"
442 proof (induct al rule: clearjunk.induct [case_names Nil Cons])
443   case Nil
444   then show ?case by simp
445 next
446   case (Cons kv al)
447   moreover have "length (delete (fst kv) al) \<le> length al"
448     by (fact length_delete_le)
449   ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al"
450     by (rule order_trans)
451   then show ?case
452     by simp
453 qed
455 lemma delete_map:
456   assumes "\<And>kv. fst (f kv) = fst kv"
457   shows "delete k (map f ps) = map f (delete k ps)"
458   by (simp add: delete_eq filter_map comp_def split_def assms)
460 lemma clearjunk_map:
461   assumes "\<And>kv. fst (f kv) = fst kv"
462   shows "clearjunk (map f ps) = map f (clearjunk ps)"
463   by (induct ps rule: clearjunk.induct [case_names Nil Cons])
464     (simp_all add: clearjunk_delete delete_map assms)
467 subsection \<open>@{text map_ran}\<close>
469 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
470   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
472 lemma map_ran_simps [simp]:
473   "map_ran f [] = []"
474   "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
477 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
478   by (simp add: map_ran_def image_image split_def)
480 lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
481   by (induct al) auto
483 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
484   by (simp add: map_ran_def split_def comp_def)
486 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
487   by (simp add: map_ran_def filter_map split_def comp_def)
489 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
490   by (simp add: map_ran_def split_def clearjunk_map)
493 subsection \<open>@{text merge}\<close>
495 qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
496   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
498 lemma merge_simps [simp]:
499   "merge qs [] = qs"
500   "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
501   by (simp_all add: merge_def split_def)
503 lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
506 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
507   by (induct ys arbitrary: xs) (auto simp add: dom_update)
509 lemma distinct_merge:
510   assumes "distinct (map fst xs)"
511   shows "distinct (map fst (merge xs ys))"
514 lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
517 lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys"
518 proof -
519   have "map_of \<circ> fold (case_prod update) (rev ys) =
520       fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
521     by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
522   then show ?thesis
524 qed
526 corollary merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
529 lemma merge_empty: "map_of (merge [] ys) = map_of ys"
532 lemma merge_assoc [simp]: "map_of (merge m1 (merge m2 m3)) = map_of (merge (merge m1 m2) m3)"
535 lemma merge_Some_iff:
536   "map_of (merge m n) k = Some x \<longleftrightarrow>
537     map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x"
540 lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
542 lemma merge_find_right [simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
545 lemma merge_None [iff]:
546   "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
549 lemma merge_upd [simp]:
550   "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
551   by (simp add: update_conv' merge_conv')
554   "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
557 lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)"
561 subsection \<open>@{text compose}\<close>
563 qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
564 where
565   "compose [] ys = []"
566 | "compose (x # xs) ys =
567     (case map_of ys (snd x) of
568       None \<Rightarrow> compose (delete (fst x) xs) ys
569     | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
570   by pat_completeness auto
571 termination
572   by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
574 lemma compose_first_None [simp]:
575   assumes "map_of xs k = None"
576   shows "map_of (compose xs ys) k = None"
577   using assms by (induct xs ys rule: compose.induct) (auto split: option.splits split_if_asm)
579 lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
580 proof (induct xs ys rule: compose.induct)
581   case 1
582   then show ?case by simp
583 next
584   case (2 x xs ys)
585   show ?case
586   proof (cases "map_of ys (snd x)")
587     case None
588     with 2 have hyp: "map_of (compose (delete (fst x) xs) ys) k =
589         (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
590       by simp
591     show ?thesis
592     proof (cases "fst x = k")
593       case True
594       from True delete_notin_dom [of k xs]
595       have "map_of (delete (fst x) xs) k = None"
597       with hyp show ?thesis
598         using True None
599         by simp
600     next
601       case False
602       from False have "map_of (delete (fst x) xs) k = map_of xs k"
603         by simp
604       with hyp show ?thesis
605         using False None by (simp add: map_comp_def)
606     qed
607   next
608     case (Some v)
609     with 2
610     have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
611       by simp
612     with Some show ?thesis
613       by (auto simp add: map_comp_def)
614   qed
615 qed
617 lemma compose_conv': "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
618   by (rule ext) (rule compose_conv)
620 lemma compose_first_Some [simp]:
621   assumes "map_of xs k = Some v"
622   shows "map_of (compose xs ys) k = map_of ys v"
623   using assms by (simp add: compose_conv)
625 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
626 proof (induct xs ys rule: compose.induct)
627   case 1
628   then show ?case by simp
629 next
630   case (2 x xs ys)
631   show ?case
632   proof (cases "map_of ys (snd x)")
633     case None
634     with "2.hyps"
635     have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
636       by simp
637     also
638     have "\<dots> \<subseteq> fst ` set xs"
639       by (rule dom_delete_subset)
640     finally show ?thesis
641       using None
642       by auto
643   next
644     case (Some v)
645     with "2.hyps"
646     have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
647       by simp
648     with Some show ?thesis
649       by auto
650   qed
651 qed
653 lemma distinct_compose:
654   assumes "distinct (map fst xs)"
655   shows "distinct (map fst (compose xs ys))"
656   using assms
657 proof (induct xs ys rule: compose.induct)
658   case 1
659   then show ?case by simp
660 next
661   case (2 x xs ys)
662   show ?case
663   proof (cases "map_of ys (snd x)")
664     case None
665     with 2 show ?thesis by simp
666   next
667     case (Some v)
668     with 2 dom_compose [of xs ys] show ?thesis
669       by auto
670   qed
671 qed
673 lemma compose_delete_twist: "compose (delete k xs) ys = delete k (compose xs ys)"
674 proof (induct xs ys rule: compose.induct)
675   case 1
676   then show ?case by simp
677 next
678   case (2 x xs ys)
679   show ?case
680   proof (cases "map_of ys (snd x)")
681     case None
682     with 2 have hyp: "compose (delete k (delete (fst x) xs)) ys =
683         delete k (compose (delete (fst x) xs) ys)"
684       by simp
685     show ?thesis
686     proof (cases "fst x = k")
687       case True
688       with None hyp show ?thesis
690     next
691       case False
692       from None False hyp show ?thesis
694     qed
695   next
696     case (Some v)
697     with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)"
698       by simp
699     with Some show ?thesis
700       by simp
701   qed
702 qed
704 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
705   by (induct xs ys rule: compose.induct)
706     (auto simp add: map_of_clearjunk split: option.splits)
708 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
709   by (induct xs rule: clearjunk.induct)
710     (auto split: option.splits simp add: clearjunk_delete delete_idem compose_delete_twist)
712 lemma compose_empty [simp]: "compose xs [] = []"
713   by (induct xs) (auto simp add: compose_delete_twist)
715 lemma compose_Some_iff:
716   "(map_of (compose xs ys) k = Some v) \<longleftrightarrow>
717     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)"
718   by (simp add: compose_conv map_comp_Some_iff)
720 lemma map_comp_None_iff:
721   "map_of (compose xs ys) k = None \<longleftrightarrow>
722     (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None))"
723   by (simp add: compose_conv map_comp_None_iff)
726 subsection \<open>@{text map_entry}\<close>
728 qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
729 where
730   "map_entry k f [] = []"
731 | "map_entry k f (p # ps) =
732     (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
734 lemma map_of_map_entry:
735   "map_of (map_entry k f xs) =
736     (map_of xs)(k := case map_of xs k of None \<Rightarrow> None | Some v' \<Rightarrow> Some (f v'))"
737   by (induct xs) auto
739 lemma dom_map_entry: "fst ` set (map_entry k f xs) = fst ` set xs"
740   by (induct xs) auto
742 lemma distinct_map_entry:
743   assumes "distinct (map fst xs)"
744   shows "distinct (map fst (map_entry k f xs))"
745   using assms by (induct xs) (auto simp add: dom_map_entry)
748 subsection \<open>@{text map_default}\<close>
750 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
751 where
752   "map_default k v f [] = [(k, v)]"
753 | "map_default k v f (p # ps) =
754     (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
756 lemma map_of_map_default:
757   "map_of (map_default k v f xs) =
758     (map_of xs)(k := case map_of xs k of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (f v'))"
759   by (induct xs) auto
761 lemma dom_map_default: "fst ` set (map_default k v f xs) = insert k (fst ` set xs)"
762   by (induct xs) auto
764 lemma distinct_map_default:
765   assumes "distinct (map fst xs)"
766   shows "distinct (map fst (map_default k v f xs))"
767   using assms by (induct xs) (auto simp add: dom_map_default)
769 end
771 end