Generate the hints to verify the guards of the new function,
when the function is not recursive,
when
(isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres appcond-thm-names old$ arg-isomaps res-isomaps old-fn-unnorm-name wrld) → hints
This is according to the design notes.
Function:
(defun isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres (appcond-thm-names old$ arg-isomaps res-isomaps old-fn-unnorm-name wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp old-fn-unnorm-name) (plist-worldp wrld)))) (declare (xargs :guard (consp res-isomaps))) (let ((__function__ 'isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres)) (declare (ignorable __function__)) (b* ((oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names))) (instance-guard-thm-old (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn (cons ':guard-theorem (cons old$ 'nil)) old$ arg-isomaps wrld)) (instances-newp-guard (isodata-gen-newp-guard-instances-to-x1...xn arg-isomaps wrld)) (instances-back-guard (isodata-gen-back-guard-instances-to-x1...xn arg-isomaps wrld)) (instances-back-image (isodata-gen-back-image-instances-to-x1...xn arg-isomaps wrld)) (instance-oldp-of-old (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn oldp-of-old old$ arg-isomaps wrld)) (x1...xn (formals old$ wrld)) (old-call (fcons-term old$ x1...xn)) (back-of-x1...xn (isodata-gen-back-of-terms x1...xn arg-isomaps)) (old-call-of-back-x1...xn (subcor-var x1...xn back-of-x1...xn old-call)) (instances-forth-guard-res (if (= (len res-isomaps) 1) (b* ((res-isomap (cdar res-isomaps)) (forth-guard-res (isodata-isomap->forth-guard res-isomap)) (var (isodata-formal-of-forth res-isomap wrld))) (cons (cons ':instance (cons forth-guard-res (cons ':extra-bindings-ok (cons (cons var (cons old-call-of-back-x1...xn 'nil)) 'nil)))) 'nil)) (isodata-gen-forth-guard-instances-to-mv-nth old-call-of-back-x1...xn res-isomaps wrld))) (instance-old-fn-unnorm-name (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn old-fn-unnorm-name old$ arg-isomaps wrld))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons instance-guard-thm-old (append instances-newp-guard (append instances-back-guard (append instances-back-image (cons instance-oldp-of-old (append instances-forth-guard-res (cons instance-old-fn-unnorm-name 'nil))))))) 'nil))))) 'nil))))
Theorem:
(defthm true-listp-of-isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres (b* ((hints (isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres appcond-thm-names old$ arg-isomaps res-isomaps old-fn-unnorm-name wrld))) (true-listp hints)) :rule-classes :rewrite)