Generate the local lemma about the generated measure function that asserts that the value of the measure function is the minimum number of iterations of the argument update functions that turn terminating arguments into values satisfying the exit test.
(defarbrec-gen-measure-fn-min-lemma x1...xn$ test update-names$ measure-name$ k l names-to-avoid wrld) → (mv event name)
This corresponds to the theorem
(implies (and (natp l) (natp k) (>= l k) test<(update*-x1 l x1 ... xn), ..., (update*-xn l x1 ... xn)>) (>= l (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-min-lemma (x1...xn$ test update-names$ measure-name$ k l names-to-avoid wrld) (declare (xargs :guard (and (symbol-listp x1...xn$) (pseudo-termp test) (symbol-listp update-names$) (symbolp measure-name$) (symbolp k) (symbolp l) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'defarbrec-gen-measure-fn-min-lemma)) (declare (ignorable __function__)) (b* ((name (add-suffix measure-name$ "-MIN")) ((mv name &) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (test-of-updates-l (defarbrec-gen-test-of-updates-term x1...xn$ test update-names$ l)) (test-of-updates-l (untranslate test-of-updates-l nil wrld)) (event (cons 'local (cons (cons 'defthm (cons name (cons (cons 'implies (cons (cons 'and (cons (cons 'natp (cons l 'nil)) (cons (cons 'natp (cons k 'nil)) (cons (cons '>= (cons l (cons k 'nil))) (cons test-of-updates-l 'nil))))) (cons (cons '>= (cons 'l (cons (cons measure-name$ (append x1...xn$ (cons k 'nil))) 'nil))) 'nil))) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons measure-name$ '(natp nfix)) 'nil)) (cons ':induct (cons (cons measure-name$ (append x1...xn$ (cons k 'nil))) 'nil))))) 'nil) '(:rule-classes nil)))))) 'nil)))) (mv event name))))