11 |
11 |
12 section {* Definitional rewrites *} |
12 section {* Definitional rewrites *} |
13 |
13 |
14 instance set :: (eq) eq .. |
14 instance set :: (eq) eq .. |
15 |
15 |
|
16 definition |
|
17 minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
18 "minus_set xs ys = ys - xs" |
|
19 |
|
20 lemma [code inline]: |
|
21 "op - = (\<lambda>xs ys. minus_set ys xs)" |
|
22 unfolding minus_set_def .. |
|
23 |
|
24 definition |
|
25 subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
26 subset_def: "subset = op \<subseteq>" |
|
27 |
|
28 lemmas [symmetric, code inline] = subset_def |
|
29 |
16 lemma [code target: Set]: |
30 lemma [code target: Set]: |
17 "(A = B) \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)" |
31 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
18 by blast |
32 by blast |
19 |
33 |
20 lemma [code func]: |
34 lemma [code func]: |
21 "Code_Generator.eq A B \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)" |
35 "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A" |
22 unfolding eq_def by blast |
36 unfolding eq_def subset_def by blast |
|
37 |
|
38 lemma [code func]: |
|
39 "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
40 unfolding subset_def Set.subset_def .. |
23 |
41 |
24 lemma [code]: |
42 lemma [code]: |
25 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)" |
43 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)" |
26 unfolding bex_triv_one_point1 .. |
44 unfolding bex_triv_one_point1 .. |
27 |
45 |
28 |
46 definition |
29 section {* HOL definitions *} |
47 filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
48 filter_set_def: "filter_set P xs = {x\<in>xs. P x}" |
|
49 |
|
50 lemmas [symmetric, code inline] = filter_set_def |
|
51 |
|
52 |
|
53 section {* Operations on lists *} |
30 |
54 |
31 subsection {* Basic definitions *} |
55 subsection {* Basic definitions *} |
32 |
56 |
33 definition |
57 definition |
34 flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" |
58 flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" |
167 unfolding insertl_def iso_member by (simp add: Set.insert_absorb) |
191 unfolding insertl_def iso_member by (simp add: Set.insert_absorb) |
168 |
192 |
169 lemma iso_remove1: |
193 lemma iso_remove1: |
170 assumes distnct: "distinct xs" |
194 assumes distnct: "distinct xs" |
171 shows "set (remove1 x xs) = set xs - {x}" |
195 shows "set (remove1 x xs) = set xs - {x}" |
172 using distnct set_remove1_eq by auto |
196 using distnct set_remove1_eq by auto |
173 |
197 |
174 lemma iso_union: |
198 lemma iso_union: |
175 "set (unionl xs ys) = set xs \<union> set ys" |
199 "set (unionl xs ys) = set xs \<union> set ys" |
176 unfolding unionl_def |
200 unfolding unionl_def |
177 by (induct xs arbitrary: ys) (simp_all add: iso_insert) |
201 by (induct xs arbitrary: ys) (simp_all add: iso_insert) |
178 |
202 |
179 lemma iso_intersect: |
203 lemma iso_intersect: |
180 "set (intersect xs ys) = set xs \<inter> set ys" |
204 "set (intersect xs ys) = set xs \<inter> set ys" |
181 unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto |
205 unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto |
182 |
206 |
183 lemma iso_subtract: |
207 lemma iso_subtract: |
184 fixes ys |
208 fixes ys |
185 assumes distnct: "distinct ys" |
209 assumes distnct: "distinct ys" |
186 shows "set (subtract xs ys) = set ys - set xs" |
210 shows "set (subtract xs ys) = minus_set (set xs) (set ys)" |
187 and "distinct (subtract xs ys)" |
211 and "distinct (subtract xs ys)" |
188 unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto) |
212 unfolding subtract_def minus_set_def |
189 |
213 using distnct by (induct xs arbitrary: ys) auto |
190 corollary iso_subtract': |
|
191 fixes xs ys |
|
192 assumes distnct: "distinct xs" |
|
193 shows "set ((flip subtract) xs ys) = set xs - set ys" |
|
194 proof - |
|
195 from distnct iso_subtract have "set (subtract ys xs) = set xs - set ys" by auto |
|
196 thus ?thesis unfolding flip_def by auto |
|
197 qed |
|
198 |
214 |
199 lemma iso_map_distinct: |
215 lemma iso_map_distinct: |
200 "set (map_distinct f xs) = image f (set xs)" |
216 "set (map_distinct f xs) = image f (set xs)" |
201 unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) |
217 unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) |
202 |
218 |
232 |
248 |
233 lemma iso_Bex: |
249 lemma iso_Bex: |
234 "Blex xs f = Bex (set xs) f" |
250 "Blex xs f = Bex (set xs) f" |
235 unfolding Blex_def flip_def by (induct xs) simp_all |
251 unfolding Blex_def flip_def by (induct xs) simp_all |
236 |
252 |
|
253 lemma iso_filter: |
|
254 "set (filter P xs) = filter_set P (set xs)" |
|
255 unfolding filter_set_def by (induct xs) auto |
237 |
256 |
238 section {* code generator setup *} |
257 section {* code generator setup *} |
239 |
258 |
240 ML {* |
259 ML {* |
241 nonfix inter; |
260 nonfix inter; |
242 nonfix union; |
261 nonfix union; |
243 *} |
262 *} |
244 |
263 |
245 code_modulename SML |
264 code_modulename SML |
246 ExecutableSet List |
265 ExecutableSet List |
|
266 Set List |
|
267 |
|
268 code_modulename Haskell |
|
269 ExecutableSet List |
|
270 Set List |
247 |
271 |
248 definition [code inline]: |
272 definition [code inline]: |
249 "empty_list = []" |
273 "empty_list = []" |
250 |
274 |
251 lemma [code func]: |
275 lemma [code func]: |
272 lemma [code func]: |
296 lemma [code func]: |
273 "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" .. |
297 "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" .. |
274 |
298 |
275 lemma [code func]: |
299 lemma [code func]: |
276 "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" .. |
300 "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" .. |
|
301 |
|
302 lemma [code func]: |
|
303 "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" .. |
277 |
304 |
278 code_abstype "'a set" "'a list" where |
305 code_abstype "'a set" "'a list" where |
279 "{}" \<equiv> empty_list |
306 "{}" \<equiv> empty_list |
280 insert \<equiv> insertl |
307 insert \<equiv> insertl |
281 "op \<union>" \<equiv> unionl |
308 "op \<union>" \<equiv> unionl |
282 "op \<inter>" \<equiv> intersect |
309 "op \<inter>" \<equiv> intersect |
283 "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract' |
310 minus_set \<equiv> subtract |
284 image \<equiv> map_distinct |
311 image \<equiv> map_distinct |
285 Union \<equiv> unions |
312 Union \<equiv> unions |
286 Inter \<equiv> intersects |
313 Inter \<equiv> intersects |
287 UNION \<equiv> map_union |
314 UNION \<equiv> map_union |
288 INTER \<equiv> map_inter |
315 INTER \<equiv> map_inter |
289 Ball \<equiv> Blall |
316 Ball \<equiv> Blall |
290 Bex \<equiv> Blex |
317 Bex \<equiv> Blex |
291 |
318 filter_set \<equiv> filter |
292 code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
319 |
293 image Union Inter UNION INTER Ball Bex (SML -) |
320 code_gen "{}" insert "op \<union>" "op \<inter>" minus_set |
|
321 image Union Inter UNION INTER Ball Bex filter_set (SML -) |
294 |
322 |
295 |
323 |
296 subsection {* type serializations *} |
324 subsection {* type serializations *} |
297 |
325 |
298 types_code |
326 types_code |