Generate the local lemma about the generated measure function that asserts that the measure function returns a natural number.
(defarbrec-gen-measure-fn-natp-lemma x1...xn$ measure-name$ k names-to-avoid wrld) → (mv event name)
This corresponds to the theorem
(natp (measure x1 ... xn k))
We generate this theorem without rule classes
(instead of a rewrite rule as in the template)
because we do not generate a function corresponding to
Function:
(defun defarbrec-gen-measure-fn-natp-lemma (x1...xn$ measure-name$ k names-to-avoid wrld) (declare (xargs :guard (and (symbol-listp x1...xn$) (symbolp measure-name$) (symbolp k) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'defarbrec-gen-measure-fn-natp-lemma)) (declare (ignorable __function__)) (b* ((name (add-suffix measure-name$ "-NATP")) ((mv name &) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (event (cons 'local (cons (cons 'defthm (cons name (cons (cons 'natp (cons (cons measure-name$ (append x1...xn$ (cons k 'nil))) 'nil)) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons (cons ':type-prescription (cons measure-name$ 'nil)) '((:compound-recognizer natp-compound-recognizer))) 'nil)) 'nil))) 'nil) '(:rule-classes nil)))))) 'nil)))) (mv event name))))