src/HOL/Fun.thy
author nipkow
Fri Apr 04 16:33:28 1997 +0200 (1997-04-04)
changeset 2912 3fac3e8d5d3e
parent 1475 7f5a4cd08209
child 4059 59c1422c9da5
permissions -rw-r--r--
moved inj and surj from Set to Fun and Inv -> inv.
     1 (*  Title:      HOL/Fun.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Notions about functions.
     7 *)
     8 
     9 Fun = Set +
    10 
    11 consts
    12 
    13   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    14   inj_onto      :: ['a => 'b, 'a set] => bool
    15   inv           :: ('a => 'b) => ('b => 'a)
    16 
    17 defs
    18 
    19   inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    20   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    21   surj_def      "surj f         == ! y. ? x. y=f(x)"
    22   inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    23 
    24 end