author | kuncar |
Tue, 03 Apr 2012 16:26:48 +0200 | |
changeset 47308 | 9caab698dbe4 |
parent 47178 | 2ae2b6fa9c84 |
child 49834 | b27bbb021df1 |
permissions | -rw-r--r-- |
46237 | 1 |
(* Title: HOL/Library/DAList.thy |
46167 | 2 |
Author: Lukas Bulwahn, TU Muenchen *) |
3 |
||
4 |
header {* Abstract type of association lists with unique keys *} |
|
5 |
||
46237 | 6 |
theory DAList |
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
7 |
imports AList |
46167 | 8 |
begin |
9 |
||
10 |
text {* This was based on some existing fragments in the AFP-Collection framework. *} |
|
11 |
||
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
12 |
subsection {* Preliminaries *} |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
13 |
|
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
14 |
lemma distinct_map_fst_filter: |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
15 |
"distinct (map fst xs) ==> distinct (map fst (List.filter P xs))" |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
16 |
by (induct xs) auto |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
17 |
|
46167 | 18 |
subsection {* Type @{text "('key, 'value) alist" } *} |
19 |
||
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
20 |
typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}" |
46507 | 21 |
morphisms impl_of Alist |
22 |
proof |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
23 |
show "[] \<in> {xs. (distinct o map fst) xs}" by simp |
46507 | 24 |
qed |
46167 | 25 |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
26 |
setup_lifting type_definition_alist |
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
27 |
|
46167 | 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 |
||
47308 | 42 |
lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of .. |
46167 | 43 |
|
47308 | 44 |
lift_definition empty :: "('key, 'value) alist" is "[]" by simp |
46167 | 45 |
|
47308 | 46 |
lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
47 |
is AList.update |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
48 |
by (simp add: distinct_update) |
46167 | 49 |
|
50 |
(* FIXME: we use an unoptimised delete operation. *) |
|
47308 | 51 |
lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
52 |
is AList.delete |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
53 |
by (simp add: distinct_delete) |
46167 | 54 |
|
47308 | 55 |
lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
56 |
is AList.map_entry |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
57 |
by (simp add: distinct_map_entry) |
46167 | 58 |
|
47308 | 59 |
lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist" |
60 |
is List.filter |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
61 |
by (simp add: distinct_map_fst_filter) |
46167 | 62 |
|
47308 | 63 |
lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" |
64 |
is AList.map_default |
|
47143
212f7a975d49
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
bulwahn
parents:
46507
diff
changeset
|
65 |
by (simp add: distinct_map_default) |
46167 | 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 |
||
46171
19f68d7671f0
proper hiding of facts and constants in AList_Impl and AList theory
bulwahn
parents:
46167
diff
changeset
|
162 |
hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def |
46167 | 163 |
hide_const (open) impl_of lookup empty update delete map_entry filter map_default |
164 |
||
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
165 |
end |