Bitwise operations on integers #

Possibly only of archaeological significance.

Recursors #

• Int.bitCasesOn: Parity disjunction. Something is true/defined on ℤ if it's true/defined for even and for odd values.
def Int.div2 :

div2 n = n/2

Equations
• x.div2 = match x with | => n.div2 | => Int.negSucc n.div2
Instances For
def Int.bodd :

bodd n returns true if n is odd

Equations
• x.bodd = match x with | => n.bodd | => !n.bodd
Instances For
def Int.bit (b : Bool) :

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

Equations
• = bif b then bit1 else bit0
Instances For
def Int.testBit :

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

Equations
• x✝.testBit x = match x✝, x with | , n => m.testBit n | , n => !m.testBit n
Instances For
def Int.natBitwise (f : ) (m : ) (n : ) :

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

Equations
Instances For
def Int.bitwise (f : ) :

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.
Instances For
def Int.lnot :

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

Equations
• x.lnot = match x with | => | => m
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
def Int.xor :

xor computes the bitwise xor of two natural numbers

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

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.

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

Equations

bitwise ops #

@[simp]
theorem Int.bodd_zero :
@[simp]
theorem Int.bodd_one :
@[simp]
theorem Int.bodd_coe (n : ) :
(n).bodd = n.bodd
@[simp]
theorem Int.bodd_subNatNat (m : ) (n : ) :
().bodd = xor m.bodd n.bodd
@[simp]
theorem Int.bodd_negOfNat (n : ) :
().bodd = n.bodd
@[simp]
theorem Int.bodd_neg (n : ) :
(-n).bodd = n.bodd
@[simp]
theorem Int.bodd_add (m : ) (n : ) :
(m + n).bodd = xor m.bodd n.bodd
@[simp]
theorem Int.bodd_mul (m : ) (n : ) :
(m * n).bodd = (m.bodd && n.bodd)
theorem Int.bodd_add_div2 (n : ) :
(bif n.bodd then 1 else 0) + 2 * n.div2 = n
theorem Int.div2_val (n : ) :
n.div2 = n / 2
@[deprecated]
theorem Int.bit0_val (n : ) :
bit0 n = 2 * n
@[deprecated]
theorem Int.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem Int.bit_val (b : Bool) (n : ) :
Int.bit b n = 2 * n + bif b then 1 else 0
theorem Int.bit_decomp (n : ) :
Int.bit n.bodd n.div2 = n
def Int.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Int.bit b n)) :
C n

Defines a function from ℤ conditionally, if it is defined for odd and even integers separately using bit.

Equations
• n.bitCasesOn h = .mpr (h n.bodd n.div2)
Instances For
@[simp]
theorem Int.bit_zero :
= 0
@[simp]
theorem Int.bit_coe_nat (b : Bool) (n : ) :
Int.bit b n = (Nat.bit b n)
@[simp]
theorem Int.bit_negSucc (b : Bool) (n : ) :
@[simp]
theorem Int.bodd_bit (b : Bool) (n : ) :
(Int.bit b n).bodd = b
@[simp, deprecated]
theorem Int.bodd_bit0 (n : ) :
(bit0 n).bodd = false
@[simp, deprecated]
theorem Int.bodd_bit1 (n : ) :
(bit1 n).bodd = true
@[deprecated]
theorem Int.bit0_ne_bit1 (m : ) (n : ) :
@[deprecated]
theorem Int.bit1_ne_bit0 (m : ) (n : ) :
@[deprecated]
theorem Int.bit1_ne_zero (m : ) :
bit1 m 0
@[simp]
theorem Int.testBit_bit_zero (b : Bool) (n : ) :
(Int.bit b n).testBit 0 = b
@[simp]
theorem Int.testBit_bit_succ (m : ) (b : Bool) (n : ) :
(Int.bit b n).testBit m.succ = n.testBit m
theorem Int.bitwise_diff :
(Int.bitwise fun (a b : Bool) => a && !b) = Int.ldiff
@[simp]
theorem Int.bitwise_bit (f : ) (a : Bool) (m : ) (b : Bool) (n : ) :
Int.bitwise f (Int.bit a m) (Int.bit b n) = Int.bit (f a b) (Int.bitwise f m n)
@[simp]
theorem Int.lor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
(Int.bit a m).lor (Int.bit b n) = Int.bit (a || b) (m.lor n)
@[simp]
theorem Int.land_bit (a : Bool) (m : ) (b : Bool) (n : ) :
(Int.bit a m).land (Int.bit b n) = Int.bit (a && b) (m.land n)
@[simp]
theorem Int.ldiff_bit (a : Bool) (m : ) (b : Bool) (n : ) :
(Int.bit a m).ldiff (Int.bit b n) = Int.bit (a && !b) (m.ldiff n)
@[simp]
theorem Int.lxor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
(Int.bit a m).xor (Int.bit b n) = Int.bit (xor a b) (m.xor n)
@[simp]
theorem Int.lnot_bit (b : Bool) (n : ) :
(Int.bit b n).lnot = Int.bit (!b) n.lnot
@[simp]
theorem Int.testBit_bitwise (f : ) (m : ) (n : ) (k : ) :
(Int.bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
@[simp]
theorem Int.testBit_lor (m : ) (n : ) (k : ) :
(m.lor n).testBit k = (m.testBit k || n.testBit k)
@[simp]
theorem Int.testBit_land (m : ) (n : ) (k : ) :
(m.land n).testBit k = (m.testBit k && n.testBit k)
@[simp]
theorem Int.testBit_ldiff (m : ) (n : ) (k : ) :
(m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
@[simp]
theorem Int.testBit_lxor (m : ) (n : ) (k : ) :
(m.xor n).testBit k = xor (m.testBit k) (n.testBit k)
@[simp]
theorem Int.testBit_lnot (n : ) (k : ) :
n.lnot.testBit k = !n.testBit k
@[simp]
theorem Int.shiftLeft_neg (m : ) (n : ) :
m <<< (-n) = m >>> n
@[simp]
theorem Int.shiftRight_neg (m : ) (n : ) :
m >>> (-n) = m <<< n
@[simp]
theorem Int.shiftLeft_coe_nat (m : ) (n : ) :
m <<< n = (m <<< n)
@[simp]
theorem Int.shiftRight_coe_nat (m : ) (n : ) :
m >>> n = (m >>> n)
@[simp]
theorem Int.shiftLeft_negSucc (m : ) (n : ) :
<<< n =
@[simp]
theorem Int.shiftRight_negSucc (m : ) (n : ) :
>>> n = Int.negSucc (m >>> n)
theorem Int.shiftRight_add (m : ) (n : ) (k : ) :
m >>> (n + k) = m >>> n >>> k

bitwise ops #

theorem Int.shiftLeft_add (m : ) (n : ) (k : ) :
m <<< (n + k) = m <<< n <<< k
theorem Int.shiftLeft_sub (m : ) (n : ) (k : ) :
m <<< (n - k) = m <<< n >>> k
theorem Int.shiftLeft_eq_mul_pow (m : ) (n : ) :
m <<< n = m * (2 ^ n)
theorem Int.shiftRight_eq_div_pow (m : ) (n : ) :
m >>> n = m / (2 ^ n)
theorem Int.one_shiftLeft (n : ) :
1 <<< n = (2 ^ n)
@[simp]
theorem Int.zero_shiftLeft (n : ) :
0 <<< n = 0
@[simp]
theorem Int.zero_shiftRight (n : ) :
0 >>> n = 0