moving connection of association lists to Mappings into a separate theory
authorbulwahn
Mon Sep 12 10:57:58 2011 +0200 (2011-09-12)
changeset 44897787983a08bfb
parent 44896 8b55b9c986a4
child 44898 ec3f30b8c78c
moving connection of association lists to Mappings into a separate theory
CONTRIBUTORS
src/HOL/IsaMakefile
src/HOL/Library/AList_Impl.thy
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Mon Sep 12 10:27:36 2011 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Sep 12 10:57:58 2011 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4    Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
     1.5    Prover IDE.
     1.6  
     1.7 +* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
     1.8 +  Theory HOL/Library/Cset_Monad allows do notation for computable
     1.9 +  sets (cset) via the generic monad ad-hoc overloading facility.
    1.10  
    1.11  Contributions to Isabelle2011
    1.12  -----------------------------
     2.1 --- a/src/HOL/IsaMakefile	Mon Sep 12 10:27:36 2011 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Sep 12 10:57:58 2011 +0200
     2.3 @@ -430,7 +430,8 @@
     2.4  $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
     2.5    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
     2.6    Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
     2.7 -  Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
     2.8 +  Library/AList_Impl.thy Library/AList_Mapping.thy 			\
     2.9 +  Library/BigO.thy Library/Binomial.thy 				\
    2.10    Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
    2.11    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    2.12    Library/Code_Char_ord.thy Library/Code_Integer.thy			\
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/AList_Impl.thy	Mon Sep 12 10:57:58 2011 +0200
     3.3 @@ -0,0 +1,656 @@
     3.4 +(*  Title:      HOL/Library/AList_Impl.thy
     3.5 +    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Implementation of Association Lists *}
     3.9 +
    3.10 +theory AList_Impl 
    3.11 +imports Main More_List
    3.12 +begin
    3.13 +
    3.14 +text {*
    3.15 +  The operations preserve distinctness of keys and 
    3.16 +  function @{term "clearjunk"} distributes over them. Since 
    3.17 +  @{term clearjunk} enforces distinctness of keys it can be used
    3.18 +  to establish the invariant, e.g. for inductive proofs.
    3.19 +*}
    3.20 +
    3.21 +subsection {* @{text update} and @{text updates} *}
    3.22 +
    3.23 +primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    3.24 +    "update k v [] = [(k, v)]"
    3.25 +  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    3.26 +
    3.27 +lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    3.28 +  by (induct al) (auto simp add: fun_eq_iff)
    3.29 +
    3.30 +corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
    3.31 +  by (simp add: update_conv')
    3.32 +
    3.33 +lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
    3.34 +  by (induct al) auto
    3.35 +
    3.36 +lemma update_keys:
    3.37 +  "map fst (update k v al) =
    3.38 +    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
    3.39 +  by (induct al) simp_all
    3.40 +
    3.41 +lemma distinct_update:
    3.42 +  assumes "distinct (map fst al)" 
    3.43 +  shows "distinct (map fst (update k v al))"
    3.44 +  using assms by (simp add: update_keys)
    3.45 +
    3.46 +lemma update_filter: 
    3.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]"
    3.48 +  by (induct ps) auto
    3.49 +
    3.50 +lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    3.51 +  by (induct al) auto
    3.52 +
    3.53 +lemma update_nonempty [simp]: "update k v al \<noteq> []"
    3.54 +  by (induct al) auto
    3.55 +
    3.56 +lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
    3.57 +proof (induct al arbitrary: al') 
    3.58 +  case Nil thus ?case 
    3.59 +    by (cases al') (auto split: split_if_asm)
    3.60 +next
    3.61 +  case Cons thus ?case
    3.62 +    by (cases al') (auto split: split_if_asm)
    3.63 +qed
    3.64 +
    3.65 +lemma update_last [simp]: "update k v (update k v' al) = update k v al"
    3.66 +  by (induct al) auto
    3.67 +
    3.68 +text {* Note that the lists are not necessarily the same:
    3.69 +        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and 
    3.70 +        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
    3.71 +lemma update_swap: "k\<noteq>k' 
    3.72 +  \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
    3.73 +  by (simp add: update_conv' fun_eq_iff)
    3.74 +
    3.75 +lemma update_Some_unfold: 
    3.76 +  "map_of (update k v al) x = Some y \<longleftrightarrow>
    3.77 +    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
    3.78 +  by (simp add: update_conv' map_upd_Some_unfold)
    3.79 +
    3.80 +lemma image_update [simp]:
    3.81 +  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    3.82 +  by (simp add: update_conv' image_map_upd)
    3.83 +
    3.84 +definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    3.85 +  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
    3.86 +
    3.87 +lemma updates_simps [simp]:
    3.88 +  "updates [] vs ps = ps"
    3.89 +  "updates ks [] ps = ps"
    3.90 +  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
    3.91 +  by (simp_all add: updates_def)
    3.92 +
    3.93 +lemma updates_key_simp [simp]:
    3.94 +  "updates (k # ks) vs ps =
    3.95 +    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
    3.96 +  by (cases vs) simp_all
    3.97 +
    3.98 +lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
    3.99 +proof -
   3.100 +  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
   3.101 +    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   3.102 +    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   3.103 +  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
   3.104 +qed
   3.105 +
   3.106 +lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   3.107 +  by (simp add: updates_conv')
   3.108 +
   3.109 +lemma distinct_updates:
   3.110 +  assumes "distinct (map fst al)"
   3.111 +  shows "distinct (map fst (updates ks vs al))"
   3.112 +proof -
   3.113 +  have "distinct (More_List.fold
   3.114 +       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
   3.115 +       (zip ks vs) (map fst al))"
   3.116 +    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   3.117 +  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
   3.118 +    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   3.119 +    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   3.120 +  ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
   3.121 +qed
   3.122 +
   3.123 +lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   3.124 +  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   3.125 +  by (induct ks arbitrary: vs al) (auto split: list.splits)
   3.126 +
   3.127 +lemma updates_list_update_drop[simp]:
   3.128 + "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
   3.129 +   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
   3.130 +  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
   3.131 +
   3.132 +lemma update_updates_conv_if: "
   3.133 + map_of (updates xs ys (update x y al)) =
   3.134 + map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
   3.135 +                                  else (update x y (updates xs ys al)))"
   3.136 +  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
   3.137 +
   3.138 +lemma updates_twist [simp]:
   3.139 + "k \<notin> set ks \<Longrightarrow> 
   3.140 +  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
   3.141 +  by (simp add: updates_conv' update_conv' map_upds_twist)
   3.142 +
   3.143 +lemma updates_apply_notin[simp]:
   3.144 + "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
   3.145 +  by (simp add: updates_conv)
   3.146 +
   3.147 +lemma updates_append_drop[simp]:
   3.148 +  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
   3.149 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
   3.150 +
   3.151 +lemma updates_append2_drop[simp]:
   3.152 +  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   3.153 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
   3.154 +
   3.155 +
   3.156 +subsection {* @{text delete} *}
   3.157 +
   3.158 +definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   3.159 +  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
   3.160 +
   3.161 +lemma delete_simps [simp]:
   3.162 +  "delete k [] = []"
   3.163 +  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   3.164 +  by (auto simp add: delete_eq)
   3.165 +
   3.166 +lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
   3.167 +  by (induct al) (auto simp add: fun_eq_iff)
   3.168 +
   3.169 +corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   3.170 +  by (simp add: delete_conv')
   3.171 +
   3.172 +lemma delete_keys:
   3.173 +  "map fst (delete k al) = removeAll k (map fst al)"
   3.174 +  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
   3.175 +
   3.176 +lemma distinct_delete:
   3.177 +  assumes "distinct (map fst al)" 
   3.178 +  shows "distinct (map fst (delete k al))"
   3.179 +  using assms by (simp add: delete_keys distinct_removeAll)
   3.180 +
   3.181 +lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   3.182 +  by (auto simp add: image_iff delete_eq filter_id_conv)
   3.183 +
   3.184 +lemma delete_idem: "delete k (delete k al) = delete k al"
   3.185 +  by (simp add: delete_eq)
   3.186 +
   3.187 +lemma map_of_delete [simp]:
   3.188 +    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
   3.189 +  by (simp add: delete_conv')
   3.190 +
   3.191 +lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   3.192 +  by (auto simp add: delete_eq)
   3.193 +
   3.194 +lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
   3.195 +  by (auto simp add: delete_eq)
   3.196 +
   3.197 +lemma delete_update_same:
   3.198 +  "delete k (update k v al) = delete k al"
   3.199 +  by (induct al) simp_all
   3.200 +
   3.201 +lemma delete_update:
   3.202 +  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
   3.203 +  by (induct al) simp_all
   3.204 +
   3.205 +lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
   3.206 +  by (simp add: delete_eq conj_commute)
   3.207 +
   3.208 +lemma length_delete_le: "length (delete k al) \<le> length al"
   3.209 +  by (simp add: delete_eq)
   3.210 +
   3.211 +
   3.212 +subsection {* @{text restrict} *}
   3.213 +
   3.214 +definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   3.215 +  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
   3.216 +
   3.217 +lemma restr_simps [simp]:
   3.218 +  "restrict A [] = []"
   3.219 +  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
   3.220 +  by (auto simp add: restrict_eq)
   3.221 +
   3.222 +lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   3.223 +proof
   3.224 +  fix k
   3.225 +  show "map_of (restrict A al) k = ((map_of al)|` A) k"
   3.226 +    by (induct al) (simp, cases "k \<in> A", auto)
   3.227 +qed
   3.228 +
   3.229 +corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   3.230 +  by (simp add: restr_conv')
   3.231 +
   3.232 +lemma distinct_restr:
   3.233 +  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   3.234 +  by (induct al) (auto simp add: restrict_eq)
   3.235 +
   3.236 +lemma restr_empty [simp]: 
   3.237 +  "restrict {} al = []" 
   3.238 +  "restrict A [] = []"
   3.239 +  by (induct al) (auto simp add: restrict_eq)
   3.240 +
   3.241 +lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
   3.242 +  by (simp add: restr_conv')
   3.243 +
   3.244 +lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
   3.245 +  by (simp add: restr_conv')
   3.246 +
   3.247 +lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   3.248 +  by (induct al) (auto simp add: restrict_eq)
   3.249 +
   3.250 +lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   3.251 +  by (induct al) (auto simp add: restrict_eq)
   3.252 +
   3.253 +lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   3.254 +  by (induct al) (auto simp add: restrict_eq)
   3.255 +
   3.256 +lemma restr_update[simp]:
   3.257 + "map_of (restrict D (update x y al)) = 
   3.258 +  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   3.259 +  by (simp add: restr_conv' update_conv')
   3.260 +
   3.261 +lemma restr_delete [simp]:
   3.262 +  "(delete x (restrict D al)) = 
   3.263 +    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
   3.264 +apply (simp add: delete_eq restrict_eq)
   3.265 +apply (auto simp add: split_def)
   3.266 +proof -
   3.267 +  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
   3.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]"
   3.269 +    by simp
   3.270 +  assume "x \<notin> D"
   3.271 +  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
   3.272 +  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
   3.273 +    by simp
   3.274 +qed
   3.275 +
   3.276 +lemma update_restr:
   3.277 + "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   3.278 +  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
   3.279 +
   3.280 +lemma upate_restr_conv [simp]:
   3.281 + "x \<in> D \<Longrightarrow> 
   3.282 + map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   3.283 +  by (simp add: update_conv' restr_conv')
   3.284 +
   3.285 +lemma restr_updates [simp]: "
   3.286 + \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   3.287 + \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
   3.288 +     map_of (updates xs ys (restrict (D - set xs) al))"
   3.289 +  by (simp add: updates_conv' restr_conv')
   3.290 +
   3.291 +lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   3.292 +  by (induct ps) auto
   3.293 +
   3.294 +
   3.295 +subsection {* @{text clearjunk} *}
   3.296 +
   3.297 +function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   3.298 +    "clearjunk [] = []"  
   3.299 +  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   3.300 +  by pat_completeness auto
   3.301 +termination by (relation "measure length")
   3.302 +  (simp_all add: less_Suc_eq_le length_delete_le)
   3.303 +
   3.304 +lemma map_of_clearjunk:
   3.305 +  "map_of (clearjunk al) = map_of al"
   3.306 +  by (induct al rule: clearjunk.induct)
   3.307 +    (simp_all add: fun_eq_iff)
   3.308 +
   3.309 +lemma clearjunk_keys_set:
   3.310 +  "set (map fst (clearjunk al)) = set (map fst al)"
   3.311 +  by (induct al rule: clearjunk.induct)
   3.312 +    (simp_all add: delete_keys)
   3.313 +
   3.314 +lemma dom_clearjunk:
   3.315 +  "fst ` set (clearjunk al) = fst ` set al"
   3.316 +  using clearjunk_keys_set by simp
   3.317 +
   3.318 +lemma distinct_clearjunk [simp]:
   3.319 +  "distinct (map fst (clearjunk al))"
   3.320 +  by (induct al rule: clearjunk.induct)
   3.321 +    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
   3.322 +
   3.323 +lemma ran_clearjunk:
   3.324 +  "ran (map_of (clearjunk al)) = ran (map_of al)"
   3.325 +  by (simp add: map_of_clearjunk)
   3.326 +
   3.327 +lemma ran_map_of:
   3.328 +  "ran (map_of al) = snd ` set (clearjunk al)"
   3.329 +proof -
   3.330 +  have "ran (map_of al) = ran (map_of (clearjunk al))"
   3.331 +    by (simp add: ran_clearjunk)
   3.332 +  also have "\<dots> = snd ` set (clearjunk al)"
   3.333 +    by (simp add: ran_distinct)
   3.334 +  finally show ?thesis .
   3.335 +qed
   3.336 +
   3.337 +lemma clearjunk_update:
   3.338 +  "clearjunk (update k v al) = update k v (clearjunk al)"
   3.339 +  by (induct al rule: clearjunk.induct)
   3.340 +    (simp_all add: delete_update)
   3.341 +
   3.342 +lemma clearjunk_updates:
   3.343 +  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   3.344 +proof -
   3.345 +  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
   3.346 +    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
   3.347 +    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   3.348 +  then show ?thesis by (simp add: updates_def fun_eq_iff)
   3.349 +qed
   3.350 +
   3.351 +lemma clearjunk_delete:
   3.352 +  "clearjunk (delete x al) = delete x (clearjunk al)"
   3.353 +  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   3.354 +
   3.355 +lemma clearjunk_restrict:
   3.356 + "clearjunk (restrict A al) = restrict A (clearjunk al)"
   3.357 +  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
   3.358 +
   3.359 +lemma distinct_clearjunk_id [simp]:
   3.360 +  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
   3.361 +  by (induct al rule: clearjunk.induct) auto
   3.362 +
   3.363 +lemma clearjunk_idem:
   3.364 +  "clearjunk (clearjunk al) = clearjunk al"
   3.365 +  by simp
   3.366 +
   3.367 +lemma length_clearjunk:
   3.368 +  "length (clearjunk al) \<le> length al"
   3.369 +proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   3.370 +  case Nil then show ?case by simp
   3.371 +next
   3.372 +  case (Cons kv al)
   3.373 +  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
   3.374 +  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
   3.375 +  then show ?case by simp
   3.376 +qed
   3.377 +
   3.378 +lemma delete_map:
   3.379 +  assumes "\<And>kv. fst (f kv) = fst kv"
   3.380 +  shows "delete k (map f ps) = map f (delete k ps)"
   3.381 +  by (simp add: delete_eq filter_map comp_def split_def assms)
   3.382 +
   3.383 +lemma clearjunk_map:
   3.384 +  assumes "\<And>kv. fst (f kv) = fst kv"
   3.385 +  shows "clearjunk (map f ps) = map f (clearjunk ps)"
   3.386 +  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
   3.387 +    (simp_all add: clearjunk_delete delete_map assms)
   3.388 +
   3.389 +
   3.390 +subsection {* @{text map_ran} *}
   3.391 +
   3.392 +definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   3.393 +  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
   3.394 +
   3.395 +lemma map_ran_simps [simp]:
   3.396 +  "map_ran f [] = []"
   3.397 +  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
   3.398 +  by (simp_all add: map_ran_def)
   3.399 +
   3.400 +lemma dom_map_ran:
   3.401 +  "fst ` set (map_ran f al) = fst ` set al"
   3.402 +  by (simp add: map_ran_def image_image split_def)
   3.403 +  
   3.404 +lemma map_ran_conv:
   3.405 +  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
   3.406 +  by (induct al) auto
   3.407 +
   3.408 +lemma distinct_map_ran:
   3.409 +  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
   3.410 +  by (simp add: map_ran_def split_def comp_def)
   3.411 +
   3.412 +lemma map_ran_filter:
   3.413 +  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   3.414 +  by (simp add: map_ran_def filter_map split_def comp_def)
   3.415 +
   3.416 +lemma clearjunk_map_ran:
   3.417 +  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   3.418 +  by (simp add: map_ran_def split_def clearjunk_map)
   3.419 +
   3.420 +
   3.421 +subsection {* @{text merge} *}
   3.422 +
   3.423 +definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   3.424 +  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
   3.425 +
   3.426 +lemma merge_simps [simp]:
   3.427 +  "merge qs [] = qs"
   3.428 +  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
   3.429 +  by (simp_all add: merge_def split_def)
   3.430 +
   3.431 +lemma merge_updates:
   3.432 +  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
   3.433 +  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
   3.434 +
   3.435 +lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   3.436 +  by (induct ys arbitrary: xs) (auto simp add: dom_update)
   3.437 +
   3.438 +lemma distinct_merge:
   3.439 +  assumes "distinct (map fst xs)"
   3.440 +  shows "distinct (map fst (merge xs ys))"
   3.441 +using assms by (simp add: merge_updates distinct_updates)
   3.442 +
   3.443 +lemma clearjunk_merge:
   3.444 +  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   3.445 +  by (simp add: merge_updates clearjunk_updates)
   3.446 +
   3.447 +lemma merge_conv':
   3.448 +  "map_of (merge xs ys) = map_of xs ++ map_of ys"
   3.449 +proof -
   3.450 +  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
   3.451 +    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   3.452 +    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   3.453 +  then show ?thesis
   3.454 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
   3.455 +qed
   3.456 +
   3.457 +corollary merge_conv:
   3.458 +  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
   3.459 +  by (simp add: merge_conv')
   3.460 +
   3.461 +lemma merge_empty: "map_of (merge [] ys) = map_of ys"
   3.462 +  by (simp add: merge_conv')
   3.463 +
   3.464 +lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
   3.465 +                           map_of (merge (merge m1 m2) m3)"
   3.466 +  by (simp add: merge_conv')
   3.467 +
   3.468 +lemma merge_Some_iff: 
   3.469 + "(map_of (merge m n) k = Some x) = 
   3.470 +  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
   3.471 +  by (simp add: merge_conv' map_add_Some_iff)
   3.472 +
   3.473 +lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
   3.474 +
   3.475 +lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   3.476 +  by (simp add: merge_conv')
   3.477 +
   3.478 +lemma merge_None [iff]: 
   3.479 +  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   3.480 +  by (simp add: merge_conv')
   3.481 +
   3.482 +lemma merge_upd[simp]: 
   3.483 +  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   3.484 +  by (simp add: update_conv' merge_conv')
   3.485 +
   3.486 +lemma merge_updatess[simp]: 
   3.487 +  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
   3.488 +  by (simp add: updates_conv' merge_conv')
   3.489 +
   3.490 +lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   3.491 +  by (simp add: merge_conv')
   3.492 +
   3.493 +
   3.494 +subsection {* @{text compose} *}
   3.495 +
   3.496 +function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
   3.497 +    "compose [] ys = []"
   3.498 +  | "compose (x#xs) ys = (case map_of ys (snd x)
   3.499 +       of None \<Rightarrow> compose (delete (fst x) xs) ys
   3.500 +        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   3.501 +  by pat_completeness auto
   3.502 +termination by (relation "measure (length \<circ> fst)")
   3.503 +  (simp_all add: less_Suc_eq_le length_delete_le)
   3.504 +
   3.505 +lemma compose_first_None [simp]: 
   3.506 +  assumes "map_of xs k = None" 
   3.507 +  shows "map_of (compose xs ys) k = None"
   3.508 +using assms by (induct xs ys rule: compose.induct)
   3.509 +  (auto split: option.splits split_if_asm)
   3.510 +
   3.511 +lemma compose_conv: 
   3.512 +  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   3.513 +proof (induct xs ys rule: compose.induct)
   3.514 +  case 1 then show ?case by simp
   3.515 +next
   3.516 +  case (2 x xs ys) show ?case
   3.517 +  proof (cases "map_of ys (snd x)")
   3.518 +    case None with 2
   3.519 +    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
   3.520 +               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
   3.521 +      by simp
   3.522 +    show ?thesis
   3.523 +    proof (cases "fst x = k")
   3.524 +      case True
   3.525 +      from True delete_notin_dom [of k xs]
   3.526 +      have "map_of (delete (fst x) xs) k = None"
   3.527 +        by (simp add: map_of_eq_None_iff)
   3.528 +      with hyp show ?thesis
   3.529 +        using True None
   3.530 +        by simp
   3.531 +    next
   3.532 +      case False
   3.533 +      from False have "map_of (delete (fst x) xs) k = map_of xs k"
   3.534 +        by simp
   3.535 +      with hyp show ?thesis
   3.536 +        using False None
   3.537 +        by (simp add: map_comp_def)
   3.538 +    qed
   3.539 +  next
   3.540 +    case (Some v)
   3.541 +    with 2
   3.542 +    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   3.543 +      by simp
   3.544 +    with Some show ?thesis
   3.545 +      by (auto simp add: map_comp_def)
   3.546 +  qed
   3.547 +qed
   3.548 +   
   3.549 +lemma compose_conv': 
   3.550 +  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   3.551 +  by (rule ext) (rule compose_conv)
   3.552 +
   3.553 +lemma compose_first_Some [simp]:
   3.554 +  assumes "map_of xs k = Some v" 
   3.555 +  shows "map_of (compose xs ys) k = map_of ys v"
   3.556 +using assms by (simp add: compose_conv)
   3.557 +
   3.558 +lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   3.559 +proof (induct xs ys rule: compose.induct)
   3.560 +  case 1 thus ?case by simp
   3.561 +next
   3.562 +  case (2 x xs ys)
   3.563 +  show ?case
   3.564 +  proof (cases "map_of ys (snd x)")
   3.565 +    case None
   3.566 +    with "2.hyps"
   3.567 +    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   3.568 +      by simp
   3.569 +    also
   3.570 +    have "\<dots> \<subseteq> fst ` set xs"
   3.571 +      by (rule dom_delete_subset)
   3.572 +    finally show ?thesis
   3.573 +      using None
   3.574 +      by auto
   3.575 +  next
   3.576 +    case (Some v)
   3.577 +    with "2.hyps"
   3.578 +    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   3.579 +      by simp
   3.580 +    with Some show ?thesis
   3.581 +      by auto
   3.582 +  qed
   3.583 +qed
   3.584 +
   3.585 +lemma distinct_compose:
   3.586 + assumes "distinct (map fst xs)"
   3.587 + shows "distinct (map fst (compose xs ys))"
   3.588 +using assms
   3.589 +proof (induct xs ys rule: compose.induct)
   3.590 +  case 1 thus ?case by simp
   3.591 +next
   3.592 +  case (2 x xs ys)
   3.593 +  show ?case
   3.594 +  proof (cases "map_of ys (snd x)")
   3.595 +    case None
   3.596 +    with 2 show ?thesis by simp
   3.597 +  next
   3.598 +    case (Some v)
   3.599 +    with 2 dom_compose [of xs ys] show ?thesis 
   3.600 +      by (auto)
   3.601 +  qed
   3.602 +qed
   3.603 +
   3.604 +lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
   3.605 +proof (induct xs ys rule: compose.induct)
   3.606 +  case 1 thus ?case by simp
   3.607 +next
   3.608 +  case (2 x xs ys)
   3.609 +  show ?case
   3.610 +  proof (cases "map_of ys (snd x)")
   3.611 +    case None
   3.612 +    with 2 have 
   3.613 +      hyp: "compose (delete k (delete (fst x) xs)) ys =
   3.614 +            delete k (compose (delete (fst x) xs) ys)"
   3.615 +      by simp
   3.616 +    show ?thesis
   3.617 +    proof (cases "fst x = k")
   3.618 +      case True
   3.619 +      with None hyp
   3.620 +      show ?thesis
   3.621 +        by (simp add: delete_idem)
   3.622 +    next
   3.623 +      case False
   3.624 +      from None False hyp
   3.625 +      show ?thesis
   3.626 +        by (simp add: delete_twist)
   3.627 +    qed
   3.628 +  next
   3.629 +    case (Some v)
   3.630 +    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
   3.631 +    with Some show ?thesis
   3.632 +      by simp
   3.633 +  qed
   3.634 +qed
   3.635 +
   3.636 +lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
   3.637 +  by (induct xs ys rule: compose.induct) 
   3.638 +     (auto simp add: map_of_clearjunk split: option.splits)
   3.639 +   
   3.640 +lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
   3.641 +  by (induct xs rule: clearjunk.induct)
   3.642 +     (auto split: option.splits simp add: clearjunk_delete delete_idem
   3.643 +               compose_delete_twist)
   3.644 +   
   3.645 +lemma compose_empty [simp]:
   3.646 + "compose xs [] = []"
   3.647 +  by (induct xs) (auto simp add: compose_delete_twist)
   3.648 +
   3.649 +lemma compose_Some_iff:
   3.650 +  "(map_of (compose xs ys) k = Some v) = 
   3.651 +     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
   3.652 +  by (simp add: compose_conv map_comp_Some_iff)
   3.653 +
   3.654 +lemma map_comp_None_iff:
   3.655 +  "(map_of (compose xs ys) k = None) = 
   3.656 +    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
   3.657 +  by (simp add: compose_conv map_comp_None_iff)
   3.658 +
   3.659 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/AList_Mapping.thy	Mon Sep 12 10:57:58 2011 +0200
     4.3 @@ -0,0 +1,72 @@
     4.4 +(* Title: HOL/Library/AList_Mapping.thy
     4.5 +   Author: Florian Haftmann, TU Muenchen
     4.6 +*)
     4.7 +
     4.8 +header {* Implementation of mappings with Association Lists *}
     4.9 +
    4.10 +theory AList_Mapping
    4.11 +imports AList_Impl Mapping
    4.12 +begin
    4.13 +
    4.14 +definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    4.15 +  "Mapping xs = Mapping.Mapping (map_of xs)"
    4.16 +
    4.17 +code_datatype Mapping
    4.18 +
    4.19 +lemma lookup_Mapping [simp, code]:
    4.20 +  "Mapping.lookup (Mapping xs) = map_of xs"
    4.21 +  by (simp add: Mapping_def)
    4.22 +
    4.23 +lemma keys_Mapping [simp, code]:
    4.24 +  "Mapping.keys (Mapping xs) = set (map fst xs)"
    4.25 +  by (simp add: keys_def dom_map_of_conv_image_fst)
    4.26 +
    4.27 +lemma empty_Mapping [code]:
    4.28 +  "Mapping.empty = Mapping []"
    4.29 +  by (rule mapping_eqI) simp
    4.30 +
    4.31 +lemma is_empty_Mapping [code]:
    4.32 +  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    4.33 +  by (cases xs) (simp_all add: is_empty_def null_def)
    4.34 +
    4.35 +lemma update_Mapping [code]:
    4.36 +  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
    4.37 +  by (rule mapping_eqI) (simp add: update_conv')
    4.38 +
    4.39 +lemma delete_Mapping [code]:
    4.40 +  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    4.41 +  by (rule mapping_eqI) (simp add: delete_conv')
    4.42 +
    4.43 +lemma ordered_keys_Mapping [code]:
    4.44 +  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    4.45 +  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
    4.46 +
    4.47 +lemma size_Mapping [code]:
    4.48 +  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    4.49 +  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
    4.50 +
    4.51 +lemma tabulate_Mapping [code]:
    4.52 +  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    4.53 +  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    4.54 +
    4.55 +lemma bulkload_Mapping [code]:
    4.56 +  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    4.57 +  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    4.58 +
    4.59 +lemma equal_Mapping [code]:
    4.60 +  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    4.61 +    (let ks = map fst xs; ls = map fst ys
    4.62 +    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))"
    4.63 +proof -
    4.64 +  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    4.65 +    by (auto simp add: image_def intro!: bexI)
    4.66 +  show ?thesis
    4.67 +    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    4.68 +      (auto dest!: map_of_eq_dom intro: aux)
    4.69 +qed
    4.70 +
    4.71 +lemma [code nbe]:
    4.72 +  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    4.73 +  by (fact equal_refl)
    4.74 +  
    4.75 +end
    4.76 \ No newline at end of file
     5.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 12 10:27:36 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,720 +0,0 @@
     5.4 -(*  Title:      HOL/Library/AssocList.thy
     5.5 -    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     5.6 -*)
     5.7 -
     5.8 -header {* Map operations implemented on association lists*}
     5.9 -
    5.10 -theory AssocList 
    5.11 -imports Main More_List Mapping
    5.12 -begin
    5.13 -
    5.14 -text {*
    5.15 -  The operations preserve distinctness of keys and 
    5.16 -  function @{term "clearjunk"} distributes over them. Since 
    5.17 -  @{term clearjunk} enforces distinctness of keys it can be used
    5.18 -  to establish the invariant, e.g. for inductive proofs.
    5.19 -*}
    5.20 -
    5.21 -subsection {* @{text update} and @{text updates} *}
    5.22 -
    5.23 -primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    5.24 -    "update k v [] = [(k, v)]"
    5.25 -  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    5.26 -
    5.27 -lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    5.28 -  by (induct al) (auto simp add: fun_eq_iff)
    5.29 -
    5.30 -corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
    5.31 -  by (simp add: update_conv')
    5.32 -
    5.33 -lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
    5.34 -  by (induct al) auto
    5.35 -
    5.36 -lemma update_keys:
    5.37 -  "map fst (update k v al) =
    5.38 -    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
    5.39 -  by (induct al) simp_all
    5.40 -
    5.41 -lemma distinct_update:
    5.42 -  assumes "distinct (map fst al)" 
    5.43 -  shows "distinct (map fst (update k v al))"
    5.44 -  using assms by (simp add: update_keys)
    5.45 -
    5.46 -lemma update_filter: 
    5.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]"
    5.48 -  by (induct ps) auto
    5.49 -
    5.50 -lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    5.51 -  by (induct al) auto
    5.52 -
    5.53 -lemma update_nonempty [simp]: "update k v al \<noteq> []"
    5.54 -  by (induct al) auto
    5.55 -
    5.56 -lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
    5.57 -proof (induct al arbitrary: al') 
    5.58 -  case Nil thus ?case 
    5.59 -    by (cases al') (auto split: split_if_asm)
    5.60 -next
    5.61 -  case Cons thus ?case
    5.62 -    by (cases al') (auto split: split_if_asm)
    5.63 -qed
    5.64 -
    5.65 -lemma update_last [simp]: "update k v (update k v' al) = update k v al"
    5.66 -  by (induct al) auto
    5.67 -
    5.68 -text {* Note that the lists are not necessarily the same:
    5.69 -        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and 
    5.70 -        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
    5.71 -lemma update_swap: "k\<noteq>k' 
    5.72 -  \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
    5.73 -  by (simp add: update_conv' fun_eq_iff)
    5.74 -
    5.75 -lemma update_Some_unfold: 
    5.76 -  "map_of (update k v al) x = Some y \<longleftrightarrow>
    5.77 -    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
    5.78 -  by (simp add: update_conv' map_upd_Some_unfold)
    5.79 -
    5.80 -lemma image_update [simp]:
    5.81 -  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    5.82 -  by (simp add: update_conv' image_map_upd)
    5.83 -
    5.84 -definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    5.85 -  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
    5.86 -
    5.87 -lemma updates_simps [simp]:
    5.88 -  "updates [] vs ps = ps"
    5.89 -  "updates ks [] ps = ps"
    5.90 -  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
    5.91 -  by (simp_all add: updates_def)
    5.92 -
    5.93 -lemma updates_key_simp [simp]:
    5.94 -  "updates (k # ks) vs ps =
    5.95 -    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
    5.96 -  by (cases vs) simp_all
    5.97 -
    5.98 -lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
    5.99 -proof -
   5.100 -  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
   5.101 -    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   5.102 -    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   5.103 -  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
   5.104 -qed
   5.105 -
   5.106 -lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   5.107 -  by (simp add: updates_conv')
   5.108 -
   5.109 -lemma distinct_updates:
   5.110 -  assumes "distinct (map fst al)"
   5.111 -  shows "distinct (map fst (updates ks vs al))"
   5.112 -proof -
   5.113 -  have "distinct (More_List.fold
   5.114 -       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
   5.115 -       (zip ks vs) (map fst al))"
   5.116 -    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   5.117 -  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
   5.118 -    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   5.119 -    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   5.120 -  ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
   5.121 -qed
   5.122 -
   5.123 -lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   5.124 -  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   5.125 -  by (induct ks arbitrary: vs al) (auto split: list.splits)
   5.126 -
   5.127 -lemma updates_list_update_drop[simp]:
   5.128 - "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
   5.129 -   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
   5.130 -  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
   5.131 -
   5.132 -lemma update_updates_conv_if: "
   5.133 - map_of (updates xs ys (update x y al)) =
   5.134 - map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
   5.135 -                                  else (update x y (updates xs ys al)))"
   5.136 -  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
   5.137 -
   5.138 -lemma updates_twist [simp]:
   5.139 - "k \<notin> set ks \<Longrightarrow> 
   5.140 -  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
   5.141 -  by (simp add: updates_conv' update_conv' map_upds_twist)
   5.142 -
   5.143 -lemma updates_apply_notin[simp]:
   5.144 - "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
   5.145 -  by (simp add: updates_conv)
   5.146 -
   5.147 -lemma updates_append_drop[simp]:
   5.148 -  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
   5.149 -  by (induct xs arbitrary: ys al) (auto split: list.splits)
   5.150 -
   5.151 -lemma updates_append2_drop[simp]:
   5.152 -  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   5.153 -  by (induct xs arbitrary: ys al) (auto split: list.splits)
   5.154 -
   5.155 -
   5.156 -subsection {* @{text delete} *}
   5.157 -
   5.158 -definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   5.159 -  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
   5.160 -
   5.161 -lemma delete_simps [simp]:
   5.162 -  "delete k [] = []"
   5.163 -  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   5.164 -  by (auto simp add: delete_eq)
   5.165 -
   5.166 -lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
   5.167 -  by (induct al) (auto simp add: fun_eq_iff)
   5.168 -
   5.169 -corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   5.170 -  by (simp add: delete_conv')
   5.171 -
   5.172 -lemma delete_keys:
   5.173 -  "map fst (delete k al) = removeAll k (map fst al)"
   5.174 -  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
   5.175 -
   5.176 -lemma distinct_delete:
   5.177 -  assumes "distinct (map fst al)" 
   5.178 -  shows "distinct (map fst (delete k al))"
   5.179 -  using assms by (simp add: delete_keys distinct_removeAll)
   5.180 -
   5.181 -lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   5.182 -  by (auto simp add: image_iff delete_eq filter_id_conv)
   5.183 -
   5.184 -lemma delete_idem: "delete k (delete k al) = delete k al"
   5.185 -  by (simp add: delete_eq)
   5.186 -
   5.187 -lemma map_of_delete [simp]:
   5.188 -    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
   5.189 -  by (simp add: delete_conv')
   5.190 -
   5.191 -lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   5.192 -  by (auto simp add: delete_eq)
   5.193 -
   5.194 -lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
   5.195 -  by (auto simp add: delete_eq)
   5.196 -
   5.197 -lemma delete_update_same:
   5.198 -  "delete k (update k v al) = delete k al"
   5.199 -  by (induct al) simp_all
   5.200 -
   5.201 -lemma delete_update:
   5.202 -  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
   5.203 -  by (induct al) simp_all
   5.204 -
   5.205 -lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
   5.206 -  by (simp add: delete_eq conj_commute)
   5.207 -
   5.208 -lemma length_delete_le: "length (delete k al) \<le> length al"
   5.209 -  by (simp add: delete_eq)
   5.210 -
   5.211 -
   5.212 -subsection {* @{text restrict} *}
   5.213 -
   5.214 -definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   5.215 -  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
   5.216 -
   5.217 -lemma restr_simps [simp]:
   5.218 -  "restrict A [] = []"
   5.219 -  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
   5.220 -  by (auto simp add: restrict_eq)
   5.221 -
   5.222 -lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   5.223 -proof
   5.224 -  fix k
   5.225 -  show "map_of (restrict A al) k = ((map_of al)|` A) k"
   5.226 -    by (induct al) (simp, cases "k \<in> A", auto)
   5.227 -qed
   5.228 -
   5.229 -corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   5.230 -  by (simp add: restr_conv')
   5.231 -
   5.232 -lemma distinct_restr:
   5.233 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   5.234 -  by (induct al) (auto simp add: restrict_eq)
   5.235 -
   5.236 -lemma restr_empty [simp]: 
   5.237 -  "restrict {} al = []" 
   5.238 -  "restrict A [] = []"
   5.239 -  by (induct al) (auto simp add: restrict_eq)
   5.240 -
   5.241 -lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
   5.242 -  by (simp add: restr_conv')
   5.243 -
   5.244 -lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
   5.245 -  by (simp add: restr_conv')
   5.246 -
   5.247 -lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   5.248 -  by (induct al) (auto simp add: restrict_eq)
   5.249 -
   5.250 -lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   5.251 -  by (induct al) (auto simp add: restrict_eq)
   5.252 -
   5.253 -lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   5.254 -  by (induct al) (auto simp add: restrict_eq)
   5.255 -
   5.256 -lemma restr_update[simp]:
   5.257 - "map_of (restrict D (update x y al)) = 
   5.258 -  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   5.259 -  by (simp add: restr_conv' update_conv')
   5.260 -
   5.261 -lemma restr_delete [simp]:
   5.262 -  "(delete x (restrict D al)) = 
   5.263 -    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
   5.264 -apply (simp add: delete_eq restrict_eq)
   5.265 -apply (auto simp add: split_def)
   5.266 -proof -
   5.267 -  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
   5.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]"
   5.269 -    by simp
   5.270 -  assume "x \<notin> D"
   5.271 -  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
   5.272 -  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
   5.273 -    by simp
   5.274 -qed
   5.275 -
   5.276 -lemma update_restr:
   5.277 - "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   5.278 -  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
   5.279 -
   5.280 -lemma upate_restr_conv [simp]:
   5.281 - "x \<in> D \<Longrightarrow> 
   5.282 - map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   5.283 -  by (simp add: update_conv' restr_conv')
   5.284 -
   5.285 -lemma restr_updates [simp]: "
   5.286 - \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   5.287 - \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
   5.288 -     map_of (updates xs ys (restrict (D - set xs) al))"
   5.289 -  by (simp add: updates_conv' restr_conv')
   5.290 -
   5.291 -lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   5.292 -  by (induct ps) auto
   5.293 -
   5.294 -
   5.295 -subsection {* @{text clearjunk} *}
   5.296 -
   5.297 -function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   5.298 -    "clearjunk [] = []"  
   5.299 -  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   5.300 -  by pat_completeness auto
   5.301 -termination by (relation "measure length")
   5.302 -  (simp_all add: less_Suc_eq_le length_delete_le)
   5.303 -
   5.304 -lemma map_of_clearjunk:
   5.305 -  "map_of (clearjunk al) = map_of al"
   5.306 -  by (induct al rule: clearjunk.induct)
   5.307 -    (simp_all add: fun_eq_iff)
   5.308 -
   5.309 -lemma clearjunk_keys_set:
   5.310 -  "set (map fst (clearjunk al)) = set (map fst al)"
   5.311 -  by (induct al rule: clearjunk.induct)
   5.312 -    (simp_all add: delete_keys)
   5.313 -
   5.314 -lemma dom_clearjunk:
   5.315 -  "fst ` set (clearjunk al) = fst ` set al"
   5.316 -  using clearjunk_keys_set by simp
   5.317 -
   5.318 -lemma distinct_clearjunk [simp]:
   5.319 -  "distinct (map fst (clearjunk al))"
   5.320 -  by (induct al rule: clearjunk.induct)
   5.321 -    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
   5.322 -
   5.323 -lemma ran_clearjunk:
   5.324 -  "ran (map_of (clearjunk al)) = ran (map_of al)"
   5.325 -  by (simp add: map_of_clearjunk)
   5.326 -
   5.327 -lemma ran_map_of:
   5.328 -  "ran (map_of al) = snd ` set (clearjunk al)"
   5.329 -proof -
   5.330 -  have "ran (map_of al) = ran (map_of (clearjunk al))"
   5.331 -    by (simp add: ran_clearjunk)
   5.332 -  also have "\<dots> = snd ` set (clearjunk al)"
   5.333 -    by (simp add: ran_distinct)
   5.334 -  finally show ?thesis .
   5.335 -qed
   5.336 -
   5.337 -lemma clearjunk_update:
   5.338 -  "clearjunk (update k v al) = update k v (clearjunk al)"
   5.339 -  by (induct al rule: clearjunk.induct)
   5.340 -    (simp_all add: delete_update)
   5.341 -
   5.342 -lemma clearjunk_updates:
   5.343 -  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   5.344 -proof -
   5.345 -  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
   5.346 -    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
   5.347 -    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   5.348 -  then show ?thesis by (simp add: updates_def fun_eq_iff)
   5.349 -qed
   5.350 -
   5.351 -lemma clearjunk_delete:
   5.352 -  "clearjunk (delete x al) = delete x (clearjunk al)"
   5.353 -  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   5.354 -
   5.355 -lemma clearjunk_restrict:
   5.356 - "clearjunk (restrict A al) = restrict A (clearjunk al)"
   5.357 -  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
   5.358 -
   5.359 -lemma distinct_clearjunk_id [simp]:
   5.360 -  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
   5.361 -  by (induct al rule: clearjunk.induct) auto
   5.362 -
   5.363 -lemma clearjunk_idem:
   5.364 -  "clearjunk (clearjunk al) = clearjunk al"
   5.365 -  by simp
   5.366 -
   5.367 -lemma length_clearjunk:
   5.368 -  "length (clearjunk al) \<le> length al"
   5.369 -proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   5.370 -  case Nil then show ?case by simp
   5.371 -next
   5.372 -  case (Cons kv al)
   5.373 -  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
   5.374 -  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
   5.375 -  then show ?case by simp
   5.376 -qed
   5.377 -
   5.378 -lemma delete_map:
   5.379 -  assumes "\<And>kv. fst (f kv) = fst kv"
   5.380 -  shows "delete k (map f ps) = map f (delete k ps)"
   5.381 -  by (simp add: delete_eq filter_map comp_def split_def assms)
   5.382 -
   5.383 -lemma clearjunk_map:
   5.384 -  assumes "\<And>kv. fst (f kv) = fst kv"
   5.385 -  shows "clearjunk (map f ps) = map f (clearjunk ps)"
   5.386 -  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
   5.387 -    (simp_all add: clearjunk_delete delete_map assms)
   5.388 -
   5.389 -
   5.390 -subsection {* @{text map_ran} *}
   5.391 -
   5.392 -definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   5.393 -  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
   5.394 -
   5.395 -lemma map_ran_simps [simp]:
   5.396 -  "map_ran f [] = []"
   5.397 -  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
   5.398 -  by (simp_all add: map_ran_def)
   5.399 -
   5.400 -lemma dom_map_ran:
   5.401 -  "fst ` set (map_ran f al) = fst ` set al"
   5.402 -  by (simp add: map_ran_def image_image split_def)
   5.403 -  
   5.404 -lemma map_ran_conv:
   5.405 -  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
   5.406 -  by (induct al) auto
   5.407 -
   5.408 -lemma distinct_map_ran:
   5.409 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
   5.410 -  by (simp add: map_ran_def split_def comp_def)
   5.411 -
   5.412 -lemma map_ran_filter:
   5.413 -  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   5.414 -  by (simp add: map_ran_def filter_map split_def comp_def)
   5.415 -
   5.416 -lemma clearjunk_map_ran:
   5.417 -  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   5.418 -  by (simp add: map_ran_def split_def clearjunk_map)
   5.419 -
   5.420 -
   5.421 -subsection {* @{text merge} *}
   5.422 -
   5.423 -definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
   5.424 -  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
   5.425 -
   5.426 -lemma merge_simps [simp]:
   5.427 -  "merge qs [] = qs"
   5.428 -  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
   5.429 -  by (simp_all add: merge_def split_def)
   5.430 -
   5.431 -lemma merge_updates:
   5.432 -  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
   5.433 -  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
   5.434 -
   5.435 -lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   5.436 -  by (induct ys arbitrary: xs) (auto simp add: dom_update)
   5.437 -
   5.438 -lemma distinct_merge:
   5.439 -  assumes "distinct (map fst xs)"
   5.440 -  shows "distinct (map fst (merge xs ys))"
   5.441 -using assms by (simp add: merge_updates distinct_updates)
   5.442 -
   5.443 -lemma clearjunk_merge:
   5.444 -  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   5.445 -  by (simp add: merge_updates clearjunk_updates)
   5.446 -
   5.447 -lemma merge_conv':
   5.448 -  "map_of (merge xs ys) = map_of xs ++ map_of ys"
   5.449 -proof -
   5.450 -  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
   5.451 -    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   5.452 -    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   5.453 -  then show ?thesis
   5.454 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
   5.455 -qed
   5.456 -
   5.457 -corollary merge_conv:
   5.458 -  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
   5.459 -  by (simp add: merge_conv')
   5.460 -
   5.461 -lemma merge_empty: "map_of (merge [] ys) = map_of ys"
   5.462 -  by (simp add: merge_conv')
   5.463 -
   5.464 -lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
   5.465 -                           map_of (merge (merge m1 m2) m3)"
   5.466 -  by (simp add: merge_conv')
   5.467 -
   5.468 -lemma merge_Some_iff: 
   5.469 - "(map_of (merge m n) k = Some x) = 
   5.470 -  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
   5.471 -  by (simp add: merge_conv' map_add_Some_iff)
   5.472 -
   5.473 -lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
   5.474 -
   5.475 -lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   5.476 -  by (simp add: merge_conv')
   5.477 -
   5.478 -lemma merge_None [iff]: 
   5.479 -  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   5.480 -  by (simp add: merge_conv')
   5.481 -
   5.482 -lemma merge_upd[simp]: 
   5.483 -  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   5.484 -  by (simp add: update_conv' merge_conv')
   5.485 -
   5.486 -lemma merge_updatess[simp]: 
   5.487 -  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
   5.488 -  by (simp add: updates_conv' merge_conv')
   5.489 -
   5.490 -lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   5.491 -  by (simp add: merge_conv')
   5.492 -
   5.493 -
   5.494 -subsection {* @{text compose} *}
   5.495 -
   5.496 -function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
   5.497 -    "compose [] ys = []"
   5.498 -  | "compose (x#xs) ys = (case map_of ys (snd x)
   5.499 -       of None \<Rightarrow> compose (delete (fst x) xs) ys
   5.500 -        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   5.501 -  by pat_completeness auto
   5.502 -termination by (relation "measure (length \<circ> fst)")
   5.503 -  (simp_all add: less_Suc_eq_le length_delete_le)
   5.504 -
   5.505 -lemma compose_first_None [simp]: 
   5.506 -  assumes "map_of xs k = None" 
   5.507 -  shows "map_of (compose xs ys) k = None"
   5.508 -using assms by (induct xs ys rule: compose.induct)
   5.509 -  (auto split: option.splits split_if_asm)
   5.510 -
   5.511 -lemma compose_conv: 
   5.512 -  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   5.513 -proof (induct xs ys rule: compose.induct)
   5.514 -  case 1 then show ?case by simp
   5.515 -next
   5.516 -  case (2 x xs ys) show ?case
   5.517 -  proof (cases "map_of ys (snd x)")
   5.518 -    case None with 2
   5.519 -    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
   5.520 -               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
   5.521 -      by simp
   5.522 -    show ?thesis
   5.523 -    proof (cases "fst x = k")
   5.524 -      case True
   5.525 -      from True delete_notin_dom [of k xs]
   5.526 -      have "map_of (delete (fst x) xs) k = None"
   5.527 -        by (simp add: map_of_eq_None_iff)
   5.528 -      with hyp show ?thesis
   5.529 -        using True None
   5.530 -        by simp
   5.531 -    next
   5.532 -      case False
   5.533 -      from False have "map_of (delete (fst x) xs) k = map_of xs k"
   5.534 -        by simp
   5.535 -      with hyp show ?thesis
   5.536 -        using False None
   5.537 -        by (simp add: map_comp_def)
   5.538 -    qed
   5.539 -  next
   5.540 -    case (Some v)
   5.541 -    with 2
   5.542 -    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   5.543 -      by simp
   5.544 -    with Some show ?thesis
   5.545 -      by (auto simp add: map_comp_def)
   5.546 -  qed
   5.547 -qed
   5.548 -   
   5.549 -lemma compose_conv': 
   5.550 -  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   5.551 -  by (rule ext) (rule compose_conv)
   5.552 -
   5.553 -lemma compose_first_Some [simp]:
   5.554 -  assumes "map_of xs k = Some v" 
   5.555 -  shows "map_of (compose xs ys) k = map_of ys v"
   5.556 -using assms by (simp add: compose_conv)
   5.557 -
   5.558 -lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   5.559 -proof (induct xs ys rule: compose.induct)
   5.560 -  case 1 thus ?case by simp
   5.561 -next
   5.562 -  case (2 x xs ys)
   5.563 -  show ?case
   5.564 -  proof (cases "map_of ys (snd x)")
   5.565 -    case None
   5.566 -    with "2.hyps"
   5.567 -    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   5.568 -      by simp
   5.569 -    also
   5.570 -    have "\<dots> \<subseteq> fst ` set xs"
   5.571 -      by (rule dom_delete_subset)
   5.572 -    finally show ?thesis
   5.573 -      using None
   5.574 -      by auto
   5.575 -  next
   5.576 -    case (Some v)
   5.577 -    with "2.hyps"
   5.578 -    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   5.579 -      by simp
   5.580 -    with Some show ?thesis
   5.581 -      by auto
   5.582 -  qed
   5.583 -qed
   5.584 -
   5.585 -lemma distinct_compose:
   5.586 - assumes "distinct (map fst xs)"
   5.587 - shows "distinct (map fst (compose xs ys))"
   5.588 -using assms
   5.589 -proof (induct xs ys rule: compose.induct)
   5.590 -  case 1 thus ?case by simp
   5.591 -next
   5.592 -  case (2 x xs ys)
   5.593 -  show ?case
   5.594 -  proof (cases "map_of ys (snd x)")
   5.595 -    case None
   5.596 -    with 2 show ?thesis by simp
   5.597 -  next
   5.598 -    case (Some v)
   5.599 -    with 2 dom_compose [of xs ys] show ?thesis 
   5.600 -      by (auto)
   5.601 -  qed
   5.602 -qed
   5.603 -
   5.604 -lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
   5.605 -proof (induct xs ys rule: compose.induct)
   5.606 -  case 1 thus ?case by simp
   5.607 -next
   5.608 -  case (2 x xs ys)
   5.609 -  show ?case
   5.610 -  proof (cases "map_of ys (snd x)")
   5.611 -    case None
   5.612 -    with 2 have 
   5.613 -      hyp: "compose (delete k (delete (fst x) xs)) ys =
   5.614 -            delete k (compose (delete (fst x) xs) ys)"
   5.615 -      by simp
   5.616 -    show ?thesis
   5.617 -    proof (cases "fst x = k")
   5.618 -      case True
   5.619 -      with None hyp
   5.620 -      show ?thesis
   5.621 -        by (simp add: delete_idem)
   5.622 -    next
   5.623 -      case False
   5.624 -      from None False hyp
   5.625 -      show ?thesis
   5.626 -        by (simp add: delete_twist)
   5.627 -    qed
   5.628 -  next
   5.629 -    case (Some v)
   5.630 -    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
   5.631 -    with Some show ?thesis
   5.632 -      by simp
   5.633 -  qed
   5.634 -qed
   5.635 -
   5.636 -lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
   5.637 -  by (induct xs ys rule: compose.induct) 
   5.638 -     (auto simp add: map_of_clearjunk split: option.splits)
   5.639 -   
   5.640 -lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
   5.641 -  by (induct xs rule: clearjunk.induct)
   5.642 -     (auto split: option.splits simp add: clearjunk_delete delete_idem
   5.643 -               compose_delete_twist)
   5.644 -   
   5.645 -lemma compose_empty [simp]:
   5.646 - "compose xs [] = []"
   5.647 -  by (induct xs) (auto simp add: compose_delete_twist)
   5.648 -
   5.649 -lemma compose_Some_iff:
   5.650 -  "(map_of (compose xs ys) k = Some v) = 
   5.651 -     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
   5.652 -  by (simp add: compose_conv map_comp_Some_iff)
   5.653 -
   5.654 -lemma map_comp_None_iff:
   5.655 -  "(map_of (compose xs ys) k = None) = 
   5.656 -    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
   5.657 -  by (simp add: compose_conv map_comp_None_iff)
   5.658 -
   5.659 -
   5.660 -subsection {* Implementation of mappings *}
   5.661 -
   5.662 -definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
   5.663 -  "Mapping xs = Mapping.Mapping (map_of xs)"
   5.664 -
   5.665 -code_datatype Mapping
   5.666 -
   5.667 -lemma lookup_Mapping [simp, code]:
   5.668 -  "Mapping.lookup (Mapping xs) = map_of xs"
   5.669 -  by (simp add: Mapping_def)
   5.670 -
   5.671 -lemma keys_Mapping [simp, code]:
   5.672 -  "Mapping.keys (Mapping xs) = set (map fst xs)"
   5.673 -  by (simp add: keys_def dom_map_of_conv_image_fst)
   5.674 -
   5.675 -lemma empty_Mapping [code]:
   5.676 -  "Mapping.empty = Mapping []"
   5.677 -  by (rule mapping_eqI) simp
   5.678 -
   5.679 -lemma is_empty_Mapping [code]:
   5.680 -  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
   5.681 -  by (cases xs) (simp_all add: is_empty_def null_def)
   5.682 -
   5.683 -lemma update_Mapping [code]:
   5.684 -  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
   5.685 -  by (rule mapping_eqI) (simp add: update_conv')
   5.686 -
   5.687 -lemma delete_Mapping [code]:
   5.688 -  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
   5.689 -  by (rule mapping_eqI) (simp add: delete_conv')
   5.690 -
   5.691 -lemma ordered_keys_Mapping [code]:
   5.692 -  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
   5.693 -  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
   5.694 -
   5.695 -lemma size_Mapping [code]:
   5.696 -  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
   5.697 -  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
   5.698 -
   5.699 -lemma tabulate_Mapping [code]:
   5.700 -  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
   5.701 -  by (rule mapping_eqI) (simp add: map_of_map_restrict)
   5.702 -
   5.703 -lemma bulkload_Mapping [code]:
   5.704 -  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   5.705 -  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
   5.706 -
   5.707 -lemma equal_Mapping [code]:
   5.708 -  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
   5.709 -    (let ks = map fst xs; ls = map fst ys
   5.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))"
   5.711 -proof -
   5.712 -  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
   5.713 -    by (auto simp add: image_def intro!: bexI)
   5.714 -  show ?thesis
   5.715 -    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
   5.716 -      (auto dest!: map_of_eq_dom intro: aux)
   5.717 -qed
   5.718 -
   5.719 -lemma [code nbe]:
   5.720 -  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   5.721 -  by (fact equal_refl)
   5.722 -
   5.723 -end
     6.1 --- a/src/HOL/Library/Library.thy	Mon Sep 12 10:27:36 2011 +0200
     6.2 +++ b/src/HOL/Library/Library.thy	Mon Sep 12 10:57:58 2011 +0200
     6.3 @@ -2,7 +2,7 @@
     6.4  theory Library
     6.5  imports
     6.6    Abstract_Rat
     6.7 -  AssocList
     6.8 +  AList_Mapping
     6.9    BigO
    6.10    Binomial
    6.11    Bit