		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Path-list-renamevar

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

Signature
(path-list-renamevar old new ren) → _
Arguments: old — Guard (path-listp old).; new — Guard (path-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: path-list-renamevar

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

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

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

Theorem: same-len-when-path-list-renamevar

(defthm same-len-when-path-list-renamevar
  (implies (not (reserrp (path-list-renamevar old new ren)))
           (equal (len new) (len old))))

Theorem: path-list-renamevar-of-path-list-fix-old

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

Theorem: path-list-renamevar-path-list-equiv-congruence-on-old

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

Theorem: path-list-renamevar-of-path-list-fix-new

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

Theorem: path-list-renamevar-path-list-equiv-congruence-on-new

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

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

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

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

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