author  wenzelm 
Wed, 21 Nov 2001 00:33:40 +0100  
changeset 12258  5da24e7e9aba 
parent 12114  a8e860c86252 
child 12338  de0f4a63baa5 
permissions  rwrr 
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 

12258  9 
Fun = Typedef + 
2912  10 

4059  11 
instance set :: (term) order 
12 
(subset_refl,subset_trans,subset_antisym,psubset_eq) 

6171  13 
consts 
14 
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" 

15 

9141  16 
nonterminals 
17 
updbinds updbind 

5305  18 
syntax 
19 
"_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)") 

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

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

8258  22 
"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900) 
5305  23 

24 
translations 

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

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

2912  27 

28 
defs 

6171  29 
fun_upd_def "f(a:=b) == % x. if x=a then b else f x" 
2912  30 

9340  31 
(* Hint: to define the sum of two functions (or maps), use sum_case. 
32 
A nice infix syntax could be defined (in Datatype.thy or below) by 

33 
consts 

34 
fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) 

35 
translations 

36 
"fun_sum" == "sum_case" 

37 
*) 

12258  38 

6171  39 
constdefs 
40 
id :: 'a => 'a 

41 
"id == %x. x" 

42 

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

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

11123  45 

6171  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 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11609
diff
changeset

49 
syntax (xsymbols) 
9352  50 
"op o" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\\<circ>" 55) 
51 

6171  52 
syntax 
53 
inj :: ('a => 'b) => bool (*injective*) 

54 

55 
translations 

56 
"inj f" == "inj_on f UNIV" 

5852  57 

7374  58 
constdefs 
59 
surj :: ('a => 'b) => bool (*surjective*) 

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

12258  61 

7374  62 
bij :: ('a => 'b) => bool (*bijective*) 
63 
"bij f == inj f & surj f" 

12258  64 

7374  65 

5852  66 
(*The Pioperator, by Florian Kammueller*) 
12258  67 

5852  68 
constdefs 
69 
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

70 
"Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}" 
5852  71 

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

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

73 
"restrict f A == (%x. if x : A then f x else arbitrary)" 
5852  74 

75 
syntax 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

76 
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) 
12258  77 
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60) 
5852  78 
"@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10) 
79 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

80 
(*Giving funcset the arrow syntax (namely >) clashes with other theories*) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

81 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11609
diff
changeset

82 
syntax (xsymbols) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11123
diff
changeset

83 
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<Pi> _\\<in>_./ _)" 10) 
5852  84 

85 
translations 

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

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

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

89 

90 
constdefs 

9309  91 
compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" 
5852  92 
"compose A g f == lam x : A. g(f x)" 
93 

2912  94 
end 
5852  95 

96 
ML 

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