		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Expressions-renamefun

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

Definitions and Theorems

Function: expression-renamefun

(defun expression-renamefun (old new ren)
  (declare (xargs :guard (and (expressionp old)
                              (expressionp new)
                              (renamingp ren))))
  (let ((__function__ 'expression-renamefun))
    (declare (ignorable __function__))
    (expression-case
         old :path
         (if (expression-equiv old new)
             nil
           (reserrf (list :mismatch (expression-fix old)
                          (expression-fix new))))
         :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-renamefun old.get new.get ren)))))

Function: expression-list-renamefun

(defun expression-list-renamefun (old new ren)
 (declare (xargs :guard (and (expression-listp old)
                             (expression-listp new)
                             (renamingp ren))))
 (let ((__function__ 'expression-list-renamefun))
  (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-renamefun (car old)
                           (car new)
                           ren)))
   (expression-list-renamefun (cdr old)
                              (cdr new)
                              ren))))

Function: funcall-renamefun

(defun funcall-renamefun (old new ren)
  (declare (xargs :guard (and (funcallp old)
                              (funcallp new)
                              (renamingp ren))))
  (let ((__function__ 'funcall-renamefun))
    (declare (ignorable __function__))
    (b* (((funcall old) old)
         ((funcall new) new)
         ((okf &)
          (fun-renamefun old.name new.name ren)))
      (expression-list-renamefun old.args new.args ren))))

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

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

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

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

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

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

Theorem: expression-renamefun-of-expression-fix-old

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

Theorem: expression-renamefun-of-expression-fix-new

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

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

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

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

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

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

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

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

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

Theorem: funcall-renamefun-of-funcall-fix-old

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

Theorem: funcall-renamefun-of-funcall-fix-new

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

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