17632
|
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 |
|
18702
|
30 |
code_syntax_tyco set
|
|
31 |
ml ("_ list")
|
18757
|
32 |
haskell (target_atom "[_]")
|
18702
|
33 |
|
|
34 |
code_syntax_const "{}"
|
18757
|
35 |
ml (target_atom "[]")
|
|
36 |
haskell (target_atom "[]")
|
18702
|
37 |
|
17632
|
38 |
consts_code
|
|
39 |
"{}" ("[]")
|
|
40 |
"insert" ("(_ ins _)")
|
|
41 |
"op Un" ("(_ union _)")
|
|
42 |
"op Int" ("(_ inter _)")
|
|
43 |
"op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
|
|
44 |
"image" ("\<module>image")
|
|
45 |
attach {*
|
|
46 |
fun image f S = distinct (map f S);
|
|
47 |
*}
|
|
48 |
"UNION" ("\<module>UNION")
|
|
49 |
attach {*
|
|
50 |
fun UNION S f = Library.foldr Library.union (map f S, []);
|
|
51 |
*}
|
|
52 |
"INTER" ("\<module>INTER")
|
|
53 |
attach {*
|
|
54 |
fun INTER S f = Library.foldr1 Library.inter (map f S);
|
|
55 |
*}
|
|
56 |
"Bex" ("\<module>Bex")
|
|
57 |
attach {*
|
|
58 |
fun Bex S P = Library.exists P S;
|
|
59 |
*}
|
|
60 |
"Ball" ("\<module>Ball")
|
|
61 |
attach {*
|
|
62 |
fun Ball S P = Library.forall P S;
|
|
63 |
*}
|
|
64 |
|
18963
|
65 |
consts
|
|
66 |
flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
|
|
67 |
member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
|
|
68 |
insert_ :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
|
69 |
remove :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
|
70 |
inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
18702
|
71 |
|
18963
|
72 |
defs
|
|
73 |
flip_def: "flip f a b == f b a"
|
|
74 |
member_def: "member xs x == x mem xs"
|
|
75 |
insert_def: "insert_ x xs == if member xs x then xs else x#xs"
|
18702
|
76 |
|
18963
|
77 |
primrec
|
|
78 |
"remove x [] = []"
|
|
79 |
"remove x (y#ys) = (if x = y then ys else y # remove x ys)"
|
18702
|
80 |
|
18963
|
81 |
primrec
|
|
82 |
"inter [] ys = []"
|
|
83 |
"inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
|
|
84 |
|
|
85 |
code_syntax_const "insert"
|
|
86 |
ml ("{*insert_*} _ _")
|
|
87 |
haskell ("{*insert_*} _ _")
|
18702
|
88 |
|
18963
|
89 |
code_syntax_const "op Un"
|
|
90 |
ml ("{*foldr insert_*} _ _")
|
|
91 |
haskell ("{*foldr insert_*} _ _")
|
|
92 |
|
|
93 |
code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
|
|
94 |
ml ("{*(flip o foldr) remove*} _ _")
|
|
95 |
haskell ("{*(flip o foldr) remove*} _ _")
|
|
96 |
|
|
97 |
code_syntax_const "op Int"
|
|
98 |
ml ("{*inter*} _ _")
|
|
99 |
haskell ("{*inter*} _ _")
|
18702
|
100 |
|
18963
|
101 |
code_syntax_const "image"
|
|
102 |
ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
|
|
103 |
haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
|
18702
|
104 |
|
18963
|
105 |
code_syntax_const "INTER"
|
|
106 |
ml ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _")
|
|
107 |
haskell ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _")
|
18851
|
108 |
|
18963
|
109 |
code_syntax_const "UNION"
|
|
110 |
ml ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _")
|
|
111 |
haskell ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _")
|
18702
|
112 |
|
|
113 |
code_primconst "Ball"
|
|
114 |
ml {*
|
18963
|
115 |
fun `_` [] f = true
|
|
116 |
| `_` (x::xs) f = f x andalso `_` xs f;
|
18702
|
117 |
*}
|
|
118 |
haskell {*
|
18963
|
119 |
`_` = flip all
|
18702
|
120 |
*}
|
|
121 |
|
|
122 |
code_primconst "Bex"
|
|
123 |
ml {*
|
18963
|
124 |
fun `_` [] f = false
|
|
125 |
| `_` (x::xs) f = f x orelse `_` xs f;
|
18702
|
126 |
*}
|
|
127 |
haskell {*
|
18963
|
128 |
`_` = flip any
|
18702
|
129 |
*}
|
|
130 |
|
17632
|
131 |
end
|