src/HOL/Library/AList.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69661 a03a63b81f44 permissions -rw-r--r--
improved code equations taken over from AFP
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>\<open>clearjunk\<close> distributes over them. Since
17   \<^term>\<open>clearjunk\<close> enforces distinctness of keys it can be used
18   to establish the invariant, e.g. for inductive proofs.
19 \<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: if_split_asm)
62 next
63   case Cons
64   then show ?case
65     by (cases al') (auto split: if_split_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>\<open>update k v (update k' v' []) = [(k', v'), (k, v)]\<close> and
73         \<^term>\<open>update k' v' (update k v []) = [(k, v), (k', v')]\<close>.\<close>
75 lemma update_swap:
76   "k \<noteq> k' \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
77   by (simp add: update_conv' fun_eq_iff)
79 lemma update_Some_unfold:
80   "map_of (update k v al) x = Some y \<longleftrightarrow>
81     x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
82   by (simp add: update_conv' map_upd_Some_unfold)
84 lemma image_update [simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
85   by (auto simp add: update_conv')
88     "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
89   where "updates ks vs = fold (case_prod update) (zip ks vs)"
92   "updates [] vs ps = ps"
93   "updates ks [] ps = ps"
94   "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
98   "updates (k # ks) vs ps =
99     (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
100   by (cases vs) simp_all
103 proof -
104   have "map_of \<circ> fold (case_prod update) (zip ks vs) =
105       fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
106     by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
107   then show ?thesis
109 qed
111 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
115   assumes "distinct (map fst al)"
116   shows "distinct (map fst (updates ks vs al))"
117 proof -
118   have "distinct (fold
119        (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
120        (zip ks vs) (map fst al))"
121     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
122   moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
123       fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
124     by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
125   ultimately show ?thesis
127 qed
129 lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
130     updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
131   by (induct ks arbitrary: vs al) (auto split: list.splits)
134   "size ks \<le> i \<Longrightarrow> i < size vs \<Longrightarrow>
136   by (induct ks arbitrary: al vs i) (auto split: list.splits nat.splits)
139   "map_of (updates xs ys (update x y al)) =
140     map_of
141      (if x \<in> set (take (length ys) xs)
142       then updates xs ys al
143       else (update x y (updates xs ys al)))"
147   "k \<notin> set ks \<Longrightarrow>
148     map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
152   "k \<notin> set ks \<Longrightarrow> map_of (updates ks vs al) k = map_of al k"
156   "size xs = size ys \<Longrightarrow> updates (xs @ zs) ys al = updates xs ys al"
157   by (induct xs arbitrary: ys al) (auto split: list.splits)
160   "size xs = size ys \<Longrightarrow> updates xs (ys @ zs) al = updates xs ys al"
161   by (induct xs arbitrary: ys al) (auto split: list.splits)
164 subsection \<open>\<open>delete\<close>\<close>
166 qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
167   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
169 lemma delete_simps [simp]:
170   "delete k [] = []"
171   "delete k (p # ps) = (if fst p = k then delete k ps else p # delete k ps)"
172   by (auto simp add: delete_eq)
174 lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
175   by (induct al) (auto simp add: fun_eq_iff)
177 corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
180 lemma delete_keys: "map fst (delete k al) = removeAll k (map fst al)"
181   by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
183 lemma distinct_delete:
184   assumes "distinct (map fst al)"
185   shows "distinct (map fst (delete k al))"
186   using assms by (simp add: delete_keys distinct_removeAll)
188 lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
189   by (auto simp add: image_iff delete_eq filter_id_conv)
191 lemma delete_idem: "delete k (delete k al) = delete k al"
194 lemma map_of_delete [simp]: "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
197 lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
198   by (auto simp add: delete_eq)
200 lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
201   by (auto simp add: delete_eq)
203 lemma delete_update_same: "delete k (update k v al) = delete k al"
204   by (induct al) simp_all
206 lemma delete_update: "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
207   by (induct al) simp_all
209 lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
210   by (simp add: delete_eq conj_commute)
212 lemma length_delete_le: "length (delete k al) \<le> length al"
216 subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
218 qualified primrec update_with_aux ::
219     "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
220   where
221     "update_with_aux v k f [] = [(k, f v)]"
222   | "update_with_aux v k f (p # ps) =
223       (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>\<open>delete\<close> 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' =
236     ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
237   by (induct ps) auto
239 lemma map_of_update_with_aux:
240   "map_of (update_with_aux v k f ps) =
241     (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
242   by (simp add: fun_eq_iff map_of_update_with_aux')
244 lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
245   by (induct ps) auto
247 lemma distinct_update_with_aux [simp]:
248   "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
249   by (induct ps) (auto simp add: dom_update_with_aux)
251 lemma set_update_with_aux:
252   "distinct (map fst xs) \<Longrightarrow>
253     set (update_with_aux v k f xs) =
254       (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
255   by (induct xs) (auto intro: rev_image_eqI)
257 lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
258   apply (induct xs)
259    apply simp_all
260   apply clarsimp
261   apply (fastforce intro: rev_image_eqI)
262   done
264 lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
265   by (auto simp add: set_delete_aux)
267 lemma distinct_delete_aux [simp]: "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
268 proof (induct ps)
269   case Nil
270   then show ?case by simp
271 next
272   case (Cons a ps)
273   obtain k' v where a: "a = (k', v)"
274     by (cases a)
275   show ?case
276   proof (cases "k' = k")
277     case True
278     with Cons a show ?thesis by simp
279   next
280     case False
281     with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)"
282       by simp_all
283     with False a have "k' \<notin> fst ` set (delete_aux k ps)"
284       by (auto dest!: dom_delete_aux[where k=k])
285     with Cons a show ?thesis
286       by simp
287   qed
288 qed
290 lemma map_of_delete_aux':
291   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
292   apply (induct xs)
293    apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
294   apply (auto intro!: ext)
296   done
298 lemma map_of_delete_aux:
299   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
302 lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
303   by (cases ts) (auto split: if_split_asm)
306 subsection \<open>\<open>restrict\<close>\<close>
308 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
309   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
311 lemma restr_simps [simp]:
312   "restrict A [] = []"
313   "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
314   by (auto simp add: restrict_eq)
316 lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
317 proof
318   show "map_of (restrict A al) k = ((map_of al)|` A) k" for k
319     apply (induct al)
320      apply simp
321     apply (cases "k \<in> A")
322      apply auto
323     done
324 qed
326 corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
329 lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
330   by (induct al) (auto simp add: restrict_eq)
332 lemma restr_empty [simp]:
333   "restrict {} al = []"
334   "restrict A [] = []"
335   by (induct al) (auto simp add: restrict_eq)
337 lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
340 lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
343 lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
344   by (induct al) (auto simp add: restrict_eq)
346 lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
347   by (induct al) (auto simp add: restrict_eq)
349 lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
350   by (induct al) (auto simp add: restrict_eq)
352 lemma restr_update[simp]:
353   "map_of (restrict D (update x y al)) =
354     map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
355   by (simp add: restr_conv' update_conv')
357 lemma restr_delete [simp]:
358   "delete x (restrict D al) = (if x \<in> D then restrict (D - {x}) al else restrict D al)"
359   apply (simp add: delete_eq restrict_eq)
360   apply (auto simp add: split_def)
361 proof -
362   have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
363     by auto
364   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]"
365     by simp
366   assume "x \<notin> D"
367   then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
368     by auto
369   then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
370     by simp
371 qed
373 lemma update_restr:
374   "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
375   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
377 lemma update_restr_conv [simp]:
378   "x \<in> D \<Longrightarrow>
379     map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
380   by (simp add: update_conv' restr_conv')
383   "length xs = length ys \<Longrightarrow> set xs \<subseteq> D \<Longrightarrow>
384     map_of (restrict D (updates xs ys al)) =
385       map_of (updates xs ys (restrict (D - set xs) al))"
388 lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
389   by (induct ps) auto
392 subsection \<open>\<open>clearjunk\<close>\<close>
394 qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
395   where
396     "clearjunk [] = []"
397   | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
398   by pat_completeness auto
399 termination
400   by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le)
402 lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
403   by (induct al rule: clearjunk.induct) (simp_all add: fun_eq_iff)
405 lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)"
406   by (induct al rule: clearjunk.induct) (simp_all add: delete_keys)
408 lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
409   using clearjunk_keys_set by simp
411 lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
412   by (induct al rule: clearjunk.induct) (simp_all del: set_map add: clearjunk_keys_set delete_keys)
414 lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)"
417 lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)"
418 proof -
419   have "ran (map_of al) = ran (map_of (clearjunk al))"
421   also have "\<dots> = snd ` set (clearjunk al)"
423   finally show ?thesis .
424 qed
426 lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
427   by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
430 proof -
431   have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
432       fold (case_prod update) (zip ks vs) \<circ> clearjunk"
433     by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
434   then show ?thesis
436 qed
438 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
439   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
441 lemma clearjunk_restrict: "clearjunk (restrict A al) = restrict A (clearjunk al)"
442   by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
444 lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
445   by (induct al rule: clearjunk.induct) auto
447 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
448   by simp
450 lemma length_clearjunk: "length (clearjunk al) \<le> length al"
451 proof (induct al rule: clearjunk.induct [case_names Nil Cons])
452   case Nil
453   then show ?case by simp
454 next
455   case (Cons kv al)
456   moreover have "length (delete (fst kv) al) \<le> length al"
457     by (fact length_delete_le)
458   ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al"
459     by (rule order_trans)
460   then show ?case
461     by simp
462 qed
464 lemma delete_map:
465   assumes "\<And>kv. fst (f kv) = fst kv"
466   shows "delete k (map f ps) = map f (delete k ps)"
467   by (simp add: delete_eq filter_map comp_def split_def assms)
469 lemma clearjunk_map:
470   assumes "\<And>kv. fst (f kv) = fst kv"
471   shows "clearjunk (map f ps) = map f (clearjunk ps)"
472   by (induct ps rule: clearjunk.induct [case_names Nil Cons])
473     (simp_all add: clearjunk_delete delete_map assms)
476 subsection \<open>\<open>map_ran\<close>\<close>
478 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
479   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
481 lemma map_ran_simps [simp]:
482   "map_ran f [] = []"
483   "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
486 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
487   by (simp add: map_ran_def image_image split_def)
489 lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
490   by (induct al) auto
492 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
493   by (simp add: map_ran_def split_def comp_def)
495 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
496   by (simp add: map_ran_def filter_map split_def comp_def)
498 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
499   by (simp add: map_ran_def split_def clearjunk_map)
502 subsection \<open>\<open>merge\<close>\<close>
504 qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
505   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
507 lemma merge_simps [simp]:
508   "merge qs [] = qs"
509   "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
510   by (simp_all add: merge_def split_def)
512 lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
515 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
516   by (induct ys arbitrary: xs) (auto simp add: dom_update)
518 lemma distinct_merge: "distinct (map fst xs) \<Longrightarrow> distinct (map fst (merge xs ys))"
521 lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
524 lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys"
525 proof -
526   have "map_of \<circ> fold (case_prod update) (rev ys) =
527       fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
528     by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
529   then show ?thesis
531 qed
533 corollary merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
536 lemma merge_empty: "map_of (merge [] ys) = map_of ys"
539 lemma merge_assoc [simp]: "map_of (merge m1 (merge m2 m3)) = map_of (merge (merge m1 m2) m3)"
542 lemma merge_Some_iff:
543   "map_of (merge m n) k = Some x \<longleftrightarrow>
544     map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x"
547 lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
549 lemma merge_find_right [simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
552 lemma merge_None [iff]: "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
555 lemma merge_upd [simp]: "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
556   by (simp add: update_conv' merge_conv')
559   "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
562 lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)"
566 subsection \<open>\<open>compose\<close>\<close>
568 qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
569   where
570     "compose [] ys = []"
571   | "compose (x # xs) ys =
572       (case map_of ys (snd x) of
573         None \<Rightarrow> compose (delete (fst x) xs) ys
574       | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
575   by pat_completeness auto
576 termination
577   by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
579 lemma compose_first_None [simp]: "map_of xs k = None \<Longrightarrow> map_of (compose xs ys) k = None"
580   by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
582 lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
583 proof (induct xs ys rule: compose.induct)
584   case 1
585   then show ?case by simp
586 next
587   case (2 x xs ys)
588   show ?case
589   proof (cases "map_of ys (snd x)")
590     case None
591     with 2 have hyp: "map_of (compose (delete (fst x) xs) ys) k =
592         (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
593       by simp
594     show ?thesis
595     proof (cases "fst x = k")
596       case True
597       from True delete_notin_dom [of k xs]
598       have "map_of (delete (fst x) xs) k = None"
600       with hyp show ?thesis
601         using True None
602         by simp
603     next
604       case False
605       from False have "map_of (delete (fst x) xs) k = map_of xs k"
606         by simp
607       with hyp show ?thesis
608         using False None by (simp add: map_comp_def)
609     qed
610   next
611     case (Some v)
612     with 2
613     have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
614       by simp
615     with Some show ?thesis
616       by (auto simp add: map_comp_def)
617   qed
618 qed
620 lemma compose_conv': "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
621   by (rule ext) (rule compose_conv)
623 lemma compose_first_Some [simp]: "map_of xs k = Some v \<Longrightarrow> map_of (compose xs ys) k = map_of ys v"
626 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
627 proof (induct xs ys rule: compose.induct)
628   case 1
629   then show ?case by simp
630 next
631   case (2 x xs ys)
632   show ?case
633   proof (cases "map_of ys (snd x)")
634     case None
635     with "2.hyps" have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
636       by simp
637     also have "\<dots> \<subseteq> fst ` set xs"
638       by (rule dom_delete_subset)
639     finally show ?thesis
640       using None by auto
641   next
642     case (Some v)
643     with "2.hyps" have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
644       by simp
645     with Some show ?thesis
646       by auto
647   qed
648 qed
650 lemma distinct_compose:
651   assumes "distinct (map fst xs)"
652   shows "distinct (map fst (compose xs ys))"
653   using assms
654 proof (induct xs ys rule: compose.induct)
655   case 1
656   then show ?case by simp
657 next
658   case (2 x xs ys)
659   show ?case
660   proof (cases "map_of ys (snd x)")
661     case None
662     with 2 show ?thesis by simp
663   next
664     case (Some v)
665     with 2 dom_compose [of xs ys] show ?thesis
666       by auto
667   qed
668 qed
670 lemma compose_delete_twist: "compose (delete k xs) ys = delete k (compose xs ys)"
671 proof (induct xs ys rule: compose.induct)
672   case 1
673   then show ?case by simp
674 next
675   case (2 x xs ys)
676   show ?case
677   proof (cases "map_of ys (snd x)")
678     case None
679     with 2 have hyp: "compose (delete k (delete (fst x) xs)) ys =
680         delete k (compose (delete (fst x) xs) ys)"
681       by simp
682     show ?thesis
683     proof (cases "fst x = k")
684       case True
685       with None hyp show ?thesis
687     next
688       case False
689       from None False hyp show ?thesis
691     qed
692   next
693     case (Some v)
694     with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)"
695       by simp
696     with Some show ?thesis
697       by simp
698   qed
699 qed
701 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
702   by (induct xs ys rule: compose.induct)
703     (auto simp add: map_of_clearjunk split: option.splits)
705 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
706   by (induct xs rule: clearjunk.induct)
707     (auto split: option.splits simp add: clearjunk_delete delete_idem compose_delete_twist)
709 lemma compose_empty [simp]: "compose xs [] = []"
710   by (induct xs) (auto simp add: compose_delete_twist)
712 lemma compose_Some_iff:
713   "(map_of (compose xs ys) k = Some v) \<longleftrightarrow>
714     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)"
715   by (simp add: compose_conv map_comp_Some_iff)
717 lemma map_comp_None_iff:
718   "map_of (compose xs ys) k = None \<longleftrightarrow>
719     (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None))"
720   by (simp add: compose_conv map_comp_None_iff)
723 subsection \<open>\<open>map_entry\<close>\<close>
725 qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
726   where
727     "map_entry k f [] = []"
728   | "map_entry k f (p # ps) =
729       (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
731 lemma map_of_map_entry:
732   "map_of (map_entry k f xs) =
733     (map_of xs)(k := case map_of xs k of None \<Rightarrow> None | Some v' \<Rightarrow> Some (f v'))"
734   by (induct xs) auto
736 lemma dom_map_entry: "fst ` set (map_entry k f xs) = fst ` set xs"
737   by (induct xs) auto
739 lemma distinct_map_entry:
740   assumes "distinct (map fst xs)"
741   shows "distinct (map fst (map_entry k f xs))"
742   using assms by (induct xs) (auto simp add: dom_map_entry)
745 subsection \<open>\<open>map_default\<close>\<close>
747 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
748   where
749     "map_default k v f [] = [(k, v)]"
750   | "map_default k v f (p # ps) =
751       (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
753 lemma map_of_map_default:
754   "map_of (map_default k v f xs) =
755     (map_of xs)(k := case map_of xs k of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (f v'))"
756   by (induct xs) auto
758 lemma dom_map_default: "fst ` set (map_default k v f xs) = insert k (fst ` set xs)"
759   by (induct xs) auto
761 lemma distinct_map_default:
762   assumes "distinct (map fst xs)"
763   shows "distinct (map fst (map_default k v f xs))"
764   using assms by (induct xs) (auto simp add: dom_map_default)
766 end
768 end