Recognize the Java input types generated by ATJ.
(atj-jitypep x) → yes/no
This includes the types for
all the AIJ public class types for ACL2 values
(integers, rationals, numbers,
characters, strings, symbols,
cons pairs, and all values),
the
Function:
(defun atj-jitypep (x) (declare (xargs :guard t)) (let ((__function__ 'atj-jitypep)) (declare (ignorable __function__)) (and (member-equal x (list *aij-type-int* *aij-type-rational* *aij-type-number* *aij-type-char* *aij-type-string* *aij-type-symbol* *aij-type-cons* *aij-type-value* (jtype-class "String") (jtype-boolean) (jtype-char) (jtype-byte) (jtype-short) (jtype-int) (jtype-long) (jtype-float) (jtype-double) (jtype-array (jtype-boolean)) (jtype-array (jtype-char)) (jtype-array (jtype-byte)) (jtype-array (jtype-short)) (jtype-array (jtype-int)) (jtype-array (jtype-long)) (jtype-array (jtype-float)) (jtype-array (jtype-double)))) t)))
Theorem:
(defthm booleanp-of-atj-jitypep (b* ((yes/no (atj-jitypep x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm jtypep-when-atj-jitypep (implies (atj-jitypep x) (jtypep x)))