11 "r^-1 == {(y, x). (x, y) : r}" |
11 "r^-1 == {(y, x). (x, y) : r}" |
12 syntax (xsymbols) |
12 syntax (xsymbols) |
13 converse :: "('a * 'b) set => ('b * 'a) set" ("(_\\<inverse>)" [1000] 999) |
13 converse :: "('a * 'b) set => ('b * 'a) set" ("(_\\<inverse>)" [1000] 999) |
14 |
14 |
15 constdefs |
15 constdefs |
16 comp :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr "O" 60) |
16 comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60) |
17 "r O s == {(x,z). ? y. (x,y):s & (y,z):r}" |
17 "r O s == {(x,z). ? y. (x,y):s & (y,z):r}" |
18 |
18 |
19 Image :: "[('a*'b) set,'a set] => 'b set" (infixl "``" 90) |
19 Image :: "[('a * 'b) set, 'a set] => 'b set" (infixl "``" 90) |
20 "r `` s == {y. ? x:s. (x,y):r}" |
20 "r `` s == {y. ? x:s. (x,y):r}" |
21 |
21 |
22 Id :: "('a * 'a)set" (*the identity relation*) |
22 Id :: "('a * 'a) set" (*the identity relation*) |
23 "Id == {p. ? x. p = (x,x)}" |
23 "Id == {p. ? x. p = (x,x)}" |
24 |
24 |
25 diag :: "'a set => ('a * 'a)set" (*diagonal: identity over a set*) |
25 diag :: "'a set => ('a * 'a) set" (*diagonal: identity over a set*) |
26 "diag(A) == UN x:A. {(x,x)}" |
26 "diag(A) == UN x:A. {(x,x)}" |
27 |
27 |
28 Domain :: "('a*'b) set => 'a set" |
28 Domain :: "('a * 'b) set => 'a set" |
29 "Domain(r) == {x. ? y. (x,y):r}" |
29 "Domain(r) == {x. ? y. (x,y):r}" |
30 |
30 |
31 Range :: "('a*'b) set => 'b set" |
31 Range :: "('a * 'b) set => 'b set" |
32 "Range(r) == Domain(r^-1)" |
32 "Range(r) == Domain(r^-1)" |
33 |
33 |
34 Field :: "('a*'a)set=>'a set" |
34 Field :: "('a * 'a) set => 'a set" |
35 "Field r == Domain r Un Range r" |
35 "Field r == Domain r Un Range r" |
36 |
36 |
37 refl :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*) |
37 refl :: "['a set, ('a * 'a) set] => bool" (*reflexivity over a set*) |
38 "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)" |
38 "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)" |
39 |
39 |
40 sym :: "('a*'a) set=>bool" (*symmetry predicate*) |
40 sym :: "('a * 'a) set => bool" (*symmetry predicate*) |
41 "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
41 "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
42 |
42 |
43 antisym:: "('a * 'a)set => bool" (*antisymmetry predicate*) |
43 antisym:: "('a * 'a) set => bool" (*antisymmetry predicate*) |
44 "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y" |
44 "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y" |
45 |
45 |
46 trans :: "('a * 'a)set => bool" (*transitivity predicate*) |
46 trans :: "('a * 'a) set => bool" (*transitivity predicate*) |
47 "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" |
47 "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" |
48 |
48 |
49 single_valued :: "('a * 'b)set => bool" |
49 single_valued :: "('a * 'b) set => bool" |
50 "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" |
50 "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" |
51 |
51 |
52 fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set" |
52 fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set" |
53 "fun_rel_comp f R == {g. !x. (f x, g x) : R}" |
53 "fun_rel_comp f R == {g. !x. (f x, g x) : R}" |
54 |
54 |
|
55 inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" |
|
56 "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
|
57 |
55 syntax |
58 syntax |
56 reflexive :: "('a * 'a)set => bool" (*reflexivity over a type*) |
59 reflexive :: "('a * 'a) set => bool" (*reflexivity over a type*) |
57 translations |
60 translations |
58 "reflexive" == "refl UNIV" |
61 "reflexive" == "refl UNIV" |
59 |
62 |
60 end |
63 end |