133 !!y. y:B ==> d(y): A; |
129 !!y. y:B ==> d(y): A; |
134 !!x. x:A ==> d(c(x)) = x; |
130 !!x. x:A ==> d(c(x)) = x; |
135 !!y. y:B ==> c(d(y)) = y |
131 !!y. y:B ==> c(d(y)) = y |
136 |] ==> (lam x:A. c(x)) : bij(A,B)" |
132 |] ==> (lam x:A. c(x)) : bij(A,B)" |
137 apply (unfold bij_def) |
133 apply (unfold bij_def) |
138 apply (blast intro!: lam_injective lam_surjective); |
134 apply (blast intro!: lam_injective lam_surjective) |
139 done |
135 done |
140 |
136 |
141 lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y)) |
137 lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y)) |
142 ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)" |
138 ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)" |
143 apply (rule_tac d = "f" in lam_bijective) |
139 apply (rule_tac d = "f" in lam_bijective) |
151 apply (unfold id_def) |
147 apply (unfold id_def) |
152 apply (erule lamI) |
148 apply (erule lamI) |
153 done |
149 done |
154 |
150 |
155 lemma idE [elim!]: "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P |] ==> P" |
151 lemma idE [elim!]: "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P |] ==> P" |
156 apply (simp add: id_def lam_def) |
152 by (simp add: id_def lam_def, blast) |
157 apply (blast intro: elim:); |
|
158 done |
|
159 |
153 |
160 lemma id_type: "id(A) : A->A" |
154 lemma id_type: "id(A) : A->A" |
161 apply (unfold id_def) |
155 apply (unfold id_def) |
162 apply (rule lam_type) |
156 apply (rule lam_type, assumption) |
163 apply assumption |
|
164 done |
157 done |
165 |
158 |
166 lemma id_conv [simp]: "x:A ==> id(A)`x = x" |
159 lemma id_conv [simp]: "x:A ==> id(A)`x = x" |
167 apply (unfold id_def) |
160 apply (unfold id_def) |
168 apply (simp (no_asm_simp)) |
161 apply (simp (no_asm_simp)) |
212 lemma left_inverse_lemma: |
205 lemma left_inverse_lemma: |
213 "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a" |
206 "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a" |
214 by (blast intro: apply_Pair apply_equality converseI) |
207 by (blast intro: apply_Pair apply_equality converseI) |
215 |
208 |
216 lemma left_inverse [simp]: "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a" |
209 lemma left_inverse [simp]: "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a" |
217 apply (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) |
210 by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) |
218 done |
|
219 |
211 |
220 lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard] |
212 lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard] |
221 |
213 |
222 lemma right_inverse_lemma: |
214 lemma right_inverse_lemma: |
223 "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b" |
215 "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b" |
224 apply (rule apply_Pair [THEN converseD [THEN apply_equality]]) |
216 apply (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) |
225 apply (auto ); |
|
226 done |
217 done |
227 |
218 |
228 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
219 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
229 No: they would not imply that converse(f) was a function! *) |
220 No: they would not imply that converse(f) was a function! *) |
230 lemma right_inverse [simp]: |
221 lemma right_inverse [simp]: |
231 "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b" |
222 "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b" |
232 by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun) |
223 by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun) |
233 |
224 |
234 lemma right_inverse_bij: "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b" |
225 lemma right_inverse_bij: "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b" |
235 apply (force simp add: bij_def surj_range) |
226 by (force simp add: bij_def surj_range) |
236 done |
|
237 |
227 |
238 (** Converses of injections, surjections, bijections **) |
228 (** Converses of injections, surjections, bijections **) |
239 |
229 |
240 lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)" |
230 lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)" |
241 apply (rule f_imp_injective) |
231 apply (rule f_imp_injective) |
242 apply (erule inj_converse_fun) |
232 apply (erule inj_converse_fun, clarify) |
243 apply (clarify ); |
233 apply (rule right_inverse) |
244 apply (rule right_inverse); |
|
245 apply assumption |
234 apply assumption |
246 apply (blast intro: elim:); |
235 apply blast |
247 done |
236 done |
248 |
237 |
249 lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)" |
238 lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)" |
250 by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun |
239 by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun |
251 range_of_fun [THEN apply_type]) |
240 range_of_fun [THEN apply_type]) |
261 (** Composition of two relations **) |
250 (** Composition of two relations **) |
262 |
251 |
263 (*The inductive definition package could derive these theorems for (r O s)*) |
252 (*The inductive definition package could derive these theorems for (r O s)*) |
264 |
253 |
265 lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s" |
254 lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s" |
266 apply (unfold comp_def) |
255 by (unfold comp_def, blast) |
267 apply blast |
|
268 done |
|
269 |
256 |
270 lemma compE [elim!]: |
257 lemma compE [elim!]: |
271 "[| xz : r O s; |
258 "[| xz : r O s; |
272 !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |] |
259 !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |] |
273 ==> P" |
260 ==> P" |
274 apply (unfold comp_def) |
261 by (unfold comp_def, blast) |
275 apply blast |
|
276 done |
|
277 |
262 |
278 lemma compEpair: |
263 lemma compEpair: |
279 "[| <a,c> : r O s; |
264 "[| <a,c> : r O s; |
280 !!y. [| <a,y>:s; <y,c>:r |] ==> P |] |
265 !!y. [| <a,y>:s; <y,c>:r |] ==> P |] |
281 ==> P" |
266 ==> P" |
282 apply (erule compE) |
267 by (erule compE, simp) |
283 apply (simp add: ); |
|
284 done |
|
285 |
268 |
286 lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" |
269 lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" |
287 apply blast |
270 by blast |
288 done |
|
289 |
271 |
290 |
272 |
291 (** Domain and Range -- see Suppes, section 3.1 **) |
273 (** Domain and Range -- see Suppes, section 3.1 **) |
292 |
274 |
293 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) |
275 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) |
294 lemma range_comp: "range(r O s) <= range(r)" |
276 lemma range_comp: "range(r O s) <= range(r)" |
295 apply blast |
277 by blast |
296 done |
|
297 |
278 |
298 lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)" |
279 lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)" |
299 apply (rule range_comp [THEN equalityI]) |
280 by (rule range_comp [THEN equalityI], blast) |
300 apply blast |
|
301 done |
|
302 |
281 |
303 lemma domain_comp: "domain(r O s) <= domain(s)" |
282 lemma domain_comp: "domain(r O s) <= domain(s)" |
304 apply blast |
283 by blast |
305 done |
|
306 |
284 |
307 lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)" |
285 lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)" |
308 apply (rule domain_comp [THEN equalityI]) |
286 by (rule domain_comp [THEN equalityI], blast) |
309 apply blast |
|
310 done |
|
311 |
287 |
312 lemma image_comp: "(r O s)``A = r``(s``A)" |
288 lemma image_comp: "(r O s)``A = r``(s``A)" |
313 apply blast |
289 by blast |
314 done |
|
315 |
290 |
316 |
291 |
317 (** Other results **) |
292 (** Other results **) |
318 |
293 |
319 lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" |
294 lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" |
320 apply blast |
295 by blast |
321 done |
|
322 |
296 |
323 (*composition preserves relations*) |
297 (*composition preserves relations*) |
324 lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C" |
298 lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C" |
325 apply blast |
299 by blast |
326 done |
|
327 |
300 |
328 (*associative law for composition*) |
301 (*associative law for composition*) |
329 lemma comp_assoc: "(r O s) O t = r O (s O t)" |
302 lemma comp_assoc: "(r O s) O t = r O (s O t)" |
330 apply blast |
303 by blast |
331 done |
|
332 |
304 |
333 (*left identity of composition; provable inclusions are |
305 (*left identity of composition; provable inclusions are |
334 id(A) O r <= r |
306 id(A) O r <= r |
335 and [| r<=A*B; B<=C |] ==> r <= id(C) O r *) |
307 and [| r<=A*B; B<=C |] ==> r <= id(C) O r *) |
336 lemma left_comp_id: "r<=A*B ==> id(B) O r = r" |
308 lemma left_comp_id: "r<=A*B ==> id(B) O r = r" |
337 apply blast |
309 by blast |
338 done |
|
339 |
310 |
340 (*right identity of composition; provable inclusions are |
311 (*right identity of composition; provable inclusions are |
341 r O id(A) <= r |
312 r O id(A) <= r |
342 and [| r<=A*B; A<=C |] ==> r <= r O id(C) *) |
313 and [| r<=A*B; A<=C |] ==> r <= r O id(C) *) |
343 lemma right_comp_id: "r<=A*B ==> r O id(A) = r" |
314 lemma right_comp_id: "r<=A*B ==> r O id(A) = r" |
344 apply blast |
315 by blast |
345 done |
|
346 |
316 |
347 |
317 |
348 (** Composition preserves functions, injections, and surjections **) |
318 (** Composition preserves functions, injections, and surjections **) |
349 |
319 |
350 lemma comp_function: |
320 lemma comp_function: "[| function(g); function(f) |] ==> function(f O g)" |
351 "[| function(g); function(f) |] ==> function(f O g)" |
321 by (unfold function_def, blast) |
352 apply (unfold function_def) |
|
353 apply blast |
|
354 done |
|
355 |
322 |
356 (*Don't think the premises can be weakened much*) |
323 (*Don't think the premises can be weakened much*) |
357 lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) : A->C" |
324 lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) : A->C" |
358 apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) |
325 apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) |
359 apply (subst range_rel_subset [THEN domain_comp_eq]); |
326 apply (subst range_rel_subset [THEN domain_comp_eq], auto) |
360 apply (auto ); |
|
361 done |
327 done |
362 |
328 |
363 (*Thanks to the new definition of "apply", the premise f: B->C is gone!*) |
329 (*Thanks to the new definition of "apply", the premise f: B->C is gone!*) |
364 lemma comp_fun_apply [simp]: |
330 lemma comp_fun_apply [simp]: |
365 "[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)" |
331 "[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)" |
374 ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))" |
340 ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))" |
375 apply (subgoal_tac "(lam x:A. b(x)) : A -> B") |
341 apply (subgoal_tac "(lam x:A. b(x)) : A -> B") |
376 apply (rule fun_extension) |
342 apply (rule fun_extension) |
377 apply (blast intro: comp_fun lam_funtype) |
343 apply (blast intro: comp_fun lam_funtype) |
378 apply (rule lam_funtype) |
344 apply (rule lam_funtype) |
379 apply (simp add: ); |
345 apply simp |
380 apply (simp add: lam_type); |
346 apply (simp add: lam_type) |
381 done |
347 done |
382 |
348 |
383 lemma comp_inj: |
349 lemma comp_inj: |
384 "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)" |
350 "[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)" |
385 apply (frule inj_is_fun [of g]) |
351 apply (frule inj_is_fun [of g]) |
386 apply (frule inj_is_fun [of f]) |
352 apply (frule inj_is_fun [of f]) |
387 apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective) |
353 apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective) |
388 apply (blast intro: comp_fun); |
354 apply (blast intro: comp_fun, simp) |
389 apply (simp add: ); |
|
390 done |
355 done |
391 |
356 |
392 lemma comp_surj: |
357 lemma comp_surj: |
393 "[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)" |
358 "[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)" |
394 apply (unfold surj_def) |
359 apply (unfold surj_def) |
406 D Pastre. Automatic theorem proving in set theory. |
371 D Pastre. Automatic theorem proving in set theory. |
407 Artificial Intelligence, 10:1--27, 1978. **) |
372 Artificial Intelligence, 10:1--27, 1978. **) |
408 |
373 |
409 lemma comp_mem_injD1: |
374 lemma comp_mem_injD1: |
410 "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)" |
375 "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)" |
411 apply (unfold inj_def) |
376 apply (unfold inj_def, force) |
412 apply (force ); |
|
413 done |
377 done |
414 |
378 |
415 lemma comp_mem_injD2: |
379 lemma comp_mem_injD2: |
416 "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)" |
380 "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)" |
417 apply (unfold inj_def surj_def) |
381 apply (unfold inj_def surj_def, safe) |
418 apply safe |
|
419 apply (rule_tac x1 = "x" in bspec [THEN bexE]) |
382 apply (rule_tac x1 = "x" in bspec [THEN bexE]) |
420 apply (erule_tac [3] x1 = "w" in bspec [THEN bexE]) |
383 apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+) |
421 apply assumption+ |
|
422 apply safe |
384 apply safe |
423 apply (rule_tac t = "op ` (g) " in subst_context) |
385 apply (rule_tac t = "op ` (g) " in subst_context) |
424 apply (erule asm_rl bspec [THEN bspec, THEN mp])+ |
386 apply (erule asm_rl bspec [THEN bspec, THEN mp])+ |
425 apply (simp (no_asm_simp)) |
387 apply (simp (no_asm_simp)) |
426 done |
388 done |
432 done |
394 done |
433 |
395 |
434 |
396 |
435 lemma comp_mem_surjD2: |
397 lemma comp_mem_surjD2: |
436 "[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)" |
398 "[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)" |
437 apply (unfold inj_def surj_def) |
399 apply (unfold inj_def surj_def, safe) |
438 apply safe |
400 apply (drule_tac x = "f`y" in bspec, auto) |
439 apply (drule_tac x = "f`y" in bspec); |
|
440 apply (auto ); |
|
441 apply (blast intro: apply_funtype) |
401 apply (blast intro: apply_funtype) |
442 done |
402 done |
443 |
403 |
444 (** inverses of composition **) |
404 (** inverses of composition **) |
445 |
405 |
446 (*left inverse of composition; one inclusion is |
406 (*left inverse of composition; one inclusion is |
447 f: A->B ==> id(A) <= converse(f) O f *) |
407 f: A->B ==> id(A) <= converse(f) O f *) |
448 lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)" |
408 lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)" |
449 apply (unfold inj_def) |
409 apply (unfold inj_def, clarify) |
450 apply (clarify ); |
|
451 apply (rule equalityI) |
410 apply (rule equalityI) |
452 apply (auto simp add: apply_iff) |
411 apply (auto simp add: apply_iff, blast) |
453 apply (blast intro: elim:); |
|
454 done |
412 done |
455 |
413 |
456 (*right inverse of composition; one inclusion is |
414 (*right inverse of composition; one inclusion is |
457 f: A->B ==> f O converse(f) <= id(B) |
415 f: A->B ==> f O converse(f) <= id(B) *) |
458 *) |
|
459 lemma right_comp_inverse: |
416 lemma right_comp_inverse: |
460 "f: surj(A,B) ==> f O converse(f) = id(B)" |
417 "f: surj(A,B) ==> f O converse(f) = id(B)" |
461 apply (simp add: surj_def) |
418 apply (simp add: surj_def, clarify) |
462 apply (clarify ); |
|
463 apply (rule equalityI) |
419 apply (rule equalityI) |
464 apply (best elim: domain_type range_type dest: apply_equality2) |
420 apply (best elim: domain_type range_type dest: apply_equality2) |
465 apply (blast intro: apply_Pair) |
421 apply (blast intro: apply_Pair) |
466 done |
422 done |
467 |
423 |
468 |
424 |
469 (** Proving that a function is a bijection **) |
425 (** Proving that a function is a bijection **) |
470 |
426 |
471 lemma comp_eq_id_iff: |
427 lemma comp_eq_id_iff: |
472 "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)" |
428 "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)" |
473 apply (unfold id_def) |
429 apply (unfold id_def, safe) |
474 apply safe |
|
475 apply (drule_tac t = "%h. h`y " in subst_context) |
430 apply (drule_tac t = "%h. h`y " in subst_context) |
476 apply simp |
431 apply simp |
477 apply (rule fun_extension) |
432 apply (rule fun_extension) |
478 apply (blast intro: comp_fun lam_type) |
433 apply (blast intro: comp_fun lam_type) |
479 apply auto |
434 apply auto |
481 |
436 |
482 lemma fg_imp_bijective: |
437 lemma fg_imp_bijective: |
483 "[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f : bij(A,B)" |
438 "[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f : bij(A,B)" |
484 apply (unfold bij_def) |
439 apply (unfold bij_def) |
485 apply (simp add: comp_eq_id_iff) |
440 apply (simp add: comp_eq_id_iff) |
486 apply (blast intro: f_imp_injective f_imp_surjective apply_funtype); |
441 apply (blast intro: f_imp_injective f_imp_surjective apply_funtype) |
487 done |
442 done |
488 |
443 |
489 lemma nilpotent_imp_bijective: "[| f: A->A; f O f = id(A) |] ==> f : bij(A,A)" |
444 lemma nilpotent_imp_bijective: "[| f: A->A; f O f = id(A) |] ==> f : bij(A,A)" |
490 apply (blast intro: fg_imp_bijective) |
445 by (blast intro: fg_imp_bijective) |
491 done |
446 |
492 |
447 lemma invertible_imp_bijective: |
493 lemma invertible_imp_bijective: "[| converse(f): B->A; f: A->B |] ==> f : bij(A,B)" |
448 "[| converse(f): B->A; f: A->B |] ==> f : bij(A,B)" |
494 apply (simp (no_asm_simp) add: fg_imp_bijective comp_eq_id_iff left_inverse_lemma right_inverse_lemma) |
449 by (simp add: fg_imp_bijective comp_eq_id_iff |
495 done |
450 left_inverse_lemma right_inverse_lemma) |
496 |
451 |
497 (** Unions of functions -- cf similar theorems on func.ML **) |
452 (** Unions of functions -- cf similar theorems on func.ML **) |
498 |
453 |
499 (*Theorem by KG, proof by LCP*) |
454 (*Theorem by KG, proof by LCP*) |
500 lemma inj_disjoint_Un: |
455 lemma inj_disjoint_Un: |
501 "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] |
456 "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] |
502 ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)" |
457 ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)" |
503 apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" in lam_injective) |
458 apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" |
|
459 in lam_injective) |
504 apply (auto simp add: inj_is_fun [THEN apply_type]) |
460 apply (auto simp add: inj_is_fun [THEN apply_type]) |
505 apply (blast intro: inj_is_fun [THEN apply_type]) |
461 apply (blast intro: inj_is_fun [THEN apply_type]) |
506 done |
462 done |
507 |
463 |
508 lemma surj_disjoint_Un: |
464 lemma surj_disjoint_Un: |
509 "[| f: surj(A,B); g: surj(C,D); A Int C = 0 |] |
465 "[| f: surj(A,B); g: surj(C,D); A Int C = 0 |] |
510 ==> (f Un g) : surj(A Un C, B Un D)" |
466 ==> (f Un g) : surj(A Un C, B Un D)" |
511 apply (unfold surj_def) |
467 apply (simp add: surj_def fun_disjoint_Un) |
512 apply (blast intro: fun_disjoint_apply1 fun_disjoint_apply2 fun_disjoint_Un trans) |
468 apply (blast dest!: domain_of_fun |
|
469 intro!: fun_disjoint_apply1 fun_disjoint_apply2) |
513 done |
470 done |
514 |
471 |
515 (*A simple, high-level proof; the version for injections follows from it, |
472 (*A simple, high-level proof; the version for injections follows from it, |
516 using f:inj(A,B) <-> f:bij(A,range(f)) *) |
473 using f:inj(A,B) <-> f:bij(A,range(f)) *) |
517 lemma bij_disjoint_Un: |
474 lemma bij_disjoint_Un: |
525 |
482 |
526 (** Restrictions as surjections and bijections *) |
483 (** Restrictions as surjections and bijections *) |
527 |
484 |
528 lemma surj_image: |
485 lemma surj_image: |
529 "f: Pi(A,B) ==> f: surj(A, f``A)" |
486 "f: Pi(A,B) ==> f: surj(A, f``A)" |
530 apply (simp add: surj_def); |
487 apply (simp add: surj_def) |
531 apply (blast intro: apply_equality apply_Pair Pi_type); |
488 apply (blast intro: apply_equality apply_Pair Pi_type) |
532 done |
489 done |
533 |
490 |
534 lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)" |
491 lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)" |
535 apply (auto simp add: restrict_def) |
492 by (auto simp add: restrict_def) |
536 done |
|
537 |
493 |
538 lemma restrict_inj: |
494 lemma restrict_inj: |
539 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)" |
495 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)" |
540 apply (unfold inj_def) |
496 apply (unfold inj_def) |
541 apply (safe elim!: restrict_type2); |
497 apply (safe elim!: restrict_type2, auto) |
542 apply (auto ); |
|
543 done |
498 done |
544 |
499 |
545 lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)" |
500 lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)" |
546 apply (insert restrict_type2 [THEN surj_image]) |
501 apply (insert restrict_type2 [THEN surj_image]) |
547 apply (simp add: restrict_image); |
502 apply (simp add: restrict_image) |
548 done |
503 done |
549 |
504 |
550 lemma restrict_bij: |
505 lemma restrict_bij: |
551 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)" |
506 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)" |
552 apply (unfold inj_def bij_def) |
507 apply (simp add: inj_def bij_def) |
553 apply (blast intro!: restrict restrict_surj intro: box_equals surj_is_fun) |
508 apply (blast intro: restrict_surj surj_is_fun) |
554 done |
509 done |
555 |
510 |
556 |
511 |
557 (*** Lemmas for Ramsey's Theorem ***) |
512 (*** Lemmas for Ramsey's Theorem ***) |
558 |
513 |