|
1 (* Title: HOL/Library/ExecutableSet.thy |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Implementation of finite sets by lists *} |
|
7 |
|
8 theory ExecutableSet |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 lemma [code target: Set]: "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)" |
|
13 by blast |
|
14 |
|
15 declare bex_triv_one_point1 [symmetric, standard, code] |
|
16 |
|
17 types_code |
|
18 set ("_ list") |
|
19 attach (term_of) {* |
|
20 fun term_of_set f T [] = Const ("{}", Type ("set", [T])) |
|
21 | term_of_set f T (x :: xs) = Const ("insert", |
|
22 T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; |
|
23 *} |
|
24 attach (test) {* |
|
25 fun gen_set' aG i j = frequency |
|
26 [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () |
|
27 and gen_set aG i = gen_set' aG i i; |
|
28 *} |
|
29 |
|
30 consts_code |
|
31 "{}" ("[]") |
|
32 "insert" ("(_ ins _)") |
|
33 "op Un" ("(_ union _)") |
|
34 "op Int" ("(_ inter _)") |
|
35 "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)") |
|
36 "image" ("\<module>image") |
|
37 attach {* |
|
38 fun image f S = distinct (map f S); |
|
39 *} |
|
40 "UNION" ("\<module>UNION") |
|
41 attach {* |
|
42 fun UNION S f = Library.foldr Library.union (map f S, []); |
|
43 *} |
|
44 "INTER" ("\<module>INTER") |
|
45 attach {* |
|
46 fun INTER S f = Library.foldr1 Library.inter (map f S); |
|
47 *} |
|
48 "Bex" ("\<module>Bex") |
|
49 attach {* |
|
50 fun Bex S P = Library.exists P S; |
|
51 *} |
|
52 "Ball" ("\<module>Ball") |
|
53 attach {* |
|
54 fun Ball S P = Library.forall P S; |
|
55 *} |
|
56 |
|
57 end |