mathlib3 documentation

data.int.bitwise

Bitwise operations on integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Recursors #

bitwise ops #

@[simp]
theorem int.bodd_zero  :
@[simp]
theorem int.bodd_one  :
theorem int.bodd_two  :
@[simp, norm_cast]
theorem int.bodd_coe (n : ) :
@[simp]
theorem int.bodd_sub_nat_nat (m n : ) :
@[simp]
theorem int.bodd_neg_of_nat (n : ) :
@[simp]
theorem int.bodd_neg (n : ) :
(-n).bodd = n.bodd
@[simp]
theorem int.bodd_add (m n : ) :
(m + n).bodd = bxor m.bodd n.bodd
@[simp]
theorem int.bodd_mul (m n : ) :
(m * n).bodd = m.bodd && n.bodd
theorem int.bodd_add_div2 (n : ) :
cond n.bodd 1 0 + 2 * n.div2 = n
theorem int.div2_val (n : ) :
n.div2 = n / 2
theorem int.bit0_val (n : ) :
bit0 n = 2 * n
theorem int.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem int.bit_val (b : bool) (n : ) :
int.bit b n = 2 * n + cond b 1 0
theorem int.bit_decomp (n : ) :
def int.bit_cases_on {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
@[simp]
theorem int.bit_zero  :
@[simp]
theorem int.bit_coe_nat (b : bool) (n : ) :
@[simp]
theorem int.bit_neg_succ (b : bool) (n : ) :
@[simp]
theorem int.bodd_bit (b : bool) (n : ) :
(int.bit b n).bodd = b
@[simp]
theorem int.bodd_bit0 (n : ) :
@[simp]
theorem int.bodd_bit1 (n : ) :
theorem int.bit0_ne_bit1 (m n : ) :
theorem int.bit1_ne_bit0 (m n : ) :
theorem int.bit1_ne_zero (m : ) :
bit1 m 0
@[simp]
theorem int.test_bit_zero (b : bool) (n : ) :
(int.bit b n).test_bit 0 = b
@[simp]
theorem int.test_bit_succ (m : ) (b : bool) (n : ) :
theorem int.bitwise_diff  :
int.bitwise (λ (a b : bool), a && !b) = int.ldiff
@[simp]
theorem int.bitwise_bit (f : bool bool bool) (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).lxor (int.bit b n) = int.bit (bxor a b) (m.lxor n)
@[simp]
theorem int.lnot_bit (b : bool) (n : ) :
(int.bit b n).lnot = int.bit (!b) n.lnot
@[simp]
theorem int.test_bit_bitwise (f : bool bool bool) (m n : ) (k : ) :
(int.bitwise f m n).test_bit k = f (m.test_bit k) (n.test_bit k)
@[simp]
theorem int.test_bit_lor (m n : ) (k : ) :
(m.lor n).test_bit k = m.test_bit k || n.test_bit k
@[simp]
theorem int.test_bit_land (m n : ) (k : ) :
(m.land n).test_bit k = m.test_bit k && n.test_bit k
@[simp]
theorem int.test_bit_ldiff (m n : ) (k : ) :
@[simp]
theorem int.test_bit_lxor (m n : ) (k : ) :
(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)
@[simp]
theorem int.test_bit_lnot (n : ) (k : ) :
@[simp]
theorem int.shiftl_neg (m n : ) :
m.shiftl (-n) = m.shiftr n
@[simp]
theorem int.shiftr_neg (m n : ) :
m.shiftr (-n) = m.shiftl n
@[simp]
theorem int.shiftl_coe_nat (m n : ) :
@[simp]
theorem int.shiftr_coe_nat (m n : ) :
@[simp]
@[simp]
theorem int.shiftr_neg_succ (m n : ) :
theorem int.shiftr_add (m : ) (n k : ) :

bitwise ops #

theorem int.shiftl_add (m : ) (n : ) (k : ) :
m.shiftl (n + k) = (m.shiftl n).shiftl k
theorem int.shiftl_sub (m : ) (n : ) (k : ) :
m.shiftl (n - k) = (m.shiftl n).shiftr k
theorem int.shiftl_eq_mul_pow (m : ) (n : ) :
m.shiftl n = m * (2 ^ n)
theorem int.shiftr_eq_div_pow (m : ) (n : ) :
m.shiftr n = m / (2 ^ n)
theorem int.one_shiftl (n : ) :
1.shiftl n = (2 ^ n)
@[simp]
theorem int.zero_shiftl (n : ) :
0.shiftl n = 0
@[simp]
theorem int.zero_shiftr (n : ) :
0.shiftr n = 0