equal
deleted
inserted
replaced
56 "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)" |
56 "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)" |
57 |
57 |
58 inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" |
58 inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" |
59 "inv_image r f == {(x, y). (f x, f y) : r}" |
59 "inv_image r f == {(x, y). (f x, f y) : r}" |
60 |
60 |
61 syntax |
61 abbreviation (output) |
62 reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *} |
62 reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *} |
63 translations |
63 "reflexive = refl UNIV" |
64 "reflexive" == "refl UNIV" |
|
65 |
64 |
66 |
65 |
67 subsection {* The identity relation *} |
66 subsection {* The identity relation *} |
68 |
67 |
69 lemma IdI [intro]: "(a, a) : Id" |
68 lemma IdI [intro]: "(a, a) : Id" |