		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Iconst-rename

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

Definitions and Theorems

Function: iconst-rename

(defun iconst-rename (iconst subst)
  (declare (xargs :guard (and (c$::iconstp iconst)
                              (ident-ident-alistp subst))))
  (declare (ignorable iconst subst))
  (let ((__function__ 'iconst-rename))
    (declare (ignorable __function__))
    (c$::iconst-fix iconst)))

Theorem: iconstp-of-iconst-rename

(defthm iconstp-of-iconst-rename
  (b* ((fty::result (iconst-rename iconst subst)))
    (c$::iconstp fty::result))
  :rule-classes :rewrite)

Theorem: iconst-rename-of-iconst-fix-iconst

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

Theorem: iconst-rename-iconst-equiv-congruence-on-iconst

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

Theorem: iconst-rename-of-ident-ident-alist-fix-subst

(defthm iconst-rename-of-ident-ident-alist-fix-subst
  (equal (iconst-rename iconst (ident-ident-alist-fix subst))
         (iconst-rename iconst subst)))

Theorem: iconst-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm iconst-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (iconst-rename iconst subst)
                  (iconst-rename iconst subst-equiv)))
  :rule-classes :congruence)