new thms image_0_left, image_Un_left, etc.
--- 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)";