Theory "quotient_pair"

Parents     quotient

Signature

Constant Type
### :(α -> γ -> bool) -> (β -> δ -> bool) -> α # β -> γ # δ -> bool

Definitions

PAIR_REL
⊢ ∀R1 R2. $### R1 R2 = (λ(a,b) (c,d). R1 a c ∧ R2 b d)


Theorems

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)
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)
PAIR_EQUIV
⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV ($### R1 R2)
PAIR_MAP_I
⊢ I ## I = I
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)
PAIR_QUOTIENT
⊢ ∀R1 abs1 rep1.
    QUOTIENT R1 abs1 rep1 ⇒
    ∀R2 abs2 rep2.
      QUOTIENT R2 abs2 rep2 ⇒
      QUOTIENT ($### R1 R2) (abs1 ## abs2) (rep1 ## rep2)
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_REL_THM
⊢ ∀R1 R2 a b c d. $### R1 R2 (a,b) (c,d) ⇔ R1 a c ∧ R2 b d
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)
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. fᴾ p = abs3 (((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) f1ᴾ f2ᴾ