equal
deleted
inserted
replaced
1 (* Title: ZF/Rel.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Relations in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 Rel = equalities + |
|
10 consts |
|
11 refl :: "[i,i]=>o" |
|
12 irrefl :: "[i,i]=>o" |
|
13 equiv :: "[i,i]=>o" |
|
14 sym :: "i=>o" |
|
15 asym :: "i=>o" |
|
16 antisym :: "i=>o" |
|
17 trans :: "i=>o" |
|
18 trans_on :: "[i,i]=>o" ("trans[_]'(_')") |
|
19 |
|
20 defs |
|
21 refl_def "refl(A,r) == (ALL x: A. <x,x> : r)" |
|
22 |
|
23 irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r" |
|
24 |
|
25 sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r" |
|
26 |
|
27 asym_def "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r" |
|
28 |
|
29 antisym_def "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y" |
|
30 |
|
31 trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r" |
|
32 |
|
33 trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. |
|
34 <x,y>: r --> <y,z>: r --> <x,z>: r" |
|
35 |
|
36 equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)" |
|
37 |
|
38 end |
|