src/HOL/Library/DAList.thy
author bulwahn
Tue Mar 27 14:14:46 2012 +0200 (2012-03-27)
changeset 47143 212f7a975d49
parent 46507 1b24c24017dd
child 47178 2ae2b6fa9c84
permissions -rw-r--r--
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
added remarks about further improvements
bulwahn@46237
     1
(*  Title:      HOL/Library/DAList.thy
bulwahn@46167
     2
    Author:     Lukas Bulwahn, TU Muenchen *)
bulwahn@46167
     3
bulwahn@46167
     4
header {* Abstract type of association lists with unique keys *}
bulwahn@46167
     5
bulwahn@46237
     6
theory DAList
bulwahn@46238
     7
imports AList
bulwahn@46167
     8
begin
bulwahn@46167
     9
bulwahn@46167
    10
text {* This was based on some existing fragments in the AFP-Collection framework. *}
bulwahn@46167
    11
bulwahn@47143
    12
subsection {* Preliminaries *}
bulwahn@47143
    13
bulwahn@47143
    14
lemma distinct_map_fst_filter:
bulwahn@47143
    15
   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
bulwahn@47143
    16
by (induct xs) auto
bulwahn@47143
    17
bulwahn@46167
    18
subsection {* Type @{text "('key, 'value) alist" } *}
bulwahn@46167
    19
bulwahn@47143
    20
typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
wenzelm@46507
    21
  morphisms impl_of Alist
wenzelm@46507
    22
proof
bulwahn@47143
    23
  show "[] \<in> {xs. (distinct o map fst) xs}" by simp
wenzelm@46507
    24
qed
bulwahn@46167
    25
bulwahn@47143
    26
setup_lifting type_definition_alist
bulwahn@47143
    27
bulwahn@46167
    28
lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
bulwahn@46167
    29
by(simp add: impl_of_inject)
bulwahn@46167
    30
bulwahn@46167
    31
lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
bulwahn@46167
    32
by(simp add: impl_of_inject)
bulwahn@46167
    33
bulwahn@46167
    34
lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
bulwahn@46167
    35
using impl_of[of xs] by simp
bulwahn@46167
    36
bulwahn@46167
    37
lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
bulwahn@46167
    38
by(rule impl_of_inverse)
bulwahn@46167
    39
bulwahn@46167
    40
subsection {* Primitive operations *}
bulwahn@46167
    41
bulwahn@47143
    42
(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) 
bulwahn@47143
    43
bulwahn@47143
    44
quotient_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
bulwahn@47143
    45
where "lookup" is "map_of :: ('key * 'value) list \<Rightarrow> 'key \<Rightarrow> 'value option" ..
bulwahn@46167
    46
bulwahn@47143
    47
quotient_definition empty :: "('key, 'value) alist"
bulwahn@47143
    48
where "empty" is "[] :: ('key * 'value) list" by simp
bulwahn@46167
    49
bulwahn@47143
    50
quotient_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
bulwahn@47143
    51
where "update" is "AList.update :: 'key \<Rightarrow> 'value \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
bulwahn@47143
    52
by (simp add: distinct_update)
bulwahn@46167
    53
bulwahn@46167
    54
(* FIXME: we use an unoptimised delete operation. *)
bulwahn@47143
    55
quotient_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
bulwahn@47143
    56
where "delete" is "AList.delete :: 'key \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
bulwahn@47143
    57
by (simp add: distinct_delete)
bulwahn@46167
    58
bulwahn@47143
    59
quotient_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
bulwahn@47143
    60
where "map_entry" is "AList.map_entry :: 'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
bulwahn@47143
    61
by (simp add: distinct_map_entry)
bulwahn@46167
    62
bulwahn@47143
    63
quotient_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
bulwahn@47143
    64
where "filter" is "List.filter :: ('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
bulwahn@47143
    65
by (simp add: distinct_map_fst_filter)
bulwahn@46167
    66
bulwahn@47143
    67
quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
bulwahn@47143
    68
where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
bulwahn@47143
    69
by (simp add: distinct_map_default)
bulwahn@46167
    70
bulwahn@47143
    71
(* FIXME: theorems are still used in Multiset; make code certificates available to the user *)
bulwahn@47143
    72
lemma impl_of_empty: "impl_of empty = []"
bulwahn@46167
    73
by (simp add: empty_def Alist_inverse)
bulwahn@46167
    74
bulwahn@47143
    75
lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
bulwahn@46167
    76
by (simp add: update_def Alist_inverse distinct_update)
bulwahn@46167
    77
bulwahn@47143
    78
lemma impl_of_filter:
bulwahn@46167
    79
  "impl_of (filter P xs) = List.filter P (impl_of xs)"
bulwahn@46167
    80
unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
bulwahn@46167
    81
bulwahn@46167
    82
subsection {* Abstract operation properties *}
bulwahn@46167
    83
bulwahn@46167
    84
(* FIXME: to be completed *)
bulwahn@46167
    85
bulwahn@46167
    86
lemma lookup_empty [simp]: "lookup empty k = None"
bulwahn@46167
    87
by(simp add: empty_def lookup_def Alist_inverse)
bulwahn@46167
    88
bulwahn@46167
    89
lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
bulwahn@46167
    90
by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
bulwahn@46167
    91
bulwahn@46167
    92
subsection {* Further operations *}
bulwahn@46167
    93
bulwahn@46167
    94
subsubsection {* Equality *}
bulwahn@46167
    95
bulwahn@46167
    96
instantiation alist :: (equal, equal) equal begin
bulwahn@46167
    97
bulwahn@46167
    98
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
bulwahn@46167
    99
bulwahn@46167
   100
instance
bulwahn@46167
   101
proof
bulwahn@46167
   102
qed (simp add: equal_alist_def impl_of_inject)
bulwahn@46167
   103
bulwahn@46167
   104
end
bulwahn@46167
   105
bulwahn@46167
   106
subsubsection {* Size *}
bulwahn@46167
   107
bulwahn@46167
   108
instantiation alist :: (type, type) size begin
bulwahn@46167
   109
bulwahn@46167
   110
definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
bulwahn@46167
   111
bulwahn@46167
   112
instance ..
bulwahn@46167
   113
bulwahn@46167
   114
end
bulwahn@46167
   115
bulwahn@46167
   116
subsection {* Quickcheck generators *}
bulwahn@46167
   117
bulwahn@46167
   118
notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   119
notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   120
bulwahn@46167
   121
definition (in term_syntax)
bulwahn@46167
   122
  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
bulwahn@46167
   123
where
bulwahn@46167
   124
  "valterm_empty = Code_Evaluation.valtermify empty"
bulwahn@46167
   125
bulwahn@46167
   126
definition (in term_syntax)
bulwahn@46167
   127
  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   128
  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   129
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
bulwahn@46167
   130
  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
bulwahn@46167
   131
  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
bulwahn@46167
   132
bulwahn@46167
   133
fun (in term_syntax) random_aux_alist 
bulwahn@46167
   134
where
bulwahn@46167
   135
  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
bulwahn@46167
   136
bulwahn@46167
   137
instantiation alist :: (random, random) random
bulwahn@46167
   138
begin
bulwahn@46167
   139
bulwahn@46167
   140
definition random_alist
bulwahn@46167
   141
where
bulwahn@46167
   142
  "random_alist i = random_aux_alist i i"
bulwahn@46167
   143
 
bulwahn@46167
   144
instance ..
bulwahn@46167
   145
bulwahn@46167
   146
end
bulwahn@46167
   147
bulwahn@46167
   148
no_notation fcomp (infixl "\<circ>>" 60)
bulwahn@46167
   149
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@46167
   150
bulwahn@46167
   151
instantiation alist :: (exhaustive, exhaustive) exhaustive
bulwahn@46167
   152
begin
bulwahn@46167
   153
bulwahn@46167
   154
fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
bulwahn@46167
   155
where
bulwahn@46167
   156
  "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
bulwahn@46167
   157
     exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
bulwahn@46167
   158
bulwahn@46167
   159
instance ..
bulwahn@46167
   160
bulwahn@46167
   161
end
bulwahn@46167
   162
bulwahn@46167
   163
instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
bulwahn@46167
   164
begin
bulwahn@46167
   165
bulwahn@46167
   166
fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
bulwahn@46167
   167
where
bulwahn@46167
   168
  "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
bulwahn@46167
   169
     full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))"
bulwahn@46167
   170
bulwahn@46167
   171
instance ..
bulwahn@46167
   172
bulwahn@46167
   173
end
bulwahn@46167
   174
bulwahn@46167
   175
hide_const valterm_empty valterm_update random_aux_alist
bulwahn@46167
   176
bulwahn@46171
   177
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
bulwahn@46167
   178
hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
bulwahn@46167
   179
bulwahn@46238
   180
end