src/HOL/Library/AssocList.thy
changeset 44897 787983a08bfb
parent 44896 8b55b9c986a4
child 44898 ec3f30b8c78c
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 12 10:27:36 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,720 +0,0 @@
     1.4 -(*  Title:      HOL/Library/AssocList.thy
     1.5 -    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Map operations implemented on association lists*}
     1.9 -
    1.10 -theory AssocList 
    1.11 -imports Main More_List Mapping
    1.12 -begin
    1.13 -
    1.14 -text {*
    1.15 -  The operations preserve distinctness of keys and 
    1.16 -  function @{term "clearjunk"} distributes over them. Since 
    1.17 -  @{term clearjunk} enforces distinctness of keys it can be used
    1.18 -  to establish the invariant, e.g. for inductive proofs.
    1.19 -*}
    1.20 -
    1.21 -subsection {* @{text update} and @{text updates} *}
    1.22 -
    1.23 -primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    1.24 -    "update k v [] = [(k, v)]"
    1.25 -  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.26 -
    1.27 -lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    1.28 -  by (induct al) (auto simp add: fun_eq_iff)
    1.29 -
    1.30 -corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
    1.31 -  by (simp add: update_conv')
    1.32 -
    1.33 -lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
    1.34 -  by (induct al) auto
    1.35 -
    1.36 -lemma update_keys:
    1.37 -  "map fst (update k v al) =
    1.38 -    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
    1.39 -  by (induct al) simp_all
    1.40 -
    1.41 -lemma distinct_update:
    1.42 -  assumes "distinct (map fst al)" 
    1.43 -  shows "distinct (map fst (update k v al))"
    1.44 -  using assms by (simp add: update_keys)
    1.45 -
    1.46 -lemma update_filter: 
    1.47 -  "a\<noteq>k \<Longrightarrow> update k v [q\<leftarrow>ps . fst q \<noteq> a] = [q\<leftarrow>update k v ps . fst q \<noteq> a]"
    1.48 -  by (induct ps) auto
    1.49 -
    1.50 -lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    1.51 -  by (induct al) auto
    1.52 -
    1.53 -lemma update_nonempty [simp]: "update k v al \<noteq> []"
    1.54 -  by (induct al) auto
    1.55 -
    1.56 -lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
    1.57 -proof (induct al arbitrary: al') 
    1.58 -  case Nil thus ?case 
    1.59 -    by (cases al') (auto split: split_if_asm)
    1.60 -next
    1.61 -  case Cons thus ?case
    1.62 -    by (cases al') (auto split: split_if_asm)
    1.63 -qed
    1.64 -
    1.65 -lemma update_last [simp]: "update k v (update k v' al) = update k v al"
    1.66 -  by (induct al) auto
    1.67 -
    1.68 -text {* Note that the lists are not necessarily the same:
    1.69 -        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and 
    1.70 -        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
    1.71 -lemma update_swap: "k\<noteq>k' 
    1.72 -  \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
    1.73 -  by (simp add: update_conv' fun_eq_iff)
    1.74 -
    1.75 -lemma update_Some_unfold: 
    1.76 -  "map_of (update k v al) x = Some y \<longleftrightarrow>
    1.77 -    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
    1.78 -  by (simp add: update_conv' map_upd_Some_unfold)
    1.79 -
    1.80 -lemma image_update [simp]:
    1.81 -  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    1.82 -  by (simp add: update_conv' image_map_upd)
    1.83 -
    1.84 -definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    1.85 -  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
    1.86 -
    1.87 -lemma updates_simps [simp]:
    1.88 -  "updates [] vs ps = ps"
    1.89 -  "updates ks [] ps = ps"
    1.90 -  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
    1.91 -  by (simp_all add: updates_def)
    1.92 -
    1.93 -lemma updates_key_simp [simp]:
    1.94 -  "updates (k # ks) vs ps =
    1.95 -    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
    1.96 -  by (cases vs) simp_all
    1.97 -
    1.98 -lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
    1.99 -proof -
   1.100 -  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
   1.101 -    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   1.102 -    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   1.103 -  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
   1.104 -qed
   1.105 -
   1.106 -lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   1.107 -  by (simp add: updates_conv')
   1.108 -
   1.109 -lemma distinct_updates:
   1.110 -  assumes "distinct (map fst al)"
   1.111 -  shows "distinct (map fst (updates ks vs al))"
   1.112 -proof -
   1.113 -  have "distinct (More_List.fold
   1.114 -       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
   1.115 -       (zip ks vs) (map fst al))"
   1.116 -    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   1.117 -  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
   1.118 -    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   1.119 -    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   1.120 -  ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
   1.121 -qed
   1.122 -
   1.123 -lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   1.124 -  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   1.125 -  by (induct ks arbitrary: vs al) (auto split: list.splits)
   1.126 -
   1.127 -lemma updates_list_update_drop[simp]:
   1.128 - "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
   1.129 -   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
   1.130 -  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
   1.131 -
   1.132 -lemma update_updates_conv_if: "
   1.133 - map_of (updates xs ys (update x y al)) =
   1.134 - map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
   1.135 -                                  else (update x y (updates xs ys al)))"
   1.136 -  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
   1.137 -
   1.138 -lemma updates_twist [simp]:
   1.139 - "k \<notin> set ks \<Longrightarrow> 
   1.140 -  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
   1.141 -  by (simp add: updates_conv' update_conv' map_upds_twist)
   1.142 -
   1.143 -lemma updates_apply_notin[simp]:
   1.144 - "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
   1.145 -  by (simp add: updates_conv)
   1.146 -
   1.147 -lemma updates_append_drop[simp]:
   1.148 -  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
   1.149 -  by (induct xs arbitrary: ys al) (auto split: list.splits)
   1.150 -
   1.151 -lemma updates_append2_drop[simp]:
   1.152 -  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   1.153 -  by (induct xs arbitrary: ys al) (auto split: list.splits)
   1.154 -
   1.155 -
   1.156 -subsection {* @{text delete} *}
   1.157 -
   1.158 -definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   1.159 -  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
   1.160 -
   1.161 -lemma delete_simps [simp]:
   1.162 -  "delete k [] = []"
   1.163 -  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   1.164 -  by (auto simp add: delete_eq)
   1.165 -
   1.166 -lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
   1.167 -  by (induct al) (auto simp add: fun_eq_iff)
   1.168 -
   1.169 -corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   1.170 -  by (simp add: delete_conv')
   1.171 -
   1.172 -lemma delete_keys:
   1.173 -  "map fst (delete k al) = removeAll k (map fst al)"
   1.174 -  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
   1.175 -
   1.176 -lemma distinct_delete:
   1.177 -  assumes "distinct (map fst al)" 
   1.178 -  shows "distinct (map fst (delete k al))"
   1.179 -  using assms by (simp add: delete_keys distinct_removeAll)
   1.180 -
   1.181 -lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   1.182 -  by (auto simp add: image_iff delete_eq filter_id_conv)
   1.183 -
   1.184 -lemma delete_idem: "delete k (delete k al) = delete k al"
   1.185 -  by (simp add: delete_eq)
   1.186 -
   1.187 -lemma map_of_delete [simp]:
   1.188 -    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
   1.189 -  by (simp add: delete_conv')
   1.190 -
   1.191 -lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   1.192 -  by (auto simp add: delete_eq)
   1.193 -
   1.194 -lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
   1.195 -  by (auto simp add: delete_eq)
   1.196 -
   1.197 -lemma delete_update_same:
   1.198 -  "delete k (update k v al) = delete k al"
   1.199 -  by (induct al) simp_all
   1.200 -
   1.201 -lemma delete_update:
   1.202 -  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
   1.203 -  by (induct al) simp_all
   1.204 -
   1.205 -lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
   1.206 -  by (simp add: delete_eq conj_commute)
   1.207 -
   1.208 -lemma length_delete_le: "length (delete k al) \<le> length al"
   1.209 -  by (simp add: delete_eq)
   1.210 -
   1.211 -
   1.212 -subsection {* @{text restrict} *}
   1.213 -
   1.214 -definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   1.215 -  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
   1.216 -
   1.217 -lemma restr_simps [simp]:
   1.218 -  "restrict A [] = []"
   1.219 -  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
   1.220 -  by (auto simp add: restrict_eq)
   1.221 -
   1.222 -lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   1.223 -proof
   1.224 -  fix k
   1.225 -  show "map_of (restrict A al) k = ((map_of al)|` A) k"
   1.226 -    by (induct al) (simp, cases "k \<in> A", auto)
   1.227 -qed
   1.228 -
   1.229 -corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   1.230 -  by (simp add: restr_conv')
   1.231 -
   1.232 -lemma distinct_restr:
   1.233 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   1.234 -  by (induct al) (auto simp add: restrict_eq)
   1.235 -
   1.236 -lemma restr_empty [simp]: 
   1.237 -  "restrict {} al = []" 
   1.238 -  "restrict A [] = []"
   1.239 -  by (induct al) (auto simp add: restrict_eq)
   1.240 -
   1.241 -lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
   1.242 -  by (simp add: restr_conv')
   1.243 -
   1.244 -lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
   1.245 -  by (simp add: restr_conv')
   1.246 -
   1.247 -lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   1.248 -  by (induct al) (auto simp add: restrict_eq)
   1.249 -
   1.250 -lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   1.251 -  by (induct al) (auto simp add: restrict_eq)
   1.252 -
   1.253 -lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   1.254 -  by (induct al) (auto simp add: restrict_eq)
   1.255 -
   1.256 -lemma restr_update[simp]:
   1.257 - "map_of (restrict D (update x y al)) = 
   1.258 -  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   1.259 -  by (simp add: restr_conv' update_conv')
   1.260 -
   1.261 -lemma restr_delete [simp]:
   1.262 -  "(delete x (restrict D al)) = 
   1.263 -    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
   1.264 -apply (simp add: delete_eq restrict_eq)
   1.265 -apply (auto simp add: split_def)
   1.266 -proof -
   1.267 -  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
   1.268 -  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]"
   1.269 -    by simp
   1.270 -  assume "x \<notin> D"
   1.271 -  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
   1.272 -  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
   1.273 -    by simp
   1.274 -qed
   1.275 -
   1.276 -lemma update_restr:
   1.277 - "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   1.278 -  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
   1.279 -
   1.280 -lemma upate_restr_conv [simp]:
   1.281 - "x \<in> D \<Longrightarrow> 
   1.282 - map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   1.283 -  by (simp add: update_conv' restr_conv')
   1.284 -
   1.285 -lemma restr_updates [simp]: "
   1.286 - \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   1.287 - \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
   1.288 -     map_of (updates xs ys (restrict (D - set xs) al))"
   1.289 -  by (simp add: updates_conv' restr_conv')
   1.290 -
   1.291 -lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   1.292 -  by (induct ps) auto
   1.293 -
   1.294 -
   1.295 -subsection {* @{text clearjunk} *}
   1.296 -
   1.297 -function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   1.298 -    "clearjunk [] = []"  
   1.299 -  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   1.300 -  by pat_completeness auto
   1.301 -termination by (relation "measure length")
   1.302 -  (simp_all add: less_Suc_eq_le length_delete_le)
   1.303 -
   1.304 -lemma map_of_clearjunk:
   1.305 -  "map_of (clearjunk al) = map_of al"
   1.306 -  by (induct al rule: clearjunk.induct)
   1.307 -    (simp_all add: fun_eq_iff)
   1.308 -
   1.309 -lemma clearjunk_keys_set:
   1.310 -  "set (map fst (clearjunk al)) = set (map fst al)"
   1.311 -  by (induct al rule: clearjunk.induct)
   1.312 -    (simp_all add: delete_keys)
   1.313 -
   1.314 -lemma dom_clearjunk:
   1.315 -  "fst ` set (clearjunk al) = fst ` set al"
   1.316 -  using clearjunk_keys_set by simp
   1.317 -
   1.318 -lemma distinct_clearjunk [simp]:
   1.319 -  "distinct (map fst (clearjunk al))"
   1.320 -  by (induct al rule: clearjunk.induct)
   1.321 -    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
   1.322 -
   1.323 -lemma ran_clearjunk:
   1.324 -  "ran (map_of (clearjunk al)) = ran (map_of al)"
   1.325 -  by (simp add: map_of_clearjunk)
   1.326 -
   1.327 -lemma ran_map_of:
   1.328 -  "ran (map_of al) = snd ` set (clearjunk al)"
   1.329 -proof -
   1.330 -  have "ran (map_of al) = ran (map_of (clearjunk al))"
   1.331 -    by (simp add: ran_clearjunk)
   1.332 -  also have "\<dots> = snd ` set (clearjunk al)"
   1.333 -    by (simp add: ran_distinct)
   1.334 -  finally show ?thesis .
   1.335 -qed
   1.336 -
   1.337 -lemma clearjunk_update:
   1.338 -  "clearjunk (update k v al) = update k v (clearjunk al)"
   1.339 -  by (induct al rule: clearjunk.induct)
   1.340 -    (simp_all add: delete_update)
   1.341 -
   1.342 -lemma clearjunk_updates:
   1.343 -  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   1.344 -proof -
   1.345 -  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
   1.346 -    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
   1.347 -    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   1.348 -  then show ?thesis by (simp add: updates_def fun_eq_iff)
   1.349 -qed
   1.350 -
   1.351 -lemma clearjunk_delete:
   1.352 -  "clearjunk (delete x al) = delete x (clearjunk al)"
   1.353 -  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   1.354 -
   1.355 -lemma clearjunk_restrict:
   1.356 - "clearjunk (restrict A al) = restrict A (clearjunk al)"
   1.357 -  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
   1.358 -
   1.359 -lemma distinct_clearjunk_id [simp]:
   1.360 -  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
   1.361 -  by (induct al rule: clearjunk.induct) auto
   1.362 -
   1.363 -lemma clearjunk_idem:
   1.364 -  "clearjunk (clearjunk al) = clearjunk al"
   1.365 -  by simp
   1.366 -
   1.367 -lemma length_clearjunk:
   1.368 -  "length (clearjunk al) \<le> length al"
   1.369 -proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   1.370 -  case Nil then show ?case by simp
   1.371 -next
   1.372 -  case (Cons kv al)
   1.373 -  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
   1.374 -  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
   1.375 -  then show ?case by simp
   1.376 -qed
   1.377 -
   1.378 -lemma delete_map:
   1.379 -  assumes "\<And>kv. fst (f kv) = fst kv"
   1.380 -  shows "delete k (map f ps) = map f (delete k ps)"
   1.381 -  by (simp add: delete_eq filter_map comp_def split_def assms)
   1.382 -
   1.383 -lemma clearjunk_map:
   1.384 -  assumes "\<And>kv. fst (f kv) = fst kv"
   1.385 -  shows "clearjunk (map f ps) = map f (clearjunk ps)"
   1.386 -  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
   1.387 -    (simp_all add: clearjunk_delete delete_map assms)
   1.388 -
   1.389 -
   1.390 -subsection {* @{text map_ran} *}
   1.391 -
   1.392 -definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   1.393 -  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
   1.394 -
   1.395 -lemma map_ran_simps [simp]:
   1.396 -  "map_ran f [] = []"
   1.397 -  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
   1.398 -  by (simp_all add: map_ran_def)
   1.399 -
   1.400 -lemma dom_map_ran:
   1.401 -  "fst ` set (map_ran f al) = fst ` set al"
   1.402 -  by (simp add: map_ran_def image_image split_def)
   1.403 -  
   1.404 -lemma map_ran_conv:
   1.405 -  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
   1.406 -  by (induct al) auto
   1.407 -
   1.408 -lemma distinct_map_ran:
   1.409 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
   1.410 -  by (simp add: map_ran_def split_def comp_def)
   1.411 -
   1.412 -lemma map_ran_filter:
   1.413 -  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   1.414 -  by (simp add: map_ran_def filter_map split_def comp_def)
   1.415 -
   1.416 -lemma clearjunk_map_ran:
   1.417 -  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   1.418 -  by (simp add: map_ran_def split_def clearjunk_map)
   1.419 -
   1.420 -
   1.421 -subsection {* @{text merge} *}
   1.422 -
   1.423 -definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   1.424 -  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
   1.425 -
   1.426 -lemma merge_simps [simp]:
   1.427 -  "merge qs [] = qs"
   1.428 -  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
   1.429 -  by (simp_all add: merge_def split_def)
   1.430 -
   1.431 -lemma merge_updates:
   1.432 -  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
   1.433 -  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
   1.434 -
   1.435 -lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   1.436 -  by (induct ys arbitrary: xs) (auto simp add: dom_update)
   1.437 -
   1.438 -lemma distinct_merge:
   1.439 -  assumes "distinct (map fst xs)"
   1.440 -  shows "distinct (map fst (merge xs ys))"
   1.441 -using assms by (simp add: merge_updates distinct_updates)
   1.442 -
   1.443 -lemma clearjunk_merge:
   1.444 -  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   1.445 -  by (simp add: merge_updates clearjunk_updates)
   1.446 -
   1.447 -lemma merge_conv':
   1.448 -  "map_of (merge xs ys) = map_of xs ++ map_of ys"
   1.449 -proof -
   1.450 -  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
   1.451 -    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   1.452 -    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   1.453 -  then show ?thesis
   1.454 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
   1.455 -qed
   1.456 -
   1.457 -corollary merge_conv:
   1.458 -  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
   1.459 -  by (simp add: merge_conv')
   1.460 -
   1.461 -lemma merge_empty: "map_of (merge [] ys) = map_of ys"
   1.462 -  by (simp add: merge_conv')
   1.463 -
   1.464 -lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
   1.465 -                           map_of (merge (merge m1 m2) m3)"
   1.466 -  by (simp add: merge_conv')
   1.467 -
   1.468 -lemma merge_Some_iff: 
   1.469 - "(map_of (merge m n) k = Some x) = 
   1.470 -  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
   1.471 -  by (simp add: merge_conv' map_add_Some_iff)
   1.472 -
   1.473 -lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
   1.474 -
   1.475 -lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   1.476 -  by (simp add: merge_conv')
   1.477 -
   1.478 -lemma merge_None [iff]: 
   1.479 -  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   1.480 -  by (simp add: merge_conv')
   1.481 -
   1.482 -lemma merge_upd[simp]: 
   1.483 -  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   1.484 -  by (simp add: update_conv' merge_conv')
   1.485 -
   1.486 -lemma merge_updatess[simp]: 
   1.487 -  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
   1.488 -  by (simp add: updates_conv' merge_conv')
   1.489 -
   1.490 -lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   1.491 -  by (simp add: merge_conv')
   1.492 -
   1.493 -
   1.494 -subsection {* @{text compose} *}
   1.495 -
   1.496 -function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
   1.497 -    "compose [] ys = []"
   1.498 -  | "compose (x#xs) ys = (case map_of ys (snd x)
   1.499 -       of None \<Rightarrow> compose (delete (fst x) xs) ys
   1.500 -        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   1.501 -  by pat_completeness auto
   1.502 -termination by (relation "measure (length \<circ> fst)")
   1.503 -  (simp_all add: less_Suc_eq_le length_delete_le)
   1.504 -
   1.505 -lemma compose_first_None [simp]: 
   1.506 -  assumes "map_of xs k = None" 
   1.507 -  shows "map_of (compose xs ys) k = None"
   1.508 -using assms by (induct xs ys rule: compose.induct)
   1.509 -  (auto split: option.splits split_if_asm)
   1.510 -
   1.511 -lemma compose_conv: 
   1.512 -  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   1.513 -proof (induct xs ys rule: compose.induct)
   1.514 -  case 1 then show ?case by simp
   1.515 -next
   1.516 -  case (2 x xs ys) show ?case
   1.517 -  proof (cases "map_of ys (snd x)")
   1.518 -    case None with 2
   1.519 -    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
   1.520 -               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
   1.521 -      by simp
   1.522 -    show ?thesis
   1.523 -    proof (cases "fst x = k")
   1.524 -      case True
   1.525 -      from True delete_notin_dom [of k xs]
   1.526 -      have "map_of (delete (fst x) xs) k = None"
   1.527 -        by (simp add: map_of_eq_None_iff)
   1.528 -      with hyp show ?thesis
   1.529 -        using True None
   1.530 -        by simp
   1.531 -    next
   1.532 -      case False
   1.533 -      from False have "map_of (delete (fst x) xs) k = map_of xs k"
   1.534 -        by simp
   1.535 -      with hyp show ?thesis
   1.536 -        using False None
   1.537 -        by (simp add: map_comp_def)
   1.538 -    qed
   1.539 -  next
   1.540 -    case (Some v)
   1.541 -    with 2
   1.542 -    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   1.543 -      by simp
   1.544 -    with Some show ?thesis
   1.545 -      by (auto simp add: map_comp_def)
   1.546 -  qed
   1.547 -qed
   1.548 -   
   1.549 -lemma compose_conv': 
   1.550 -  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   1.551 -  by (rule ext) (rule compose_conv)
   1.552 -
   1.553 -lemma compose_first_Some [simp]:
   1.554 -  assumes "map_of xs k = Some v" 
   1.555 -  shows "map_of (compose xs ys) k = map_of ys v"
   1.556 -using assms by (simp add: compose_conv)
   1.557 -
   1.558 -lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   1.559 -proof (induct xs ys rule: compose.induct)
   1.560 -  case 1 thus ?case by simp
   1.561 -next
   1.562 -  case (2 x xs ys)
   1.563 -  show ?case
   1.564 -  proof (cases "map_of ys (snd x)")
   1.565 -    case None
   1.566 -    with "2.hyps"
   1.567 -    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   1.568 -      by simp
   1.569 -    also
   1.570 -    have "\<dots> \<subseteq> fst ` set xs"
   1.571 -      by (rule dom_delete_subset)
   1.572 -    finally show ?thesis
   1.573 -      using None
   1.574 -      by auto
   1.575 -  next
   1.576 -    case (Some v)
   1.577 -    with "2.hyps"
   1.578 -    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   1.579 -      by simp
   1.580 -    with Some show ?thesis
   1.581 -      by auto
   1.582 -  qed
   1.583 -qed
   1.584 -
   1.585 -lemma distinct_compose:
   1.586 - assumes "distinct (map fst xs)"
   1.587 - shows "distinct (map fst (compose xs ys))"
   1.588 -using assms
   1.589 -proof (induct xs ys rule: compose.induct)
   1.590 -  case 1 thus ?case by simp
   1.591 -next
   1.592 -  case (2 x xs ys)
   1.593 -  show ?case
   1.594 -  proof (cases "map_of ys (snd x)")
   1.595 -    case None
   1.596 -    with 2 show ?thesis by simp
   1.597 -  next
   1.598 -    case (Some v)
   1.599 -    with 2 dom_compose [of xs ys] show ?thesis 
   1.600 -      by (auto)
   1.601 -  qed
   1.602 -qed
   1.603 -
   1.604 -lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
   1.605 -proof (induct xs ys rule: compose.induct)
   1.606 -  case 1 thus ?case by simp
   1.607 -next
   1.608 -  case (2 x xs ys)
   1.609 -  show ?case
   1.610 -  proof (cases "map_of ys (snd x)")
   1.611 -    case None
   1.612 -    with 2 have 
   1.613 -      hyp: "compose (delete k (delete (fst x) xs)) ys =
   1.614 -            delete k (compose (delete (fst x) xs) ys)"
   1.615 -      by simp
   1.616 -    show ?thesis
   1.617 -    proof (cases "fst x = k")
   1.618 -      case True
   1.619 -      with None hyp
   1.620 -      show ?thesis
   1.621 -        by (simp add: delete_idem)
   1.622 -    next
   1.623 -      case False
   1.624 -      from None False hyp
   1.625 -      show ?thesis
   1.626 -        by (simp add: delete_twist)
   1.627 -    qed
   1.628 -  next
   1.629 -    case (Some v)
   1.630 -    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
   1.631 -    with Some show ?thesis
   1.632 -      by simp
   1.633 -  qed
   1.634 -qed
   1.635 -
   1.636 -lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
   1.637 -  by (induct xs ys rule: compose.induct) 
   1.638 -     (auto simp add: map_of_clearjunk split: option.splits)
   1.639 -   
   1.640 -lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
   1.641 -  by (induct xs rule: clearjunk.induct)
   1.642 -     (auto split: option.splits simp add: clearjunk_delete delete_idem
   1.643 -               compose_delete_twist)
   1.644 -   
   1.645 -lemma compose_empty [simp]:
   1.646 - "compose xs [] = []"
   1.647 -  by (induct xs) (auto simp add: compose_delete_twist)
   1.648 -
   1.649 -lemma compose_Some_iff:
   1.650 -  "(map_of (compose xs ys) k = Some v) = 
   1.651 -     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
   1.652 -  by (simp add: compose_conv map_comp_Some_iff)
   1.653 -
   1.654 -lemma map_comp_None_iff:
   1.655 -  "(map_of (compose xs ys) k = None) = 
   1.656 -    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
   1.657 -  by (simp add: compose_conv map_comp_None_iff)
   1.658 -
   1.659 -
   1.660 -subsection {* Implementation of mappings *}
   1.661 -
   1.662 -definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
   1.663 -  "Mapping xs = Mapping.Mapping (map_of xs)"
   1.664 -
   1.665 -code_datatype Mapping
   1.666 -
   1.667 -lemma lookup_Mapping [simp, code]:
   1.668 -  "Mapping.lookup (Mapping xs) = map_of xs"
   1.669 -  by (simp add: Mapping_def)
   1.670 -
   1.671 -lemma keys_Mapping [simp, code]:
   1.672 -  "Mapping.keys (Mapping xs) = set (map fst xs)"
   1.673 -  by (simp add: keys_def dom_map_of_conv_image_fst)
   1.674 -
   1.675 -lemma empty_Mapping [code]:
   1.676 -  "Mapping.empty = Mapping []"
   1.677 -  by (rule mapping_eqI) simp
   1.678 -
   1.679 -lemma is_empty_Mapping [code]:
   1.680 -  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
   1.681 -  by (cases xs) (simp_all add: is_empty_def null_def)
   1.682 -
   1.683 -lemma update_Mapping [code]:
   1.684 -  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
   1.685 -  by (rule mapping_eqI) (simp add: update_conv')
   1.686 -
   1.687 -lemma delete_Mapping [code]:
   1.688 -  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
   1.689 -  by (rule mapping_eqI) (simp add: delete_conv')
   1.690 -
   1.691 -lemma ordered_keys_Mapping [code]:
   1.692 -  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
   1.693 -  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
   1.694 -
   1.695 -lemma size_Mapping [code]:
   1.696 -  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
   1.697 -  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
   1.698 -
   1.699 -lemma tabulate_Mapping [code]:
   1.700 -  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
   1.701 -  by (rule mapping_eqI) (simp add: map_of_map_restrict)
   1.702 -
   1.703 -lemma bulkload_Mapping [code]:
   1.704 -  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   1.705 -  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
   1.706 -
   1.707 -lemma equal_Mapping [code]:
   1.708 -  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
   1.709 -    (let ks = map fst xs; ls = map fst ys
   1.710 -    in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
   1.711 -proof -
   1.712 -  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
   1.713 -    by (auto simp add: image_def intro!: bexI)
   1.714 -  show ?thesis
   1.715 -    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
   1.716 -      (auto dest!: map_of_eq_dom intro: aux)
   1.717 -qed
   1.718 -
   1.719 -lemma [code nbe]:
   1.720 -  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   1.721 -  by (fact equal_refl)
   1.722 -
   1.723 -end