Generate the function and theorem for a numeric range.
(deftreeops-gen-numrange-events range info prefix) → (mv get-nat-fn-event bounds-thm-event)
Function:
(defun deftreeops-gen-numrange-events (range info prefix) (declare (xargs :guard (and (num-range-p range) (deftreeops-numrange-infop info) (common-lisp::symbolp prefix)))) (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))))))))))))) (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))))))))) (mv get-nat-fn-event bounds-thm-event))))
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-numrange-events.get-nat-fn-event (b* (((mv ?get-nat-fn-event ?bounds-thm-event) (deftreeops-gen-numrange-events range info prefix))) (pseudo-event-formp get-nat-fn-event)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-numrange-events.bounds-thm-event (b* (((mv ?get-nat-fn-event ?bounds-thm-event) (deftreeops-gen-numrange-events range info prefix))) (pseudo-event-formp bounds-thm-event)) :rule-classes :rewrite)