		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Expressions-renamevar

Mutually recursive ACL2 functions to check if expressions are related by variable renaming.

Definitions and Theorems

Function: expression-renamevar

(defun expression-renamevar (old new ren)
  (declare (xargs :guard (and (expressionp old)
                              (expressionp new)
                              (renamingp ren))))
  (let ((__function__ 'expression-renamevar))
    (declare (ignorable __function__))
    (expression-case
         old :path
         (b* (((unless (expression-case new :path))
               (reserrf (list :mismatch (expression-fix old)
                              (expression-fix new))))
              ((expression-path new) new))
           (path-renamevar old.get new.get ren))
         :literal
         (if (expression-equiv old new)
             nil
           (reserrf (list :mismatch (expression-fix old)
                          (expression-fix new))))
         :funcall
         (b* (((unless (expression-case new :funcall))
               (reserrf (list :mismatch (expression-fix old)
                              (expression-fix new))))
              ((expression-funcall new) new))
           (funcall-renamevar old.get new.get ren)))))

Function: expression-list-renamevar

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

Function: funcall-renamevar

(defun funcall-renamevar (old new ren)
  (declare (xargs :guard (and (funcallp old)
                              (funcallp new)
                              (renamingp ren))))
  (let ((__function__ 'funcall-renamevar))
    (declare (ignorable __function__))
    (b* (((funcall old) old)
         ((funcall new) new)
         ((unless (equal old.name new.name))
          (reserrf (list :mismatch (funcall-fix old)
                         (funcall-fix new)))))
      (expression-list-renamevar old.args new.args ren))))

Theorem: return-type-of-expression-renamevar._

(defthm return-type-of-expression-renamevar._
  (b* ((?_ (expression-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-expression-list-renamevar._

(defthm return-type-of-expression-list-renamevar._
  (b* ((?_ (expression-list-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-funcall-renamevar._

(defthm return-type-of-funcall-renamevar._
  (b* ((?_ (funcall-renamevar old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: expression-renamevar-of-expression-fix-old

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

Theorem: expression-renamevar-of-expression-fix-new

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

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

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

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

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

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

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

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

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

Theorem: funcall-renamevar-of-funcall-fix-old

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

Theorem: funcall-renamevar-of-funcall-fix-new

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Expression-renamevar: Check if two expressions are related by variable renaming.
Expression-list-renamevar: Check if two lists of expressions are related by variable renaming.
Funcall-renamevar: Check if two function calls are related by variable renaming.