Theory "quotient_sum"

Parents quotient

Signature

Constant	Type
+++	:(α -> α -> bool) -> (β -> β -> bool) -> α + β -> α + β -> bool

Theorems

SUM_REL_ind

⊢ ∀P.
      (∀R1 R2 a1 a2. P R1 R2 (INL a1) (INL a2)) ∧
      (∀R1 R2 b1 b2. P R1 R2 (INR b1) (INR b2)) ∧
      (∀R1 R2 a1 b2. P R1 R2 (INL a1) (INR b2)) ∧
      (∀R1 R2 b1 a2. P R1 R2 (INR b1) (INL a2)) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

SUM_REL_EQ

⊢ $= +++ $= = $=

SUM_REL_def

⊢ ((R1 +++ R2) (INL a1) (INL a2) ⇔ R1 a1 a2) ∧
  ((R1 +++ R2) (INR b1) (INR b2) ⇔ R2 b1 b2) ∧
  ((R1 +++ R2) (INL a1) (INR b2) ⇔ F) ∧ ((R1 +++ R2) (INR b1) (INL a2) ⇔ F)

SUM_QUOTIENT

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          QUOTIENT (R1 +++ R2) (SUM_MAP abs1 abs2) (SUM_MAP rep1 rep2)

SUM_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) (SUM_MAP f1 g1)
                        (SUM_MAP f2 g2)

SUM_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.
                      SUM_MAP f g =
                      (SUM_MAP rep1 rep3 --> SUM_MAP abs2 abs4)
                        (SUM_MAP ((abs1 --> rep2) f) ((abs3 --> rep4) g))

SUM_EQUIV

⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV (R1 +++ R2)

ISR_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀a1 a2. (R1 +++ R2) a1 a2 ⇒ (ISR a1 ⇔ ISR a2)

ISR_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀a. ISR a ⇔ ISR (SUM_MAP rep1 rep2 a)

ISL_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀a1 a2. (R1 +++ R2) a1 a2 ⇒ (ISL a1 ⇔ ISL a2)

ISL_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀a. ISL a ⇔ ISL (SUM_MAP rep1 rep2 a)

INR_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀b1 b2. R2 b1 b2 ⇒ (R1 +++ R2) (INR b1) (INR b2)

INR_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀b. INR b = SUM_MAP abs1 abs2 (INR (rep2 b))

INL_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀a1 a2. R1 a1 a2 ⇒ (R1 +++ R2) (INL a1) (INL a2)

INL_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒ ∀a. INL a = SUM_MAP abs1 abs2 (INL (rep1 a))