		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-thm-instances-to-x1...xn

Generate a function to generate certain kinds of lemma instances.

The function generated by this macro generates a list of lemma instances of the form ((:instance thm1 (var1 x1)) ... (:instance thmn (varn xn))), where each thmi is one of forthi-image, backi-image, backi-of-forthi, newpi-guard, forthi-guard, and backi-guard, and where vari is the formal parameter of (respectively) forthi, backi, forthi, newpi, forthi, and backi. The choice of the thmi theorems is the input of the macro, from which the choice of the vari variables is derived.

Macro: expdata-gen-thm-instances-to-x1...xn

(defmacro expdata-gen-thm-instances-to-x1...xn (thm)
 (declare
  (xargs
      :guard
      (member-eq thm
                 '(forth-image back-image back-of-forth
                               newp-guard forth-guard back-guard))))
 (b* ((name (packn (list 'expdata-gen-
                         thm '-instances-to-x1...xn)))
      (thm-selector (packn (list 'expdata-surjmap-> thm)))
      (thm-string (case thm
                    (forth-image "forthi-image")
                    (back-image "backi-image")
                    (back-of-forth "backi-of-forthi")
                    (newp-guard "newpi-guard")
                    (forth-guard "forthi-guard")
                    (back-guard "backi-guard")
                    (t (impossible))))
      (fn (case thm
            (forth-image 'forth)
            (back-image 'back)
            (back-of-forth 'forth)
            (newp-guard 'newp)
            (forth-guard 'forth)
            (back-guard 'back)
            (t (impossible))))
      (fn-selector (packn (list 'expdata-surjmap-> fn)))
      (fn-string (str::downcase-string (symbol-name fn)))
      (param (packn (list fn '-arg))))
  (cons
   'define
   (cons
    name
    (cons
     '((arg-surjmaps expdata-symbol-surjmap-alistp)
       (wrld plist-worldp))
     (cons
      ':returns
      (cons
       '(lemma-instances true-list-listp)
       (cons
        ':verify-guards
        (cons
         'nil
         (cons
          ':short
          (cons
           (str::cat
            "Generate @('n') lemma instances
                            such that the @('i')-th instance
                            is of theorem @('"
            thm-string
            "')
                            and instantiates
                            the formal parameter of @('"
            fn-string
            "')
                            with @('xi').")
           (cons
            (cons
             'b*
             (cons
              (cons
               '((when (endp arg-surjmaps)) nil)
               (cons
                '(arg (caar arg-surjmaps))
                (cons
                 '(surjmap (cdar arg-surjmaps))
                 (cons
                  (cons thm
                        (cons (cons thm-selector '(surjmap))
                              'nil))
                  (cons
                   (cons
                     param
                     (cons (cons 'expdata-formal-of-unary
                                 (cons (cons fn-selector '(surjmap))
                                       '(wrld)))
                           'nil))
                   (cons
                    (cons
                     'instance
                     (cons
                      (cons
                       'list
                       (cons
                        ':instance
                        (cons
                         thm
                         (cons
                              ':extra-bindings-ok
                              (cons (cons 'list (cons param '(arg)))
                                    'nil)))))
                      'nil))
                    (cons
                     (cons
                        'instances
                        (cons (cons name '((cdr arg-surjmaps) wrld))
                              'nil))
                     'nil)))))))
              '((cons instance instances))))
            'nil))))))))))))