		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Var-list-renamevar

Check if two lists of variables are related by variable renaming.

Signature
(var-list-renamevar old new ren) → _
Arguments: old — Guard (identifier-listp old).; new — Guard (identifier-listp new).; ren — Guard (renamingp ren).
Returns: _ — Type (reserr-optionp _).

The two lists must have the same length, and corresponding elements must be related.

Definitions and Theorems

Function: var-list-renamevar

(defun var-list-renamevar (old new ren)
 (declare (xargs :guard (and (identifier-listp old)
                             (identifier-listp new)
                             (renamingp ren))))
 (let ((__function__ 'var-list-renamevar))
  (declare (ignorable __function__))
  (b*
   (((when (endp old))
     (if (endp new)
         nil
       (reserrf
            (list :mismatch-extra-new (identifier-list-fix new)))))
    ((when (endp new))
     (reserrf (list :mismatch-extra-old (identifier-list-fix old))))
    ((okf &)
     (var-renamevar (car old)
                    (car new)
                    ren)))
   (var-list-renamevar (cdr old)
                       (cdr new)
                       ren))))

Theorem: reserr-optionp-of-var-list-renamevar

(defthm reserr-optionp-of-var-list-renamevar
  (b* ((_ (var-list-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: var-list-renamevar-of-identifier-list-fix-old

(defthm var-list-renamevar-of-identifier-list-fix-old
  (equal (var-list-renamevar (identifier-list-fix old)
                             new ren)
         (var-list-renamevar old new ren)))

Theorem: var-list-renamevar-identifier-list-equiv-congruence-on-old

(defthm var-list-renamevar-identifier-list-equiv-congruence-on-old
  (implies (identifier-list-equiv old old-equiv)
           (equal (var-list-renamevar old new ren)
                  (var-list-renamevar old-equiv new ren)))
  :rule-classes :congruence)

Theorem: var-list-renamevar-of-identifier-list-fix-new

(defthm var-list-renamevar-of-identifier-list-fix-new
  (equal (var-list-renamevar old (identifier-list-fix new)
                             ren)
         (var-list-renamevar old new ren)))

Theorem: var-list-renamevar-identifier-list-equiv-congruence-on-new

(defthm var-list-renamevar-identifier-list-equiv-congruence-on-new
  (implies (identifier-list-equiv new new-equiv)
           (equal (var-list-renamevar old new ren)
                  (var-list-renamevar old new-equiv ren)))
  :rule-classes :congruence)

Theorem: var-list-renamevar-of-renaming-fix-ren

(defthm var-list-renamevar-of-renaming-fix-ren
  (equal (var-list-renamevar old new (renaming-fix ren))
         (var-list-renamevar old new ren)))

Theorem: var-list-renamevar-renaming-equiv-congruence-on-ren

(defthm var-list-renamevar-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (var-list-renamevar old new ren)
                  (var-list-renamevar old new ren-equiv)))
  :rule-classes :congruence)