		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Expression-option-renamefun

Check if two optional expressions are related by function renaming.

Signature
(expression-option-renamefun old new ren) → _
Arguments: old — Guard (expression-optionp old).; new — Guard (expression-optionp new).; ren — Guard (renamingp ren).
Returns: _ — Type (reserr-optionp _).

Either both expressions must be present or both must be absent. If present, they must be related.

Definitions and Theorems

Function: expression-option-renamefun

(defun expression-option-renamefun (old new ren)
 (declare (xargs :guard (and (expression-optionp old)
                             (expression-optionp new)
                             (renamingp ren))))
 (let ((__function__ 'expression-option-renamefun))
  (declare (ignorable __function__))
  (expression-option-case
   old :none
   (if (expression-option-case new :none)
       nil
     (reserrf (list :mismatch (expression-option-fix old)
                    (expression-option-fix new))))
   :some
   (expression-option-case
       new
       :none (reserrf (list :mismatch (expression-option-fix old)
                            (expression-option-fix new)))
       :some (expression-renamefun (expression-option-some->val old)
                                   (expression-option-some->val new)
                                   ren)))))

Theorem: reserr-optionp-of-expression-option-renamefun

(defthm reserr-optionp-of-expression-option-renamefun
  (b* ((_ (expression-option-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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