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