Structure res_quanTheory

signature res_quanTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val IN_BIGINTER_RES_FORALL : thm
    val IN_BIGUNION_RES_EXISTS : thm
    val NOT_RES_EXISTS : thm
    val NOT_RES_FORALL : thm
    val RES_ABSTRACT : thm
    val RES_ABSTRACT_EQUAL : thm
    val RES_ABSTRACT_EQUAL_EQ : thm
    val RES_ABSTRACT_IDEMPOT : thm
    val RES_ABSTRACT_UNIV : thm
    val RES_DISJ_EXISTS_DIST : thm
    val RES_EXISTS : thm
    val RES_EXISTS_ALT : thm
    val RES_EXISTS_BIGINTER : thm
    val RES_EXISTS_BIGUNION : thm
    val RES_EXISTS_DIFF : thm
    val RES_EXISTS_DISJ_DIST : thm
    val RES_EXISTS_EMPTY : thm
    val RES_EXISTS_EQUAL : thm
    val RES_EXISTS_F : thm
    val RES_EXISTS_NOT_EMPTY : thm
    val RES_EXISTS_NULL : thm
    val RES_EXISTS_REORDER : thm
    val RES_EXISTS_SUBSET : thm
    val RES_EXISTS_T : thm
    val RES_EXISTS_UNION : thm
    val RES_EXISTS_UNIQUE : thm
    val RES_EXISTS_UNIQUE_ALT : thm
    val RES_EXISTS_UNIQUE_ELIM : thm
    val RES_EXISTS_UNIQUE_EMPTY : thm
    val RES_EXISTS_UNIQUE_EXISTS : thm
    val RES_EXISTS_UNIQUE_F : thm
    val RES_EXISTS_UNIQUE_NOT_EMPTY : thm
    val RES_EXISTS_UNIQUE_NULL : thm
    val RES_EXISTS_UNIQUE_SING : thm
    val RES_EXISTS_UNIQUE_T : thm
    val RES_EXISTS_UNIQUE_UNIV : thm
    val RES_EXISTS_UNIV : thm
    val RES_FORALL : thm
    val RES_FORALL_BIGINTER : thm
    val RES_FORALL_BIGUNION : thm
    val RES_FORALL_CONJ_DIST : thm
    val RES_FORALL_DIFF : thm
    val RES_FORALL_DISJ_DIST : thm
    val RES_FORALL_EMPTY : thm
    val RES_FORALL_F : thm
    val RES_FORALL_FORALL : thm
    val RES_FORALL_NOT_EMPTY : thm
    val RES_FORALL_NULL : thm
    val RES_FORALL_REORDER : thm
    val RES_FORALL_SUBSET : thm
    val RES_FORALL_T : thm
    val RES_FORALL_UNION : thm
    val RES_FORALL_UNIQUE : thm
    val RES_FORALL_UNIV : thm
    val RES_SELECT : thm
    val RES_SELECT_EMPTY : thm
    val RES_SELECT_UNIV : thm
  
  val res_quan_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [pred_set] Parent theory of "res_quan"
   
   [IN_BIGINTER_RES_FORALL]  Theorem
      
      ⊢ ∀x sos. x ∈ BIGINTER sos ⇔ ∀s::sos. x ∈ s
   
   [IN_BIGUNION_RES_EXISTS]  Theorem
      
      ⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s::sos. x ∈ s
   
   [NOT_RES_EXISTS]  Theorem
      
      ⊢ ∀P s. ¬(∃x::s. P x) ⇔ ∀x::s. ¬P x
   
   [NOT_RES_FORALL]  Theorem
      
      ⊢ ∀P s. ¬(∀x::s. P x) ⇔ ∃x::s. ¬P x
   
   [RES_ABSTRACT]  Theorem
      
      ⊢ ∀p m x. x ∈ p ⇒ RES_ABSTRACT p m x = m x
   
   [RES_ABSTRACT_EQUAL]  Theorem
      
      ⊢ ∀p m1 m2.
            (∀x. x ∈ p ⇒ m1 x = m2 x) ⇒
            RES_ABSTRACT p m1 = RES_ABSTRACT p m2
   
   [RES_ABSTRACT_EQUAL_EQ]  Theorem
      
      ⊢ ∀p m1 m2.
            RES_ABSTRACT p m1 = RES_ABSTRACT p m2 ⇔ ∀x. x ∈ p ⇒ m1 x = m2 x
   
   [RES_ABSTRACT_IDEMPOT]  Theorem
      
      ⊢ ∀p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m
   
   [RES_ABSTRACT_UNIV]  Theorem
      
      ⊢ ∀m. RES_ABSTRACT 𝕌(:α) m = m
   
   [RES_DISJ_EXISTS_DIST]  Theorem
      
      ⊢ ∀P Q R. (∃i::(λi. P i ∨ Q i). R i) ⇔ (∃i::P. R i) ∨ ∃i::Q. R i
   
   [RES_EXISTS]  Theorem
      
      ⊢ ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x
   
   [RES_EXISTS_ALT]  Theorem
      
      ⊢ ∀p m. RES_EXISTS p m ⇔ RES_SELECT p m ∈ p ∧ m (RES_SELECT p m)
   
   [RES_EXISTS_BIGINTER]  Theorem
      
      ⊢ ∀P sos. (∃x::BIGINTER sos. P x) ⇔ ∃x. (∀s::sos. x ∈ s) ∧ P x
   
   [RES_EXISTS_BIGUNION]  Theorem
      
      ⊢ ∀P sos. (∃x::BIGUNION sos. P x) ⇔ ∃(s::sos) (x::s). P x
   
   [RES_EXISTS_DIFF]  Theorem
      
      ⊢ ∀P s t x. (∃x::s DIFF t. P x) ⇔ ∃x::s. x ∉ t ∧ P x
   
   [RES_EXISTS_DISJ_DIST]  Theorem
      
      ⊢ ∀P Q R. (∃i::P. Q i ∨ R i) ⇔ (∃i::P. Q i) ∨ ∃i::P. R i
   
   [RES_EXISTS_EMPTY]  Theorem
      
      ⊢ ∀p. ¬RES_EXISTS ∅ p
   
   [RES_EXISTS_EQUAL]  Theorem
      
      ⊢ ∀P j. (∃i:: $= j. P i) ⇔ P j
   
   [RES_EXISTS_F]  Theorem
      
      ⊢ ∀P s x. ¬∃s::x. F
   
   [RES_EXISTS_NOT_EMPTY]  Theorem
      
      ⊢ ∀P s. RES_EXISTS s P ⇒ s ≠ ∅
   
   [RES_EXISTS_NULL]  Theorem
      
      ⊢ ∀p m. (∃x::p. m) ⇔ p ≠ ∅ ∧ m
   
   [RES_EXISTS_REORDER]  Theorem
      
      ⊢ ∀P Q R. (∃(i::P) (j::Q). R i j) ⇔ ∃(j::Q) (i::P). R i j
   
   [RES_EXISTS_SUBSET]  Theorem
      
      ⊢ ∀P s t. s ⊆ t ⇒ RES_EXISTS s P ⇒ RES_EXISTS t P
   
   [RES_EXISTS_T]  Theorem
      
      ⊢ ∀P s x. (∃x::s. T) ⇔ s ≠ ∅
   
   [RES_EXISTS_UNION]  Theorem
      
      ⊢ ∀P s t. RES_EXISTS (s ∪ t) P ⇔ RES_EXISTS s P ∨ RES_EXISTS t P
   
   [RES_EXISTS_UNIQUE]  Theorem
      
      ⊢ ∀P f.
            RES_EXISTS_UNIQUE P f ⇔
            (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ x = y
   
   [RES_EXISTS_UNIQUE_ALT]  Theorem
      
      ⊢ ∀p m. RES_EXISTS_UNIQUE p m ⇔ ∃x::p. m x ∧ ∀y::p. m y ⇒ y = x
   
   [RES_EXISTS_UNIQUE_ELIM]  Theorem
      
      ⊢ ∀P s. (∃!x::s. P x) ⇔ ∃!x. x ∈ s ∧ P x
   
   [RES_EXISTS_UNIQUE_EMPTY]  Theorem
      
      ⊢ ∀p. ¬RES_EXISTS_UNIQUE ∅ p
   
   [RES_EXISTS_UNIQUE_EXISTS]  Theorem
      
      ⊢ ∀P s. RES_EXISTS_UNIQUE P s ⇒ RES_EXISTS P s
   
   [RES_EXISTS_UNIQUE_F]  Theorem
      
      ⊢ ∀P s x. ¬∃!x::s. F
   
   [RES_EXISTS_UNIQUE_NOT_EMPTY]  Theorem
      
      ⊢ ∀P s. RES_EXISTS_UNIQUE s P ⇒ s ≠ ∅
   
   [RES_EXISTS_UNIQUE_NULL]  Theorem
      
      ⊢ ∀p m. (∃!x::p. m) ⇔ (∃x. p = {x}) ∧ m
   
   [RES_EXISTS_UNIQUE_SING]  Theorem
      
      ⊢ ∀P s x. (∃!x::s. T) ⇔ ∃y. s = {y}
   
   [RES_EXISTS_UNIQUE_T]  Theorem
      
      ⊢ ∀P s x. (∃!x::s. T) ⇔ ∃!x. x ∈ s
   
   [RES_EXISTS_UNIQUE_UNIV]  Theorem
      
      ⊢ ∀p. RES_EXISTS_UNIQUE 𝕌(:α) p ⇔ $?! p
   
   [RES_EXISTS_UNIV]  Theorem
      
      ⊢ ∀p. RES_EXISTS 𝕌(:α) p ⇔ $? p
   
   [RES_FORALL]  Theorem
      
      ⊢ ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x
   
   [RES_FORALL_BIGINTER]  Theorem
      
      ⊢ ∀P sos. (∀x::BIGINTER sos. P x) ⇔ ∀x. (∀s::sos. x ∈ s) ⇒ P x
   
   [RES_FORALL_BIGUNION]  Theorem
      
      ⊢ ∀P sos. (∀x::BIGUNION sos. P x) ⇔ ∀(s::sos) (x::s). P x
   
   [RES_FORALL_CONJ_DIST]  Theorem
      
      ⊢ ∀P Q R. (∀i::P. Q i ∧ R i) ⇔ (∀i::P. Q i) ∧ ∀i::P. R i
   
   [RES_FORALL_DIFF]  Theorem
      
      ⊢ ∀P s t x. (∀x::s DIFF t. P x) ⇔ ∀x::s. x ∉ t ⇒ P x
   
   [RES_FORALL_DISJ_DIST]  Theorem
      
      ⊢ ∀P Q R. (∀i::(λj. P j ∨ Q j). R i) ⇔ (∀i::P. R i) ∧ ∀i::Q. R i
   
   [RES_FORALL_EMPTY]  Theorem
      
      ⊢ ∀p. RES_FORALL ∅ p
   
   [RES_FORALL_F]  Theorem
      
      ⊢ ∀P s x. (∀x::s. F) ⇔ s = ∅
   
   [RES_FORALL_FORALL]  Theorem
      
      ⊢ ∀P R x. (∀x (i::P). R i x) ⇔ ∀(i::P) x. R i x
   
   [RES_FORALL_NOT_EMPTY]  Theorem
      
      ⊢ ∀P s. ¬RES_FORALL s P ⇒ s ≠ ∅
   
   [RES_FORALL_NULL]  Theorem
      
      ⊢ ∀p m. (∀x::p. m) ⇔ p = ∅ ∨ m
   
   [RES_FORALL_REORDER]  Theorem
      
      ⊢ ∀P Q R. (∀(i::P) (j::Q). R i j) ⇔ ∀(j::Q) (i::P). R i j
   
   [RES_FORALL_SUBSET]  Theorem
      
      ⊢ ∀P s t. s ⊆ t ⇒ RES_FORALL t P ⇒ RES_FORALL s P
   
   [RES_FORALL_T]  Theorem
      
      ⊢ ∀P s x (x::s). T
   
   [RES_FORALL_UNION]  Theorem
      
      ⊢ ∀P s t. RES_FORALL (s ∪ t) P ⇔ RES_FORALL s P ∧ RES_FORALL t P
   
   [RES_FORALL_UNIQUE]  Theorem
      
      ⊢ ∀P j. (∀i:: $= j. P i) ⇔ P j
   
   [RES_FORALL_UNIV]  Theorem
      
      ⊢ ∀p. RES_FORALL 𝕌(:α) p ⇔ $! p
   
   [RES_SELECT]  Theorem
      
      ⊢ ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x
   
   [RES_SELECT_EMPTY]  Theorem
      
      ⊢ ∀p. RES_SELECT ∅ p = @x. F
   
   [RES_SELECT_UNIV]  Theorem
      
      ⊢ ∀p. RES_SELECT 𝕌(:α) p = $@ p
   
   
*)
end

HOL 4, Kananaskis-13