src/HOL/Library/DAList.thy
author wenzelm
Mon Jul 06 22:57:34 2015 +0200 (2015-07-06)
changeset 60679 ade12ef2773c
parent 59581 09722854b8f4
child 60919 b0ba7799d05a
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@58806
    20
subsection \<open>Type @{text "('key, 'value) alist" }\<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"
wenzelm@58806
    80
  by (simp add: empty_def lookup_def Alist_inverse)
bulwahn@46167
    81
bulwahn@46167
    82
lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
wenzelm@58806
    83
  by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
bulwahn@46167
    84
wenzelm@58806
    85
wenzelm@58806
    86
subsection \<open>Further operations\<close>
bulwahn@46167
    87
wenzelm@58806
    88
subsubsection \<open>Equality\<close>
bulwahn@46167
    89
wenzelm@58806
    90
instantiation alist :: (equal, equal) equal
wenzelm@58806
    91
begin
bulwahn@46167
    92
bulwahn@46167
    93
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
bulwahn@46167
    94
bulwahn@46167
    95
instance
wenzelm@60679
    96
  by standard (simp add: equal_alist_def impl_of_inject)
bulwahn@46167
    97
bulwahn@46167
    98
end
bulwahn@46167
    99
wenzelm@58806
   100
wenzelm@58806
   101
subsubsection \<open>Size\<close>
bulwahn@46167
   102
wenzelm@58806
   103
instantiation alist :: (type, type) size
wenzelm@58806
   104
begin
bulwahn@46167
   105
bulwahn@46167
   106
definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
bulwahn@46167
   107
bulwahn@46167
   108
instance ..
bulwahn@46167
   109
bulwahn@46167
   110
end
bulwahn@46167
   111
wenzelm@58806
   112
wenzelm@58806
   113
subsection \<open>Quickcheck generators\<close>
bulwahn@46167
   114
bulwahn@46167
   115
notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   116
notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   117
bulwahn@46167
   118
definition (in term_syntax)
bulwahn@46167
   119
  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
wenzelm@58806
   120
  where "valterm_empty = Code_Evaluation.valtermify empty"
bulwahn@46167
   121
bulwahn@46167
   122
definition (in term_syntax)
bulwahn@46167
   123
  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   124
  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   125
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   126
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
bulwahn@46167
   127
  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
bulwahn@46167
   128
wenzelm@58806
   129
fun (in term_syntax) random_aux_alist
bulwahn@46167
   130
where
wenzelm@58806
   131
  "random_aux_alist i j =
wenzelm@58806
   132
    (if i = 0 then Pair valterm_empty
wenzelm@58806
   133
     else Quickcheck_Random.collapse
wenzelm@58806
   134
       (Random.select_weight
wenzelm@58806
   135
         [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow>
wenzelm@58806
   136
           (\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
wenzelm@58806
   137
          (1, Pair valterm_empty)]))"
bulwahn@46167
   138
bulwahn@46167
   139
instantiation alist :: (random, random) random
bulwahn@46167
   140
begin
bulwahn@46167
   141
bulwahn@46167
   142
definition random_alist
bulwahn@46167
   143
where
bulwahn@46167
   144
  "random_alist i = random_aux_alist i i"
wenzelm@58806
   145
bulwahn@46167
   146
instance ..
bulwahn@46167
   147
bulwahn@46167
   148
end
bulwahn@46167
   149
bulwahn@46167
   150
no_notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   151
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   152
bulwahn@46167
   153
instantiation alist :: (exhaustive, exhaustive) exhaustive
bulwahn@46167
   154
begin
bulwahn@46167
   155
wenzelm@58806
   156
fun exhaustive_alist ::
wenzelm@58806
   157
  "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
bulwahn@46167
   158
where
wenzelm@58806
   159
  "exhaustive_alist f i =
wenzelm@58806
   160
    (if i = 0 then None
wenzelm@58806
   161
     else
wenzelm@58806
   162
      case f empty of
wenzelm@58806
   163
        Some ts \<Rightarrow> Some ts
wenzelm@58806
   164
      | None \<Rightarrow>
wenzelm@58806
   165
          exhaustive_alist
wenzelm@58806
   166
            (\<lambda>a. Quickcheck_Exhaustive.exhaustive
wenzelm@58806
   167
              (\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1))
wenzelm@58806
   168
            (i - 1))"
bulwahn@46167
   169
bulwahn@46167
   170
instance ..
bulwahn@46167
   171
bulwahn@46167
   172
end
bulwahn@46167
   173
bulwahn@46167
   174
instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
bulwahn@46167
   175
begin
bulwahn@46167
   176
wenzelm@58806
   177
fun full_exhaustive_alist ::
wenzelm@58806
   178
  "(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow>
wenzelm@58806
   179
    (bool \<times> term list) option"
bulwahn@46167
   180
where
wenzelm@58806
   181
  "full_exhaustive_alist f i =
wenzelm@58806
   182
    (if i = 0 then None
wenzelm@58806
   183
     else
wenzelm@58806
   184
      case f valterm_empty of
wenzelm@58806
   185
        Some ts \<Rightarrow> Some ts
wenzelm@58806
   186
      | None \<Rightarrow>
wenzelm@58806
   187
          full_exhaustive_alist
wenzelm@58806
   188
            (\<lambda>a.
wenzelm@58806
   189
              Quickcheck_Exhaustive.full_exhaustive
wenzelm@58806
   190
                (\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1))
wenzelm@58806
   191
              (i - 1))
wenzelm@58806
   192
            (i - 1))"
bulwahn@46167
   193
bulwahn@46167
   194
instance ..
bulwahn@46167
   195
bulwahn@46167
   196
end
bulwahn@46167
   197
traytel@59581
   198
traytel@59581
   199
section \<open>alist is a BNF\<close>
traytel@59581
   200
traytel@59581
   201
lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('k, 'a) alist \<Rightarrow> ('k, 'b) alist"
traytel@59581
   202
  is "\<lambda>f xs. List.map (map_prod id f) xs" by simp
traytel@59581
   203
traytel@59581
   204
lift_definition set :: "('k, 'v) alist => 'v set"
traytel@59581
   205
  is "\<lambda>xs. snd ` List.set xs" .
traytel@59581
   206
traytel@59581
   207
lift_definition rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('k, 'a) alist \<Rightarrow> ('k, 'b) alist \<Rightarrow> bool"
traytel@59581
   208
  is "\<lambda>R xs ys. list_all2 (rel_prod op = R) xs ys" .
traytel@59581
   209
traytel@59581
   210
bnf "('k, 'v) alist"
traytel@59581
   211
  map: map
traytel@59581
   212
  sets: set
traytel@59581
   213
  bd: natLeq
traytel@59581
   214
  wits: empty
traytel@59581
   215
  rel: rel
traytel@59581
   216
proof (unfold OO_Grp_alt)
traytel@59581
   217
  show "map id = id" by (rule ext, transfer) (simp add: prod.map_id0)
traytel@59581
   218
next
traytel@59581
   219
  fix f g
traytel@59581
   220
  show "map (g \<circ> f) = map g \<circ> map f"
traytel@59581
   221
    by (rule ext, transfer) (simp add: prod.map_comp)
traytel@59581
   222
next
traytel@59581
   223
  fix x f g
traytel@59581
   224
  assume "(\<And>z. z \<in> set x \<Longrightarrow> f z = g z)"
traytel@59581
   225
  then show "map f x = map g x" by transfer force
traytel@59581
   226
next
traytel@59581
   227
  fix f
traytel@59581
   228
  show "set \<circ> map f = op ` f \<circ> set"
traytel@59581
   229
    by (rule ext, transfer) (simp add: image_image)
traytel@59581
   230
next
traytel@59581
   231
  fix x
traytel@59581
   232
  show "ordLeq3 (card_of (set x)) natLeq"
traytel@59581
   233
    by transfer (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
traytel@59581
   234
next
traytel@59581
   235
  fix R S
traytel@59581
   236
  show "rel R OO rel S \<le> rel (R OO S)"
traytel@59581
   237
    by (rule predicate2I, transfer)
traytel@59581
   238
      (auto simp: list.rel_compp prod.rel_compp[of "op =", unfolded eq_OO])
traytel@59581
   239
next
traytel@59581
   240
  fix R
traytel@59581
   241
  show "rel R = (\<lambda>x y. \<exists>z. z \<in> {x. set x \<subseteq> {(x, y). R x y}} \<and> map fst z = x \<and> map snd z = y)"
traytel@59581
   242
   unfolding fun_eq_iff by transfer (fastforce simp: list.in_rel o_def intro:
traytel@59581
   243
     exI[of _ "List.map (\<lambda>p. ((fst p, fst (snd p)), (fst p, snd (snd p)))) z" for z]
traytel@59581
   244
     exI[of _ "List.map (\<lambda>p. (fst (fst p), snd (fst p), snd (snd p))) z" for z])
traytel@59581
   245
next
traytel@59581
   246
  fix z assume "z \<in> set empty"
traytel@59581
   247
  then show False by transfer simp
traytel@59581
   248
qed (simp_all add: natLeq_cinfinite natLeq_card_order)
traytel@59581
   249
bulwahn@46167
   250
hide_const valterm_empty valterm_update random_aux_alist
bulwahn@46167
   251
bulwahn@46171
   252
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
traytel@59581
   253
hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
bulwahn@46167
   254
bulwahn@46238
   255
end