1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Relating (finite) sets and lists *} |
|
5 |
|
6 theory More_Set |
|
7 imports More_List |
|
8 begin |
|
9 |
|
10 lemma comp_fun_idem_remove: |
|
11 "comp_fun_idem Set.remove" |
|
12 proof - |
|
13 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
|
14 show ?thesis by (simp only: comp_fun_idem_remove rem) |
|
15 qed |
|
16 |
|
17 lemma minus_fold_remove: |
|
18 assumes "finite A" |
|
19 shows "B - A = Finite_Set.fold Set.remove B A" |
|
20 proof - |
|
21 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
|
22 show ?thesis by (simp only: rem assms minus_fold_remove) |
|
23 qed |
|
24 |
|
25 lemma bounded_Collect_code: (* FIXME delete candidate *) |
|
26 "{x \<in> A. P x} = Set.project P A" |
|
27 by (simp add: project_def) |
|
28 |
|
29 |
|
30 subsection {* Basic set operations *} |
|
31 |
|
32 lemma is_empty_set: |
|
33 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
|
34 by (simp add: Set.is_empty_def null_def) |
|
35 |
|
36 lemma empty_set: |
|
37 "{} = set []" |
|
38 by simp |
|
39 |
|
40 lemma insert_set_compl: |
|
41 "insert x (- set xs) = - set (removeAll x xs)" |
|
42 by auto |
|
43 |
|
44 lemma remove_set_compl: |
|
45 "Set.remove x (- set xs) = - set (List.insert x xs)" |
|
46 by (auto simp add: remove_def List.insert_def) |
|
47 |
|
48 lemma image_set: |
|
49 "image f (set xs) = set (map f xs)" |
|
50 by simp |
|
51 |
|
52 lemma project_set: |
|
53 "Set.project P (set xs) = set (filter P xs)" |
|
54 by (auto simp add: project_def) |
|
55 |
|
56 |
|
57 subsection {* Functorial set operations *} |
|
58 |
|
59 lemma union_set: |
|
60 "set xs \<union> A = fold Set.insert xs A" |
|
61 proof - |
|
62 interpret comp_fun_idem Set.insert |
|
63 by (fact comp_fun_idem_insert) |
|
64 show ?thesis by (simp add: union_fold_insert fold_set_fold) |
|
65 qed |
|
66 |
|
67 lemma union_set_foldr: |
|
68 "set xs \<union> A = foldr Set.insert xs A" |
|
69 proof - |
|
70 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
|
71 by auto |
|
72 then show ?thesis by (simp add: union_set foldr_fold) |
|
73 qed |
|
74 |
|
75 lemma minus_set: |
|
76 "A - set xs = fold Set.remove xs A" |
|
77 proof - |
|
78 interpret comp_fun_idem Set.remove |
|
79 by (fact comp_fun_idem_remove) |
|
80 show ?thesis |
|
81 by (simp add: minus_fold_remove [of _ A] fold_set_fold) |
|
82 qed |
|
83 |
|
84 lemma minus_set_foldr: |
|
85 "A - set xs = foldr Set.remove xs A" |
|
86 proof - |
|
87 have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
|
88 by (auto simp add: remove_def) |
|
89 then show ?thesis by (simp add: minus_set foldr_fold) |
|
90 qed |
|
91 |
|
92 |
|
93 subsection {* Derived set operations *} |
|
94 |
|
95 lemma member: |
|
96 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
|
97 by simp |
|
98 |
|
99 lemma subset_eq: |
|
100 "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
101 by (fact subset_eq) |
|
102 |
|
103 lemma subset: |
|
104 "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
|
105 by (fact less_le_not_le) |
|
106 |
|
107 lemma set_eq: |
|
108 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
109 by (fact eq_iff) |
|
110 |
|
111 lemma inter: |
|
112 "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" |
|
113 by (auto simp add: project_def) |
|
114 |
|
115 |
|
116 subsection {* Theorems on relations *} |
|
117 |
|
118 lemma product_code: |
|
119 "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
|
120 by (auto simp add: Product_Type.product_def) |
|
121 |
|
122 lemma Id_on_set: |
|
123 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
|
124 by (auto simp add: Id_on_def) |
|
125 |
|
126 lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
|
127 by (simp add: finite_trancl_ntranl) |
|
128 |
|
129 lemma set_rel_comp: |
|
130 "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
|
131 by (auto simp add: Bex_def) |
|
132 |
|
133 lemma wf_set: |
|
134 "wf (set xs) = acyclic (set xs)" |
|
135 by (simp add: wf_iff_acyclic_if_finite) |
|
136 |
|
137 |
|
138 subsection {* Code generator setup *} |
|
139 |
|
140 definition coset :: "'a list \<Rightarrow> 'a set" where |
|
141 [simp]: "coset xs = - set xs" |
|
142 |
|
143 code_datatype set coset |
|
144 |
|
145 |
|
146 subsection {* Basic operations *} |
|
147 |
|
148 lemma [code]: |
|
149 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
|
150 "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" |
|
151 by (simp_all add: member_def) |
|
152 |
|
153 lemma [code_unfold]: |
|
154 "A = {} \<longleftrightarrow> Set.is_empty A" |
|
155 by (simp add: Set.is_empty_def) |
|
156 |
|
157 declare empty_set [code] |
|
158 |
|
159 declare is_empty_set [code] |
|
160 |
|
161 lemma UNIV_coset [code]: |
|
162 "UNIV = coset []" |
|
163 by simp |
|
164 |
|
165 lemma insert_code [code]: |
|
166 "insert x (set xs) = set (List.insert x xs)" |
|
167 "insert x (coset xs) = coset (removeAll x xs)" |
|
168 by simp_all |
|
169 |
|
170 lemma remove_code [code]: |
|
171 "Set.remove x (set xs) = set (removeAll x xs)" |
|
172 "Set.remove x (coset xs) = coset (List.insert x xs)" |
|
173 by (simp_all add: remove_def Compl_insert) |
|
174 |
|
175 declare image_set [code] |
|
176 |
|
177 declare project_set [code] |
|
178 |
|
179 lemma Ball_set [code]: |
|
180 "Ball (set xs) P \<longleftrightarrow> list_all P xs" |
|
181 by (simp add: list_all_iff) |
|
182 |
|
183 lemma Bex_set [code]: |
|
184 "Bex (set xs) P \<longleftrightarrow> list_ex P xs" |
|
185 by (simp add: list_ex_iff) |
|
186 |
|
187 lemma card_set [code]: |
|
188 "card (set xs) = length (remdups xs)" |
|
189 proof - |
|
190 have "card (set (remdups xs)) = length (remdups xs)" |
|
191 by (rule distinct_card) simp |
|
192 then show ?thesis by simp |
|
193 qed |
|
194 |
|
195 |
|
196 subsection {* Derived operations *} |
|
197 |
|
198 declare subset_eq [code] |
|
199 |
|
200 declare subset [code] |
|
201 |
|
202 |
|
203 subsection {* Functorial operations *} |
|
204 |
|
205 lemma inter_code [code]: |
|
206 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
207 "A \<inter> coset xs = foldr Set.remove xs A" |
|
208 by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
|
209 |
|
210 lemma subtract_code [code]: |
|
211 "A - set xs = foldr Set.remove xs A" |
|
212 "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
213 by (auto simp add: minus_set_foldr) |
|
214 |
|
215 lemma union_code [code]: |
|
216 "set xs \<union> A = foldr insert xs A" |
|
217 "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
|
218 by (auto simp add: union_set_foldr) |
|
219 |
|
220 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
221 [simp, code_abbrev]: "Inf = Complete_Lattices.Inf" |
|
222 |
|
223 hide_const (open) Inf |
|
224 |
|
225 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
226 [simp, code_abbrev]: "Sup = Complete_Lattices.Sup" |
|
227 |
|
228 hide_const (open) Sup |
|
229 |
|
230 lemma Inf_code [code]: |
|
231 "More_Set.Inf (set xs) = foldr inf xs top" |
|
232 "More_Set.Inf (coset []) = bot" |
|
233 by (simp_all add: Inf_set_foldr) |
|
234 |
|
235 lemma Sup_sup [code]: |
|
236 "More_Set.Sup (set xs) = foldr sup xs bot" |
|
237 "More_Set.Sup (coset []) = top" |
|
238 by (simp_all add: Sup_set_foldr) |
|
239 |
|
240 lemma INF_code [code]: |
|
241 "INFI (set xs) f = foldr (inf \<circ> f) xs top" |
|
242 by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map) |
|
243 |
|
244 lemma SUP_sup [code]: |
|
245 "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" |
|
246 by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map) |
|
247 |
|
248 (* FIXME: better implement conversion by bisection *) |
|
249 |
|
250 lemma pred_of_set_fold_sup: |
|
251 assumes "finite A" |
|
252 shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") |
|
253 proof (rule sym) |
|
254 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
255 by (fact comp_fun_idem_sup) |
|
256 from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) |
|
257 qed |
|
258 |
|
259 lemma pred_of_set_set_fold_sup: |
|
260 "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot" |
|
261 proof - |
|
262 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" |
|
263 by (fact comp_fun_idem_sup) |
|
264 show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) |
|
265 qed |
|
266 |
|
267 lemma pred_of_set_set_foldr_sup [code]: |
|
268 "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot" |
|
269 by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) |
|
270 |
|
271 hide_const (open) coset |
|
272 |
|
273 |
|
274 subsection {* Operations on relations *} |
|
275 |
|
276 text {* Initially contributed by Tjark Weber. *} |
|
277 |
|
278 declare Domain_fst [code] |
|
279 |
|
280 declare Range_snd [code] |
|
281 |
|
282 declare trans_join [code] |
|
283 |
|
284 declare irrefl_distinct [code] |
|
285 |
|
286 declare trancl_set_ntrancl [code] |
|
287 |
|
288 declare acyclic_irrefl [code] |
|
289 |
|
290 declare product_code [code] |
|
291 |
|
292 declare Id_on_set [code] |
|
293 |
|
294 declare set_rel_comp [code] |
|
295 |
|
296 declare wf_set [code] |
|
297 |
|
298 end |
|
299 |
|