		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Ext-declon-list-rename-fn

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

Definitions and Theorems

Function: ext-declon-list-rename-fn

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

Theorem: ext-declon-listp-of-ext-declon-list-rename-fn

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

Theorem: ext-declon-list-rename-fn-type-prescription

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

Theorem: ext-declon-list-rename-fn-when-atom

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

Theorem: ext-declon-list-rename-fn-of-cons

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

Theorem: ext-declon-list-rename-fn-of-append

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

Theorem: consp-of-ext-declon-list-rename-fn

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

Theorem: len-of-ext-declon-list-rename-fn

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

Theorem: nth-of-ext-declon-list-rename-fn

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

Theorem: ext-declon-list-rename-fn-of-revappend

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

Theorem: ext-declon-list-rename-fn-of-reverse

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

Theorem: ext-declon-list-rename-fn-of-ext-declon-list-fix-ext-declon-list

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

Theorem: ext-declon-list-rename-fn-ext-declon-list-equiv-congruence-on-ext-declon-list

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

Theorem: ext-declon-list-rename-fn-of-uid-fix-uid

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

Theorem: ext-declon-list-rename-fn-uid-equiv-congruence-on-uid

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

Theorem: ext-declon-list-rename-fn-of-ident-fix-new-fn

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

Theorem: ext-declon-list-rename-fn-ident-equiv-congruence-on-new-fn

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