src/HOL/Library/AList.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 63476 ff1d86b07751
child 68249 949d93804740
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
bulwahn@46238
     1
(*  Title:      HOL/Library/AList.thy
haftmann@34975
     2
    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
schirmer@19234
     3
*)
schirmer@19234
     4
wenzelm@60500
     5
section \<open>Implementation of Association Lists\<close>
schirmer@19234
     6
bulwahn@46238
     7
theory AList
wenzelm@63462
     8
  imports Main
schirmer@19234
     9
begin
schirmer@19234
    10
wenzelm@59943
    11
context
wenzelm@59943
    12
begin
wenzelm@59943
    13
wenzelm@60500
    14
text \<open>
wenzelm@56327
    15
  The operations preserve distinctness of keys and
wenzelm@56327
    16
  function @{term "clearjunk"} distributes over them. Since
haftmann@22740
    17
  @{term clearjunk} enforces distinctness of keys it can be used
haftmann@22740
    18
  to establish the invariant, e.g. for inductive proofs.
wenzelm@60500
    19
\<close>
schirmer@19234
    20
wenzelm@61585
    21
subsection \<open>\<open>update\<close> and \<open>updates\<close>\<close>
nipkow@19323
    22
wenzelm@59990
    23
qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
    24
  where
wenzelm@63462
    25
    "update k v [] = [(k, v)]"
wenzelm@63462
    26
  | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
schirmer@19234
    27
haftmann@34975
    28
lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
nipkow@39302
    29
  by (induct al) (auto simp add: fun_eq_iff)
wenzelm@23373
    30
haftmann@34975
    31
corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
haftmann@34975
    32
  by (simp add: update_conv')
schirmer@19234
    33
schirmer@19234
    34
lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
schirmer@19234
    35
  by (induct al) auto
schirmer@19234
    36
haftmann@34975
    37
lemma update_keys:
haftmann@34975
    38
  "map fst (update k v al) =
haftmann@34975
    39
    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
haftmann@34975
    40
  by (induct al) simp_all
haftmann@34975
    41
schirmer@19234
    42
lemma distinct_update:
wenzelm@56327
    43
  assumes "distinct (map fst al)"
schirmer@19234
    44
  shows "distinct (map fst (update k v al))"
haftmann@34975
    45
  using assms by (simp add: update_keys)
schirmer@19234
    46
wenzelm@56327
    47
lemma update_filter:
wenzelm@56327
    48
  "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
schirmer@19234
    49
  by (induct ps) auto
schirmer@19234
    50
schirmer@19234
    51
lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
schirmer@19234
    52
  by (induct al) auto
schirmer@19234
    53
schirmer@19234
    54
lemma update_nonempty [simp]: "update k v al \<noteq> []"
schirmer@19234
    55
  by (induct al) auto
schirmer@19234
    56
haftmann@34975
    57
lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
wenzelm@56327
    58
proof (induct al arbitrary: al')
wenzelm@56327
    59
  case Nil
wenzelm@56327
    60
  then show ?case
nipkow@62390
    61
    by (cases al') (auto split: if_split_asm)
schirmer@19234
    62
next
wenzelm@56327
    63
  case Cons
wenzelm@56327
    64
  then show ?case
nipkow@62390
    65
    by (cases al') (auto split: if_split_asm)
schirmer@19234
    66
qed
schirmer@19234
    67
schirmer@19234
    68
lemma update_last [simp]: "update k v (update k v' al) = update k v al"
schirmer@19234
    69
  by (induct al) auto
schirmer@19234
    70
wenzelm@60500
    71
text \<open>Note that the lists are not necessarily the same:
wenzelm@56327
    72
        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and
wenzelm@60500
    73
        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.\<close>
wenzelm@56327
    74
wenzelm@56327
    75
lemma update_swap:
wenzelm@63476
    76
  "k \<noteq> k' \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
nipkow@39302
    77
  by (simp add: update_conv' fun_eq_iff)
schirmer@19234
    78
wenzelm@56327
    79
lemma update_Some_unfold:
haftmann@34975
    80
  "map_of (update k v al) x = Some y \<longleftrightarrow>
haftmann@34975
    81
    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
schirmer@19234
    82
  by (simp add: update_conv' map_upd_Some_unfold)
schirmer@19234
    83
wenzelm@63462
    84
lemma image_update [simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
haftmann@46133
    85
  by (simp add: update_conv')
schirmer@19234
    86
wenzelm@63476
    87
qualified definition updates ::
wenzelm@63476
    88
    "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@56327
    89
  where "updates ks vs = fold (case_prod update) (zip ks vs)"
schirmer@19234
    90
haftmann@34975
    91
lemma updates_simps [simp]:
haftmann@34975
    92
  "updates [] vs ps = ps"
haftmann@34975
    93
  "updates ks [] ps = ps"
haftmann@34975
    94
  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
haftmann@34975
    95
  by (simp_all add: updates_def)
haftmann@34975
    96
haftmann@34975
    97
lemma updates_key_simp [simp]:
haftmann@34975
    98
  "updates (k # ks) vs ps =
haftmann@34975
    99
    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
haftmann@34975
   100
  by (cases vs) simp_all
haftmann@34975
   101
haftmann@34975
   102
lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
haftmann@34975
   103
proof -
blanchet@55414
   104
  have "map_of \<circ> fold (case_prod update) (zip ks vs) =
wenzelm@56327
   105
      fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
haftmann@39921
   106
    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
wenzelm@56327
   107
  then show ?thesis
wenzelm@56327
   108
    by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
haftmann@34975
   109
qed
schirmer@19234
   110
schirmer@19234
   111
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
haftmann@34975
   112
  by (simp add: updates_conv')
schirmer@19234
   113
schirmer@19234
   114
lemma distinct_updates:
schirmer@19234
   115
  assumes "distinct (map fst al)"
schirmer@19234
   116
  shows "distinct (map fst (updates ks vs al))"
haftmann@34975
   117
proof -
haftmann@46133
   118
  have "distinct (fold
haftmann@37458
   119
       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
haftmann@37458
   120
       (zip ks vs) (map fst al))"
haftmann@37458
   121
    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
blanchet@55414
   122
  moreover have "map fst \<circ> fold (case_prod update) (zip ks vs) =
wenzelm@56327
   123
      fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
blanchet@55414
   124
    by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def)
wenzelm@56327
   125
  ultimately show ?thesis
wenzelm@56327
   126
    by (simp add: updates_def fun_eq_iff)
haftmann@34975
   127
qed
schirmer@19234
   128
schirmer@19234
   129
lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
wenzelm@56327
   130
    updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
wenzelm@20503
   131
  by (induct ks arbitrary: vs al) (auto split: list.splits)
schirmer@19234
   132
schirmer@19234
   133
lemma updates_list_update_drop[simp]:
wenzelm@56327
   134
  "size ks \<le> i \<Longrightarrow> i < size vs \<Longrightarrow>
wenzelm@56327
   135
    updates ks (vs[i:=v]) al = updates ks vs al"
wenzelm@56327
   136
  by (induct ks arbitrary: al vs i) (auto split: list.splits nat.splits)
schirmer@19234
   137
wenzelm@56327
   138
lemma update_updates_conv_if:
wenzelm@56327
   139
  "map_of (updates xs ys (update x y al)) =
wenzelm@56327
   140
    map_of
wenzelm@56327
   141
     (if x \<in> set (take (length ys) xs)
wenzelm@56327
   142
      then updates xs ys al
wenzelm@56327
   143
      else (update x y (updates xs ys al)))"
schirmer@19234
   144
  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
schirmer@19234
   145
schirmer@19234
   146
lemma updates_twist [simp]:
wenzelm@56327
   147
  "k \<notin> set ks \<Longrightarrow>
wenzelm@56327
   148
    map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
wenzelm@46507
   149
  by (simp add: updates_conv' update_conv')
schirmer@19234
   150
wenzelm@56327
   151
lemma updates_apply_notin [simp]:
wenzelm@56327
   152
  "k \<notin> set ks \<Longrightarrow> map_of (updates ks vs al) k = map_of al k"
schirmer@19234
   153
  by (simp add: updates_conv)
schirmer@19234
   154
wenzelm@56327
   155
lemma updates_append_drop [simp]:
wenzelm@56327
   156
  "size xs = size ys \<Longrightarrow> updates (xs @ zs) ys al = updates xs ys al"
wenzelm@20503
   157
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   158
wenzelm@56327
   159
lemma updates_append2_drop [simp]:
wenzelm@56327
   160
  "size xs = size ys \<Longrightarrow> updates xs (ys @ zs) al = updates xs ys al"
wenzelm@20503
   161
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   162
wenzelm@23373
   163
wenzelm@61585
   164
subsection \<open>\<open>delete\<close>\<close>
haftmann@34975
   165
wenzelm@59990
   166
qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@56327
   167
  where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
haftmann@34975
   168
haftmann@34975
   169
lemma delete_simps [simp]:
haftmann@34975
   170
  "delete k [] = []"
wenzelm@56327
   171
  "delete k (p # ps) = (if fst p = k then delete k ps else p # delete k ps)"
haftmann@34975
   172
  by (auto simp add: delete_eq)
haftmann@34975
   173
haftmann@34975
   174
lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
nipkow@39302
   175
  by (induct al) (auto simp add: fun_eq_iff)
haftmann@34975
   176
haftmann@34975
   177
corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
haftmann@34975
   178
  by (simp add: delete_conv')
haftmann@34975
   179
wenzelm@56327
   180
lemma delete_keys: "map fst (delete k al) = removeAll k (map fst al)"
haftmann@34975
   181
  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
haftmann@34975
   182
haftmann@34975
   183
lemma distinct_delete:
wenzelm@56327
   184
  assumes "distinct (map fst al)"
haftmann@34975
   185
  shows "distinct (map fst (delete k al))"
haftmann@34975
   186
  using assms by (simp add: delete_keys distinct_removeAll)
haftmann@34975
   187
haftmann@34975
   188
lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
haftmann@34975
   189
  by (auto simp add: image_iff delete_eq filter_id_conv)
haftmann@34975
   190
haftmann@34975
   191
lemma delete_idem: "delete k (delete k al) = delete k al"
haftmann@34975
   192
  by (simp add: delete_eq)
haftmann@34975
   193
wenzelm@56327
   194
lemma map_of_delete [simp]: "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
haftmann@34975
   195
  by (simp add: delete_conv')
haftmann@34975
   196
haftmann@34975
   197
lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
haftmann@34975
   198
  by (auto simp add: delete_eq)
haftmann@34975
   199
haftmann@34975
   200
lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
haftmann@34975
   201
  by (auto simp add: delete_eq)
haftmann@34975
   202
wenzelm@56327
   203
lemma delete_update_same: "delete k (update k v al) = delete k al"
haftmann@34975
   204
  by (induct al) simp_all
haftmann@34975
   205
wenzelm@56327
   206
lemma delete_update: "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
haftmann@34975
   207
  by (induct al) simp_all
haftmann@34975
   208
haftmann@34975
   209
lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
haftmann@34975
   210
  by (simp add: delete_eq conj_commute)
haftmann@34975
   211
haftmann@34975
   212
lemma length_delete_le: "length (delete k al) \<le> length al"
haftmann@34975
   213
  by (simp add: delete_eq)
haftmann@34975
   214
haftmann@34975
   215
wenzelm@61585
   216
subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
nipkow@60043
   217
wenzelm@63476
   218
qualified primrec update_with_aux ::
wenzelm@63476
   219
    "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
   220
  where
wenzelm@63462
   221
    "update_with_aux v k f [] = [(k, f v)]"
wenzelm@63462
   222
  | "update_with_aux v k f (p # ps) =
wenzelm@63462
   223
      (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
nipkow@60043
   224
wenzelm@60500
   225
text \<open>
nipkow@60043
   226
  The above @{term "delete"} traverses all the list even if it has found the key.
nipkow@60043
   227
  This one does not have to keep going because is assumes the invariant that keys are distinct.
wenzelm@60500
   228
\<close>
nipkow@60043
   229
qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
   230
  where
wenzelm@63462
   231
    "delete_aux k [] = []"
wenzelm@63462
   232
  | "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
nipkow@60043
   233
nipkow@60043
   234
lemma map_of_update_with_aux':
wenzelm@63462
   235
  "map_of (update_with_aux v k f ps) k' =
wenzelm@63462
   236
    ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
wenzelm@63462
   237
  by (induct ps) auto
nipkow@60043
   238
nipkow@60043
   239
lemma map_of_update_with_aux:
wenzelm@63462
   240
  "map_of (update_with_aux v k f ps) =
wenzelm@63462
   241
    (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
wenzelm@63462
   242
  by (simp add: fun_eq_iff map_of_update_with_aux')
nipkow@60043
   243
nipkow@60043
   244
lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
nipkow@60043
   245
  by (induct ps) auto
nipkow@60043
   246
nipkow@60043
   247
lemma distinct_update_with_aux [simp]:
nipkow@60043
   248
  "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
wenzelm@63462
   249
  by (induct ps) (auto simp add: dom_update_with_aux)
nipkow@60043
   250
nipkow@60043
   251
lemma set_update_with_aux:
wenzelm@63462
   252
  "distinct (map fst xs) \<Longrightarrow>
wenzelm@63462
   253
    set (update_with_aux v k f xs) =
wenzelm@63462
   254
      (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
wenzelm@63462
   255
  by (induct xs) (auto intro: rev_image_eqI)
nipkow@60043
   256
nipkow@60043
   257
lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
wenzelm@63462
   258
  apply (induct xs)
wenzelm@63476
   259
   apply simp_all
wenzelm@63462
   260
  apply clarsimp
wenzelm@63462
   261
  apply (fastforce intro: rev_image_eqI)
wenzelm@63462
   262
  done
nipkow@60043
   263
nipkow@60043
   264
lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
wenzelm@63462
   265
  by (auto simp add: set_delete_aux)
nipkow@60043
   266
wenzelm@63462
   267
lemma distinct_delete_aux [simp]: "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
wenzelm@63462
   268
proof (induct ps)
wenzelm@63462
   269
  case Nil
wenzelm@63462
   270
  then show ?case by simp
nipkow@60043
   271
next
nipkow@60043
   272
  case (Cons a ps)
wenzelm@63462
   273
  obtain k' v where a: "a = (k', v)"
wenzelm@63462
   274
    by (cases a)
nipkow@60043
   275
  show ?case
wenzelm@63462
   276
  proof (cases "k' = k")
wenzelm@63462
   277
    case True
wenzelm@63462
   278
    with Cons a show ?thesis by simp
nipkow@60043
   279
  next
nipkow@60043
   280
    case False
wenzelm@63462
   281
    with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)"
wenzelm@63462
   282
      by simp_all
nipkow@60043
   283
    with False a have "k' \<notin> fst ` set (delete_aux k ps)"
wenzelm@63462
   284
      by (auto dest!: dom_delete_aux[where k=k])
wenzelm@63462
   285
    with Cons a show ?thesis
wenzelm@63462
   286
      by simp
nipkow@60043
   287
  qed
nipkow@60043
   288
qed
nipkow@60043
   289
nipkow@60043
   290
lemma map_of_delete_aux':
nipkow@60043
   291
  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
nipkow@60043
   292
  apply (induct xs)
wenzelm@63476
   293
   apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
nipkow@60043
   294
  apply (auto intro!: ext)
nipkow@60043
   295
  apply (simp add: map_of_eq_None_iff)
nipkow@60043
   296
  done
nipkow@60043
   297
nipkow@60043
   298
lemma map_of_delete_aux:
nipkow@60043
   299
  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
wenzelm@63462
   300
  by (simp add: map_of_delete_aux')
nipkow@60043
   301
nipkow@60043
   302
lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
wenzelm@63462
   303
  by (cases ts) (auto split: if_split_asm)
nipkow@60043
   304
nipkow@60043
   305
wenzelm@61585
   306
subsection \<open>\<open>restrict\<close>\<close>
haftmann@34975
   307
wenzelm@59990
   308
qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@56327
   309
  where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
haftmann@34975
   310
haftmann@34975
   311
lemma restr_simps [simp]:
haftmann@34975
   312
  "restrict A [] = []"
haftmann@34975
   313
  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
haftmann@34975
   314
  by (auto simp add: restrict_eq)
haftmann@34975
   315
haftmann@34975
   316
lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
haftmann@34975
   317
proof
wenzelm@63462
   318
  show "map_of (restrict A al) k = ((map_of al)|` A) k" for k
wenzelm@63462
   319
    apply (induct al)
wenzelm@63476
   320
     apply simp
wenzelm@63462
   321
    apply (cases "k \<in> A")
wenzelm@63476
   322
     apply auto
wenzelm@63462
   323
    done
haftmann@34975
   324
qed
haftmann@34975
   325
haftmann@34975
   326
corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
haftmann@34975
   327
  by (simp add: restr_conv')
haftmann@34975
   328
wenzelm@63462
   329
lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
haftmann@34975
   330
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   331
wenzelm@56327
   332
lemma restr_empty [simp]:
wenzelm@56327
   333
  "restrict {} al = []"
haftmann@34975
   334
  "restrict A [] = []"
haftmann@34975
   335
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   336
haftmann@34975
   337
lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
haftmann@34975
   338
  by (simp add: restr_conv')
haftmann@34975
   339
haftmann@34975
   340
lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
haftmann@34975
   341
  by (simp add: restr_conv')
haftmann@34975
   342
haftmann@34975
   343
lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
haftmann@34975
   344
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   345
haftmann@34975
   346
lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
haftmann@34975
   347
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   348
haftmann@34975
   349
lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
haftmann@34975
   350
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   351
haftmann@34975
   352
lemma restr_update[simp]:
wenzelm@63462
   353
  "map_of (restrict D (update x y al)) =
wenzelm@63462
   354
    map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
haftmann@34975
   355
  by (simp add: restr_conv' update_conv')
haftmann@34975
   356
haftmann@34975
   357
lemma restr_delete [simp]:
wenzelm@56327
   358
  "delete x (restrict D al) = (if x \<in> D then restrict (D - {x}) al else restrict D al)"
wenzelm@56327
   359
  apply (simp add: delete_eq restrict_eq)
wenzelm@56327
   360
  apply (auto simp add: split_def)
haftmann@34975
   361
proof -
wenzelm@63462
   362
  have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
wenzelm@56327
   363
    by auto
haftmann@34975
   364
  then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
haftmann@34975
   365
    by simp
haftmann@34975
   366
  assume "x \<notin> D"
wenzelm@63462
   367
  then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
wenzelm@56327
   368
    by auto
haftmann@34975
   369
  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
haftmann@34975
   370
    by simp
haftmann@34975
   371
qed
haftmann@34975
   372
haftmann@34975
   373
lemma update_restr:
wenzelm@56327
   374
  "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
haftmann@34975
   375
  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
schirmer@19234
   376
bulwahn@45867
   377
lemma update_restr_conv [simp]:
wenzelm@56327
   378
  "x \<in> D \<Longrightarrow>
wenzelm@56327
   379
    map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))"
haftmann@34975
   380
  by (simp add: update_conv' restr_conv')
haftmann@34975
   381
wenzelm@56327
   382
lemma restr_updates [simp]:
wenzelm@56327
   383
  "length xs = length ys \<Longrightarrow> set xs \<subseteq> D \<Longrightarrow>
wenzelm@56327
   384
    map_of (restrict D (updates xs ys al)) =
wenzelm@56327
   385
      map_of (updates xs ys (restrict (D - set xs) al))"
haftmann@34975
   386
  by (simp add: updates_conv' restr_conv')
haftmann@34975
   387
haftmann@34975
   388
lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
haftmann@34975
   389
  by (induct ps) auto
haftmann@34975
   390
haftmann@34975
   391
wenzelm@61585
   392
subsection \<open>\<open>clearjunk\<close>\<close>
haftmann@34975
   393
wenzelm@59990
   394
qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
   395
  where
wenzelm@63462
   396
    "clearjunk [] = []"
wenzelm@63462
   397
  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
haftmann@34975
   398
  by pat_completeness auto
wenzelm@56327
   399
termination
wenzelm@56327
   400
  by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le)
haftmann@34975
   401
wenzelm@56327
   402
lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al"
wenzelm@56327
   403
  by (induct al rule: clearjunk.induct) (simp_all add: fun_eq_iff)
haftmann@34975
   404
wenzelm@56327
   405
lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)"
wenzelm@56327
   406
  by (induct al rule: clearjunk.induct) (simp_all add: delete_keys)
haftmann@34975
   407
wenzelm@56327
   408
lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
haftmann@34975
   409
  using clearjunk_keys_set by simp
haftmann@34975
   410
wenzelm@56327
   411
lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
wenzelm@56327
   412
  by (induct al rule: clearjunk.induct) (simp_all del: set_map add: clearjunk_keys_set delete_keys)
haftmann@34975
   413
wenzelm@56327
   414
lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)"
haftmann@34975
   415
  by (simp add: map_of_clearjunk)
haftmann@34975
   416
wenzelm@56327
   417
lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)"
haftmann@34975
   418
proof -
haftmann@34975
   419
  have "ran (map_of al) = ran (map_of (clearjunk al))"
haftmann@34975
   420
    by (simp add: ran_clearjunk)
haftmann@34975
   421
  also have "\<dots> = snd ` set (clearjunk al)"
haftmann@34975
   422
    by (simp add: ran_distinct)
haftmann@34975
   423
  finally show ?thesis .
haftmann@34975
   424
qed
haftmann@34975
   425
wenzelm@56327
   426
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
wenzelm@56327
   427
  by (induct al rule: clearjunk.induct) (simp_all add: delete_update)
schirmer@19234
   428
wenzelm@56327
   429
lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
haftmann@34975
   430
proof -
blanchet@55414
   431
  have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
wenzelm@63462
   432
      fold (case_prod update) (zip ks vs) \<circ> clearjunk"
blanchet@55414
   433
    by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
wenzelm@56327
   434
  then show ?thesis
wenzelm@56327
   435
    by (simp add: updates_def fun_eq_iff)
haftmann@34975
   436
qed
haftmann@34975
   437
wenzelm@56327
   438
lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
haftmann@34975
   439
  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
haftmann@34975
   440
wenzelm@56327
   441
lemma clearjunk_restrict: "clearjunk (restrict A al) = restrict A (clearjunk al)"
haftmann@34975
   442
  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
haftmann@34975
   443
wenzelm@56327
   444
lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
haftmann@34975
   445
  by (induct al rule: clearjunk.induct) auto
haftmann@34975
   446
wenzelm@56327
   447
lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
haftmann@34975
   448
  by simp
haftmann@34975
   449
wenzelm@56327
   450
lemma length_clearjunk: "length (clearjunk al) \<le> length al"
haftmann@34975
   451
proof (induct al rule: clearjunk.induct [case_names Nil Cons])
wenzelm@56327
   452
  case Nil
wenzelm@56327
   453
  then show ?case by simp
haftmann@34975
   454
next
haftmann@34975
   455
  case (Cons kv al)
wenzelm@56327
   456
  moreover have "length (delete (fst kv) al) \<le> length al"
wenzelm@56327
   457
    by (fact length_delete_le)
wenzelm@56327
   458
  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al"
wenzelm@56327
   459
    by (rule order_trans)
wenzelm@56327
   460
  then show ?case
wenzelm@56327
   461
    by simp
haftmann@34975
   462
qed
haftmann@34975
   463
haftmann@34975
   464
lemma delete_map:
haftmann@34975
   465
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   466
  shows "delete k (map f ps) = map f (delete k ps)"
haftmann@34975
   467
  by (simp add: delete_eq filter_map comp_def split_def assms)
haftmann@34975
   468
haftmann@34975
   469
lemma clearjunk_map:
haftmann@34975
   470
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   471
  shows "clearjunk (map f ps) = map f (clearjunk ps)"
haftmann@34975
   472
  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
haftmann@34975
   473
    (simp_all add: clearjunk_delete delete_map assms)
haftmann@34975
   474
haftmann@34975
   475
wenzelm@61585
   476
subsection \<open>\<open>map_ran\<close>\<close>
haftmann@34975
   477
wenzelm@56327
   478
definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@56327
   479
  where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
haftmann@34975
   480
haftmann@34975
   481
lemma map_ran_simps [simp]:
haftmann@34975
   482
  "map_ran f [] = []"
haftmann@34975
   483
  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
haftmann@34975
   484
  by (simp_all add: map_ran_def)
haftmann@34975
   485
wenzelm@56327
   486
lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
haftmann@34975
   487
  by (simp add: map_ran_def image_image split_def)
wenzelm@56327
   488
wenzelm@56327
   489
lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
schirmer@19234
   490
  by (induct al) auto
schirmer@19234
   491
wenzelm@56327
   492
lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
haftmann@34975
   493
  by (simp add: map_ran_def split_def comp_def)
schirmer@19234
   494
wenzelm@56327
   495
lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
haftmann@34975
   496
  by (simp add: map_ran_def filter_map split_def comp_def)
schirmer@19234
   497
wenzelm@56327
   498
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
haftmann@34975
   499
  by (simp add: map_ran_def split_def clearjunk_map)
schirmer@19234
   500
wenzelm@23373
   501
wenzelm@61585
   502
subsection \<open>\<open>merge\<close>\<close>
haftmann@34975
   503
wenzelm@59990
   504
qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@56327
   505
  where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
haftmann@34975
   506
haftmann@34975
   507
lemma merge_simps [simp]:
haftmann@34975
   508
  "merge qs [] = qs"
haftmann@34975
   509
  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
haftmann@34975
   510
  by (simp_all add: merge_def split_def)
haftmann@34975
   511
wenzelm@56327
   512
lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
haftmann@47397
   513
  by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd)
schirmer@19234
   514
schirmer@19234
   515
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
wenzelm@20503
   516
  by (induct ys arbitrary: xs) (auto simp add: dom_update)
schirmer@19234
   517
wenzelm@63462
   518
lemma distinct_merge: "distinct (map fst xs) \<Longrightarrow> distinct (map fst (merge xs ys))"
wenzelm@63462
   519
  by (simp add: merge_updates distinct_updates)
schirmer@19234
   520
wenzelm@56327
   521
lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
haftmann@34975
   522
  by (simp add: merge_updates clearjunk_updates)
schirmer@19234
   523
wenzelm@56327
   524
lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys"
haftmann@34975
   525
proof -
blanchet@55414
   526
  have "map_of \<circ> fold (case_prod update) (rev ys) =
wenzelm@56327
   527
      fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
blanchet@55414
   528
    by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff)
haftmann@34975
   529
  then show ?thesis
haftmann@47397
   530
    by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
schirmer@19234
   531
qed
schirmer@19234
   532
wenzelm@56327
   533
corollary merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
haftmann@34975
   534
  by (simp add: merge_conv')
schirmer@19234
   535
haftmann@34975
   536
lemma merge_empty: "map_of (merge [] ys) = map_of ys"
schirmer@19234
   537
  by (simp add: merge_conv')
schirmer@19234
   538
wenzelm@56327
   539
lemma merge_assoc [simp]: "map_of (merge m1 (merge m2 m3)) = map_of (merge (merge m1 m2) m3)"
schirmer@19234
   540
  by (simp add: merge_conv')
schirmer@19234
   541
wenzelm@56327
   542
lemma merge_Some_iff:
wenzelm@56327
   543
  "map_of (merge m n) k = Some x \<longleftrightarrow>
wenzelm@56327
   544
    map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x"
schirmer@19234
   545
  by (simp add: merge_conv' map_add_Some_iff)
schirmer@19234
   546
wenzelm@45605
   547
lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
schirmer@19234
   548
wenzelm@56327
   549
lemma merge_find_right [simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
schirmer@19234
   550
  by (simp add: merge_conv')
schirmer@19234
   551
wenzelm@63462
   552
lemma merge_None [iff]: "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
schirmer@19234
   553
  by (simp add: merge_conv')
schirmer@19234
   554
wenzelm@63462
   555
lemma merge_upd [simp]: "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
schirmer@19234
   556
  by (simp add: update_conv' merge_conv')
schirmer@19234
   557
wenzelm@56327
   558
lemma merge_updatess [simp]:
schirmer@19234
   559
  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
schirmer@19234
   560
  by (simp add: updates_conv' merge_conv')
schirmer@19234
   561
wenzelm@56327
   562
lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)"
schirmer@19234
   563
  by (simp add: merge_conv')
schirmer@19234
   564
wenzelm@23373
   565
wenzelm@61585
   566
subsection \<open>\<open>compose\<close>\<close>
haftmann@34975
   567
wenzelm@59990
   568
qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
wenzelm@63462
   569
  where
wenzelm@63462
   570
    "compose [] ys = []"
wenzelm@63462
   571
  | "compose (x # xs) ys =
wenzelm@63462
   572
      (case map_of ys (snd x) of
wenzelm@63462
   573
        None \<Rightarrow> compose (delete (fst x) xs) ys
wenzelm@63462
   574
      | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
haftmann@34975
   575
  by pat_completeness auto
wenzelm@56327
   576
termination
wenzelm@56327
   577
  by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
schirmer@19234
   578
wenzelm@63462
   579
lemma compose_first_None [simp]: "map_of xs k = None \<Longrightarrow> map_of (compose xs ys) k = None"
wenzelm@63462
   580
  by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
schirmer@19234
   581
wenzelm@56327
   582
lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
haftmann@22916
   583
proof (induct xs ys rule: compose.induct)
wenzelm@56327
   584
  case 1
wenzelm@56327
   585
  then show ?case by simp
schirmer@19234
   586
next
wenzelm@56327
   587
  case (2 x xs ys)
wenzelm@56327
   588
  show ?case
schirmer@19234
   589
  proof (cases "map_of ys (snd x)")
wenzelm@56327
   590
    case None
wenzelm@56327
   591
    with 2 have hyp: "map_of (compose (delete (fst x) xs) ys) k =
wenzelm@56327
   592
        (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
schirmer@19234
   593
      by simp
schirmer@19234
   594
    show ?thesis
schirmer@19234
   595
    proof (cases "fst x = k")
schirmer@19234
   596
      case True
schirmer@19234
   597
      from True delete_notin_dom [of k xs]
schirmer@19234
   598
      have "map_of (delete (fst x) xs) k = None"
wenzelm@32960
   599
        by (simp add: map_of_eq_None_iff)
schirmer@19234
   600
      with hyp show ?thesis
wenzelm@32960
   601
        using True None
wenzelm@32960
   602
        by simp
schirmer@19234
   603
    next
schirmer@19234
   604
      case False
schirmer@19234
   605
      from False have "map_of (delete (fst x) xs) k = map_of xs k"
wenzelm@32960
   606
        by simp
schirmer@19234
   607
      with hyp show ?thesis
wenzelm@56327
   608
        using False None by (simp add: map_comp_def)
schirmer@19234
   609
    qed
schirmer@19234
   610
  next
schirmer@19234
   611
    case (Some v)
haftmann@22916
   612
    with 2
schirmer@19234
   613
    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
schirmer@19234
   614
      by simp
schirmer@19234
   615
    with Some show ?thesis
schirmer@19234
   616
      by (auto simp add: map_comp_def)
schirmer@19234
   617
  qed
schirmer@19234
   618
qed
wenzelm@56327
   619
wenzelm@56327
   620
lemma compose_conv': "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
schirmer@19234
   621
  by (rule ext) (rule compose_conv)
schirmer@19234
   622
wenzelm@63462
   623
lemma compose_first_Some [simp]: "map_of xs k = Some v \<Longrightarrow> map_of (compose xs ys) k = map_of ys v"
wenzelm@63462
   624
  by (simp add: compose_conv)
schirmer@19234
   625
schirmer@19234
   626
lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
haftmann@22916
   627
proof (induct xs ys rule: compose.induct)
wenzelm@56327
   628
  case 1
wenzelm@56327
   629
  then show ?case by simp
schirmer@19234
   630
next
haftmann@22916
   631
  case (2 x xs ys)
schirmer@19234
   632
  show ?case
schirmer@19234
   633
  proof (cases "map_of ys (snd x)")
schirmer@19234
   634
    case None
wenzelm@63462
   635
    with "2.hyps" have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
schirmer@19234
   636
      by simp
wenzelm@63462
   637
    also have "\<dots> \<subseteq> fst ` set xs"
schirmer@19234
   638
      by (rule dom_delete_subset)
schirmer@19234
   639
    finally show ?thesis
wenzelm@63462
   640
      using None by auto
schirmer@19234
   641
  next
schirmer@19234
   642
    case (Some v)
wenzelm@63462
   643
    with "2.hyps" have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
schirmer@19234
   644
      by simp
schirmer@19234
   645
    with Some show ?thesis
schirmer@19234
   646
      by auto
schirmer@19234
   647
  qed
schirmer@19234
   648
qed
schirmer@19234
   649
schirmer@19234
   650
lemma distinct_compose:
wenzelm@56327
   651
  assumes "distinct (map fst xs)"
wenzelm@56327
   652
  shows "distinct (map fst (compose xs ys))"
wenzelm@56327
   653
  using assms
haftmann@22916
   654
proof (induct xs ys rule: compose.induct)
wenzelm@56327
   655
  case 1
wenzelm@56327
   656
  then show ?case by simp
schirmer@19234
   657
next
haftmann@22916
   658
  case (2 x xs ys)
schirmer@19234
   659
  show ?case
schirmer@19234
   660
  proof (cases "map_of ys (snd x)")
schirmer@19234
   661
    case None
haftmann@22916
   662
    with 2 show ?thesis by simp
schirmer@19234
   663
  next
schirmer@19234
   664
    case (Some v)
wenzelm@56327
   665
    with 2 dom_compose [of xs ys] show ?thesis
wenzelm@56327
   666
      by auto
schirmer@19234
   667
  qed
schirmer@19234
   668
qed
schirmer@19234
   669
wenzelm@56327
   670
lemma compose_delete_twist: "compose (delete k xs) ys = delete k (compose xs ys)"
haftmann@22916
   671
proof (induct xs ys rule: compose.induct)
wenzelm@56327
   672
  case 1
wenzelm@56327
   673
  then show ?case by simp
schirmer@19234
   674
next
haftmann@22916
   675
  case (2 x xs ys)
schirmer@19234
   676
  show ?case
schirmer@19234
   677
  proof (cases "map_of ys (snd x)")
schirmer@19234
   678
    case None
wenzelm@56327
   679
    with 2 have hyp: "compose (delete k (delete (fst x) xs)) ys =
wenzelm@56327
   680
        delete k (compose (delete (fst x) xs) ys)"
schirmer@19234
   681
      by simp
schirmer@19234
   682
    show ?thesis
schirmer@19234
   683
    proof (cases "fst x = k")
schirmer@19234
   684
      case True
wenzelm@56327
   685
      with None hyp show ?thesis
wenzelm@32960
   686
        by (simp add: delete_idem)
schirmer@19234
   687
    next
schirmer@19234
   688
      case False
wenzelm@56327
   689
      from None False hyp show ?thesis
wenzelm@32960
   690
        by (simp add: delete_twist)
schirmer@19234
   691
    qed
schirmer@19234
   692
  next
schirmer@19234
   693
    case (Some v)
wenzelm@56327
   694
    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)"
wenzelm@56327
   695
      by simp
schirmer@19234
   696
    with Some show ?thesis
schirmer@19234
   697
      by simp
schirmer@19234
   698
  qed
schirmer@19234
   699
qed
schirmer@19234
   700
schirmer@19234
   701
lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
wenzelm@56327
   702
  by (induct xs ys rule: compose.induct)
wenzelm@56327
   703
    (auto simp add: map_of_clearjunk split: option.splits)
wenzelm@56327
   704
schirmer@19234
   705
lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
schirmer@19234
   706
  by (induct xs rule: clearjunk.induct)
wenzelm@56327
   707
    (auto split: option.splits simp add: clearjunk_delete delete_idem compose_delete_twist)
wenzelm@56327
   708
wenzelm@56327
   709
lemma compose_empty [simp]: "compose xs [] = []"
haftmann@22916
   710
  by (induct xs) (auto simp add: compose_delete_twist)
schirmer@19234
   711
schirmer@19234
   712
lemma compose_Some_iff:
wenzelm@56327
   713
  "(map_of (compose xs ys) k = Some v) \<longleftrightarrow>
wenzelm@56327
   714
    (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)"
schirmer@19234
   715
  by (simp add: compose_conv map_comp_Some_iff)
schirmer@19234
   716
schirmer@19234
   717
lemma map_comp_None_iff:
wenzelm@56327
   718
  "map_of (compose xs ys) k = None \<longleftrightarrow>
wenzelm@56327
   719
    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None))"
schirmer@19234
   720
  by (simp add: compose_conv map_comp_None_iff)
schirmer@19234
   721
wenzelm@56327
   722
wenzelm@61585
   723
subsection \<open>\<open>map_entry\<close>\<close>
bulwahn@45869
   724
wenzelm@59990
   725
qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
   726
  where
wenzelm@63462
   727
    "map_entry k f [] = []"
wenzelm@63462
   728
  | "map_entry k f (p # ps) =
wenzelm@63462
   729
      (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
bulwahn@45869
   730
bulwahn@45869
   731
lemma map_of_map_entry:
wenzelm@56327
   732
  "map_of (map_entry k f xs) =
wenzelm@56327
   733
    (map_of xs)(k := case map_of xs k of None \<Rightarrow> None | Some v' \<Rightarrow> Some (f v'))"
wenzelm@56327
   734
  by (induct xs) auto
bulwahn@45869
   735
wenzelm@56327
   736
lemma dom_map_entry: "fst ` set (map_entry k f xs) = fst ` set xs"
wenzelm@56327
   737
  by (induct xs) auto
bulwahn@45869
   738
bulwahn@45869
   739
lemma distinct_map_entry:
bulwahn@45869
   740
  assumes "distinct (map fst xs)"
bulwahn@45869
   741
  shows "distinct (map fst (map_entry k f xs))"
wenzelm@56327
   742
  using assms by (induct xs) (auto simp add: dom_map_entry)
wenzelm@56327
   743
bulwahn@45869
   744
wenzelm@61585
   745
subsection \<open>\<open>map_default\<close>\<close>
bulwahn@45868
   746
bulwahn@45868
   747
fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
wenzelm@63462
   748
  where
wenzelm@63462
   749
    "map_default k v f [] = [(k, v)]"
wenzelm@63462
   750
  | "map_default k v f (p # ps) =
wenzelm@63462
   751
      (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
bulwahn@45868
   752
bulwahn@45868
   753
lemma map_of_map_default:
wenzelm@56327
   754
  "map_of (map_default k v f xs) =
wenzelm@56327
   755
    (map_of xs)(k := case map_of xs k of None \<Rightarrow> Some v | Some v' \<Rightarrow> Some (f v'))"
wenzelm@56327
   756
  by (induct xs) auto
bulwahn@45868
   757
wenzelm@56327
   758
lemma dom_map_default: "fst ` set (map_default k v f xs) = insert k (fst ` set xs)"
wenzelm@56327
   759
  by (induct xs) auto
bulwahn@45868
   760
bulwahn@45868
   761
lemma distinct_map_default:
bulwahn@45868
   762
  assumes "distinct (map fst xs)"
bulwahn@45868
   763
  shows "distinct (map fst (map_default k v f xs))"
wenzelm@56327
   764
  using assms by (induct xs) (auto simp add: dom_map_default)
bulwahn@45868
   765
wenzelm@59943
   766
end
bulwahn@45884
   767
schirmer@19234
   768
end