		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-numrange-events

Generate the function and theorem for a numeric range.

Signature
(deftreeops-gen-numrange-events range info prefix print) → (mv get-nat-fn-events bounds-thm-events event-alist)
Arguments: range — Guard (num-range-p range).; info — Guard (deftreeops-numrange-infop info).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).
Returns: get-nat-fn-events — The function <prefix>-%<b><min>-<max>-nat described in deftreeops.
Type (pseudo-event-form-listp get-nat-fn-events).; bounds-thm-events — The theorem <prefix>-%<b><min>-<max>-nat-bounds described in deftreeops.
Type (pseudo-event-form-listp bounds-thm-events).; event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-numrange-events

(defun deftreeops-gen-numrange-events (range info prefix print)
 (declare (xargs :guard (and (num-range-p range)
                             (deftreeops-numrange-infop info)
                             (common-lisp::symbolp prefix)
                             (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-numrange-events))
  (declare (ignorable __function__))
  (b*
   (((num-range range) range)
    ((deftreeops-numrange-info info) info)
    (matchp (deftreeops-match-pred prefix))
    (matchp$ (packn-pos (list matchp "$") matchp))
    (range-desc
        (pretty-print-num-val-range range.min range.max range.base))
    (get-nat-fn-event
     (cons
      'define
      (cons
       info.get-nat-fn
       (cons
        '((cst treep))
        (cons
         ':guard
         (cons
          (cons matchp
                (cons 'cst (cons range-desc 'nil)))
          (cons
           ':returns
           (cons
            (cons
             'nat
             (cons
              'natp
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                     'quote
                     (cons (cons info.get-nat-fn '(lnfix nfix natp))
                           'nil))
                    'nil)))
                 'nil)
                'nil))))
            (cons
             '(lnfix (nth 0 (tree-leafterm->get cst)))
             (cons
              ':guard-hints
              (cons
               (cons
                (cons
                 '"Goal"
                 (cons
                  ':in-theory
                  (cons
                   (cons
                    'quote
                    (cons
                        (cons matchp$
                              '(tree-match-element-p
                                    tree-match-num-val-p
                                    nat-listp-of-tree-leafterm->get
                                    acl2::natp-of-nth-when-nat-listp
                                    (:e element-kind)
                                    (:e element-num-val->get)
                                    (:e num-val-kind)
                                    (:e num-val-range->max)
                                    (:e num-val-range->min)
                                    (:e nfix)
                                    (:t tree-leafterm->get)))
                        'nil))
                   'nil)))
                'nil)
               (cons
                '///
                (cons
                 (cons
                  'fty::deffixequiv
                  (cons
                   info.get-nat-fn
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons ':in-theory
                             (cons (cons 'quote
                                         (cons (cons info.get-nat-fn
                                                     '(tree-leafterm->get$inline-of-tree-fix-x))
                                               'nil))
                                   'nil)))
                      'nil)
                     'nil))))
                 'nil)))))))))))))
    (get-nat-fn-events
     (cons
      get-nat-fn-event
      (and
          (evmac-input-print->= print :result)
          (cons (cons 'cw-event
                      (cons '"Function ~x0.~%"
                            (cons (cons 'quote
                                        (cons info.get-nat-fn 'nil))
                                  'nil)))
                'nil))))
    (bounds-thm-event
     (cons
      'defrule
      (cons
       info.bounds-thm
       (cons
        (cons
         'implies
         (cons
          (cons matchp
                (cons 'cst (cons range-desc 'nil)))
          (cons
           (cons
               'and
               (cons (cons '<=
                           (cons range.min
                                 (cons (cons info.get-nat-fn '(cst))
                                       'nil)))
                     (cons (cons '<=
                                 (cons (cons info.get-nat-fn '(cst))
                                       (cons range.max 'nil)))
                           'nil)))
           'nil)))
        (cons
         ':rule-classes
         (cons
          ':linear
          (cons
           ':hints
           (cons
            (cons
             (cons
              '"Goal"
              (cons
               ':in-theory
               (cons
                (cons
                 'quote
                 (cons
                  (cons
                   info.get-nat-fn
                   (cons
                      matchp$
                      '(tree-match-element-p
                            tree-match-num-val-p lnfix nfix
                            nth acl2::integerp-of-car-when-nat-listp
                            nat-listp-of-tree-leafterm->get
                            (:e element-kind)
                            (:e element-num-val->get)
                            (:e num-val-kind)
                            (:e num-val-range->max)
                            (:e num-val-range->min)
                            (:e zp))))
                  'nil))
                'nil)))
             'nil)
            'nil))))))))
    (bounds-thm-events
     (cons
      bounds-thm-event
      (and
          (evmac-input-print->= print :result)
          (cons (cons 'cw-event
                      (cons '"Function ~x0.~%"
                            (cons (cons 'quote
                                        (cons info.bounds-thm 'nil))
                                  'nil)))
                'nil)))))
   (mv get-nat-fn-events bounds-thm-events
       (list (cons info.get-nat-fn get-nat-fn-event)
             (cons info.bounds-thm bounds-thm-event))))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-numrange-events.get-nat-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-numrange-events.get-nat-fn-events
 (b* (((mv ?get-nat-fn-events
           ?bounds-thm-events ?event-alist)
       (deftreeops-gen-numrange-events range info prefix print)))
   (pseudo-event-form-listp get-nat-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-numrange-events.bounds-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-numrange-events.bounds-thm-events
 (b* (((mv ?get-nat-fn-events
           ?bounds-thm-events ?event-alist)
       (deftreeops-gen-numrange-events range info prefix print)))
   (pseudo-event-form-listp bounds-thm-events))
 :rule-classes :rewrite)

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

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-numrange-events.event-alist
 (b* (((mv ?get-nat-fn-events
           ?bounds-thm-events ?event-alist)
       (deftreeops-gen-numrange-events range info prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)