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