Filtering...

quantify

books/std/osets/quantify
other
(in-package "SET")
other
(include-book "top")
other
(set-verify-guards-eagerness 2)
other
(local (in-theory (enable expensive-rules definitions)))
other
(defconst *positive-functions*
  '((defun all-list
     (x)
     (declare (xargs :guard (true-listp x)
         :verify-guards nil))
     (if (endp x)
       t
       (and (predicate (car x))
         (all-list (cdr x))))) (defun exists-list
      (x)
      (declare (xargs :guard (true-listp x)
          :verify-guards nil))
      (cond ((endp x) nil)
        ((predicate (car x)) t)
        (t (exists-list (cdr x)))))
    (defun find-list
      (x)
      (declare (xargs :guard (true-listp x)
          :verify-guards nil))
      (cond ((endp x) nil)
        ((predicate (car x)) (car x))
        (t (find-list (cdr x)))))
    (defun filter-list
      (x)
      (declare (xargs :guard (true-listp x)
          :verify-guards nil))
      (cond ((endp x) nil)
        ((predicate (car x)) (cons (car x) (filter-list (cdr x))))
        (t (filter-list (cdr x)))))
    (defun all
      (set-for-all-reduction)
      (declare (xargs :guard (setp set-for-all-reduction)
          :verify-guards nil))
      (if (emptyp set-for-all-reduction)
        t
        (and (predicate (head set-for-all-reduction))
          (all (tail set-for-all-reduction)))))
    (defun exists
      (x)
      (declare (xargs :guard (setp x) :verify-guards nil))
      (cond ((emptyp x) nil)
        ((predicate (head x)) t)
        (t (exists (tail x)))))
    (defun find
      (x)
      (declare (xargs :guard (setp x) :verify-guards nil))
      (cond ((emptyp x) nil)
        ((predicate (head x)) (head x))
        (t (find (tail x)))))
    (defun filter
      (x)
      (declare (xargs :guard (setp x) :verify-guards nil))
      (cond ((emptyp x) (sfix x))
        ((predicate (head x)) (insert (head x)
            (filter (tail x))))
        (t (filter (tail x)))))))
other
(defconst *negative-functions*
  (instance-defuns *positive-functions*
    '(((predicate ?x) (not (predicate ?x))) ((all ?x) (all<not> ?x))
      ((exists ?x) (exists<not> ?x))
      ((find ?x) (find<not> ?x))
      ((filter ?x) (filter<not> ?x))
      ((all-list ?x) (all-list<not> ?x))
      ((exists-list ?x) (exists-list<not> ?x))
      ((find-list ?x) (find-list<not> ?x))
      ((filter-list ?x) (filter-list<not> ?x)))))
other
(defconst *functions*
  (append *positive-functions* *negative-functions*))
other
(instance *functions*)
other
(instance-*functions*)
other
(defconst *positive-theorems*
  '((defthm all-list-type
     (or (equal (all-list x) t)
       (equal (all-list x) nil))
     :rule-classes :type-prescription) (defthm all-list-cdr
      (implies (all-list x)
        (all-list (cdr x))))
    (defthm all-list-endp
      (implies (endp x) (all-list x)))
    (defthm all-list-member
      (implies (and (all-list x) (member a x))
        (predicate a)))
    (defthm all-list-in-2
      (implies (and (all-list x) (not (predicate a)))
        (not (member a x))))
    (defthm all-list-cons
      (equal (all-list (cons a x))
        (and (predicate a) (all-list x))))
    (defthm all-list-append
      (equal (all-list (append x y))
        (and (all-list x) (all-list y))))
    (defthm all-list-nth
      (implies (and (all-list x)
          (<= 0 n)
          (< n (len x)))
        (predicate (nth n x))))
    (encapsulate nil
      (local (defthm lemma1
          (implies (and (all-list acc) (all-list x))
            (all-list (revappend x acc)))))
      (local (defthm lemma2
          (implies (not (all-list acc))
            (not (all-list (revappend x acc))))))
      (local (defthm lemma3
          (implies (and (all-list acc) (not (all-list x)))
            (not (all-list (revappend x acc))))))
      (defthm all-list-revappend
        (equal (all-list (revappend x acc))
          (and (all-list x) (all-list acc)))))
    (defthm all-list-reverse
      (equal (all-list (reverse x))
        (all-list x)))
    (defthm exists-list-elimination
      (equal (exists-list x)
        (not (all-list<not> x))))
    (defthm filter-list-true-list
      (true-listp (filter-list x))
      :rule-classes :type-prescription)
    (defthm filter-list-membership
      (iff (member a (filter-list x))
        (and (predicate a) (member a x))))
    (defthm filter-list-all-list
      (all-list (filter-list x)))
    (defthm all-type
      (or (equal (all x) t)
        (equal (all x) nil))
      :rule-classes :type-prescription)
    (defthm all-sfix
      (equal (all (sfix x)) (all x)))
    (defthm all-tail
      (implies (all x)
        (all (tail x))))
    (defthm all-emptyp
      (implies (emptyp x) (all x)))
    (defthm all-in
      (implies (and (all x) (in a x))
        (predicate a)))
    (defthm all-in-2
      (implies (and (all x) (not (predicate a)))
        (not (in a x))))
    (defthm all-insert
      (equal (all (insert a x))
        (and (predicate a) (all x)))
      :hints (("Goal" :induct (insert a x))))
    (defthm all-delete
      (implies (all x)
        (all (delete a x))))
    (defthm all-delete-2
      (implies (predicate a)
        (equal (all (delete a x)) (all x))))
    (defthm all-union
      (equal (all (union x y))
        (and (all x) (all y))))
    (defthm all-intersect-x
      (implies (all x)
        (all (intersect x y))))
    (defthm all-intersect-y
      (implies (all x)
        (all (intersect y x))))
    (defthm all-difference
      (implies (all x)
        (all (difference x y))))
    (defthm all-difference-2
      (implies (all y)
        (equal (all (difference x y))
          (all x))))
    (defthm exists-elimination
      (equal (exists x) (not (all<not> x))))
    (defthm find-sfix
      (equal (find (sfix x)) (find x)))
    (defthm find-witness
      (implies (not (all x))
        (and (in (find<not> x) x)
          (not (predicate (find<not> x)))))
      :rule-classes :forward-chaining)
    (defthm filter-set
      (setp (filter x)))
    (defthm filter-sfix
      (equal (filter (sfix x))
        (filter x)))
    (defthm filter-in
      (equal (in a (filter x))
        (and (predicate a) (in a x)))
      :hints (("Goal" :induct (filter x))))
    (defthm filter-subset
      (subset (filter x) x))
    (defthm filter-all
      (all (filter x)))
    (defthm filter-all-2
      (implies (all x)
        (equal (filter x) (sfix x)))
      :hints (("Goal" :in-theory (disable double-containment))))
    (defthm all-mergesort
      (equal (all (mergesort x))
        (all-list x)))
    (defthm all-list-applied-to-set
      (implies (setp x)
        (equal (all-list x) (all x)))
      :hints (("Goal" :in-theory (enable setp
           emptyp
           sfix
           head
           tail))))))
other
(defconst *negative-theorems*
  (instance-rewrite *positive-theorems*
    '(((predicate ?x) (predicate-temp ?x)) ((all ?x) (all-temp ?x))
      ((exists ?x) (exists-temp ?x))
      ((find ?x) (find-temp ?x))
      ((filter ?x) (filter-temp ?x))
      ((all-list ?x) (all-list-temp ?x))
      ((exists-list ?x) (exists-list-temp ?x))
      ((find-list ?x) (find-list-temp ?x))
      ((filter-list ?x) (filter-list-temp ?x))
      ((not (predicate ?x)) (predicate ?x))
      ((all<not> ?x) (all ?x))
      ((exists<not> ?x) (exists ?x))
      ((find<not> ?x) (find ?x))
      ((filter<not> ?x) (filter ?x))
      ((all-list<not> ?x) (all-list ?x))
      ((exists-list<not> ?x) (exists-list ?x))
      ((find-list<not> ?x) (find-list ?x))
      ((filter-list<not> ?x) (filter-list ?x))
      ((predicate-temp ?x) (not (predicate ?x)))
      ((all-temp ?x) (all<not> ?x))
      ((exists-temp ?x) (exists<not> ?x))
      ((find-temp ?x) (find<not> ?x))
      ((filter-temp ?x) (filter<not> ?x))
      ((all-list-temp ?x) (all-list<not> ?x))
      ((exists-list-temp ?x) (exists-list<not> ?x))
      ((find-list-temp ?x) (find-list<not> ?x))
      ((filter-list-temp ?x) (filter-list<not> ?x)))))
other
(defconst *theorems*
  (append *positive-theorems*
    (rename-defthms *negative-theorems*
      '-not)))
other
(instance *theorems*)
other
(instance-*theorems*)
other
(encapsulate (((all-list-hyps) => *) ((all-list-list) => *))
  (local (defun all-list-hyps nil nil))
  (local (defun all-list-list nil nil))
  (defthmd list-membership-constraint
    (implies (all-list-hyps)
      (implies (member arbitrary-element (all-list-list))
        (predicate arbitrary-element)))))
other
(encapsulate nil
  (local (defthm witness-lemma
      (implies (not (all-list x))
        (and (member (find-list<not> x) x)
          (not (predicate (find-list<not> x)))))))
  (defthmd all-list-by-membership
    (implies (all-list-hyps)
      (all-list (all-list-list)))
    :hints (("Goal" :use (:instance list-membership-constraint
         (arbitrary-element (find-list<not> (all-list-list))))))))
other
(defconst *final-theorems*
  '((defthm cardinality-filter
     (equal (cardinality x)
       (+ (cardinality (filter x))
         (cardinality (filter<not> x))))
     :rule-classes :linear) (defthm all-subset
      (implies (and (all y) (subset x y))
        (all x))
      :hints (("Goal" :use (:functional-instance all-by-membership
           (all-hyps (lambda nil
               (and (all y) (subset x y))))
           (all-set (lambda nil x))))))
    (defthm all-subset-not
      (implies (and (all<not> y) (subset x y))
        (all<not> x))
      :hints (("Goal" :use (:functional-instance all-by-membership
           (all-hyps (lambda nil
               (and (all<not> y) (subset x y))))
           (all-set (lambda nil x))
           (predicate (lambda (x) (not (predicate x))))
           (all (lambda (x) (all<not> x)))))))))
other
(instance *final-theorems*)
other
(instance-*final-theorems*)
other
(verify-guards all)
other
(verify-guards all<not>)
other
(verify-guards exists)
other
(verify-guards exists<not>)
other
(verify-guards find)
other
(verify-guards find<not>)
other
(verify-guards filter)
other
(verify-guards filter<not>)
other
(verify-guards all-list)
other
(verify-guards all-list<not>)
other
(verify-guards exists-list)
other
(verify-guards exists-list<not>)
other
(verify-guards find-list)
other
(verify-guards find-list<not>)
other
(verify-guards filter-list)
other
(verify-guards filter-list<not>)
mksymfunction
(defun mksym
  (name sym)
  (declare (xargs :mode :program))
  (intern-in-package-of-symbol (string-upcase name)
    sym))
appfunction
(defun app
  (x y)
  (declare (xargs :mode :program))
  (string-append x y))
?ifyfunction
(defun ?ify
  (args)
  (declare (xargs :mode :program))
  (if (endp args)
    nil
    (cons (mksym (app "?" (symbol-name (car args)))
        (car args))
      (?ify (cdr args)))))
standardize-to-packagefunction
(defun standardize-to-package
  (symbol-name replacement term)
  (declare (xargs :mode :program))
  (if (atom term)
    (if (and (symbolp term)
        (equal (symbol-name term) symbol-name))
      replacement
      term)
    (cons (standardize-to-package symbol-name
        replacement
        (car term))
      (standardize-to-package symbol-name
        replacement
        (cdr term)))))
quantify-simple-predicatefunction
(defun quantify-simple-predicate
  (predicate in-package
    set-guard
    list-guard
    arg-guard
    verify-guards)
  (declare (xargs :guard (symbolp in-package) :mode :program))
  (let* ((name (car predicate)) (args (cons '?x (cddr predicate)))
      (wrap (app "<" (app (symbol-name name) ">")))
      (not-wrap (app "<"
          (app "not-" (app (symbol-name name) ">"))))
      (all<p> (mksym (app "all" wrap) in-package))
      (exists<p> (mksym (app "exists" wrap) in-package))
      (find<p> (mksym (app "find" wrap) in-package))
      (filter<p> (mksym (app "filter" wrap) in-package))
      (all<not-p> (mksym (app "all" not-wrap) in-package))
      (exists<not-p> (mksym (app "exists" not-wrap) in-package))
      (find<not-p> (mksym (app "find" not-wrap) in-package))
      (filter<not-p> (mksym (app "filter" not-wrap) in-package))
      (all-list<p> (mksym (app "all-list" wrap) in-package))
      (exists-list<p> (mksym (app "exists-list" wrap) in-package))
      (find-list<p> (mksym (app "find-list" wrap) in-package))
      (filter-list<p> (mksym (app "filter-list" wrap) in-package))
      (all-list<not-p> (mksym (app "all-list" not-wrap) in-package))
      (exists-list<not-p> (mksym (app "exists-list" not-wrap)
          in-package))
      (find-list<not-p> (mksym (app "find-list" not-wrap) in-package))
      (filter-list<not-p> (mksym (app "filter-list" not-wrap)
          in-package))
      (subs `(((predicate ?x) (,SET::NAME ,@SET::ARGS)) ((all ?x) (,SET::ALL<P> ,@SET::ARGS))
          ((exists ?x) (,SET::EXISTS<P> ,@SET::ARGS))
          ((find ?x) (,SET::FIND<P> ,@SET::ARGS))
          ((filter ?x) (,SET::FILTER<P> ,@SET::ARGS))
          ((all<not> ?x) (,SET::ALL<NOT-P> ,@SET::ARGS))
          ((exists<not> ?x) (,SET::EXISTS<NOT-P> ,@SET::ARGS))
          ((find<not> ?x) (,SET::FIND<NOT-P> ,@SET::ARGS))
          ((filter<not> ?x) (,SET::FILTER<NOT-P> ,@SET::ARGS))
          ((all-list ?x) (,SET::ALL-LIST<P> ,@SET::ARGS))
          ((exists-list ?x) (,SET::EXISTS-LIST<P> ,@SET::ARGS))
          ((find-list ?x) (,SET::FIND-LIST<P> ,@SET::ARGS))
          ((filter-list ?x) (,SET::FILTER-LIST<P> ,@SET::ARGS))
          ((all-list<not> ?x) (,SET::ALL-LIST<NOT-P> ,@SET::ARGS))
          ((exists-list<not> ?x) (,SET::EXISTS-LIST<NOT-P> ,@SET::ARGS))
          ((find-list<not> ?x) (,SET::FIND-LIST<NOT-P> ,@SET::ARGS))
          ((filter-list<not> ?x) (,SET::FILTER-LIST<NOT-P> ,@SET::ARGS))))
      (fn-subs (list* `((xargs :guard (true-listp ?list)
             :verify-guards nil) (xargs :guard (and (true-listp ?list)
                ,@SET::LIST-GUARD
                ,@SET::ARG-GUARD)
              :verify-guards nil))
          `((xargs :guard (setp ?set) :verify-guards nil) (xargs :guard (and (setp ?set)
                ,@SET::SET-GUARD
                ,@SET::ARG-GUARD)
              :verify-guards nil))
          subs))
      (all-trigger<p> (mksym (app "all-trigger" wrap) in-package))
      (all-trigger<not-p> (mksym (app "all-trigger" not-wrap)
          in-package))
      (all-strategy<p> (mksym (app "all-strategy" wrap) in-package))
      (all-strategy<not-p> (mksym (app "all-strategy" not-wrap)
          in-package))
      (all-list-trigger<p> (mksym (app "all-list-trigger" wrap)
          in-package))
      (all-list-trigger<not-p> (mksym (app "all-list-trigger" not-wrap)
          in-package))
      (all-list-strategy<p> (mksym (app "all-list-strategy" wrap)
          in-package))
      (all-list-strategy<not-p> (mksym (app "all-list-strategy" not-wrap)
          in-package))
      (theory<p> (mksym (app "theory" wrap) in-package))
      (suffix (mksym wrap in-package))
      (thm-names (append (defthm-names *theorems*)
          (defthm-names *final-theorems*)))
      (thm-name-map (create-new-names thm-names suffix))
      (theory<p>-defthms (sublis thm-name-map thm-names)))
    `(encapsulate nil
      (instance-*functions* :subs ,SET::FN-SUBS
        :suffix ,SET::NAME)
      (instance-*theorems* :subs ,SET::SUBS
        :suffix ,(SET::MKSYM SET::WRAP IN-PACKAGE))
      (defund ,SET::ALL-TRIGGER<P>
        (,@SET::ARGS)
        (declare (xargs :verify-guards nil))
        (,SET::ALL<P> ,@SET::ARGS))
      (defund ,SET::ALL-TRIGGER<NOT-P>
        (,@SET::ARGS)
        (declare (xargs :verify-guards nil))
        (,SET::ALL<NOT-P> ,@SET::ARGS))
      (defund ,SET::ALL-LIST-TRIGGER<P>
        (,@SET::ARGS)
        (declare (xargs :verify-guards nil))
        (,SET::ALL-LIST<P> ,@SET::ARGS))
      (defund ,SET::ALL-LIST-TRIGGER<NOT-P>
        (,@SET::ARGS)
        (declare (xargs :verify-guards nil))
        (,SET::ALL-LIST<NOT-P> ,@SET::ARGS))
      (defthm ,SET::ALL-STRATEGY<P>
        (implies (and (syntaxp (rewriting-goal-lit mfc state))
            (syntaxp (rewriting-conc-lit (list ',SET::ALL<P> ,@SET::ARGS)
                mfc
                state)))
          (equal (,SET::ALL<P> ,@SET::ARGS)
            (,SET::ALL-TRIGGER<P> ,@SET::ARGS)))
        :hints (("Goal" :in-theory (union-theories (theory 'minimal-theory)
             '((:d ,SET::ALL-TRIGGER<P>))))))
      (defthm ,SET::ALL-STRATEGY<NOT-P>
        (implies (and (syntaxp (rewriting-goal-lit mfc state))
            (syntaxp (rewriting-conc-lit (list ',SET::ALL<NOT-P> ,@SET::ARGS)
                mfc
                state)))
          (equal (,SET::ALL<NOT-P> ,@SET::ARGS)
            (,SET::ALL-TRIGGER<NOT-P> ,@SET::ARGS)))
        :hints (("Goal" :in-theory (union-theories (theory 'minimal-theory)
             '((:d ,SET::ALL-TRIGGER<NOT-P>))))))
      (defthm ,SET::ALL-LIST-STRATEGY<P>
        (implies (and (syntaxp (rewriting-goal-lit mfc state))
            (syntaxp (rewriting-conc-lit (list ',SET::ALL-LIST<P> ,@SET::ARGS)
                mfc
                state)))
          (equal (,SET::ALL-LIST<P> ,@SET::ARGS)
            (,SET::ALL-LIST-TRIGGER<P> ,@SET::ARGS)))
        :hints (("Goal" :in-theory (union-theories (theory 'minimal-theory)
             '((:d ,SET::ALL-LIST-TRIGGER<P>))))))
      (defthm ,SET::ALL-LIST-STRATEGY<NOT-P>
        (implies (and (syntaxp (rewriting-goal-lit mfc state))
            (syntaxp (rewriting-conc-lit (list ',SET::ALL-LIST<NOT-P> ,@SET::ARGS)
                mfc
                state)))
          (equal (,SET::ALL-LIST<NOT-P> ,@SET::ARGS)
            (,SET::ALL-LIST-TRIGGER<NOT-P> ,@SET::ARGS)))
        :hints (("Goal" :in-theory (union-theories (theory 'minimal-theory)
             '((:d ,SET::ALL-LIST-TRIGGER<NOT-P>))))))
      (automate-instantiation :new-hint-name ,(SET::MKSYM (SET::APP "all-by-membership-hint" SET::WRAP) IN-PACKAGE)
        :generic-theorem all-by-membership
        :generic-predicate predicate
        :generic-hyps all-hyps
        :generic-collection all-set
        :generic-collection-predicate all
        :actual-collection-predicate ,SET::ALL<P>
        :actual-trigger ,SET::ALL-TRIGGER<P>
        :predicate-rewrite (((predicate ,@(SET::?IFY SET::ARGS)) (,SET::NAME ,@(SET::?IFY SET::ARGS))))
        :tagging-theorem ,SET::ALL-STRATEGY<P>)
      (automate-instantiation :new-hint-name ,(SET::MKSYM (SET::APP "all-by-membership-hint" SET::NOT-WRAP) IN-PACKAGE)
        :generic-theorem all-by-membership
        :generic-predicate predicate
        :generic-hyps all-hyps
        :generic-collection all-set
        :generic-collection-predicate all
        :actual-collection-predicate ,SET::ALL<NOT-P>
        :actual-trigger ,SET::ALL-TRIGGER<NOT-P>
        :predicate-rewrite (((predicate ,@(SET::?IFY SET::ARGS)) (not (,SET::NAME ,@(SET::?IFY SET::ARGS)))))
        :tagging-theorem ,SET::ALL-STRATEGY<NOT-P>)
      (automate-instantiation :new-hint-name ,(SET::MKSYM (SET::APP "all-list-by-membership-hint" SET::WRAP) IN-PACKAGE)
        :generic-theorem all-list-by-membership
        :generic-predicate predicate
        :generic-hyps all-list-hyps
        :generic-collection all-list-list
        :generic-collection-predicate all-list
        :actual-collection-predicate ,SET::ALL-LIST<P>
        :actual-trigger ,SET::ALL-LIST-TRIGGER<P>
        :predicate-rewrite (((predicate ,@(SET::?IFY SET::ARGS)) (,SET::NAME ,@(SET::?IFY SET::ARGS))))
        :tagging-theorem ,SET::ALL-LIST-STRATEGY<P>)
      (automate-instantiation :new-hint-name ,(SET::MKSYM (SET::APP "all-list-by-membership-hint" SET::NOT-WRAP) IN-PACKAGE)
        :generic-theorem all-list-by-membership
        :generic-predicate predicate
        :generic-hyps all-list-hyps
        :generic-collection all-list-list
        :generic-collection-predicate all-list
        :actual-collection-predicate ,SET::ALL-LIST<NOT-P>
        :actual-trigger ,SET::ALL-LIST-TRIGGER<NOT-P>
        :predicate-rewrite (((predicate ,@(SET::?IFY SET::ARGS)) (not (,SET::NAME ,@(SET::?IFY SET::ARGS)))))
        :tagging-theorem ,SET::ALL-LIST-STRATEGY<NOT-P>)
      (instance-*final-theorems* :subs ,SET::SUBS
        :suffix ,(SET::MKSYM SET::WRAP IN-PACKAGE))
      ,@(AND SET::VERIFY-GUARDS
       `((SET::LOCAL
          (SET::IN-THEORY
           (SET::ENABLE ,SET::ALL<P> ,SET::EXISTS<P> ,SET::FIND<P>
            ,SET::FILTER<P> ,SET::ALL<NOT-P> ,SET::EXISTS<NOT-P>
            ,SET::FIND<NOT-P> ,SET::FILTER<NOT-P> ,SET::ALL-LIST<P>
            ,SET::EXISTS-LIST<P> ,SET::FIND-LIST<P> ,SET::FILTER-LIST<P>
            ,SET::ALL-LIST<NOT-P> ,SET::EXISTS-LIST<NOT-P>
            ,SET::FIND-LIST<NOT-P> ,SET::FILTER-LIST<NOT-P>)))
         (SET::VERIFY-GUARDS ,SET::ALL<P>) (SET::VERIFY-GUARDS ,SET::EXISTS<P>)
         (SET::VERIFY-GUARDS ,SET::FIND<P>)
         (SET::VERIFY-GUARDS ,SET::FILTER<P>)
         (SET::VERIFY-GUARDS ,SET::ALL<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::EXISTS<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::FIND<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::FILTER<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::ALL-LIST<P>)
         (SET::VERIFY-GUARDS ,SET::EXISTS-LIST<P>)
         (SET::VERIFY-GUARDS ,SET::FIND-LIST<P>)
         (SET::VERIFY-GUARDS ,SET::FILTER-LIST<P>)
         (SET::VERIFY-GUARDS ,SET::ALL-LIST<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::EXISTS-LIST<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::FIND-LIST<NOT-P>)
         (SET::VERIFY-GUARDS ,SET::FILTER-LIST<NOT-P>)))
      (deftheory ,SET::THEORY<P>
        '(,@SET::THEORY<P>-DEFTHMS ,SET::ALL<P>
          ,SET::ALL-LIST<P>
          ,SET::EXISTS<P>
          ,SET::EXISTS-LIST<P>
          ,SET::FIND<P>
          ,SET::FIND-LIST<P>
          ,SET::FILTER<P>
          ,SET::FILTER-LIST<P>
          ,SET::ALL<NOT-P>
          ,SET::ALL-LIST<NOT-P>
          ,SET::EXISTS<NOT-P>
          ,SET::EXISTS-LIST<NOT-P>
          ,SET::FIND<NOT-P>
          ,SET::FIND-LIST<NOT-P>
          ,SET::FILTER<NOT-P>
          ,SET::FILTER-LIST<NOT-P>
          ,SET::ALL-TRIGGER<P>
          ,SET::ALL-LIST-TRIGGER<P>
          ,SET::ALL-TRIGGER<NOT-P>
          ,SET::ALL-LIST-TRIGGER<NOT-P>
          ,SET::ALL-STRATEGY<P>
          ,SET::ALL-LIST-STRATEGY<P>
          ,SET::ALL-STRATEGY<NOT-P>
          ,SET::ALL-LIST-STRATEGY<NOT-P>)))))
quantify-predicatemacro
(defmacro quantify-predicate
  (predicate &key
    in-package-of
    set-guard
    list-guard
    arg-guard
    (verify-guards 't))
  (quantify-simple-predicate predicate
    (if in-package-of
      in-package-of
      'in)
    (standardize-to-package "?SET"
      '?set
      set-guard)
    (standardize-to-package "?LIST"
      '?list
      list-guard)
    arg-guard
    verify-guards))
other
(deftheory generic-quantification-theory
  `(,@(INSTANCE::DEFTHM-NAMES SET::*THEOREMS*) ,@(INSTANCE::DEFTHM-NAMES SET::*FINAL-THEOREMS*)
    all
    exists
    find
    filter
    all-list
    exists-list
    find-list
    filter-list
    all<not>
    exists<not>
    find<not>
    filter<not>
    all-list<not>
    exists-list<not>
    find-list<not>
    filter-list<not>))
other
(in-theory (disable generic-quantification-theory))