		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-init-scope-thm

Generate a theorem about the initial scope of a function.

Signature
(simpadd0-gen-init-scope-thm params args parargs arg-types) → (mv thm-event thm-name)
Arguments: params — Guard (c::param-declon-listp params).; args — Guard (symbol-listp args).; parargs — A term.; arg-types — Guard (true-listp arg-types).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).

The args, parargs, and arg-types inputs are the corresponding outputs of simpadd0-gen-from-params.

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.

The name of the theorem is used locally to another theorem, so it does not have to be particularly distinguished. But we should check and disambiguate this more thoroughly.

Definitions and Theorems

Function: simpadd0-gen-init-scope-thm

(defun simpadd0-gen-init-scope-thm (params args parargs arg-types)
 (declare (xargs :guard (and (c::param-declon-listp params)
                             (symbol-listp args)
                             (true-listp arg-types))))
 (let ((__function__ 'simpadd0-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))))
    (thm-name 'init-scope-thm)
    (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))))

Theorem: pseudo-event-formp-of-simpadd0-gen-init-scope-thm.thm-event

(defthm pseudo-event-formp-of-simpadd0-gen-init-scope-thm.thm-event
 (b* (((mv ?thm-event ?thm-name)
       (simpadd0-gen-init-scope-thm params args parargs arg-types)))
   (pseudo-event-formp thm-event))
 :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-gen-init-scope-thm.thm-name

(defthm symbolp-of-simpadd0-gen-init-scope-thm.thm-name
 (b* (((mv ?thm-event ?thm-name)
       (simpadd0-gen-init-scope-thm params args parargs arg-types)))
   (symbolp thm-name))
 :rule-classes :rewrite)