|
1475
|
1 |
(* Title: HOL/Fun.thy
|
|
923
|
2 |
ID: $Id$
|
|
1475
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory
|
|
923
|
4 |
Copyright 1994 University of Cambridge
|
|
|
5 |
|
|
2912
|
6 |
Notions about functions.
|
|
923
|
7 |
*)
|
|
|
8 |
|
|
2912
|
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
|