		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Funcall-option-renamefun

Check if two optional function calls are related by function renaming.

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

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

Definitions and Theorems

Function: funcall-option-renamefun

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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