Macros to formalize more concisely ACL2 functions over the Java primitive values.

The ACL2 functions that formalize Java primitive operations and conversions
have the following structure:
they take one (if unary) or two (if binary) primitive values as arguments;
they use primitive value destructors (e.g. `int-value->int`)
to obtain the ``core'' values to operate upon with existing ACL2 functions;
they use existing ACL2 functions to generate the ``core'' result;
they uses primitive value constructors (e.g. `int-value`)
to return the result primitive value.

The only ``interesting'' part is how the core result is calculated from the core arguments via existing ACL2 functions. The rest is boilerplate that can be automatically generated, which we do via macros.

We introduce two general macros: one for unary functions, and one for binary functions. These can generate functions over primitive values of any combination of operand and result types, which are all explicitly specified. Since certain combinations of operand and result types are shared by certain collections of primitive operations, we also introduce more specialized macros for these combinations.

These macros also provide options to generate certain kinds of theorems about the operations, e.g. commutativity theorems.

- Def-primitive-binary
- Macro to formalize a binary ACL2 function over Java primitive values.
- Def-primitive-unary
- Macro to formalize a unary ACL2 function over Java primitive values.
- Primitive-type-destructor
- The destructor of the fixtype of the values of a primitive type.
- Primitive-type-predicate
- The recognizer of the fixtype of the values of a primitive type.
- Primitive-type-constructor
- The constructor of the fixtype of the values of a primitive type.
- Def-long=>boolean-binary
- Specialization of
`def-primitive-binary`to the case in which the input types arelong and the output type isboolean . - Def-int=>boolean-binary
- Specialization of
`def-primitive-binary`to the case in which the input types areint and the output type isboolean . - Def-int-binary
- Specialization of
`def-primitive-binary`to the case in which input and output types areint . - Def-float=>boolean-binary
- Specialization of
`def-primitive-binary`to the case in which the input types arefloat and the output type isboolean . - Def-double=>boolean-binary
- Specialization of
`def-primitive-binary`to the case in which the input types aredouble and the output type isboolean . - Def-long-binary
- Specialization of
`def-primitive-binary`to the case in which input and output types arelong . - Def-float-binary
- Specialization of
`def-primitive-binary`to the case in which input and output types arefloat . - Def-double-binary
- Specialization of
`def-primitive-binary`to the case in which input and output types aredouble . - Def-boolean-binary
- Specialization of
`def-primitive-binary`to the case in which input and output types areboolean . - Def-long-unary
- Specialization of
`def-primitive-unary`to the case in which input and output types arelong . - Def-int-unary
- Specialization of
`def-primitive-unary`to the case in which input and output types areint . - Def-float-unary
- Specialization of
`def-primitive-unary`to the case in which input and output types arefloat . - Def-double-unary
- Specialization of
`def-primitive-unary`to the case in which input and output types aredouble . - Def-boolean-unary
- Specialization of
`def-primitive-unary`to the case in which input and output types areboolean .