# HG changeset patch
# User paulson
# Date 969979344 -7200
# Node ID 2683ff1810477626c0119da707456e06734d1a0b
# Parent  6f07d9850141f7930615e3c078f695cdf1ff0f31
removed the obsolete (and badly named) inj_select
Added new theorems about Compl, image, bij/inj/surj

diff -r 6f07d9850141 -r 2683ff181047 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Mon Sep 25 18:25:48 2000 +0200
+++ b/src/HOL/Fun.ML	Tue Sep 26 16:42:24 2000 +0200
@@ -113,15 +113,9 @@
 by (assume_tac 1);
 qed "inj_eq";
 
-Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
-by (etac injD 1);
-by (rtac someI 1);
-by (rtac refl 1);
-qed "inj_select";
-
 (*A one-to-one function has an inverse (given using select).*)
 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
-by (etac inj_select 1);
+by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
 qed "inv_f_f";
 Addsimps [inv_f_f];
 
@@ -426,6 +420,20 @@
 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
 qed "bij_vimage_eq_inv_image";
 
+Goal "surj f ==> -(f``A) <= f``(-A)";
+by (auto_tac (claset(), simpset() addsimps [surj_def]));  
+qed "surj_Compl_image_subset";
+
+Goal "inj f ==> f``(-A) <= -(f``A)";
+by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
+qed "inj_image_Compl_subset";
+
+Goalw [bij_def] "bij f ==> f``(-A) = -(f``A)";
+by (rtac equalityI 1); 
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
+                                                surj_Compl_image_subset]))); 
+qed "bij_image_Compl_eq";
+
 val set_cs = claset() delrules [equalityI];