src/HOL/Fun.thy
changeset 2912 3fac3e8d5d3e
parent 1475 7f5a4cd08209
child 4059 59c1422c9da5
     1.1 --- a/src/HOL/Fun.thy	Fri Apr 04 16:27:39 1997 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Apr 04 16:33:28 1997 +0200
     1.3 @@ -3,7 +3,22 @@
     1.4      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Lemmas about functions.
     1.8 +Notions about functions.
     1.9  *)
    1.10  
    1.11 -Fun = Set
    1.12 +Fun = Set +
    1.13 +
    1.14 +consts
    1.15 +
    1.16 +  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    1.17 +  inj_onto      :: ['a => 'b, 'a set] => bool
    1.18 +  inv           :: ('a => 'b) => ('b => 'a)
    1.19 +
    1.20 +defs
    1.21 +
    1.22 +  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    1.23 +  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.24 +  surj_def      "surj f         == ! y. ? x. y=f(x)"
    1.25 +  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    1.26 +
    1.27 +end