ev-theoremp

(defmacro def-ev-theoremp
  (ev)
  (let* ((falsify (intern-in-package-of-symbol (concatenate 'string (symbol-name ev) "-FALSIFY")
         ev)) (theoremp (intern-in-package-of-symbol (concatenate 'string (symbol-name ev) "-THEOREMP")
          ev))
      (subst `((ev . ,EV) (falsify . ,FALSIFY)
          (theoremp . ,THEOREMP)
          (disjoin-cons-unless-theoremp . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP) "-DISJOIN-CONS-UNLESS-THEOREMP")
  EV))
          (disjoin-when-consp-unless-theoremp . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP)
               "-DISJOIN-WHEN-CONSP-UNLESS-THEOREMP")
  EV))
          (conjoin-cons . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP) "-CONJOIN-CONS") EV))
          (conjoin-append . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP) "-CONJOIN-APPEND") EV))
          (conjoin-clauses-cons . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP) "-CONJOIN-CLAUSES-CONS") EV))
          (conjoin-clauses-append . ,(INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME THEOREMP) "-CONJOIN-CLAUSES-APPEND") EV))
          (disjoin-cons . ,(EV-MK-RULENAME EV 'DISJOIN-CONS))
          (disjoin-when-consp . ,(EV-MK-RULENAME EV 'DISJOIN-WHEN-CONSP))))
      (event (sublis subst
          '(encapsulate nil
            (local (in-theory nil))
            (def-join-thms ev)
            (defchoose falsify (a) (x) (not (ev x a)))
            (defmacro theoremp (x) `(ev ,X (falsify ,X)))
            (defthm conjoin-cons
              (iff (theoremp (conjoin (cons a b)))
                (and (theoremp a) (theoremp (conjoin b))))
              :hints (("goal" :use ((:instance falsify (x (conjoin (cons a b))) (a (falsify a))) (:instance falsify (x a) (a (falsify (conjoin (cons a b)))))
                   (:instance falsify
                     (x (conjoin (cons a b)))
                     (a (falsify (conjoin b))))
                   (:instance falsify
                     (x (conjoin b))
                     (a (falsify (conjoin (cons a b)))))))))
            (defthm conjoin-append
              (iff (theoremp (conjoin (append a b)))
                (and (theoremp (conjoin a)) (theoremp (conjoin b))))
              :hints (("Goal" :in-theory (enable append endp car-cdr-elim))))
            (defthm conjoin-clauses-cons
              (iff (theoremp (conjoin-clauses (cons cl1 clrest)))
                (and (theoremp (disjoin cl1))
                  (theoremp (conjoin-clauses clrest))))
              :hints (("Goal" :in-theory (enable conjoin-clauses disjoin-lst car-cons cdr-cons))))
            (defthm conjoin-clauses-append
              (iff (theoremp (conjoin-clauses (append cls1 cls2)))
                (and (theoremp (conjoin-clauses cls1))
                  (theoremp (conjoin-clauses cls2))))
              :hints (("goal" :in-theory (enable append endp car-cdr-elim)
                 :induct (append cls1 cls2))))
            (defthm disjoin-cons-unless-theoremp
              (implies (and (equal aa (falsify (disjoin (cons x y))))
                  (syntaxp (not (equal a aa))))
                (iff (ev (disjoin (cons x y)) a)
                  (or (ev x a) (ev (disjoin y) a)))))
            (defthmd disjoin-when-consp-unless-theoremp
              (implies (syntaxp (not (equal a `(falsify ,X))))
                (implies (consp x)
                  (iff (ev (disjoin x) a)
                    (or (ev (car x) a) (ev (disjoin (cdr x)) a)))))
              :hints (("Goal" :in-theory (enable disjoin-when-consp))))
            (in-theory (disable disjoin-cons))))))
    event))