Theory "quotient_pred_set"

Signature

Definitions

SUBSETR_def

⊢ ∀R s t. SUBSETR R s t ⇔ ∀x::respects R. x ∈ s ⇒ x ∈ t

PSUBSETR_def

⊢ ∀R s t. PSUBSETR R s t ⇔ SUBSETR R s t ∧ ¬$===> R $<=> s t

INSERTR_def

⊢ ∀R x s. INSERTR R x s = {y | R y x ∨ y ∈ s}

IMAGER_def

⊢ ∀R1 R2 f s. IMAGER R1 R2 f s = {y | ∃x::respects R1. R2 y (f x) ∧ x ∈ s}

GSPECR_def

⊢ ∀R1 R2 f v. GSPECR R1 R2 f v ⇔ ∃x::respects R1. $### R2 $<=> (v,T) (f x)

FINITER_def

⊢ ∀R s.
      FINITER R s ⇔
      ∀P::respects ($===> ($===> R $<=>) $<=>).
        P ∅ ∧
        (∀s::respects ($===> R $<=>). P s ⇒ ∀e::respects R. P (INSERTR R e s)) ⇒
        P s

DISJOINTR_def

⊢ ∀R s t. DISJOINTR R s t ⇔ ¬∃x::respects R. x ∈ s ∧ x ∈ t

DELETER_def

⊢ ∀R s x. DELETER R s x = {y | y ∈ s ∧ ¬R x y}

Theorems

UNIV_RSP

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ $===> R $<=> 𝕌(:α) 𝕌(:α)

UNIV_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ (𝕌(:β) = (rep --> I) 𝕌(:α))

UNION_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          $===> R $<=> (s1 ∪ t1) (s2 ∪ t2)

UNION_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. s ∪ t = (rep --> I) ((abs --> I) s ∪ (abs --> I) t)

SUBSETR_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          (SUBSETR R s1 t1 ⇔ SUBSETR R s2 t2)

SUBSET_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. s ⊆ t ⇔ SUBSETR R ((abs --> I) s) ((abs --> I) t)

SET_REL_MP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t x y. $===> R $<=> s t ∧ R x y ⇒ (x ∈ s ⇔ y ∈ t)

SET_REL

⊢ ∀R s t. $===> R $<=> s t ⇔ ∀x y. R x y ⇒ (x ∈ s ⇔ y ∈ t)

PSUBSETR_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          (PSUBSETR R s1 t1 ⇔ PSUBSETR R s2 t2)

PSUBSET_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. s ⊂ t ⇔ PSUBSETR R ((abs --> I) s) ((abs --> I) t)

INTER_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          $===> R $<=> (s1 ∩ t1) (s2 ∩ t2)

INTER_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. s ∩ t = (rep --> I) ((abs --> I) s ∩ (abs --> I) t)

INSERTR_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀x1 x2 s1 s2.
          R x1 x2 ∧ $===> R $<=> s1 s2 ⇒
          $===> R $<=> (INSERTR R x1 s1) (INSERTR R x2 s2)

INSERT_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s x. x INSERT s = (rep --> I) (INSERTR R (rep x) ((abs --> I) s))

IN_SET_MAP

⊢ ∀f s x. x ∈ (f --> I) s ⇔ f x ∈ s

IN_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀x1 x2 s1 s2. R x1 x2 ∧ $===> R $<=> s1 s2 ⇒ (x1 ∈ s1 ⇔ x2 ∈ s2)

IN_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x s. x ∈ s ⇔ rep x ∈ (abs --> I) s

IN_INSERTR

⊢ ∀R x s y. y ∈ INSERTR R x s ⇔ R y x ∨ y ∈ s

IN_IMAGER

⊢ ∀R1 R2 y f s. y ∈ IMAGER R1 R2 f s ⇔ ∃x::respects R1. R2 y (f x) ∧ x ∈ s

IN_GSPECR

⊢ ∀R1 R2 f v. v ∈ GSPECR R1 R2 f ⇔ ∃x::respects R1. $### R2 $<=> (v,T) (f x)

IN_DELETER

⊢ ∀R s x y. y ∈ DELETER R s x ⇔ y ∈ s ∧ ¬R x y

IMAGER_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀f1 f2 s1 s2.
              $===> R1 R2 f1 f2 ∧ $===> R1 $<=> s1 s2 ⇒
              $===> R2 $<=> (IMAGER R1 R2 f1 s1) (IMAGER R1 R2 f2 s2)

IMAGE_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀f s.
              IMAGE f s =
              (rep2 --> I) (IMAGER R1 R2 ((abs1 --> rep2) f) ((abs1 --> I) s))

GSPECR_RSP

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀f1 f2.
              $===> R1 ($### R2 $<=>) f1 f2 ⇒
              $===> R2 $<=> (GSPECR R1 R2 f1) (GSPECR R1 R2 f2)

GSPEC_PRS

⊢ ∀R1 abs1 rep1.
      QUOTIENT R1 abs1 rep1 ⇒
      ∀R2 abs2 rep2.
          QUOTIENT R2 abs2 rep2 ⇒
          ∀f. GSPEC f = (rep2 --> I) (GSPECR R1 R2 ((abs1 --> (rep2 ## I)) f))

FINITER_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2. $===> R $<=> s1 s2 ⇒ (FINITER R s1 ⇔ FINITER R s2)

FINITER_INSERTR

⊢ ∀R (s::respects ($===> R $<=>)).
      FINITER R s ⇒ ∀x::respects R. FINITER R (INSERTR R x s)

FINITER_INDUCT

⊢ ∀R (P::respects ($===> ($===> R $<=>) $<=>)).
      P ∅ ∧
      (∀s::respects ($===> R $<=>).
         FINITER R s ∧ P s ⇒ ∀e::respects R. e ∉ s ⇒ P (INSERTR R e s)) ⇒
      ∀s::respects ($===> R $<=>). FINITER R s ⇒ P s

FINITER_EQ

⊢ ∀R s1 s2. $===> R $<=> s1 s2 ⇒ (FINITER R s1 ⇔ FINITER R s2)

FINITER_EMPTY

⊢ ∀R. FINITER R ∅

FINITE_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀s. FINITE s ⇔ FINITER R ((abs --> I) s)

EMPTY_RSP

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ $===> R $<=> ∅ ∅

EMPTY_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ (∅ = (rep --> I) ∅)

DISJOINTR_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          (DISJOINTR R s1 t1 ⇔ DISJOINTR R s2 t2)

DISJOINT_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. DISJOINT s t ⇔ DISJOINTR R ((abs --> I) s) ((abs --> I) t)

DIFF_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 t1 t2.
          $===> R $<=> s1 s2 ∧ $===> R $<=> t1 t2 ⇒
          $===> R $<=> (s1 DIFF t1) (s2 DIFF t2)

DIFF_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s t. s DIFF t = (rep --> I) ((abs --> I) s DIFF (abs --> I) t)

DELETER_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s1 s2 x1 x2.
          $===> R $<=> s1 s2 ∧ R x1 x2 ⇒
          $===> R $<=> (DELETER R s1 x1) (DELETER R s2 x2)

DELETE_PRS

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      ∀s x. s DELETE x = (rep --> I) (DELETER R ((abs --> I) s) (rep x))

ABSORPTIONR

⊢ ∀R (x::respects R) (s::respects ($===> R $<=>)).
      x ∈ s ⇔ $===> R $<=> (INSERTR R x s) s