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