Event to generate the ACL2 models of the C integer operations that involve two integer types.
(def-integer-operations-2 type1 type2) → event
These include all the strict pure binary operators.
For all the operations except shifts, we treat two cases differently: when the two usual arithmetic conversions applied to the operand types yields the same as the two operand types (which must therefore be equal), we generate a definition that performs a direct computation; otherwise, we generate a definition that converts the operands to the common type and then calls the function for that type as operand types. For shift operations, we turn the second operand into an ACL2 integer and then we call the shift function generated by def-integer-operations-1; the result has the promoted type of the first operand.
Function:
(defun def-integer-operations-2 (type1 type2) (declare (xargs :guard (and (typep type1) (typep type2)))) (declare (xargs :guard (and (type-nonchar-integerp type1) (type-nonchar-integerp type2)))) (let ((__function__ 'def-integer-operations-2)) (declare (ignorable __function__)) (b* ((type1-string (integer-type-xdoc-string type1)) (type2-string (integer-type-xdoc-string type2)) (type (uaconvert-types type1 type2)) (samep (and (equal type type1) (equal type type2))) (signedp (type-signed-integerp type)) (ptype1 (promote-type type1)) (<type1> (integer-type-to-fixtype type1)) (<type2> (integer-type-to-fixtype type2)) (<type> (integer-type-to-fixtype type)) (<ptype1> (integer-type-to-fixtype ptype1)) (<type1>p (pack <type1> 'p)) (<type2>p (pack <type2> 'p)) (<type>p (pack <type> 'p)) (<ptype1>p (pack <ptype1> 'p)) (integer-from-<type1> (pack 'integer-from- <type1>)) (integer-from-<type2> (pack 'integer-from- <type2>)) (<type>-from-integer (pack <type> '-from-integer)) (<type>-from-integer-mod (pack <type>-from-integer '-mod)) (<type>-integerp (pack <type> '-integerp)) (<type>-from-<type1> (pack <type> '-from- <type1>)) (<type>-from-<type2> (pack <type> '-from- <type2>)) (add-<type1>-<type2> (pack 'add- <type1> '- <type2>)) (add-<type1>-<type2>-okp (pack add-<type1>-<type2> '-okp)) (add-<type>-<type> (pack 'add- <type> '- <type>)) (add-<type>-<type>-okp (pack add-<type>-<type> '-okp)) (sub-<type1>-<type2> (pack 'sub- <type1> '- <type2>)) (sub-<type1>-<type2>-okp (pack sub-<type1>-<type2> '-okp)) (sub-<type>-<type> (pack 'sub- <type> '- <type>)) (sub-<type>-<type>-okp (pack sub-<type>-<type> '-okp)) (mul-<type1>-<type2> (pack 'mul- <type1> '- <type2>)) (mul-<type1>-<type2>-okp (pack mul-<type1>-<type2> '-okp)) (mul-<type>-<type> (pack 'mul- <type> '- <type>)) (mul-<type>-<type>-okp (pack mul-<type>-<type> '-okp)) (div-<type1>-<type2> (pack 'div- <type1> '- <type2>)) (div-<type1>-<type2>-okp (pack div-<type1>-<type2> '-okp)) (div-<type>-<type> (pack 'div- <type> '- <type>)) (div-<type>-<type>-okp (pack div-<type>-<type> '-okp)) (rem-<type1>-<type2> (pack 'rem- <type1> '- <type2>)) (rem-<type1>-<type2>-okp (pack rem-<type1>-<type2> '-okp)) (rem-<type>-<type> (pack 'rem- <type> '- <type>)) (rem-<type>-<type>-okp (pack rem-<type>-<type> '-okp)) (shl-<type1>-<type2> (pack 'shl- <type1> '- <type2>)) (shl-<type1>-<type2>-okp (pack shl-<type1>-<type2> '-okp)) (shl-<type1> (pack 'shl- <type1>)) (shl-<type1>-okp (pack shl-<type1> '-okp)) (shr-<type1>-<type2> (pack 'shr- <type1> '- <type2>)) (shr-<type1>-<type2>-okp (pack shr-<type1>-<type2> '-okp)) (shr-<type1> (pack 'shr- <type1>)) (shr-<type1>-okp (pack shr-<type1> '-okp)) (lt-<type1>-<type2> (pack 'lt- <type1> '- <type2>)) (lt-<type>-<type> (pack 'lt- <type> '- <type>)) (gt-<type1>-<type2> (pack 'gt- <type1> '- <type2>)) (gt-<type>-<type> (pack 'gt- <type> '- <type>)) (le-<type1>-<type2> (pack 'le- <type1> '- <type2>)) (le-<type>-<type> (pack 'le- <type> '- <type>)) (ge-<type1>-<type2> (pack 'ge- <type1> '- <type2>)) (ge-<type>-<type> (pack 'ge- <type> '- <type>)) (eq-<type1>-<type2> (pack 'eq- <type1> '- <type2>)) (eq-<type>-<type> (pack 'eq- <type> '- <type>)) (ne-<type1>-<type2> (pack 'ne- <type1> '- <type2>)) (ne-<type>-<type> (pack 'ne- <type> '- <type>)) (bitand-<type1>-<type2> (pack 'bitand- <type1> '- <type2>)) (bitand-<type>-<type> (pack 'bitand- <type> '- <type>)) (bitxor-<type1>-<type2> (pack 'bitxor- <type1> '- <type2>)) (bitxor-<type>-<type> (pack 'bitxor- <type> '- <type>)) (bitior-<type1>-<type2> (pack 'bitior- <type1> '- <type2>)) (bitior-<type>-<type> (pack 'bitior- <type> '- <type>))) (cons 'progn (cons '(set-ignore-ok t) (cons '(set-irrelevant-formals-ok t) (append (and signedp (cons (cons 'defun-integer (cons add-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the addition of a value of " type1-string " and a value of " type2-string " is well-defined.") (cons ':body (cons (if samep (cons <type>-integerp (cons (cons '+ (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons add-<type>-<type>-okp (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) 'nil)) (cons (cons 'defun-integer (cons add-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (append (and signedp (cons ':guard (cons (cons add-<type1>-<type2>-okp '(x y)) 'nil))) (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Addition of a value of " type1-string " and a value of " type2-string " [C:6.5.6].") (cons ':body (cons (if samep (cons (if signedp <type>-from-integer <type>-from-integer-mod) (cons (cons '+ (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons add-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and signedp (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons add-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (append (and signedp (cons (cons 'defun-integer (cons sub-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the subtraction of a value of " type1-string " and a value of " type2-string " is well-defined.") (cons ':body (cons (if samep (cons <type>-integerp (cons (cons '- (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons sub-<type>-<type>-okp (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) 'nil)) (cons (cons 'defun-integer (cons sub-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (append (and signedp (cons ':guard (cons (cons sub-<type1>-<type2>-okp '(x y)) 'nil))) (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Subtraction of a value of " type1-string " and a value of " type2-string " [C:6.5.6].") (cons ':body (cons (if samep (cons (if signedp <type>-from-integer <type>-from-integer-mod) (cons (cons '- (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons sub-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and signedp (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons sub-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (append (and signedp (cons (cons 'defun-integer (cons mul-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the multiplication of a value of " type1-string " and a value of " type2-string " is well-defined.") (cons ':body (cons (if samep (cons <type>-integerp (cons (cons '* (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons mul-<type>-<type>-okp (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) 'nil)) (cons (cons 'defun-integer (cons mul-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (append (and signedp (cons ':guard (cons (cons mul-<type1>-<type2>-okp '(x y)) 'nil))) (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Multiplication of a value of " type1-string " and a value of " type2-string " [C:6.5.5].") (cons ':body (cons (if samep (cons (if signedp <type>-from-integer <type>-from-integer-mod) (cons (cons '* (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons mul-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and signedp (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons mul-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (cons (cons 'defun-integer (cons div-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the division of a value of " type1-string " and a value of " type2-string " is well-defined.") (cons ':body (cons (if samep (if signedp (cons 'and (cons (cons 'not (cons (cons 'equal (cons (cons integer-from-<type2> '(y)) '(0))) 'nil)) (cons (cons <type>-integerp (cons (cons 'truncate (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) 'nil))) (cons 'not (cons (cons 'equal (cons (cons integer-from-<type2> '(y)) '(0))) 'nil))) (cons div-<type>-<type>-okp (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons div-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':guard (cons (cons div-<type1>-<type2>-okp '(x y)) (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Division of a value of " type1-string " and a value of " type2-string " [C:6.5.5].") (cons ':body (cons (if samep (cons (if signedp <type>-from-integer <type>-from-integer-mod) (cons (cons 'truncate (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons div-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons div-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (cons (cons 'defun-integer (cons rem-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the remainder of a value of " type1-string " and a value of " type2-string " is well-defined.") (cons ':body (cons (if samep (if signedp (cons 'and (cons (cons 'not (cons (cons 'equal (cons (cons integer-from-<type2> '(y)) '(0))) 'nil)) (cons (cons <type>-integerp (cons (cons 'rem (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) 'nil))) (cons 'not (cons (cons 'equal (cons (cons integer-from-<type2> '(y)) '(0))) 'nil))) (cons rem-<type>-<type>-okp (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons rem-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':guard (cons (cons rem-<type1>-<type2>-okp '(x y)) (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Remainder of a value of " type1-string " and a value of " type2-string " [C:6.5.5].") (cons ':body (cons (if samep (cons (if signedp <type>-from-integer <type>-from-integer-mod) (cons (cons 'rem (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons rem-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons rem-<type1>-<type2>-okp (and (not signedp) (list 'rem)))) 'nil))) 'nil) 'nil)))))))))))))))) (cons (cons 'defun-integer (cons shl-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the left shift of a value of " type1-string " by a value of " type2-string " is well-defined.") (cons ':body (cons (cons shl-<type1>-okp (cons 'x (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)))))))))))) (cons (cons 'defun-integer (cons shl-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':guard (cons (cons shl-<type1>-<type2>-okp '(x y)) (cons ':res-type (cons <ptype1>p (cons ':short (cons (str::cat "Left shift of a value of " type1-string " and a value of " type2-string " [C:6.5.7].") (cons ':body (cons (cons shl-<type1> (cons 'x (cons (cons integer-from-<type2> '(y)) 'nil))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons shl-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (cons (cons 'defun-integer (cons shr-<type1>-<type2>-okp (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'booleanp (cons ':short (cons (str::cat "Check if the right shift of a value of " type1-string " by a value of " type2-string " is well-defined.") (cons ':body (cons (cons shr-<type1>-okp (cons 'x (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)))))))))))) (cons (cons 'defun-integer (cons shr-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':guard (cons (cons shr-<type1>-<type2>-okp '(x y)) (cons ':res-type (cons <ptype1>p (cons ':short (cons (str::cat "Right shift of a value of " type1-string " and a value of " type2-string " [C:6.5.7].") (cons ':body (cons (cons shr-<type1> (cons 'x (cons (cons integer-from-<type2> '(y)) 'nil))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons shr-<type1>-<type2>-okp 'nil)) 'nil))) 'nil) 'nil)))))))))))))))) (cons (cons 'defun-integer (cons lt-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Less-than relation of a value of " type1-string " and a value of " type2-string " [C:6.5.8].") (cons ':body (cons (if samep (cons 'if (cons (cons '< (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons lt-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons gt-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Greater-than relation of a value of " type1-string " and a value of " type2-string " [C:6.5.8].") (cons ':body (cons (if samep (cons 'if (cons (cons '> (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons gt-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons le-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Less-than-or-equal-to relation of a value of " type1-string " and a value of " type2-string " [C:6.5.8].") (cons ':body (cons (if samep (cons 'if (cons (cons '<= (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons le-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons ge-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Greater-than-or-equal-to relation of a value of " type1-string " and a value of " type2-string " [C:6.5.8].") (cons ':body (cons (if samep (cons 'if (cons (cons '>= (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons ge-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons eq-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Equality of a value of " type1-string " and a value of " type2-string " [C:6.5.9].") (cons ':body (cons (if samep (cons 'if (cons (cons '= (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons eq-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons ne-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons 'sintp (cons ':short (cons (str::cat "Non-equality of a value of " type1-string " and a value of " type2-string " [C:6.5.9].") (cons ':body (cons (if samep (cons 'if (cons (cons '/= (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) '((sint-from-integer 1) (sint-from-integer 0)))) (cons ne-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) 'nil)))))))))))) (cons (cons 'defun-integer (cons bitand-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Bitwise conjunction of a value of " type1-string " and a value of " type2-string " [C:6.5.10].") (cons ':body (cons (if samep (cons <type>-from-integer (cons (cons 'logand (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons bitand-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and samep (cons ':prepwork (cons '((local (include-book "ihs/logops-lemmas" :dir :system))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-integerp (cons <type>p (cons integer-from-<type1> 'nil)))) 'nil))) 'nil) 'nil))))))))))))))))) (cons (cons 'defun-integer (cons bitxor-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Bitwise exclusive disjunction of a value of " type1-string " and a value of " type2-string " [C:6.5.11].") (cons ':body (cons (if samep (cons <type>-from-integer (cons (cons 'logxor (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons bitxor-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and samep (cons ':prepwork (cons '((local (include-book "centaur/bitops/ihs-extensions" :dir :system))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-integerp (cons <type>p (cons integer-from-<type1> 'nil)))) 'nil))) 'nil) 'nil))))))))))))))))) (cons (cons 'defun-integer (cons bitior-<type1>-<type2> (cons ':arg1-type (cons <type1>p (cons ':arg2-type (cons <type2>p (cons ':res-type (cons <type>p (cons ':short (cons (str::cat "Bitwise inclusive disjunction of a value of " type1-string " and a value of " type2-string " [C:6.5.12].") (cons ':body (cons (if samep (cons <type>-from-integer (cons (cons 'logior (cons (cons integer-from-<type1> '(x)) (cons (cons integer-from-<type2> '(y)) 'nil))) 'nil)) (cons bitior-<type>-<type> (cons (if (eq <type> <type1>) 'x (cons <type>-from-<type1> '(x))) (cons (if (eq <type> <type2>) 'y (cons <type>-from-<type2> '(y))) 'nil)))) (and samep (cons ':prepwork (cons '((local (include-book "centaur/bitops/ihs-extensions" :dir :system))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons <type>-integerp (cons <type>p (cons integer-from-<type1> 'nil)))) 'nil))) 'nil) 'nil))))))))))))))))) 'nil)))))))))))))))))))))))))))))
Theorem:
(defthm pseudo-event-formp-of-def-integer-operations-2 (b* ((event (def-integer-operations-2 type1 type2))) (pseudo-event-formp event)) :rule-classes :rewrite)