Map an ACL2 function that models a Java primitive unary operation to the corresponding unary operator in the Java abstract syntax.
(atj-jprim-unop-fn-to-junop fn) → unop
Function:
(defun atj-jprim-unop-fn-to-junop (fn) (declare (xargs :guard (atj-jprim-unop-fn-p fn))) (let ((__function__ 'atj-jprim-unop-fn-to-junop)) (declare (ignorable __function__)) (case fn (boolean-not (junop-logcompl)) (int-plus (junop-uplus)) (long-plus (junop-uplus)) (int-minus (junop-uminus)) (long-minus (junop-uminus)) (int-not (junop-bitcompl)) (long-not (junop-bitcompl)) (float-plus (junop-uplus)) (double-plus (junop-uplus)) (float-minus (junop-uminus)) (double-minus (junop-uminus)) (t (prog2$ (impossible) (ec-call (junop-fix :irrelevant)))))))
Theorem:
(defthm junopp-of-atj-jprim-unop-fn-to-junop (b* ((unop (atj-jprim-unop-fn-to-junop fn))) (junopp unop)) :rule-classes :rewrite)