src/HOL/Library/DAList.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60919 b0ba7799d05a
child 61585 a9599d3d7610
permissions -rw-r--r--
tuned references
     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 @{text "('key, 'value) alist" }\<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 o 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_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    83   by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    84 
    85 
    86 subsection \<open>Further operations\<close>
    87 
    88 subsubsection \<open>Equality\<close>
    89 
    90 instantiation alist :: (equal, equal) equal
    91 begin
    92 
    93 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
    94 
    95 instance
    96   by standard (simp add: equal_alist_def impl_of_inject)
    97 
    98 end
    99 
   100 
   101 subsubsection \<open>Size\<close>
   102 
   103 instantiation alist :: (type, type) size
   104 begin
   105 
   106 definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
   107 
   108 instance ..
   109 
   110 end
   111 
   112 
   113 subsection \<open>Quickcheck generators\<close>
   114 
   115 notation fcomp (infixl "\<circ>>" 60)
   116 notation scomp (infixl "\<circ>\<rightarrow>" 60)
   117 
   118 definition (in term_syntax)
   119   valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   120   where "valterm_empty = Code_Evaluation.valtermify empty"
   121 
   122 definition (in term_syntax)
   123   valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   124   'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   125   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   126   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   127   [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   128 
   129 fun (in term_syntax) random_aux_alist
   130 where
   131   "random_aux_alist i j =
   132     (if i = 0 then Pair valterm_empty
   133      else Quickcheck_Random.collapse
   134        (Random.select_weight
   135          [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow>
   136            (\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))),
   137           (1, Pair valterm_empty)]))"
   138 
   139 instantiation alist :: (random, random) random
   140 begin
   141 
   142 definition random_alist
   143 where
   144   "random_alist i = random_aux_alist i i"
   145 
   146 instance ..
   147 
   148 end
   149 
   150 no_notation fcomp (infixl "\<circ>>" 60)
   151 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   152 
   153 instantiation alist :: (exhaustive, exhaustive) exhaustive
   154 begin
   155 
   156 fun exhaustive_alist ::
   157   "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   158 where
   159   "exhaustive_alist f i =
   160     (if i = 0 then None
   161      else
   162       case f empty of
   163         Some ts \<Rightarrow> Some ts
   164       | None \<Rightarrow>
   165           exhaustive_alist
   166             (\<lambda>a. Quickcheck_Exhaustive.exhaustive
   167               (\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1))
   168             (i - 1))"
   169 
   170 instance ..
   171 
   172 end
   173 
   174 instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   175 begin
   176 
   177 fun full_exhaustive_alist ::
   178   "(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow>
   179     (bool \<times> term list) option"
   180 where
   181   "full_exhaustive_alist f i =
   182     (if i = 0 then None
   183      else
   184       case f valterm_empty of
   185         Some ts \<Rightarrow> Some ts
   186       | None \<Rightarrow>
   187           full_exhaustive_alist
   188             (\<lambda>a.
   189               Quickcheck_Exhaustive.full_exhaustive
   190                 (\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1))
   191               (i - 1))
   192             (i - 1))"
   193 
   194 instance ..
   195 
   196 end
   197 
   198 
   199 section \<open>alist is a BNF\<close>
   200 
   201 lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel
   202   by auto
   203 
   204 hide_const valterm_empty valterm_update random_aux_alist
   205 
   206 hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   207 hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
   208 
   209 end