5 |
5 |
6 theory More_Set |
6 theory More_Set |
7 imports Main More_List |
7 imports Main More_List |
8 begin |
8 begin |
9 |
9 |
10 subsection {* Various additional set functions *} |
|
11 |
|
12 definition is_empty :: "'a set \<Rightarrow> bool" where |
|
13 "is_empty A \<longleftrightarrow> A = {}" |
|
14 |
|
15 hide_const (open) is_empty |
|
16 |
|
17 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
18 "remove x A = A - {x}" |
|
19 |
|
20 hide_const (open) remove |
|
21 |
|
22 lemma comp_fun_idem_remove: |
10 lemma comp_fun_idem_remove: |
23 "comp_fun_idem More_Set.remove" |
11 "comp_fun_idem Set.remove" |
24 proof - |
12 proof - |
25 have rem: "More_Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
13 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
26 show ?thesis by (simp only: comp_fun_idem_remove rem) |
14 show ?thesis by (simp only: comp_fun_idem_remove rem) |
27 qed |
15 qed |
28 |
16 |
29 lemma minus_fold_remove: |
17 lemma minus_fold_remove: |
30 assumes "finite A" |
18 assumes "finite A" |
31 shows "B - A = Finite_Set.fold More_Set.remove B A" |
19 shows "B - A = Finite_Set.fold Set.remove B A" |
32 proof - |
20 proof - |
33 have rem: "More_Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
21 have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
34 show ?thesis by (simp only: rem assms minus_fold_remove) |
22 show ?thesis by (simp only: rem assms minus_fold_remove) |
35 qed |
23 qed |
36 |
24 |
37 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
38 "project P A = {a \<in> A. P a}" |
|
39 |
|
40 hide_const (open) project |
|
41 |
|
42 lemma bounded_Collect_code [code_unfold_post]: |
25 lemma bounded_Collect_code [code_unfold_post]: |
43 "{x \<in> A. P x} = More_Set.project P A" |
26 "{x \<in> A. P x} = Set.project P A" |
44 by (simp add: project_def) |
27 by (simp add: project_def) |
45 |
28 |
46 definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where |
|
47 "product A B = Sigma A (\<lambda>_. B)" |
|
48 |
|
49 hide_const (open) product |
|
50 |
|
51 lemma [code_unfold_post]: |
|
52 "Sigma A (\<lambda>_. B) = More_Set.product A B" |
|
53 by (simp add: product_def) |
|
54 |
|
55 |
29 |
56 subsection {* Basic set operations *} |
30 subsection {* Basic set operations *} |
57 |
31 |
58 lemma is_empty_set: |
32 lemma is_empty_set: |
59 "More_Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
33 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
60 by (simp add: is_empty_def null_def) |
34 by (simp add: Set.is_empty_def null_def) |
61 |
35 |
62 lemma empty_set: |
36 lemma empty_set: |
63 "{} = set []" |
37 "{} = set []" |
64 by simp |
38 by simp |
65 |
39 |
66 lemma insert_set_compl: |
40 lemma insert_set_compl: |
67 "insert x (- set xs) = - set (removeAll x xs)" |
41 "insert x (- set xs) = - set (removeAll x xs)" |
68 by auto |
42 by auto |
69 |
43 |
70 lemma remove_set_compl: |
44 lemma remove_set_compl: |
71 "More_Set.remove x (- set xs) = - set (List.insert x xs)" |
45 "Set.remove x (- set xs) = - set (List.insert x xs)" |
72 by (auto simp add: remove_def List.insert_def) |
46 by (auto simp add: remove_def List.insert_def) |
73 |
47 |
74 lemma image_set: |
48 lemma image_set: |
75 "image f (set xs) = set (map f xs)" |
49 "image f (set xs) = set (map f xs)" |
76 by simp |
50 by simp |
77 |
51 |
78 lemma project_set: |
52 lemma project_set: |
79 "More_Set.project P (set xs) = set (filter P xs)" |
53 "Set.project P (set xs) = set (filter P xs)" |
80 by (auto simp add: project_def) |
54 by (auto simp add: project_def) |
81 |
55 |
82 |
56 |
83 subsection {* Functorial set operations *} |
57 subsection {* Functorial set operations *} |
84 |
58 |
97 by auto |
71 by auto |
98 then show ?thesis by (simp add: union_set foldr_fold) |
72 then show ?thesis by (simp add: union_set foldr_fold) |
99 qed |
73 qed |
100 |
74 |
101 lemma minus_set: |
75 lemma minus_set: |
102 "A - set xs = fold More_Set.remove xs A" |
76 "A - set xs = fold Set.remove xs A" |
103 proof - |
77 proof - |
104 interpret comp_fun_idem More_Set.remove |
78 interpret comp_fun_idem Set.remove |
105 by (fact comp_fun_idem_remove) |
79 by (fact comp_fun_idem_remove) |
106 show ?thesis |
80 show ?thesis |
107 by (simp add: minus_fold_remove [of _ A] fold_set) |
81 by (simp add: minus_fold_remove [of _ A] fold_set) |
108 qed |
82 qed |
109 |
83 |
110 lemma minus_set_foldr: |
84 lemma minus_set_foldr: |
111 "A - set xs = foldr More_Set.remove xs A" |
85 "A - set xs = foldr Set.remove xs A" |
112 proof - |
86 proof - |
113 have "\<And>x y :: 'a. More_Set.remove y \<circ> More_Set.remove x = More_Set.remove x \<circ> More_Set.remove y" |
87 have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
114 by (auto simp add: remove_def) |
88 by (auto simp add: remove_def) |
115 then show ?thesis by (simp add: minus_set foldr_fold) |
89 then show ?thesis by (simp add: minus_set foldr_fold) |
116 qed |
90 qed |
117 |
91 |
118 |
92 |
133 lemma set_eq: |
107 lemma set_eq: |
134 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
108 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
135 by (fact eq_iff) |
109 by (fact eq_iff) |
136 |
110 |
137 lemma inter: |
111 lemma inter: |
138 "A \<inter> B = More_Set.project (\<lambda>x. x \<in> A) B" |
112 "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" |
139 by (auto simp add: project_def) |
113 by (auto simp add: project_def) |
140 |
114 |
141 |
115 |
142 subsection {* Theorems on relations *} |
116 subsection {* Theorems on relations *} |
143 |
117 |
144 lemma product_code: |
118 lemma product_code: |
145 "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
119 "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
146 by (auto simp add: product_def) |
120 by (auto simp add: Product_Type.product_def) |
147 |
121 |
148 lemma Id_on_set: |
122 lemma Id_on_set: |
149 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
123 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
150 by (auto simp add: Id_on_def) |
124 by (auto simp add: Id_on_def) |
151 |
125 |
175 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
149 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
176 "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" |
150 "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x" |
177 by (simp_all add: member_def) |
151 by (simp_all add: member_def) |
178 |
152 |
179 lemma [code_unfold]: |
153 lemma [code_unfold]: |
180 "A = {} \<longleftrightarrow> More_Set.is_empty A" |
154 "A = {} \<longleftrightarrow> Set.is_empty A" |
181 by (simp add: is_empty_def) |
155 by (simp add: Set.is_empty_def) |
182 |
156 |
183 declare empty_set [code] |
157 declare empty_set [code] |
184 |
158 |
185 declare is_empty_set [code] |
159 declare is_empty_set [code] |
186 |
160 |
192 "insert x (set xs) = set (List.insert x xs)" |
166 "insert x (set xs) = set (List.insert x xs)" |
193 "insert x (coset xs) = coset (removeAll x xs)" |
167 "insert x (coset xs) = coset (removeAll x xs)" |
194 by simp_all |
168 by simp_all |
195 |
169 |
196 lemma remove_code [code]: |
170 lemma remove_code [code]: |
197 "More_Set.remove x (set xs) = set (removeAll x xs)" |
171 "Set.remove x (set xs) = set (removeAll x xs)" |
198 "More_Set.remove x (coset xs) = coset (List.insert x xs)" |
172 "Set.remove x (coset xs) = coset (List.insert x xs)" |
199 by (simp_all add: remove_def Compl_insert) |
173 by (simp_all add: remove_def Compl_insert) |
200 |
174 |
201 declare image_set [code] |
175 declare image_set [code] |
202 |
176 |
203 declare project_set [code] |
177 declare project_set [code] |
219 qed |
193 qed |
220 |
194 |
221 |
195 |
222 subsection {* Derived operations *} |
196 subsection {* Derived operations *} |
223 |
197 |
224 instantiation set :: (equal) equal |
|
225 begin |
|
226 |
|
227 definition |
|
228 "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
229 |
|
230 instance proof |
|
231 qed (auto simp add: equal_set_def) |
|
232 |
|
233 end |
|
234 |
|
235 declare subset_eq [code] |
198 declare subset_eq [code] |
236 |
199 |
237 declare subset [code] |
200 declare subset [code] |
238 |
201 |
239 |
202 |
240 subsection {* Functorial operations *} |
203 subsection {* Functorial operations *} |
241 |
204 |
242 lemma inter_code [code]: |
205 lemma inter_code [code]: |
243 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
206 "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
244 "A \<inter> coset xs = foldr More_Set.remove xs A" |
207 "A \<inter> coset xs = foldr Set.remove xs A" |
245 by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
208 by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
246 |
209 |
247 lemma subtract_code [code]: |
210 lemma subtract_code [code]: |
248 "A - set xs = foldr More_Set.remove xs A" |
211 "A - set xs = foldr Set.remove xs A" |
249 "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
212 "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" |
250 by (auto simp add: minus_set_foldr) |
213 by (auto simp add: minus_set_foldr) |
251 |
214 |
252 lemma union_code [code]: |
215 lemma union_code [code]: |
253 "set xs \<union> A = foldr insert xs A" |
216 "set xs \<union> A = foldr insert xs A" |