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