8 |
8 |
9 Fun = Vimage + equalities + |
9 Fun = Vimage + equalities + |
10 |
10 |
11 instance set :: (term) order |
11 instance set :: (term) order |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
13 consts |
|
14 |
|
15 id :: 'a => 'a |
|
16 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
|
17 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
|
18 inj_on :: ['a => 'b, 'a set] => bool |
|
19 inv :: ('a => 'b) => ('b => 'a) |
|
20 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
|
21 |
|
22 nonterminals |
13 nonterminals |
23 updbinds updbind |
14 updbinds updbind |
|
15 |
|
16 consts |
|
17 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
24 |
18 |
25 syntax |
19 syntax |
26 |
20 |
27 (* Let expressions *) |
21 (* Let expressions *) |
28 |
22 |
34 translations |
28 translations |
35 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
29 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
36 "f(x:=y)" == "fun_upd f x y" |
30 "f(x:=y)" == "fun_upd f x y" |
37 |
31 |
38 defs |
32 defs |
|
33 fun_upd_def "f(a:=b) == % x. if x=a then b else f x" |
39 |
34 |
40 id_def "id == %x. x" |
35 |
41 o_def "f o g == %x. f(g(x))" |
36 constdefs |
42 inj_def "inj f == ! x y. f(x)=f(y) --> x=y" |
37 id :: 'a => 'a |
43 inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
38 "id == %x. x" |
44 surj_def "surj f == ! y. ? x. y=f(x)" |
|
45 inv_def "inv(f::'a=>'b) == % y. @x. f(x)=y" |
|
46 fun_upd_def "f(a:=b) == % x. if x=a then b else f x" |
|
47 |
39 |
|
40 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
|
41 "f o g == %x. f(g(x))" |
|
42 |
|
43 inj_on :: ['a => 'b, 'a set] => bool |
|
44 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
|
45 |
|
46 surj :: ('a => 'b) => bool (*surjective*) |
|
47 "surj f == ! y. ? x. y=f(x)" |
|
48 |
|
49 inv :: ('a => 'b) => ('b => 'a) |
|
50 "inv(f::'a=>'b) == % y. @x. f(x)=y" |
|
51 |
|
52 |
|
53 |
|
54 syntax |
|
55 inj :: ('a => 'b) => bool (*injective*) |
|
56 |
|
57 translations |
|
58 "inj f" == "inj_on f UNIV" |
48 |
59 |
49 (*The Pi-operator, by Florian Kammueller*) |
60 (*The Pi-operator, by Florian Kammueller*) |
50 |
61 |
51 constdefs |
62 constdefs |
52 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
63 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |