		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-variable-multi

Check if a multiple variable declaration is safe.

Signature
(check-safe-variable-multi names init varset funtab) → varset?
Arguments: names — Guard (identifier-listp names).; init — Guard (funcall-optionp init).; varset — Guard (identifier-setp varset).; funtab — Guard (funtablep funtab).
Returns: varset? — Type (identifier-set-resultp varset?).

This is used by check-safe-statement: see that function's documentation for background.

The name of the variables must be identifiers that are not already in the variable table. They must also be distinct and at least two. The expression is checked if present, and it must return the same number of results as the number of variables.

Definitions and Theorems

Function: check-safe-variable-multi

(defun check-safe-variable-multi (names init varset funtab)
  (declare (xargs :guard (and (identifier-listp names)
                              (funcall-optionp init)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-variable-multi))
    (declare (ignorable __function__))
    (b* ((names (identifier-list-fix names))
         (init (funcall-option-fix init))
         ((okf varset-new)
          (add-vars names varset))
         ((unless (>= (len names) 2))
          (reserrf (list :declare-zero-one-var names)))
         ((when (not init)) varset-new)
         ((okf results)
          (check-safe-funcall init varset funtab))
         ((unless (= results (len names)))
          (reserrf (list :declare-multi-var-mismatch
                         names results))))
      varset-new)))

Theorem: identifier-set-resultp-of-check-safe-variable-multi

(defthm identifier-set-resultp-of-check-safe-variable-multi
  (b*
    ((varset? (check-safe-variable-multi names init varset funtab)))
    (identifier-set-resultp varset?))
  :rule-classes :rewrite)

Theorem: check-safe-variable-multi-of-identifier-list-fix-names

(defthm check-safe-variable-multi-of-identifier-list-fix-names
  (equal (check-safe-variable-multi (identifier-list-fix names)
                                    init varset funtab)
         (check-safe-variable-multi names init varset funtab)))

Theorem: check-safe-variable-multi-identifier-list-equiv-congruence-on-names

(defthm
 check-safe-variable-multi-identifier-list-equiv-congruence-on-names
 (implies
   (identifier-list-equiv names names-equiv)
   (equal
        (check-safe-variable-multi names init varset funtab)
        (check-safe-variable-multi names-equiv init varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-multi-of-funcall-option-fix-init

(defthm check-safe-variable-multi-of-funcall-option-fix-init
  (equal (check-safe-variable-multi names (funcall-option-fix init)
                                    varset funtab)
         (check-safe-variable-multi names init varset funtab)))

Theorem: check-safe-variable-multi-funcall-option-equiv-congruence-on-init

(defthm
  check-safe-variable-multi-funcall-option-equiv-congruence-on-init
 (implies
   (funcall-option-equiv init init-equiv)
   (equal
        (check-safe-variable-multi names init varset funtab)
        (check-safe-variable-multi names init-equiv varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-multi-of-identifier-set-fix-varset

(defthm check-safe-variable-multi-of-identifier-set-fix-varset
 (equal
   (check-safe-variable-multi names init (identifier-set-fix varset)
                              funtab)
   (check-safe-variable-multi names init varset funtab)))

Theorem: check-safe-variable-multi-identifier-set-equiv-congruence-on-varset

(defthm
 check-safe-variable-multi-identifier-set-equiv-congruence-on-varset
 (implies
   (identifier-set-equiv varset varset-equiv)
   (equal
        (check-safe-variable-multi names init varset funtab)
        (check-safe-variable-multi names init varset-equiv funtab)))
 :rule-classes :congruence)

Theorem: check-safe-variable-multi-of-funtable-fix-funtab

(defthm check-safe-variable-multi-of-funtable-fix-funtab
  (equal (check-safe-variable-multi
              names init varset (funtable-fix funtab))
         (check-safe-variable-multi names init varset funtab)))

Theorem: check-safe-variable-multi-funtable-equiv-congruence-on-funtab

(defthm
      check-safe-variable-multi-funtable-equiv-congruence-on-funtab
 (implies
   (funtable-equiv funtab funtab-equiv)
   (equal
        (check-safe-variable-multi names init varset funtab)
        (check-safe-variable-multi names init varset funtab-equiv)))
 :rule-classes :congruence)