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