		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Funscope-renamevarp

Variable renaming relation over function scopes.

Signature
(funscope-renamevarp old new) → yes/no
Arguments: old — Guard (funscopep old).; new — Guard (funscopep new).
Returns: yes/no — Type (booleanp yes/no).

The two scopes must have the same function names, and the function information for the same function name must be related.

Definitions and Theorems

Function: funscope-renamevarp

(defun funscope-renamevarp (old new)
 (declare (xargs :guard (and (funscopep old) (funscopep new))))
 (let ((__function__ 'funscope-renamevarp))
  (declare (ignorable __function__))
  (b* ((old (funscope-fix old))
       (new (funscope-fix new)))
   (and
      (or (and (omap::emptyp old)
               (omap::emptyp new))
          (and (not (omap::emptyp old))
               (not (omap::emptyp new))
               (b* (((mv old-fun old-info) (omap::head old))
                    ((mv new-fun new-info)
                     (omap::head new)))
                 (and (equal old-fun new-fun)
                      (funinfo-renamevarp old-info new-info)
                      (funscope-renamevarp (omap::tail old)
                                           (omap::tail new))))))))))

Theorem: booleanp-of-funscope-renamevarp

(defthm booleanp-of-funscope-renamevarp
  (b* ((yes/no (funscope-renamevarp old new)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: funscope-renamevarp-of-funscope-fix-old

(defthm funscope-renamevarp-of-funscope-fix-old
  (equal (funscope-renamevarp (funscope-fix old)
                              new)
         (funscope-renamevarp old new)))

Theorem: funscope-renamevarp-funscope-equiv-congruence-on-old

(defthm funscope-renamevarp-funscope-equiv-congruence-on-old
  (implies (funscope-equiv old old-equiv)
           (equal (funscope-renamevarp old new)
                  (funscope-renamevarp old-equiv new)))
  :rule-classes :congruence)

Theorem: funscope-renamevarp-of-funscope-fix-new

(defthm funscope-renamevarp-of-funscope-fix-new
  (equal (funscope-renamevarp old (funscope-fix new))
         (funscope-renamevarp old new)))

Theorem: funscope-renamevarp-funscope-equiv-congruence-on-new

(defthm funscope-renamevarp-funscope-equiv-congruence-on-new
  (implies (funscope-equiv new new-equiv)
           (equal (funscope-renamevarp old new)
                  (funscope-renamevarp old new-equiv)))
  :rule-classes :congruence)