		Search-engine friendly clone of the ACL2 documentation.

Vl-scope

Vl-scope-p

Recognizer for vl-scope.

Signature
(vl-scope-p x) → *

Definitions and Theorems

Function: vl-scope-p

(defun vl-scope-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scope-p))
    (declare (ignorable __function__))
    (common-lisp::case (tag x)
      ((:vl-interface) (vl-interface-p x))
      ((:vl-module) (vl-module-p x))
      ((:vl-class) (vl-class-p x))
      ((:vl-genblob) (vl-genblob-p x))
      ((:vl-blockscope) (vl-blockscope-p x))
      ((:vl-design) (vl-design-p x))
      ((:vl-package) (vl-package-p x))
      (otherwise (vl-scopeinfo-p x)))))

Theorem: consp-when-vl-scope-p

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

Theorem: vl-scope-p-when-vl-interface-p

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

Theorem: vl-scope-p-when-vl-module-p

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

Theorem: vl-scope-p-when-vl-class-p

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

Theorem: vl-scope-p-when-vl-genblob-p

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

Theorem: vl-scope-p-when-vl-blockscope-p

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

Theorem: vl-scope-p-when-vl-design-p

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

Theorem: vl-scope-p-when-vl-package-p

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

Theorem: vl-scope-p-when-vl-scopeinfo-p

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

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

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

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

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

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

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

Theorem: vl-genblob-p-by-tag-when-vl-scope-p

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

Theorem: vl-blockscope-p-by-tag-when-vl-scope-p

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

Theorem: vl-design-p-by-tag-when-vl-scope-p

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

Theorem: vl-package-p-by-tag-when-vl-scope-p

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

Theorem: vl-scopeinfo-p-by-tag-when-vl-scope-p

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

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

(defthm vl-scope-p-when-invalid-tag
  (implies (and (not (equal (tag x) :vl-interface))
                (not (equal (tag x) :vl-module))
                (not (equal (tag x) :vl-class))
                (not (equal (tag x) :vl-genblob))
                (not (equal (tag x) :vl-blockscope))
                (not (equal (tag x) :vl-design))
                (not (equal (tag x) :vl-package))
                (not (equal (tag x) :vl-scopeinfo)))
           (not (vl-scope-p x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

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

(defthm tag-when-vl-scope-p-forward
  (implies (vl-scope-p x)
           (or (equal (tag x) :vl-interface)
               (equal (tag x) :vl-module)
               (equal (tag x) :vl-class)
               (equal (tag x) :vl-genblob)
               (equal (tag x) :vl-blockscope)
               (equal (tag x) :vl-design)
               (equal (tag x) :vl-package)
               (equal (tag x) :vl-scopeinfo)))
  :rule-classes ((:forward-chaining)))