		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-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: isodata-gen-thm-instances-to-terms-back

(defmacro isodata-gen-thm-instances-to-terms-back (thm)
 (declare
  (xargs
       :guard (member-eq thm
                         '(forth-image back-of-forth forth-guard))))
 (b* ((name1 (packn (list 'isodata-gen-
                          thm '-instances-to-terms-back)))
      (name1-aux (packn (list name1 '-aux)))
      (name2 (packn (list 'isodata-gen-all-
                          thm '-instances-to-terms-back)))
      (name1-string (str::downcase-string (symbol-name name1)))
      (thm-selector (packn (list 'isodata-isomap-> thm)))
      (thm-string (case thm
                    (forth-image "forthi-image")
                    (back-of-forth "backi-of-forthi")
                    (forth-guard "forthi-guard")
                    (t (impossible)))))
  (cons
   'encapsulate
   (cons
    'nil
    (cons
     (cons
      'define
      (cons
       name1
       (cons
        '((terms pseudo-term-listp)
          (old$ symbolp)
          (arg-isomaps isodata-symbol-isomap-alistp)
          (wrld plist-worldp))
        (cons
         ':guard
         (cons
          '(= (len terms) (len arg-isomaps))
          (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 (isodata-gen-back-of-terms
                                           x1...xn arg-isomaps)))
                   (cons
                        (cons name1-aux
                              '(terms arg-isomaps
                                      x1...xn back-of-x1...xn wrld))
                        'nil)))
                 (cons
                  ':prepwork
                  (cons
                   (cons
                    (cons
                     'define
                     (cons
                      name1-aux
                      (cons
                       '((terms pseudo-term-listp)
                         (arg-isomaps isodata-symbol-isomap-alistp)
                         (x1...xn symbol-listp)
                         (back-of-x1...xn pseudo-term-listp)
                         (wrld plist-worldp))
                       (cons
                        ':guard
                        (cons
                         '(= (len terms) (len arg-isomaps))
                         (cons
                          ':returns
                          (cons
                           '(lemma-instances true-list-listp)
                           (cons
                            ':parents
                            (cons
                             'nil
                             (cons
                              ':verify-guards
                              (cons
                               'nil
                               (cons
                                (cons
                                 'b*
                                 (cons
                                  (cons
                                   '((when (endp terms)) nil)
                                   (cons
                                    '(term (car terms))
                                    (cons
                                     '(isomap (cdar arg-isomaps))
                                     (cons
                                      (cons
                                       thm
                                       (cons
                                        (cons
                                             thm-selector '(isomap))
                                        'nil))
                                      (cons
                                       '(var (isodata-formal-of-forth
                                                  isomap 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-isomaps)
                                                   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-isomaps isodata-symbol-isomap-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-isomaps wrld))
                         'nil))
                       (cons
                        (cons
                         'more-instances
                         (cons
                          (cons
                           name2
                           '((cdr rec-calls) old$ arg-isomaps wrld))
                          'nil))
                        'nil))))))
                  '((append instances more-instances))))
                'nil))))))))))
      'nil))))))