Theorem generated by atj-main-function-type for the/an output of an ACL2 function.
(atj-main-function-type-output-theorem fn guard formals result out-type hints wrld) → event
The
The theorem states that, under the guard, the result of the function (applied to its formals) satisfies the predicate that corresponds to the specified 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-main-function-type-output-theorem (fn guard formals result out-type hints wrld) (declare (xargs :guard (and (symbolp fn) (pseudo-termp guard) (symbol-listp formals) (maybe-natp result) (atj-typep out-type) (true-listp hints) (plist-worldp wrld)))) (let ((__function__ 'atj-main-function-type-output-theorem)) (declare (ignorable __function__)) (b* ((thm-name (if result (packn-pos (list 'atj- fn '-output- result '- (atj-type-to-keyword out-type)) (pkg-witness (symbol-package-name fn))) (packn-pos (list 'atj- fn '-output- (atj-type-to-keyword out-type)) (pkg-witness (symbol-package-name fn))))) (fn-result (if result (cons 'mv-nth (cons result (cons (cons fn formals) 'nil))) (cons fn formals))) (thm-formula (implicate guard (cons (atj-type-to-pred out-type) (cons fn-result 'nil))))) (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)))))