# HG changeset patch
# User paulson
# Date 935761271 -7200
# Node ID dec7b838f5cb6d10871e1abd9772f0a83d8b0763
# Parent  776d888472aa65aa2cb75ada0e13290fed6e2219
the bij predicate (at last)

diff -r 776d888472aa -r dec7b838f5cb src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Aug 27 10:54:31 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Aug 27 15:41:11 1999 +0200
@@ -185,6 +185,21 @@
 qed "surjD";
 
 
+(** Bijections **)
+
+Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
+by (Blast_tac 1);
+qed "bijI";
+
+Goalw [bij_def] "bij f ==> inj f";
+by (Blast_tac 1);
+qed "bij_is_inj";
+
+Goalw [bij_def] "bij f ==> surj f";
+by (Blast_tac 1);
+qed "bij_is_surj";
+
+
 (*** Lemmas about injective functions and inv ***)
 
 Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
diff -r 776d888472aa -r dec7b838f5cb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Aug 27 10:54:31 1999 +0200
+++ b/src/HOL/Fun.thy	Fri Aug 27 15:41:11 1999 +0200
@@ -39,24 +39,27 @@
 
   o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     "f o g == %x. f(g(x))"
+  
+  inv :: ('a => 'b) => ('b => 'a)
+    "inv(f::'a=>'b) == % y. @x. f(x)=y"
 
   inj_on :: ['a => 'b, 'a set] => bool
     "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
 
-  surj :: ('a => 'b) => bool                   (*surjective*)
-    "surj f == ! y. ? x. y=f(x)"
-  
-  inv :: ('a => 'b) => ('b => 'a)
-    "inv(f::'a=>'b) == % y. @x. f(x)=y"
-  
-
-
 syntax
   inj   :: ('a => 'b) => bool                   (*injective*)
 
 translations
   "inj f" == "inj_on f UNIV"
 
+constdefs
+  surj :: ('a => 'b) => bool                   (*surjective*)
+    "surj f == ! y. ? x. y=f(x)"
+  
+  bij :: ('a => 'b) => bool                    (*bijective*)
+    "bij f == inj f & surj f"
+  
+
 (*The Pi-operator, by Florian Kammueller*)
   
 constdefs