# HG changeset patch
# User paulson
# Date 951298982 -3600
# Node ID 16216dbe4f20daae17a6e3989d7a11b73958881a
# Parent  95c022a866ca4c207a8b65124ad1f7e403b2f411
new theorems inj_iff, surj_iff

diff -r 95c022a866ca -r 16216dbe4f20 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Feb 23 10:41:37 2000 +0100
+++ b/src/HOL/Fun.ML	Wed Feb 23 10:43:02 2000 +0100
@@ -161,6 +161,11 @@
 qed "inj_on_inverseI";
 val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
 
+Goal "(inj f) = (inv f o f = id)";
+by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
+by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
+qed "inj_iff";
+
 Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
 by (Blast_tac 1);
 qed "inj_onD";
@@ -230,6 +235,11 @@
 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
 qed "surj_imp_inj_inv";
 
+Goal "(surj f) = (f o inv f = id)";
+by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
+by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
+qed "surj_iff";
+
 
 (** Bijections **)