		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Add-funs

Add functions to the function environment.

Signature
(add-funs fundefs funenv) → new-funenv
Arguments: fundefs — Guard (fundef-listp fundefs).; funenv — Guard (funenvp funenv).
Returns: new-funenv — Type (funenv-resultp new-funenv).

We create a function scope for the given list of function definitions and we push that onto the function environment. We ensure that the new functions have different names from the functions already in the environment. This ACL2 function is used for all the function definitions in a block; see exec-block.

Definitions and Theorems

Function: add-funs

(defun add-funs (fundefs funenv)
  (declare (xargs :guard (and (fundef-listp fundefs)
                              (funenvp funenv))))
  (let ((__function__ 'add-funs))
    (declare (ignorable __function__))
    (b* (((okf funscope)
          (funscope-for-fundefs fundefs))
         ((okf &)
          (ensure-funscope-disjoint funscope funenv)))
      (cons funscope (funenv-fix funenv)))))

Theorem: funenv-resultp-of-add-funs

(defthm funenv-resultp-of-add-funs
  (b* ((new-funenv (add-funs fundefs funenv)))
    (funenv-resultp new-funenv))
  :rule-classes :rewrite)

Theorem: add-funs-of-no-fundefs

(defthm add-funs-of-no-fundefs
  (equal (add-funs nil funenv)
         (cons nil (funenv-fix funenv))))

Theorem: error-info-wfp-of-add-funs

(defthm error-info-wfp-of-add-funs
  (b* ((?new-funenv (add-funs fundefs funenv)))
    (implies (reserrp new-funenv)
             (error-info-wfp new-funenv))))

Theorem: add-funs-of-fundef-list-fix-fundefs

(defthm add-funs-of-fundef-list-fix-fundefs
  (equal (add-funs (fundef-list-fix fundefs)
                   funenv)
         (add-funs fundefs funenv)))

Theorem: add-funs-fundef-list-equiv-congruence-on-fundefs

(defthm add-funs-fundef-list-equiv-congruence-on-fundefs
  (implies (fundef-list-equiv fundefs fundefs-equiv)
           (equal (add-funs fundefs funenv)
                  (add-funs fundefs-equiv funenv)))
  :rule-classes :congruence)

Theorem: add-funs-of-funenv-fix-funenv

(defthm add-funs-of-funenv-fix-funenv
  (equal (add-funs fundefs (funenv-fix funenv))
         (add-funs fundefs funenv)))

Theorem: add-funs-funenv-equiv-congruence-on-funenv

(defthm add-funs-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (add-funs fundefs funenv)
                  (add-funs fundefs funenv-equiv)))
  :rule-classes :congruence)