		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-thm-instances-to-terms-back

Generate functions to generate certain kinds of lemma instances.

The first function generated by this macro generates a list of lemma instances of the form ((:instance thm1 (var1 bterm1)) ... (:instance thmn (varn btermn))), where each thmi is one of forthi-image, backi-of-forthi, and forthi-guard, where vari is the formal parameter of forthi, and where btermi is obtained by replacing x1, ..., xn with (back1 x1), ..., (backn xn) in a term termi that is part of a list of terms term1, ..., termn supplied as input to the function. The choice of the thmi theorems is in the input of the macro, from which the choice of the vari variables is derived.

The second function generated by this macro calls the first function once for each recursively call of old. Each such call of the first function is passed, as the terms argument, the arguments of the corresponding recursive call of old. Each call of the first function generates n lemma instances, thus if there are r recursive calls a total of r * n lemma instances are generated, which are all concatenated together in one list and returned by the second function generated by this macro.

Macro: expdata-gen-thm-instances-to-terms-back

(defmacro expdata-gen-thm-instances-to-terms-back (thm)
 (declare
  (xargs
       :guard (member-eq thm
                         '(forth-image back-of-forth forth-guard))))
 (b* ((name1 (packn (list 'expdata-gen-
                          thm '-instances-to-terms-back)))
      (name1-aux (packn (list name1 '-aux)))
      (name2 (packn (list 'expdata-gen-all-
                          thm '-instances-to-terms-back)))
      (name1-string (str::downcase-string (symbol-name name1)))
      (thm-selector (packn (list 'expdata-surjmap-> thm)))
      (thm-string (case thm
                    (forth-image "forthi-image")
                    (back-of-forth "backi-of-forthi")
                    (forth-guard "forthi-guard")
                    (t (impossible)))))
  (cons
   'progn
   (cons
    (cons
     'define
     (cons
      name1
      (cons
       '((terms pseudo-term-listp)
         (old$ symbolp)
         (arg-surjmaps expdata-symbol-surjmap-alistp)
         (wrld plist-worldp))
       (cons
        ':guard
        (cons
         '(= (len terms) (len arg-surjmaps))
         (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 @('forthi')
                              with a given term @('termi') in which
                              @('x1'), ..., @('xn') are replaced with
                              @('(back1 x1)'), ..., @('(backn xn)').")
               (cons
                (cons
                 'b*
                 (cons
                  '((x1...xn (formals old$ wrld))
                    (back-of-x1...xn (expdata-gen-back-of-terms
                                          x1...xn arg-surjmaps)))
                  (cons (cons name1-aux
                              '(terms arg-surjmaps
                                      x1...xn back-of-x1...xn wrld))
                        'nil)))
                (cons
                 ':prepwork
                 (cons
                  (cons
                   (cons
                    'define
                    (cons
                     name1-aux
                     (cons
                      '((terms pseudo-term-listp)
                        (arg-surjmaps expdata-symbol-surjmap-alistp)
                        (x1...xn symbol-listp)
                        (back-of-x1...xn pseudo-term-listp)
                        (wrld plist-worldp))
                      (cons
                       ':guard
                       (cons
                        '(= (len terms) (len arg-surjmaps))
                        (cons
                         ':returns
                         (cons
                          '(lemma-instances true-list-listp)
                          (cons
                           ':verify-guards
                           (cons
                            'nil
                            (cons
                             (cons
                              'b*
                              (cons
                               (cons
                                '((when (endp terms)) nil)
                                (cons
                                 '(term (car terms))
                                 (cons
                                  '(surjmap (cdar arg-surjmaps))
                                  (cons
                                   (cons
                                    thm
                                    (cons
                                      (cons thm-selector '(surjmap))
                                      'nil))
                                   (cons
                                    '(var (expdata-formal-of-forth
                                               surjmap wrld))
                                    (cons
                                     '(term-with-back
                                         (subcor-var
                                              x1...xn
                                              back-of-x1...xn term))
                                     (cons
                                      (cons
                                       'instance
                                       (cons
                                        (cons
                                         'list
                                         (cons
                                          ':instance
                                          (cons
                                           thm
                                           '(:extra-bindings-ok
                                             (list
                                                 var
                                                 term-with-back)))))
                                        'nil))
                                      (cons
                                       (cons
                                        'instances
                                        (cons
                                         (cons
                                            name1-aux
                                            '((cdr terms)
                                              (cdr arg-surjmaps)
                                              x1...xn
                                              back-of-x1...xn wrld))
                                         'nil))
                                       'nil))))))))
                               '((cons instance instances))))
                             'nil))))))))))
                   'nil)
                  'nil))))))))))))))
    (cons
     (cons
      'define
      (cons
       name2
       (cons
        '((rec-calls pseudo-tests-and-call-listp)
          (old$ symbolp)
          (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 the concatenation of
                              all the @('n * r') lemma instances generated by
                              @('"
               name1-string
               "')
                              for all the recursive call arguments of @('old')
                              passed as the @('terms') input.")
              (cons
               (cons
                'b*
                (cons
                 (cons
                  '((when (endp rec-calls)) nil)
                  (cons
                   '(tests-and-call (car rec-calls))
                   (cons
                    '(rec-call
                       (access tests-and-call tests-and-call :call))
                    (cons
                     '(updates (fargs rec-call))
                     (cons
                      (cons
                       'instances
                       (cons
                        (cons
                            name1 '(updates old$ arg-surjmaps wrld))
                        'nil))
                      (cons
                        (cons 'more-instances
                              (cons (cons name2
                                          '((cdr rec-calls)
                                            old$ arg-surjmaps wrld))
                                    'nil))
                        'nil))))))
                 '((append instances more-instances))))
               'nil))))))))))
     'nil)))))