80 |
80 |
81 |
81 |
82 subsection {* The identity relation *} |
82 subsection {* The identity relation *} |
83 |
83 |
84 lemma IdI [intro]: "(a, a) : Id" |
84 lemma IdI [intro]: "(a, a) : Id" |
85 by (simp add: Id_def) |
85 by (simp add: Id_def) |
86 |
86 |
87 lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" |
87 lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" |
88 by (unfold Id_def) (iprover elim: CollectE) |
88 by (unfold Id_def) (iprover elim: CollectE) |
89 |
89 |
90 lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" |
90 lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" |
91 by (unfold Id_def) blast |
91 by (unfold Id_def) blast |
92 |
92 |
93 lemma reflexive_Id: "reflexive Id" |
93 lemma reflexive_Id: "reflexive Id" |
94 by (simp add: refl_def) |
94 by (simp add: refl_def) |
95 |
95 |
96 lemma antisym_Id: "antisym Id" |
96 lemma antisym_Id: "antisym Id" |
97 -- {* A strange result, since @{text Id} is also symmetric. *} |
97 -- {* A strange result, since @{text Id} is also symmetric. *} |
98 by (simp add: antisym_def) |
98 by (simp add: antisym_def) |
99 |
99 |
100 lemma sym_Id: "sym Id" |
100 lemma sym_Id: "sym Id" |
101 by (simp add: sym_def) |
101 by (simp add: sym_def) |
102 |
102 |
103 lemma trans_Id: "trans Id" |
103 lemma trans_Id: "trans Id" |
104 by (simp add: trans_def) |
104 by (simp add: trans_def) |
105 |
105 |
106 |
106 |
107 subsection {* Diagonal: identity over a set *} |
107 subsection {* Diagonal: identity over a set *} |
108 |
108 |
109 lemma diag_empty [simp]: "diag {} = {}" |
109 lemma diag_empty [simp]: "diag {} = {}" |
110 by (simp add: diag_def) |
110 by (simp add: diag_def) |
111 |
111 |
112 lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A" |
112 lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A" |
113 by (simp add: diag_def) |
113 by (simp add: diag_def) |
114 |
114 |
115 lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A" |
115 lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A" |
116 by (rule diag_eqI) (rule refl) |
116 by (rule diag_eqI) (rule refl) |
117 |
117 |
118 lemma diagE [elim!]: |
118 lemma diagE [elim!]: |
119 "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" |
119 "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" |
120 -- {* The general elimination rule. *} |
120 -- {* The general elimination rule. *} |
121 by (unfold diag_def) (iprover elim!: UN_E singletonE) |
121 by (unfold diag_def) (iprover elim!: UN_E singletonE) |
122 |
122 |
123 lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)" |
123 lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)" |
124 by blast |
124 by blast |
125 |
125 |
126 lemma diag_subset_Times: "diag A \<subseteq> A \<times> A" |
126 lemma diag_subset_Times: "diag A \<subseteq> A \<times> A" |
127 by blast |
127 by blast |
128 |
128 |
129 |
129 |
130 subsection {* Composition of two relations *} |
130 subsection {* Composition of two relations *} |
131 |
131 |
132 lemma rel_compI [intro]: |
132 lemma rel_compI [intro]: |
133 "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s" |
133 "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s" |
134 by (unfold rel_comp_def) blast |
134 by (unfold rel_comp_def) blast |
135 |
135 |
136 lemma rel_compE [elim!]: "xz : r O s ==> |
136 lemma rel_compE [elim!]: "xz : r O s ==> |
137 (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P" |
137 (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P" |
138 by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE) |
138 by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE) |
139 |
139 |
140 lemma rel_compEpair: |
140 lemma rel_compEpair: |
141 "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P" |
141 "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P" |
142 by (iprover elim: rel_compE Pair_inject ssubst) |
142 by (iprover elim: rel_compE Pair_inject ssubst) |
143 |
143 |
144 lemma R_O_Id [simp]: "R O Id = R" |
144 lemma R_O_Id [simp]: "R O Id = R" |
145 by fast |
145 by fast |
146 |
146 |
147 lemma Id_O_R [simp]: "Id O R = R" |
147 lemma Id_O_R [simp]: "Id O R = R" |
148 by fast |
148 by fast |
149 |
149 |
150 lemma rel_comp_empty1[simp]: "{} O R = {}" |
150 lemma rel_comp_empty1[simp]: "{} O R = {}" |
151 by blast |
151 by blast |
152 |
152 |
153 lemma rel_comp_empty2[simp]: "R O {} = {}" |
153 lemma rel_comp_empty2[simp]: "R O {} = {}" |
154 by blast |
154 by blast |
155 |
155 |
156 lemma O_assoc: "(R O S) O T = R O (S O T)" |
156 lemma O_assoc: "(R O S) O T = R O (S O T)" |
157 by blast |
157 by blast |
158 |
158 |
159 lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" |
159 lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" |
160 by (unfold trans_def) blast |
160 by (unfold trans_def) blast |
161 |
161 |
162 lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)" |
162 lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)" |
163 by blast |
163 by blast |
164 |
164 |
165 lemma rel_comp_subset_Sigma: |
165 lemma rel_comp_subset_Sigma: |
166 "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C" |
166 "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C" |
167 by blast |
167 by blast |
168 |
168 |
169 |
169 |
170 subsection {* Reflexivity *} |
170 subsection {* Reflexivity *} |
171 |
171 |
172 lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r" |
172 lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r" |
173 by (unfold refl_def) (iprover intro!: ballI) |
173 by (unfold refl_def) (iprover intro!: ballI) |
174 |
174 |
175 lemma reflD: "refl A r ==> a : A ==> (a, a) : r" |
175 lemma reflD: "refl A r ==> a : A ==> (a, a) : r" |
176 by (unfold refl_def) blast |
176 by (unfold refl_def) blast |
177 |
177 |
178 lemma reflD1: "refl A r ==> (x, y) : r ==> x : A" |
178 lemma reflD1: "refl A r ==> (x, y) : r ==> x : A" |
179 by (unfold refl_def) blast |
179 by (unfold refl_def) blast |
180 |
180 |
181 lemma reflD2: "refl A r ==> (x, y) : r ==> y : A" |
181 lemma reflD2: "refl A r ==> (x, y) : r ==> y : A" |
182 by (unfold refl_def) blast |
182 by (unfold refl_def) blast |
183 |
183 |
184 lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)" |
184 lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)" |
185 by (unfold refl_def) blast |
185 by (unfold refl_def) blast |
186 |
186 |
187 lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)" |
187 lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)" |
188 by (unfold refl_def) blast |
188 by (unfold refl_def) blast |
189 |
189 |
190 lemma refl_INTER: |
190 lemma refl_INTER: |
191 "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)" |
191 "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)" |
192 by (unfold refl_def) fast |
192 by (unfold refl_def) fast |
193 |
193 |
194 lemma refl_UNION: |
194 lemma refl_UNION: |
195 "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)" |
195 "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)" |
196 by (unfold refl_def) blast |
196 by (unfold refl_def) blast |
197 |
197 |
198 lemma refl_diag: "refl A (diag A)" |
198 lemma refl_diag: "refl A (diag A)" |
199 by (rule reflI [OF diag_subset_Times diagI]) |
199 by (rule reflI [OF diag_subset_Times diagI]) |
200 |
200 |
201 |
201 |
202 subsection {* Antisymmetry *} |
202 subsection {* Antisymmetry *} |
203 |
203 |
204 lemma antisymI: |
204 lemma antisymI: |
205 "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" |
205 "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" |
206 by (unfold antisym_def) iprover |
206 by (unfold antisym_def) iprover |
207 |
207 |
208 lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" |
208 lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" |
209 by (unfold antisym_def) iprover |
209 by (unfold antisym_def) iprover |
210 |
210 |
211 lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r" |
211 lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r" |
212 by (unfold antisym_def) blast |
212 by (unfold antisym_def) blast |
213 |
213 |
214 lemma antisym_empty [simp]: "antisym {}" |
214 lemma antisym_empty [simp]: "antisym {}" |
215 by (unfold antisym_def) blast |
215 by (unfold antisym_def) blast |
216 |
216 |
217 lemma antisym_diag [simp]: "antisym (diag A)" |
217 lemma antisym_diag [simp]: "antisym (diag A)" |
218 by (unfold antisym_def) blast |
218 by (unfold antisym_def) blast |
219 |
219 |
220 |
220 |
221 subsection {* Symmetry *} |
221 subsection {* Symmetry *} |
222 |
222 |
223 lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r" |
223 lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r" |
224 by (unfold sym_def) iprover |
224 by (unfold sym_def) iprover |
225 |
225 |
226 lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r" |
226 lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r" |
227 by (unfold sym_def, blast) |
227 by (unfold sym_def, blast) |
228 |
228 |
229 lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)" |
229 lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)" |
230 by (fast intro: symI dest: symD) |
230 by (fast intro: symI dest: symD) |
231 |
231 |
232 lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)" |
232 lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)" |
233 by (fast intro: symI dest: symD) |
233 by (fast intro: symI dest: symD) |
234 |
234 |
235 lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)" |
235 lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)" |
236 by (fast intro: symI dest: symD) |
236 by (fast intro: symI dest: symD) |
237 |
237 |
238 lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)" |
238 lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)" |
239 by (fast intro: symI dest: symD) |
239 by (fast intro: symI dest: symD) |
240 |
240 |
241 lemma sym_diag [simp]: "sym (diag A)" |
241 lemma sym_diag [simp]: "sym (diag A)" |
242 by (rule symI) clarify |
242 by (rule symI) clarify |
243 |
243 |
244 |
244 |
245 subsection {* Transitivity *} |
245 subsection {* Transitivity *} |
246 |
246 |
247 lemma transI: |
247 lemma transI: |
248 "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" |
248 "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" |
249 by (unfold trans_def) iprover |
249 by (unfold trans_def) iprover |
250 |
250 |
251 lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r" |
251 lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r" |
252 by (unfold trans_def) iprover |
252 by (unfold trans_def) iprover |
253 |
253 |
254 lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)" |
254 lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)" |
255 by (fast intro: transI elim: transD) |
255 by (fast intro: transI elim: transD) |
256 |
256 |
257 lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)" |
257 lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)" |
258 by (fast intro: transI elim: transD) |
258 by (fast intro: transI elim: transD) |
259 |
259 |
260 lemma trans_diag [simp]: "trans (diag A)" |
260 lemma trans_diag [simp]: "trans (diag A)" |
261 by (fast intro: transI elim: transD) |
261 by (fast intro: transI elim: transD) |
262 |
262 |
263 |
263 |
264 subsection {* Converse *} |
264 subsection {* Converse *} |
265 |
265 |
266 lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)" |
266 lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)" |
267 by (simp add: converse_def) |
267 by (simp add: converse_def) |
268 |
268 |
269 lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1" |
269 lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1" |
270 by (simp add: converse_def) |
270 by (simp add: converse_def) |
271 |
271 |
272 lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r" |
272 lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r" |
273 by (simp add: converse_def) |
273 by (simp add: converse_def) |
274 |
274 |
275 lemma converseE [elim!]: |
275 lemma converseE [elim!]: |
276 "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P" |
276 "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P" |
277 -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} |
277 -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} |
278 by (unfold converse_def) (iprover elim!: CollectE splitE bexE) |
278 by (unfold converse_def) (iprover elim!: CollectE splitE bexE) |
279 |
279 |
280 lemma converse_converse [simp]: "(r^-1)^-1 = r" |
280 lemma converse_converse [simp]: "(r^-1)^-1 = r" |
281 by (unfold converse_def) blast |
281 by (unfold converse_def) blast |
282 |
282 |
283 lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1" |
283 lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1" |
284 by blast |
284 by blast |
285 |
285 |
286 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1" |
286 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1" |
287 by blast |
287 by blast |
288 |
288 |
289 lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1" |
289 lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1" |
290 by blast |
290 by blast |
291 |
291 |
292 lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)" |
292 lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)" |
293 by fast |
293 by fast |
294 |
294 |
295 lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)" |
295 lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)" |
296 by blast |
296 by blast |
297 |
297 |
298 lemma converse_Id [simp]: "Id^-1 = Id" |
298 lemma converse_Id [simp]: "Id^-1 = Id" |
299 by blast |
299 by blast |
300 |
300 |
301 lemma converse_diag [simp]: "(diag A)^-1 = diag A" |
301 lemma converse_diag [simp]: "(diag A)^-1 = diag A" |
302 by blast |
302 by blast |
303 |
303 |
304 lemma refl_converse [simp]: "refl A (converse r) = refl A r" |
304 lemma refl_converse [simp]: "refl A (converse r) = refl A r" |
305 by (unfold refl_def) auto |
305 by (unfold refl_def) auto |
306 |
306 |
307 lemma sym_converse [simp]: "sym (converse r) = sym r" |
307 lemma sym_converse [simp]: "sym (converse r) = sym r" |
308 by (unfold sym_def) blast |
308 by (unfold sym_def) blast |
309 |
309 |
310 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
310 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
311 by (unfold antisym_def) blast |
311 by (unfold antisym_def) blast |
312 |
312 |
313 lemma trans_converse [simp]: "trans (converse r) = trans r" |
313 lemma trans_converse [simp]: "trans (converse r) = trans r" |
314 by (unfold trans_def) blast |
314 by (unfold trans_def) blast |
315 |
315 |
316 lemma sym_conv_converse_eq: "sym r = (r^-1 = r)" |
316 lemma sym_conv_converse_eq: "sym r = (r^-1 = r)" |
317 by (unfold sym_def) fast |
317 by (unfold sym_def) fast |
318 |
318 |
319 lemma sym_Un_converse: "sym (r \<union> r^-1)" |
319 lemma sym_Un_converse: "sym (r \<union> r^-1)" |
320 by (unfold sym_def) blast |
320 by (unfold sym_def) blast |
321 |
321 |
322 lemma sym_Int_converse: "sym (r \<inter> r^-1)" |
322 lemma sym_Int_converse: "sym (r \<inter> r^-1)" |
323 by (unfold sym_def) blast |
323 by (unfold sym_def) blast |
324 |
324 |
325 |
325 |
326 subsection {* Domain *} |
326 subsection {* Domain *} |
327 |
327 |
328 declare Domain_def [noatp] |
328 declare Domain_def [noatp] |
329 |
329 |
330 lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)" |
330 lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)" |
331 by (unfold Domain_def) blast |
331 by (unfold Domain_def) blast |
332 |
332 |
333 lemma DomainI [intro]: "(a, b) : r ==> a : Domain r" |
333 lemma DomainI [intro]: "(a, b) : r ==> a : Domain r" |
334 by (iprover intro!: iffD2 [OF Domain_iff]) |
334 by (iprover intro!: iffD2 [OF Domain_iff]) |
335 |
335 |
336 lemma DomainE [elim!]: |
336 lemma DomainE [elim!]: |
337 "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P" |
337 "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P" |
338 by (iprover dest!: iffD1 [OF Domain_iff]) |
338 by (iprover dest!: iffD1 [OF Domain_iff]) |
339 |
339 |
340 lemma Domain_empty [simp]: "Domain {} = {}" |
340 lemma Domain_empty [simp]: "Domain {} = {}" |
341 by blast |
341 by blast |
342 |
342 |
343 lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)" |
343 lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)" |
344 by blast |
344 by blast |
345 |
345 |
346 lemma Domain_Id [simp]: "Domain Id = UNIV" |
346 lemma Domain_Id [simp]: "Domain Id = UNIV" |
347 by blast |
347 by blast |
348 |
348 |
349 lemma Domain_diag [simp]: "Domain (diag A) = A" |
349 lemma Domain_diag [simp]: "Domain (diag A) = A" |
350 by blast |
350 by blast |
351 |
351 |
352 lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)" |
352 lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)" |
353 by blast |
353 by blast |
354 |
354 |
355 lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)" |
355 lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)" |
356 by blast |
356 by blast |
357 |
357 |
358 lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)" |
358 lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)" |
359 by blast |
359 by blast |
360 |
360 |
361 lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)" |
361 lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)" |
362 by blast |
362 by blast |
|
363 |
|
364 lemma Domain_converse[simp]: "Domain(r^-1) = Range r" |
|
365 by(auto simp:Range_def) |
363 |
366 |
364 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" |
367 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" |
365 by blast |
368 by blast |
366 |
369 |
367 lemma fst_eq_Domain: "fst ` R = Domain R"; |
370 lemma fst_eq_Domain: "fst ` R = Domain R"; |
368 apply auto |
371 by (auto intro!:image_eqI) |
369 apply (rule image_eqI, auto) |
|
370 done |
|
371 |
372 |
372 |
373 |
373 subsection {* Range *} |
374 subsection {* Range *} |
374 |
375 |
375 lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" |
376 lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" |
376 by (simp add: Domain_def Range_def) |
377 by (simp add: Domain_def Range_def) |
377 |
378 |
378 lemma RangeI [intro]: "(a, b) : r ==> b : Range r" |
379 lemma RangeI [intro]: "(a, b) : r ==> b : Range r" |
379 by (unfold Range_def) (iprover intro!: converseI DomainI) |
380 by (unfold Range_def) (iprover intro!: converseI DomainI) |
380 |
381 |
381 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P" |
382 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P" |
382 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD) |
383 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD) |
383 |
384 |
384 lemma Range_empty [simp]: "Range {} = {}" |
385 lemma Range_empty [simp]: "Range {} = {}" |
385 by blast |
386 by blast |
386 |
387 |
387 lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)" |
388 lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)" |
388 by blast |
389 by blast |
389 |
390 |
390 lemma Range_Id [simp]: "Range Id = UNIV" |
391 lemma Range_Id [simp]: "Range Id = UNIV" |
391 by blast |
392 by blast |
392 |
393 |
393 lemma Range_diag [simp]: "Range (diag A) = A" |
394 lemma Range_diag [simp]: "Range (diag A) = A" |
394 by auto |
395 by auto |
395 |
396 |
396 lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)" |
397 lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)" |
397 by blast |
398 by blast |
398 |
399 |
399 lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)" |
400 lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)" |
400 by blast |
401 by blast |
401 |
402 |
402 lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)" |
403 lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)" |
403 by blast |
404 by blast |
404 |
405 |
405 lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" |
406 lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" |
406 by blast |
407 by blast |
|
408 |
|
409 lemma Range_converse[simp]: "Range(r^-1) = Domain r" |
|
410 by blast |
407 |
411 |
408 lemma snd_eq_Range: "snd ` R = Range R"; |
412 lemma snd_eq_Range: "snd ` R = Range R"; |
409 apply auto |
413 by (auto intro!:image_eqI) |
410 apply (rule image_eqI, auto) |
414 |
411 done |
415 |
|
416 subsection {* Field *} |
|
417 |
|
418 lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s" |
|
419 by(auto simp:Field_def Domain_def Range_def) |
|
420 |
|
421 lemma Field_empty[simp]: "Field {} = {}" |
|
422 by(auto simp:Field_def) |
|
423 |
|
424 lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r" |
|
425 by(auto simp:Field_def) |
|
426 |
|
427 lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s" |
|
428 by(auto simp:Field_def) |
|
429 |
|
430 lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)" |
|
431 by(auto simp:Field_def) |
|
432 |
|
433 lemma Field_converse[simp]: "Field(r^-1) = Field r" |
|
434 by(auto simp:Field_def) |
412 |
435 |
413 |
436 |
414 subsection {* Image of a set under a relation *} |
437 subsection {* Image of a set under a relation *} |
415 |
438 |
416 declare Image_def [noatp] |
439 declare Image_def [noatp] |
417 |
440 |
418 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" |
441 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" |
419 by (simp add: Image_def) |
442 by (simp add: Image_def) |
420 |
443 |
421 lemma Image_singleton: "r``{a} = {b. (a, b) : r}" |
444 lemma Image_singleton: "r``{a} = {b. (a, b) : r}" |
422 by (simp add: Image_def) |
445 by (simp add: Image_def) |
423 |
446 |
424 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)" |
447 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)" |
425 by (rule Image_iff [THEN trans]) simp |
448 by (rule Image_iff [THEN trans]) simp |
426 |
449 |
427 lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A" |
450 lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A" |
428 by (unfold Image_def) blast |
451 by (unfold Image_def) blast |
429 |
452 |
430 lemma ImageE [elim!]: |
453 lemma ImageE [elim!]: |
431 "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" |
454 "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" |
432 by (unfold Image_def) (iprover elim!: CollectE bexE) |
455 by (unfold Image_def) (iprover elim!: CollectE bexE) |
433 |
456 |
434 lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A" |
457 lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A" |
435 -- {* This version's more effective when we already have the required @{text a} *} |
458 -- {* This version's more effective when we already have the required @{text a} *} |
436 by blast |
459 by blast |
437 |
460 |
438 lemma Image_empty [simp]: "R``{} = {}" |
461 lemma Image_empty [simp]: "R``{} = {}" |
439 by blast |
462 by blast |
440 |
463 |
441 lemma Image_Id [simp]: "Id `` A = A" |
464 lemma Image_Id [simp]: "Id `` A = A" |
442 by blast |
465 by blast |
443 |
466 |
444 lemma Image_diag [simp]: "diag A `` B = A \<inter> B" |
467 lemma Image_diag [simp]: "diag A `` B = A \<inter> B" |
445 by blast |
468 by blast |
446 |
469 |
447 lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" |
470 lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" |
448 by blast |
471 by blast |
449 |
472 |
450 lemma Image_Int_eq: |
473 lemma Image_Int_eq: |
451 "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B" |
474 "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B" |
452 by (simp add: single_valued_def, blast) |
475 by (simp add: single_valued_def, blast) |
453 |
476 |
454 lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" |
477 lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" |
455 by blast |
478 by blast |
456 |
479 |
457 lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" |
480 lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" |
458 by blast |
481 by blast |
459 |
482 |
460 lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B" |
483 lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B" |
461 by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) |
484 by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) |
462 |
485 |
463 lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" |
486 lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" |
464 -- {* NOT suitable for rewriting *} |
487 -- {* NOT suitable for rewriting *} |
465 by blast |
488 by blast |
466 |
489 |
467 lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)" |
490 lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)" |
468 by blast |
491 by blast |
469 |
492 |
470 lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" |
493 lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" |
471 by blast |
494 by blast |
472 |
495 |
473 lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" |
496 lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" |
474 by blast |
497 by blast |
475 |
498 |
476 text{*Converse inclusion requires some assumptions*} |
499 text{*Converse inclusion requires some assumptions*} |
477 lemma Image_INT_eq: |
500 lemma Image_INT_eq: |
478 "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)" |
501 "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)" |
479 apply (rule equalityI) |
502 apply (rule equalityI) |
480 apply (rule Image_INT_subset) |
503 apply (rule Image_INT_subset) |
481 apply (simp add: single_valued_def, blast) |
504 apply (simp add: single_valued_def, blast) |
482 done |
505 done |
483 |
506 |
484 lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))" |
507 lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))" |
485 by blast |
508 by blast |
486 |
509 |
487 |
510 |
488 subsection {* Single valued relations *} |
511 subsection {* Single valued relations *} |
489 |
512 |
490 lemma single_valuedI: |
513 lemma single_valuedI: |
491 "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r" |
514 "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r" |
492 by (unfold single_valued_def) |
515 by (unfold single_valued_def) |
493 |
516 |
494 lemma single_valuedD: |
517 lemma single_valuedD: |
495 "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" |
518 "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" |
496 by (simp add: single_valued_def) |
519 by (simp add: single_valued_def) |
497 |
520 |
498 lemma single_valued_rel_comp: |
521 lemma single_valued_rel_comp: |
499 "single_valued r ==> single_valued s ==> single_valued (r O s)" |
522 "single_valued r ==> single_valued s ==> single_valued (r O s)" |
500 by (unfold single_valued_def) blast |
523 by (unfold single_valued_def) blast |
501 |
524 |
502 lemma single_valued_subset: |
525 lemma single_valued_subset: |
503 "r \<subseteq> s ==> single_valued s ==> single_valued r" |
526 "r \<subseteq> s ==> single_valued s ==> single_valued r" |
504 by (unfold single_valued_def) blast |
527 by (unfold single_valued_def) blast |
505 |
528 |
506 lemma single_valued_Id [simp]: "single_valued Id" |
529 lemma single_valued_Id [simp]: "single_valued Id" |
507 by (unfold single_valued_def) blast |
530 by (unfold single_valued_def) blast |
508 |
531 |
509 lemma single_valued_diag [simp]: "single_valued (diag A)" |
532 lemma single_valued_diag [simp]: "single_valued (diag A)" |
510 by (unfold single_valued_def) blast |
533 by (unfold single_valued_def) blast |
511 |
534 |
512 |
535 |
513 subsection {* Graphs given by @{text Collect} *} |
536 subsection {* Graphs given by @{text Collect} *} |
514 |
537 |
515 lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}" |
538 lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}" |
516 by auto |
539 by auto |
517 |
540 |
518 lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}" |
541 lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}" |
519 by auto |
542 by auto |
520 |
543 |
521 lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}" |
544 lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}" |
522 by auto |
545 by auto |
523 |
546 |
524 |
547 |
525 subsection {* Inverse image *} |
548 subsection {* Inverse image *} |
526 |
549 |
527 lemma sym_inv_image: "sym r ==> sym (inv_image r f)" |
550 lemma sym_inv_image: "sym r ==> sym (inv_image r f)" |
528 by (unfold sym_def inv_image_def) blast |
551 by (unfold sym_def inv_image_def) blast |
529 |
552 |
530 lemma trans_inv_image: "trans r ==> trans (inv_image r f)" |
553 lemma trans_inv_image: "trans r ==> trans (inv_image r f)" |
531 apply (unfold trans_def inv_image_def) |
554 apply (unfold trans_def inv_image_def) |
532 apply (simp (no_asm)) |
555 apply (simp (no_asm)) |
533 apply blast |
556 apply blast |