		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-cfun-fun-env-thm

Generate the theorem saying that looking up a certain C function in the function environment yields the information for that function.

Signature
(atc-gen-cfun-fun-env-thm fn thm-name prog-const finfo init-fun-env-thm) → event
Arguments: fn — Guard (symbolp fn).; thm-name — Guard (symbolp thm-name).; prog-const — Guard (symbolp prog-const).; finfo — Guard (fun-infop finfo).; init-fun-env-thm — Guard (symbolp init-fun-env-thm).
Returns: event — Type (pseudo-event-formp event).

This serves to speed up the proofs when there is a large number of functions involved. A previous version of ATC was generating proofs that were executing function lookups, which worked fine for small C programs, but was slow for larger C programs.

Definitions and Theorems

Function: atc-gen-cfun-fun-env-thm

(defun atc-gen-cfun-fun-env-thm
       (fn thm-name
           prog-const finfo init-fun-env-thm)
 (declare (xargs :guard (and (symbolp fn)
                             (symbolp thm-name)
                             (symbolp prog-const)
                             (fun-infop finfo)
                             (symbolp init-fun-env-thm))))
 (let ((__function__ 'atc-gen-cfun-fun-env-thm))
  (declare (ignorable __function__))
  (b*
   ((fn-name (symbol-name fn))
    (formula
     (cons
      'equal
      (cons
         (cons 'fun-env-lookup
               (cons (cons 'ident (cons fn-name 'nil))
                     (cons (cons 'init-fun-env
                                 (cons (cons 'preprocess
                                             (cons prog-const 'nil))
                                       'nil))
                           'nil)))
         (cons (cons 'quote (cons finfo 'nil))
               'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons (cons 'quote
                    (cons (cons '(:e fun-env-lookup)
                                (cons '(:e ident)
                                      (cons init-fun-env-thm 'nil)))
                          'nil))
              'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm thm-name
                            :formula formula
                            :hints hints
                            :enable nil)))
   event)))

Theorem: pseudo-event-formp-of-atc-gen-cfun-fun-env-thm

(defthm pseudo-event-formp-of-atc-gen-cfun-fun-env-thm
 (b*
  ((event
      (atc-gen-cfun-fun-env-thm fn thm-name
                                prog-const finfo init-fun-env-thm)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)