author | haftmann |
Mon, 23 Aug 2010 11:17:13 +0200 | |
changeset 38642 | 8fa437809c67 |
parent 38512 | ed4703b416ed |
child 38857 | 97775f3e8722 |
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: |
38512 | 18 |
assumes "list_of_dlist dxs = list_of_dlist dys" |
19 |
shows "dxs = dys" |
|
36274 | 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 |
|
37765 | 26 |
"Dlist xs = Abs_dlist (remdups xs)" |
35303 | 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 |
|
38512 | 110 |
text {* Equality *} |
111 |
||
112 |
instantiation dlist :: (eq) eq |
|
113 |
begin |
|
114 |
||
115 |
definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)" |
|
116 |
||
117 |
instance proof |
|
118 |
qed (simp add: eq_dlist_def eq list_of_dlist_inject) |
|
119 |
||
120 |
end |
|
121 |
||
122 |
||
37106 | 123 |
section {* Induction principle and case distinction *} |
124 |
||
125 |
lemma dlist_induct [case_names empty insert, induct type: dlist]: |
|
126 |
assumes empty: "P empty" |
|
127 |
assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)" |
|
128 |
shows "P dxs" |
|
129 |
proof (cases dxs) |
|
130 |
case (Abs_dlist xs) |
|
131 |
then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) |
|
132 |
from `distinct xs` have "P (Dlist xs)" |
|
133 |
proof (induct xs rule: distinct_induct) |
|
134 |
case Nil from empty show ?case by (simp add: empty_def) |
|
135 |
next |
|
136 |
case (insert x xs) |
|
137 |
then have "\<not> member (Dlist xs) x" and "P (Dlist xs)" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
138 |
by (simp_all add: member_def List.member_def) |
37106 | 139 |
with insrt have "P (insert x (Dlist xs))" . |
140 |
with insert show ?case by (simp add: insert_def distinct_remdups_id) |
|
141 |
qed |
|
142 |
with dxs show "P dxs" by simp |
|
143 |
qed |
|
144 |
||
145 |
lemma dlist_case [case_names empty insert, cases type: dlist]: |
|
146 |
assumes empty: "dxs = empty \<Longrightarrow> P" |
|
147 |
assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P" |
|
148 |
shows P |
|
149 |
proof (cases dxs) |
|
150 |
case (Abs_dlist xs) |
|
151 |
then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" |
|
152 |
by (simp_all add: Dlist_def distinct_remdups_id) |
|
153 |
show P proof (cases xs) |
|
154 |
case Nil with dxs have "dxs = empty" by (simp add: empty_def) |
|
155 |
with empty show P . |
|
156 |
next |
|
157 |
case (Cons x xs) |
|
158 |
with dxs distinct have "\<not> member (Dlist xs) x" |
|
159 |
and "dxs = insert x (Dlist xs)" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
160 |
by (simp_all add: member_def List.member_def insert_def distinct_remdups_id) |
37106 | 161 |
with insert show P . |
162 |
qed |
|
163 |
qed |
|
164 |
||
165 |
||
35303 | 166 |
section {* Implementation of sets by distinct lists -- canonical! *} |
167 |
||
168 |
definition Set :: "'a dlist \<Rightarrow> 'a fset" where |
|
169 |
"Set dxs = Fset.Set (list_of_dlist dxs)" |
|
170 |
||
171 |
definition Coset :: "'a dlist \<Rightarrow> 'a fset" where |
|
172 |
"Coset dxs = Fset.Coset (list_of_dlist dxs)" |
|
173 |
||
174 |
code_datatype Set Coset |
|
175 |
||
176 |
declare member_code [code del] |
|
177 |
declare is_empty_Set [code del] |
|
178 |
declare empty_Set [code del] |
|
179 |
declare UNIV_Set [code del] |
|
180 |
declare insert_Set [code del] |
|
181 |
declare remove_Set [code del] |
|
37029 | 182 |
declare compl_Set [code del] |
183 |
declare compl_Coset [code del] |
|
35303 | 184 |
declare map_Set [code del] |
185 |
declare filter_Set [code del] |
|
186 |
declare forall_Set [code del] |
|
187 |
declare exists_Set [code del] |
|
188 |
declare card_Set [code del] |
|
189 |
declare inter_project [code del] |
|
190 |
declare subtract_remove [code del] |
|
191 |
declare union_insert [code del] |
|
192 |
declare Infimum_inf [code del] |
|
193 |
declare Supremum_sup [code del] |
|
194 |
||
195 |
lemma Set_Dlist [simp]: |
|
196 |
"Set (Dlist xs) = Fset (set xs)" |
|
37473 | 197 |
by (rule fset_eqI) (simp add: Set_def) |
35303 | 198 |
|
199 |
lemma Coset_Dlist [simp]: |
|
200 |
"Coset (Dlist xs) = Fset (- set xs)" |
|
37473 | 201 |
by (rule fset_eqI) (simp add: Coset_def) |
35303 | 202 |
|
203 |
lemma member_Set [simp]: |
|
204 |
"Fset.member (Set dxs) = List.member (list_of_dlist dxs)" |
|
205 |
by (simp add: Set_def member_set) |
|
206 |
||
207 |
lemma member_Coset [simp]: |
|
208 |
"Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)" |
|
209 |
by (simp add: Coset_def member_set not_set_compl) |
|
210 |
||
36980
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
211 |
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
|
212 |
"Fset.Set xs = Set (dlist_of_list xs)" |
37473 | 213 |
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
|
214 |
|
1a4cc941171a
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
haftmann
parents:
36274
diff
changeset
|
215 |
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
|
216 |
"Fset.Coset xs = Coset (dlist_of_list xs)" |
37473 | 217 |
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
|
218 |
|
35303 | 219 |
lemma is_empty_Set [code]: |
220 |
"Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37473
diff
changeset
|
221 |
by (simp add: null_def List.null_def member_set) |
35303 | 222 |
|
223 |
lemma bot_code [code]: |
|
224 |
"bot = Set empty" |
|
225 |
by (simp add: empty_def) |
|
226 |
||
227 |
lemma top_code [code]: |
|
228 |
"top = Coset empty" |
|
229 |
by (simp add: empty_def) |
|
230 |
||
231 |
lemma insert_code [code]: |
|
232 |
"Fset.insert x (Set dxs) = Set (insert x dxs)" |
|
233 |
"Fset.insert x (Coset dxs) = Coset (remove x dxs)" |
|
234 |
by (simp_all add: insert_def remove_def member_set not_set_compl) |
|
235 |
||
236 |
lemma remove_code [code]: |
|
237 |
"Fset.remove x (Set dxs) = Set (remove x dxs)" |
|
238 |
"Fset.remove x (Coset dxs) = Coset (insert x dxs)" |
|
239 |
by (auto simp add: insert_def remove_def member_set not_set_compl) |
|
240 |
||
241 |
lemma member_code [code]: |
|
242 |
"Fset.member (Set dxs) = member dxs" |
|
243 |
"Fset.member (Coset dxs) = Not \<circ> member dxs" |
|
244 |
by (simp_all add: member_def) |
|
245 |
||
37029 | 246 |
lemma compl_code [code]: |
247 |
"- Set dxs = Coset dxs" |
|
248 |
"- Coset dxs = Set dxs" |
|
37473 | 249 |
by (rule fset_eqI, simp add: member_set not_set_compl)+ |
37029 | 250 |
|
35303 | 251 |
lemma map_code [code]: |
252 |
"Fset.map f (Set dxs) = Set (map f dxs)" |
|
37473 | 253 |
by (rule fset_eqI) (simp add: member_set) |
35303 | 254 |
|
255 |
lemma filter_code [code]: |
|
256 |
"Fset.filter f (Set dxs) = Set (filter f dxs)" |
|
37473 | 257 |
by (rule fset_eqI) (simp add: member_set) |
35303 | 258 |
|
259 |
lemma forall_Set [code]: |
|
260 |
"Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)" |
|
261 |
by (simp add: member_set list_all_iff) |
|
262 |
||
263 |
lemma exists_Set [code]: |
|
264 |
"Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)" |
|
265 |
by (simp add: member_set list_ex_iff) |
|
266 |
||
267 |
lemma card_code [code]: |
|
268 |
"Fset.card (Set dxs) = length dxs" |
|
269 |
by (simp add: length_def member_set distinct_card) |
|
270 |
||
271 |
lemma inter_code [code]: |
|
272 |
"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
|
273 |
"inf A (Coset xs) = foldr Fset.remove xs A" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
274 |
by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter) |
35303 | 275 |
|
276 |
lemma subtract_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
277 |
"A - Set xs = foldr Fset.remove xs A" |
35303 | 278 |
"A - Coset xs = Set (filter (Fset.member A) xs)" |
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
279 |
by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter) |
35303 | 280 |
|
281 |
lemma union_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
282 |
"sup (Set xs) A = foldr Fset.insert xs A" |
35303 | 283 |
"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
|
284 |
by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter) |
35303 | 285 |
|
286 |
context complete_lattice |
|
287 |
begin |
|
288 |
||
289 |
lemma Infimum_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
290 |
"Infimum (Set As) = foldr inf As top" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
291 |
by (simp only: Set_def Infimum_inf foldr_def inf.commute) |
35303 | 292 |
|
293 |
lemma Supremum_code [code]: |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
294 |
"Supremum (Set As) = foldr sup As bot" |
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
295 |
by (simp only: Set_def Supremum_sup foldr_def sup.commute) |
35303 | 296 |
|
297 |
end |
|
298 |
||
38512 | 299 |
|
37022
f9681d9d1d56
moved generic List operations to theory More_List
haftmann
parents:
36980
diff
changeset
|
300 |
hide_const (open) member fold foldr empty insert remove map filter null member length fold |
35303 | 301 |
|
302 |
end |