		Search-engine friendly clone of the ACL2 documentation.

No-function-definitions-in-dynamic-semantics

Funscope-nofunp

Check that a function scope has no function definitions in the functions' bodies.

Signature
(funscope-nofunp funscope) → yes/no
Arguments: funscope — Guard (funscopep funscope).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: funscope-nofunp

(defun funscope-nofunp (funscope)
  (declare (xargs :guard (funscopep funscope)))
  (let ((__function__ 'funscope-nofunp))
    (declare (ignorable __function__))
    (or (not (mbt (funscopep funscope)))
        (omap::emptyp funscope)
        (and (b* (((mv & funinfo) (omap::head funscope)))
               (funinfo-nofunp funinfo))
             (funscope-nofunp (omap::tail funscope))))))

Theorem: booleanp-of-funscope-nofunp

(defthm booleanp-of-funscope-nofunp
  (b* ((yes/no (funscope-nofunp funscope)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: funinfo-nofunp-of-cdr-of-in-when-funscope-nofunp

(defthm funinfo-nofunp-of-cdr-of-in-when-funscope-nofunp
  (implies (and (funscopep funscope)
                (funscope-nofunp funscope)
                (consp (omap::assoc fun funscope)))
           (funinfo-nofunp (cdr (omap::assoc fun funscope)))))

Theorem: funscope-nofunp-of-update

(defthm funscope-nofunp-of-update
  (implies (and (funscopep funscope)
                (funscope-nofunp funscope)
                (funinfop funinfo)
                (funinfo-nofunp funinfo))
           (funscope-nofunp (omap::update fun funinfo funscope))))

Theorem: funscope-nofunp-of-funscope-fix-funscope

(defthm funscope-nofunp-of-funscope-fix-funscope
  (equal (funscope-nofunp (funscope-fix funscope))
         (funscope-nofunp funscope)))

Theorem: funscope-nofunp-funscope-equiv-congruence-on-funscope

(defthm funscope-nofunp-funscope-equiv-congruence-on-funscope
  (implies (funscope-equiv funscope funscope-equiv)
           (equal (funscope-nofunp funscope)
                  (funscope-nofunp funscope-equiv)))
  :rule-classes :congruence)