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