Theory "quotient_pred_set"

Signature

Definitions

DELETER_def

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

DISJOINTR_def

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

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

GSPECR_def

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

IMAGER_def

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

INSERTR_def

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

PSUBSETR_def

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

SUBSETR_def

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

Theorems

ABSORPTIONR

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

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))

DIFF_PRS

⊢ ∀R abs rep.
    QUOTIENT R abs rep ⇒
    ∀s t. s DIFF t = (rep ⟶ I) ((abs ⟶ I) s DIFF (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)

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)

EMPTY_PRS

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

EMPTY_RSP

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

FINITER_EMPTY

⊢ ∀R. FINITER R ∅

FINITER_EQ

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

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_INSERTR

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

FINITER_RSP

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

FINITE_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀s. FINITE s ⇔ FINITER R ((abs ⟶ 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))

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))

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))

INTER_PRS

⊢ ∀R abs rep.
    QUOTIENT R abs rep ⇒ ∀s t. s ∩ t = (rep ⟶ I) ((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)

IN_DELETER

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

IN_GSPECR

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

IN_IMAGER

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

IN_INSERTR

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

IN_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x s. x ∈ s ⇔ rep x ∈ (abs ⟶ I) 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_SET_MAP

⊢ ∀f s x. x ∈ (f ⟶ I) s ⇔ f x ∈ s

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)

SET_REL

⊢ ∀R s t. (R ===> $<=>) s t ⇔ ∀x y. R x y ⇒ (x ∈ s ⇔ y ∈ 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)

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)

UNION_PRS

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

UNION_RSP

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

UNIV_PRS

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

UNIV_RSP

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