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 #

source
@[simp]
theorem int.bodd_zero  :
0.bodd = bool.ff
source
@[simp]
theorem int.bodd_one  :
1.bodd = bool.tt
source
theorem int.bodd_two  :
2.bodd = bool.ff
source
@[simp, norm_cast]
theorem int.bodd_coe (n : ℕ) :
↑n.bodd = n.bodd
source
@[simp]
theorem int.bodd_sub_nat_nat (m n : ℕ) :
(int.sub_nat_nat m n).bodd = bxor m.bodd n.bodd
source
@[simp]
theorem int.bodd_neg_of_nat (n : ℕ) :
(int.neg_of_nat n).bodd = n.bodd
source
@[simp]
theorem int.bodd_neg (n : ℤ) :
(-n).bodd = n.bodd
source
@[simp]
theorem int.bodd_add (m n : ℤ) :
(m + n).bodd = bxor m.bodd n.bodd
source
@[simp]
theorem int.bodd_mul (m n : ℤ) :
(m * n).bodd = m.bodd && n.bodd
source
theorem int.bodd_add_div2 (n : ℤ) :
cond n.bodd 1 0 + 2 * n.div2 = n
source
theorem int.div2_val (n : ℤ) :
n.div2 = n / 2
source
theorem int.bit0_val (n : ℤ) :
bit0 n = 2 * n
source
theorem int.bit1_val (n : ℤ) :
bit1 n = 2 * n + 1
source
theorem int.bit_val (b : bool) (n : ℤ) :
int.bit b n = 2 * n + cond b 1 0
source
theorem int.bit_decomp (n : ℤ) :
int.bit n.bodd n.div2 = n
source
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
source
@[simp]
theorem int.bit_zero  :
int.bit bool.ff 0 = 0
source
@[simp]
theorem int.bit_coe_nat (b : bool) (n : ℕ) :
int.bit b ↑n = ↑(nat.bit b n)
source
@[simp]
theorem int.bit_neg_succ (b : bool) (n : ℕ) :
int.bit b -[1+ n] = -[1+ nat.bit (!b) n]
source
@[simp]
theorem int.bodd_bit (b : bool) (n : ℤ) :
(int.bit b n).bodd = b
source
@[simp]
theorem int.bodd_bit0 (n : ℤ) :
(bit0 n).bodd = bool.ff
source
@[simp]
theorem int.bodd_bit1 (n : ℤ) :
(bit1 n).bodd = bool.tt
source
theorem int.bit0_ne_bit1 (m n : ℤ) :
bit0 m ≠ bit1 n
source
theorem int.bit1_ne_bit0 (m n : ℤ) :
bit1 m ≠ bit0 n
source
theorem int.bit1_ne_zero (m : ℤ) :
bit1 m ≠ 0
source
@[simp]
theorem int.test_bit_zero (b : bool) (n : ℤ) :
(int.bit b n).test_bit 0 = b
source
@[simp]
theorem int.test_bit_succ (m : ℕ) (b : bool) (n : ℤ) :
(int.bit b n).test_bit m.succ = n.test_bit m
source
theorem int.bitwise_or  :
int.bitwise bor = int.lor
source
theorem int.bitwise_and  :
int.bitwise band = int.land
source
theorem int.bitwise_diff  :
int.bitwise (λ (a b : bool), a && !b) = int.ldiff
source
theorem int.bitwise_xor  :
int.bitwise bxor = int.lxor
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[simp]
theorem int.lnot_bit (b : bool) (n : ℤ) :
(int.bit b n).lnot = int.bit (!b) n.lnot
source
@[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)
source
@[simp]
theorem int.test_bit_lor (m n : ℤ) (k : ℕ) :
(m.lor n).test_bit k = m.test_bit k || n.test_bit k
source
@[simp]
theorem int.test_bit_land (m n : ℤ) (k : ℕ) :
(m.land n).test_bit k = m.test_bit k && n.test_bit k
source
@[simp]
theorem int.test_bit_ldiff (m n : ℤ) (k : ℕ) :
(m.ldiff n).test_bit k = m.test_bit k && !n.test_bit k
source
@[simp]
theorem int.test_bit_lxor (m n : ℤ) (k : ℕ) :
(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)
source
@[simp]
theorem int.test_bit_lnot (n : ℤ) (k : ℕ) :
n.lnot.test_bit k = !n.test_bit k
source
@[simp]
theorem int.shiftl_neg (m n : ℤ) :
m.shiftl (-n) = m.shiftr n
source
@[simp]
theorem int.shiftr_neg (m n : ℤ) :
m.shiftr (-n) = m.shiftl n
source
@[simp]
theorem int.shiftl_coe_nat (m n : ℕ) :
↑m.shiftl ↑n = ↑(m.shiftl n)
source
@[simp]
theorem int.shiftr_coe_nat (m n : ℕ) :
↑m.shiftr ↑n = ↑(m.shiftr n)
source
@[simp]
theorem int.shiftl_neg_succ (m n : ℕ) :
-[1+ m].shiftl ↑n = -[1+ nat.shiftl' bool.tt m n]
source
@[simp]
theorem int.shiftr_neg_succ (m n : ℕ) :
-[1+ m].shiftr ↑n = -[1+ m.shiftr n]
source
theorem int.shiftr_add (m : ℤ) (n k : ℕ) :
m.shiftr (↑n + ↑k) = (m.shiftr ↑n).shiftr ↑k

bitwise ops #

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