Theory "quotient_pair"

Signature

Definitions

PAIR_REL

|- !R1 R2. R1 ### R2 = (\(a,b) (c,d). R1 a c /\ R2 b d)

Theorems

PAIR_MAP_I

|- I ## I = I

PAIR_REL_THM

|- !R1 R2 a b c d. (R1 ### R2) (a,b) (c,d) = R1 a c /\ R2 b d

PAIR_REL_EQ

|- $= ### $= = $=

PAIR_REL_REFL

|- !R1 R2.
     (!x y. R1 x y = (R1 x = R1 y)) /\ (!x y. R2 x y = (R2 x = R2 y)) ==>
     !x. (R1 ### R2) x x

PAIR_EQUIV

|- !R1 R2. EQUIV R1 ==> EQUIV R2 ==> EQUIV (R1 ### R2)

PAIR_QUOTIENT

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       QUOTIENT (R1 ### R2) (abs1 ## abs2) (rep1 ## rep2)

FST_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==> !p. FST p = abs1 (FST ((rep1 ## rep2) p))

FST_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !p1 p2. (R1 ### R2) p1 p2 ==> R1 (FST p1) (FST p2)

SND_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==> !p. SND p = abs2 (SND ((rep1 ## rep2) p))

SND_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !p1 p2. (R1 ### R2) p1 p2 ==> R2 (SND p1) (SND p2)

COMMA_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==> !a b. (a,b) = (abs1 ## abs2) (rep1 a,rep2 b)

COMMA_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !a1 a2 b1 b2. R1 a1 b1 /\ R2 a2 b2 ==> (R1 ### R2) (a1,a2) (b1,b2)

CURRY_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !f a b.
           CURRY f a b =
           abs3 (CURRY (((abs1 ## abs2) --> rep3) f) (rep1 a) (rep2 b))

CURRY_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !f1 f2.
           ((R1 ### R2) ===> R3) f1 f2 ==>
           (R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)

UNCURRY_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !f p.
           UNCURRY f p =
           abs3 (UNCURRY ((abs1 --> abs2 --> rep3) f) ((rep1 ## rep2) p))

UNCURRY_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !f1 f2.
           (R1 ===> R2 ===> R3) f1 f2 ==>
           ((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)

PAIR_MAP_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !R4 abs4 rep4.
           QUOTIENT R4 abs4 rep4 ==>
           !f g.
             f ## g =
             ((rep1 ## rep3) --> (abs2 ## abs4))
               ((abs1 --> rep2) f ## (abs3 --> rep4) g)

PAIR_MAP_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !R3 abs3 rep3.
         QUOTIENT R3 abs3 rep3 ==>
         !R4 abs4 rep4.
           QUOTIENT R4 abs4 rep4 ==>
           !f1 f2 g1 g2.
             (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
             ((R1 ### R3) ===> R2 ### R4) (f1 ## g1) (f2 ## g2)