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