author  clasohm 
Thu, 22 Jun 1995 17:13:05 +0200  
changeset 1155  928a16e02f9f 
parent 753  ec86863e87c8 
child 1401  0c439768f45c 
permissions  rwrr 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

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

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

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
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 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

11 
"'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

12 
congruent :: "[i,i=>i]=>o" 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

13 
congruent2 :: "[i,[i,i]=>i]=>o" 
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 