author | haftmann |
Sun, 31 Jan 2010 14:51:31 +0100 | |
changeset 34976 | 06df18c9a091 |
parent 34048 | 369509057220 |
child 36176 | 3fe7e97ccca8 |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
4 |
header {* Executable finite sets *} |
|
5 |
||
31849 | 6 |
theory Fset |
31807 | 7 |
imports List_Set |
8 |
begin |
|
9 |
||
31846 | 10 |
declare mem_def [simp] |
11 |
||
31807 | 12 |
subsection {* Lifting *} |
13 |
||
14 |
datatype 'a fset = Fset "'a set" |
|
15 |
||
16 |
primrec member :: "'a fset \<Rightarrow> 'a set" where |
|
17 |
"member (Fset A) = A" |
|
18 |
||
34048 | 19 |
lemma member_inject [simp]: |
20 |
"member A = member B \<Longrightarrow> A = B" |
|
21 |
by (cases A, cases B) simp |
|
22 |
||
31807 | 23 |
lemma Fset_member [simp]: |
24 |
"Fset (member A) = A" |
|
25 |
by (cases A) simp |
|
26 |
||
27 |
definition Set :: "'a list \<Rightarrow> 'a fset" where |
|
28 |
"Set xs = Fset (set xs)" |
|
29 |
||
30 |
lemma member_Set [simp]: |
|
31 |
"member (Set xs) = set xs" |
|
32 |
by (simp add: Set_def) |
|
33 |
||
32880 | 34 |
definition Coset :: "'a list \<Rightarrow> 'a fset" where |
35 |
"Coset xs = Fset (- set xs)" |
|
36 |
||
37 |
lemma member_Coset [simp]: |
|
38 |
"member (Coset xs) = - set xs" |
|
39 |
by (simp add: Coset_def) |
|
40 |
||
41 |
code_datatype Set Coset |
|
42 |
||
43 |
lemma member_code [code]: |
|
44 |
"member (Set xs) y \<longleftrightarrow> List.member y xs" |
|
45 |
"member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs" |
|
46 |
by (simp_all add: mem_iff fun_Compl_def bool_Compl_def) |
|
47 |
||
48 |
lemma member_image_UNIV [simp]: |
|
49 |
"member ` UNIV = UNIV" |
|
50 |
proof - |
|
51 |
have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B" |
|
52 |
proof |
|
53 |
fix A :: "'a set" |
|
54 |
show "A = member (Fset A)" by simp |
|
55 |
qed |
|
56 |
then show ?thesis by (simp add: image_def) |
|
57 |
qed |
|
31807 | 58 |
|
59 |
||
34048 | 60 |
subsection {* Lattice instantiation *} |
61 |
||
62 |
instantiation fset :: (type) boolean_algebra |
|
63 |
begin |
|
64 |
||
65 |
definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
66 |
[simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B" |
|
67 |
||
68 |
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
69 |
[simp]: "A < B \<longleftrightarrow> member A \<subset> member B" |
|
70 |
||
71 |
definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
72 |
[simp]: "inf A B = Fset (member A \<inter> member B)" |
|
73 |
||
74 |
definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
75 |
[simp]: "sup A B = Fset (member A \<union> member B)" |
|
76 |
||
77 |
definition bot_fset :: "'a fset" where |
|
78 |
[simp]: "bot = Fset {}" |
|
79 |
||
80 |
definition top_fset :: "'a fset" where |
|
81 |
[simp]: "top = Fset UNIV" |
|
82 |
||
83 |
definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where |
|
84 |
[simp]: "- A = Fset (- (member A))" |
|
85 |
||
86 |
definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
87 |
[simp]: "A - B = Fset (member A - member B)" |
|
88 |
||
89 |
instance proof |
|
90 |
qed auto |
|
91 |
||
92 |
end |
|
93 |
||
94 |
instantiation fset :: (type) complete_lattice |
|
95 |
begin |
|
96 |
||
97 |
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where |
|
98 |
[simp, code del]: "Inf_fset As = Fset (Inf (image member As))" |
|
99 |
||
100 |
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where |
|
101 |
[simp, code del]: "Sup_fset As = Fset (Sup (image member As))" |
|
102 |
||
103 |
instance proof |
|
104 |
qed (auto simp add: le_fun_def le_bool_def) |
|
105 |
||
106 |
end |
|
107 |
||
31807 | 108 |
subsection {* Basic operations *} |
109 |
||
110 |
definition is_empty :: "'a fset \<Rightarrow> bool" where |
|
31846 | 111 |
[simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)" |
31807 | 112 |
|
113 |
lemma is_empty_Set [code]: |
|
114 |
"is_empty (Set xs) \<longleftrightarrow> null xs" |
|
31846 | 115 |
by (simp add: is_empty_set) |
31807 | 116 |
|
34048 | 117 |
lemma empty_Set [code]: |
118 |
"bot = Set []" |
|
119 |
by simp |
|
31807 | 120 |
|
34048 | 121 |
lemma UNIV_Set [code]: |
122 |
"top = Coset []" |
|
123 |
by simp |
|
31807 | 124 |
|
125 |
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
31846 | 126 |
[simp]: "insert x A = Fset (Set.insert x (member A))" |
31807 | 127 |
|
128 |
lemma insert_Set [code]: |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
129 |
"insert x (Set xs) = Set (List.insert x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
130 |
"insert x (Coset xs) = Coset (removeAll x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
131 |
by (simp_all add: Set_def Coset_def set_insert) |
31807 | 132 |
|
133 |
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
31846 | 134 |
[simp]: "remove x A = Fset (List_Set.remove x (member A))" |
31807 | 135 |
|
136 |
lemma remove_Set [code]: |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
137 |
"remove x (Set xs) = Set (removeAll x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
138 |
"remove x (Coset xs) = Coset (List.insert x xs)" |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
139 |
by (simp_all add: Set_def Coset_def remove_set_compl) |
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
140 |
(simp add: List_Set.remove_def) |
31807 | 141 |
|
142 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
|
31846 | 143 |
[simp]: "map f A = Fset (image f (member A))" |
31807 | 144 |
|
145 |
lemma map_Set [code]: |
|
146 |
"map f (Set xs) = Set (remdups (List.map f xs))" |
|
31846 | 147 |
by (simp add: Set_def) |
31807 | 148 |
|
31847 | 149 |
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
150 |
[simp]: "filter P A = Fset (List_Set.project P (member A))" |
|
31807 | 151 |
|
31847 | 152 |
lemma filter_Set [code]: |
153 |
"filter P (Set xs) = Set (List.filter P xs)" |
|
31846 | 154 |
by (simp add: Set_def project_set) |
31807 | 155 |
|
156 |
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
31846 | 157 |
[simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
31807 | 158 |
|
159 |
lemma forall_Set [code]: |
|
160 |
"forall P (Set xs) \<longleftrightarrow> list_all P xs" |
|
31846 | 161 |
by (simp add: Set_def ball_set) |
31807 | 162 |
|
163 |
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
31846 | 164 |
[simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
31807 | 165 |
|
166 |
lemma exists_Set [code]: |
|
167 |
"exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
|
31846 | 168 |
by (simp add: Set_def bex_set) |
169 |
||
31849 | 170 |
definition card :: "'a fset \<Rightarrow> nat" where |
171 |
[simp]: "card A = Finite_Set.card (member A)" |
|
172 |
||
173 |
lemma card_Set [code]: |
|
174 |
"card (Set xs) = length (remdups xs)" |
|
175 |
proof - |
|
176 |
have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" |
|
177 |
by (rule distinct_card) simp |
|
178 |
then show ?thesis by (simp add: Set_def card_def) |
|
179 |
qed |
|
180 |
||
31846 | 181 |
|
182 |
subsection {* Derived operations *} |
|
183 |
||
184 |
lemma subfset_eq_forall [code]: |
|
34048 | 185 |
"A \<le> B \<longleftrightarrow> forall (member B) A" |
31846 | 186 |
by (simp add: subset_eq) |
187 |
||
188 |
lemma subfset_subfset_eq [code]: |
|
34048 | 189 |
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)" |
190 |
by (fact less_le_not_le) |
|
31846 | 191 |
|
192 |
lemma eq_fset_subfset_eq [code]: |
|
34048 | 193 |
"eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)" |
31846 | 194 |
by (cases A, cases B) (simp add: eq set_eq) |
195 |
||
31807 | 196 |
|
197 |
subsection {* Functorial operations *} |
|
198 |
||
32880 | 199 |
lemma inter_project [code]: |
34048 | 200 |
"inf A (Set xs) = Set (List.filter (member A) xs)" |
201 |
"inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs" |
|
31807 | 202 |
proof - |
34048 | 203 |
show "inf A (Set xs) = Set (List.filter (member A) xs)" |
32880 | 204 |
by (simp add: inter project_def Set_def) |
205 |
have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
|
206 |
member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
207 |
by (rule foldl_apply) (simp add: expand_fun_eq) |
34048 | 208 |
then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs" |
32880 | 209 |
by (simp add: Diff_eq [symmetric] minus_set) |
31807 | 210 |
qed |
211 |
||
212 |
lemma subtract_remove [code]: |
|
34048 | 213 |
"A - Set xs = foldl (\<lambda>A x. remove x A) A xs" |
214 |
"A - Coset xs = Set (List.filter (member A) xs)" |
|
31807 | 215 |
proof - |
216 |
have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
|
217 |
member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
218 |
by (rule foldl_apply) (simp add: expand_fun_eq) |
34048 | 219 |
then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs" |
32880 | 220 |
by (simp add: minus_set) |
34048 | 221 |
show "A - Coset xs = Set (List.filter (member A) xs)" |
32880 | 222 |
by (auto simp add: Coset_def Set_def) |
223 |
qed |
|
224 |
||
225 |
lemma union_insert [code]: |
|
34048 | 226 |
"sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
227 |
"sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)" |
|
32880 | 228 |
proof - |
229 |
have "foldl (\<lambda>A x. Set.insert x A) (member A) xs = |
|
230 |
member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)" |
|
34976
06df18c9a091
generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34048
diff
changeset
|
231 |
by (rule foldl_apply) (simp add: expand_fun_eq) |
34048 | 232 |
then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
32880 | 233 |
by (simp add: union_set) |
34048 | 234 |
show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)" |
32880 | 235 |
by (auto simp add: Coset_def) |
31807 | 236 |
qed |
237 |
||
34048 | 238 |
context complete_lattice |
239 |
begin |
|
31807 | 240 |
|
34048 | 241 |
definition Infimum :: "'a fset \<Rightarrow> 'a" where |
242 |
[simp]: "Infimum A = Inf (member A)" |
|
31807 | 243 |
|
34048 | 244 |
lemma Infimum_inf [code]: |
245 |
"Infimum (Set As) = foldl inf top As" |
|
246 |
"Infimum (Coset []) = bot" |
|
247 |
by (simp_all add: Inf_set_fold Inf_UNIV) |
|
31807 | 248 |
|
34048 | 249 |
definition Supremum :: "'a fset \<Rightarrow> 'a" where |
250 |
[simp]: "Supremum A = Sup (member A)" |
|
251 |
||
252 |
lemma Supremum_sup [code]: |
|
253 |
"Supremum (Set As) = foldl sup bot As" |
|
254 |
"Supremum (Coset []) = top" |
|
255 |
by (simp_all add: Sup_set_fold Sup_UNIV) |
|
256 |
||
257 |
end |
|
31807 | 258 |
|
259 |
||
260 |
subsection {* Misc operations *} |
|
261 |
||
262 |
lemma size_fset [code]: |
|
263 |
"fset_size f A = 0" |
|
264 |
"size A = 0" |
|
265 |
by (cases A, simp) (cases A, simp) |
|
266 |
||
267 |
lemma fset_case_code [code]: |
|
268 |
"fset_case f A = f (member A)" |
|
269 |
by (cases A) simp |
|
270 |
||
271 |
lemma fset_rec_code [code]: |
|
272 |
"fset_rec f A = f (member A)" |
|
273 |
by (cases A) simp |
|
274 |
||
31846 | 275 |
|
276 |
subsection {* Simplified simprules *} |
|
277 |
||
278 |
lemma is_empty_simp [simp]: |
|
279 |
"is_empty A \<longleftrightarrow> member A = {}" |
|
280 |
by (simp add: List_Set.is_empty_def) |
|
281 |
declare is_empty_def [simp del] |
|
282 |
||
283 |
lemma remove_simp [simp]: |
|
284 |
"remove x A = Fset (member A - {x})" |
|
285 |
by (simp add: List_Set.remove_def) |
|
286 |
declare remove_def [simp del] |
|
287 |
||
31847 | 288 |
lemma filter_simp [simp]: |
289 |
"filter P A = Fset {x \<in> member A. P x}" |
|
31846 | 290 |
by (simp add: List_Set.project_def) |
31847 | 291 |
declare filter_def [simp del] |
31846 | 292 |
|
293 |
declare mem_def [simp del] |
|
294 |
||
31849 | 295 |
|
34048 | 296 |
hide (open) const is_empty insert remove map filter forall exists card |
297 |
Inter Union |
|
31849 | 298 |
|
31807 | 299 |
end |