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