src/HOL/equalities.ML
changeset 1179 7678408f9751
parent 923 ff1574a81019
child 1264 3eb91524b938
     1.1 --- a/src/HOL/equalities.ML	Mon Jul 03 15:39:53 1995 +0200
     1.2 +++ b/src/HOL/equalities.ML	Wed Jul 05 20:14:22 1995 +0200
     1.3 @@ -22,6 +22,12 @@
     1.4  
     1.5  (** insert **)
     1.6  
     1.7 +goal Set.thy "insert a A ~= {}";
     1.8 +by (fast_tac (set_cs addEs [equalityCE]) 1);
     1.9 +qed"insert_not_empty";
    1.10 +
    1.11 +bind_thm("empty_not_insert",insert_not_empty RS not_sym);
    1.12 +
    1.13  goal Set.thy "!!a. a:A ==> insert a A = A";
    1.14  by (fast_tac eq_cs 1);
    1.15  qed "insert_absorb";
    1.16 @@ -185,6 +191,14 @@
    1.17  
    1.18  (*Basic identities*)
    1.19  
    1.20 +goal Set.thy "(UN x:{}. B x) = {}";
    1.21 +by (fast_tac eq_cs 1);
    1.22 +qed "UN_empty";
    1.23 +
    1.24 +goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
    1.25 +by (fast_tac eq_cs 1);
    1.26 +qed "UN_insert";
    1.27 +
    1.28  goal Set.thy "Union(range(f)) = (UN x.f(x))";
    1.29  by (fast_tac eq_cs 1);
    1.30  qed "Union_range_eq";
    1.31 @@ -325,8 +339,10 @@
    1.32  
    1.33  val set_ss = set_ss addsimps
    1.34    [in_empty,in_insert,insert_subset,
    1.35 +   insert_not_empty,empty_not_insert,
    1.36     Int_absorb,Int_empty_left,Int_empty_right,
    1.37     Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
    1.38 +   UN_empty, UN_insert,
    1.39     UN1_constant,image_empty,
    1.40     Compl_disjoint,double_complement,
    1.41     Union_empty,Union_insert,empty_subsetI,subset_refl,