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