Map an ACL2 function that models a Java primitive binary operation to the corresponding binary operator in the Java abstract syntax.
(atj-jprim-binop-fn-to-jbinop fn) → binop
Function:
(defun atj-jprim-binop-fn-to-jbinop (fn) (declare (xargs :guard (atj-jprim-binop-fn-p fn))) (let ((__function__ 'atj-jprim-binop-fn-to-jbinop)) (declare (ignorable __function__)) (case fn (boolean-and (jbinop-and)) (boolean-xor (jbinop-xor)) (boolean-ior (jbinop-ior)) (boolean-eq (jbinop-eq)) (boolean-neq (jbinop-ne)) (int-add (jbinop-add)) (long-add (jbinop-add)) (int-sub (jbinop-sub)) (long-sub (jbinop-sub)) (int-mul (jbinop-mul)) (long-mul (jbinop-mul)) (int-div (jbinop-div)) (long-div (jbinop-div)) (int-rem (jbinop-rem)) (long-rem (jbinop-rem)) (int-and (jbinop-and)) (long-and (jbinop-and)) (int-xor (jbinop-xor)) (long-xor (jbinop-xor)) (int-ior (jbinop-ior)) (long-ior (jbinop-ior)) (int-eq (jbinop-eq)) (long-eq (jbinop-eq)) (int-neq (jbinop-ne)) (long-neq (jbinop-ne)) (int-less (jbinop-lt)) (long-less (jbinop-lt)) (int-lesseq (jbinop-le)) (long-lesseq (jbinop-le)) (int-great (jbinop-gt)) (long-great (jbinop-gt)) (int-greateq (jbinop-ge)) (long-greateq (jbinop-ge)) (int-int-shiftl (jbinop-shl)) (long-long-shiftl (jbinop-shl)) (long-int-shiftl (jbinop-shl)) (int-long-shiftl (jbinop-shl)) (int-int-shiftr (jbinop-sshr)) (long-long-shiftr (jbinop-sshr)) (long-int-shiftr (jbinop-sshr)) (int-long-shiftr (jbinop-sshr)) (int-int-ushiftr (jbinop-ushr)) (long-long-ushiftr (jbinop-ushr)) (long-int-ushiftr (jbinop-ushr)) (int-long-ushiftr (jbinop-ushr)) (float-add (jbinop-add)) (double-add (jbinop-add)) (float-sub (jbinop-sub)) (double-sub (jbinop-sub)) (float-mul (jbinop-mul)) (double-mul (jbinop-mul)) (float-div (jbinop-div)) (double-div (jbinop-div)) (float-rem (jbinop-rem)) (double-rem (jbinop-rem)) (float-eq (jbinop-eq)) (double-eq (jbinop-eq)) (float-neq (jbinop-ne)) (double-neq (jbinop-ne)) (float-less (jbinop-lt)) (double-less (jbinop-lt)) (float-lesseq (jbinop-le)) (double-lesseq (jbinop-le)) (float-great (jbinop-gt)) (double-great (jbinop-gt)) (float-greateq (jbinop-ge)) (double-greateq (jbinop-ge)) (t (prog2$ (impossible) (ec-call (jbinop-fix :irrelevant)))))))
Theorem:
(defthm jbinopp-of-atj-jprim-binop-fn-to-jbinop (b* ((binop (atj-jprim-binop-fn-to-jbinop fn))) (jbinopp binop)) :rule-classes :rewrite)