Refactor rule for arithmetic operators.

This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers. This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts. The changes are the following:

• Define a function arith_op_result that, given the two operands and the op computes the result.
• Define a predicate arith_op_sidecond that gives the side conditions for a given op.
• Use the above functions in the rule type_arith_op_int_int, and factor in the rules for / and %.
• Give more precise side conditions for the right and left shift operators (this is the goal of this PR). Note that the standard leaves it as implementation-define what is the result of right-shifting a negative number. I thing we should consider that UB.

Some further factoring of code is possible with the operational semantics, but we can do that as a second step.