		Search-engine friendly clone of the ACL2 documentation.

Fgl-generic-rule

Fgl-generic-rule-p

Signature
(fgl-generic-rule-p x) → *

Definitions and Theorems

Function: fgl-generic-rule-p

(defun fgl-generic-rule-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-generic-rule-p))
    (declare (ignorable __function__))
    (case (tag x)
      ((:brewrite :bmeta)
       (fgl-binder-rule-p x))
      (otherwise (fgl-rule-p x)))))

Theorem: consp-when-fgl-generic-rule-p

(defthm consp-when-fgl-generic-rule-p
  (implies (fgl-generic-rule-p x)
           (consp x))
  :rule-classes :compound-recognizer)

Theorem: fgl-generic-rule-p-when-fgl-binder-rule-p

(defthm fgl-generic-rule-p-when-fgl-binder-rule-p
  (implies (fgl-binder-rule-p x)
           (fgl-generic-rule-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: fgl-generic-rule-p-when-fgl-rule-p

(defthm fgl-generic-rule-p-when-fgl-rule-p
  (implies (fgl-rule-p x)
           (fgl-generic-rule-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: fgl-binder-rule-p-by-tag-when-fgl-generic-rule-p

(defthm fgl-binder-rule-p-by-tag-when-fgl-generic-rule-p
  (implies (and (or (equal (tag x) :brewrite)
                    (equal (tag x) :bmeta))
                (fgl-generic-rule-p x))
           (fgl-binder-rule-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: fgl-rule-p-by-tag-when-fgl-generic-rule-p

(defthm fgl-rule-p-by-tag-when-fgl-generic-rule-p
  (implies (and (or (equal (tag x) :rewrite)
                    (equal (tag x) :primitive)
                    (equal (tag x) :meta))
                (fgl-generic-rule-p x))
           (fgl-rule-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: fgl-generic-rule-p-when-invalid-tag

(defthm fgl-generic-rule-p-when-invalid-tag
  (implies (and (not (equal (tag x) :brewrite))
                (not (equal (tag x) :bmeta))
                (not (equal (tag x) :rewrite))
                (not (equal (tag x) :primitive))
                (not (equal (tag x) :meta)))
           (not (fgl-generic-rule-p x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: tag-when-fgl-generic-rule-p-forward

(defthm tag-when-fgl-generic-rule-p-forward
  (implies (fgl-generic-rule-p x)
           (or (equal (tag x) :brewrite)
               (equal (tag x) :bmeta)
               (equal (tag x) :rewrite)
               (equal (tag x) :primitive)
               (equal (tag x) :meta)))
  :rule-classes ((:forward-chaining)))