An FTY variant of check-mv-let-call.
(fty-check-mv-let-call term) → (mv yes/no mv-var vars indices hides mv-term body-term)
Like many other system utilities, check-mv-let-call is written to use the built-in ACL2 term API. When using this kind of system utilities in code that is written to use the FTY term API, there may be a slight ``mismatch'', e.g. in the way the two APIs fix non-terms, or in the fact that, for termination, the ACL2 API is based on ACL2-count while the FTY API is based on pseudo-term-count.
The mismatch can be often bridged by introducing
simple wrappers of those system utilities
that fix the term (in the FTY way) and then call the wrapped utilities.
This utility,
Note that the retun type theorems readily become unconditional, as is common with fixtypes. In order to prove that the FTY term count decreases, we first prove lemmas saying that, under the assumption pseudo-termp, the results of check-mv-let-call are smaller. Note that, under that assumption, the wrapper and the original utility return the same result (they only possibly differ on non-terms). In proving those lemmas, we need to break the FTY abstraction so that we can reduce the FTY term API operations to the ACL2 term API operations.
Function:
(defun fty-check-mv-let-call (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'fty-check-mv-let-call)) (declare (ignorable __function__)) (check-mv-let-call (pseudo-term-fix term))))
Theorem:
(defthm booleanp-of-fty-check-mv-let-call.yes/no (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-fty-check-mv-let-call.mv-var (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (symbolp mv-var)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-fty-check-mv-let-call.vars (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (symbol-listp vars)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-fty-check-mv-let-call.indices (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (nat-listp indices)) :rule-classes :rewrite)
Theorem:
(defthm boolean-listp-of-fty-check-mv-let-call.hides (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (boolean-listp hides)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-fty-check-mv-let-call.mv-term (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (pseudo-termp mv-term)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-fty-check-mv-let-call.body-term (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (pseudo-termp body-term)) :rule-classes :rewrite)
Theorem:
(defthm len-of-fty-check-mv-let-call.indices/vars (implies (and (pseudo-termp term)) (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (implies yes/no (equal (len indices) (len vars))))))
Theorem:
(defthm len-of-fty-check-mv-let-call.hides/vars (implies (and (pseudo-termp term)) (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (implies yes/no (equal (len hides) (len vars))))))
Theorem:
(defthm pseudo-term-count-of-fty-check-mv-let-call.mv-term (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (implies yes/no (< (pseudo-term-count mv-term) (pseudo-term-count term)))) :rule-classes :linear)
Theorem:
(defthm pseudo-term-count-of-fty-check-mv-let-call.body-term (b* (((mv ?yes/no ?mv-var ?vars ?indices ?hides ?mv-term ?body-term) (fty-check-mv-let-call term))) (implies yes/no (< (pseudo-term-count body-term) (pseudo-term-count term)))) :rule-classes :linear)