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