author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1478  2b8c2a7547ab 
permissions  rwrr 
1478  1 
(* Title: ZF/EquivClass.thy 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

5 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

6 
Equivalence relations in ZermeloFraenkel Set Theory 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

7 
*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

8 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

9 
EquivClass = Rel + Perm + 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

10 
consts 
1401  11 
"'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*) 
1478  12 
congruent :: [i,i=>i]=>o 
1401  13 
congruent2 :: [i,[i,i]=>i]=>o 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

14 

753  15 
defs 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

16 
quotient_def "A/r == {r``{x} . x:A}" 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

17 
congruent_def "congruent(r,b) == ALL y z. <y,z>:r > b(y)=b(z)" 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

18 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

19 
congruent2_def 
1155  20 
"congruent2(r,b) == ALL y1 z1 y2 z2. 
21 
<y1,z1>:r > <y2,z2>:r > b(y1,y2) = b(z1,z2)" 

535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

22 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

23 
end 