		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Extdecl-list-rename-fn

Signature
(extdecl-list-rename-fn c$::extdecl-list uid new-fn) → fty::result
Arguments: c$::extdecl-list — Guard (extdecl-listp c$::extdecl-list).; uid — Guard (c$::uidp uid).; new-fn — Guard (identp new-fn).
Returns: fty::result — Type (extdecl-listp fty::result).

Definitions and Theorems

Function: extdecl-list-rename-fn

(defun extdecl-list-rename-fn (c$::extdecl-list uid new-fn)
  (declare (xargs :guard (and (extdecl-listp c$::extdecl-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::extdecl-list)
      nil
    (cons (extdecl-rename-fn (car c$::extdecl-list)
                             uid new-fn)
          (extdecl-list-rename-fn (cdr c$::extdecl-list)
                                  uid new-fn))))

Theorem: extdecl-listp-of-extdecl-list-rename-fn

(defthm extdecl-listp-of-extdecl-list-rename-fn
  (b* ((fty::result
            (extdecl-list-rename-fn c$::extdecl-list uid new-fn)))
    (extdecl-listp fty::result))
  :rule-classes :rewrite)

Theorem: extdecl-list-rename-fn-type-prescription

(defthm extdecl-list-rename-fn-type-prescription
  (true-listp (extdecl-list-rename-fn c$::extdecl-list uid new-fn))
  :rule-classes :type-prescription)

Theorem: extdecl-list-rename-fn-when-atom

(defthm extdecl-list-rename-fn-when-atom
  (implies
       (atom c$::extdecl-list)
       (equal (extdecl-list-rename-fn c$::extdecl-list uid new-fn)
              nil)))

Theorem: extdecl-list-rename-fn-of-cons

(defthm extdecl-list-rename-fn-of-cons
  (equal
       (extdecl-list-rename-fn (cons c$::extdecl c$::extdecl-list)
                               uid new-fn)
       (cons (extdecl-rename-fn c$::extdecl uid new-fn)
             (extdecl-list-rename-fn c$::extdecl-list uid new-fn))))

Theorem: extdecl-list-rename-fn-of-append

(defthm extdecl-list-rename-fn-of-append
  (equal (extdecl-list-rename-fn (append acl2::x acl2::y)
                                 uid new-fn)
         (append (extdecl-list-rename-fn acl2::x uid new-fn)
                 (extdecl-list-rename-fn acl2::y uid new-fn))))

Theorem: consp-of-extdecl-list-rename-fn

(defthm consp-of-extdecl-list-rename-fn
 (equal (consp (extdecl-list-rename-fn c$::extdecl-list uid new-fn))
        (consp c$::extdecl-list)))

Theorem: len-of-extdecl-list-rename-fn

(defthm len-of-extdecl-list-rename-fn
  (equal (len (extdecl-list-rename-fn c$::extdecl-list uid new-fn))
         (len c$::extdecl-list)))

Theorem: nth-of-extdecl-list-rename-fn

(defthm nth-of-extdecl-list-rename-fn
  (equal (nth acl2::n
              (extdecl-list-rename-fn c$::extdecl-list uid new-fn))
         (if (< (nfix acl2::n)
                (len c$::extdecl-list))
             (extdecl-rename-fn (nth acl2::n c$::extdecl-list)
                                uid new-fn)
           nil)))

Theorem: extdecl-list-rename-fn-of-revappend

(defthm extdecl-list-rename-fn-of-revappend
  (equal (extdecl-list-rename-fn (revappend acl2::x acl2::y)
                                 uid new-fn)
         (revappend (extdecl-list-rename-fn acl2::x uid new-fn)
                    (extdecl-list-rename-fn acl2::y uid new-fn))))

Theorem: extdecl-list-rename-fn-of-reverse

(defthm extdecl-list-rename-fn-of-reverse
 (equal
    (extdecl-list-rename-fn (reverse c$::extdecl-list)
                            uid new-fn)
    (reverse (extdecl-list-rename-fn c$::extdecl-list uid new-fn))))

Theorem: extdecl-list-rename-fn-of-extdecl-list-fix-extdecl-list

(defthm extdecl-list-rename-fn-of-extdecl-list-fix-extdecl-list
  (equal (extdecl-list-rename-fn (extdecl-list-fix c$::extdecl-list)
                                 uid new-fn)
         (extdecl-list-rename-fn c$::extdecl-list uid new-fn)))

Theorem: extdecl-list-rename-fn-extdecl-list-equiv-congruence-on-extdecl-list

(defthm
 extdecl-list-rename-fn-extdecl-list-equiv-congruence-on-extdecl-list
 (implies
     (c$::extdecl-list-equiv c$::extdecl-list extdecl-list-equiv)
     (equal (extdecl-list-rename-fn c$::extdecl-list uid new-fn)
            (extdecl-list-rename-fn extdecl-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: extdecl-list-rename-fn-of-uid-fix-uid

(defthm extdecl-list-rename-fn-of-uid-fix-uid
  (equal (extdecl-list-rename-fn c$::extdecl-list (c$::uid-fix uid)
                                 new-fn)
         (extdecl-list-rename-fn c$::extdecl-list uid new-fn)))

Theorem: extdecl-list-rename-fn-uid-equiv-congruence-on-uid

(defthm extdecl-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal
        (extdecl-list-rename-fn c$::extdecl-list uid new-fn)
        (extdecl-list-rename-fn c$::extdecl-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: extdecl-list-rename-fn-of-ident-fix-new-fn

(defthm extdecl-list-rename-fn-of-ident-fix-new-fn
 (equal
    (extdecl-list-rename-fn c$::extdecl-list uid (ident-fix new-fn))
    (extdecl-list-rename-fn c$::extdecl-list uid new-fn)))

Theorem: extdecl-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm extdecl-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal
        (extdecl-list-rename-fn c$::extdecl-list uid new-fn)
        (extdecl-list-rename-fn c$::extdecl-list uid new-fn-equiv)))
 :rule-classes :congruence)