		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Attrib-name-rename

Signature
(attrib-name-rename c$::attrib-name subst) → fty::result
Arguments: c$::attrib-name — Guard (c$::attrib-namep c$::attrib-name).; subst — Guard (ident-ident-alistp subst).
Returns: fty::result — Type (c$::attrib-namep fty::result).

Definitions and Theorems

Function: attrib-name-rename

(defun attrib-name-rename (c$::attrib-name subst)
 (declare (xargs :guard (and (c$::attrib-namep c$::attrib-name)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::attrib-name subst))
 (let ((__function__ 'attrib-name-rename))
  (declare (ignorable __function__))
  (c$::attrib-name-case
   c$::attrib-name
   :ident
   (c$::attrib-name-ident
       (ident-rename (c$::attrib-name-ident->unwrap c$::attrib-name)
                     subst))
   :keyword (c$::attrib-name-fix c$::attrib-name))))

Theorem: attrib-namep-of-attrib-name-rename

(defthm attrib-namep-of-attrib-name-rename
  (b* ((fty::result (attrib-name-rename c$::attrib-name subst)))
    (c$::attrib-namep fty::result))
  :rule-classes :rewrite)

Theorem: attrib-name-rename-of-attrib-name-fix-attrib-name

(defthm attrib-name-rename-of-attrib-name-fix-attrib-name
  (equal (attrib-name-rename (c$::attrib-name-fix c$::attrib-name)
                             subst)
         (attrib-name-rename c$::attrib-name subst)))

Theorem: attrib-name-rename-attrib-name-equiv-congruence-on-attrib-name

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

Theorem: attrib-name-rename-of-ident-ident-alist-fix-subst

(defthm attrib-name-rename-of-ident-ident-alist-fix-subst
  (equal (attrib-name-rename c$::attrib-name
                             (ident-ident-alist-fix subst))
         (attrib-name-rename c$::attrib-name subst)))

Theorem: attrib-name-rename-ident-ident-alist-equiv-congruence-on-subst

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