src/HOL/Fun.thy
author nipkow
Mon Apr 27 16:45:11 1998 +0200 (1998-04-27)
changeset 4830 bd73675adbed
parent 4648 f04da668581c
child 5305 513925de8962
permissions -rw-r--r--
Added a few lemmas.
Renamed expand_const -> split_const.
     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 = Vimage +
    10 
    11 instance set :: (term) order
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    13 consts
    14 
    15   inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    16   inj_on      :: ['a => 'b, 'a set] => bool
    17   inv         :: ('a => 'b) => ('b => 'a)
    18 
    19 defs
    20 
    21   inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
    22   inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    23   surj_def    "surj f         == ! y. ? x. y=f(x)"
    24   inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    25 
    26 end