		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-push-init-thm

Generate the theorem about the initial computation state of a function execution.

Signature
(atc-gen-push-init-thm fn fn-guard typed-formals prec-tags context-preamble omap-update-nest compst-var names-to-avoid wrld) → (mv thm-event thm-name add-var-nest names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; context-preamble — Guard (true-listp context-preamble).; omap-update-nest — An untranslated term.; compst-var — Guard (symbolp compst-var).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).; add-var-nest — An untranslated term.; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

This theorem says that pushing onto the frame stack a new frame with the initial scope for the function yields a computation state expressed as an add-var nest ended by an add-frame.

We also return that computation state term, since it is used in subsequent theorems.

Definitions and Theorems

Function: atc-gen-push-init-thm

(defun atc-gen-push-init-thm (fn fn-guard typed-formals prec-tags
                                 context-preamble omap-update-nest
                                 compst-var names-to-avoid wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-string-taginfo-alistp prec-tags)
                         (true-listp context-preamble)
                         (symbolp compst-var)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-push-init-thm))
  (declare (ignorable __function__))
  (b*
   ((add-var-nest
         (atc-gen-add-var-formals fn typed-formals compst-var))
    (formals (strip-cars typed-formals))
    (name (pack fn '-push-init))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (formal-thms
         (atc-var-info-list->thm-list (strip-cdrs typed-formals)))
    (formula
     (cons
      'implies
      (cons
       (cons 'and
             (cons (cons 'compustatep
                         (cons compst-var 'nil))
                   (append context-preamble
                           (cons (cons fn-guard formals) 'nil))))
       (cons
        (cons
         'equal
         (cons
          (cons
           'push-frame
           (cons
            (cons
             'make-frame
             (cons
               ':function
               (cons (cons 'ident
                           (cons (symbol-name fn) 'nil))
                     (cons ':scopes
                           (cons (cons 'list
                                       (cons omap-update-nest 'nil))
                                 'nil)))))
            (cons compst-var 'nil)))
          (cons add-var-nest 'nil)))
        'nil))))
    (flexible-thms
         (atc-string-taginfo-alist-to-flexiblep-thms prec-tags))
    (valuep-thms
         (atc-string-taginfo-alist-to-valuep-thms prec-tags))
    (value-kind-thms
         (atc-string-taginfo-alist-to-value-kind-thms prec-tags))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'push-frame-of-one-nonempty-scope
            (cons
             'push-frame-of-one-empty-scope
             (append
              formal-thms
              (cons
               'valuep-when-ucharp
               (cons
                'valuep-when-scharp
                (cons
                 'valuep-when-ushortp
                 (cons
                  'valuep-when-sshortp
                  (cons
                   'valuep-when-uintp
                   (cons
                    'valuep-when-sintp
                    (cons
                     'valuep-when-ulongp
                     (cons
                      'valuep-when-slongp
                      (cons
                       'valuep-when-ullongp
                       (cons
                        'valuep-when-sllongp
                        (append
                         valuep-thms
                         (cons
                          'not-flexible-array-member-p-when-ucharp
                          (cons
                           'not-flexible-array-member-p-when-scharp
                           (cons
                            'not-flexible-array-member-p-when-ushortp
                            (cons
                             'not-flexible-array-member-p-when-sshortp
                             (cons
                              'not-flexible-array-member-p-when-uintp
                              (cons
                               'not-flexible-array-member-p-when-sintp
                               (cons
                                'not-flexible-array-member-p-when-ulongp
                                (cons
                                 'not-flexible-array-member-p-when-slongp
                                 (cons
                                  'not-flexible-array-member-p-when-ullongp
                                  (cons
                                   'not-flexible-array-member-p-when-sllongp
                                   (cons
                                    'not-flexible-array-member-p-when-value-pointer
                                    (cons
                                     'not-flexible-array-member-p-when-value-struct
                                     (append
                                      flexible-thms
                                      (append
                                       value-kind-thms
                                       '(scopep-of-update
                                         (:e scopep)
                                         identp-of-ident)))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv event
       name add-var-nest names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-push-init-thm.thm-event

(defthm pseudo-event-formp-of-atc-gen-push-init-thm.thm-event
  (b* (((mv ?thm-event
            ?thm-name ?add-var-nest ?names-to-avoid)
        (atc-gen-push-init-thm fn fn-guard typed-formals prec-tags
                               context-preamble omap-update-nest
                               compst-var names-to-avoid wrld)))
    (pseudo-event-formp thm-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-push-init-thm.thm-name

(defthm symbolp-of-atc-gen-push-init-thm.thm-name
  (b* (((mv ?thm-event
            ?thm-name ?add-var-nest ?names-to-avoid)
        (atc-gen-push-init-thm fn fn-guard typed-formals prec-tags
                               context-preamble omap-update-nest
                               compst-var names-to-avoid wrld)))
    (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-push-init-thm.names-to-avoid

(defthm symbol-listp-of-atc-gen-push-init-thm.names-to-avoid
 (implies
    (symbol-listp names-to-avoid)
    (b* (((mv ?thm-event
              ?thm-name ?add-var-nest ?names-to-avoid)
          (atc-gen-push-init-thm fn fn-guard typed-formals prec-tags
                                 context-preamble omap-update-nest
                                 compst-var names-to-avoid wrld)))
      (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)