		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 — Guard (true-listp parargs).; 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 int values 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 it directly as an alist) 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 parargs)
                             (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 (cons 'list parargs) 'nil)))
            'nil))))
    (hints
     '(("Goal"
            :in-theory
            '(omap::mapp omap::mfix-when-mapp omap::head
                         omap::tail omap::update omap::assoc
                         omap::mapp-non-nil-implies-not-emptyp
                         (:e omap::emptyp)
                         c::errorp c::init-scope
                         c::not-flexible-array-member-p-when-sintp
                         c::remove-flexible-array-member-when-absent
                         c::sintp-alt-def
                         c::type-of-value-when-sintp
                         c::value-fix-when-valuep
                         c::value-list-fix-of-cons
                         (: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-sint)
                         (:e c::value-list-fix$inline)
                         mv-nth car-cons cdr-cons (:e <<)))))
    (thm-name 'init-scope-thm)
    (thm-event
         (cons 'defruled
               (cons thm-name
                     (cons formula
                           (cons ':hints (cons hints 'nil)))))))
   (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)