# HG changeset patch
# User paulson
# Date 949331889 -3600
# Node ID a9966d5ab84d4bee227961a8a8ab3424a20dc184
# Parent  988a7737e15843c2b64ea9981d8b3dc7e426e1d3
various theorems about image and inverse image

diff -r 988a7737e158 -r a9966d5ab84d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Mon Jan 31 16:13:28 2000 +0100
+++ b/src/HOL/Fun.ML	Mon Jan 31 16:18:09 2000 +0100
@@ -262,6 +262,36 @@
 by (blast_tac (claset() addIs [sym]) 1);
 qed "vimage_image_eq";
 
+Goal "f `` (f -`` A) <= A";
+by (Blast_tac 1);
+qed "image_vimage_subset";
+
+Goal "f `` (f -`` A) = A Int range f";
+by (Blast_tac 1);
+qed "image_vimage_eq";
+Addsimps [image_vimage_eq];
+
+Goal "surj f ==> f `` (f -`` A) = A";
+by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
+qed "surj_image_vimage_eq";
+
+Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
+by (Blast_tac 1);
+qed "inj_vimage_image_eq";
+
+Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
+by (blast_tac (claset() addIs [sym]) 1);
+qed "vimage_subsetD";
+
+Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
+by (Blast_tac 1);
+qed "vimage_subsetI";
+
+Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
+by (blast_tac (claset() delrules [subsetI]
+			addIs [vimage_subsetI, vimage_subsetD]) 1);
+qed "vimage_subset_eq";
+
 Goal "f``(A Int B) <= f``A Int f``B";
 by (Blast_tac 1);
 qed "image_Int_subset";