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