		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Fun-renamefun

Check if two function names are related by function renaming.

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

We check if the two function names form a pair in the renaming list.

Definitions and Theorems

Function: fun-renamefun

(defun fun-renamefun (old new ren)
  (declare (xargs :guard (and (identifierp old)
                              (identifierp new)
                              (renamingp ren))))
  (let ((__function__ 'fun-renamefun))
    (declare (ignorable __function__))
    (b* ((old (identifier-fix old))
         (new (identifier-fix new)))
      (if (member-equal (cons old new)
                        (renaming->list ren))
          nil
        (reserrf (list :mismatch
                       old new (renaming-fix ren)))))))

Theorem: reserr-optionp-of-fun-renamefun

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

Theorem: fun-renamefun-of-identifier-fix-old

(defthm fun-renamefun-of-identifier-fix-old
  (equal (fun-renamefun (identifier-fix old)
                        new ren)
         (fun-renamefun old new ren)))

Theorem: fun-renamefun-identifier-equiv-congruence-on-old

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

Theorem: fun-renamefun-of-identifier-fix-new

(defthm fun-renamefun-of-identifier-fix-new
  (equal (fun-renamefun old (identifier-fix new)
                        ren)
         (fun-renamefun old new ren)))

Theorem: fun-renamefun-identifier-equiv-congruence-on-new

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

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

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

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

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