src/HOL/Library/AssocList.thy
author haftmann
Tue Jun 29 07:55:18 2010 +0200 (2010-06-29)
changeset 37608 165cd386288d
parent 37591 d3daea901123
parent 37595 9591362629e3
child 38857 97775f3e8722
permissions -rw-r--r--
merged
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@37458
     8
imports Main More_List Mapping
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@37458
    82
  "updates ks vs = More_List.fold (prod_case update) (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@37458
    97
  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
haftmann@37458
    98
    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
haftmann@37458
    99
    by (rule fold_apply) (auto simp add: expand_fun_eq update_conv')
haftmann@37458
   100
  then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def)
haftmann@34975
   101
qed
schirmer@19234
   102
schirmer@19234
   103
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
haftmann@34975
   104
  by (simp add: updates_conv')
schirmer@19234
   105
schirmer@19234
   106
lemma distinct_updates:
schirmer@19234
   107
  assumes "distinct (map fst al)"
schirmer@19234
   108
  shows "distinct (map fst (updates ks vs al))"
haftmann@34975
   109
proof -
haftmann@37458
   110
  have "distinct (More_List.fold
haftmann@37458
   111
       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
haftmann@37458
   112
       (zip ks vs) (map fst al))"
haftmann@37458
   113
    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
haftmann@37458
   114
  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
haftmann@37458
   115
    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
haftmann@37458
   116
    by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
haftmann@37458
   117
  ultimately show ?thesis by (simp add: updates_def expand_fun_eq)
haftmann@34975
   118
qed
schirmer@19234
   119
schirmer@19234
   120
lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
schirmer@19234
   121
  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
wenzelm@20503
   122
  by (induct ks arbitrary: vs al) (auto split: list.splits)
schirmer@19234
   123
schirmer@19234
   124
lemma updates_list_update_drop[simp]:
schirmer@19234
   125
 "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
schirmer@19234
   126
   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
wenzelm@20503
   127
  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
schirmer@19234
   128
schirmer@19234
   129
lemma update_updates_conv_if: "
schirmer@19234
   130
 map_of (updates xs ys (update x y al)) =
schirmer@19234
   131
 map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
schirmer@19234
   132
                                  else (update x y (updates xs ys al)))"
schirmer@19234
   133
  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
schirmer@19234
   134
schirmer@19234
   135
lemma updates_twist [simp]:
schirmer@19234
   136
 "k \<notin> set ks \<Longrightarrow> 
schirmer@19234
   137
  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
schirmer@19234
   138
  by (simp add: updates_conv' update_conv' map_upds_twist)
schirmer@19234
   139
schirmer@19234
   140
lemma updates_apply_notin[simp]:
schirmer@19234
   141
 "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
schirmer@19234
   142
  by (simp add: updates_conv)
schirmer@19234
   143
schirmer@19234
   144
lemma updates_append_drop[simp]:
schirmer@19234
   145
  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
wenzelm@20503
   146
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   147
schirmer@19234
   148
lemma updates_append2_drop[simp]:
schirmer@19234
   149
  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
wenzelm@20503
   150
  by (induct xs arbitrary: ys al) (auto split: list.splits)
schirmer@19234
   151
wenzelm@23373
   152
haftmann@34975
   153
subsection {* @{text delete} *}
haftmann@34975
   154
haftmann@34975
   155
definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   156
  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
haftmann@34975
   157
haftmann@34975
   158
lemma delete_simps [simp]:
haftmann@34975
   159
  "delete k [] = []"
haftmann@34975
   160
  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
haftmann@34975
   161
  by (auto simp add: delete_eq)
haftmann@34975
   162
haftmann@34975
   163
lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
haftmann@34975
   164
  by (induct al) (auto simp add: expand_fun_eq)
haftmann@34975
   165
haftmann@34975
   166
corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
haftmann@34975
   167
  by (simp add: delete_conv')
haftmann@34975
   168
haftmann@34975
   169
lemma delete_keys:
haftmann@34975
   170
  "map fst (delete k al) = removeAll k (map fst al)"
haftmann@34975
   171
  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
haftmann@34975
   172
haftmann@34975
   173
lemma distinct_delete:
haftmann@34975
   174
  assumes "distinct (map fst al)" 
haftmann@34975
   175
  shows "distinct (map fst (delete k al))"
haftmann@34975
   176
  using assms by (simp add: delete_keys distinct_removeAll)
haftmann@34975
   177
haftmann@34975
   178
lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
haftmann@34975
   179
  by (auto simp add: image_iff delete_eq filter_id_conv)
haftmann@34975
   180
haftmann@34975
   181
lemma delete_idem: "delete k (delete k al) = delete k al"
haftmann@34975
   182
  by (simp add: delete_eq)
haftmann@34975
   183
haftmann@34975
   184
lemma map_of_delete [simp]:
haftmann@34975
   185
    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
haftmann@34975
   186
  by (simp add: delete_conv')
haftmann@34975
   187
haftmann@34975
   188
lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
haftmann@34975
   189
  by (auto simp add: delete_eq)
haftmann@34975
   190
haftmann@34975
   191
lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
haftmann@34975
   192
  by (auto simp add: delete_eq)
haftmann@34975
   193
haftmann@34975
   194
lemma delete_update_same:
haftmann@34975
   195
  "delete k (update k v al) = delete k al"
haftmann@34975
   196
  by (induct al) simp_all
haftmann@34975
   197
haftmann@34975
   198
lemma delete_update:
haftmann@34975
   199
  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
haftmann@34975
   200
  by (induct al) simp_all
haftmann@34975
   201
haftmann@34975
   202
lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
haftmann@34975
   203
  by (simp add: delete_eq conj_commute)
haftmann@34975
   204
haftmann@34975
   205
lemma length_delete_le: "length (delete k al) \<le> length al"
haftmann@34975
   206
  by (simp add: delete_eq)
haftmann@34975
   207
haftmann@34975
   208
haftmann@34975
   209
subsection {* @{text restrict} *}
haftmann@34975
   210
haftmann@34975
   211
definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   212
  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
haftmann@34975
   213
haftmann@34975
   214
lemma restr_simps [simp]:
haftmann@34975
   215
  "restrict A [] = []"
haftmann@34975
   216
  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
haftmann@34975
   217
  by (auto simp add: restrict_eq)
haftmann@34975
   218
haftmann@34975
   219
lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
haftmann@34975
   220
proof
haftmann@34975
   221
  fix k
haftmann@34975
   222
  show "map_of (restrict A al) k = ((map_of al)|` A) k"
haftmann@34975
   223
    by (induct al) (simp, cases "k \<in> A", auto)
haftmann@34975
   224
qed
haftmann@34975
   225
haftmann@34975
   226
corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
haftmann@34975
   227
  by (simp add: restr_conv')
haftmann@34975
   228
haftmann@34975
   229
lemma distinct_restr:
haftmann@34975
   230
  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
haftmann@34975
   231
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   232
haftmann@34975
   233
lemma restr_empty [simp]: 
haftmann@34975
   234
  "restrict {} al = []" 
haftmann@34975
   235
  "restrict A [] = []"
haftmann@34975
   236
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   237
haftmann@34975
   238
lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
haftmann@34975
   239
  by (simp add: restr_conv')
haftmann@34975
   240
haftmann@34975
   241
lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
haftmann@34975
   242
  by (simp add: restr_conv')
haftmann@34975
   243
haftmann@34975
   244
lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
haftmann@34975
   245
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   246
haftmann@34975
   247
lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
haftmann@34975
   248
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   249
haftmann@34975
   250
lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
haftmann@34975
   251
  by (induct al) (auto simp add: restrict_eq)
haftmann@34975
   252
haftmann@34975
   253
lemma restr_update[simp]:
haftmann@34975
   254
 "map_of (restrict D (update x y al)) = 
haftmann@34975
   255
  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
haftmann@34975
   256
  by (simp add: restr_conv' update_conv')
haftmann@34975
   257
haftmann@34975
   258
lemma restr_delete [simp]:
haftmann@34975
   259
  "(delete x (restrict D al)) = 
haftmann@34975
   260
    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
haftmann@34975
   261
apply (simp add: delete_eq restrict_eq)
haftmann@34975
   262
apply (auto simp add: split_def)
haftmann@34975
   263
proof -
haftmann@34975
   264
  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
haftmann@34975
   265
  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
   266
    by simp
haftmann@34975
   267
  assume "x \<notin> D"
haftmann@34975
   268
  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
haftmann@34975
   269
  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
haftmann@34975
   270
    by simp
haftmann@34975
   271
qed
haftmann@34975
   272
haftmann@34975
   273
lemma update_restr:
haftmann@34975
   274
 "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
haftmann@34975
   275
  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
schirmer@19234
   276
haftmann@34975
   277
lemma upate_restr_conv [simp]:
haftmann@34975
   278
 "x \<in> D \<Longrightarrow> 
haftmann@34975
   279
 map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
haftmann@34975
   280
  by (simp add: update_conv' restr_conv')
haftmann@34975
   281
haftmann@34975
   282
lemma restr_updates [simp]: "
haftmann@34975
   283
 \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
haftmann@34975
   284
 \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
haftmann@34975
   285
     map_of (updates xs ys (restrict (D - set xs) al))"
haftmann@34975
   286
  by (simp add: updates_conv' restr_conv')
haftmann@34975
   287
haftmann@34975
   288
lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
haftmann@34975
   289
  by (induct ps) auto
haftmann@34975
   290
haftmann@34975
   291
haftmann@34975
   292
subsection {* @{text clearjunk} *}
haftmann@34975
   293
haftmann@34975
   294
function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   295
    "clearjunk [] = []"  
haftmann@34975
   296
  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
haftmann@34975
   297
  by pat_completeness auto
haftmann@34975
   298
termination by (relation "measure length")
haftmann@34975
   299
  (simp_all add: less_Suc_eq_le length_delete_le)
haftmann@34975
   300
haftmann@34975
   301
lemma map_of_clearjunk:
haftmann@34975
   302
  "map_of (clearjunk al) = map_of al"
haftmann@34975
   303
  by (induct al rule: clearjunk.induct)
haftmann@34975
   304
    (simp_all add: expand_fun_eq)
haftmann@34975
   305
haftmann@34975
   306
lemma clearjunk_keys_set:
haftmann@34975
   307
  "set (map fst (clearjunk al)) = set (map fst al)"
haftmann@34975
   308
  by (induct al rule: clearjunk.induct)
haftmann@34975
   309
    (simp_all add: delete_keys)
haftmann@34975
   310
haftmann@34975
   311
lemma dom_clearjunk:
haftmann@34975
   312
  "fst ` set (clearjunk al) = fst ` set al"
haftmann@34975
   313
  using clearjunk_keys_set by simp
haftmann@34975
   314
haftmann@34975
   315
lemma distinct_clearjunk [simp]:
haftmann@34975
   316
  "distinct (map fst (clearjunk al))"
haftmann@34975
   317
  by (induct al rule: clearjunk.induct)
haftmann@34975
   318
    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
haftmann@34975
   319
haftmann@34975
   320
lemma ran_clearjunk:
haftmann@34975
   321
  "ran (map_of (clearjunk al)) = ran (map_of al)"
haftmann@34975
   322
  by (simp add: map_of_clearjunk)
haftmann@34975
   323
haftmann@34975
   324
lemma ran_map_of:
haftmann@34975
   325
  "ran (map_of al) = snd ` set (clearjunk al)"
haftmann@34975
   326
proof -
haftmann@34975
   327
  have "ran (map_of al) = ran (map_of (clearjunk al))"
haftmann@34975
   328
    by (simp add: ran_clearjunk)
haftmann@34975
   329
  also have "\<dots> = snd ` set (clearjunk al)"
haftmann@34975
   330
    by (simp add: ran_distinct)
haftmann@34975
   331
  finally show ?thesis .
haftmann@34975
   332
qed
haftmann@34975
   333
haftmann@34975
   334
lemma clearjunk_update:
haftmann@34975
   335
  "clearjunk (update k v al) = update k v (clearjunk al)"
haftmann@34975
   336
  by (induct al rule: clearjunk.induct)
haftmann@34975
   337
    (simp_all add: delete_update)
schirmer@19234
   338
haftmann@34975
   339
lemma clearjunk_updates:
haftmann@34975
   340
  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
haftmann@34975
   341
proof -
haftmann@37458
   342
  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
haftmann@37458
   343
    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
haftmann@37458
   344
    by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
haftmann@37458
   345
  then show ?thesis by (simp add: updates_def expand_fun_eq)
haftmann@34975
   346
qed
haftmann@34975
   347
haftmann@34975
   348
lemma clearjunk_delete:
haftmann@34975
   349
  "clearjunk (delete x al) = delete x (clearjunk al)"
haftmann@34975
   350
  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
haftmann@34975
   351
haftmann@34975
   352
lemma clearjunk_restrict:
haftmann@34975
   353
 "clearjunk (restrict A al) = restrict A (clearjunk al)"
haftmann@34975
   354
  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
haftmann@34975
   355
haftmann@34975
   356
lemma distinct_clearjunk_id [simp]:
haftmann@34975
   357
  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
haftmann@34975
   358
  by (induct al rule: clearjunk.induct) auto
haftmann@34975
   359
haftmann@34975
   360
lemma clearjunk_idem:
haftmann@34975
   361
  "clearjunk (clearjunk al) = clearjunk al"
haftmann@34975
   362
  by simp
haftmann@34975
   363
haftmann@34975
   364
lemma length_clearjunk:
haftmann@34975
   365
  "length (clearjunk al) \<le> length al"
haftmann@34975
   366
proof (induct al rule: clearjunk.induct [case_names Nil Cons])
haftmann@34975
   367
  case Nil then show ?case by simp
haftmann@34975
   368
next
haftmann@34975
   369
  case (Cons kv al)
haftmann@34975
   370
  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
haftmann@34975
   371
  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
haftmann@34975
   372
  then show ?case by simp
haftmann@34975
   373
qed
haftmann@34975
   374
haftmann@34975
   375
lemma delete_map:
haftmann@34975
   376
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   377
  shows "delete k (map f ps) = map f (delete k ps)"
haftmann@34975
   378
  by (simp add: delete_eq filter_map comp_def split_def assms)
haftmann@34975
   379
haftmann@34975
   380
lemma clearjunk_map:
haftmann@34975
   381
  assumes "\<And>kv. fst (f kv) = fst kv"
haftmann@34975
   382
  shows "clearjunk (map f ps) = map f (clearjunk ps)"
haftmann@34975
   383
  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
haftmann@34975
   384
    (simp_all add: clearjunk_delete delete_map assms)
haftmann@34975
   385
haftmann@34975
   386
haftmann@34975
   387
subsection {* @{text map_ran} *}
haftmann@34975
   388
haftmann@34975
   389
definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   390
  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
haftmann@34975
   391
haftmann@34975
   392
lemma map_ran_simps [simp]:
haftmann@34975
   393
  "map_ran f [] = []"
haftmann@34975
   394
  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
haftmann@34975
   395
  by (simp_all add: map_ran_def)
haftmann@34975
   396
haftmann@34975
   397
lemma dom_map_ran:
haftmann@34975
   398
  "fst ` set (map_ran f al) = fst ` set al"
haftmann@34975
   399
  by (simp add: map_ran_def image_image split_def)
haftmann@34975
   400
  
haftmann@34975
   401
lemma map_ran_conv:
haftmann@34975
   402
  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
schirmer@19234
   403
  by (induct al) auto
schirmer@19234
   404
haftmann@34975
   405
lemma distinct_map_ran:
haftmann@34975
   406
  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
haftmann@34975
   407
  by (simp add: map_ran_def split_def comp_def)
schirmer@19234
   408
haftmann@34975
   409
lemma map_ran_filter:
haftmann@34975
   410
  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
haftmann@34975
   411
  by (simp add: map_ran_def filter_map split_def comp_def)
schirmer@19234
   412
haftmann@34975
   413
lemma clearjunk_map_ran:
haftmann@34975
   414
  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
haftmann@34975
   415
  by (simp add: map_ran_def split_def clearjunk_map)
schirmer@19234
   416
wenzelm@23373
   417
haftmann@34975
   418
subsection {* @{text merge} *}
haftmann@34975
   419
haftmann@34975
   420
definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
haftmann@34975
   421
  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
haftmann@34975
   422
haftmann@34975
   423
lemma merge_simps [simp]:
haftmann@34975
   424
  "merge qs [] = qs"
haftmann@34975
   425
  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
haftmann@34975
   426
  by (simp_all add: merge_def split_def)
haftmann@34975
   427
haftmann@34975
   428
lemma merge_updates:
haftmann@34975
   429
  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
haftmann@37591
   430
  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
schirmer@19234
   431
schirmer@19234
   432
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
wenzelm@20503
   433
  by (induct ys arbitrary: xs) (auto simp add: dom_update)
schirmer@19234
   434
schirmer@19234
   435
lemma distinct_merge:
schirmer@19234
   436
  assumes "distinct (map fst xs)"
schirmer@19234
   437
  shows "distinct (map fst (merge xs ys))"
haftmann@34975
   438
using assms by (simp add: merge_updates distinct_updates)
schirmer@19234
   439
schirmer@19234
   440
lemma clearjunk_merge:
haftmann@34975
   441
  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
haftmann@34975
   442
  by (simp add: merge_updates clearjunk_updates)
schirmer@19234
   443
haftmann@34975
   444
lemma merge_conv':
haftmann@34975
   445
  "map_of (merge xs ys) = map_of xs ++ map_of ys"
haftmann@34975
   446
proof -
haftmann@37458
   447
  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
haftmann@37458
   448
    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
haftmann@37458
   449
    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
haftmann@34975
   450
  then show ?thesis
haftmann@37591
   451
    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
schirmer@19234
   452
qed
schirmer@19234
   453
haftmann@34975
   454
corollary merge_conv:
haftmann@34975
   455
  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
haftmann@34975
   456
  by (simp add: merge_conv')
schirmer@19234
   457
haftmann@34975
   458
lemma merge_empty: "map_of (merge [] ys) = map_of ys"
schirmer@19234
   459
  by (simp add: merge_conv')
schirmer@19234
   460
schirmer@19234
   461
lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
schirmer@19234
   462
                           map_of (merge (merge m1 m2) m3)"
schirmer@19234
   463
  by (simp add: merge_conv')
schirmer@19234
   464
schirmer@19234
   465
lemma merge_Some_iff: 
schirmer@19234
   466
 "(map_of (merge m n) k = Some x) = 
schirmer@19234
   467
  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
schirmer@19234
   468
  by (simp add: merge_conv' map_add_Some_iff)
schirmer@19234
   469
haftmann@34975
   470
lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
schirmer@19234
   471
schirmer@19234
   472
lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
schirmer@19234
   473
  by (simp add: merge_conv')
schirmer@19234
   474
schirmer@19234
   475
lemma merge_None [iff]: 
schirmer@19234
   476
  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
schirmer@19234
   477
  by (simp add: merge_conv')
schirmer@19234
   478
schirmer@19234
   479
lemma merge_upd[simp]: 
schirmer@19234
   480
  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
schirmer@19234
   481
  by (simp add: update_conv' merge_conv')
schirmer@19234
   482
schirmer@19234
   483
lemma merge_updatess[simp]: 
schirmer@19234
   484
  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
schirmer@19234
   485
  by (simp add: updates_conv' merge_conv')
schirmer@19234
   486
schirmer@19234
   487
lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
schirmer@19234
   488
  by (simp add: merge_conv')
schirmer@19234
   489
wenzelm@23373
   490
haftmann@34975
   491
subsection {* @{text compose} *}
haftmann@34975
   492
haftmann@34975
   493
function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
haftmann@34975
   494
    "compose [] ys = []"
haftmann@34975
   495
  | "compose (x#xs) ys = (case map_of ys (snd x)
haftmann@34975
   496
       of None \<Rightarrow> compose (delete (fst x) xs) ys
haftmann@34975
   497
        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
haftmann@34975
   498
  by pat_completeness auto
haftmann@34975
   499
termination by (relation "measure (length \<circ> fst)")
haftmann@34975
   500
  (simp_all add: less_Suc_eq_le length_delete_le)
schirmer@19234
   501
schirmer@19234
   502
lemma compose_first_None [simp]: 
schirmer@19234
   503
  assumes "map_of xs k = None" 
schirmer@19234
   504
  shows "map_of (compose xs ys) k = None"
wenzelm@23373
   505
using assms by (induct xs ys rule: compose.induct)
haftmann@22916
   506
  (auto split: option.splits split_if_asm)
schirmer@19234
   507
schirmer@19234
   508
lemma compose_conv: 
schirmer@19234
   509
  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
haftmann@22916
   510
proof (induct xs ys rule: compose.induct)
haftmann@22916
   511
  case 1 then show ?case by simp
schirmer@19234
   512
next
haftmann@22916
   513
  case (2 x xs ys) show ?case
schirmer@19234
   514
  proof (cases "map_of ys (snd x)")
haftmann@22916
   515
    case None with 2
schirmer@19234
   516
    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
schirmer@19234
   517
               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
schirmer@19234
   518
      by simp
schirmer@19234
   519
    show ?thesis
schirmer@19234
   520
    proof (cases "fst x = k")
schirmer@19234
   521
      case True
schirmer@19234
   522
      from True delete_notin_dom [of k xs]
schirmer@19234
   523
      have "map_of (delete (fst x) xs) k = None"
wenzelm@32960
   524
        by (simp add: map_of_eq_None_iff)
schirmer@19234
   525
      with hyp show ?thesis
wenzelm@32960
   526
        using True None
wenzelm@32960
   527
        by simp
schirmer@19234
   528
    next
schirmer@19234
   529
      case False
schirmer@19234
   530
      from False have "map_of (delete (fst x) xs) k = map_of xs k"
wenzelm@32960
   531
        by simp
schirmer@19234
   532
      with hyp show ?thesis
wenzelm@32960
   533
        using False None
wenzelm@32960
   534
        by (simp add: map_comp_def)
schirmer@19234
   535
    qed
schirmer@19234
   536
  next
schirmer@19234
   537
    case (Some v)
haftmann@22916
   538
    with 2
schirmer@19234
   539
    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
schirmer@19234
   540
      by simp
schirmer@19234
   541
    with Some show ?thesis
schirmer@19234
   542
      by (auto simp add: map_comp_def)
schirmer@19234
   543
  qed
schirmer@19234
   544
qed
schirmer@19234
   545
   
schirmer@19234
   546
lemma compose_conv': 
schirmer@19234
   547
  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
schirmer@19234
   548
  by (rule ext) (rule compose_conv)
schirmer@19234
   549
schirmer@19234
   550
lemma compose_first_Some [simp]:
schirmer@19234
   551
  assumes "map_of xs k = Some v" 
schirmer@19234
   552
  shows "map_of (compose xs ys) k = map_of ys v"
wenzelm@23373
   553
using assms by (simp add: compose_conv)
schirmer@19234
   554
schirmer@19234
   555
lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
haftmann@22916
   556
proof (induct xs ys rule: compose.induct)
haftmann@22916
   557
  case 1 thus ?case by simp
schirmer@19234
   558
next
haftmann@22916
   559
  case (2 x xs ys)
schirmer@19234
   560
  show ?case
schirmer@19234
   561
  proof (cases "map_of ys (snd x)")
schirmer@19234
   562
    case None
haftmann@22916
   563
    with "2.hyps"
schirmer@19234
   564
    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
schirmer@19234
   565
      by simp
schirmer@19234
   566
    also
schirmer@19234
   567
    have "\<dots> \<subseteq> fst ` set xs"
schirmer@19234
   568
      by (rule dom_delete_subset)
schirmer@19234
   569
    finally show ?thesis
schirmer@19234
   570
      using None
schirmer@19234
   571
      by auto
schirmer@19234
   572
  next
schirmer@19234
   573
    case (Some v)
haftmann@22916
   574
    with "2.hyps"
schirmer@19234
   575
    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
schirmer@19234
   576
      by simp
schirmer@19234
   577
    with Some show ?thesis
schirmer@19234
   578
      by auto
schirmer@19234
   579
  qed
schirmer@19234
   580
qed
schirmer@19234
   581
schirmer@19234
   582
lemma distinct_compose:
schirmer@19234
   583
 assumes "distinct (map fst xs)"
schirmer@19234
   584
 shows "distinct (map fst (compose xs ys))"
wenzelm@23373
   585
using assms
haftmann@22916
   586
proof (induct xs ys rule: compose.induct)
haftmann@22916
   587
  case 1 thus ?case by simp
schirmer@19234
   588
next
haftmann@22916
   589
  case (2 x xs ys)
schirmer@19234
   590
  show ?case
schirmer@19234
   591
  proof (cases "map_of ys (snd x)")
schirmer@19234
   592
    case None
haftmann@22916
   593
    with 2 show ?thesis by simp
schirmer@19234
   594
  next
schirmer@19234
   595
    case (Some v)
haftmann@22916
   596
    with 2 dom_compose [of xs ys] show ?thesis 
schirmer@19234
   597
      by (auto)
schirmer@19234
   598
  qed
schirmer@19234
   599
qed
schirmer@19234
   600
schirmer@19234
   601
lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
haftmann@22916
   602
proof (induct xs ys rule: compose.induct)
haftmann@22916
   603
  case 1 thus ?case by simp
schirmer@19234
   604
next
haftmann@22916
   605
  case (2 x xs ys)
schirmer@19234
   606
  show ?case
schirmer@19234
   607
  proof (cases "map_of ys (snd x)")
schirmer@19234
   608
    case None
haftmann@22916
   609
    with 2 have 
schirmer@19234
   610
      hyp: "compose (delete k (delete (fst x) xs)) ys =
schirmer@19234
   611
            delete k (compose (delete (fst x) xs) ys)"
schirmer@19234
   612
      by simp
schirmer@19234
   613
    show ?thesis
schirmer@19234
   614
    proof (cases "fst x = k")
schirmer@19234
   615
      case True
schirmer@19234
   616
      with None hyp
schirmer@19234
   617
      show ?thesis
wenzelm@32960
   618
        by (simp add: delete_idem)
schirmer@19234
   619
    next
schirmer@19234
   620
      case False
schirmer@19234
   621
      from None False hyp
schirmer@19234
   622
      show ?thesis
wenzelm@32960
   623
        by (simp add: delete_twist)
schirmer@19234
   624
    qed
schirmer@19234
   625
  next
schirmer@19234
   626
    case (Some v)
haftmann@22916
   627
    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
schirmer@19234
   628
    with Some show ?thesis
schirmer@19234
   629
      by simp
schirmer@19234
   630
  qed
schirmer@19234
   631
qed
schirmer@19234
   632
schirmer@19234
   633
lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
haftmann@22916
   634
  by (induct xs ys rule: compose.induct) 
schirmer@19234
   635
     (auto simp add: map_of_clearjunk split: option.splits)
schirmer@19234
   636
   
schirmer@19234
   637
lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
schirmer@19234
   638
  by (induct xs rule: clearjunk.induct)
schirmer@19234
   639
     (auto split: option.splits simp add: clearjunk_delete delete_idem
schirmer@19234
   640
               compose_delete_twist)
schirmer@19234
   641
   
schirmer@19234
   642
lemma compose_empty [simp]:
schirmer@19234
   643
 "compose xs [] = []"
haftmann@22916
   644
  by (induct xs) (auto simp add: compose_delete_twist)
schirmer@19234
   645
schirmer@19234
   646
lemma compose_Some_iff:
schirmer@19234
   647
  "(map_of (compose xs ys) k = Some v) = 
schirmer@19234
   648
     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
schirmer@19234
   649
  by (simp add: compose_conv map_comp_Some_iff)
schirmer@19234
   650
schirmer@19234
   651
lemma map_comp_None_iff:
schirmer@19234
   652
  "(map_of (compose xs ys) k = None) = 
schirmer@19234
   653
    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
schirmer@19234
   654
  by (simp add: compose_conv map_comp_None_iff)
schirmer@19234
   655
haftmann@35156
   656
haftmann@35156
   657
subsection {* Implementation of mappings *}
haftmann@35156
   658
haftmann@36109
   659
definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
haftmann@36109
   660
  "Mapping xs = Mapping.Mapping (map_of xs)"
haftmann@35156
   661
haftmann@36109
   662
code_datatype Mapping
haftmann@35156
   663
haftmann@36109
   664
lemma lookup_Mapping [simp, code]:
haftmann@36109
   665
  "Mapping.lookup (Mapping xs) = map_of xs"
haftmann@36109
   666
  by (simp add: Mapping_def)
haftmann@35156
   667
haftmann@37051
   668
lemma keys_Mapping [simp, code]:
haftmann@37051
   669
  "Mapping.keys (Mapping xs) = set (map fst xs)"
haftmann@37051
   670
  by (simp add: keys_def dom_map_of_conv_image_fst)
haftmann@37051
   671
haftmann@36109
   672
lemma empty_Mapping [code]:
haftmann@36109
   673
  "Mapping.empty = Mapping []"
haftmann@35156
   674
  by (rule mapping_eqI) simp
haftmann@35156
   675
haftmann@36109
   676
lemma is_empty_Mapping [code]:
haftmann@37595
   677
  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
haftmann@37595
   678
  by (cases xs) (simp_all add: is_empty_def null_def)
haftmann@35156
   679
haftmann@36109
   680
lemma update_Mapping [code]:
haftmann@36109
   681
  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
haftmann@35156
   682
  by (rule mapping_eqI) (simp add: update_conv')
haftmann@35156
   683
haftmann@36109
   684
lemma delete_Mapping [code]:
haftmann@36109
   685
  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
haftmann@35156
   686
  by (rule mapping_eqI) (simp add: delete_conv')
haftmann@35156
   687
haftmann@36109
   688
lemma ordered_keys_Mapping [code]:
haftmann@36109
   689
  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
haftmann@37051
   690
  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
haftmann@35194
   691
haftmann@36109
   692
lemma size_Mapping [code]:
haftmann@36109
   693
  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
haftmann@35156
   694
  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
haftmann@35156
   695
haftmann@36109
   696
lemma tabulate_Mapping [code]:
haftmann@36109
   697
  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
haftmann@35156
   698
  by (rule mapping_eqI) (simp add: map_of_map_restrict)
haftmann@35156
   699
haftmann@36109
   700
lemma bulkload_Mapping [code]:
haftmann@36109
   701
  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
haftmann@35156
   702
  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
haftmann@35156
   703
haftmann@37051
   704
lemma [code, code del]:
haftmann@37051
   705
  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
haftmann@37051
   706
schirmer@19234
   707
end