Structure quotient_pred_setTheory

signature quotient_pred_setTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val DELETER_def : thm
    val DISJOINTR_def : thm
    val FINITER_def : thm
    val GSPECR_def : thm
    val IMAGER_def : thm
    val INSERTR_def : thm
    val PSUBSETR_def : thm
    val SUBSETR_def : thm

  (*  Theorems  *)
    val ABSORPTIONR : thm
    val DELETER_RSP : thm
    val DELETE_PRS : thm
    val DIFF_PRS : thm
    val DIFF_RSP : thm
    val DISJOINTR_RSP : thm
    val DISJOINT_PRS : thm
    val EMPTY_PRS : thm
    val EMPTY_RSP : thm
    val FINITER_EMPTY : thm
    val FINITER_EQ : thm
    val FINITER_INDUCT : thm
    val FINITER_INSERTR : thm
    val FINITER_RSP : thm
    val FINITE_PRS : thm
    val GSPECR_RSP : thm
    val GSPEC_PRS : thm
    val IMAGER_RSP : thm
    val IMAGE_PRS : thm
    val INSERTR_RSP : thm
    val INSERT_PRS : thm
    val INTER_PRS : thm
    val INTER_RSP : thm
    val IN_DELETER : thm
    val IN_GSPECR : thm
    val IN_IMAGER : thm
    val IN_INSERTR : thm
    val IN_PRS : thm
    val IN_RSP : thm
    val IN_SET_MAP : thm
    val PSUBSETR_RSP : thm
    val PSUBSET_PRS : thm
    val SET_REL : thm
    val SET_REL_MP : thm
    val SUBSETR_RSP : thm
    val SUBSET_PRS : thm
    val UNION_PRS : thm
    val UNION_RSP : thm
    val UNIV_PRS : thm
    val UNIV_RSP : thm

  val quotient_pred_set_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [quotient_pair] Parent theory of "quotient_pred_set"

   [DELETER_def]  Definition

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

   [DISJOINTR_def]  Definition

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

   [FINITER_def]  Definition

      |- ∀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]  Definition

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

   [IMAGER_def]  Definition

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

   [INSERTR_def]  Definition

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

   [PSUBSETR_def]  Definition

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

   [SUBSETR_def]  Definition

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

   [ABSORPTIONR]  Theorem

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

   [DELETER_RSP]  Theorem

      |- ∀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]  Theorem

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

   [DIFF_PRS]  Theorem

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

   [DIFF_RSP]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

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

   [EMPTY_PRS]  Theorem

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

   [EMPTY_RSP]  Theorem

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

   [FINITER_EMPTY]  Theorem

      |- ∀R. FINITER R ∅

   [FINITER_EQ]  Theorem

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

   [FINITER_INDUCT]  Theorem

      |- ∀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]  Theorem

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

   [FINITER_RSP]  Theorem

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

   [FINITE_PRS]  Theorem

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

   [GSPECR_RSP]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

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

   [INTER_PRS]  Theorem

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

   [INTER_RSP]  Theorem

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

   [IN_DELETER]  Theorem

      |- ∀R s x y. y ∈ DELETER R s x ⇔ y ∈ s ∧ ¬R x y

   [IN_GSPECR]  Theorem

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

   [IN_IMAGER]  Theorem

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

   [IN_INSERTR]  Theorem

      |- ∀R x s y. y ∈ INSERTR R x s ⇔ R y x ∨ y ∈ s

   [IN_PRS]  Theorem

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

   [IN_RSP]  Theorem

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

   [IN_SET_MAP]  Theorem

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

   [PSUBSETR_RSP]  Theorem

      |- ∀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]  Theorem

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

   [SET_REL]  Theorem

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

   [SET_REL_MP]  Theorem

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

   [SUBSETR_RSP]  Theorem

      |- ∀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]  Theorem

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

   [UNION_PRS]  Theorem

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

   [UNION_RSP]  Theorem

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

   [UNIV_PRS]  Theorem

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

   [UNIV_RSP]  Theorem

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


*)
end

HOL 4, Kananaskis-10