|
|
|---|
|
|
|
|---|
Generate a theorem about the initial scope of a function.
(gen-init-scope-thm params args
parargs arg-types const-new thm-index)
→
(mv thm-event thm-name updated-thm-index)The
The theorem says that, given values of certain types for the arguments, c::init-scope applied to the list of parameter declarations and to the list of parameter values yields an omap (which we express as an omap::update nest) that associates parameter name and argument value.
Function:
(defun gen-init-scope-thm (params args parargs arg-types const-new thm-index) (declare (xargs :guard (and (c::param-declon-listp params) (symbol-listp args) (true-listp arg-types) (symbolp const-new) (posp thm-index)))) (let ((__function__ 'gen-init-scope-thm)) (declare (ignorable __function__)) (b* ((formula (cons 'implies (cons (cons 'and arg-types) (cons (cons 'equal (cons (cons 'c::init-scope (cons (cons 'quote (cons params 'nil)) (cons (cons 'list args) 'nil))) (cons parargs 'nil))) 'nil)))) (hints '(("Goal" :in-theory '(omap::assoc-when-emptyp (:e omap::emptyp) omap::assoc-of-update c::init-scope c::not-flexible-array-member-p-when-ucharp c::not-flexible-array-member-p-when-scharp c::not-flexible-array-member-p-when-ushortp c::not-flexible-array-member-p-when-sshortp c::not-flexible-array-member-p-when-uintp c::not-flexible-array-member-p-when-sintp c::not-flexible-array-member-p-when-ulongp c::not-flexible-array-member-p-when-slongp c::not-flexible-array-member-p-when-ullongp c::not-flexible-array-member-p-when-sllongp c::remove-flexible-array-member-when-absent c::ucharp-alt-def c::scharp-alt-def c::ushortp-alt-def c::sshortp-alt-def c::uintp-alt-def c::sintp-alt-def c::ulongp-alt-def c::slongp-alt-def c::ullongp-alt-def c::sllongp-alt-def c::type-of-value-when-ucharp c::type-of-value-when-scharp c::type-of-value-when-ushortp c::type-of-value-when-sshortp c::type-of-value-when-uintp c::type-of-value-when-sintp c::type-of-value-when-ulongp c::type-of-value-when-slongp c::type-of-value-when-ullongp c::type-of-value-when-sllongp c::value-fix-when-valuep c::value-list-fix-of-cons c::type-of-value c::type-array c::type-pointer c::type-struct (:e c::adjust-type) (:e c::apconvert-type) (:e c::ident) (:e c::param-declon-list-fix$inline) (:e c::param-declon-to-ident+tyname) (:e c::tyname-to-type) (:e c::type-uchar) (:e c::type-schar) (:e c::type-ushort) (:e c::type-sshort) (:e c::type-uint) (:e c::type-sint) (:e c::type-ulong) (:e c::type-slong) (:e c::type-ullong) (:e c::type-sllong) (:e c::value-list-fix$inline) mv-nth car-cons cdr-cons (:e <<) lemma1 lemma2)))) ((mv thm-name thm-index) (gen-thm-name const-new thm-index)) (thm-event (cons 'defruled (cons thm-name (cons formula (cons ':hints (cons hints '(:prep-lemmas ((defruled lemma1 (not (c::errorp nil))) (defruled lemma2 (not (c::errorp (omap::update key val map))) :enable (c::errorp omap::update))))))))))) (mv thm-event thm-name thm-index))))
Theorem:
(defthm pseudo-event-formp-of-gen-init-scope-thm.thm-event (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (gen-init-scope-thm params args parargs arg-types const-new thm-index))) (pseudo-event-formp thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-gen-init-scope-thm.thm-name (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (gen-init-scope-thm params args parargs arg-types const-new thm-index))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-gen-init-scope-thm.updated-thm-index (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (gen-init-scope-thm params args parargs arg-types const-new thm-index))) (posp updated-thm-index)) :rule-classes (:rewrite :type-prescription))