diff -r 52b13dfbe954 -r 43c081a0858d src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Jun 10 10:34:55 1999 +0200 +++ b/src/HOL/Relation.thy Thu Jun 10 10:35:58 1999 +0200 @@ -17,22 +17,37 @@ Image_def "r ^^ s == {y. ? x:s. (x,y):r}" constdefs - Id :: "('a * 'a)set" (*the identity relation*) + Id :: "('a * 'a)set" (*the identity relation*) "Id == {p. ? x. p = (x,x)}" diag :: "'a set => ('a * 'a)set" "diag(A) == UN x:A. {(x,x)}" - Domain :: "('a*'b) set => 'a set" + Domain :: "('a*'b) set => 'a set" "Domain(r) == {x. ? y. (x,y):r}" - Range :: "('a*'b) set => 'b set" + Range :: "('a*'b) set => 'b set" "Range(r) == Domain(r^-1)" - trans :: "('a * 'a)set => bool" (*transitivity predicate*) + refl :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*) + "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)" + + sym :: "('a*'a) set=>bool" (*symmetry predicate*) + "sym(r) == ALL x y. (x,y): r --> (y,x): r" + + antisym:: "('a * 'a)set => bool" (*antisymmetry predicate*) + "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y" + + trans :: "('a * 'a)set => bool" (*transitivity predicate*) "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" - Univalent :: "('a * 'b)set => bool" + Univalent :: "('a * 'b)set => bool" "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" +syntax + reflexive :: "('a * 'a)set => bool" (*reflexivity over a type*) + +translations + "reflexive" == "refl UNIV" + end