		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-add-ord-objfuns-file-scope

Add a list of ordinary identifiers corresponding to objects or functions to the file scope of a validation table.

Signature
(valid-add-ord-objfuns-file-scope idents type linkage defstatus table) → new-table
Arguments: idents — Guard (ident-listp idents).; type — Guard (typep type).; linkage — Guard (linkagep linkage).; defstatus — Guard (valid-defstatusp defstatus).; table — Guard (valid-tablep table).
Returns: new-table — Type (valid-tablep new-table).

See valid-add-ord-file-scope.

Definitions and Theorems

Function: valid-add-ord-objfuns-file-scope

(defun valid-add-ord-objfuns-file-scope
       (idents type linkage defstatus table)
  (declare (xargs :guard (and (ident-listp idents)
                              (typep type)
                              (linkagep linkage)
                              (valid-defstatusp defstatus)
                              (valid-tablep table))))
  (b* (((when (endp idents))
        (valid-table-fix table))
       ((mv uid table)
        (valid-get-fresh-uid (first idents)
                             linkage table)))
    (valid-add-ord-objfuns-file-scope
         (rest idents)
         type linkage defstatus
         (valid-add-ord-file-scope
              (first idents)
              (make-valid-ord-info-objfun :type type
                                          :linkage linkage
                                          :defstatus defstatus
                                          :uid uid)
              table))))

Theorem: valid-tablep-of-valid-add-ord-objfuns-file-scope

(defthm valid-tablep-of-valid-add-ord-objfuns-file-scope
  (b* ((new-table (valid-add-ord-objfuns-file-scope
                       idents type linkage defstatus table)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: valid-add-ord-objfuns-file-scope-of-ident-list-fix-idents

(defthm valid-add-ord-objfuns-file-scope-of-ident-list-fix-idents
 (equal
     (valid-add-ord-objfuns-file-scope (ident-list-fix idents)
                                       type linkage defstatus table)
     (valid-add-ord-objfuns-file-scope
          idents type linkage defstatus table)))

Theorem: valid-add-ord-objfuns-file-scope-ident-list-equiv-congruence-on-idents

(defthm
 valid-add-ord-objfuns-file-scope-ident-list-equiv-congruence-on-idents
 (implies
  (ident-list-equiv idents idents-equiv)
  (equal
   (valid-add-ord-objfuns-file-scope
        idents type linkage defstatus table)
   (valid-add-ord-objfuns-file-scope idents-equiv
                                     type linkage defstatus table)))
 :rule-classes :congruence)

Theorem: valid-add-ord-objfuns-file-scope-of-type-fix-type

(defthm valid-add-ord-objfuns-file-scope-of-type-fix-type
  (equal (valid-add-ord-objfuns-file-scope idents (type-fix type)
                                           linkage defstatus table)
         (valid-add-ord-objfuns-file-scope
              idents type linkage defstatus table)))

Theorem: valid-add-ord-objfuns-file-scope-type-equiv-congruence-on-type

(defthm
     valid-add-ord-objfuns-file-scope-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (valid-add-ord-objfuns-file-scope
                       idents type linkage defstatus table)
                  (valid-add-ord-objfuns-file-scope
                       idents
                       type-equiv linkage defstatus table)))
  :rule-classes :congruence)

Theorem: valid-add-ord-objfuns-file-scope-of-linkage-fix-linkage

(defthm valid-add-ord-objfuns-file-scope-of-linkage-fix-linkage
  (equal (valid-add-ord-objfuns-file-scope
              idents type (linkage-fix linkage)
              defstatus table)
         (valid-add-ord-objfuns-file-scope
              idents type linkage defstatus table)))

Theorem: valid-add-ord-objfuns-file-scope-linkage-equiv-congruence-on-linkage

(defthm
 valid-add-ord-objfuns-file-scope-linkage-equiv-congruence-on-linkage
 (implies (linkage-equiv linkage linkage-equiv)
          (equal (valid-add-ord-objfuns-file-scope
                      idents type linkage defstatus table)
                 (valid-add-ord-objfuns-file-scope
                      idents
                      type linkage-equiv defstatus table)))
 :rule-classes :congruence)

Theorem: valid-add-ord-objfuns-file-scope-of-valid-defstatus-fix-defstatus

(defthm
  valid-add-ord-objfuns-file-scope-of-valid-defstatus-fix-defstatus
  (equal (valid-add-ord-objfuns-file-scope
              idents type
              linkage (valid-defstatus-fix defstatus)
              table)
         (valid-add-ord-objfuns-file-scope
              idents type linkage defstatus table)))

Theorem: valid-add-ord-objfuns-file-scope-valid-defstatus-equiv-congruence-on-defstatus

(defthm
 valid-add-ord-objfuns-file-scope-valid-defstatus-equiv-congruence-on-defstatus
 (implies (valid-defstatus-equiv defstatus defstatus-equiv)
          (equal (valid-add-ord-objfuns-file-scope
                      idents type linkage defstatus table)
                 (valid-add-ord-objfuns-file-scope
                      idents
                      type linkage defstatus-equiv table)))
 :rule-classes :congruence)

Theorem: valid-add-ord-objfuns-file-scope-of-valid-table-fix-table

(defthm valid-add-ord-objfuns-file-scope-of-valid-table-fix-table
  (equal (valid-add-ord-objfuns-file-scope
              idents type linkage
              defstatus (valid-table-fix table))
         (valid-add-ord-objfuns-file-scope
              idents type linkage defstatus table)))

Theorem: valid-add-ord-objfuns-file-scope-valid-table-equiv-congruence-on-table

(defthm
 valid-add-ord-objfuns-file-scope-valid-table-equiv-congruence-on-table
 (implies (valid-table-equiv table table-equiv)
          (equal (valid-add-ord-objfuns-file-scope
                      idents type linkage defstatus table)
                 (valid-add-ord-objfuns-file-scope
                      idents
                      type linkage defstatus table-equiv)))
 :rule-classes :congruence)