src/HOL/Fun.thy
changeset 7374 dec7b838f5cb
parent 6171 cd237a10cbf8
child 8258 666d3a4f3b9d
     1.1 --- a/src/HOL/Fun.thy	Fri Aug 27 10:54:31 1999 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Aug 27 15:41:11 1999 +0200
     1.3 @@ -39,24 +39,27 @@
     1.4  
     1.5    o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     1.6      "f o g == %x. f(g(x))"
     1.7 +  
     1.8 +  inv :: ('a => 'b) => ('b => 'a)
     1.9 +    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.10  
    1.11    inj_on :: ['a => 'b, 'a set] => bool
    1.12      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.13  
    1.14 -  surj :: ('a => 'b) => bool                   (*surjective*)
    1.15 -    "surj f == ! y. ? x. y=f(x)"
    1.16 -  
    1.17 -  inv :: ('a => 'b) => ('b => 'a)
    1.18 -    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.19 -  
    1.20 -
    1.21 -
    1.22  syntax
    1.23    inj   :: ('a => 'b) => bool                   (*injective*)
    1.24  
    1.25  translations
    1.26    "inj f" == "inj_on f UNIV"
    1.27  
    1.28 +constdefs
    1.29 +  surj :: ('a => 'b) => bool                   (*surjective*)
    1.30 +    "surj f == ! y. ? x. y=f(x)"
    1.31 +  
    1.32 +  bij :: ('a => 'b) => bool                    (*bijective*)
    1.33 +    "bij f == inj f & surj f"
    1.34 +  
    1.35 +
    1.36  (*The Pi-operator, by Florian Kammueller*)
    1.37    
    1.38  constdefs