equal
deleted
inserted
replaced
475 Goal "(UN x:insert a A. B x) = B a Un UNION A B"; |
475 Goal "(UN x:insert a A. B x) = B a Un UNION A B"; |
476 by (Blast_tac 1); |
476 by (Blast_tac 1); |
477 qed "UN_insert"; |
477 qed "UN_insert"; |
478 Addsimps[UN_insert]; |
478 Addsimps[UN_insert]; |
479 |
479 |
480 Goal "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))"; |
480 Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)"; |
481 by (Blast_tac 1); |
481 by (Blast_tac 1); |
482 qed "UN_Un"; |
482 qed "UN_Un"; |
483 |
483 |
484 Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)"; |
484 Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)"; |
485 by (Blast_tac 1); |
485 by (Blast_tac 1); |
487 |
487 |
488 Goal "(INT x:insert a A. B x) = B a Int INTER A B"; |
488 Goal "(INT x:insert a A. B x) = B a Int INTER A B"; |
489 by (Blast_tac 1); |
489 by (Blast_tac 1); |
490 qed "INT_insert"; |
490 qed "INT_insert"; |
491 Addsimps[INT_insert]; |
491 Addsimps[INT_insert]; |
|
492 |
|
493 Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)"; |
|
494 by (Blast_tac 1); |
|
495 qed "INT_Un"; |
492 |
496 |
493 Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; |
497 Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; |
494 by (Blast_tac 1); |
498 by (Blast_tac 1); |
495 qed "INT_insert_distrib"; |
499 qed "INT_insert_distrib"; |
496 |
500 |