src/HOL/Library/DAList.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47178 2ae2b6fa9c84
child 47308 9caab698dbe4
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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 subsection {* Abstract operation properties *}
    72 
    73 (* FIXME: to be completed *)
    74 
    75 lemma lookup_empty [simp]: "lookup empty k = None"
    76 by(simp add: empty_def lookup_def Alist_inverse)
    77 
    78 lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    79 by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    80 
    81 subsection {* Further operations *}
    82 
    83 subsubsection {* Equality *}
    84 
    85 instantiation alist :: (equal, equal) equal begin
    86 
    87 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
    88 
    89 instance
    90 proof
    91 qed (simp add: equal_alist_def impl_of_inject)
    92 
    93 end
    94 
    95 subsubsection {* Size *}
    96 
    97 instantiation alist :: (type, type) size begin
    98 
    99 definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
   100 
   101 instance ..
   102 
   103 end
   104 
   105 subsection {* Quickcheck generators *}
   106 
   107 notation fcomp (infixl "\<circ>>" 60)
   108 notation scomp (infixl "\<circ>\<rightarrow>" 60)
   109 
   110 definition (in term_syntax)
   111   valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   112 where
   113   "valterm_empty = Code_Evaluation.valtermify empty"
   114 
   115 definition (in term_syntax)
   116   valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   117   'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   118   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   119   ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   120   [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   121 
   122 fun (in term_syntax) random_aux_alist 
   123 where
   124   "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)]))"
   125 
   126 instantiation alist :: (random, random) random
   127 begin
   128 
   129 definition random_alist
   130 where
   131   "random_alist i = random_aux_alist i i"
   132  
   133 instance ..
   134 
   135 end
   136 
   137 no_notation fcomp (infixl "\<circ>>" 60)
   138 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   139 
   140 instantiation alist :: (exhaustive, exhaustive) exhaustive
   141 begin
   142 
   143 fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
   144 where
   145   "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
   146      exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
   147 
   148 instance ..
   149 
   150 end
   151 
   152 instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   153 begin
   154 
   155 fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   156 where
   157   "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
   158      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))"
   159 
   160 instance ..
   161 
   162 end
   163 
   164 hide_const valterm_empty valterm_update random_aux_alist
   165 
   166 hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   167 hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
   168 
   169 end