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 

8960

9 
Fun = Vimage + equalities +

2912

10 

4059

11 
instance set :: (term) order


12 
(subset_refl,subset_trans,subset_antisym,psubset_eq)

5305

13 
nonterminals


14 
updbinds updbind


15 

6171

16 
consts


17 
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"


18 

5305

19 
syntax


20 


21 
(* Let expressions *)


22 


23 
"_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")


24 
"" :: updbind => updbinds ("_")


25 
"_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")

8258

26 
"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900)

5305

27 


28 
translations


29 
"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"


30 
"f(x:=y)" == "fun_upd f x y"

2912

31 


32 
defs

6171

33 
fun_upd_def "f(a:=b) == % x. if x=a then b else f x"

2912

34 

6171

35 


36 
constdefs


37 
id :: 'a => 'a


38 
"id == %x. x"


39 


40 
o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)


41 
"f o g == %x. f(g(x))"

7374

42 


43 
inv :: ('a => 'b) => ('b => 'a)


44 
"inv(f::'a=>'b) == % y. @x. f(x)=y"

6171

45 


46 
inj_on :: ['a => 'b, 'a set] => bool


47 
"inj_on f A == ! x:A. ! y:A. f(x)=f(y) > x=y"

2912

48 

6171

49 
syntax


50 
inj :: ('a => 'b) => bool (*injective*)


51 


52 
translations


53 
"inj f" == "inj_on f UNIV"

5852

54 

7374

55 
constdefs


56 
surj :: ('a => 'b) => bool (*surjective*)


57 
"surj f == ! y. ? x. y=f(x)"


58 


59 
bij :: ('a => 'b) => bool (*bijective*)


60 
"bij f == inj f & surj f"


61 


62 

5852

63 
(*The Pioperator, by Florian Kammueller*)


64 


65 
constdefs


66 
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"


67 
"Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"


68 


69 
restrict :: "['a => 'b, 'a set] => ('a => 'b)"


70 
"restrict f A == (%x. if x : A then f x else (@ y. True))"


71 


72 
syntax


73 
"@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)


74 
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)


75 
"@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)


76 


77 
(*Giving funcset the nice arrow syntax > clashes with existing theories*)


78 


79 
translations


80 
"PI x:A. B" => "Pi A (%x. B)"


81 
"A funcset B" => "Pi A (_K B)"


82 
"lam x:A. f" == "restrict (%x. f) A"


83 


84 
constdefs


85 
Applyall :: "[('a => 'b) set, 'a]=> 'b set"


86 
"Applyall F a == (%f. f a) `` F"


87 


88 
compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"


89 
"compose A g f == lam x : A. g(f x)"


90 


91 
Inv :: "['a set, 'a => 'b] => ('b => 'a)"


92 
"Inv A f == (% x. (@ y. y : A & f y = x))"


93 


94 

2912

95 
end

5852

96 


97 
ML


98 
val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
