		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-ext-declon-list

Validate a list of external declarations.

Signature
(valid-ext-declon-list edecls table ienv) → (mv erp new-edecls new-table)
Arguments: edecls — Guard (ext-declon-listp edecls).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-edecls — Type (ext-declon-listp new-edecls).; new-table — Type (valid-tablep new-table).

We validate them in order, threading the validation table through.

Definitions and Theorems

Function: valid-ext-declon-list

(defun valid-ext-declon-list (edecls table ienv)
  (declare (xargs :guard (and (ext-declon-listp edecls)
                              (valid-tablep table)
                              (ienvp ienv))))
  (declare (xargs :guard (ext-declon-list-unambp edecls)))
  (b* (((reterr) nil (irr-valid-table))
       ((when (endp edecls))
        (retok nil (valid-table-fix table)))
       ((erp new-edecl table)
        (valid-ext-declon (car edecls)
                          table ienv))
       ((erp new-edecls table)
        (valid-ext-declon-list (cdr edecls)
                               table ienv)))
    (retok (cons new-edecl new-edecls)
           table)))

Theorem: maybe-msgp-of-valid-ext-declon-list.erp

(defthm maybe-msgp-of-valid-ext-declon-list.erp
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (valid-ext-declon-list edecls table ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: ext-declon-listp-of-valid-ext-declon-list.new-edecls

(defthm ext-declon-listp-of-valid-ext-declon-list.new-edecls
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (valid-ext-declon-list edecls table ienv)))
    (ext-declon-listp new-edecls))
  :rule-classes :rewrite)

Theorem: valid-tablep-of-valid-ext-declon-list.new-table

(defthm valid-tablep-of-valid-ext-declon-list.new-table
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (valid-ext-declon-list edecls table ienv)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: ext-declon-list-unambp-of-valid-ext-declon-list

(defthm ext-declon-list-unambp-of-valid-ext-declon-list
  (implies (ext-declon-list-unambp edecls)
           (b* (((mv acl2::?erp ?new-edecls ?new-table)
                 (valid-ext-declon-list edecls table ienv)))
             (implies (not erp)
                      (ext-declon-list-unambp new-edecls)))))

Theorem: valid-ext-declon-list-of-ext-declon-list-fix-edecls

(defthm valid-ext-declon-list-of-ext-declon-list-fix-edecls
  (equal (valid-ext-declon-list (ext-declon-list-fix edecls)
                                table ienv)
         (valid-ext-declon-list edecls table ienv)))

Theorem: valid-ext-declon-list-ext-declon-list-equiv-congruence-on-edecls

(defthm
   valid-ext-declon-list-ext-declon-list-equiv-congruence-on-edecls
  (implies (ext-declon-list-equiv edecls edecls-equiv)
           (equal (valid-ext-declon-list edecls table ienv)
                  (valid-ext-declon-list edecls-equiv table ienv)))
  :rule-classes :congruence)

Theorem: valid-ext-declon-list-of-valid-table-fix-table

(defthm valid-ext-declon-list-of-valid-table-fix-table
  (equal (valid-ext-declon-list edecls (valid-table-fix table)
                                ienv)
         (valid-ext-declon-list edecls table ienv)))

Theorem: valid-ext-declon-list-valid-table-equiv-congruence-on-table

(defthm valid-ext-declon-list-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-ext-declon-list edecls table ienv)
                  (valid-ext-declon-list edecls table-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-ext-declon-list-of-ienv-fix-ienv

(defthm valid-ext-declon-list-of-ienv-fix-ienv
  (equal (valid-ext-declon-list edecls table (ienv-fix ienv))
         (valid-ext-declon-list edecls table ienv)))

Theorem: valid-ext-declon-list-ienv-equiv-congruence-on-ienv

(defthm valid-ext-declon-list-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-ext-declon-list edecls table ienv)
                  (valid-ext-declon-list edecls table ienv-equiv)))
  :rule-classes :congruence)