src/HOL/Library/DAList.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63684 905d3fc815ff
child 67091 1393c2340eec
permissions -rw-r--r--
executable domain membership checks
     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 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_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