		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Extdecl-rename-fn

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

Definitions and Theorems

Function: extdecl-rename-fn

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

Theorem: extdeclp-of-extdecl-rename-fn

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

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

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

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

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

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

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

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

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

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

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

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

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