src/HOL/Relation.thy
 changeset 11136 e34e7f6d9b57 parent 10832 e33b47e4246d child 12487 bbd564190c9b
```     1.1 --- a/src/HOL/Relation.thy	Thu Feb 15 16:00:38 2001 +0100
1.2 +++ b/src/HOL/Relation.thy	Thu Feb 15 16:00:40 2001 +0100
1.3 @@ -13,47 +13,50 @@
1.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
1.5
1.6  constdefs
1.7 -  comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
1.8 +  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
1.9      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
1.10
1.11 -  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
1.12 +  Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
1.13      "r `` s == {y. ? x:s. (x,y):r}"
1.14
1.15 -  Id    :: "('a * 'a)set"                            (*the identity relation*)
1.16 +  Id    :: "('a * 'a) set"                            (*the identity relation*)
1.17      "Id == {p. ? x. p = (x,x)}"
1.18
1.19 -  diag  :: "'a set => ('a * 'a)set"          (*diagonal: identity over a set*)
1.20 +  diag  :: "'a set => ('a * 'a) set"          (*diagonal: identity over a set*)
1.21      "diag(A) == UN x:A. {(x,x)}"
1.22
1.23 -  Domain :: "('a*'b) set => 'a set"
1.24 +  Domain :: "('a * 'b) set => 'a set"
1.25      "Domain(r) == {x. ? y. (x,y):r}"
1.26
1.27 -  Range  :: "('a*'b) set => 'b set"
1.28 +  Range  :: "('a * 'b) set => 'b set"
1.29      "Range(r) == Domain(r^-1)"
1.30
1.31 -  Field :: "('a*'a)set=>'a set"
1.32 +  Field :: "('a * 'a) set => 'a set"
1.33      "Field r == Domain r Un Range r"
1.34
1.35 -  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
1.36 +  refl   :: "['a set, ('a * 'a) set] => bool" (*reflexivity over a set*)
1.37      "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
1.38
1.39 -  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
1.40 +  sym    :: "('a * 'a) set => bool"             (*symmetry predicate*)
1.41      "sym(r) == ALL x y. (x,y): r --> (y,x): r"
1.42
1.43 -  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
1.44 +  antisym:: "('a * 'a) set => bool"          (*antisymmetry predicate*)
1.45      "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
1.46
1.47 -  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
1.48 +  trans  :: "('a * 'a) set => bool"          (*transitivity predicate*)
1.49      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.50
1.51 -  single_valued :: "('a * 'b)set => bool"
1.52 +  single_valued :: "('a * 'b) set => bool"
1.53      "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
1.54
1.55    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
1.56      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
1.57
1.58 +  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
1.59 +    "inv_image r f == {(x,y). (f(x), f(y)) : r}"
1.60 +
1.61  syntax
1.62 -  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
1.63 +  reflexive :: "('a * 'a) set => bool"       (*reflexivity over a type*)
1.64  translations
1.65    "reflexive" == "refl UNIV"
1.66
```