src/HOL/Library/DAList.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63684 905d3fc815ff
child 67091 1393c2340eec
permissions -rw-r--r--
tuned proofs;
bulwahn@46237
     1
(*  Title:      HOL/Library/DAList.thy
wenzelm@58806
     2
    Author:     Lukas Bulwahn, TU Muenchen
wenzelm@58806
     3
*)
bulwahn@46167
     4
wenzelm@58881
     5
section \<open>Abstract type of association lists with unique keys\<close>
bulwahn@46167
     6
bulwahn@46237
     7
theory DAList
bulwahn@46238
     8
imports AList
bulwahn@46167
     9
begin
bulwahn@46167
    10
wenzelm@58806
    11
text \<open>This was based on some existing fragments in the AFP-Collection framework.\<close>
bulwahn@46167
    12
wenzelm@58806
    13
subsection \<open>Preliminaries\<close>
bulwahn@47143
    14
bulwahn@47143
    15
lemma distinct_map_fst_filter:
wenzelm@58806
    16
  "distinct (map fst xs) \<Longrightarrow> distinct (map fst (List.filter P xs))"
wenzelm@58806
    17
  by (induct xs) auto
wenzelm@58806
    18
bulwahn@47143
    19
wenzelm@61585
    20
subsection \<open>Type \<open>('key, 'value) alist\<close>\<close>
bulwahn@46167
    21
wenzelm@58806
    22
typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
wenzelm@46507
    23
  morphisms impl_of Alist
wenzelm@46507
    24
proof
wenzelm@58806
    25
  show "[] \<in> {xs. (distinct o map fst) xs}"
wenzelm@58806
    26
    by simp
wenzelm@46507
    27
qed
bulwahn@46167
    28
bulwahn@47143
    29
setup_lifting type_definition_alist
bulwahn@47143
    30
bulwahn@46167
    31
lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
wenzelm@58806
    32
  by (simp add: impl_of_inject)
bulwahn@46167
    33
bulwahn@46167
    34
lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
wenzelm@58806
    35
  by (simp add: impl_of_inject)
bulwahn@46167
    36
bulwahn@46167
    37
lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
wenzelm@58806
    38
  using impl_of[of xs] by simp
bulwahn@46167
    39
bulwahn@46167
    40
lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
wenzelm@58806
    41
  by (rule impl_of_inverse)
bulwahn@46167
    42
wenzelm@58806
    43
wenzelm@58806
    44
subsection \<open>Primitive operations\<close>
bulwahn@46167
    45
kuncar@55565
    46
lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  .
bulwahn@46167
    47
wenzelm@58806
    48
lift_definition empty :: "('key, 'value) alist" is "[]"
wenzelm@58806
    49
  by simp
bulwahn@46167
    50
kuncar@47308
    51
lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308
    52
  is AList.update
wenzelm@58806
    53
  by (simp add: distinct_update)
bulwahn@46167
    54
bulwahn@46167
    55
(* FIXME: we use an unoptimised delete operation. *)
kuncar@47308
    56
lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308
    57
  is AList.delete
wenzelm@58806
    58
  by (simp add: distinct_delete)
bulwahn@46167
    59
wenzelm@58806
    60
lift_definition map_entry ::
wenzelm@58806
    61
    "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308
    62
  is AList.map_entry
wenzelm@58806
    63
  by (simp add: distinct_map_entry)
bulwahn@46167
    64
kuncar@47308
    65
lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308
    66
  is List.filter
wenzelm@58806
    67
  by (simp add: distinct_map_fst_filter)
bulwahn@46167
    68
wenzelm@58806
    69
lift_definition map_default ::
wenzelm@58806
    70
    "'key \<Rightarrow> 'value \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
kuncar@47308
    71
  is AList.map_default
wenzelm@58806
    72
  by (simp add: distinct_map_default)
bulwahn@46167
    73
wenzelm@58806
    74
wenzelm@58806
    75
subsection \<open>Abstract operation properties\<close>
bulwahn@46167
    76
bulwahn@46167
    77
(* FIXME: to be completed *)
bulwahn@46167
    78
bulwahn@46167
    79
lemma lookup_empty [simp]: "lookup empty k = None"
nipkow@63684
    80
by (simp add: empty_def lookup_def Alist_inverse)
nipkow@63684
    81
nipkow@63684
    82
lemma lookup_update:
nipkow@63684
    83
  "lookup (update k1 v xs) k2 = (if k1 = k2 then Some v else lookup xs k2)"
nipkow@63684
    84
by(transfer)(simp add: update_conv')
nipkow@63684
    85
nipkow@63684
    86
lemma lookup_update_eq [simp]:
nipkow@63684
    87
  "k1 = k2 \<Longrightarrow> lookup (update k1 v xs) k2 = Some v"
nipkow@63684
    88
by(simp add: lookup_update)
nipkow@63684
    89
nipkow@63684
    90
lemma lookup_update_neq [simp]:
nipkow@63684
    91
  "k1 \<noteq> k2 \<Longrightarrow> lookup (update k1 v xs) k2 = lookup xs k2"
nipkow@63684
    92
by(simp add: lookup_update)
nipkow@63684
    93
nipkow@63684
    94
lemma update_update_eq [simp]:
nipkow@63684
    95
  "k1 = k2 \<Longrightarrow> update k2 v2 (update k1 v1 xs) = update k2 v2 xs"
nipkow@63684
    96
by(transfer)(simp add: update_conv')
bulwahn@46167
    97
bulwahn@46167
    98
lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
wenzelm@58806
    99
  by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
bulwahn@46167
   100
wenzelm@58806
   101
wenzelm@58806
   102
subsection \<open>Further operations\<close>
bulwahn@46167
   103
wenzelm@58806
   104
subsubsection \<open>Equality\<close>
bulwahn@46167
   105
wenzelm@58806
   106
instantiation alist :: (equal, equal) equal
wenzelm@58806
   107
begin
bulwahn@46167
   108
bulwahn@46167
   109
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
bulwahn@46167
   110
bulwahn@46167
   111
instance
wenzelm@60679
   112
  by standard (simp add: equal_alist_def impl_of_inject)
bulwahn@46167
   113
bulwahn@46167
   114
end
bulwahn@46167
   115
wenzelm@58806
   116
wenzelm@58806
   117
subsubsection \<open>Size\<close>
bulwahn@46167
   118
wenzelm@58806
   119
instantiation alist :: (type, type) size
wenzelm@58806
   120
begin
bulwahn@46167
   121
bulwahn@46167
   122
definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
bulwahn@46167
   123
bulwahn@46167
   124
instance ..
bulwahn@46167
   125
bulwahn@46167
   126
end
bulwahn@46167
   127
wenzelm@58806
   128
wenzelm@58806
   129
subsection \<open>Quickcheck generators\<close>
bulwahn@46167
   130
bulwahn@46167
   131
notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   132
notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   133
bulwahn@46167
   134
definition (in term_syntax)
bulwahn@46167
   135
  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
wenzelm@58806
   136
  where "valterm_empty = Code_Evaluation.valtermify empty"
bulwahn@46167
   137
bulwahn@46167
   138
definition (in term_syntax)
bulwahn@46167
   139
  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   140
  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   141
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   142
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
bulwahn@46167
   143
  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
bulwahn@46167
   144
wenzelm@58806
   145
fun (in term_syntax) random_aux_alist
bulwahn@46167
   146
where
wenzelm@58806
   147
  "random_aux_alist i j =
wenzelm@58806
   148
    (if i = 0 then Pair valterm_empty
wenzelm@58806
   149
     else Quickcheck_Random.collapse
wenzelm@58806
   150
       (Random.select_weight
wenzelm@58806
   151
         [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow>
wenzelm@58806
   152
           (\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
wenzelm@58806
   153
          (1, Pair valterm_empty)]))"
bulwahn@46167
   154
bulwahn@46167
   155
instantiation alist :: (random, random) random
bulwahn@46167
   156
begin
bulwahn@46167
   157
bulwahn@46167
   158
definition random_alist
bulwahn@46167
   159
where
bulwahn@46167
   160
  "random_alist i = random_aux_alist i i"
wenzelm@58806
   161
bulwahn@46167
   162
instance ..
bulwahn@46167
   163
bulwahn@46167
   164
end
bulwahn@46167
   165
bulwahn@46167
   166
no_notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   167
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   168
bulwahn@46167
   169
instantiation alist :: (exhaustive, exhaustive) exhaustive
bulwahn@46167
   170
begin
bulwahn@46167
   171
wenzelm@58806
   172
fun exhaustive_alist ::
wenzelm@58806
   173
  "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
bulwahn@46167
   174
where
wenzelm@58806
   175
  "exhaustive_alist f i =
wenzelm@58806
   176
    (if i = 0 then None
wenzelm@58806
   177
     else
wenzelm@58806
   178
      case f empty of
wenzelm@58806
   179
        Some ts \<Rightarrow> Some ts
wenzelm@58806
   180
      | None \<Rightarrow>
wenzelm@58806
   181
          exhaustive_alist
wenzelm@58806
   182
            (\<lambda>a. Quickcheck_Exhaustive.exhaustive
wenzelm@58806
   183
              (\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1))
wenzelm@58806
   184
            (i - 1))"
bulwahn@46167
   185
bulwahn@46167
   186
instance ..
bulwahn@46167
   187
bulwahn@46167
   188
end
bulwahn@46167
   189
bulwahn@46167
   190
instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
bulwahn@46167
   191
begin
bulwahn@46167
   192
wenzelm@58806
   193
fun full_exhaustive_alist ::
wenzelm@58806
   194
  "(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow>
wenzelm@58806
   195
    (bool \<times> term list) option"
bulwahn@46167
   196
where
wenzelm@58806
   197
  "full_exhaustive_alist f i =
wenzelm@58806
   198
    (if i = 0 then None
wenzelm@58806
   199
     else
wenzelm@58806
   200
      case f valterm_empty of
wenzelm@58806
   201
        Some ts \<Rightarrow> Some ts
wenzelm@58806
   202
      | None \<Rightarrow>
wenzelm@58806
   203
          full_exhaustive_alist
wenzelm@58806
   204
            (\<lambda>a.
wenzelm@58806
   205
              Quickcheck_Exhaustive.full_exhaustive
wenzelm@58806
   206
                (\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1))
wenzelm@58806
   207
              (i - 1))
wenzelm@58806
   208
            (i - 1))"
bulwahn@46167
   209
bulwahn@46167
   210
instance ..
bulwahn@46167
   211
bulwahn@46167
   212
end
bulwahn@46167
   213
traytel@59581
   214
traytel@59581
   215
section \<open>alist is a BNF\<close>
traytel@59581
   216
traytel@60919
   217
lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel
traytel@60919
   218
  by auto
traytel@59581
   219
bulwahn@46167
   220
hide_const valterm_empty valterm_update random_aux_alist
bulwahn@46167
   221
bulwahn@46171
   222
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
traytel@59581
   223
hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
bulwahn@46167
   224
bulwahn@46238
   225
end