		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Ext-declon-rename

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

Definitions and Theorems

Function: ext-declon-rename

(defun ext-declon-rename (c$::ext-declon subst)
 (declare (xargs :guard (and (ext-declonp c$::ext-declon)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::ext-declon subst))
 (let ((__function__ 'ext-declon-rename))
  (declare (ignorable __function__))
  (ext-declon-case
   c$::ext-declon
   :fundef
   (ext-declon-fundef
        (fundef-rename (ext-declon-fundef->fundef c$::ext-declon)
                       subst))
   :declon
   (ext-declon-declon
       (declon-rename (c$::ext-declon-declon->declon c$::ext-declon)
                      subst))
   :empty (ext-declon-fix c$::ext-declon)
   :asm
   (c$::ext-declon-asm
        (asm-stmt-rename (c$::ext-declon-asm->stmt c$::ext-declon)
                         subst)))))

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

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

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

(defthm ext-declon-rename-of-ext-declon-fix-ext-declon
  (equal (ext-declon-rename (ext-declon-fix c$::ext-declon)
                            subst)
         (ext-declon-rename c$::ext-declon subst)))

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

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

Theorem: ext-declon-rename-of-ident-ident-alist-fix-subst

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

Theorem: ext-declon-rename-ident-ident-alist-equiv-congruence-on-subst

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