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