haftmann@34020
|
1 |
(* Title: HOL/Library/Executable_Set.thy
|
haftmann@34020
|
2 |
Author: Stefan Berghofer, TU Muenchen
|
haftmann@33913
|
3 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@33913
|
4 |
*)
|
haftmann@33913
|
5 |
|
haftmann@33913
|
6 |
header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
|
haftmann@33913
|
7 |
|
haftmann@34020
|
8 |
theory Executable_Set
|
haftmann@37016
|
9 |
imports More_Set
|
haftmann@33913
|
10 |
begin
|
haftmann@33913
|
11 |
|
haftmann@39380
|
12 |
text {*
|
haftmann@39380
|
13 |
This is just an ad-hoc hack which will rarely give you what you want.
|
haftmann@39380
|
14 |
For the moment, whenever you need executable sets, consider using
|
haftmann@44234
|
15 |
type @{text Cset.set} from theory @{text Cset}.
|
haftmann@39380
|
16 |
*}
|
haftmann@39380
|
17 |
|
haftmann@33913
|
18 |
declare mem_def [code del]
|
haftmann@33913
|
19 |
declare Collect_def [code del]
|
haftmann@33913
|
20 |
declare insert_code [code del]
|
haftmann@33913
|
21 |
declare vimage_code [code del]
|
haftmann@33913
|
22 |
|
haftmann@33913
|
23 |
subsection {* Set representation *}
|
haftmann@33913
|
24 |
|
haftmann@33913
|
25 |
setup {*
|
haftmann@33913
|
26 |
Code.add_type_cmd "set"
|
haftmann@33913
|
27 |
*}
|
haftmann@33913
|
28 |
|
haftmann@33913
|
29 |
definition Set :: "'a list \<Rightarrow> 'a set" where
|
haftmann@33913
|
30 |
[simp]: "Set = set"
|
haftmann@33913
|
31 |
|
haftmann@33913
|
32 |
definition Coset :: "'a list \<Rightarrow> 'a set" where
|
haftmann@33913
|
33 |
[simp]: "Coset xs = - set xs"
|
haftmann@33913
|
34 |
|
haftmann@33913
|
35 |
setup {*
|
haftmann@33913
|
36 |
Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
|
haftmann@33913
|
37 |
#> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
|
haftmann@33913
|
38 |
#> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
|
haftmann@33913
|
39 |
#> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
|
haftmann@33913
|
40 |
*}
|
haftmann@33913
|
41 |
|
haftmann@33913
|
42 |
code_datatype Set Coset
|
haftmann@33913
|
43 |
|
haftmann@34020
|
44 |
consts_code
|
haftmann@34020
|
45 |
Coset ("\<module>Coset")
|
haftmann@34020
|
46 |
Set ("\<module>Set")
|
haftmann@34020
|
47 |
attach {*
|
haftmann@34020
|
48 |
datatype 'a set = Set of 'a list | Coset of 'a list;
|
haftmann@34020
|
49 |
*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
|
haftmann@34020
|
50 |
|
haftmann@33913
|
51 |
|
haftmann@33913
|
52 |
subsection {* Basic operations *}
|
haftmann@33913
|
53 |
|
haftmann@33913
|
54 |
lemma [code]:
|
haftmann@33913
|
55 |
"set xs = Set (remdups xs)"
|
haftmann@33913
|
56 |
by simp
|
haftmann@33913
|
57 |
|
haftmann@33913
|
58 |
lemma [code]:
|
haftmann@37595
|
59 |
"x \<in> Set xs \<longleftrightarrow> List.member xs x"
|
haftmann@37595
|
60 |
"x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
|
haftmann@37595
|
61 |
by (simp_all add: member_def)
|
haftmann@33913
|
62 |
|
haftmann@33913
|
63 |
definition is_empty :: "'a set \<Rightarrow> bool" where
|
haftmann@33913
|
64 |
[simp]: "is_empty A \<longleftrightarrow> A = {}"
|
haftmann@33913
|
65 |
|
haftmann@34020
|
66 |
lemma [code_unfold]:
|
haftmann@33913
|
67 |
"A = {} \<longleftrightarrow> is_empty A"
|
haftmann@33913
|
68 |
by simp
|
haftmann@33913
|
69 |
|
haftmann@33913
|
70 |
definition empty :: "'a set" where
|
haftmann@33913
|
71 |
[simp]: "empty = {}"
|
haftmann@33913
|
72 |
|
haftmann@34020
|
73 |
lemma [code_unfold]:
|
haftmann@33913
|
74 |
"{} = empty"
|
haftmann@33913
|
75 |
by simp
|
haftmann@33913
|
76 |
|
haftmann@34020
|
77 |
lemma [code_unfold, code_inline del]:
|
haftmann@34020
|
78 |
"empty = Set []"
|
haftmann@34020
|
79 |
by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
|
haftmann@34020
|
80 |
|
haftmann@33913
|
81 |
setup {*
|
haftmann@33913
|
82 |
Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
|
haftmann@33913
|
83 |
#> Code.add_signature_cmd ("empty", "'a set")
|
haftmann@33913
|
84 |
#> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@37016
|
85 |
#> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@33913
|
86 |
#> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
|
haftmann@37016
|
87 |
#> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@33913
|
88 |
#> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
|
haftmann@33913
|
89 |
#> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
|
haftmann@33913
|
90 |
#> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
|
haftmann@33913
|
91 |
*}
|
haftmann@33913
|
92 |
|
haftmann@33913
|
93 |
lemma is_empty_Set [code]:
|
haftmann@37595
|
94 |
"is_empty (Set xs) \<longleftrightarrow> List.null xs"
|
haftmann@37595
|
95 |
by (simp add: null_def)
|
haftmann@33913
|
96 |
|
haftmann@33913
|
97 |
lemma empty_Set [code]:
|
haftmann@33913
|
98 |
"empty = Set []"
|
haftmann@33913
|
99 |
by simp
|
haftmann@33913
|
100 |
|
haftmann@33913
|
101 |
lemma insert_Set [code]:
|
haftmann@34967
|
102 |
"insert x (Set xs) = Set (List.insert x xs)"
|
haftmann@34967
|
103 |
"insert x (Coset xs) = Coset (removeAll x xs)"
|
haftmann@45883
|
104 |
by simp_all
|
haftmann@33913
|
105 |
|
haftmann@33913
|
106 |
lemma remove_Set [code]:
|
haftmann@34967
|
107 |
"remove x (Set xs) = Set (removeAll x xs)"
|
haftmann@34967
|
108 |
"remove x (Coset xs) = Coset (List.insert x xs)"
|
haftmann@45883
|
109 |
by (auto simp add: remove_def)
|
haftmann@33913
|
110 |
|
haftmann@33913
|
111 |
lemma image_Set [code]:
|
haftmann@33913
|
112 |
"image f (Set xs) = Set (remdups (map f xs))"
|
haftmann@33913
|
113 |
by simp
|
haftmann@33913
|
114 |
|
haftmann@33913
|
115 |
lemma project_Set [code]:
|
haftmann@33913
|
116 |
"project P (Set xs) = Set (filter P xs)"
|
haftmann@33913
|
117 |
by (simp add: project_set)
|
haftmann@33913
|
118 |
|
haftmann@33913
|
119 |
lemma Ball_Set [code]:
|
haftmann@33913
|
120 |
"Ball (Set xs) P \<longleftrightarrow> list_all P xs"
|
haftmann@37595
|
121 |
by (simp add: list_all_iff)
|
haftmann@33913
|
122 |
|
haftmann@33913
|
123 |
lemma Bex_Set [code]:
|
haftmann@33913
|
124 |
"Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
|
haftmann@37595
|
125 |
by (simp add: list_ex_iff)
|
haftmann@33913
|
126 |
|
bulwahn@45972
|
127 |
lemma
|
bulwahn@45972
|
128 |
[code, code del]: "card S = card S" ..
|
bulwahn@45972
|
129 |
|
haftmann@33913
|
130 |
lemma card_Set [code]:
|
haftmann@33913
|
131 |
"card (Set xs) = length (remdups xs)"
|
haftmann@33913
|
132 |
proof -
|
haftmann@33913
|
133 |
have "card (set (remdups xs)) = length (remdups xs)"
|
haftmann@33913
|
134 |
by (rule distinct_card) simp
|
haftmann@33913
|
135 |
then show ?thesis by simp
|
haftmann@33913
|
136 |
qed
|
haftmann@33913
|
137 |
|
haftmann@33913
|
138 |
|
haftmann@33913
|
139 |
subsection {* Derived operations *}
|
haftmann@33913
|
140 |
|
haftmann@33913
|
141 |
definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
|
haftmann@33913
|
142 |
[simp]: "set_eq = op ="
|
haftmann@33913
|
143 |
|
haftmann@34020
|
144 |
lemma [code_unfold]:
|
haftmann@33913
|
145 |
"op = = set_eq"
|
haftmann@33913
|
146 |
by simp
|
haftmann@33913
|
147 |
|
haftmann@33913
|
148 |
definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
|
haftmann@33913
|
149 |
[simp]: "subset_eq = op \<subseteq>"
|
haftmann@33913
|
150 |
|
haftmann@34020
|
151 |
lemma [code_unfold]:
|
haftmann@33913
|
152 |
"op \<subseteq> = subset_eq"
|
haftmann@33913
|
153 |
by simp
|
haftmann@33913
|
154 |
|
haftmann@33913
|
155 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
|
haftmann@33913
|
156 |
[simp]: "subset = op \<subset>"
|
haftmann@33913
|
157 |
|
haftmann@34020
|
158 |
lemma [code_unfold]:
|
haftmann@33913
|
159 |
"op \<subset> = subset"
|
haftmann@33913
|
160 |
by simp
|
haftmann@33913
|
161 |
|
haftmann@33913
|
162 |
setup {*
|
haftmann@33913
|
163 |
Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
|
haftmann@33913
|
164 |
#> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
|
haftmann@33913
|
165 |
#> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
|
haftmann@33913
|
166 |
*}
|
haftmann@33913
|
167 |
|
haftmann@33913
|
168 |
lemma set_eq_subset_eq [code]:
|
haftmann@33913
|
169 |
"set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
|
haftmann@33913
|
170 |
by auto
|
haftmann@33913
|
171 |
|
haftmann@33913
|
172 |
lemma subset_eq_forall [code]:
|
haftmann@33913
|
173 |
"subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
|
haftmann@33913
|
174 |
by (simp add: subset_eq)
|
haftmann@33913
|
175 |
|
haftmann@33913
|
176 |
lemma subset_subset_eq [code]:
|
haftmann@33913
|
177 |
"subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
|
haftmann@33913
|
178 |
by (simp add: subset)
|
haftmann@33913
|
179 |
|
haftmann@33913
|
180 |
|
haftmann@33913
|
181 |
subsection {* Functorial operations *}
|
haftmann@33913
|
182 |
|
haftmann@33913
|
183 |
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
|
haftmann@33913
|
184 |
[simp]: "inter = op \<inter>"
|
haftmann@33913
|
185 |
|
haftmann@34020
|
186 |
lemma [code_unfold]:
|
haftmann@33913
|
187 |
"op \<inter> = inter"
|
haftmann@33913
|
188 |
by simp
|
haftmann@33913
|
189 |
|
haftmann@33913
|
190 |
definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
|
haftmann@33913
|
191 |
[simp]: "subtract A B = B - A"
|
haftmann@33913
|
192 |
|
haftmann@34020
|
193 |
lemma [code_unfold]:
|
haftmann@33913
|
194 |
"B - A = subtract A B"
|
haftmann@33913
|
195 |
by simp
|
haftmann@33913
|
196 |
|
haftmann@33913
|
197 |
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
|
haftmann@33913
|
198 |
[simp]: "union = op \<union>"
|
haftmann@33913
|
199 |
|
haftmann@34020
|
200 |
lemma [code_unfold]:
|
haftmann@33913
|
201 |
"op \<union> = union"
|
haftmann@33913
|
202 |
by simp
|
haftmann@33913
|
203 |
|
haftmann@33913
|
204 |
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
|
haftmann@45731
|
205 |
[simp]: "Inf = Complete_Lattices.Inf"
|
haftmann@33913
|
206 |
|
haftmann@34020
|
207 |
lemma [code_unfold]:
|
haftmann@45731
|
208 |
"Complete_Lattices.Inf = Inf"
|
haftmann@33913
|
209 |
by simp
|
haftmann@33913
|
210 |
|
haftmann@33913
|
211 |
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
|
haftmann@45731
|
212 |
[simp]: "Sup = Complete_Lattices.Sup"
|
haftmann@33913
|
213 |
|
haftmann@34020
|
214 |
lemma [code_unfold]:
|
haftmann@45731
|
215 |
"Complete_Lattices.Sup = Sup"
|
haftmann@33913
|
216 |
by simp
|
haftmann@33913
|
217 |
|
haftmann@33913
|
218 |
definition Inter :: "'a set set \<Rightarrow> 'a set" where
|
haftmann@33913
|
219 |
[simp]: "Inter = Inf"
|
haftmann@33913
|
220 |
|
haftmann@34020
|
221 |
lemma [code_unfold]:
|
haftmann@33913
|
222 |
"Inf = Inter"
|
haftmann@33913
|
223 |
by simp
|
haftmann@33913
|
224 |
|
haftmann@33913
|
225 |
definition Union :: "'a set set \<Rightarrow> 'a set" where
|
haftmann@33913
|
226 |
[simp]: "Union = Sup"
|
haftmann@33913
|
227 |
|
haftmann@34020
|
228 |
lemma [code_unfold]:
|
haftmann@33913
|
229 |
"Sup = Union"
|
haftmann@33913
|
230 |
by simp
|
haftmann@33913
|
231 |
|
haftmann@33913
|
232 |
setup {*
|
haftmann@33913
|
233 |
Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@33913
|
234 |
#> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@33913
|
235 |
#> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
|
haftmann@33913
|
236 |
#> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
|
haftmann@33913
|
237 |
#> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
|
haftmann@33913
|
238 |
#> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
|
haftmann@33913
|
239 |
#> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
|
haftmann@33913
|
240 |
*}
|
haftmann@33913
|
241 |
|
haftmann@33913
|
242 |
lemma inter_project [code]:
|
haftmann@33913
|
243 |
"inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
|
haftmann@37015
|
244 |
"inter A (Coset xs) = foldr remove xs A"
|
haftmann@37015
|
245 |
by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
|
haftmann@33913
|
246 |
|
haftmann@33913
|
247 |
lemma subtract_remove [code]:
|
haftmann@37015
|
248 |
"subtract (Set xs) A = foldr remove xs A"
|
haftmann@33913
|
249 |
"subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
|
haftmann@37015
|
250 |
by (auto simp add: minus_set_foldr)
|
haftmann@33913
|
251 |
|
haftmann@33913
|
252 |
lemma union_insert [code]:
|
haftmann@37015
|
253 |
"union (Set xs) A = foldr insert xs A"
|
haftmann@33913
|
254 |
"union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
|
haftmann@37015
|
255 |
by (auto simp add: union_set_foldr)
|
haftmann@33913
|
256 |
|
haftmann@33913
|
257 |
lemma Inf_inf [code]:
|
haftmann@37015
|
258 |
"Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
|
haftmann@33913
|
259 |
"Inf (Coset []) = (bot :: 'a::complete_lattice)"
|
haftmann@45883
|
260 |
by (simp_all add: Inf_set_foldr)
|
haftmann@33913
|
261 |
|
haftmann@33913
|
262 |
lemma Sup_sup [code]:
|
haftmann@37015
|
263 |
"Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
|
haftmann@33913
|
264 |
"Sup (Coset []) = (top :: 'a::complete_lattice)"
|
haftmann@45883
|
265 |
by (simp_all add: Sup_set_foldr)
|
haftmann@33913
|
266 |
|
haftmann@33913
|
267 |
lemma Inter_inter [code]:
|
haftmann@37015
|
268 |
"Inter (Set xs) = foldr inter xs (Coset [])"
|
haftmann@33913
|
269 |
"Inter (Coset []) = empty"
|
haftmann@33913
|
270 |
unfolding Inter_def Inf_inf by simp_all
|
haftmann@33913
|
271 |
|
haftmann@33913
|
272 |
lemma Union_union [code]:
|
haftmann@37015
|
273 |
"Union (Set xs) = foldr union xs empty"
|
haftmann@33913
|
274 |
"Union (Coset []) = Coset []"
|
haftmann@33913
|
275 |
unfolding Union_def Sup_sup by simp_all
|
haftmann@33913
|
276 |
|
wenzelm@36176
|
277 |
hide_const (open) is_empty empty remove
|
haftmann@33913
|
278 |
set_eq subset_eq subset inter union subtract Inf Sup Inter Union
|
haftmann@33913
|
279 |
|
haftmann@38528
|
280 |
|
haftmann@38528
|
281 |
subsection {* Operations on relations *}
|
haftmann@38528
|
282 |
|
haftmann@38528
|
283 |
text {* Initially contributed by Tjark Weber. *}
|
haftmann@38528
|
284 |
|
haftmann@45883
|
285 |
lemma [code]:
|
haftmann@45883
|
286 |
"Domain r = fst ` r"
|
haftmann@45883
|
287 |
by (fact Domain_fst)
|
haftmann@38528
|
288 |
|
haftmann@45883
|
289 |
lemma [code]:
|
haftmann@45883
|
290 |
"Range r = snd ` r"
|
haftmann@45883
|
291 |
by (fact Range_snd)
|
haftmann@38528
|
292 |
|
haftmann@45883
|
293 |
lemma [code]:
|
haftmann@45883
|
294 |
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
|
haftmann@45883
|
295 |
by (fact trans_join)
|
haftmann@38528
|
296 |
|
haftmann@45883
|
297 |
lemma [code]:
|
haftmann@45883
|
298 |
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
|
haftmann@45883
|
299 |
by (fact irrefl_distinct)
|
haftmann@38528
|
300 |
|
haftmann@45883
|
301 |
lemma [code]:
|
haftmann@45883
|
302 |
"acyclic r \<longleftrightarrow> irrefl (r^+)"
|
haftmann@45883
|
303 |
by (fact acyclic_irrefl)
|
haftmann@38528
|
304 |
|
haftmann@45883
|
305 |
lemma [code]:
|
haftmann@45883
|
306 |
"More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
|
haftmann@45883
|
307 |
by (unfold Set_def) (fact product_code)
|
haftmann@38528
|
308 |
|
haftmann@45883
|
309 |
lemma [code]:
|
haftmann@45883
|
310 |
"Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
|
haftmann@45883
|
311 |
by (unfold Set_def) (fact Id_on_set)
|
haftmann@38528
|
312 |
|
haftmann@45883
|
313 |
lemma [code]:
|
haftmann@45883
|
314 |
"Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
|
haftmann@45883
|
315 |
by (unfold Set_def) (fact set_rel_comp)
|
haftmann@38528
|
316 |
|
haftmann@45883
|
317 |
lemma [code]:
|
haftmann@38528
|
318 |
"wf (Set xs) = acyclic (Set xs)"
|
haftmann@45883
|
319 |
by (unfold Set_def) (fact wf_set)
|
haftmann@38528
|
320 |
|
haftmann@33913
|
321 |
end
|