equal
deleted
inserted
replaced
1 (* Title: ZF/EquivClass.thy |
1 (* Title: ZF/EquivClass.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Equivalence relations in Zermelo-Fraenkel Set Theory |
6 Equivalence relations in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 EquivClass = Rel + Perm + |
9 EquivClass = Rel + Perm + |
10 consts |
10 consts |
11 "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*) |
11 "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*) |
12 congruent :: [i,i=>i]=>o |
12 congruent :: [i,i=>i]=>o |
13 congruent2 :: [i,[i,i]=>i]=>o |
13 congruent2 :: [i,[i,i]=>i]=>o |
14 |
14 |
15 defs |
15 defs |
16 quotient_def "A/r == {r``{x} . x:A}" |
16 quotient_def "A/r == {r``{x} . x:A}" |
17 congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)" |
17 congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)" |