mathlib documentation

core.init.data.nat.bitwise

def nat.bodd_div2  :

Equations
def nat.div2  :

Equations
def nat.bodd  :
bool

Equations
@[simp]
theorem nat.bodd_zero  :

@[simp]
theorem nat.bodd_one  :

@[simp]
theorem nat.bodd_two  :

@[simp]
theorem nat.bodd_succ (n : ) :

@[simp]
theorem nat.bodd_add (m n : ) :
(m + n).bodd = bxor m.bodd n.bodd

@[simp]
theorem nat.bodd_mul (m n : ) :
(m * n).bodd = m.bodd && n.bodd

theorem nat.mod_two_of_bodd (n : ) :
n % 2 = cond n.bodd 1 0

@[simp]
theorem nat.div2_zero  :
0.div2 = 0

@[simp]
theorem nat.div2_one  :
1.div2 = 0

@[simp]
theorem nat.div2_two  :
2.div2 = 1

@[simp]
theorem nat.div2_succ (n : ) :

theorem nat.bodd_add_div2 (n : ) :
cond n.bodd 1 0 + 2 * n.div2 = n

theorem nat.div2_val (n : ) :
n.div2 = n / 2

def nat.bit  :
bool

Equations
theorem nat.bit0_val (n : ) :
bit0 n = 2 * n

theorem nat.bit1_val (n : ) :
bit1 n = 2 * n + 1

theorem nat.bit_val (b : bool) (n : ) :
nat.bit b n = 2 * n + cond b 1 0

theorem nat.bit_decomp (n : ) :

def nat.bit_cases_on {C : Sort u} (n : ) :
(Π (b : bool) (n : ), C (nat.bit b n))C n

Equations
@[simp]
theorem nat.bit_zero  :

def nat.shiftl'  :
bool

Equations
def nat.shiftl  :

Equations
@[simp]
theorem nat.shiftl_zero (m : ) :
m.shiftl 0 = m

@[simp]
theorem nat.shiftl_succ (m n : ) :
m.shiftl (n + 1) = bit0 (m.shiftl n)

def nat.shiftr  :

Equations
def nat.test_bit  :
bool

Equations
def nat.binary_rec {C : Sort u} (z : C 0) (f : Π (b : bool) (n : ), C nC (nat.bit b n)) (n : ) :
C n

Equations
def nat.size  :

Equations
def nat.bits  :

Equations
def nat.bitwise  :
(boolboolbool)

Equations
def nat.lor  :

Equations
def nat.land  :

Equations
def nat.ldiff  :

Equations
def nat.lxor  :

Equations
@[simp]
theorem nat.binary_rec_zero {C : Sort u} (z : C 0) (f : Π (b : bool) (n : ), C nC (nat.bit b n)) :

theorem nat.bodd_bit (b : bool) (n : ) :
(nat.bit b n).bodd = b

theorem nat.div2_bit (b : bool) (n : ) :
(nat.bit b n).div2 = n

theorem nat.shiftl'_add (b : bool) (m n k : ) :
nat.shiftl' b m (n + k) = nat.shiftl' b (nat.shiftl' b m n) k

theorem nat.shiftl_add (m n k : ) :
m.shiftl (n + k) = (m.shiftl n).shiftl k

theorem nat.shiftr_add (m n k : ) :
m.shiftr (n + k) = (m.shiftr n).shiftr k

theorem nat.shiftl'_sub (b : bool) (m : ) {n k : } :
k nnat.shiftl' b m (n - k) = (nat.shiftl' b m n).shiftr k

theorem nat.shiftl_sub (m : ) {n k : } :
k nm.shiftl (n - k) = (m.shiftl n).shiftr k

@[simp]
theorem nat.test_bit_zero (b : bool) (n : ) :
(nat.bit b n).test_bit 0 = b

theorem nat.test_bit_succ (m : ) (b : bool) (n : ) :

theorem nat.binary_rec_eq {C : Sort u} {z : C 0} {f : Π (b : bool) (n : ), C nC (nat.bit b n)} (h : f ff 0 z = z) (b : bool) (n : ) :
nat.binary_rec z f (nat.bit b n) = f b n (nat.binary_rec z f n)

theorem nat.bitwise_bit_aux {f : boolboolbool} :
f ff ff = ff(nat.binary_rec (cond (f tt ff) (nat.bit ff 0) 0) (λ (b : bool) (n : ) (_x : (λ (_x : ), ) n), nat.bit (f ff b) (cond (f ff tt) n 0)) = λ (n : ), cond (f ff tt) n 0)

@[simp]
theorem nat.bitwise_zero_left (f : boolboolbool) (n : ) :
nat.bitwise f 0 n = cond (f ff tt) n 0

@[simp]
theorem nat.bitwise_zero_right (f : boolboolbool) (h : f ff ff = ff) (m : ) :
nat.bitwise f m 0 = cond (f tt ff) m 0

@[simp]
theorem nat.bitwise_zero (f : boolboolbool) :
nat.bitwise f 0 0 = 0

@[simp]
theorem nat.bitwise_bit {f : boolboolbool} (h : f ff ff = ff) (a : bool) (m : ) (b : bool) (n : ) :
nat.bitwise f (nat.bit a m) (nat.bit b n) = nat.bit (f a b) (nat.bitwise f m n)

@[simp]
theorem nat.lor_bit (a : bool) (m : ) (b : bool) (n : ) :
(nat.bit a m).lor (nat.bit b n) = nat.bit (a || b) (m.lor n)

@[simp]
theorem nat.land_bit (a : bool) (m : ) (b : bool) (n : ) :
(nat.bit a m).land (nat.bit b n) = nat.bit (a && b) (m.land n)

@[simp]
theorem nat.ldiff_bit (a : bool) (m : ) (b : bool) (n : ) :
(nat.bit a m).ldiff (nat.bit b n) = nat.bit (a && !b) (m.ldiff n)

@[simp]
theorem nat.lxor_bit (a : bool) (m : ) (b : bool) (n : ) :
(nat.bit a m).lxor (nat.bit b n) = nat.bit (bxor a b) (m.lxor n)

@[simp]
theorem nat.test_bit_bitwise {f : boolboolbool} (h : f ff ff = ff) (m n k : ) :
(nat.bitwise f m n).test_bit k = f (m.test_bit k) (n.test_bit k)

@[simp]
theorem nat.test_bit_lor (m n k : ) :
(m.lor n).test_bit k = m.test_bit k || n.test_bit k

@[simp]
theorem nat.test_bit_land (m n k : ) :
(m.land n).test_bit k = m.test_bit k && n.test_bit k

@[simp]
theorem nat.test_bit_ldiff (m n k : ) :

@[simp]
theorem nat.test_bit_lxor (m n k : ) :
(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)