author | haftmann |
Mon, 21 Jun 2010 09:06:14 +0200 | |
changeset 37473 | 013f78aed840 |
parent 37106 | d56e0b30ce5a |
child 37595 | 9591362629e3 |
permissions | -rw-r--r-- |
35303 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
2 |
||
3 |
header {* Lists with elements distinct as canonical example for datatype invariants *} |
|
4 |
||
5 |
theory Dlist |
|
37473 | 6 |
imports Main Fset |
35303 | 7 |
begin |
8 |
||
9 |
section {* The type of distinct lists *} |
|
10 |
||
11 |
typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |
|
12 |
morphisms list_of_dlist Abs_dlist |
|
13 |
proof |
|
14 |
show "[] \<in> ?dlist" by simp |
|
15 |
qed |
|
16 |
||
36274 | 17 |
lemma dlist_ext: |
18 |
assumes "list_of_dlist xs = list_of_dlist ys" |
|
19 |
shows "xs = ys" |
|
20 |
using assms by (simp add: list_of_dlist_inject) |
|
21 |
||
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35688
diff
changeset
|
22 |
|
35303 | 23 |
text {* Formal, totalized constructor for @{typ "'a dlist"}: *} |
24 |
||
25 |
definition Dlist :: "'a list \<Rightarrow> 'a dlist" where |
|
26 |
[code del]: "Dlist xs = Abs_dlist (remdups xs)" |
|
27 |
||
28 |
lemma distinct_list_of_dlist [simp]: |
|
29 |
"distinct (list_of_dlist dxs)" |
|
30 |
using list_of_dlist [of dxs] by simp |
|
31 |
||
32 |
lemma list_of_dlist_Dlist [simp]: |
|
33 |
"list_of_dlist (Dlist xs) = remdups xs" |
|
34 |
by (simp add: Dlist_def Abs_dlist_inverse) |
|
35 |
||
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35688
diff
changeset
|
36 |
lemma Dlist_list_of_dlist [simp, code abstype]: |
35303 | 37 |
"Dlist (list_of_dlist dxs) = dxs" |
38 |
by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id) |
|
39 |
||
40 |
||
41 |
text {* Fundamental operations: *} |
|
42 |
||
43 |
definition empty :: "'a dlist" where |
|
44 |
"empty = Dlist []" |
|
45 |
||
46 |
definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where |
|
47 |
"insert x dxs = Dlist (List.insert x (list_of_dlist dxs))" |
|
48 |
||
49 |
definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where |
|
50 |
"remove x dxs = Dlist (remove1 x (list_of_dlist dxs))" |
|
51 |
||
52 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where |
|
53 |
"map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))" |
|
54 |
||
55 |
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where |
|
56 |
"filter P dxs = Dlist (List.filter P (list_of_dlist dxs))" |
|
57 |
||
58 |
||
59 |
text {* Derived operations: *} |
|
60 |
||
61 |
definition null :: "'a dlist \<Rightarrow> bool" where |
|
62 |
"null dxs = List.null (list_of_dlist dxs)" |
|
63 |
||
64 |
definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where |
|
65 |
"member dxs = List.member (list_of_dlist dxs)" |
|
66 |
||
67 |
definition length :: "'a dlist \<Rightarrow> nat" where |
|
68 |
"length dxs = List.length (list_of_dlist dxs)" |
|
69 |
||
70 |
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
71 |
"fold f dxs = More_List.fold f (list_of_dlist dxs)" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
72 |
|
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
73 |
definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
74 |
"foldr f dxs = List.foldr f (list_of_dlist dxs)" |
35303 | 75 |
|
76 |
||
77 |
section {* Executable version obeying invariant *} |
|
78 |
||
79 |
lemma list_of_dlist_empty [simp, code abstract]: |
|
80 |
"list_of_dlist empty = []" |
|
81 |
by (simp add: empty_def) |
|
82 |
||
83 |
lemma list_of_dlist_insert [simp, code abstract]: |
|
84 |
"list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)" |
|
85 |
by (simp add: insert_def) |
|
86 |
||
87 |
lemma list_of_dlist_remove [simp, code abstract]: |
|
88 |
"list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)" |
|
89 |
by (simp add: remove_def) |
|
90 |
||
91 |
lemma list_of_dlist_map [simp, code abstract]: |
|
92 |
"list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))" |
|
93 |
by (simp add: map_def) |
|
94 |
||
95 |
lemma list_of_dlist_filter [simp, code abstract]: |
|
96 |
"list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)" |
|
97 |
by (simp add: filter_def) |
|
98 |
||
99 |
||
36980
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
100 |
text {* Explicit executable conversion *} |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
101 |
|
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
102 |
definition dlist_of_list [simp]: |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
103 |
"dlist_of_list = Dlist" |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
104 |
|
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
105 |
lemma [code abstract]: |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
106 |
"list_of_dlist (dlist_of_list xs) = remdups xs" |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
107 |
by simp |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
108 |
|
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
109 |
|
37106 | 110 |
section {* Induction principle and case distinction *} |
111 |
||
112 |
lemma dlist_induct [case_names empty insert, induct type: dlist]: |
|
113 |
assumes empty: "P empty" |
|
114 |
assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)" |
|
115 |
shows "P dxs" |
|
116 |
proof (cases dxs) |
|
117 |
case (Abs_dlist xs) |
|
118 |
then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) |
|
119 |
from `distinct xs` have "P (Dlist xs)" |
|
120 |
proof (induct xs rule: distinct_induct) |
|
121 |
case Nil from empty show ?case by (simp add: empty_def) |
|
122 |
next |
|
123 |
case (insert x xs) |
|
124 |
then have "\<not> member (Dlist xs) x" and "P (Dlist xs)" |
|
125 |
by (simp_all add: member_def mem_iff) |
|
126 |
with insrt have "P (insert x (Dlist xs))" . |
|
127 |
with insert show ?case by (simp add: insert_def distinct_remdups_id) |
|
128 |
qed |
|
129 |
with dxs show "P dxs" by simp |
|
130 |
qed |
|
131 |
||
132 |
lemma dlist_case [case_names empty insert, cases type: dlist]: |
|
133 |
assumes empty: "dxs = empty \<Longrightarrow> P" |
|
134 |
assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P" |
|
135 |
shows P |
|
136 |
proof (cases dxs) |
|
137 |
case (Abs_dlist xs) |
|
138 |
then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" |
|
139 |
by (simp_all add: Dlist_def distinct_remdups_id) |
|
140 |
show P proof (cases xs) |
|
141 |
case Nil with dxs have "dxs = empty" by (simp add: empty_def) |
|
142 |
with empty show P . |
|
143 |
next |
|
144 |
case (Cons x xs) |
|
145 |
with dxs distinct have "\<not> member (Dlist xs) x" |
|
146 |
and "dxs = insert x (Dlist xs)" |
|
147 |
by (simp_all add: member_def mem_iff insert_def distinct_remdups_id) |
|
148 |
with insert show P . |
|
149 |
qed |
|
150 |
qed |
|
151 |
||
152 |
||
35303 | 153 |
section {* Implementation of sets by distinct lists -- canonical! *} |
154 |
||
155 |
definition Set :: "'a dlist \<Rightarrow> 'a fset" where |
|
156 |
"Set dxs = Fset.Set (list_of_dlist dxs)" |
|
157 |
||
158 |
definition Coset :: "'a dlist \<Rightarrow> 'a fset" where |
|
159 |
"Coset dxs = Fset.Coset (list_of_dlist dxs)" |
|
160 |
||
161 |
code_datatype Set Coset |
|
162 |
||
163 |
declare member_code [code del] |
|
164 |
declare is_empty_Set [code del] |
|
165 |
declare empty_Set [code del] |
|
166 |
declare UNIV_Set [code del] |
|
167 |
declare insert_Set [code del] |
|
168 |
declare remove_Set [code del] |
|
37029 | 169 |
declare compl_Set [code del] |
170 |
declare compl_Coset [code del] |
|
35303 | 171 |
declare map_Set [code del] |
172 |
declare filter_Set [code del] |
|
173 |
declare forall_Set [code del] |
|
174 |
declare exists_Set [code del] |
|
175 |
declare card_Set [code del] |
|
176 |
declare inter_project [code del] |
|
177 |
declare subtract_remove [code del] |
|
178 |
declare union_insert [code del] |
|
179 |
declare Infimum_inf [code del] |
|
180 |
declare Supremum_sup [code del] |
|
181 |
||
182 |
lemma Set_Dlist [simp]: |
|
183 |
"Set (Dlist xs) = Fset (set xs)" |
|
37473 | 184 |
by (rule fset_eqI) (simp add: Set_def) |
35303 | 185 |
|
186 |
lemma Coset_Dlist [simp]: |
|
187 |
"Coset (Dlist xs) = Fset (- set xs)" |
|
37473 | 188 |
by (rule fset_eqI) (simp add: Coset_def) |
35303 | 189 |
|
190 |
lemma member_Set [simp]: |
|
191 |
"Fset.member (Set dxs) = List.member (list_of_dlist dxs)" |
|
192 |
by (simp add: Set_def member_set) |
|
193 |
||
194 |
lemma member_Coset [simp]: |
|
195 |
"Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)" |
|
196 |
by (simp add: Coset_def member_set not_set_compl) |
|
197 |
||
36980
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
198 |
lemma Set_dlist_of_list [code]: |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
199 |
"Fset.Set xs = Set (dlist_of_list xs)" |
37473 | 200 |
by (rule fset_eqI) simp |
36980
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
201 |
|
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
202 |
lemma Coset_dlist_of_list [code]: |
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
203 |
"Fset.Coset xs = Coset (dlist_of_list xs)" |
37473 | 204 |
by (rule fset_eqI) simp |
36980
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
205 |
|
35303 | 206 |
lemma is_empty_Set [code]: |
207 |
"Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs" |
|
208 |
by (simp add: null_def null_empty member_set) |
|
209 |
||
210 |
lemma bot_code [code]: |
|
211 |
"bot = Set empty" |
|
212 |
by (simp add: empty_def) |
|
213 |
||
214 |
lemma top_code [code]: |
|
215 |
"top = Coset empty" |
|
216 |
by (simp add: empty_def) |
|
217 |
||
218 |
lemma insert_code [code]: |
|
219 |
"Fset.insert x (Set dxs) = Set (insert x dxs)" |
|
220 |
"Fset.insert x (Coset dxs) = Coset (remove x dxs)" |
|
221 |
by (simp_all add: insert_def remove_def member_set not_set_compl) |
|
222 |
||
223 |
lemma remove_code [code]: |
|
224 |
"Fset.remove x (Set dxs) = Set (remove x dxs)" |
|
225 |
"Fset.remove x (Coset dxs) = Coset (insert x dxs)" |
|
226 |
by (auto simp add: insert_def remove_def member_set not_set_compl) |
|
227 |
||
228 |
lemma member_code [code]: |
|
229 |
"Fset.member (Set dxs) = member dxs" |
|
230 |
"Fset.member (Coset dxs) = Not \<circ> member dxs" |
|
231 |
by (simp_all add: member_def) |
|
232 |
||
37029 | 233 |
lemma compl_code [code]: |
234 |
"- Set dxs = Coset dxs" |
|
235 |
"- Coset dxs = Set dxs" |
|
37473 | 236 |
by (rule fset_eqI, simp add: member_set not_set_compl)+ |
37029 | 237 |
|
35303 | 238 |
lemma map_code [code]: |
239 |
"Fset.map f (Set dxs) = Set (map f dxs)" |
|
37473 | 240 |
by (rule fset_eqI) (simp add: member_set) |
35303 | 241 |
|
242 |
lemma filter_code [code]: |
|
243 |
"Fset.filter f (Set dxs) = Set (filter f dxs)" |
|
37473 | 244 |
by (rule fset_eqI) (simp add: member_set) |
35303 | 245 |
|
246 |
lemma forall_Set [code]: |
|
247 |
"Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)" |
|
248 |
by (simp add: member_set list_all_iff) |
|
249 |
||
250 |
lemma exists_Set [code]: |
|
251 |
"Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)" |
|
252 |
by (simp add: member_set list_ex_iff) |
|
253 |
||
254 |
lemma card_code [code]: |
|
255 |
"Fset.card (Set dxs) = length dxs" |
|
256 |
by (simp add: length_def member_set distinct_card) |
|
257 |
||
258 |
lemma inter_code [code]: |
|
259 |
"inf A (Set xs) = Set (filter (Fset.member A) xs)" |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
260 |
"inf A (Coset xs) = foldr Fset.remove xs A" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
261 |
by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter) |
35303 | 262 |
|
263 |
lemma subtract_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
264 |
"A - Set xs = foldr Fset.remove xs A" |
35303 | 265 |
"A - Coset xs = Set (filter (Fset.member A) xs)" |
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
266 |
by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter) |
35303 | 267 |
|
268 |
lemma union_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
269 |
"sup (Set xs) A = foldr Fset.insert xs A" |
35303 | 270 |
"sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)" |
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
271 |
by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter) |
35303 | 272 |
|
273 |
context complete_lattice |
|
274 |
begin |
|
275 |
||
276 |
lemma Infimum_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
277 |
"Infimum (Set As) = foldr inf As top" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
278 |
by (simp only: Set_def Infimum_inf foldr_def inf.commute) |
35303 | 279 |
|
280 |
lemma Supremum_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
281 |
"Supremum (Set As) = foldr sup As bot" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
282 |
by (simp only: Set_def Supremum_sup foldr_def sup.commute) |
35303 | 283 |
|
284 |
end |
|
285 |
||
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
286 |
hide_const (open) member fold foldr empty insert remove map filter null member length fold |
35303 | 287 |
|
288 |
end |