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 abbreviation (output) |
61 abbreviation |
62 reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *} |
62 reflexive :: "('a * 'a) set => bool" -- {* reflexivity over a type *} |
63 "reflexive = refl UNIV" |
63 "reflexive == refl UNIV" |
64 |
64 |
65 |
65 |
66 subsection {* The identity relation *} |
66 subsection {* The identity relation *} |
67 |
67 |
68 lemma IdI [intro]: "(a, a) : Id" |
68 lemma IdI [intro]: "(a, a) : Id" |