Lemmas about bitwise operations on integers.

Possibly only of archaeological significance.

def Int.div2 : ℤ → ℤ

div2 n = n/2

Equations

• Int.div2 x = match x with | Int.ofNat n => ↑(Nat.div2 n) | Int.negSucc n => Int.negSucc (Nat.div2 n)

def Int.bodd : ℤ → Bool

bodd n returns true if n is odd

Equations

• Int.bodd x = match x with | Int.ofNat n => Nat.bodd n | Int.negSucc n => !Nat.bodd n

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

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

Equations

• Int.bit b = bif b then bit1 else bit0

def Int.testBit : ℤ → ℕ → Bool

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

Equations

• Int.testBit x x = match x, x with | Int.ofNat m, n => Nat.testBit m n | Int.negSucc m, n => !Nat.testBit m n

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

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

Equations

• Int.natBitwise f m n = bif f false false then Int.negSucc (Nat.bitwise' (fun x y => !f x y) m n) else ↑(Nat.bitwise' f m n)

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.

Equations

• One or more equations did not get rendered due to their size.

def Int.lnot : ℤ → ℤ

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

Equations

• Int.lnot x = match x with | Int.ofNat m => Int.negSucc m | Int.negSucc m => ↑m

def Int.lor : ℤ → ℤ → ℤ

lor takes two integers and returns their bitwise or

Equations

• One or more equations did not get rendered due to their size.

def Int.land : ℤ → ℤ → ℤ

land takes two integers and returns their bitwise and

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Int.lxor' : ℤ → ℤ → ℤ

lxor' computes the bitwise xor of two natural numbers

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Int.instShiftRightInt = { shiftRight := fun m n => m <<< (-n) }