6 Equivalence relations in Higher-Order Set Theory |
6 Equivalence relations in Higher-Order Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Equiv = Relation + Finite + |
9 Equiv = Relation + Finite + |
10 consts |
10 consts |
11 refl,equiv :: "['a set,('a*'a) set]=>bool" |
11 equiv :: "['a set, ('a*'a) set] => bool" |
12 sym :: "('a*'a) set=>bool" |
12 quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/" 90) |
13 "'/" :: "['a set,('a*'a) set]=>'a set set" (infixl 90) |
13 (*set of equiv classes*) |
14 (*set of equiv classes*) |
14 congruent :: "[('a*'a) set, 'a=>'b] => bool" |
15 congruent :: "[('a*'a) set,'a=>'b]=>bool" |
15 congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool" |
16 congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool" |
|
17 |
16 |
18 defs |
17 defs |
19 refl_def "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)" |
|
20 sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
|
21 equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
18 equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
22 quotient_def "A/r == UN x:A. {r^^{x}}" |
19 quotient_def "A/r == UN x:A. {r^^{x}}" |
23 congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
20 congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
24 congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. |
21 congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. |
25 (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |
22 (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |