src/HOL/Library/AssocList.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23281 e26ec695c9b3
child 23373 ead82c82da9e
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/AssocList.thy
     2     ID:         $Id$
     3     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
     4 *)
     5 
     6 header {* Map operations implemented on association lists*}
     7 
     8 theory AssocList 
     9 imports Map
    10 begin
    11 
    12 text {*
    13   The operations preserve distinctness of keys and 
    14   function @{term "clearjunk"} distributes over them. Since 
    15   @{term clearjunk} enforces distinctness of keys it can be used
    16   to establish the invariant, e.g. for inductive proofs.
    17 *}
    18 
    19 fun
    20   delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    21 where
    22   "delete k [] = []"
    23   | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
    24 
    25 fun
    26   update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    27 where
    28     "update k v [] = [(k, v)]"
    29   | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    30 
    31 function
    32   updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    33 where
    34     "updates [] vs ps = ps"
    35   | "updates (k#ks) vs ps = (case vs
    36       of [] \<Rightarrow> ps
    37        | (v#vs') \<Rightarrow> updates ks vs' (update k v ps))"
    38 by pat_completeness auto
    39 termination by lexicographic_order
    40 
    41 fun
    42   merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    43 where
    44     "merge qs [] = qs"
    45   | "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
    46 
    47 lemma length_delete_le: "length (delete k al) \<le> length al"
    48 proof (induct al)
    49   case Nil thus ?case by simp
    50 next
    51   case (Cons a al)
    52   note length_filter_le [of "\<lambda>p. fst p \<noteq> fst a" al] 
    53   also have "\<And>n. n \<le> Suc n"
    54     by simp
    55   finally have "length [p\<leftarrow>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
    56   with Cons show ?case
    57     by auto
    58 qed
    59 
    60 lemma compose_hint [simp]:
    61   "length (delete k al) < Suc (length al)"
    62 proof -
    63   note length_delete_le
    64   also have "\<And>n. n < Suc n"
    65     by simp
    66   finally show ?thesis .
    67 qed
    68 
    69 function
    70   compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    71 where
    72     "compose [] ys = []"
    73   | "compose (x#xs) ys = (case map_of ys (snd x)
    74        of None \<Rightarrow> compose (delete (fst x) xs) ys
    75         | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
    76 by pat_completeness auto
    77 termination by lexicographic_order
    78 
    79 fun
    80   restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    81 where
    82   "restrict A [] = []"
    83   | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
    84 
    85 fun
    86   map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    87 where
    88   "map_ran f [] = []"
    89   | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
    90 
    91 fun
    92   clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    93 where
    94   "clearjunk [] = []"  
    95   | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
    96 
    97 lemmas [simp del] = compose_hint
    98 
    99 
   100 (* ******************************************************************************** *)
   101 subsection {* Lookup *}
   102 (* ******************************************************************************** *)
   103 
   104 lemma lookup_simps [code func]: 
   105   "map_of [] k = None"
   106   "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
   107   by simp_all
   108 
   109 
   110 (* ******************************************************************************** *)
   111 subsection {* @{const delete} *}
   112 (* ******************************************************************************** *)
   113 
   114 lemma delete_def:
   115   "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
   116   by (induct xs) auto
   117 
   118 lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   119   by (induct al) auto
   120 
   121 lemma delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   122   by (induct al) auto
   123 
   124 lemma delete_conv': "map_of (delete k al) = ((map_of al)(k := None))"
   125   by (rule ext) (rule delete_conv)
   126 
   127 lemma delete_idem: "delete k (delete k al) = delete k al"
   128   by (induct al) auto
   129 
   130 lemma map_of_delete [simp]:
   131     "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
   132   by (induct al) auto
   133 
   134 lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   135   by (induct al) auto
   136 
   137 lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
   138   by (induct al) auto
   139 
   140 lemma distinct_delete:
   141   assumes "distinct (map fst al)" 
   142   shows "distinct (map fst (delete k al))"
   143 using prems
   144 proof (induct al)
   145   case Nil thus ?case by simp
   146 next
   147   case (Cons a al)
   148   from Cons.prems obtain 
   149     a_notin_al: "fst a \<notin> fst ` set al" and
   150     dist_al: "distinct (map fst al)"
   151     by auto
   152   show ?case
   153   proof (cases "fst a = k")
   154     case True
   155     from True dist_al show ?thesis by simp
   156   next
   157     case False
   158     from dist_al
   159     have "distinct (map fst (delete k al))"
   160       by (rule Cons.hyps)
   161     moreover from a_notin_al dom_delete_subset [of k al] 
   162     have "fst a \<notin> fst ` set (delete k al)"
   163       by blast
   164     ultimately show ?thesis using False by simp
   165   qed
   166 qed
   167 
   168 lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
   169   by (induct al) auto
   170 
   171 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
   172   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
   173 
   174 (* ******************************************************************************** *)
   175 subsection {* @{const clearjunk} *}
   176 (* ******************************************************************************** *)
   177 
   178 lemma insert_fst_filter: 
   179   "insert a(fst ` {x \<in> set ps. fst x \<noteq> a}) = insert a (fst ` set ps)"
   180   by (induct ps) auto
   181 
   182 lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
   183   by (induct al rule: clearjunk.induct) (simp_all add: insert_fst_filter delete_def)
   184 
   185 lemma notin_filter_fst: "a \<notin> fst ` {x \<in> set ps. fst x \<noteq> a}"
   186   by (induct ps) auto
   187 
   188 lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
   189   by (induct al rule: clearjunk.induct) 
   190      (simp_all add: dom_clearjunk notin_filter_fst delete_def)
   191 
   192 lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<leftarrow>ps . fst q \<noteq> a] k = map_of ps k"
   193   by (induct ps) auto
   194 
   195 lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
   196   apply (rule ext)
   197   apply (induct al rule: clearjunk.induct)
   198   apply  simp
   199   apply (simp add: map_of_filter)
   200   done
   201 
   202 lemma length_clearjunk: "length (clearjunk al) \<le> length al"
   203 proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   204   case Nil thus ?case by simp
   205 next
   206   case (Cons p ps)
   207   from Cons have "length (clearjunk [q\<leftarrow>ps . fst q \<noteq> fst p]) \<le> length [q\<leftarrow>ps . fst q \<noteq> fst p]" 
   208     by (simp add: delete_def)
   209   also have "\<dots> \<le> length ps"
   210     by simp
   211   finally show ?case
   212     by (simp add: delete_def)
   213 qed
   214 
   215 lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<leftarrow>ps . fst q \<noteq> a] = ps"
   216   by (induct ps) auto
   217             
   218 lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
   219   by (induct al rule: clearjunk.induct) (auto simp add: notin_fst_filter)
   220 
   221 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
   222   by simp
   223 
   224 (* ******************************************************************************** *)
   225 subsection {* @{const dom} and @{term "ran"} *}
   226 (* ******************************************************************************** *)
   227 
   228 lemma dom_map_of': "fst ` set al = dom (map_of al)"
   229   by (induct al) auto
   230 
   231 lemmas dom_map_of = dom_map_of' [symmetric]
   232 
   233 lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)"
   234   by (simp add: map_of_clearjunk)
   235 
   236 lemma ran_distinct: 
   237   assumes dist: "distinct (map fst al)" 
   238   shows "ran (map_of al) = snd ` set al"
   239 using dist
   240 proof (induct al) 
   241   case Nil
   242   thus ?case by simp
   243 next
   244   case (Cons a al)
   245   hence hyp: "snd ` set al = ran (map_of al)"
   246     by simp
   247 
   248   have "ran (map_of (a # al)) = {snd a} \<union> ran (map_of al)"
   249   proof 
   250     show "ran (map_of (a # al)) \<subseteq> {snd a} \<union> ran (map_of al)"
   251     proof   
   252       fix v
   253       assume "v \<in> ran (map_of (a#al))"
   254       then obtain x where "map_of (a#al) x = Some v"
   255 	by (auto simp add: ran_def)
   256       then show "v \<in> {snd a} \<union> ran (map_of al)"
   257 	by (auto split: split_if_asm simp add: ran_def)
   258     qed
   259   next
   260     show "{snd a} \<union> ran (map_of al) \<subseteq> ran (map_of (a # al))"
   261     proof 
   262       fix v
   263       assume v_in: "v \<in> {snd a} \<union> ran (map_of al)"
   264       show "v \<in> ran (map_of (a#al))"
   265       proof (cases "v=snd a")
   266 	case True
   267 	with v_in show ?thesis
   268 	  by (auto simp add: ran_def)
   269       next
   270 	case False
   271 	with v_in have "v \<in> ran (map_of al)" by auto
   272 	then obtain x where al_x: "map_of al x = Some v"
   273 	  by (auto simp add: ran_def)
   274 	from map_of_SomeD [OF this]
   275 	have "x \<in> fst ` set al"
   276 	  by (force simp add: image_def)
   277 	with Cons.prems have "x\<noteq>fst a"
   278 	  by - (rule ccontr,simp)
   279 	with al_x
   280 	show ?thesis
   281 	  by (auto simp add: ran_def)
   282       qed
   283     qed
   284   qed
   285   with hyp show ?case
   286     by (simp only:) auto
   287 qed
   288 
   289 lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)"
   290 proof -
   291   have "ran (map_of al) = ran (map_of (clearjunk al))"
   292     by (simp add: ran_clearjunk)
   293   also have "\<dots> = snd ` set (clearjunk al)"
   294     by (simp add: ran_distinct)
   295   finally show ?thesis .
   296 qed
   297    
   298 (* ******************************************************************************** *)
   299 subsection {* @{const update} *}
   300 (* ******************************************************************************** *)
   301 
   302 lemma update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
   303   by (induct al) auto
   304 
   305 lemma update_conv': "map_of (update k v al)  = ((map_of al)(k\<mapsto>v))"
   306   by (rule ext) (rule update_conv)
   307 
   308 lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
   309   by (induct al) auto
   310 
   311 lemma distinct_update:
   312   assumes "distinct (map fst al)" 
   313   shows "distinct (map fst (update k v al))"
   314 using prems
   315 proof (induct al)
   316   case Nil thus ?case by simp
   317 next
   318   case (Cons a al)
   319   from Cons.prems obtain 
   320     a_notin_al: "fst a \<notin> fst ` set al" and
   321     dist_al: "distinct (map fst al)"
   322     by auto
   323   show ?case
   324   proof (cases "fst a = k")
   325     case True
   326     from True dist_al a_notin_al show ?thesis by simp
   327   next
   328     case False
   329     from dist_al
   330     have "distinct (map fst (update k v al))"
   331       by (rule Cons.hyps)
   332     with False a_notin_al show ?thesis by (simp add: dom_update)
   333   qed
   334 qed
   335 
   336 lemma update_filter: 
   337   "a\<noteq>k \<Longrightarrow> update k v [q\<leftarrow>ps . fst q \<noteq> a] = [q\<leftarrow>update k v ps . fst q \<noteq> a]"
   338   by (induct ps) auto
   339 
   340 lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
   341   by (induct al rule: clearjunk.induct) (auto simp add: update_filter delete_def)
   342 
   343 lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
   344   by (induct al) auto
   345 
   346 lemma update_nonempty [simp]: "update k v al \<noteq> []"
   347   by (induct al) auto
   348 
   349 lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v=v'"
   350 proof (induct al arbitrary: al') 
   351   case Nil thus ?case 
   352     by (cases al') (auto split: split_if_asm)
   353 next
   354   case Cons thus ?case
   355     by (cases al') (auto split: split_if_asm)
   356 qed
   357 
   358 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
   359   by (induct al) auto
   360 
   361 text {* Note that the lists are not necessarily the same:
   362         @{term "update k v (update k' v' []) = [(k',v'),(k,v)]"} and 
   363         @{term "update k' v' (update k v []) = [(k,v),(k',v')]"}.*}
   364 lemma update_swap: "k\<noteq>k' 
   365   \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
   366   by (auto simp add: update_conv' intro: ext)
   367 
   368 lemma update_Some_unfold: 
   369   "(map_of (update k v al) x = Some y) = 
   370      (x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y)"
   371   by (simp add: update_conv' map_upd_Some_unfold)
   372 
   373 lemma image_update[simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
   374   by (simp add: update_conv' image_map_upd)
   375 
   376 
   377 (* ******************************************************************************** *)
   378 subsection {* @{const updates} *}
   379 (* ******************************************************************************** *)
   380 
   381 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   382 proof (induct ks arbitrary: vs al)
   383   case Nil
   384   thus ?case by simp
   385 next
   386   case (Cons k ks)
   387   show ?case
   388   proof (cases vs)
   389     case Nil
   390     with Cons show ?thesis by simp
   391   next
   392     case (Cons k ks')
   393     with Cons.hyps show ?thesis
   394       by (simp add: update_conv fun_upd_def)
   395   qed
   396 qed
   397 
   398 lemma updates_conv': "map_of (updates ks vs al) = ((map_of al)(ks[\<mapsto>]vs))"
   399   by (rule ext) (rule updates_conv)
   400 
   401 lemma distinct_updates:
   402   assumes "distinct (map fst al)"
   403   shows "distinct (map fst (updates ks vs al))"
   404   using prems
   405   by (induct ks arbitrary: vs al)
   406    (auto simp add: distinct_update split: list.splits)
   407 
   408 lemma clearjunk_updates:
   409  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   410   by (induct ks arbitrary: vs al) (auto simp add: clearjunk_update split: list.splits)
   411 
   412 lemma updates_empty[simp]: "updates vs [] al = al"
   413   by (induct vs) auto 
   414 
   415 lemma updates_Cons: "updates (k#ks) (v#vs) al = updates ks vs (update k v al)"
   416   by simp
   417 
   418 lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   419   updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   420   by (induct ks arbitrary: vs al) (auto split: list.splits)
   421 
   422 lemma updates_list_update_drop[simp]:
   423  "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
   424    \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
   425   by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
   426 
   427 lemma update_updates_conv_if: "
   428  map_of (updates xs ys (update x y al)) =
   429  map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
   430                                   else (update x y (updates xs ys al)))"
   431   by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
   432 
   433 lemma updates_twist [simp]:
   434  "k \<notin> set ks \<Longrightarrow> 
   435   map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
   436   by (simp add: updates_conv' update_conv' map_upds_twist)
   437 
   438 lemma updates_apply_notin[simp]:
   439  "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
   440   by (simp add: updates_conv)
   441 
   442 lemma updates_append_drop[simp]:
   443   "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
   444   by (induct xs arbitrary: ys al) (auto split: list.splits)
   445 
   446 lemma updates_append2_drop[simp]:
   447   "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   448   by (induct xs arbitrary: ys al) (auto split: list.splits)
   449 
   450 (* ******************************************************************************** *)
   451 subsection {* @{const map_ran} *}
   452 (* ******************************************************************************** *)
   453 
   454 lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
   455   by (induct al) auto
   456 
   457 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
   458   by (induct al) auto
   459 
   460 lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
   461   by (induct al) (auto simp add: dom_map_ran)
   462 
   463 lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
   464   by (induct ps) auto
   465 
   466 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   467   by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
   468 
   469 (* ******************************************************************************** *)
   470 subsection {* @{const merge} *}
   471 (* ******************************************************************************** *)
   472 
   473 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   474   by (induct ys arbitrary: xs) (auto simp add: dom_update)
   475 
   476 lemma distinct_merge:
   477   assumes "distinct (map fst xs)"
   478   shows "distinct (map fst (merge xs ys))"
   479   using prems
   480 by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
   481 
   482 lemma clearjunk_merge:
   483  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   484   by (induct ys) (auto simp add: clearjunk_update)
   485 
   486 lemma merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
   487 proof (induct ys)
   488   case Nil thus ?case by simp 
   489 next
   490   case (Cons y ys)
   491   show ?case
   492   proof (cases "k = fst y")
   493     case True
   494     from True show ?thesis
   495       by (simp add: update_conv)
   496   next
   497     case False
   498     from False show ?thesis
   499       by (auto simp add: update_conv Cons.hyps map_add_def)
   500   qed
   501 qed
   502 
   503 lemma merge_conv': "map_of (merge xs ys) = (map_of xs ++ map_of ys)"
   504   by (rule ext) (rule merge_conv)
   505 
   506 lemma merge_emty: "map_of (merge [] ys) = map_of ys"
   507   by (simp add: merge_conv')
   508 
   509 lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
   510                            map_of (merge (merge m1 m2) m3)"
   511   by (simp add: merge_conv')
   512 
   513 lemma merge_Some_iff: 
   514  "(map_of (merge m n) k = Some x) = 
   515   (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
   516   by (simp add: merge_conv' map_add_Some_iff)
   517 
   518 lemmas merge_SomeD = merge_Some_iff [THEN iffD1, standard]
   519 declare merge_SomeD [dest!]
   520 
   521 lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   522   by (simp add: merge_conv')
   523 
   524 lemma merge_None [iff]: 
   525   "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   526   by (simp add: merge_conv')
   527 
   528 lemma merge_upd[simp]: 
   529   "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   530   by (simp add: update_conv' merge_conv')
   531 
   532 lemma merge_updatess[simp]: 
   533   "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
   534   by (simp add: updates_conv' merge_conv')
   535 
   536 lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   537   by (simp add: merge_conv')
   538 
   539 (* ******************************************************************************** *)
   540 subsection {* @{const compose} *}
   541 (* ******************************************************************************** *)
   542 
   543 lemma compose_first_None [simp]: 
   544   assumes "map_of xs k = None" 
   545   shows "map_of (compose xs ys) k = None"
   546 using prems by (induct xs ys rule: compose.induct)
   547   (auto split: option.splits split_if_asm)
   548 
   549 lemma compose_conv: 
   550   shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   551 proof (induct xs ys rule: compose.induct)
   552   case 1 then show ?case by simp
   553 next
   554   case (2 x xs ys) show ?case
   555   proof (cases "map_of ys (snd x)")
   556     case None with 2
   557     have hyp: "map_of (compose (delete (fst x) xs) ys) k =
   558                (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
   559       by simp
   560     show ?thesis
   561     proof (cases "fst x = k")
   562       case True
   563       from True delete_notin_dom [of k xs]
   564       have "map_of (delete (fst x) xs) k = None"
   565 	by (simp add: map_of_eq_None_iff)
   566       with hyp show ?thesis
   567 	using True None
   568 	by simp
   569     next
   570       case False
   571       from False have "map_of (delete (fst x) xs) k = map_of xs k"
   572 	by simp
   573       with hyp show ?thesis
   574 	using False None
   575 	by (simp add: map_comp_def)
   576     qed
   577   next
   578     case (Some v)
   579     with 2
   580     have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   581       by simp
   582     with Some show ?thesis
   583       by (auto simp add: map_comp_def)
   584   qed
   585 qed
   586    
   587 lemma compose_conv': 
   588   shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   589   by (rule ext) (rule compose_conv)
   590 
   591 lemma compose_first_Some [simp]:
   592   assumes "map_of xs k = Some v" 
   593   shows "map_of (compose xs ys) k = map_of ys v"
   594 using prems by (simp add: compose_conv)
   595 
   596 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   597 proof (induct xs ys rule: compose.induct)
   598   case 1 thus ?case by simp
   599 next
   600   case (2 x xs ys)
   601   show ?case
   602   proof (cases "map_of ys (snd x)")
   603     case None
   604     with "2.hyps"
   605     have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   606       by simp
   607     also
   608     have "\<dots> \<subseteq> fst ` set xs"
   609       by (rule dom_delete_subset)
   610     finally show ?thesis
   611       using None
   612       by auto
   613   next
   614     case (Some v)
   615     with "2.hyps"
   616     have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   617       by simp
   618     with Some show ?thesis
   619       by auto
   620   qed
   621 qed
   622 
   623 lemma distinct_compose:
   624  assumes "distinct (map fst xs)"
   625  shows "distinct (map fst (compose xs ys))"
   626 using prems
   627 proof (induct xs ys rule: compose.induct)
   628   case 1 thus ?case by simp
   629 next
   630   case (2 x xs ys)
   631   show ?case
   632   proof (cases "map_of ys (snd x)")
   633     case None
   634     with 2 show ?thesis by simp
   635   next
   636     case (Some v)
   637     with 2 dom_compose [of xs ys] show ?thesis 
   638       by (auto)
   639   qed
   640 qed
   641 
   642 lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
   643 proof (induct xs ys rule: compose.induct)
   644   case 1 thus ?case by simp
   645 next
   646   case (2 x xs ys)
   647   show ?case
   648   proof (cases "map_of ys (snd x)")
   649     case None
   650     with 2 have 
   651       hyp: "compose (delete k (delete (fst x) xs)) ys =
   652             delete k (compose (delete (fst x) xs) ys)"
   653       by simp
   654     show ?thesis
   655     proof (cases "fst x = k")
   656       case True
   657       with None hyp
   658       show ?thesis
   659 	by (simp add: delete_idem)
   660     next
   661       case False
   662       from None False hyp
   663       show ?thesis
   664 	by (simp add: delete_twist)
   665     qed
   666   next
   667     case (Some v)
   668     with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
   669     with Some show ?thesis
   670       by simp
   671   qed
   672 qed
   673 
   674 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
   675   by (induct xs ys rule: compose.induct) 
   676      (auto simp add: map_of_clearjunk split: option.splits)
   677    
   678 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
   679   by (induct xs rule: clearjunk.induct)
   680      (auto split: option.splits simp add: clearjunk_delete delete_idem
   681                compose_delete_twist)
   682    
   683 lemma compose_empty [simp]:
   684  "compose xs [] = []"
   685   by (induct xs) (auto simp add: compose_delete_twist)
   686 
   687 lemma compose_Some_iff:
   688   "(map_of (compose xs ys) k = Some v) = 
   689      (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
   690   by (simp add: compose_conv map_comp_Some_iff)
   691 
   692 lemma map_comp_None_iff:
   693   "(map_of (compose xs ys) k = None) = 
   694     (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
   695   by (simp add: compose_conv map_comp_None_iff)
   696 
   697 
   698 (* ******************************************************************************** *)
   699 subsection {* @{const restrict} *}
   700 (* ******************************************************************************** *)
   701 
   702 lemma restrict_def:
   703   "restrict A = filter (\<lambda>p. fst p \<in> A)"
   704 proof
   705   fix xs
   706   show "restrict A xs = filter (\<lambda>p. fst p \<in> A) xs"
   707   by (induct xs) auto
   708 qed
   709 
   710 lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   711   by (induct al) (auto simp add: restrict_def)
   712 
   713 lemma restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   714   apply (induct al)
   715   apply  (simp add: restrict_def)
   716   apply (cases "k\<in>A")
   717   apply (auto simp add: restrict_def)
   718   done
   719 
   720 lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   721   by (rule ext) (rule restr_conv)
   722 
   723 lemma restr_empty [simp]: 
   724   "restrict {} al = []" 
   725   "restrict A [] = []"
   726   by (induct al) (auto simp add: restrict_def)
   727 
   728 lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
   729   by (simp add: restr_conv')
   730 
   731 lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
   732   by (simp add: restr_conv')
   733 
   734 lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   735   by (induct al) (auto simp add: restrict_def)
   736 
   737 lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   738   by (induct al) (auto simp add: restrict_def)
   739 
   740 lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   741   by (induct al) (auto simp add: restrict_def)
   742 
   743 lemma restr_update[simp]:
   744  "map_of (restrict D (update x y al)) = 
   745   map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   746   by (simp add: restr_conv' update_conv')
   747 
   748 lemma restr_delete [simp]:
   749   "(delete x (restrict D al)) = 
   750     (if x\<in> D then restrict (D - {x}) al else restrict D al)"
   751 proof (induct al)
   752   case Nil thus ?case by simp
   753 next
   754   case (Cons a al)
   755   show ?case
   756   proof (cases "x \<in> D")
   757     case True
   758     note x_D = this
   759     with Cons have hyp: "delete x (restrict D al) = restrict (D - {x}) al"
   760       by simp
   761     show ?thesis
   762     proof (cases "fst a = x")
   763       case True
   764       from Cons.hyps
   765       show ?thesis
   766 	using x_D True
   767 	by simp
   768     next
   769       case False
   770       note not_fst_a_x = this
   771       show ?thesis
   772       proof (cases "fst a \<in> D")
   773 	case True 
   774 	with not_fst_a_x 
   775 	have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))"
   776 	  by (cases a) (simp add: restrict_def)
   777 	also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)"
   778 	  by (cases a) (simp add: restrict_def)
   779 	finally show ?thesis
   780 	  using x_D by simp
   781       next
   782 	case False
   783 	hence "delete x (restrict D (a#al)) = delete x (restrict D al)"
   784 	  by (cases a) (simp add: restrict_def)
   785 	moreover from False not_fst_a_x
   786 	have "restrict (D - {x}) (a # al) = restrict (D - {x}) al"
   787 	  by (cases a) (simp add: restrict_def)
   788 	ultimately
   789 	show ?thesis using x_D hyp by simp
   790       qed
   791     qed
   792   next
   793     case False
   794     from False Cons show ?thesis
   795       by simp
   796   qed
   797 qed
   798 
   799 lemma update_restr:
   800  "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   801   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
   802 
   803 lemma upate_restr_conv [simp]:
   804  "x \<in> D \<Longrightarrow> 
   805  map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   806   by (simp add: update_conv' restr_conv')
   807 
   808 lemma restr_updates [simp]: "
   809  \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   810  \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
   811      map_of (updates xs ys (restrict (D - set xs) al))"
   812   by (simp add: updates_conv' restr_conv')
   813 
   814 lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   815   by (induct ps) auto
   816 
   817 lemma clearjunk_restrict:
   818  "clearjunk (restrict A al) = restrict A (clearjunk al)"
   819   by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
   820 
   821 end