1(* Title: HOL/Library/DAList.thy 2 Author: Lukas Bulwahn, TU Muenchen 3*) 4 5section \<open>Abstract type of association lists with unique keys\<close> 6 7theory DAList 8imports AList 9begin 10 11text \<open>This was based on some existing fragments in the AFP-Collection framework.\<close> 12 13subsection \<open>Preliminaries\<close> 14 15lemma distinct_map_fst_filter: 16 "distinct (map fst xs) \<Longrightarrow> distinct (map fst (List.filter P xs))" 17 by (induct xs) auto 18 19 20subsection \<open>Type \<open>('key, 'value) alist\<close>\<close> 21 22typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}" 23 morphisms impl_of Alist 24proof 25 show "[] \<in> {xs. (distinct \<circ> map fst) xs}" 26 by simp 27qed 28 29setup_lifting type_definition_alist 30 31lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys" 32 by (simp add: impl_of_inject) 33 34lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys" 35 by (simp add: impl_of_inject) 36 37lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))" 38 using impl_of[of xs] by simp 39 40lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs" 41 by (rule impl_of_inverse) 42 43 44subsection \<open>Primitive operations\<close> 45 46lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of . 47 48lift_definition empty :: "('key, 'value) alist" is "[]" 49 by simp 50 51lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" 52 is AList.update 53 by (simp add: distinct_update) 54 55(* FIXME: we use an unoptimised delete operation. *) 56lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" 57 is AList.delete 58 by (simp add: distinct_delete) 59 60lift_definition map_entry :: 61 "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" 62 is AList.map_entry 63 by (simp add: distinct_map_entry) 64 65lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" 66 is List.filter 67 by (simp add: distinct_map_fst_filter) 68 69lift_definition map_default :: 70 "'key \<Rightarrow> 'value \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" 71 is AList.map_default 72 by (simp add: distinct_map_default) 73 74 75subsection \<open>Abstract operation properties\<close> 76 77(* FIXME: to be completed *) 78 79lemma lookup_empty [simp]: "lookup empty k = None" 80by (simp add: empty_def lookup_def Alist_inverse) 81 82lemma lookup_update: 83 "lookup (update k1 v xs) k2 = (if k1 = k2 then Some v else lookup xs k2)" 84by(transfer)(simp add: update_conv') 85 86lemma lookup_update_eq [simp]: 87 "k1 = k2 \<Longrightarrow> lookup (update k1 v xs) k2 = Some v" 88by(simp add: lookup_update) 89 90lemma lookup_update_neq [simp]: 91 "k1 \<noteq> k2 \<Longrightarrow> lookup (update k1 v xs) k2 = lookup xs k2" 92by(simp add: lookup_update) 93 94lemma update_update_eq [simp]: 95 "k1 = k2 \<Longrightarrow> update k2 v2 (update k1 v1 xs) = update k2 v2 xs" 96by(transfer)(simp add: update_conv') 97 98lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)" 99 by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv') 100 101 102subsection \<open>Further operations\<close> 103 104subsubsection \<open>Equality\<close> 105 106instantiation alist :: (equal, equal) equal 107begin 108 109definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys" 110 111instance 112 by standard (simp add: equal_alist_def impl_of_inject) 113 114end 115 116 117subsubsection \<open>Size\<close> 118 119instantiation alist :: (type, type) size 120begin 121 122definition "size (al :: ('a, 'b) alist) = length (impl_of al)" 123 124instance .. 125 126end 127 128 129subsection \<open>Quickcheck generators\<close> 130 131notation fcomp (infixl "\<circ>>" 60) 132notation scomp (infixl "\<circ>\<rightarrow>" 60) 133 134definition (in term_syntax) 135 valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" 136 where "valterm_empty = Code_Evaluation.valtermify empty" 137 138definition (in term_syntax) 139 valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 140 'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 141 ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 142 ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where 143 [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a" 144 145fun (in term_syntax) random_aux_alist 146where 147 "random_aux_alist i j = 148 (if i = 0 then Pair valterm_empty 149 else Quickcheck_Random.collapse 150 (Random.select_weight 151 [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>k. Quickcheck_Random.random j \<circ>\<rightarrow> 152 (\<lambda>v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (\<lambda>a. Pair (valterm_update k v a))))), 153 (1, Pair valterm_empty)]))" 154 155instantiation alist :: (random, random) random 156begin 157 158definition random_alist 159where 160 "random_alist i = random_aux_alist i i" 161 162instance .. 163 164end 165 166no_notation fcomp (infixl "\<circ>>" 60) 167no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 168 169instantiation alist :: (exhaustive, exhaustive) exhaustive 170begin 171 172fun exhaustive_alist :: 173 "(('a, 'b) alist \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 174where 175 "exhaustive_alist f i = 176 (if i = 0 then None 177 else 178 case f empty of 179 Some ts \<Rightarrow> Some ts 180 | None \<Rightarrow> 181 exhaustive_alist 182 (\<lambda>a. Quickcheck_Exhaustive.exhaustive 183 (\<lambda>k. Quickcheck_Exhaustive.exhaustive (\<lambda>v. f (update k v a)) (i - 1)) (i - 1)) 184 (i - 1))" 185 186instance .. 187 188end 189 190instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive 191begin 192 193fun full_exhaustive_alist :: 194 "(('a, 'b) alist \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> 195 (bool \<times> term list) option" 196where 197 "full_exhaustive_alist f i = 198 (if i = 0 then None 199 else 200 case f valterm_empty of 201 Some ts \<Rightarrow> Some ts 202 | None \<Rightarrow> 203 full_exhaustive_alist 204 (\<lambda>a. 205 Quickcheck_Exhaustive.full_exhaustive 206 (\<lambda>k. Quickcheck_Exhaustive.full_exhaustive (\<lambda>v. f (valterm_update k v a)) (i - 1)) 207 (i - 1)) 208 (i - 1))" 209 210instance .. 211 212end 213 214 215section \<open>alist is a BNF\<close> 216 217lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel 218 by auto 219 220hide_const valterm_empty valterm_update random_aux_alist 221 222hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def 223hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel 224 225end 226