		Search-engine friendly clone of the ACL2 documentation.

Vl-scopedef

Vl-scopedef-p

Signature
(vl-scopedef-p x) → *

Definitions and Theorems

Function: vl-scopedef-p

(defun vl-scopedef-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scopedef-p))
    (declare (ignorable __function__))
    (common-lisp::case (tag x)
      ((:vl-module) (vl-module-p x))
      ((:vl-udp) (vl-udp-p x))
      ((:vl-interface) (vl-interface-p x))
      ((:vl-program) (vl-program-p x))
      (otherwise (vl-class-p x)))))

Theorem: consp-when-vl-scopedef-p

(defthm consp-when-vl-scopedef-p
  (implies (vl-scopedef-p x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: vl-scopedef-p-when-vl-module-p

(defthm vl-scopedef-p-when-vl-module-p
  (implies (vl-module-p x)
           (vl-scopedef-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-scopedef-p-when-vl-udp-p

(defthm vl-scopedef-p-when-vl-udp-p
  (implies (vl-udp-p x) (vl-scopedef-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-scopedef-p-when-vl-interface-p

(defthm vl-scopedef-p-when-vl-interface-p
  (implies (vl-interface-p x)
           (vl-scopedef-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-scopedef-p-when-vl-program-p

(defthm vl-scopedef-p-when-vl-program-p
  (implies (vl-program-p x)
           (vl-scopedef-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-scopedef-p-when-vl-class-p

(defthm vl-scopedef-p-when-vl-class-p
  (implies (vl-class-p x)
           (vl-scopedef-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-module-p-by-tag-when-vl-scopedef-p

(defthm vl-module-p-by-tag-when-vl-scopedef-p
  (implies (and (or (equal (tag x) :vl-module))
                (vl-scopedef-p x))
           (vl-module-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-udp-p-by-tag-when-vl-scopedef-p

(defthm vl-udp-p-by-tag-when-vl-scopedef-p
  (implies (and (or (equal (tag x) :vl-udp))
                (vl-scopedef-p x))
           (vl-udp-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-interface-p-by-tag-when-vl-scopedef-p

(defthm vl-interface-p-by-tag-when-vl-scopedef-p
  (implies (and (or (equal (tag x) :vl-interface))
                (vl-scopedef-p x))
           (vl-interface-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-program-p-by-tag-when-vl-scopedef-p

(defthm vl-program-p-by-tag-when-vl-scopedef-p
  (implies (and (or (equal (tag x) :vl-program))
                (vl-scopedef-p x))
           (vl-program-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-class-p-by-tag-when-vl-scopedef-p

(defthm vl-class-p-by-tag-when-vl-scopedef-p
  (implies (and (or (equal (tag x) :vl-class))
                (vl-scopedef-p x))
           (vl-class-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-scopedef-p-when-invalid-tag

(defthm vl-scopedef-p-when-invalid-tag
  (implies (and (not (equal (tag x) :vl-module))
                (not (equal (tag x) :vl-udp))
                (not (equal (tag x) :vl-interface))
                (not (equal (tag x) :vl-program))
                (not (equal (tag x) :vl-class)))
           (not (vl-scopedef-p x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: tag-when-vl-scopedef-p-forward

(defthm tag-when-vl-scopedef-p-forward
  (implies (vl-scopedef-p x)
           (or (equal (tag x) :vl-module)
               (equal (tag x) :vl-udp)
               (equal (tag x) :vl-interface)
               (equal (tag x) :vl-program)
               (equal (tag x) :vl-class)))
  :rule-classes ((:forward-chaining)))