src/HOL/Integ/Equiv.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2215 ebf910e7ec87
child 3373 b19b1456cc78
permissions -rw-r--r--
added AxClasses test;
clasohm@1476
     1
(*  Title:      Equiv.thy
clasohm@925
     2
    ID:         $Id$
paulson@2215
     3
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2215
     4
    Copyright   1996  University of Cambridge
clasohm@925
     5
clasohm@925
     6
Equivalence relations in Higher-Order Set Theory 
clasohm@925
     7
*)
clasohm@925
     8
clasohm@925
     9
Equiv = Relation +
clasohm@925
    10
consts
clasohm@1476
    11
    refl,equiv  ::      "['a set,('a*'a) set]=>bool"
clasohm@925
    12
    sym         ::      "('a*'a) set=>bool"
clasohm@925
    13
    "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
clasohm@925
    14
                        (*set of equiv classes*)
clasohm@1476
    15
    congruent   ::      "[('a*'a) set,'a=>'b]=>bool"
clasohm@925
    16
    congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
clasohm@925
    17
clasohm@925
    18
defs
paulson@1642
    19
    refl_def      "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
clasohm@972
    20
    sym_def       "sym(r)    == ALL x y. (x,y): r --> (y,x): r"
clasohm@925
    21
    equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
clasohm@925
    22
    quotient_def  "A/r == UN x:A. {r^^{x}}"  
clasohm@972
    23
    congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
clasohm@1151
    24
    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. 
clasohm@1151
    25
           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
clasohm@925
    26
end