equal
deleted
inserted
replaced
459 by (Blast_tac 1); |
459 by (Blast_tac 1); |
460 qed "image_Int_square"; |
460 qed "image_Int_square"; |
461 |
461 |
462 Addsimps [image_0, image_Un]; |
462 Addsimps [image_0, image_Un]; |
463 |
463 |
|
464 (*Image laws for special relations*) |
|
465 goal ZF.thy "0``A = 0"; |
|
466 by (Blast_tac 1); |
|
467 qed "image_0_left"; |
|
468 Addsimps [image_0_left]; |
|
469 |
|
470 goal ZF.thy "(r Un s)``A = (r``A) Un (s``A)"; |
|
471 by (Blast_tac 1); |
|
472 qed "image_Un_left"; |
|
473 |
|
474 goal ZF.thy "(r Int s)``A <= (r``A) Int (s``A)"; |
|
475 by (Blast_tac 1); |
|
476 qed "image_Int_subset_left"; |
|
477 |
464 |
478 |
465 (** Inverse Image **) |
479 (** Inverse Image **) |
466 |
480 |
467 goal ZF.thy "r-``0 = 0"; |
481 goal ZF.thy "r-``0 = 0"; |
468 by (Blast_tac 1); |
482 by (Blast_tac 1); |
493 goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A"; |
507 goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A"; |
494 by (Blast_tac 1); |
508 by (Blast_tac 1); |
495 qed "vimage_Int_square"; |
509 qed "vimage_Int_square"; |
496 |
510 |
497 Addsimps [vimage_0, vimage_Un]; |
511 Addsimps [vimage_0, vimage_Un]; |
|
512 |
|
513 |
|
514 (*Invese image laws for special relations*) |
|
515 goal ZF.thy "0-``A = 0"; |
|
516 by (Blast_tac 1); |
|
517 qed "vimage_0_left"; |
|
518 Addsimps [vimage_0_left]; |
|
519 |
|
520 goal ZF.thy "(r Un s)-``A = (r-``A) Un (s-``A)"; |
|
521 by (Blast_tac 1); |
|
522 qed "vimage_Un_left"; |
|
523 |
|
524 goal ZF.thy "(r Int s)-``A <= (r-``A) Int (s-``A)"; |
|
525 by (Blast_tac 1); |
|
526 qed "vimage_Int_subset_left"; |
498 |
527 |
499 |
528 |
500 (** Converse **) |
529 (** Converse **) |
501 |
530 |
502 goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; |
531 goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; |