mathlib3 documentation

core / init.data.nat.bitwise

Equations
def nat.div2 (n : ) :
Equations
def nat.bodd (n : ) :
Equations
@[simp]
theorem nat.bodd_zero  :
theorem nat.bodd_one  :
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
theorem nat.div2_one  :
1.div2 = 0
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 (b : 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 : ) (h : Π (b : bool) (n : ), C (nat.bit b n)) :
C n
Equations
theorem nat.bit_zero  :
def nat.shiftl' (b : bool) (m : ) :
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)
Equations
def nat.test_bit (m n : ) :
Equations
def nat.binary_rec {C : Sort u} (z : C 0) (f : Π (b : bool) (n : ), C n C (nat.bit b n)) (n : ) :
C n
Equations
def nat.size  :
Equations
Equations
Equations
Equations
@[simp]
theorem nat.binary_rec_zero {C : Sort u} (z : C 0) (f : Π (b : bool) (n : ), C n C (nat.bit b n)) :

bitwise ops

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 n nat.shiftl' b m (n - k) = (nat.shiftl' b m n).shiftr k
theorem nat.shiftl_sub (m : ) {n k : } :
k n m.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 n C (nat.bit b n)} (h : f bool.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 : bool bool bool} (h : f bool.ff bool.ff = bool.ff) :
nat.binary_rec (cond (f bool.tt bool.ff) (nat.bit bool.ff 0) 0) (λ (b : bool) (n : ) (_x : (λ (_x : ), ) n), nat.bit (f bool.ff b) (cond (f bool.ff bool.tt) n 0)) = λ (n : ), cond (f bool.ff bool.tt) n 0
@[simp]
theorem nat.bitwise_zero_left (f : bool bool bool) (n : ) :
@[simp]
@[simp]
theorem nat.bitwise_zero (f : bool bool bool) :
nat.bitwise f 0 0 = 0
@[simp]
theorem nat.bitwise_bit {f : bool bool bool} (h : f bool.ff bool.ff = bool.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 : bool bool bool} (h : f bool.ff bool.ff = bool.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)