		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Ident-list-rename

Signature
(ident-list-rename c$::ident-list subst) → fty::result
Arguments: c$::ident-list — Guard (ident-listp c$::ident-list).; subst — Guard (ident-ident-alistp subst).
Returns: fty::result — Type (ident-listp fty::result).

Definitions and Theorems

Function: ident-list-rename

(defun ident-list-rename (c$::ident-list subst)
  (declare (xargs :guard (and (ident-listp c$::ident-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'ident-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::ident-list)
        nil
      (cons (ident-rename (car c$::ident-list)
                          subst)
            (ident-list-rename (cdr c$::ident-list)
                               subst)))))

Theorem: ident-listp-of-ident-list-rename

(defthm ident-listp-of-ident-list-rename
  (b* ((fty::result (ident-list-rename c$::ident-list subst)))
    (ident-listp fty::result))
  :rule-classes :rewrite)

Theorem: ident-list-rename-type-prescription

(defthm ident-list-rename-type-prescription
  (true-listp (ident-list-rename c$::ident-list subst))
  :rule-classes :type-prescription)

Theorem: ident-list-rename-when-atom

(defthm ident-list-rename-when-atom
  (implies (atom c$::ident-list)
           (equal (ident-list-rename c$::ident-list subst)
                  nil)))

Theorem: ident-list-rename-of-cons

(defthm ident-list-rename-of-cons
  (equal (ident-list-rename (cons ident c$::ident-list)
                            subst)
         (cons (ident-rename ident subst)
               (ident-list-rename c$::ident-list subst))))

Theorem: ident-list-rename-of-append

(defthm ident-list-rename-of-append
  (equal (ident-list-rename (append acl2::x acl2::y)
                            subst)
         (append (ident-list-rename acl2::x subst)
                 (ident-list-rename acl2::y subst))))

Theorem: consp-of-ident-list-rename

(defthm consp-of-ident-list-rename
  (equal (consp (ident-list-rename c$::ident-list subst))
         (consp c$::ident-list)))

Theorem: len-of-ident-list-rename

(defthm len-of-ident-list-rename
  (equal (len (ident-list-rename c$::ident-list subst))
         (len c$::ident-list)))

Theorem: nth-of-ident-list-rename

(defthm nth-of-ident-list-rename
  (equal (nth acl2::n
              (ident-list-rename c$::ident-list subst))
         (if (< (nfix acl2::n) (len c$::ident-list))
             (ident-rename (nth acl2::n c$::ident-list)
                           subst)
           nil)))

Theorem: ident-list-rename-of-revappend

(defthm ident-list-rename-of-revappend
  (equal (ident-list-rename (revappend acl2::x acl2::y)
                            subst)
         (revappend (ident-list-rename acl2::x subst)
                    (ident-list-rename acl2::y subst))))

Theorem: ident-list-rename-of-reverse

(defthm ident-list-rename-of-reverse
  (equal (ident-list-rename (reverse c$::ident-list)
                            subst)
         (reverse (ident-list-rename c$::ident-list subst))))

Theorem: ident-list-rename-of-ident-list-fix-ident-list

(defthm ident-list-rename-of-ident-list-fix-ident-list
  (equal (ident-list-rename (c$::ident-list-fix c$::ident-list)
                            subst)
         (ident-list-rename c$::ident-list subst)))

Theorem: ident-list-rename-ident-list-equiv-congruence-on-ident-list

(defthm ident-list-rename-ident-list-equiv-congruence-on-ident-list
  (implies (c$::ident-list-equiv c$::ident-list ident-list-equiv)
           (equal (ident-list-rename c$::ident-list subst)
                  (ident-list-rename ident-list-equiv subst)))
  :rule-classes :congruence)

Theorem: ident-list-rename-of-ident-ident-alist-fix-subst

(defthm ident-list-rename-of-ident-ident-alist-fix-subst
  (equal (ident-list-rename c$::ident-list
                            (ident-ident-alist-fix subst))
         (ident-list-rename c$::ident-list subst)))

Theorem: ident-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      ident-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (ident-list-rename c$::ident-list subst)
                  (ident-list-rename c$::ident-list subst-equiv)))
  :rule-classes :congruence)