Lemmas about bitwise operations on integers.

Possibly only of archaeological significance.

def Int.div2 : ℤ → ℤ

div2 n = n/2

def Int.bodd : ℤ → Bool

bodd n returns true if n is odd

def Int.bit (b : Bool) : ℤ → ℤ

bit b appends the digit b to the binary representation of its integer input.

def Int.testBit : ℤ → ℕ → Bool

testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0

def Int.natBitwise (f : Bool → Bool → Bool) (m : ℕ) (n : ℕ) : ℤ

Int.natBitwise is an auxiliary definition for Int.bitwise.

def Int.bitwise (f : Bool → Bool → Bool) : ℤ → ℤ → ℤ

Int.bitwise applies the function f to pairs of bits in the same position in the binary representations of its inputs.

def Int.lnot : ℤ → ℤ

lnot flips all the bits in the binary representation of its input

def Int.lor : ℤ → ℤ → ℤ

lor takes two integers and returns their bitwise or

def Int.land : ℤ → ℤ → ℤ

land takes two integers and returns their bitwise and

def Int.ldiff' : ℤ → ℤ → ℤ

ldiff' a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

def Int.lxor' : ℤ → ℤ → ℤ

lxor' computes the bitwise xor of two natural numbers

instance Int.instShiftLeftInt : ShiftLeft ℤ

m <<< n produces an integer whose binary representation is obtained by left-shifting the binary representation of m by n places

instance Int.instShiftRightInt : ShiftRight ℤ

m >>> n produces an integer whose binary representation is obtained by right-shifting the binary representation of m by n places