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 *) |
4 *) |
4 |
5 |
5 header {* Implementation of finite sets by lists *} |
6 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} |
6 |
7 |
7 theory Executable_Set |
8 theory Executable_Set |
8 imports Main Fset SML_Quickcheck |
9 imports List_Set |
9 begin |
10 begin |
10 |
11 |
11 subsection {* Preprocessor setup *} |
12 declare mem_def [code del] |
12 |
13 declare Collect_def [code del] |
13 declare member [code] |
14 declare insert_code [code del] |
|
15 declare vimage_code [code del] |
|
16 |
|
17 subsection {* Set representation *} |
|
18 |
|
19 setup {* |
|
20 Code.add_type_cmd "set" |
|
21 *} |
|
22 |
|
23 definition Set :: "'a list \<Rightarrow> 'a set" where |
|
24 [simp]: "Set = set" |
|
25 |
|
26 definition Coset :: "'a list \<Rightarrow> 'a set" where |
|
27 [simp]: "Coset xs = - set xs" |
|
28 |
|
29 setup {* |
|
30 Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set") |
|
31 #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set") |
|
32 #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set") |
|
33 #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool") |
|
34 *} |
|
35 |
|
36 code_datatype Set Coset |
|
37 |
|
38 consts_code |
|
39 Coset ("\<module>Coset") |
|
40 Set ("\<module>Set") |
|
41 attach {* |
|
42 datatype 'a set = Set of 'a list | Coset of 'a list; |
|
43 *} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *} |
|
44 |
|
45 |
|
46 subsection {* Basic operations *} |
|
47 |
|
48 lemma [code]: |
|
49 "set xs = Set (remdups xs)" |
|
50 by simp |
|
51 |
|
52 lemma [code]: |
|
53 "x \<in> Set xs \<longleftrightarrow> member x xs" |
|
54 "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs" |
|
55 by (simp_all add: mem_iff) |
|
56 |
|
57 definition is_empty :: "'a set \<Rightarrow> bool" where |
|
58 [simp]: "is_empty A \<longleftrightarrow> A = {}" |
|
59 |
|
60 lemma [code_unfold]: |
|
61 "A = {} \<longleftrightarrow> is_empty A" |
|
62 by simp |
14 |
63 |
15 definition empty :: "'a set" where |
64 definition empty :: "'a set" where |
16 "empty = {}" |
65 [simp]: "empty = {}" |
17 |
66 |
18 declare empty_def [symmetric, code_unfold] |
67 lemma [code_unfold]: |
|
68 "{} = empty" |
|
69 by simp |
|
70 |
|
71 lemma [code_unfold, code_inline del]: |
|
72 "empty = Set []" |
|
73 by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *} |
|
74 |
|
75 setup {* |
|
76 Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool") |
|
77 #> Code.add_signature_cmd ("empty", "'a set") |
|
78 #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
79 #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
80 #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set") |
|
81 #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
82 #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
|
83 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
|
84 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat") |
|
85 *} |
|
86 |
|
87 lemma is_empty_Set [code]: |
|
88 "is_empty (Set xs) \<longleftrightarrow> null xs" |
|
89 by (simp add: empty_null) |
|
90 |
|
91 lemma empty_Set [code]: |
|
92 "empty = Set []" |
|
93 by simp |
|
94 |
|
95 lemma insert_Set [code]: |
|
96 "insert x (Set xs) = Set (List_Set.insert x xs)" |
|
97 "insert x (Coset xs) = Coset (remove_all x xs)" |
|
98 by (simp_all add: insert_set insert_set_compl) |
|
99 |
|
100 lemma remove_Set [code]: |
|
101 "remove x (Set xs) = Set (remove_all x xs)" |
|
102 "remove x (Coset xs) = Coset (List_Set.insert x xs)" |
|
103 by (simp_all add:remove_set remove_set_compl) |
|
104 |
|
105 lemma image_Set [code]: |
|
106 "image f (Set xs) = Set (remdups (map f xs))" |
|
107 by simp |
|
108 |
|
109 lemma project_Set [code]: |
|
110 "project P (Set xs) = Set (filter P xs)" |
|
111 by (simp add: project_set) |
|
112 |
|
113 lemma Ball_Set [code]: |
|
114 "Ball (Set xs) P \<longleftrightarrow> list_all P xs" |
|
115 by (simp add: ball_set) |
|
116 |
|
117 lemma Bex_Set [code]: |
|
118 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
|
119 by (simp add: bex_set) |
|
120 |
|
121 lemma card_Set [code]: |
|
122 "card (Set xs) = length (remdups xs)" |
|
123 proof - |
|
124 have "card (set (remdups xs)) = length (remdups xs)" |
|
125 by (rule distinct_card) simp |
|
126 then show ?thesis by simp |
|
127 qed |
|
128 |
|
129 |
|
130 subsection {* Derived operations *} |
|
131 |
|
132 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
133 [simp]: "set_eq = op =" |
|
134 |
|
135 lemma [code_unfold]: |
|
136 "op = = set_eq" |
|
137 by simp |
|
138 |
|
139 definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
140 [simp]: "subset_eq = op \<subseteq>" |
|
141 |
|
142 lemma [code_unfold]: |
|
143 "op \<subseteq> = subset_eq" |
|
144 by simp |
|
145 |
|
146 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
147 [simp]: "subset = op \<subset>" |
|
148 |
|
149 lemma [code_unfold]: |
|
150 "op \<subset> = subset" |
|
151 by simp |
|
152 |
|
153 setup {* |
|
154 Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
155 #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
156 #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
157 *} |
|
158 |
|
159 lemma set_eq_subset_eq [code]: |
|
160 "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A" |
|
161 by auto |
|
162 |
|
163 lemma subset_eq_forall [code]: |
|
164 "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
165 by (simp add: subset_eq) |
|
166 |
|
167 lemma subset_subset_eq [code]: |
|
168 "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A" |
|
169 by (simp add: subset) |
|
170 |
|
171 |
|
172 subsection {* Functorial operations *} |
19 |
173 |
20 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
174 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
21 "inter = op \<inter>" |
175 [simp]: "inter = op \<inter>" |
22 |
176 |
23 declare inter_def [symmetric, code_unfold] |
177 lemma [code_unfold]: |
|
178 "op \<inter> = inter" |
|
179 by simp |
|
180 |
|
181 definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
182 [simp]: "subtract A B = B - A" |
|
183 |
|
184 lemma [code_unfold]: |
|
185 "B - A = subtract A B" |
|
186 by simp |
24 |
187 |
25 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
188 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
26 "union = op \<union>" |
189 [simp]: "union = op \<union>" |
27 |
190 |
28 declare union_def [symmetric, code_unfold] |
191 lemma [code_unfold]: |
29 |
192 "op \<union> = union" |
30 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
193 by simp |
31 "subset = op \<le>" |
194 |
32 |
195 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
33 declare subset_def [symmetric, code_unfold] |
196 [simp]: "Inf = Complete_Lattice.Inf" |
34 |
197 |
35 lemma [code]: |
198 lemma [code_unfold]: |
36 "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
199 "Complete_Lattice.Inf = Inf" |
37 by (simp add: subset_def subset_eq) |
200 by simp |
38 |
201 |
39 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
202 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
40 [code del]: "eq_set = op =" |
203 [simp]: "Sup = Complete_Lattice.Sup" |
41 |
204 |
42 (*declare eq_set_def [symmetric, code_unfold]*) |
205 lemma [code_unfold]: |
43 |
206 "Complete_Lattice.Sup = Sup" |
44 lemma [code]: |
207 by simp |
45 "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
46 by (simp add: eq_set_def set_eq) |
|
47 |
|
48 declare inter [code] |
|
49 |
|
50 declare List_Set.project_def [symmetric, code_unfold] |
|
51 |
208 |
52 definition Inter :: "'a set set \<Rightarrow> 'a set" where |
209 definition Inter :: "'a set set \<Rightarrow> 'a set" where |
53 "Inter = Complete_Lattice.Inter" |
210 [simp]: "Inter = Inf" |
54 |
211 |
55 declare Inter_def [symmetric, code_unfold] |
212 lemma [code_unfold]: |
|
213 "Inf = Inter" |
|
214 by simp |
56 |
215 |
57 definition Union :: "'a set set \<Rightarrow> 'a set" where |
216 definition Union :: "'a set set \<Rightarrow> 'a set" where |
58 "Union = Complete_Lattice.Union" |
217 [simp]: "Union = Sup" |
59 |
218 |
60 declare Union_def [symmetric, code_unfold] |
219 lemma [code_unfold]: |
61 |
220 "Sup = Union" |
62 |
221 by simp |
63 subsection {* Code generator setup *} |
222 |
64 |
223 setup {* |
65 ML {* |
224 Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
66 nonfix inter; |
225 #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
67 nonfix union; |
226 #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
68 nonfix subset; |
227 #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a") |
69 *} |
228 #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a") |
70 |
229 #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set") |
71 definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
230 #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set") |
72 "flip f a b = f b a" |
231 *} |
73 |
232 |
74 types_code |
233 lemma inter_project [code]: |
75 fset ("(_/ \<module>fset)") |
234 "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
76 attach {* |
235 "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs" |
77 datatype 'a fset = Set of 'a list | Coset of 'a list; |
236 by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) |
78 *} |
237 |
79 |
238 lemma subtract_remove [code]: |
80 consts_code |
239 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
81 Set ("\<module>Set") |
240 "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
82 Coset ("\<module>Coset") |
241 by (auto simp add: minus_set) |
83 |
242 |
84 consts_code |
243 lemma union_insert [code]: |
85 "empty" ("{*Fset.empty*}") |
244 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
86 "List_Set.is_empty" ("{*Fset.is_empty*}") |
245 "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
87 "Set.insert" ("{*Fset.insert*}") |
246 by (auto simp add: union_set) |
88 "List_Set.remove" ("{*Fset.remove*}") |
247 |
89 "Set.image" ("{*Fset.map*}") |
248 lemma Inf_inf [code]: |
90 "List_Set.project" ("{*Fset.filter*}") |
249 "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" |
91 "Ball" ("{*flip Fset.forall*}") |
250 "Inf (Coset []) = (bot :: 'a::complete_lattice)" |
92 "Bex" ("{*flip Fset.exists*}") |
251 by (simp_all add: Inf_UNIV Inf_set_fold) |
93 "union" ("{*Fset.union*}") |
252 |
94 "inter" ("{*Fset.inter*}") |
253 lemma Sup_sup [code]: |
95 "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}") |
254 "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" |
96 "Union" ("{*Fset.Union*}") |
255 "Sup (Coset []) = (top :: 'a::complete_lattice)" |
97 "Inter" ("{*Fset.Inter*}") |
256 by (simp_all add: Sup_UNIV Sup_set_fold) |
98 card ("{*Fset.card*}") |
257 |
99 fold ("{*foldl o flip*}") |
258 lemma Inter_inter [code]: |
100 |
259 "Inter (Set xs) = foldl inter (Coset []) xs" |
101 hide (open) const empty inter union subset eq_set Inter Union flip |
260 "Inter (Coset []) = empty" |
|
261 unfolding Inter_def Inf_inf by simp_all |
|
262 |
|
263 lemma Union_union [code]: |
|
264 "Union (Set xs) = foldl union empty xs" |
|
265 "Union (Coset []) = Coset []" |
|
266 unfolding Union_def Sup_sup by simp_all |
|
267 |
|
268 hide (open) const is_empty empty remove |
|
269 set_eq subset_eq subset inter union subtract Inf Sup Inter Union |
102 |
270 |
103 end |
271 end |