author | haftmann |
Mon, 26 Dec 2011 18:32:43 +0100 | |
changeset 45986 | c9e50153e5ae |
parent 45974 | 2b043ed911ac |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
4 |
header {* Relating (finite) sets and lists *} |
|
5 |
||
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
6 |
theory More_Set |
37023 | 7 |
imports Main More_List |
31807 | 8 |
begin |
9 |
||
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
10 |
lemma comp_fun_idem_remove: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
11 |
"comp_fun_idem Set.remove" |
31807 | 12 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
13 |
have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
14 |
show ?thesis by (simp only: comp_fun_idem_remove rem) |
31807 | 15 |
qed |
16 |
||
17 |
lemma minus_fold_remove: |
|
18 |
assumes "finite A" |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
19 |
shows "B - A = Finite_Set.fold Set.remove B A" |
31807 | 20 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
21 |
have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
31807 | 22 |
show ?thesis by (simp only: rem assms minus_fold_remove) |
23 |
qed |
|
24 |
||
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
25 |
lemma bounded_Collect_code [code_unfold_post]: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
26 |
"{x \<in> A. P x} = Set.project P A" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
27 |
by (simp add: project_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
28 |
|
31807 | 29 |
|
30 |
subsection {* Basic set operations *} |
|
31 |
||
32 |
lemma is_empty_set: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
33 |
"Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
34 |
by (simp add: Set.is_empty_def null_def) |
31807 | 35 |
|
36 |
lemma empty_set: |
|
37 |
"{} = set []" |
|
38 |
by simp |
|
39 |
||
32880 | 40 |
lemma insert_set_compl: |
34977 | 41 |
"insert x (- set xs) = - set (removeAll x xs)" |
42 |
by auto |
|
31807 | 43 |
|
32880 | 44 |
lemma remove_set_compl: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
45 |
"Set.remove x (- set xs) = - set (List.insert x xs)" |
44326 | 46 |
by (auto simp add: remove_def List.insert_def) |
32880 | 47 |
|
31807 | 48 |
lemma image_set: |
31846 | 49 |
"image f (set xs) = set (map f xs)" |
31807 | 50 |
by simp |
51 |
||
52 |
lemma project_set: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
53 |
"Set.project P (set xs) = set (filter P xs)" |
31807 | 54 |
by (auto simp add: project_def) |
55 |
||
56 |
||
57 |
subsection {* Functorial set operations *} |
|
58 |
||
59 |
lemma union_set: |
|
37023 | 60 |
"set xs \<union> A = fold Set.insert xs A" |
31807 | 61 |
proof - |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
62 |
interpret comp_fun_idem Set.insert |
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
63 |
by (fact comp_fun_idem_insert) |
31807 | 64 |
show ?thesis by (simp add: union_fold_insert fold_set) |
65 |
qed |
|
66 |
||
37023 | 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" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
71 |
by auto |
37023 | 72 |
then show ?thesis by (simp add: union_set foldr_fold) |
73 |
qed |
|
74 |
||
31807 | 75 |
lemma minus_set: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
76 |
"A - set xs = fold Set.remove xs A" |
31807 | 77 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
78 |
interpret comp_fun_idem Set.remove |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
79 |
by (fact comp_fun_idem_remove) |
31807 | 80 |
show ?thesis |
81 |
by (simp add: minus_fold_remove [of _ A] fold_set) |
|
82 |
qed |
|
83 |
||
37023 | 84 |
lemma minus_set_foldr: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
85 |
"A - set xs = foldr Set.remove xs A" |
37023 | 86 |
proof - |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
87 |
have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
88 |
by (auto simp add: remove_def) |
37023 | 89 |
then show ?thesis by (simp add: minus_set foldr_fold) |
90 |
qed |
|
91 |
||
31807 | 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: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
112 |
"A \<inter> B = Set.project (\<lambda>x. x \<in> A) B" |
31807 | 113 |
by (auto simp add: project_def) |
114 |
||
37023 | 115 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
116 |
subsection {* Theorems on relations *} |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
117 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
118 |
lemma product_code: |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
119 |
"Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
120 |
by (auto simp add: Product_Type.product_def) |
37023 | 121 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
122 |
lemma Id_on_set: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
123 |
"Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
124 |
by (auto simp add: Id_on_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
125 |
|
45974 | 126 |
lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
127 |
by (simp add: finite_trancl_ntranl) |
|
128 |
||
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
129 |
lemma set_rel_comp: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
130 |
"set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
131 |
by (auto simp add: Bex_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
132 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
133 |
lemma wf_set: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
134 |
"wf (set xs) = acyclic (set xs)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
135 |
by (simp add: wf_iff_acyclic_if_finite) |
37023 | 136 |
|
45974 | 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]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
154 |
"A = {} \<longleftrightarrow> Set.is_empty A" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
155 |
by (simp add: Set.is_empty_def) |
45974 | 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]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
171 |
"Set.remove x (set xs) = set (removeAll x xs)" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
172 |
"Set.remove x (coset xs) = coset (List.insert x xs)" |
45974 | 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)" |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
207 |
"A \<inter> coset xs = foldr Set.remove xs A" |
45974 | 208 |
by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
209 |
||
210 |
lemma subtract_code [code]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45974
diff
changeset
|
211 |
"A - set xs = foldr Set.remove xs A" |
45974 | 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]: "Inf = Complete_Lattices.Inf" |
|
222 |
||
223 |
hide_const (open) Inf |
|
224 |
||
225 |
lemma [code_unfold_post]: |
|
226 |
"Inf = More_Set.Inf" |
|
227 |
by simp |
|
228 |
||
229 |
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
230 |
[simp]: "Sup = Complete_Lattices.Sup" |
|
231 |
||
232 |
hide_const (open) Sup |
|
233 |
||
234 |
lemma [code_unfold_post]: |
|
235 |
"Sup = More_Set.Sup" |
|
236 |
by simp |
|
237 |
||
238 |
lemma Inf_code [code]: |
|
239 |
"More_Set.Inf (set xs) = foldr inf xs top" |
|
240 |
"More_Set.Inf (coset []) = bot" |
|
241 |
by (simp_all add: Inf_set_foldr) |
|
242 |
||
243 |
lemma Sup_sup [code]: |
|
244 |
"More_Set.Sup (set xs) = foldr sup xs bot" |
|
245 |
"More_Set.Sup (coset []) = top" |
|
246 |
by (simp_all add: Sup_set_foldr) |
|
247 |
||
248 |
lemma INF_code [code]: |
|
249 |
"INFI (set xs) f = foldr (inf \<circ> f) xs top" |
|
250 |
by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map) |
|
251 |
||
252 |
lemma SUP_sup [code]: |
|
253 |
"SUPR (set xs) f = foldr (sup \<circ> f) xs bot" |
|
254 |
by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map) |
|
255 |
||
256 |
hide_const (open) coset |
|
257 |
||
258 |
||
259 |
subsection {* Operations on relations *} |
|
260 |
||
261 |
text {* Initially contributed by Tjark Weber. *} |
|
262 |
||
263 |
declare Domain_fst [code] |
|
264 |
||
265 |
declare Range_snd [code] |
|
266 |
||
267 |
declare trans_join [code] |
|
268 |
||
269 |
declare irrefl_distinct [code] |
|
270 |
||
271 |
declare trancl_set_ntrancl [code] |
|
272 |
||
273 |
declare acyclic_irrefl [code] |
|
274 |
||
275 |
declare product_code [code] |
|
276 |
||
277 |
declare Id_on_set [code] |
|
278 |
||
279 |
declare set_rel_comp [code] |
|
280 |
||
281 |
declare wf_set [code] |
|
282 |
||
283 |
end |
|
284 |