		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rep-events

Generate the functions and theorems for a repetition in a concatenation in the alternation that defines a rule name.

Signature
(deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix print) → (mv matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist)
Arguments: rep — Guard (repetitionp rep).; info — Guard (deftreeops-rep-infop info).; i — Index of the concatenation that this repetition is part of.
Guard (posp i).; get-tree-list-list-fn — The function <prefix>-<rulename>-conc or <prefix>-<rulename>-conc<i> described in deftreeops.
Guard (common-lisp::symbolp get-tree-list-list-fn).; get-tree-list-list-fn-match-thm — The theorem saying that get-tree-list-list-fn) matches the concatenation.
Guard (common-lisp::symbolp get-tree-list-list-fn-match-thm).; conc-matching-thm — Guard (common-lisp::symbolp conc-matching-thm).; check-conc-fn — Guard (common-lisp::symbolp check-conc-fn).; rulename — Guard (rulenamep rulename).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).
Returns: matching-thm-events — Type (pseudo-event-form-listp matching-thm-events).; get-tree-list-fn-events — Type (pseudo-event-form-listp get-tree-list-fn-events).; get-tree-fn-events — Type (pseudo-event-form-listp get-tree-fn-events).; event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-rep-events

(defun deftreeops-gen-rep-events
       (rep info i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)
 (declare
  (xargs :guard
         (and (repetitionp rep)
              (deftreeops-rep-infop info)
              (posp i)
              (common-lisp::symbolp get-tree-list-list-fn)
              (common-lisp::symbolp get-tree-list-list-fn-match-thm)
              (common-lisp::symbolp conc-matching-thm)
              (common-lisp::symbolp check-conc-fn)
              (rulenamep rulename)
              (common-lisp::symbolp prefix)
              (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-rep-events))
  (declare (ignorable __function__))
  (b*
   (((deftreeops-rep-info info) info)
    (matchp (deftreeops-match-pred prefix))
    (rep-matchp (deftreeops-rep-match-pred prefix))
    (rulename-string (rulename->get rulename))
    (elem (repetition->element rep))
    (matching-thm-event?
     (and
      info.matching-thm
      (cons
       (cons
        'defruled
        (cons
         info.matching-thm
         (cons
          (cons
           'implies
           (cons
            (cons rep-matchp
                  (cons 'csts
                        (cons (pretty-print-repetition rep)
                              'nil)))
            (cons
             (cons
              'and
              (cons
                 '(equal (len csts) 1)
                 (cons (cons matchp
                             (cons '(nth 0 csts)
                                   (cons (pretty-print-element elem)
                                         'nil)))
                       'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               rep-matchp
               (cons
                matchp
                '(tree-list-match-repetition-p-of-1-repetition
                  tree-terminatedp-of-car-when-tree-list-terminatedp
                  (:e nati-finite)
                  (:e repeat-range)
                  (:e repetition->element)
                  (:e repetition->range)
                  nth (:e zp)
                  len)))
              'nil))
            'nil)))))
       'nil)))
    (matching-thm-events
     (and
      matching-thm-event?
      (append
       matching-thm-event?
       (and
        (evmac-input-print->= print :result)
        (cons (cons 'cw-event
                    (cons '"Theorem ~x0.~%"
                          (cons (cons 'quote
                                      (cons info.matching-thm 'nil))
                                'nil)))
              'nil)))))
    (get-tree-list-fn-match-thm
         (packn-pos (list info.get-tree-list-fn '-match)
                    info.get-tree-list-fn))
    (get-tree-list-fn-event?
     (and
      info.get-tree-list-fn
      (cons
       (cons
        'define
        (cons
         info.get-tree-list-fn
         (cons
          '((cst treep))
          (cons
           ':guard
           (cons
            (if check-conc-fn
             (cons
                'and
                (cons (cons matchp
                            (cons 'cst (cons rulename-string 'nil)))
                      (cons (cons 'equal
                                  (cons (cons check-conc-fn '(cst))
                                        (cons i 'nil)))
                            'nil)))
             (cons matchp
                   (cons 'cst
                         (cons rulename-string 'nil))))
            (cons
             ':returns
             (cons
              (cons
               'csts
               (cons
                'tree-listp
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons
                       'quote
                       (cons
                         (cons info.get-tree-list-fn
                               '(return-type-of-tree-list-fix.newx))
                         'nil))
                      'nil)))
                   'nil)
                  'nil))))
              (cons
               (cons
                'tree-list-fix
                (cons
                 (cons
                     'nth
                     (cons '0
                           (cons (cons get-tree-list-list-fn '(cst))
                                 'nil)))
                 'nil))
               (cons
                ':prepwork
                (cons
                 '((local (in-theory nil)))
                 (cons
                  ':guard-hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                          '(:e elementp)
                          (cons
                           (cons ':t
                                 (cons get-tree-list-list-fn 'nil))
                           (cons
                            'tree-listp-of-nth-when-tree-list-listp
                            (cons
                             (packn-pos (list 'tree-list-listp-of-
                                              get-tree-list-list-fn)
                                        get-tree-list-list-fn)
                             '((:e nfix))))))
                         'nil))
                       (cons
                        ':use
                        (cons
                         (cons
                          get-tree-list-list-fn-match-thm
                          (cons
                           (cons
                            ':instance
                            (cons
                             conc-matching-thm
                             (cons
                              (cons
                               'cstss
                               (cons
                                 (cons get-tree-list-list-fn '(cst))
                                 'nil))
                              'nil)))
                           'nil))
                         'nil)))))
                    'nil)
                   (cons
                    '///
                    (cons
                     (cons
                      'more-returns
                      (cons
                       (cons
                        'csts
                        (cons
                         (cons
                           rep-matchp
                           (cons 'csts
                                 (cons (pretty-print-repetition rep)
                                       'nil)))
                         (cons
                          ':hyp
                          (cons
                           (if check-conc-fn
                            (cons
                             'and
                             (cons
                              (cons
                                 matchp
                                 (cons 'cst
                                       (cons rulename-string 'nil)))
                              (cons
                               (cons
                                   'equal
                                   (cons (cons check-conc-fn '(cst))
                                         (cons i 'nil)))
                               'nil)))
                            (cons
                                matchp
                                (cons 'cst
                                      (cons rulename-string 'nil))))
                           (cons
                            ':name
                            (cons
                             get-tree-list-fn-match-thm
                             (cons
                              ':hints
                              (cons
                               (cons
                                (cons
                                 '"Goal"
                                 (cons
                                  ':in-theory
                                  (cons
                                   (cons
                                    'quote
                                    (cons
                                     (cons
                                      info.get-tree-list-fn
                                      (cons
                                       'tree-list-fix-when-tree-listp
                                       (cons
                                        'tree-listp-of-nth-when-tree-list-listp
                                        (cons
                                         '(:e nfix)
                                         (cons
                                          (packn-pos
                                           (list
                                              'tree-list-listp-of-
                                              get-tree-list-list-fn)
                                           get-tree-list-list-fn)
                                          'nil)))))
                                     'nil))
                                   (cons
                                    ':use
                                    (cons
                                     (cons
                                      (cons
                                       ':instance
                                       (cons
                                        get-tree-list-list-fn-match-thm
                                        '((cst cst))))
                                      (cons
                                       (cons
                                        ':instance
                                        (cons
                                         conc-matching-thm
                                         (cons
                                          (cons
                                           'cstss
                                           (cons
                                            (cons
                                               get-tree-list-list-fn
                                               '(cst))
                                            'nil))
                                          'nil)))
                                       'nil))
                                     'nil)))))
                                'nil)
                               'nil))))))))
                       'nil))
                     (cons
                      (cons
                       'fty::deffixequiv
                       (cons
                        info.get-tree-list-fn
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'quote
                               (cons
                                (cons
                                 info.get-tree-list-fn
                                 (cons
                                    (packn-pos
                                         (list get-tree-list-list-fn
                                               '-of-tree-fix-cst)
                                         get-tree-list-list-fn)
                                    'nil))
                                'nil))
                              'nil)))
                           'nil)
                          'nil))))
                      'nil)))))))))))))))
       'nil)))
    (get-tree-list-fn-events
     (and
      get-tree-list-fn-event?
      (append
       get-tree-list-fn-event?
       (and
        (evmac-input-print->= print :result)
        (cons
          (cons 'cw-event
                (cons '"Function ~x0.~%"
                      (cons (cons 'quote
                                  (cons info.get-tree-list-fn 'nil))
                            'nil)))
          'nil)))))
    (get-tree-fn-event?
     (and
      info.get-tree-fn
      (cons
       (cons
        'define
        (cons
         info.get-tree-fn
         (cons
          '((cst treep))
          (cons
           ':guard
           (cons
            (if check-conc-fn
             (cons
                'and
                (cons (cons matchp
                            (cons 'cst (cons rulename-string 'nil)))
                      (cons (cons 'equal
                                  (cons (cons check-conc-fn '(cst))
                                        (cons i 'nil)))
                            'nil)))
             (cons matchp
                   (cons 'cst
                         (cons rulename-string 'nil))))
            (cons
             ':returns
             (cons
              (cons
               'cst1
               (cons
                'treep
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons
                       'quote
                       (cons (cons info.get-tree-fn
                                   '(return-type-of-tree-fix.new-x))
                             'nil))
                      'nil)))
                   'nil)
                  'nil))))
              (cons
               (cons
                'tree-fix
                (cons
                 (cons
                     'nth
                     (cons '0
                           (cons (cons info.get-tree-list-fn '(cst))
                                 'nil)))
                 'nil))
               (cons
                ':prepwork
                (cons
                 '((local (in-theory nil)))
                 (cons
                  ':guard-hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                          '(:e elementp)
                          (cons
                           (cons ':t
                                 (cons info.get-tree-list-fn 'nil))
                           (cons
                            'treep-of-nth-when-tree-listp
                            (cons
                             (packn-pos (list 'tree-listp-of-
                                              info.get-tree-list-fn)
                                        info.get-tree-list-fn)
                             '((:e nfix))))))
                         'nil))
                       (cons
                        ':use
                        (cons
                         (cons
                          get-tree-list-fn-match-thm
                          (cons
                           (cons
                            ':instance
                            (cons
                             info.matching-thm
                             (cons
                              (cons
                               'csts
                               (cons
                                 (cons info.get-tree-list-fn '(cst))
                                 'nil))
                              'nil)))
                           'nil))
                         'nil)))))
                    'nil)
                   (cons
                    '///
                    (cons
                     (cons
                      'more-returns
                      (cons
                       (cons
                        'cst1
                        (cons
                         (cons
                             matchp
                             (cons 'cst1
                                   (cons (pretty-print-element elem)
                                         'nil)))
                         (cons
                          ':hyp
                          (cons
                           (if check-conc-fn
                            (cons
                             'and
                             (cons
                              (cons
                                 matchp
                                 (cons 'cst
                                       (cons rulename-string 'nil)))
                              (cons
                               (cons
                                   'equal
                                   (cons (cons check-conc-fn '(cst))
                                         (cons i 'nil)))
                               'nil)))
                            (cons
                                matchp
                                (cons 'cst
                                      (cons rulename-string 'nil))))
                           (cons
                            ':name
                            (cons
                             (packn-pos
                                  (list info.get-tree-fn '-match)
                                  info.get-tree-fn)
                             (cons
                              ':hints
                              (cons
                               (cons
                                (cons
                                 '"Goal"
                                 (cons
                                  ':in-theory
                                  (cons
                                   (cons
                                    'quote
                                    (cons
                                     (cons
                                      info.get-tree-fn
                                      (cons
                                       'tree-fix-when-treep
                                       (cons
                                        'treep-of-nth-when-tree-listp
                                        (cons
                                         '(:e nfix)
                                         (cons
                                          (packn-pos
                                           (list
                                              'tree-listp-of-
                                              info.get-tree-list-fn)
                                           info.get-tree-list-fn)
                                          'nil)))))
                                     'nil))
                                   (cons
                                    ':use
                                    (cons
                                     (cons
                                      get-tree-list-fn-match-thm
                                      (cons
                                       (cons
                                        ':instance
                                        (cons
                                         info.matching-thm
                                         (cons
                                          (cons
                                           'csts
                                           (cons
                                            (cons
                                               info.get-tree-list-fn
                                               '(cst))
                                            'nil))
                                          'nil)))
                                       'nil))
                                     'nil)))))
                                'nil)
                               'nil))))))))
                       'nil))
                     (cons
                      (cons
                       'fty::deffixequiv
                       (cons
                        info.get-tree-fn
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'quote
                               (cons
                                (cons
                                 info.get-tree-fn
                                 (cons
                                    (packn-pos
                                         (list info.get-tree-list-fn
                                               '-of-tree-fix-cst)
                                         info.get-tree-list-fn)
                                    'nil))
                                'nil))
                              'nil)))
                           'nil)
                          'nil))))
                      'nil)))))))))))))))
       'nil)))
    (get-tree-fn-events
     (and
      get-tree-fn-event?
      (append
       get-tree-fn-event?
       (and
         (evmac-input-print->= print :result)
         (cons (cons 'cw-event
                     (cons '"Function ~x0.~%"
                           (cons (cons 'quote
                                       (cons info.get-tree-fn 'nil))
                                 'nil)))
               'nil))))))
   (mv matching-thm-events
       get-tree-list-fn-events
       get-tree-fn-events
       (append (and matching-thm-event?
                    (list (cons info.matching-thm
                                (car matching-thm-event?))))
               (and get-tree-list-fn-event?
                    (list (cons info.get-tree-list-fn
                                (car get-tree-list-fn-event?))))
               (and get-tree-fn-event?
                    (list (cons info.get-tree-fn
                                (car get-tree-fn-event?)))))))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-events.matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-events.matching-thm-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-events
            rep info i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-list-fn-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-events
            rep info i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-fn-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-events
            rep info i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-rep-events.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-rep-events.event-alist
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-events
            rep info i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)