		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-init-table

Initial validation table.

Signature
(valid-init-table filepath &optional externals (next-uid '(uid 0))) → table
Arguments: filepath — Guard (filepathp filepath).; externals — Guard (valid-externalsp externals).; next-uid — Guard (uidp next-uid).
Returns: table — Type (valid-tablep table).

This contains one empty scope (the initial file scope).

Definitions and Theorems

Function: valid-init-table-fn

(defun valid-init-table-fn (filepath externals next-uid)
  (declare (xargs :guard (and (filepathp filepath)
                              (valid-externalsp externals)
                              (uidp next-uid))))
  (make-valid-table :filepath filepath
                    :scopes (list (valid-empty-scope))
                    :externals externals
                    :next-uid next-uid))

Theorem: valid-tablep-of-valid-init-table

(defthm valid-tablep-of-valid-init-table
  (b* ((table (valid-init-table-fn filepath externals next-uid)
))
    (valid-tablep table))
  :rule-classes :rewrite)

Theorem: valid-init-table-fn-of-filepath-fix-filepath

(defthm valid-init-table-fn-of-filepath-fix-filepath
  (equal (valid-init-table-fn (filepath-fix filepath)
                              externals next-uid)
         (valid-init-table-fn filepath externals next-uid)))

Theorem: valid-init-table-fn-filepath-equiv-congruence-on-filepath

(defthm valid-init-table-fn-filepath-equiv-congruence-on-filepath
 (implies
    (filepath-equiv filepath filepath-equiv)
    (equal (valid-init-table-fn filepath externals next-uid)
           (valid-init-table-fn filepath-equiv externals next-uid)))
 :rule-classes :congruence)

Theorem: valid-init-table-fn-of-valid-externals-fix-externals

(defthm valid-init-table-fn-of-valid-externals-fix-externals
  (equal
       (valid-init-table-fn filepath (valid-externals-fix externals)
                            next-uid)
       (valid-init-table-fn filepath externals next-uid)))

Theorem: valid-init-table-fn-valid-externals-equiv-congruence-on-externals

(defthm
  valid-init-table-fn-valid-externals-equiv-congruence-on-externals
 (implies
    (valid-externals-equiv externals externals-equiv)
    (equal (valid-init-table-fn filepath externals next-uid)
           (valid-init-table-fn filepath externals-equiv next-uid)))
 :rule-classes :congruence)

Theorem: valid-init-table-fn-of-uid-fix-next-uid

(defthm valid-init-table-fn-of-uid-fix-next-uid
  (equal (valid-init-table-fn filepath externals (uid-fix next-uid))
         (valid-init-table-fn filepath externals next-uid)))

Theorem: valid-init-table-fn-uid-equiv-congruence-on-next-uid

(defthm valid-init-table-fn-uid-equiv-congruence-on-next-uid
 (implies
    (uid-equiv next-uid next-uid-equiv)
    (equal (valid-init-table-fn filepath externals next-uid)
           (valid-init-table-fn filepath externals next-uid-equiv)))
 :rule-classes :congruence)