		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinst-remove-name

Signature
(elab-modinst-remove-name name x) → xx
Arguments: name — Guard (name-p name).; x — Guard (elab-modinst-list-p x).
Returns: xx — Type (elab-modinst-list-p xx).

Definitions and Theorems

Function: elab-modinst-remove-name

(defun elab-modinst-remove-name (name x)
  (declare (xargs :guard (and (name-p name)
                              (elab-modinst-list-p x))))
  (let ((__function__ 'elab-modinst-remove-name))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (equal (name-fix (nth *elab-modinst$c->instname* (car x)))
                 (name-fix name))
          (elab-modinst-remove-name name (cdr x))
        (cons (elab-modinst-fix (car x))
              (elab-modinst-remove-name name (cdr x)))))))

Theorem: elab-modinst-list-p-of-elab-modinst-remove-name

(defthm elab-modinst-list-p-of-elab-modinst-remove-name
  (b* ((xx (elab-modinst-remove-name name x)))
    (elab-modinst-list-p xx))
  :rule-classes :rewrite)

Theorem: elab-modinst-remove-name-of-name-fix-name

(defthm elab-modinst-remove-name-of-name-fix-name
  (equal (elab-modinst-remove-name (name-fix name)
                                   x)
         (elab-modinst-remove-name name x)))

Theorem: elab-modinst-remove-name-name-equiv-congruence-on-name

(defthm elab-modinst-remove-name-name-equiv-congruence-on-name
  (implies (name-equiv name name-equiv)
           (equal (elab-modinst-remove-name name x)
                  (elab-modinst-remove-name name-equiv x)))
  :rule-classes :congruence)

Theorem: elab-modinst-remove-name-of-elab-modinst-list-fix-x

(defthm elab-modinst-remove-name-of-elab-modinst-list-fix-x
  (equal (elab-modinst-remove-name name (elab-modinst-list-fix x))
         (elab-modinst-remove-name name x)))

Theorem: elab-modinst-remove-name-elab-modinst-list-equiv-congruence-on-x

(defthm
   elab-modinst-remove-name-elab-modinst-list-equiv-congruence-on-x
  (implies (elab-modinst-list-equiv x x-equiv)
           (equal (elab-modinst-remove-name name x)
                  (elab-modinst-remove-name name x-equiv)))
  :rule-classes :congruence)

Theorem: elab-modinst-list-names-of-remove-name

(defthm elab-modinst-list-names-of-remove-name
  (equal (elab-modinst-list-names (elab-modinst-remove-name name x))
         (remove (name-fix name)
                 (elab-modinst-list-names x))))

Theorem: elab-modinst-remove-name-when-not-member

(defthm elab-modinst-remove-name-when-not-member
  (implies (not (member (name-fix x)
                        (elab-modinst-list-names y)))
           (equal (elab-modinst-remove-name x y)
                  (elab-modinst-list-fix y))))