New theorems
authorpaulson
Tue Mar 03 15:12:57 1998 +0100 (1998-03-03)
changeset 4674248b876c2fa8
parent 4673 59d80bacee62
child 4675 6efc56450d09
New theorems
src/HOL/Vimage.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Vimage.ML	Tue Mar 03 15:12:25 1998 +0100
     1.2 +++ b/src/HOL/Vimage.ML	Tue Mar 03 15:12:57 1998 +0100
     1.3 @@ -46,7 +46,11 @@
     1.4  by (Blast_tac 1);
     1.5  qed "vimage_Un";
     1.6  
     1.7 -Addsimps [vimage_empty, vimage_Compl, vimage_Un];
     1.8 +goal thy "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
     1.9 +by (Blast_tac 1);
    1.10 +qed "vimage_UN";
    1.11 +
    1.12 +Addsimps [vimage_empty, vimage_Un];
    1.13  
    1.14  (*NOT suitable for rewriting because of the recurrence of {a}*)
    1.15  goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
     2.1 --- a/src/HOL/equalities.ML	Tue Mar 03 15:12:25 1998 +0100
     2.2 +++ b/src/HOL/equalities.ML	Tue Mar 03 15:12:57 1998 +0100
     2.3 @@ -504,6 +504,10 @@
     2.4  by (Blast_tac 1);
     2.5  qed "Int_Union";
     2.6  
     2.7 +goal thy "Union(B) Int A = (UN C:B. C Int A)";
     2.8 +by (Blast_tac 1);
     2.9 +qed "Int_Union2";
    2.10 +
    2.11  (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
    2.12     Union of a family of unions **)
    2.13  goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
    2.14 @@ -573,6 +577,10 @@
    2.15  qed "Diff_cancel";
    2.16  Addsimps[Diff_cancel];
    2.17  
    2.18 +goal thy "!!A B. A Int B = {} ==> A-B = A";
    2.19 +by (blast_tac (claset() addEs [equalityE]) 1);
    2.20 +qed "Diff_triv";
    2.21 +
    2.22  goal thy "{}-A = {}";
    2.23  by (Blast_tac 1);
    2.24  qed "empty_Diff";