		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Funscope-safep

Check the safety of a function scope.

Signature
(funscope-safep funscope funtab) → yes/no
Arguments: funscope — Guard (funscopep funscope).; funtab — Guard (funtablep funtab).
Returns: yes/no — Type (booleanp yes/no).

See funinfo-safep for motivation (i.e. the invariant). This predicate checks the safety of all the values of the omap.

Definitions and Theorems

Function: funscope-safep

(defun funscope-safep (funscope funtab)
  (declare (xargs :guard (and (funscopep funscope)
                              (funtablep funtab))))
  (let ((__function__ 'funscope-safep))
    (declare (ignorable __function__))
    (b* (((when (or (not (mbt (funscopep funscope)))
                    (omap::emptyp funscope)))
          t)
         ((mv & info) (omap::head funscope)))
      (and (funinfo-safep info funtab)
           (funscope-safep (omap::tail funscope)
                           funtab)))))

Theorem: booleanp-of-funscope-safep

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

Theorem: funscope-safep-of-update

(defthm funscope-safep-of-update
  (implies (and (identifierp fun)
                (funinfop funinfo)
                (funscopep funscope)
                (funinfo-safep funinfo funtab)
                (funscope-safep funscope funtab))
           (funscope-safep (omap::update fun funinfo funscope)
                           funtab)))

Theorem: funscope-safep-of-funscope-fix-funscope

(defthm funscope-safep-of-funscope-fix-funscope
  (equal (funscope-safep (funscope-fix funscope)
                         funtab)
         (funscope-safep funscope funtab)))

Theorem: funscope-safep-funscope-equiv-congruence-on-funscope

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

Theorem: funscope-safep-of-funtable-fix-funtab

(defthm funscope-safep-of-funtable-fix-funtab
  (equal (funscope-safep funscope (funtable-fix funtab))
         (funscope-safep funscope funtab)))

Theorem: funscope-safep-funtable-equiv-congruence-on-funtab

(defthm funscope-safep-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (funscope-safep funscope funtab)
                  (funscope-safep funscope funtab-equiv)))
  :rule-classes :congruence)