src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Tue Apr 28 13:50:41 1998 +0200
+++ b/src/ZF/equalities.ML	Tue Apr 28 13:51:39 1998 +0200
@@ -461,6 +461,20 @@
 
 Addsimps [image_0, image_Un];
 
+(*Image laws for special relations*)
+goal ZF.thy "0``A = 0";
+by (Blast_tac 1);
+qed "image_0_left";
+Addsimps [image_0_left];
+
+goal ZF.thy "(r Un s)``A = (r``A) Un (s``A)";
+by (Blast_tac 1);
+qed "image_Un_left";
+
+goal ZF.thy "(r Int s)``A <= (r``A) Int (s``A)";
+by (Blast_tac 1);
+qed "image_Int_subset_left";
+
 
 (** Inverse Image **)
 
@@ -497,6 +511,21 @@
 Addsimps [vimage_0, vimage_Un];
 
 
+(*Invese image laws for special relations*)
+goal ZF.thy "0-``A = 0";
+by (Blast_tac 1);
+qed "vimage_0_left";
+Addsimps [vimage_0_left];
+
+goal ZF.thy "(r Un s)-``A = (r-``A) Un (s-``A)";
+by (Blast_tac 1);
+qed "vimage_Un_left";
+
+goal ZF.thy "(r Int s)-``A <= (r-``A) Int (s-``A)";
+by (Blast_tac 1);
+qed "vimage_Int_subset_left";
+
+
 (** Converse **)
 
 goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";