Filtering...

join-thms

books/clause-processors/join-thms

Included Books

ev-find-rules
other
(in-package "ACL2")
include-book
(include-book "ev-find-rules")
conjoin-clauses-of-onetheorem
(defthm conjoin-clauses-of-one
  (equal (conjoin-clauses (list x)) (disjoin x)))
in-theory
(in-theory (disable conjoin-clauses conjoin disjoin))
pseudo-termp-disjointheorem
(defthm pseudo-termp-disjoin
  (implies (pseudo-term-listp x) (pseudo-termp (disjoin x)))
  :hints (("Goal" :in-theory (enable pseudo-termp pseudo-term-listp disjoin)
     :induct (disjoin x))))
pseudo-termp-conjointheorem
(defthm pseudo-termp-conjoin
  (implies (pseudo-term-listp x) (pseudo-termp (conjoin x)))
  :hints (("Goal" :in-theory (enable conjoin pseudo-termp pseudo-term-listp))))
pseudo-term-listp-disjoin-lsttheorem
(defthm pseudo-term-listp-disjoin-lst
  (implies (pseudo-term-list-listp x)
    (pseudo-term-listp (disjoin-lst x))))
pseudo-termp-conjoin-clausestheorem
(defthm pseudo-termp-conjoin-clauses
  (implies (pseudo-term-list-listp clauses)
    (pseudo-termp (conjoin-clauses clauses)))
  :hints (("Goal" :in-theory (e/d (conjoin-clauses) (disjoin-lst)))))
*def-join-thms-body*constant
(defconst *def-join-thms-body*
  '(encapsulate nil
    (local (in-theory nil))
    (local (in-theory (e/d (append conjoin
            disjoin
            car-cons
            cdr-cons
            disjoin2
            conjoin2
            iff
            if-rule
            quote-rule
            endp
            atom
            car-cdr-elim)
          (default-car default-cdr))))
    (defthm disjoin-cons
      (iff (ev (disjoin (cons x y)) a)
        (or (ev x a) (ev (disjoin y) a))))
    (defthmd disjoin-when-consp
      (implies (consp x)
        (iff (ev (disjoin x) a)
          (or (ev (car x) a) (ev (disjoin (cdr x)) a)))))
    (defthm disjoin-atom
      (implies (not (consp x)) (equal (ev (disjoin x) a) nil))
      :rule-classes ((:rewrite :backchain-limit-lst 0)))
    (defthm disjoin-append
      (iff (ev (disjoin (append x y)) a)
        (or (ev (disjoin x) a) (ev (disjoin y) a)))
      :hints (("goal" :induct (append x y)
         :in-theory (e/d (disjoin-when-consp) (disjoin)))))
    (defthm conjoin-cons
      (iff (ev (conjoin (cons x y)) a)
        (and (ev x a) (ev (conjoin y) a))))
    (defthmd conjoin-when-consp
      (implies (consp x)
        (iff (ev (conjoin x) a)
          (and (ev (car x) a) (ev (conjoin (cdr x)) a)))))
    (defthm conjoin-atom
      (implies (not (consp x)) (equal (ev (conjoin x) a) t))
      :rule-classes ((:rewrite :backchain-limit-lst 0)))
    (defthm conjoin-append
      (iff (ev (conjoin (append x y)) a)
        (and (ev (conjoin x) a) (ev (conjoin y) a)))
      :hints (("goal" :induct (append x y)
         :in-theory (e/d (conjoin-when-consp) (conjoin)))))
    (defthm conjoin-clauses-cons
      (iff (ev (conjoin-clauses (cons x y)) a)
        (and (ev (disjoin x) a) (ev (conjoin-clauses y) a)))
      :hints (("Goal" :in-theory (enable conjoin-clauses disjoin-lst))))
    (defthmd conjoin-clauses-when-consp
      (implies (consp x)
        (iff (ev (conjoin-clauses x) a)
          (and (ev (disjoin (car x)) a)
            (ev (conjoin-clauses (cdr x)) a)))))
    (defthm conjoin-clauses-atom
      (implies (not (consp x))
        (equal (ev (conjoin-clauses x) a) t))
      :hints (("Goal" :in-theory (enable conjoin-clauses disjoin-lst)))
      :rule-classes ((:rewrite :backchain-limit-lst 0)))
    (defthm conjoin-clauses-append
      (iff (ev (conjoin-clauses (append x y)) a)
        (and (ev (conjoin-clauses x) a) (ev (conjoin-clauses y) a)))
      :hints (("goal" :induct (append x y))))))
ev-mk-rulenamefunction
(defun ev-mk-rulename
  (ev name)
  (intern-in-package-of-symbol (concatenate 'string
      (symbol-name ev)
      "-"
      (symbol-name name))
    ev))
ev-pair-rulenamesfunction
(defun ev-pair-rulenames
  (ev names)
  (if (atom names)
    nil
    (cons (cons (car names) (ev-mk-rulename ev (car names)))
      (ev-pair-rulenames ev (cdr names)))))
def-join-thmsmacro
(defmacro def-join-thms
  (ev)
  (let ((alist `((ev . ,EV) . ,(EV-PAIR-RULENAMES EV
  '(DISJOIN-CONS DISJOIN-WHEN-CONSP DISJOIN-ATOM DISJOIN-APPEND CONJOIN-CONS
    CONJOIN-WHEN-CONSP CONJOIN-ATOM CONJOIN-APPEND CONJOIN-CLAUSES-CONS
    CONJOIN-CLAUSES-WHEN-CONSP CONJOIN-CLAUSES-ATOM CONJOIN-CLAUSES-APPEND)))))
    `(make-event (let* ((if-rule (ev-find-fncall-rule ',EV 'if (w state))) (quote-rule (ev-find-quote-rule ',EV (w state)))
          (alist (list* (cons 'if-rule if-rule)
              (cons 'quote-rule quote-rule)
              ',ALIST)))
        (cond ((not if-rule) (er soft
              'def-join-thms
              "Unable to find a rewrite rule for (~x0 X A) when ~
                         (CAR X) is IF~%"
              ',EV))
          ((not quote-rule) (er soft
              'def-join-thms
              "Unable to find a rewrite rule for (~x0 X A) when ~
                         (CAR X) is QUOTE~%"
              ',EV))
          (t (value (sublis alist *def-join-thms-body*))))))))