# HG changeset patch
# User paulson
# Date 969718298 -7200
# Node ID 2f5686cf8c9ad7c3a3459529a1d8f10a6f1565d5
# Parent  ddb3a014f7216584a9937fd80307bc0fd12f392f
new theorems and comment

diff -r ddb3a014f721 -r 2f5686cf8c9a src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sat Sep 23 16:08:23 2000 +0200
+++ b/src/HOL/Fun.ML	Sat Sep 23 16:11:38 2000 +0200
@@ -130,6 +130,10 @@
 by (etac inv_f_f 1);
 qed "inv_f_eq";
 
+Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
+by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
+qed "inj_imp_inv_eq";
+
 (* Useful??? *)
 val [oneone,minor] = Goal
     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
@@ -238,6 +242,12 @@
 by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
 qed "surj_iff";
 
+Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
+by (rtac ext 1);
+by (dres_inst_tac [("x","inv f x")] spec 1); 
+by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
+qed "surj_imp_inv_eq";
+
 
 (** Bijections **)
 
@@ -268,6 +278,13 @@
 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
 qed "inv_inv_eq";
 
+(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
+    f(True)=f(False)=True.  Then it's consistent with axiom someI that
+    inv(f) could be any function at all, including the identity function.
+    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
+    inv(inv(f))=f all fail.
+**)
+
 Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
 by (rtac (inv_equality) 1);
 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));