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 |
|
4648
|
9 |
Fun = Vimage +
|
2912
|
10 |
|
4059
|
11 |
instance set :: (term) order
|
|
12 |
(subset_refl,subset_trans,subset_antisym,psubset_eq)
|
2912
|
13 |
consts
|
|
14 |
|
4830
|
15 |
inj, surj :: ('a => 'b) => bool (*inj/surjective*)
|
|
16 |
inj_on :: ['a => 'b, 'a set] => bool
|
|
17 |
inv :: ('a => 'b) => ('b => 'a)
|
2912
|
18 |
|
|
19 |
defs
|
|
20 |
|
4830
|
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)"
|
2912
|
25 |
|
|
26 |
end
|