src/HOL/Library/AssocList.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34975 f099b0b20646
child 35156 37872c68a385
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@22803
     1
(*  Title:      HOL/Library/AssocList.thy
haftmann@34975
     2
    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
schirmer@19234
     3
*)
schirmer@19234
     4
schirmer@19234
     5
header {* Map operations implemented on association lists*}
schirmer@19234
     6
schirmer@19234
     7
theory AssocList 
haftmann@34975
     8
imports Main
schirmer@19234
     9
begin
schirmer@19234
    10
haftmann@22740
    11
text {*
haftmann@22740
    12
  The operations preserve distinctness of keys and 
haftmann@22740
    13
  function @{term "clearjunk"} distributes over them. Since 
haftmann@22740
    14
  @{term clearjunk} enforces distinctness of keys it can be used
haftmann@22740
    15
  to establish the invariant, e.g. for inductive proofs.
haftmann@22740
    16
*}
schirmer@19234
    17
haftmann@34975
    18
subsection {* @{text update} and @{text updates} *}
nipkow@19323
    19
haftmann@34975
    20
primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@22740
    21
    "update k v [] = [(k, v)]"
haftmann@22740
    22
  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
schirmer@19234
    23
haftmann@34975
    24
lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
haftmann@34975
    25
  by (induct al) (auto simp add: expand_fun_eq)
wenzelm@23373
    26
haftmann@34975
    27
corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
haftmann@34975
    28
  by (simp add: update_conv')
schirmer@19234
    29
schirmer@19234
    30
lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
schirmer@19234
    31
  by (induct al) auto
schirmer@19234
    32
haftmann@34975
    33
lemma update_keys:
haftmann@34975
    34
  "map fst (update k v al) =
haftmann@34975
    35
    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
haftmann@34975
    36
  by (induct al) simp_all
haftmann@34975
    37
schirmer@19234
    38
lemma distinct_update:
schirmer@19234
    39
  assumes "distinct (map fst al)" 
schirmer@19234
    40
  shows "distinct (map fst (update k v al))"
haftmann@34975
    41
  using assms by (simp add: update_keys)
schirmer@19234
    42
schirmer@19234
    43
lemma update_filter: 
nipkow@23281
    44
  "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
    45
  by (induct ps) auto
schirmer@19234
    46
schirmer@19234
    47
lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
schirmer@19234
    48
  by (induct al) auto
schirmer@19234
    49
schirmer@19234
    50
lemma update_nonempty [simp]: "update k v al \<noteq> []"
schirmer@19234
    51
  by (induct al) auto
schirmer@19234
    52
haftmann@34975
    53
lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
wenzelm@20503
    54
proof (induct al arbitrary: al') 
schirmer@19234
    55
  case Nil thus ?case 
schirmer@19234
    56
    by (cases al') (auto split: split_if_asm)
schirmer@19234
    57
next
schirmer@19234
    58
  case Cons thus ?case
schirmer@19234
    59
    by (cases al') (auto split: split_if_asm)
schirmer@19234
    60
qed
schirmer@19234
    61
schirmer@19234
    62
lemma update_last [simp]: "update k v (update k v' al) = update k v al"
schirmer@19234
    63
  by (induct al) auto
schirmer@19234
    64
schirmer@19234
    65
text {* Note that the lists are not necessarily the same:
haftmann@34975
    66
        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and 
haftmann@34975
    67
        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
schirmer@19234
    68
lemma update_swap: "k\<noteq>k' 
schirmer@19234
    69
  \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
haftmann@34975
    70
  by (simp add: update_conv' expand_fun_eq)
schirmer@19234
    71
schirmer@19234
    72
lemma update_Some_unfold: 
haftmann@34975
    73
  "map_of (update k v al) x = Some y \<longleftrightarrow>
haftmann@34975
    74
    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
schirmer@19234
    75
  by (simp add: update_conv' map_upd_Some_unfold)
schirmer@19234
    76
haftmann@34975
    77
lemma image_update [simp]:
haftmann@34975
    78
  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
schirmer@19234
    79
  by (simp add: update_conv' image_map_upd)
schirmer@19234
    80
haftmann@34975
    81
definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
    82
  "updates ks vs al = foldl (\<lambda>al (k, v). update k v al) al (zip ks vs)"
schirmer@19234
    83
haftmann@34975
    84
lemma updates_simps [simp]:
haftmann@34975
    85
  "updates [] vs ps = ps"
haftmann@34975
    86
  "updates ks [] ps = ps"
haftmann@34975
    87
  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
haftmann@34975
    88
  by (simp_all add: updates_def)
haftmann@34975
    89
haftmann@34975
    90
lemma updates_key_simp [simp]:
haftmann@34975
    91
  "updates (k # ks) vs ps =
haftmann@34975
    92
    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
haftmann@34975
    93
  by (cases vs) simp_all
haftmann@34975
    94
haftmann@34975
    95
lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
haftmann@34975
    96
proof -
haftmann@34975
    97
  have "foldl (\<lambda>f (k, v). f(k \<mapsto> v)) (map_of al) (zip ks vs) =
haftmann@34975
    98
     map_of (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
haftmann@34975
    99
    by (rule foldl_apply) (auto simp add: expand_fun_eq update_conv')
haftmann@34975
   100
  then show ?thesis
haftmann@34975
   101
    by (simp add: updates_def map_upds_fold_map_upd)
haftmann@34975
   102
qed
schirmer@19234
   103
schirmer@19234
   104
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
haftmann@34975
   105
  by (simp add: updates_conv')
schirmer@19234
   106
schirmer@19234
   107
lemma distinct_updates:
schirmer@19234
   108
  assumes "distinct (map fst al)"
schirmer@19234
   109
  shows "distinct (map fst (updates ks vs al))"
haftmann@34975
   110
proof -
haftmann@34975
   111
  from assms have "distinct (foldl
haftmann@34975
   112
       (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
haftmann@34975
   113
       (map fst al) (zip ks vs))"
haftmann@34975
   114
    by (rule foldl_invariant) auto
haftmann@34975
   115
  moreover have "foldl (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
haftmann@34975
   116
       (map fst al) (zip ks vs)
haftmann@34975
   117
       = map fst (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
haftmann@34975
   118
    by (rule foldl_apply) (simp add: update_keys split_def comp_def)
haftmann@34975
   119
  ultimately show ?thesis by (simp add: updates_def)
haftmann@34975
   120
qed
schirmer@19234
   121
schirmer@19234
   122
lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
schirmer@19234
   123
  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
wenzelm@20503
   124
  by (induct ks arbitrary: vs al) (auto split: list.splits)
schirmer@19234
   125
schirmer@19234
   126
lemma updates_list_update_drop[simp]:
schirmer@19234
   127
 "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
schirmer@19234
   128
   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
wenzelm@20503
   129
  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
schirmer@19234
   130
schirmer@19234
   131
lemma update_updates_conv_if: "
schirmer@19234
   132
 map_of (updates xs ys (update x y al)) =
schirmer@19234
   133
 map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
schirmer@19234
   134
                                  else (update x y (updates xs ys al)))"
schirmer@19234
   135
  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
schirmer@19234
   136
schirmer@19234
   137
lemma updates_twist [simp]:
schirmer@19234
   138
 "k \<notin> set ks \<Longrightarrow> 
schirmer@19234
   139
  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
schirmer@19234
   140
  by (simp add: updates_conv' update_conv' map_upds_twist)
schirmer@19234
   141
schirmer@19234
   142
lemma updates_apply_notin[simp]:
schirmer@19234
   143
 "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
schirmer@19234
   144
  by (simp add: updates_conv)
schirmer@19234
   145
schirmer@19234
   146
lemma updates_append_drop[simp]:
schirmer@19234
   147
  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
wenzelm@20503
   148
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   149
schirmer@19234
   150
lemma updates_append2_drop[simp]:
schirmer@19234
   151
  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
wenzelm@20503
   152
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   153
wenzelm@23373
   154
haftmann@34975
   155
subsection {* @{text delete} *}
haftmann@34975
   156
haftmann@34975
   157
definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   158
  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
haftmann@34975
   159
haftmann@34975
   160
lemma delete_simps [simp]:
haftmann@34975
   161
  "delete k [] = []"
haftmann@34975
   162
  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
haftmann@34975
   163
  by (auto simp add: delete_eq)
haftmann@34975
   164
haftmann@34975
   165
lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
haftmann@34975
   166
  by (induct al) (auto simp add: expand_fun_eq)
haftmann@34975
   167
haftmann@34975
   168
corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
haftmann@34975
   169
  by (simp add: delete_conv')
haftmann@34975
   170
haftmann@34975
   171
lemma delete_keys:
haftmann@34975
   172
  "map fst (delete k al) = removeAll k (map fst al)"
haftmann@34975
   173
  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
haftmann@34975
   174
haftmann@34975
   175
lemma distinct_delete:
haftmann@34975
   176
  assumes "distinct (map fst al)" 
haftmann@34975
   177
  shows "distinct (map fst (delete k al))"
haftmann@34975
   178
  using assms by (simp add: delete_keys distinct_removeAll)
haftmann@34975
   179
haftmann@34975
   180
lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
haftmann@34975
   181
  by (auto simp add: image_iff delete_eq filter_id_conv)
haftmann@34975
   182
haftmann@34975
   183
lemma delete_idem: "delete k (delete k al) = delete k al"
haftmann@34975
   184
  by (simp add: delete_eq)
haftmann@34975
   185
haftmann@34975
   186
lemma map_of_delete [simp]:
haftmann@34975
   187
    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
haftmann@34975
   188
  by (simp add: delete_conv')
haftmann@34975
   189
haftmann@34975
   190
lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
haftmann@34975
   191
  by (auto simp add: delete_eq)
haftmann@34975
   192
haftmann@34975
   193
lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
haftmann@34975
   194
  by (auto simp add: delete_eq)
haftmann@34975
   195
haftmann@34975
   196
lemma delete_update_same:
haftmann@34975
   197
  "delete k (update k v al) = delete k al"
haftmann@34975
   198
  by (induct al) simp_all
haftmann@34975
   199
haftmann@34975
   200
lemma delete_update:
haftmann@34975
   201
  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
haftmann@34975
   202
  by (induct al) simp_all
haftmann@34975
   203
haftmann@34975
   204
lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
haftmann@34975
   205
  by (simp add: delete_eq conj_commute)
haftmann@34975
   206
haftmann@34975
   207
lemma length_delete_le: "length (delete k al) \<le> length al"
haftmann@34975
   208
  by (simp add: delete_eq)
haftmann@34975
   209
haftmann@34975
   210
haftmann@34975
   211
subsection {* @{text restrict} *}
haftmann@34975
   212
haftmann@34975
   213
definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   214
  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
haftmann@34975
   215
haftmann@34975
   216
lemma restr_simps [simp]:
haftmann@34975
   217
  "restrict A [] = []"
haftmann@34975
   218
  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
haftmann@34975
   219
  by (auto simp add: restrict_eq)
haftmann@34975
   220
haftmann@34975
   221
lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
haftmann@34975
   222
proof
haftmann@34975
   223
  fix k
haftmann@34975
   224
  show "map_of (restrict A al) k = ((map_of al)|` A) k"
haftmann@34975
   225
    by (induct al) (simp, cases "k \<in> A", auto)
haftmann@34975
   226
qed
haftmann@34975
   227
haftmann@34975
   228
corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
haftmann@34975
   229
  by (simp add: restr_conv')
haftmann@34975
   230
haftmann@34975
   231
lemma distinct_restr:
haftmann@34975
   232
  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
haftmann@34975
   233
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   234
haftmann@34975
   235
lemma restr_empty [simp]: 
haftmann@34975
   236
  "restrict {} al = []" 
haftmann@34975
   237
  "restrict A [] = []"
haftmann@34975
   238
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   239
haftmann@34975
   240
lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
haftmann@34975
   241
  by (simp add: restr_conv')
haftmann@34975
   242
haftmann@34975
   243
lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
haftmann@34975
   244
  by (simp add: restr_conv')
haftmann@34975
   245
haftmann@34975
   246
lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
haftmann@34975
   247
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   248
haftmann@34975
   249
lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
haftmann@34975
   250
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   251
haftmann@34975
   252
lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
haftmann@34975
   253
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   254
haftmann@34975
   255
lemma restr_update[simp]:
haftmann@34975
   256
 "map_of (restrict D (update x y al)) = 
haftmann@34975
   257
  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
haftmann@34975
   258
  by (simp add: restr_conv' update_conv')
haftmann@34975
   259
haftmann@34975
   260
lemma restr_delete [simp]:
haftmann@34975
   261
  "(delete x (restrict D al)) = 
haftmann@34975
   262
    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
haftmann@34975
   263
apply (simp add: delete_eq restrict_eq)
haftmann@34975
   264
apply (auto simp add: split_def)
haftmann@34975
   265
proof -
haftmann@34975
   266
  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
haftmann@34975
   267
  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
   268
    by simp
haftmann@34975
   269
  assume "x \<notin> D"
haftmann@34975
   270
  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
haftmann@34975
   271
  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
haftmann@34975
   272
    by simp
haftmann@34975
   273
qed
haftmann@34975
   274
haftmann@34975
   275
lemma update_restr:
haftmann@34975
   276
 "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
haftmann@34975
   277
  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
schirmer@19234
   278
haftmann@34975
   279
lemma upate_restr_conv [simp]:
haftmann@34975
   280
 "x \<in> D \<Longrightarrow> 
haftmann@34975
   281
 map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
haftmann@34975
   282
  by (simp add: update_conv' restr_conv')
haftmann@34975
   283
haftmann@34975
   284
lemma restr_updates [simp]: "
haftmann@34975
   285
 \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
haftmann@34975
   286
 \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
haftmann@34975
   287
     map_of (updates xs ys (restrict (D - set xs) al))"
haftmann@34975
   288
  by (simp add: updates_conv' restr_conv')
haftmann@34975
   289
haftmann@34975
   290
lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
haftmann@34975
   291
  by (induct ps) auto
haftmann@34975
   292
haftmann@34975
   293
haftmann@34975
   294
subsection {* @{text clearjunk} *}
haftmann@34975
   295
haftmann@34975
   296
function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   297
    "clearjunk [] = []"  
haftmann@34975
   298
  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
haftmann@34975
   299
  by pat_completeness auto
haftmann@34975
   300
termination by (relation "measure length")
haftmann@34975
   301
  (simp_all add: less_Suc_eq_le length_delete_le)
haftmann@34975
   302
haftmann@34975
   303
lemma map_of_clearjunk:
haftmann@34975
   304
  "map_of (clearjunk al) = map_of al"
haftmann@34975
   305
  by (induct al rule: clearjunk.induct)
haftmann@34975
   306
    (simp_all add: expand_fun_eq)
haftmann@34975
   307
haftmann@34975
   308
lemma clearjunk_keys_set:
haftmann@34975
   309
  "set (map fst (clearjunk al)) = set (map fst al)"
haftmann@34975
   310
  by (induct al rule: clearjunk.induct)
haftmann@34975
   311
    (simp_all add: delete_keys)
haftmann@34975
   312
haftmann@34975
   313
lemma dom_clearjunk:
haftmann@34975
   314
  "fst ` set (clearjunk al) = fst ` set al"
haftmann@34975
   315
  using clearjunk_keys_set by simp
haftmann@34975
   316
haftmann@34975
   317
lemma distinct_clearjunk [simp]:
haftmann@34975
   318
  "distinct (map fst (clearjunk al))"
haftmann@34975
   319
  by (induct al rule: clearjunk.induct)
haftmann@34975
   320
    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
haftmann@34975
   321
haftmann@34975
   322
lemma ran_clearjunk:
haftmann@34975
   323
  "ran (map_of (clearjunk al)) = ran (map_of al)"
haftmann@34975
   324
  by (simp add: map_of_clearjunk)
haftmann@34975
   325
haftmann@34975
   326
lemma ran_map_of:
haftmann@34975
   327
  "ran (map_of al) = snd ` set (clearjunk al)"
haftmann@34975
   328
proof -
haftmann@34975
   329
  have "ran (map_of al) = ran (map_of (clearjunk al))"
haftmann@34975
   330
    by (simp add: ran_clearjunk)
haftmann@34975
   331
  also have "\<dots> = snd ` set (clearjunk al)"
haftmann@34975
   332
    by (simp add: ran_distinct)
haftmann@34975
   333
  finally show ?thesis .
haftmann@34975
   334
qed
haftmann@34975
   335
haftmann@34975
   336
lemma clearjunk_update:
haftmann@34975
   337
  "clearjunk (update k v al) = update k v (clearjunk al)"
haftmann@34975
   338
  by (induct al rule: clearjunk.induct)
haftmann@34975
   339
    (simp_all add: delete_update)
schirmer@19234
   340
haftmann@34975
   341
lemma clearjunk_updates:
haftmann@34975
   342
  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
haftmann@34975
   343
proof -
haftmann@34975
   344
  have "foldl (\<lambda>al (k, v). update k v al) (clearjunk al) (zip ks vs) =
haftmann@34975
   345
    clearjunk (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
haftmann@34975
   346
    by (rule foldl_apply) (simp add: clearjunk_update expand_fun_eq split_def)
haftmann@34975
   347
  then show ?thesis by (simp add: updates_def)
haftmann@34975
   348
qed
haftmann@34975
   349
haftmann@34975
   350
lemma clearjunk_delete:
haftmann@34975
   351
  "clearjunk (delete x al) = delete x (clearjunk al)"
haftmann@34975
   352
  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
haftmann@34975
   353
haftmann@34975
   354
lemma clearjunk_restrict:
haftmann@34975
   355
 "clearjunk (restrict A al) = restrict A (clearjunk al)"
haftmann@34975
   356
  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
haftmann@34975
   357
haftmann@34975
   358
lemma distinct_clearjunk_id [simp]:
haftmann@34975
   359
  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
haftmann@34975
   360
  by (induct al rule: clearjunk.induct) auto
haftmann@34975
   361
haftmann@34975
   362
lemma clearjunk_idem:
haftmann@34975
   363
  "clearjunk (clearjunk al) = clearjunk al"
haftmann@34975
   364
  by simp
haftmann@34975
   365
haftmann@34975
   366
lemma length_clearjunk:
haftmann@34975
   367
  "length (clearjunk al) \<le> length al"
haftmann@34975
   368
proof (induct al rule: clearjunk.induct [case_names Nil Cons])
haftmann@34975
   369
  case Nil then show ?case by simp
haftmann@34975
   370
next
haftmann@34975
   371
  case (Cons kv al)
haftmann@34975
   372
  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
haftmann@34975
   373
  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
haftmann@34975
   374
  then show ?case by simp
haftmann@34975
   375
qed
haftmann@34975
   376
haftmann@34975
   377
lemma delete_map:
haftmann@34975
   378
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   379
  shows "delete k (map f ps) = map f (delete k ps)"
haftmann@34975
   380
  by (simp add: delete_eq filter_map comp_def split_def assms)
haftmann@34975
   381
haftmann@34975
   382
lemma clearjunk_map:
haftmann@34975
   383
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   384
  shows "clearjunk (map f ps) = map f (clearjunk ps)"
haftmann@34975
   385
  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
haftmann@34975
   386
    (simp_all add: clearjunk_delete delete_map assms)
haftmann@34975
   387
haftmann@34975
   388
haftmann@34975
   389
subsection {* @{text map_ran} *}
haftmann@34975
   390
haftmann@34975
   391
definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   392
  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
haftmann@34975
   393
haftmann@34975
   394
lemma map_ran_simps [simp]:
haftmann@34975
   395
  "map_ran f [] = []"
haftmann@34975
   396
  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
haftmann@34975
   397
  by (simp_all add: map_ran_def)
haftmann@34975
   398
haftmann@34975
   399
lemma dom_map_ran:
haftmann@34975
   400
  "fst ` set (map_ran f al) = fst ` set al"
haftmann@34975
   401
  by (simp add: map_ran_def image_image split_def)
haftmann@34975
   402
  
haftmann@34975
   403
lemma map_ran_conv:
haftmann@34975
   404
  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
schirmer@19234
   405
  by (induct al) auto
schirmer@19234
   406
haftmann@34975
   407
lemma distinct_map_ran:
haftmann@34975
   408
  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
haftmann@34975
   409
  by (simp add: map_ran_def split_def comp_def)
schirmer@19234
   410
haftmann@34975
   411
lemma map_ran_filter:
haftmann@34975
   412
  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
haftmann@34975
   413
  by (simp add: map_ran_def filter_map split_def comp_def)
schirmer@19234
   414
haftmann@34975
   415
lemma clearjunk_map_ran:
haftmann@34975
   416
  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
haftmann@34975
   417
  by (simp add: map_ran_def split_def clearjunk_map)
schirmer@19234
   418
wenzelm@23373
   419
haftmann@34975
   420
subsection {* @{text merge} *}
haftmann@34975
   421
haftmann@34975
   422
definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   423
  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
haftmann@34975
   424
haftmann@34975
   425
lemma merge_simps [simp]:
haftmann@34975
   426
  "merge qs [] = qs"
haftmann@34975
   427
  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
haftmann@34975
   428
  by (simp_all add: merge_def split_def)
haftmann@34975
   429
haftmann@34975
   430
lemma merge_updates:
haftmann@34975
   431
  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
haftmann@34975
   432
  by (simp add: merge_def updates_def split_def
haftmann@34975
   433
    foldr_foldl zip_rev zip_map_fst_snd)
schirmer@19234
   434
schirmer@19234
   435
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
wenzelm@20503
   436
  by (induct ys arbitrary: xs) (auto simp add: dom_update)
schirmer@19234
   437
schirmer@19234
   438
lemma distinct_merge:
schirmer@19234
   439
  assumes "distinct (map fst xs)"
schirmer@19234
   440
  shows "distinct (map fst (merge xs ys))"
haftmann@34975
   441
using assms by (simp add: merge_updates distinct_updates)
schirmer@19234
   442
schirmer@19234
   443
lemma clearjunk_merge:
haftmann@34975
   444
  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
haftmann@34975
   445
  by (simp add: merge_updates clearjunk_updates)
schirmer@19234
   446
haftmann@34975
   447
lemma merge_conv':
haftmann@34975
   448
  "map_of (merge xs ys) = map_of xs ++ map_of ys"
haftmann@34975
   449
proof -
haftmann@34975
   450
  have "foldl (\<lambda>m (k, v). m(k \<mapsto> v)) (map_of xs) (rev ys) =
haftmann@34975
   451
    map_of (foldl (\<lambda>xs (k, v). update k v xs) xs (rev ys)) "
haftmann@34975
   452
    by (rule foldl_apply) (simp add: expand_fun_eq split_def update_conv')
haftmann@34975
   453
  then show ?thesis
haftmann@34975
   454
    by (simp add: merge_def map_add_map_of_foldr foldr_foldl split_def)
schirmer@19234
   455
qed
schirmer@19234
   456
haftmann@34975
   457
corollary merge_conv:
haftmann@34975
   458
  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
haftmann@34975
   459
  by (simp add: merge_conv')
schirmer@19234
   460
haftmann@34975
   461
lemma merge_empty: "map_of (merge [] ys) = map_of ys"
schirmer@19234
   462
  by (simp add: merge_conv')
schirmer@19234
   463
schirmer@19234
   464
lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
schirmer@19234
   465
                           map_of (merge (merge m1 m2) m3)"
schirmer@19234
   466
  by (simp add: merge_conv')
schirmer@19234
   467
schirmer@19234
   468
lemma merge_Some_iff: 
schirmer@19234
   469
 "(map_of (merge m n) k = Some x) = 
schirmer@19234
   470
  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
schirmer@19234
   471
  by (simp add: merge_conv' map_add_Some_iff)
schirmer@19234
   472
haftmann@34975
   473
lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
schirmer@19234
   474
schirmer@19234
   475
lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
schirmer@19234
   476
  by (simp add: merge_conv')
schirmer@19234
   477
schirmer@19234
   478
lemma merge_None [iff]: 
schirmer@19234
   479
  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
schirmer@19234
   480
  by (simp add: merge_conv')
schirmer@19234
   481
schirmer@19234
   482
lemma merge_upd[simp]: 
schirmer@19234
   483
  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
schirmer@19234
   484
  by (simp add: update_conv' merge_conv')
schirmer@19234
   485
schirmer@19234
   486
lemma merge_updatess[simp]: 
schirmer@19234
   487
  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
schirmer@19234
   488
  by (simp add: updates_conv' merge_conv')
schirmer@19234
   489
schirmer@19234
   490
lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
schirmer@19234
   491
  by (simp add: merge_conv')
schirmer@19234
   492
wenzelm@23373
   493
haftmann@34975
   494
subsection {* @{text compose} *}
haftmann@34975
   495
haftmann@34975
   496
function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
haftmann@34975
   497
    "compose [] ys = []"
haftmann@34975
   498
  | "compose (x#xs) ys = (case map_of ys (snd x)
haftmann@34975
   499
       of None \<Rightarrow> compose (delete (fst x) xs) ys
haftmann@34975
   500
        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
haftmann@34975
   501
  by pat_completeness auto
haftmann@34975
   502
termination by (relation "measure (length \<circ> fst)")
haftmann@34975
   503
  (simp_all add: less_Suc_eq_le length_delete_le)
schirmer@19234
   504
schirmer@19234
   505
lemma compose_first_None [simp]: 
schirmer@19234
   506
  assumes "map_of xs k = None" 
schirmer@19234
   507
  shows "map_of (compose xs ys) k = None"
wenzelm@23373
   508
using assms by (induct xs ys rule: compose.induct)
haftmann@22916
   509
  (auto split: option.splits split_if_asm)
schirmer@19234
   510
schirmer@19234
   511
lemma compose_conv: 
schirmer@19234
   512
  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
haftmann@22916
   513
proof (induct xs ys rule: compose.induct)
haftmann@22916
   514
  case 1 then show ?case by simp
schirmer@19234
   515
next
haftmann@22916
   516
  case (2 x xs ys) show ?case
schirmer@19234
   517
  proof (cases "map_of ys (snd x)")
haftmann@22916
   518
    case None with 2
schirmer@19234
   519
    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
schirmer@19234
   520
               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
schirmer@19234
   521
      by simp
schirmer@19234
   522
    show ?thesis
schirmer@19234
   523
    proof (cases "fst x = k")
schirmer@19234
   524
      case True
schirmer@19234
   525
      from True delete_notin_dom [of k xs]
schirmer@19234
   526
      have "map_of (delete (fst x) xs) k = None"
wenzelm@32960
   527
        by (simp add: map_of_eq_None_iff)
schirmer@19234
   528
      with hyp show ?thesis
wenzelm@32960
   529
        using True None
wenzelm@32960
   530
        by simp
schirmer@19234
   531
    next
schirmer@19234
   532
      case False
schirmer@19234
   533
      from False have "map_of (delete (fst x) xs) k = map_of xs k"
wenzelm@32960
   534
        by simp
schirmer@19234
   535
      with hyp show ?thesis
wenzelm@32960
   536
        using False None
wenzelm@32960
   537
        by (simp add: map_comp_def)
schirmer@19234
   538
    qed
schirmer@19234
   539
  next
schirmer@19234
   540
    case (Some v)
haftmann@22916
   541
    with 2
schirmer@19234
   542
    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
schirmer@19234
   543
      by simp
schirmer@19234
   544
    with Some show ?thesis
schirmer@19234
   545
      by (auto simp add: map_comp_def)
schirmer@19234
   546
  qed
schirmer@19234
   547
qed
schirmer@19234
   548
   
schirmer@19234
   549
lemma compose_conv': 
schirmer@19234
   550
  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
schirmer@19234
   551
  by (rule ext) (rule compose_conv)
schirmer@19234
   552
schirmer@19234
   553
lemma compose_first_Some [simp]:
schirmer@19234
   554
  assumes "map_of xs k = Some v" 
schirmer@19234
   555
  shows "map_of (compose xs ys) k = map_of ys v"
wenzelm@23373
   556
using assms by (simp add: compose_conv)
schirmer@19234
   557
schirmer@19234
   558
lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
haftmann@22916
   559
proof (induct xs ys rule: compose.induct)
haftmann@22916
   560
  case 1 thus ?case by simp
schirmer@19234
   561
next
haftmann@22916
   562
  case (2 x xs ys)
schirmer@19234
   563
  show ?case
schirmer@19234
   564
  proof (cases "map_of ys (snd x)")
schirmer@19234
   565
    case None
haftmann@22916
   566
    with "2.hyps"
schirmer@19234
   567
    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
schirmer@19234
   568
      by simp
schirmer@19234
   569
    also
schirmer@19234
   570
    have "\<dots> \<subseteq> fst ` set xs"
schirmer@19234
   571
      by (rule dom_delete_subset)
schirmer@19234
   572
    finally show ?thesis
schirmer@19234
   573
      using None
schirmer@19234
   574
      by auto
schirmer@19234
   575
  next
schirmer@19234
   576
    case (Some v)
haftmann@22916
   577
    with "2.hyps"
schirmer@19234
   578
    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
schirmer@19234
   579
      by simp
schirmer@19234
   580
    with Some show ?thesis
schirmer@19234
   581
      by auto
schirmer@19234
   582
  qed
schirmer@19234
   583
qed
schirmer@19234
   584
schirmer@19234
   585
lemma distinct_compose:
schirmer@19234
   586
 assumes "distinct (map fst xs)"
schirmer@19234
   587
 shows "distinct (map fst (compose xs ys))"
wenzelm@23373
   588
using assms
haftmann@22916
   589
proof (induct xs ys rule: compose.induct)
haftmann@22916
   590
  case 1 thus ?case by simp
schirmer@19234
   591
next
haftmann@22916
   592
  case (2 x xs ys)
schirmer@19234
   593
  show ?case
schirmer@19234
   594
  proof (cases "map_of ys (snd x)")
schirmer@19234
   595
    case None
haftmann@22916
   596
    with 2 show ?thesis by simp
schirmer@19234
   597
  next
schirmer@19234
   598
    case (Some v)
haftmann@22916
   599
    with 2 dom_compose [of xs ys] show ?thesis 
schirmer@19234
   600
      by (auto)
schirmer@19234
   601
  qed
schirmer@19234
   602
qed
schirmer@19234
   603
schirmer@19234
   604
lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
haftmann@22916
   605
proof (induct xs ys rule: compose.induct)
haftmann@22916
   606
  case 1 thus ?case by simp
schirmer@19234
   607
next
haftmann@22916
   608
  case (2 x xs ys)
schirmer@19234
   609
  show ?case
schirmer@19234
   610
  proof (cases "map_of ys (snd x)")
schirmer@19234
   611
    case None
haftmann@22916
   612
    with 2 have 
schirmer@19234
   613
      hyp: "compose (delete k (delete (fst x) xs)) ys =
schirmer@19234
   614
            delete k (compose (delete (fst x) xs) ys)"
schirmer@19234
   615
      by simp
schirmer@19234
   616
    show ?thesis
schirmer@19234
   617
    proof (cases "fst x = k")
schirmer@19234
   618
      case True
schirmer@19234
   619
      with None hyp
schirmer@19234
   620
      show ?thesis
wenzelm@32960
   621
        by (simp add: delete_idem)
schirmer@19234
   622
    next
schirmer@19234
   623
      case False
schirmer@19234
   624
      from None False hyp
schirmer@19234
   625
      show ?thesis
wenzelm@32960
   626
        by (simp add: delete_twist)
schirmer@19234
   627
    qed
schirmer@19234
   628
  next
schirmer@19234
   629
    case (Some v)
haftmann@22916
   630
    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
schirmer@19234
   631
    with Some show ?thesis
schirmer@19234
   632
      by simp
schirmer@19234
   633
  qed
schirmer@19234
   634
qed
schirmer@19234
   635
schirmer@19234
   636
lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
haftmann@22916
   637
  by (induct xs ys rule: compose.induct) 
schirmer@19234
   638
     (auto simp add: map_of_clearjunk split: option.splits)
schirmer@19234
   639
   
schirmer@19234
   640
lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
schirmer@19234
   641
  by (induct xs rule: clearjunk.induct)
schirmer@19234
   642
     (auto split: option.splits simp add: clearjunk_delete delete_idem
schirmer@19234
   643
               compose_delete_twist)
schirmer@19234
   644
   
schirmer@19234
   645
lemma compose_empty [simp]:
schirmer@19234
   646
 "compose xs [] = []"
haftmann@22916
   647
  by (induct xs) (auto simp add: compose_delete_twist)
schirmer@19234
   648
schirmer@19234
   649
lemma compose_Some_iff:
schirmer@19234
   650
  "(map_of (compose xs ys) k = Some v) = 
schirmer@19234
   651
     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
schirmer@19234
   652
  by (simp add: compose_conv map_comp_Some_iff)
schirmer@19234
   653
schirmer@19234
   654
lemma map_comp_None_iff:
schirmer@19234
   655
  "(map_of (compose xs ys) k = None) = 
schirmer@19234
   656
    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
schirmer@19234
   657
  by (simp add: compose_conv map_comp_None_iff)
schirmer@19234
   658
schirmer@19234
   659
end