Generate the theorems to rewrite exec-expr-asg
with a
(atc-gen-tag-member-write-all-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld) → (mv local-events member-write-thms updated-names-to-avoid)
This relies on
Function:
(defun atc-gen-tag-member-write-all-thms (tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld) (declare (xargs :guard (and (identp tag) (symbolp recognizer) (symbolp fixer-recognizer-thm) (symbolp valuep-thm) (symbolp value-kind-thm) (defstruct-member-info-listp meminfos) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-tag-member-write-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-write-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm (car meminfos) names-to-avoid wrld)) ((mv more-events more-thms names-to-avoid) (atc-gen-tag-member-write-all-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-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-write-all-thms.local-events (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-all-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld))) (pseudo-event-form-listp local-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-write-all-thms.member-write-thms (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-all-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld))) (symbol-listp member-write-thms)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-tag-member-write-all-thms.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?local-events ?member-write-thms ?updated-names-to-avoid) (atc-gen-tag-member-write-all-thms tag recognizer fixer-recognizer-thm valuep-thm value-kind-thm meminfos names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)