# HG changeset patch
# User paulson
# Date 888573988 -3600
# Node ID 63f0b26017928dbeacaa5d8d5d02ae0c629a6cfb
# Parent  a78ecc7341e373a84c866e0173c9be510bdb7b4a
New vimage laws

diff -r a78ecc7341e3 -r 63f0b2601792 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Thu Feb 26 15:45:33 1998 +0100
+++ b/src/HOL/Vimage.ML	Fri Feb 27 11:06:28 1998 +0100
@@ -38,10 +38,16 @@
 by (Blast_tac 1);
 qed "vimage_empty";
 
+goal thy "f-``(Compl A) = Compl (f-``A)";
+by (Blast_tac 1);
+qed "vimage_Compl";
+
 goal thy "f-``(A Un B) = (f-``A) Un (f-``B)";
 by (Blast_tac 1);
 qed "vimage_Un";
 
+Addsimps [vimage_empty, vimage_Compl, vimage_Un];
+
 (*NOT suitable for rewriting because of the recurrence of {a}*)
 goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
 by (Blast_tac 1);
@@ -51,12 +57,9 @@
 by (Blast_tac 1);
 qed "vimage_Int_subset";
 
-Addsimps [vimage_empty, vimage_Un];
-
 goal thy "f-``UNIV = UNIV";
 by (Blast_tac 1);
 qed "vimage_UNIV";
-
 Addsimps [vimage_UNIV];
 
 goal thy "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
diff -r a78ecc7341e3 -r 63f0b2601792 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Feb 26 15:45:33 1998 +0100
+++ b/src/ZF/equalities.ML	Fri Feb 27 11:06:28 1998 +0100
@@ -476,6 +476,16 @@
 by (Blast_tac 1);
 qed "vimage_Int_subset";
 
+goalw thy [function_def]
+    "!!f. function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)";
+by (Blast_tac 1);
+qed "function_vimage_Int";
+
+goalw thy [function_def]
+    "!!f. function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
+by (Blast_tac 1);
+qed "function_vimage_Diff";
+
 goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
 by (Blast_tac 1);
 qed "vimage_Int_square_subset";