src/HOL/Library/AList.thy
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 56327 3e62e68fb342
child 58881 b9556a055632
permissions -rw-r--r--
simpler proof
     1 (*  Title:      HOL/Library/AList.thy
     2     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of Association Lists *}
     6 
     7 theory AList
     8 imports Main
     9 begin
    10 
    11 text {*
    12   The operations preserve distinctness of keys and
    13   function @{term "clearjunk"} distributes over them. Since
    14   @{term clearjunk} enforces distinctness of keys it can be used
    15   to establish the invariant, e.g. for inductive proofs.
    16 *}
    17 
    18 subsection {* @{text update} and @{text updates} *}
    19 
    20 primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    21 where
    22   "update k v [] = [(k, v)]"
    23 | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    24 
    25 lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    26   by (induct al) (auto simp add: fun_eq_iff)
    27 
    28 corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
    29   by (simp add: update_conv')
    30 
    31 lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
    32   by (induct al) auto
    33 
    34 lemma update_keys:
    35   "map fst (update k v al) =
    36     (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
    37   by (induct al) simp_all
    38 
    39 lemma distinct_update:
    40   assumes "distinct (map fst al)"
    41   shows "distinct (map fst (update k v al))"
    42   using assms by (simp add: update_keys)
    43 
    44 lemma update_filter:
    45   "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
    46   by (induct ps) auto
    47 
    48 lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    49   by (induct al) auto
    50 
    51 lemma update_nonempty [simp]: "update k v al \<noteq> []"
    52   by (induct al) auto
    53 
    54 lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
    55 proof (induct al arbitrary: al')
    56   case Nil
    57   then show ?case
    58     by (cases al') (auto split: split_if_asm)
    59 next
    60   case Cons
    61   then show ?case
    62     by (cases al') (auto split: split_if_asm)
    63 qed
    64 
    65 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
    66   by (induct al) auto
    67 
    68 text {* Note that the lists are not necessarily the same:
    69         @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and
    70         @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
    71 
    72 lemma update_swap:
    73   "k \<noteq> k' \<Longrightarrow>
    74     map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
    75   by (simp add: update_conv' fun_eq_iff)
    76 
    77 lemma update_Some_unfold:
    78   "map_of (update k v al) x = Some y \<longleftrightarrow>
    79     x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
    80   by (simp add: update_conv' map_upd_Some_unfold)
    81 
    82 lemma image_update [simp]:
    83   "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    84   by (simp add: update_conv')
    85 
    86 definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    87   where "updates ks vs = fold (case_prod update) (zip ks vs)"
    88 
    89 lemma updates_simps [simp]:
    90   "updates [] vs ps = ps"
    91   "updates ks [] ps = ps"
    92   "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
    93   by (simp_all add: updates_def)
    94 
    95 lemma updates_key_simp [simp]:
    96   "updates (k # ks) vs ps =
    97     (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
    98   by (cases vs) simp_all
    99 
   100 lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
   101 proof -
   102   have "map_of \<circ> fold (case_prod update) (zip ks vs) =
   103       fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   104     by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   105   then show ?thesis
   106     by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
   107 qed
   108 
   109 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   110   by (simp add: updates_conv')
   111 
   112 lemma distinct_updates:
   113   assumes "distinct (map fst al)"
   114   shows "distinct (map fst (updates ks vs al))"
   115 proof -
   116   have "distinct (fold
   117        (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
   118        (zip ks vs) (map fst al))"
   119     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   120   moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
   121       fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   122     by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
   123   ultimately show ?thesis
   124     by (simp add: updates_def fun_eq_iff)
   125 qed
   126 
   127 lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   128     updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   129   by (induct ks arbitrary: vs al) (auto split: list.splits)
   130 
   131 lemma updates_list_update_drop[simp]:
   132   "size ks \<le> i \<Longrightarrow> i < size vs \<Longrightarrow>
   133     updates ks (vs[i:=v]) al = updates ks vs al"
   134   by (induct ks arbitrary: al vs i) (auto split: list.splits nat.splits)
   135 
   136 lemma update_updates_conv_if:
   137   "map_of (updates xs ys (update x y al)) =
   138     map_of
   139      (if x \<in> set (take (length ys) xs)
   140       then updates xs ys al
   141       else (update x y (updates xs ys al)))"
   142   by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
   143 
   144 lemma updates_twist [simp]:
   145   "k \<notin> set ks \<Longrightarrow>
   146     map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
   147   by (simp add: updates_conv' update_conv')
   148 
   149 lemma updates_apply_notin [simp]:
   150   "k \<notin> set ks \<Longrightarrow> map_of (updates ks vs al) k = map_of al k"
   151   by (simp add: updates_conv)
   152 
   153 lemma updates_append_drop [simp]:
   154   "size xs = size ys \<Longrightarrow> updates (xs @ zs) ys al = updates xs ys al"
   155   by (induct xs arbitrary: ys al) (auto split: list.splits)
   156 
   157 lemma updates_append2_drop [simp]:
   158   "size xs = size ys \<Longrightarrow> updates xs (ys @ zs) al = updates xs ys al"
   159   by (induct xs arbitrary: ys al) (auto split: list.splits)
   160 
   161 
   162 subsection {* @{text delete} *}
   163 
   164 definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   165   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
   166 
   167 lemma delete_simps [simp]:
   168   "delete k [] = []"
   169   "delete k (p # ps) = (if fst p = k then delete k ps else p # delete k ps)"
   170   by (auto simp add: delete_eq)
   171 
   172 lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
   173   by (induct al) (auto simp add: fun_eq_iff)
   174 
   175 corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   176   by (simp add: delete_conv')
   177 
   178 lemma delete_keys: "map fst (delete k al) = removeAll k (map fst al)"
   179   by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
   180 
   181 lemma distinct_delete:
   182   assumes "distinct (map fst al)"
   183   shows "distinct (map fst (delete k al))"
   184   using assms by (simp add: delete_keys distinct_removeAll)
   185 
   186 lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   187   by (auto simp add: image_iff delete_eq filter_id_conv)
   188 
   189 lemma delete_idem: "delete k (delete k al) = delete k al"
   190   by (simp add: delete_eq)
   191 
   192 lemma map_of_delete [simp]: "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
   193   by (simp add: delete_conv')
   194 
   195 lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   196   by (auto simp add: delete_eq)
   197 
   198 lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
   199   by (auto simp add: delete_eq)
   200 
   201 lemma delete_update_same: "delete k (update k v al) = delete k al"
   202   by (induct al) simp_all
   203 
   204 lemma delete_update: "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
   205   by (induct al) simp_all
   206 
   207 lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
   208   by (simp add: delete_eq conj_commute)
   209 
   210 lemma length_delete_le: "length (delete k al) \<le> length al"
   211   by (simp add: delete_eq)
   212 
   213 
   214 subsection {* @{text restrict} *}
   215 
   216 definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   217   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
   218 
   219 lemma restr_simps [simp]:
   220   "restrict A [] = []"
   221   "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
   222   by (auto simp add: restrict_eq)
   223 
   224 lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   225 proof
   226   fix k
   227   show "map_of (restrict A al) k = ((map_of al)|` A) k"
   228     by (induct al) (simp, cases "k \<in> A", auto)
   229 qed
   230 
   231 corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   232   by (simp add: restr_conv')
   233 
   234 lemma distinct_restr:
   235   "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   236   by (induct al) (auto simp add: restrict_eq)
   237 
   238 lemma restr_empty [simp]:
   239   "restrict {} al = []"
   240   "restrict A [] = []"
   241   by (induct al) (auto simp add: restrict_eq)
   242 
   243 lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
   244   by (simp add: restr_conv')
   245 
   246 lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
   247   by (simp add: restr_conv')
   248 
   249 lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   250   by (induct al) (auto simp add: restrict_eq)
   251 
   252 lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   253   by (induct al) (auto simp add: restrict_eq)
   254 
   255 lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   256   by (induct al) (auto simp add: restrict_eq)
   257 
   258 lemma restr_update[simp]:
   259  "map_of (restrict D (update x y al)) =
   260   map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   261   by (simp add: restr_conv' update_conv')
   262 
   263 lemma restr_delete [simp]:
   264   "delete x (restrict D al) = (if x \<in> D then restrict (D - {x}) al else restrict D al)"
   265   apply (simp add: delete_eq restrict_eq)
   266   apply (auto simp add: split_def)
   267 proof -
   268   have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y"
   269     by auto
   270   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]"
   271     by simp
   272   assume "x \<notin> D"
   273   then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y"
   274     by auto
   275   then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
   276     by simp
   277 qed
   278 
   279 lemma update_restr:
   280   "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
   281   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
   282 
   283 lemma update_restr_conv [simp]:
   284   "x \<in> D \<Longrightarrow>
   285     map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
   286   by (simp add: update_conv' restr_conv')
   287 
   288 lemma restr_updates [simp]:
   289   "length xs = length ys \<Longrightarrow> set xs \<subseteq> D \<Longrightarrow>
   290     map_of (restrict D (updates xs ys al)) =
   291       map_of (updates xs ys (restrict (D - set xs) al))"
   292   by (simp add: updates_conv' restr_conv')
   293 
   294 lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   295   by (induct ps) auto
   296 
   297 
   298 subsection {* @{text clearjunk} *}
   299 
   300 function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   301 where
   302   "clearjunk [] = []"
   303 | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   304   by pat_completeness auto
   305 termination
   306   by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le)
   307 
   308 lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
   309   by (induct al rule: clearjunk.induct) (simp_all add: fun_eq_iff)
   310 
   311 lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)"
   312   by (induct al rule: clearjunk.induct) (simp_all add: delete_keys)
   313 
   314 lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
   315   using clearjunk_keys_set by simp
   316 
   317 lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
   318   by (induct al rule: clearjunk.induct) (simp_all del: set_map add: clearjunk_keys_set delete_keys)
   319 
   320 lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)"
   321   by (simp add: map_of_clearjunk)
   322 
   323 lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)"
   324 proof -
   325   have "ran (map_of al) = ran (map_of (clearjunk al))"
   326     by (simp add: ran_clearjunk)
   327   also have "\<dots> = snd ` set (clearjunk al)"
   328     by (simp add: ran_distinct)
   329   finally show ?thesis .
   330 qed
   331 
   332 lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
   333   by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
   334 
   335 lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   336 proof -
   337   have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
   338     fold (case_prod update) (zip ks vs) \<circ> clearjunk"
   339     by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
   340   then show ?thesis
   341     by (simp add: updates_def fun_eq_iff)
   342 qed
   343 
   344 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
   345   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   346 
   347 lemma clearjunk_restrict: "clearjunk (restrict A al) = restrict A (clearjunk al)"
   348   by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
   349 
   350 lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
   351   by (induct al rule: clearjunk.induct) auto
   352 
   353 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
   354   by simp
   355 
   356 lemma length_clearjunk: "length (clearjunk al) \<le> length al"
   357 proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   358   case Nil
   359   then show ?case by simp
   360 next
   361   case (Cons kv al)
   362   moreover have "length (delete (fst kv) al) \<le> length al"
   363     by (fact length_delete_le)
   364   ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al"
   365     by (rule order_trans)
   366   then show ?case
   367     by simp
   368 qed
   369 
   370 lemma delete_map:
   371   assumes "\<And>kv. fst (f kv) = fst kv"
   372   shows "delete k (map f ps) = map f (delete k ps)"
   373   by (simp add: delete_eq filter_map comp_def split_def assms)
   374 
   375 lemma clearjunk_map:
   376   assumes "\<And>kv. fst (f kv) = fst kv"
   377   shows "clearjunk (map f ps) = map f (clearjunk ps)"
   378   by (induct ps rule: clearjunk.induct [case_names Nil Cons])
   379     (simp_all add: clearjunk_delete delete_map assms)
   380 
   381 
   382 subsection {* @{text map_ran} *}
   383 
   384 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   385   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
   386 
   387 lemma map_ran_simps [simp]:
   388   "map_ran f [] = []"
   389   "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
   390   by (simp_all add: map_ran_def)
   391 
   392 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
   393   by (simp add: map_ran_def image_image split_def)
   394 
   395 lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
   396   by (induct al) auto
   397 
   398 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
   399   by (simp add: map_ran_def split_def comp_def)
   400 
   401 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   402   by (simp add: map_ran_def filter_map split_def comp_def)
   403 
   404 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   405   by (simp add: map_ran_def split_def clearjunk_map)
   406 
   407 
   408 subsection {* @{text merge} *}
   409 
   410 definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   411   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
   412 
   413 lemma merge_simps [simp]:
   414   "merge qs [] = qs"
   415   "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
   416   by (simp_all add: merge_def split_def)
   417 
   418 lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
   419   by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd)
   420 
   421 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   422   by (induct ys arbitrary: xs) (auto simp add: dom_update)
   423 
   424 lemma distinct_merge:
   425   assumes "distinct (map fst xs)"
   426   shows "distinct (map fst (merge xs ys))"
   427   using assms by (simp add: merge_updates distinct_updates)
   428 
   429 lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   430   by (simp add: merge_updates clearjunk_updates)
   431 
   432 lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys"
   433 proof -
   434   have "map_of \<circ> fold (case_prod update) (rev ys) =
   435       fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   436     by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
   437   then show ?thesis
   438     by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
   439 qed
   440 
   441 corollary merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
   442   by (simp add: merge_conv')
   443 
   444 lemma merge_empty: "map_of (merge [] ys) = map_of ys"
   445   by (simp add: merge_conv')
   446 
   447 lemma merge_assoc [simp]: "map_of (merge m1 (merge m2 m3)) = map_of (merge (merge m1 m2) m3)"
   448   by (simp add: merge_conv')
   449 
   450 lemma merge_Some_iff:
   451   "map_of (merge m n) k = Some x \<longleftrightarrow>
   452     map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x"
   453   by (simp add: merge_conv' map_add_Some_iff)
   454 
   455 lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
   456 
   457 lemma merge_find_right [simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   458   by (simp add: merge_conv')
   459 
   460 lemma merge_None [iff]:
   461   "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   462   by (simp add: merge_conv')
   463 
   464 lemma merge_upd [simp]:
   465   "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   466   by (simp add: update_conv' merge_conv')
   467 
   468 lemma merge_updatess [simp]:
   469   "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
   470   by (simp add: updates_conv' merge_conv')
   471 
   472 lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)"
   473   by (simp add: merge_conv')
   474 
   475 
   476 subsection {* @{text compose} *}
   477 
   478 function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
   479 where
   480   "compose [] ys = []"
   481 | "compose (x # xs) ys =
   482     (case map_of ys (snd x) of
   483       None \<Rightarrow> compose (delete (fst x) xs) ys
   484     | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   485   by pat_completeness auto
   486 termination
   487   by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
   488 
   489 lemma compose_first_None [simp]:
   490   assumes "map_of xs k = None"
   491   shows "map_of (compose xs ys) k = None"
   492   using assms by (induct xs ys rule: compose.induct) (auto split: option.splits split_if_asm)
   493 
   494 lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   495 proof (induct xs ys rule: compose.induct)
   496   case 1
   497   then show ?case by simp
   498 next
   499   case (2 x xs ys)
   500   show ?case
   501   proof (cases "map_of ys (snd x)")
   502     case None
   503     with 2 have hyp: "map_of (compose (delete (fst x) xs) ys) k =
   504         (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
   505       by simp
   506     show ?thesis
   507     proof (cases "fst x = k")
   508       case True
   509       from True delete_notin_dom [of k xs]
   510       have "map_of (delete (fst x) xs) k = None"
   511         by (simp add: map_of_eq_None_iff)
   512       with hyp show ?thesis
   513         using True None
   514         by simp
   515     next
   516       case False
   517       from False have "map_of (delete (fst x) xs) k = map_of xs k"
   518         by simp
   519       with hyp show ?thesis
   520         using False None by (simp add: map_comp_def)
   521     qed
   522   next
   523     case (Some v)
   524     with 2
   525     have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   526       by simp
   527     with Some show ?thesis
   528       by (auto simp add: map_comp_def)
   529   qed
   530 qed
   531 
   532 lemma compose_conv': "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   533   by (rule ext) (rule compose_conv)
   534 
   535 lemma compose_first_Some [simp]:
   536   assumes "map_of xs k = Some v"
   537   shows "map_of (compose xs ys) k = map_of ys v"
   538   using assms by (simp add: compose_conv)
   539 
   540 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   541 proof (induct xs ys rule: compose.induct)
   542   case 1
   543   then show ?case by simp
   544 next
   545   case (2 x xs ys)
   546   show ?case
   547   proof (cases "map_of ys (snd x)")
   548     case None
   549     with "2.hyps"
   550     have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   551       by simp
   552     also
   553     have "\<dots> \<subseteq> fst ` set xs"
   554       by (rule dom_delete_subset)
   555     finally show ?thesis
   556       using None
   557       by auto
   558   next
   559     case (Some v)
   560     with "2.hyps"
   561     have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   562       by simp
   563     with Some show ?thesis
   564       by auto
   565   qed
   566 qed
   567 
   568 lemma distinct_compose:
   569   assumes "distinct (map fst xs)"
   570   shows "distinct (map fst (compose xs ys))"
   571   using assms
   572 proof (induct xs ys rule: compose.induct)
   573   case 1
   574   then show ?case by simp
   575 next
   576   case (2 x xs ys)
   577   show ?case
   578   proof (cases "map_of ys (snd x)")
   579     case None
   580     with 2 show ?thesis by simp
   581   next
   582     case (Some v)
   583     with 2 dom_compose [of xs ys] show ?thesis
   584       by auto
   585   qed
   586 qed
   587 
   588 lemma compose_delete_twist: "compose (delete k xs) ys = delete k (compose xs ys)"
   589 proof (induct xs ys rule: compose.induct)
   590   case 1
   591   then show ?case by simp
   592 next
   593   case (2 x xs ys)
   594   show ?case
   595   proof (cases "map_of ys (snd x)")
   596     case None
   597     with 2 have hyp: "compose (delete k (delete (fst x) xs)) ys =
   598         delete k (compose (delete (fst x) xs) ys)"
   599       by simp
   600     show ?thesis
   601     proof (cases "fst x = k")
   602       case True
   603       with None hyp show ?thesis
   604         by (simp add: delete_idem)
   605     next
   606       case False
   607       from None False hyp show ?thesis
   608         by (simp add: delete_twist)
   609     qed
   610   next
   611     case (Some v)
   612     with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)"
   613       by simp
   614     with Some show ?thesis
   615       by simp
   616   qed
   617 qed
   618 
   619 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
   620   by (induct xs ys rule: compose.induct)
   621     (auto simp add: map_of_clearjunk split: option.splits)
   622 
   623 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
   624   by (induct xs rule: clearjunk.induct)
   625     (auto split: option.splits simp add: clearjunk_delete delete_idem compose_delete_twist)
   626 
   627 lemma compose_empty [simp]: "compose xs [] = []"
   628   by (induct xs) (auto simp add: compose_delete_twist)
   629 
   630 lemma compose_Some_iff:
   631   "(map_of (compose xs ys) k = Some v) \<longleftrightarrow>
   632     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)"
   633   by (simp add: compose_conv map_comp_Some_iff)
   634 
   635 lemma map_comp_None_iff:
   636   "map_of (compose xs ys) k = None \<longleftrightarrow>
   637     (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None))"
   638   by (simp add: compose_conv map_comp_None_iff)
   639 
   640 
   641 subsection {* @{text map_entry} *}
   642 
   643 fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   644 where
   645   "map_entry k f [] = []"
   646 | "map_entry k f (p # ps) =
   647     (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
   648 
   649 lemma map_of_map_entry:
   650   "map_of (map_entry k f xs) =
   651     (map_of xs)(k := case map_of xs k of None \<Rightarrow> None | Some v' \<Rightarrow> Some (f v'))"
   652   by (induct xs) auto
   653 
   654 lemma dom_map_entry: "fst ` set (map_entry k f xs) = fst ` set xs"
   655   by (induct xs) auto
   656 
   657 lemma distinct_map_entry:
   658   assumes "distinct (map fst xs)"
   659   shows "distinct (map fst (map_entry k f xs))"
   660   using assms by (induct xs) (auto simp add: dom_map_entry)
   661 
   662 
   663 subsection {* @{text map_default} *}
   664 
   665 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   666 where
   667   "map_default k v f [] = [(k, v)]"
   668 | "map_default k v f (p # ps) =
   669     (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
   670 
   671 lemma map_of_map_default:
   672   "map_of (map_default k v f xs) =
   673     (map_of xs)(k := case map_of xs k of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (f v'))"
   674   by (induct xs) auto
   675 
   676 lemma dom_map_default: "fst ` set (map_default k v f xs) = insert k (fst ` set xs)"
   677   by (induct xs) auto
   678 
   679 lemma distinct_map_default:
   680   assumes "distinct (map fst xs)"
   681   shows "distinct (map fst (map_default k v f xs))"
   682   using assms by (induct xs) (auto simp add: dom_map_default)
   683 
   684 hide_const (open) update updates delete restrict clearjunk merge compose map_entry
   685 
   686 end