		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Ext-declon-rename-fn

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

Definitions and Theorems

Function: ext-declon-rename-fn

(defun ext-declon-rename-fn (c$::ext-declon uid new-fn)
 (declare (xargs :guard (and (ext-declonp c$::ext-declon)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::ext-declon uid new-fn))
 (ext-declon-case
  c$::ext-declon
  :fundef
  (ext-declon-fundef
       (fundef-rename-fn (ext-declon-fundef->fundef c$::ext-declon)
                         uid new-fn))
  :declon
  (ext-declon-declon
    (declon-rename-fn (c$::ext-declon-declon->declon c$::ext-declon)
                      uid new-fn))
  :empty (ext-declon-fix c$::ext-declon)
  :asm
  (c$::ext-declon-asm
       (asm-stmt-rename-fn (c$::ext-declon-asm->stmt c$::ext-declon)
                           uid new-fn))))

Theorem: ext-declonp-of-ext-declon-rename-fn

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

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

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

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

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

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

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

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

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

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

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

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

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