new theorem INT_Un
authorpaulson
Tue Dec 01 10:39:35 1998 +0100 (1998-12-01)
changeset 599984fe61a08c17
parent 5998 b2ecd577b8a3
child 6000 aa84c30c1f61
new theorem INT_Un
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Tue Dec 01 10:39:02 1998 +0100
     1.2 +++ b/src/HOL/equalities.ML	Tue Dec 01 10:39:35 1998 +0100
     1.3 @@ -477,7 +477,7 @@
     1.4  qed "UN_insert";
     1.5  Addsimps[UN_insert];
     1.6  
     1.7 -Goal "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
     1.8 +Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
     1.9  by (Blast_tac 1);
    1.10  qed "UN_Un";
    1.11  
    1.12 @@ -490,6 +490,10 @@
    1.13  qed "INT_insert";
    1.14  Addsimps[INT_insert];
    1.15  
    1.16 +Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
    1.17 +by (Blast_tac 1);
    1.18 +qed "INT_Un";
    1.19 +
    1.20  Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
    1.21  by (Blast_tac 1);
    1.22  qed "INT_insert_distrib";