src/HOL/Library/DAList.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 47308 9caab698dbe4
child 49834 b27bbb021df1
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
     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 lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  ..
    43 
    44 lift_definition empty :: "('key, 'value) alist" is "[]" by simp
    45 
    46 lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    47   is AList.update
    48 by (simp add: distinct_update)
    49 
    50 (* FIXME: we use an unoptimised delete operation. *)
    51 lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    52   is AList.delete
    53 by (simp add: distinct_delete)
    54 
    55 lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    56   is AList.map_entry
    57 by (simp add: distinct_map_entry)
    58 
    59 lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    60   is List.filter
    61 by (simp add: distinct_map_fst_filter)
    62 
    63 lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    64   is AList.map_default
    65 by (simp add: distinct_map_default)
    66 
    67 subsection {* Abstract operation properties *}
    68 
    69 (* FIXME: to be completed *)
    70 
    71 lemma lookup_empty [simp]: "lookup empty k = None"
    72 by(simp add: empty_def lookup_def Alist_inverse)
    73 
    74 lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    75 by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    76 
    77 subsection {* Further operations *}
    78 
    79 subsubsection {* Equality *}
    80 
    81 instantiation alist :: (equal, equal) equal begin
    82 
    83 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
    84 
    85 instance
    86 proof
    87 qed (simp add: equal_alist_def impl_of_inject)
    88 
    89 end
    90 
    91 subsubsection {* Size *}
    92 
    93 instantiation alist :: (type, type) size begin
    94 
    95 definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
    96 
    97 instance ..
    98 
    99 end
   100 
   101 subsection {* Quickcheck generators *}
   102 
   103 notation fcomp (infixl "\<circ>>" 60)
   104 notation scomp (infixl "\<circ>\<rightarrow>" 60)
   105 
   106 definition (in term_syntax)
   107   valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   108 where
   109   "valterm_empty = Code_Evaluation.valtermify empty"
   110 
   111 definition (in term_syntax)
   112   valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   113   'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   114   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   115   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   116   [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   117 
   118 fun (in term_syntax) random_aux_alist 
   119 where
   120   "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)]))"
   121 
   122 instantiation alist :: (random, random) random
   123 begin
   124 
   125 definition random_alist
   126 where
   127   "random_alist i = random_aux_alist i i"
   128  
   129 instance ..
   130 
   131 end
   132 
   133 no_notation fcomp (infixl "\<circ>>" 60)
   134 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   135 
   136 instantiation alist :: (exhaustive, exhaustive) exhaustive
   137 begin
   138 
   139 fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
   140 where
   141   "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
   142      exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
   143 
   144 instance ..
   145 
   146 end
   147 
   148 instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   149 begin
   150 
   151 fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   152 where
   153   "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
   154      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))"
   155 
   156 instance ..
   157 
   158 end
   159 
   160 hide_const valterm_empty valterm_update random_aux_alist
   161 
   162 hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   163 hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
   164 
   165 end