		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Path-renamevar

Check if two paths are related by variable renaming.

Signature
(path-renamevar old new ren) → _
Arguments: old — Guard (pathp old).; new — Guard (pathp new).; ren — Guard (renamingp ren).
Returns: _ — Type (reserr-optionp _).

The two paths must be both singletons, whose identifiers must be related.

Definitions and Theorems

Function: path-renamevar

(defun path-renamevar (old new ren)
  (declare (xargs :guard (and (pathp old)
                              (pathp new)
                              (renamingp ren))))
  (let ((__function__ 'path-renamevar))
    (declare (ignorable __function__))
    (b* ((old-ids (path->get old))
         ((unless (and (consp old-ids)
                       (endp (cdr old-ids))))
          (reserrf (list :non-singleton-old-path (path-fix old))))
         (old-id (car old-ids))
         (new-ids (path->get new))
         ((unless (and (consp new-ids)
                       (endp (cdr new-ids))))
          (reserrf (list :non-singleton-old-path (path-fix new))))
         (new-id (car new-ids)))
      (var-renamevar old-id new-id ren))))

Theorem: reserr-optionp-of-path-renamevar

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

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

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

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

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

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

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

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

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

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

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

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

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