src/ZF/EquivClass.thy
author clasohm
Sat, 09 Dec 1995 13:36:11 +0100
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 Zermelo-Fraenkel 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
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    11
    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    12
    congruent	::	[i,i=>i]=>o
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    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
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 535
diff changeset
    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
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    20
       "congruent2(r,b) == ALL y1 z1 y2 z2. 
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    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