equal
deleted
inserted
replaced
10 imports Product_Type |
10 imports Product_Type |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definitions *} |
13 subsection {* Definitions *} |
14 |
14 |
15 constdefs |
15 definition |
16 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |
16 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |
17 "r^-1 == {(y, x). (x, y) : r}" |
17 "r^-1 == {(y, x). (x, y) : r}" |
18 syntax (xsymbols) |
18 |
19 converse :: "('a * 'b) set => ('b * 'a) set" ("(_\<inverse>)" [1000] 999) |
19 const_syntax (xsymbols) |
20 |
20 converse ("(_\<inverse>)" [1000] 999) |
21 constdefs |
21 |
|
22 definition |
22 rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60) |
23 rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60) |
23 "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}" |
24 "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}" |
24 |
25 |
25 Image :: "[('a * 'b) set, 'a set] => 'b set" (infixl "``" 90) |
26 Image :: "[('a * 'b) set, 'a set] => 'b set" (infixl "``" 90) |
26 "r `` s == {y. EX x:s. (x,y):r}" |
27 "r `` s == {y. EX x:s. (x,y):r}" |