src/HOL/Relation.thy
 changeset 6806 43c081a0858d parent 5978 fa2c2dd74f8c child 7014 11ee650edcd2
```     1.1 --- a/src/HOL/Relation.thy	Thu Jun 10 10:34:55 1999 +0200
1.2 +++ b/src/HOL/Relation.thy	Thu Jun 10 10:35:58 1999 +0200
1.3 @@ -17,22 +17,37 @@
1.4    Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
1.5
1.6  constdefs
1.7 -  Id          :: "('a * 'a)set"               (*the identity relation*)
1.8 +  Id     :: "('a * 'a)set"                 (*the identity relation*)
1.9        "Id == {p. ? x. p = (x,x)}"
1.10
1.11    diag   :: "'a set => ('a * 'a)set"
1.12      "diag(A) == UN x:A. {(x,x)}"
1.13
1.14 -  Domain      :: "('a*'b) set => 'a set"
1.15 +  Domain :: "('a*'b) set => 'a set"
1.16      "Domain(r) == {x. ? y. (x,y):r}"
1.17
1.18 -  Range       :: "('a*'b) set => 'b set"
1.19 +  Range  :: "('a*'b) set => 'b set"
1.20      "Range(r) == Domain(r^-1)"
1.21
1.22 -  trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
1.23 +  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
1.24 +    "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
1.25 +
1.26 +  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
1.27 +    "sym(r) == ALL x y. (x,y): r --> (y,x): r"
1.28 +
1.29 +  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
1.30 +    "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
1.31 +
1.32 +  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
1.33      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.34
1.35 -  Univalent   :: "('a * 'b)set => bool"
1.36 +  Univalent :: "('a * 'b)set => bool"
1.37      "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
1.38
1.39 +syntax
1.40 +  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
1.41 +
1.42 +translations
1.43 +  "reflexive" == "refl UNIV"
1.44 +
1.45  end
```