Theory "quotient_list"

Theorems

SOME_EL_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l1 l2 P1 P2.
          $===> R $<=> P1 P2 ∧ LIST_REL R l1 l2 ⇒
          (EXISTS P1 l1 ⇔ EXISTS P2 l2)

SOME_EL_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l P. EXISTS P l ⇔ EXISTS ((abs --> I) P) (MAP rep l)

REVERSE_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l1 l2. LIST_REL R l1 l2 ⇒ LIST_REL R (REVERSE l1) (REVERSE l2)

REVERSE_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l. REVERSE l = MAP abs (REVERSE (MAP rep l))

NULL_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l1 l2. LIST_REL R l1 l2 ⇒ (NULL l1 ⇔ NULL l2)

NULL_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀l. NULL l ⇔ NULL (MAP rep l)

NIL_RSP

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ LIST_REL R [] []

NIL_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ([] = MAP abs [])

MAP_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l1 l2 f1 f2.
              $===> R1 R2 f1 f2 ∧ LIST_REL R1 l1 l2 ⇒
              LIST_REL R2 (MAP f1 l1) (MAP f2 l2)

MAP_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l f. MAP f l = MAP abs2 (MAP ((abs1 --> rep2) f) (MAP rep1 l))

LIST_REL_REL

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀r s.
          LIST_REL R r s ⇔
          LIST_REL R r r ∧ LIST_REL R s s ∧ (MAP abs r = MAP abs s)

LIST_REL_REFL

⊢ ∀R. (∀x y. R x y ⇔ (R x = R y)) ⇒ ∀x. LIST_REL R x x

LIST_REL_EQ

⊢ LIST_REL $= = $=

LIST_QUOTIENT

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ QUOTIENT (LIST_REL R) (MAP abs) (MAP rep)

LIST_MAP_I

⊢ MAP I = I

LIST_EQUIV

⊢ ∀R. EQUIV R ⇒ EQUIV (LIST_REL R)

LENGTH_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l1 l2. LIST_REL R l1 l2 ⇒ (LENGTH l1 = LENGTH l2)

LENGTH_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀l. LENGTH l = LENGTH (MAP rep l)

FOLDR_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l1 l2 f1 f2 e1 e2.
              $===> R1 ($===> R2 R2) f1 f2 ∧ R2 e1 e2 ∧ LIST_REL R1 l1 l2 ⇒
              R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)

FOLDR_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l f e.
              FOLDR f e l =
              abs2 (FOLDR ((abs1 --> abs2 --> rep2) f) (rep2 e) (MAP rep1 l))

FOLDL_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l1 l2 f1 f2 e1 e2.
              $===> R1 ($===> R2 R1) f1 f2 ∧ R1 e1 e2 ∧ LIST_REL R2 l1 l2 ⇒
              R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)

FOLDL_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀l f e.
              FOLDL f e l =
              abs1 (FOLDL ((abs1 --> abs2 --> rep1) f) (rep1 e) (MAP rep2 l))

FLAT_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l1 l2. LIST_REL (LIST_REL R) l1 l2 ⇒ LIST_REL R (FLAT l1) (FLAT l2)

FLAT_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))

FILTER_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀P1 P2 l1 l2.
          $===> R $<=> P1 P2 ∧ LIST_REL R l1 l2 ⇒
          LIST_REL R (FILTER P1 l1) (FILTER P2 l2)

FILTER_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀P l. FILTER P l = MAP abs (FILTER ((abs --> I) P) (MAP rep l))

CONS_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀t1 t2 h1 h2. R h1 h2 ∧ LIST_REL R t1 t2 ⇒ LIST_REL R (h1::t1) (h2::t2)

CONS_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀t h. h::t = MAP abs (rep h::MAP rep t)

APPEND_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l1 l2 m1 m2.
          LIST_REL R l1 l2 ∧ LIST_REL R m1 m2 ⇒
          LIST_REL R (l1 ++ m1) (l2 ++ m2)

APPEND_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l m. l ++ m = MAP abs (MAP rep l ++ MAP rep m)

ALL_EL_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀l1 l2 P1 P2.
          $===> R $<=> P1 P2 ∧ LIST_REL R l1 l2 ⇒ (EVERY P1 l1 ⇔ EVERY P2 l2)

ALL_EL_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀l P. EVERY P l ⇔ EVERY ((abs --> I) P) (MAP rep l)