new theorem UN_empty; it and Un_empty inserted by AddIffs
authorpaulson
Wed Jun 21 10:32:57 2000 +0200 (2000-06-21)
changeset 90983a0912a127ec
parent 9097 44cd0f9f8e5b
child 9099 f713ef362ad0
new theorem UN_empty; it and Un_empty inserted by AddIffs
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Wed Jun 21 10:31:34 2000 +0200
     1.2 +++ b/src/HOL/equalities.ML	Wed Jun 21 10:32:57 2000 +0200
     1.3 @@ -366,7 +366,7 @@
     1.4  Goal "(A Un B = {}) = (A = {} & B = {})";
     1.5  by (blast_tac (claset() addEs [equalityCE]) 1);
     1.6  qed "Un_empty";
     1.7 -Addsimps[Un_empty];
     1.8 +AddIffs[Un_empty];
     1.9  
    1.10  Goal "(A Un B <= C) = (A <= C & B <= C)";
    1.11  by (Blast_tac 1);
    1.12 @@ -461,8 +461,8 @@
    1.13  by (Blast_tac 1);
    1.14  qed "Union_Int_subset";
    1.15  
    1.16 -Goal "(Union M = {}) = (! A : M. A = {})"; 
    1.17 -by (blast_tac (claset() addEs [equalityCE]) 1);
    1.18 +Goal "(Union A = {}) = (ALL x:A. x={})";
    1.19 +by Auto_tac; 
    1.20  qed "Union_empty_conv"; 
    1.21  AddIffs [Union_empty_conv];
    1.22  
    1.23 @@ -596,6 +596,11 @@
    1.24  by (Blast_tac 1);
    1.25  qed "INT_eq";
    1.26  
    1.27 +Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
    1.28 +by Auto_tac; 
    1.29 +qed "UN_empty";
    1.30 +AddIffs [UN_empty];
    1.31 +
    1.32  
    1.33  (*Distributive laws...*)
    1.34