Theorem generated by atj-other-function-type for the/an output of an ACL2 function.
(atj-other-function-type-theorem fn guard formals in-types result out-type hints wrld) → event
The
The theorem states that if the formal parameters satisfy both the function's guard and the predicates that correspond to the input types, then the result of the function (applied to its formal parameters) satisfies the predicate that corresponds to the output type.
The theorem has no rule classes because its only purpose is to make sure that its formula holds. The theorem is local (to the encapsulate generated by the macro) for the same reason.
Function:
(defun atj-other-function-type-theorem-aux (formals in-types) (declare (xargs :guard (and (symbol-listp formals) (atj-type-listp in-types)))) (declare (xargs :guard (= (len formals) (len in-types)))) (let ((__function__ 'atj-other-function-type-theorem-aux)) (declare (ignorable __function__)) (cond ((endp formals) nil) (t (cons (cons (atj-type-to-pred (car in-types)) (cons (car formals) 'nil)) (atj-other-function-type-theorem-aux (cdr formals) (cdr in-types)))))))
Theorem:
(defthm pseudo-term-listp-of-atj-other-function-type-theorem-aux (implies (and (symbol-listp formals) (atj-type-listp in-types) (= (len formals) (len in-types))) (b* ((terms (atj-other-function-type-theorem-aux formals in-types))) (pseudo-term-listp terms))) :rule-classes :rewrite)
Function:
(defun atj-other-function-type-theorem (fn guard formals in-types result out-type hints wrld) (declare (xargs :guard (and (symbolp fn) (pseudo-termp guard) (symbol-listp formals) (atj-type-listp in-types) (maybe-natp result) (atj-typep out-type) (true-listp hints) (plist-worldp wrld)))) (declare (xargs :guard (= (len formals) (len in-types)))) (let ((__function__ 'atj-other-function-type-theorem)) (declare (ignorable __function__)) (b* ((thm-name (if result (packn-pos (list 'atj- fn '-other-type- result '- (atj-type-to-keyword out-type)) (pkg-witness (symbol-package-name fn))) (packn-pos (list 'atj- fn '-other-type) (pkg-witness (symbol-package-name fn))))) (type-hyps (atj-other-function-type-theorem-aux formals in-types)) (fn-result (if result (cons 'mv-nth (cons result (cons (cons fn formals) 'nil))) (cons fn formals))) (concl (cons (atj-type-to-pred out-type) (cons fn-result 'nil))) (thm-formula (implicate (conjoin (cons guard type-hyps)) concl))) (cons 'local (cons (cons 'defthm (cons thm-name (cons (untranslate thm-formula t wrld) (cons ':rule-classes (cons 'nil (cons ':hints (cons hints 'nil))))))) 'nil)))))