Generate the theorems to rewrite the execution of certain pure expressions to structure reads, for all the members of a structure type.
(atc-gen-tag-member-read-all-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld) → (mv local-events member-read-thms updated-names-to-avoid)
This relies on
Function:
(defun atc-gen-tag-member-read-all-thms (tag recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld) (declare (xargs :guard (and (identp tag) (symbolp recognizer) (symbolp fixer) (symbolp fixer-recognizer-thm) (symbolp not-error-thm) (defstruct-member-info-listp meminfos) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-tag-member-read-all-thms)) (declare (ignorable __function__)) (b* (((when (endp meminfos)) (mv nil nil names-to-avoid)) ((mv events thms names-to-avoid) (atc-gen-tag-member-read-thms tag recognizer fixer fixer-recognizer-thm not-error-thm (car meminfos) names-to-avoid wrld)) ((mv more-events more-thms names-to-avoid) (atc-gen-tag-member-read-all-thms tag recognizer fixer fixer-recognizer-thm not-error-thm (cdr meminfos) names-to-avoid wrld))) (mv (append events more-events) (append thms more-thms) names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-tag-member-read-all-thms.local-events (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-all-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-read-all-thms.member-read-thms (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-all-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld))) (symbol-listp member-read-thms)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-read-all-thms.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?local-events ?member-read-thms ?updated-names-to-avoid) (atc-gen-tag-member-read-all-thms tag recognizer fixer fixer-recognizer-thm not-error-thm meminfos names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)