src/HOL/Library/DAList.thy
changeset 46237 99c80c2f841a
parent 46171 19f68d7671f0
child 46238 9ace9e5b79be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/DAList.thy	Tue Jan 17 09:38:30 2012 +0100
     1.3 @@ -0,0 +1,179 @@
     1.4 +(*  Title:      HOL/Library/DAList.thy
     1.5 +    Author:     Lukas Bulwahn, TU Muenchen *)
     1.6 +
     1.7 +header {* Abstract type of association lists with unique keys *}
     1.8 +
     1.9 +theory DAList
    1.10 +imports AList_Impl
    1.11 +begin
    1.12 +
    1.13 +text {* This was based on some existing fragments in the AFP-Collection framework. *}
    1.14 +
    1.15 +subsection {* Type @{text "('key, 'value) alist" } *}
    1.16 +
    1.17 +typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
    1.18 +morphisms impl_of Alist
    1.19 +by(rule exI[where x="[]"]) simp
    1.20 +
    1.21 +lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    1.22 +by(simp add: impl_of_inject)
    1.23 +
    1.24 +lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
    1.25 +by(simp add: impl_of_inject)
    1.26 +
    1.27 +lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
    1.28 +using impl_of[of xs] by simp
    1.29 +
    1.30 +lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
    1.31 +by(rule impl_of_inverse)
    1.32 +
    1.33 +subsection {* Primitive operations *}
    1.34 +
    1.35 +definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    1.36 +where [code]: "lookup xs = map_of (impl_of xs)" 
    1.37 +
    1.38 +definition empty :: "('key, 'value) alist"
    1.39 +where [code del]: "empty = Alist []"
    1.40 +
    1.41 +definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.42 +where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))"
    1.43 +
    1.44 +(* FIXME: we use an unoptimised delete operation. *)
    1.45 +definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.46 +where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
    1.47 +
    1.48 +definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.49 +where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" 
    1.50 +
    1.51 +definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.52 +where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
    1.53 +
    1.54 +definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.55 +where
    1.56 +  "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))"
    1.57 +
    1.58 +lemma impl_of_empty [code abstract]: "impl_of empty = []"
    1.59 +by (simp add: empty_def Alist_inverse)
    1.60 +
    1.61 +lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)"
    1.62 +by (simp add: update_def Alist_inverse distinct_update)
    1.63 +
    1.64 +lemma impl_of_delete [code abstract]:
    1.65 +  "impl_of (delete k al) = AList_Impl.delete k (impl_of al)"
    1.66 +unfolding delete_def by (simp add: Alist_inverse distinct_delete)
    1.67 +
    1.68 +lemma impl_of_map_entry [code abstract]:
    1.69 +  "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)"
    1.70 +unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
    1.71 +
    1.72 +lemma distinct_map_fst_filter:
    1.73 +   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
    1.74 +by (induct xs) auto
    1.75 +
    1.76 +lemma impl_of_filter [code abstract]:
    1.77 +  "impl_of (filter P xs) = List.filter P (impl_of xs)"
    1.78 +unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
    1.79 +
    1.80 +lemma impl_of_map_default [code abstract]:
    1.81 +  "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)"
    1.82 +by (auto simp add: map_default_def Alist_inverse distinct_map_default)
    1.83 +
    1.84 +subsection {* Abstract operation properties *}
    1.85 +
    1.86 +(* FIXME: to be completed *)
    1.87 +
    1.88 +lemma lookup_empty [simp]: "lookup empty k = None"
    1.89 +by(simp add: empty_def lookup_def Alist_inverse)
    1.90 +
    1.91 +lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    1.92 +by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    1.93 +
    1.94 +subsection {* Further operations *}
    1.95 +
    1.96 +subsubsection {* Equality *}
    1.97 +
    1.98 +instantiation alist :: (equal, equal) equal begin
    1.99 +
   1.100 +definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
   1.101 +
   1.102 +instance
   1.103 +proof
   1.104 +qed (simp add: equal_alist_def impl_of_inject)
   1.105 +
   1.106 +end
   1.107 +
   1.108 +subsubsection {* Size *}
   1.109 +
   1.110 +instantiation alist :: (type, type) size begin
   1.111 +
   1.112 +definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
   1.113 +
   1.114 +instance ..
   1.115 +
   1.116 +end
   1.117 +
   1.118 +subsection {* Quickcheck generators *}
   1.119 +
   1.120 +notation fcomp (infixl "\<circ>>" 60)
   1.121 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.122 +
   1.123 +definition (in term_syntax)
   1.124 +  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   1.125 +where
   1.126 +  "valterm_empty = Code_Evaluation.valtermify empty"
   1.127 +
   1.128 +definition (in term_syntax)
   1.129 +  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   1.130 +  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   1.131 +  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   1.132 +  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   1.133 +  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   1.134 +
   1.135 +fun (in term_syntax) random_aux_alist 
   1.136 +where
   1.137 +  "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)]))"
   1.138 +
   1.139 +instantiation alist :: (random, random) random
   1.140 +begin
   1.141 +
   1.142 +definition random_alist
   1.143 +where
   1.144 +  "random_alist i = random_aux_alist i i"
   1.145 + 
   1.146 +instance ..
   1.147 +
   1.148 +end
   1.149 +
   1.150 +no_notation fcomp (infixl "\<circ>>" 60)
   1.151 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.152 +
   1.153 +instantiation alist :: (exhaustive, exhaustive) exhaustive
   1.154 +begin
   1.155 +
   1.156 +fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.157 +where
   1.158 +  "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
   1.159 +     exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
   1.160 +
   1.161 +instance ..
   1.162 +
   1.163 +end
   1.164 +
   1.165 +instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   1.166 +begin
   1.167 +
   1.168 +fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.169 +where
   1.170 +  "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
   1.171 +     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))"
   1.172 +
   1.173 +instance ..
   1.174 +
   1.175 +end
   1.176 +
   1.177 +hide_const valterm_empty valterm_update random_aux_alist
   1.178 +
   1.179 +hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   1.180 +hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
   1.181 +
   1.182 +end
   1.183 \ No newline at end of file