mathlib3 documentation

core / init.data.nat.bitwise

source
def nat.bodd_div2  :
ℕ → bool × ℕ
Equations
source
def nat.div2 (n : ℕ) :
ℕ
Equations
source
def nat.bodd (n : ℕ) :
bool
Equations
source
@[simp]
theorem nat.bodd_zero  :
0.bodd = bool.ff
source
theorem nat.bodd_one  :
1.bodd = bool.tt
source
theorem nat.bodd_two  :
2.bodd = bool.ff
source
@[simp]
theorem nat.bodd_succ (n : ℕ) :
n.succ.bodd = !n.bodd
source
@[simp]
theorem nat.bodd_add (m n : ℕ) :
(m + n).bodd = bxor m.bodd n.bodd
source
@[simp]
theorem nat.bodd_mul (m n : ℕ) :
(m * n).bodd = m.bodd && n.bodd
source
theorem nat.mod_two_of_bodd (n : ℕ) :
n % 2 = cond n.bodd 1 0
source
@[simp]
theorem nat.div2_zero  :
0.div2 = 0
source
theorem nat.div2_one  :
1.div2 = 0
source
theorem nat.div2_two  :
2.div2 = 1
source
@[simp]
theorem nat.div2_succ (n : ℕ) :
n.succ.div2 = cond n.bodd n.div2.succ n.div2
source
theorem nat.bodd_add_div2 (n : ℕ) :
cond n.bodd 1 0 + 2 * n.div2 = n
source
theorem nat.div2_val (n : ℕ) :
n.div2 = n / 2
source
def nat.bit (b : bool) :
ℕ → ℕ
Equations
source
theorem nat.bit0_val (n : ℕ) :
bit0 n = 2 * n
source
theorem nat.bit1_val (n : ℕ) :
bit1 n = 2 * n + 1
source
theorem nat.bit_val (b : bool) (n : ℕ) :
nat.bit b n = 2 * n + cond b 1 0
source
theorem nat.bit_decomp (n : ℕ) :
nat.bit n.bodd n.div2 = n
source
def nat.bit_cases_on {C : ℕ → Sort u} (n : ℕ) (h : Π (b : bool) (n : ℕ), C (nat.bit b n)) :
C n
Equations
source
theorem nat.bit_zero  :
nat.bit bool.ff 0 = 0
source
def nat.shiftl' (b : bool) (m : ℕ) :
ℕ → ℕ
Equations
source
def nat.shiftl  :
ℕ → ℕ → ℕ
Equations
source
@[simp]
theorem nat.shiftl_zero (m : ℕ) :
m.shiftl 0 = m
source
@[simp]
theorem nat.shiftl_succ (m n : ℕ) :
m.shiftl (n + 1) = bit0 (m.shiftl n)
source
def nat.shiftr  :
ℕ → ℕ → ℕ
Equations
source
def nat.test_bit (m n : ℕ) :
bool
Equations
source
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
source
def nat.size  :
ℕ → ℕ
Equations
source
def nat.bits  :
ℕ → list bool
Equations
source
def nat.bitwise (f : bool → bool → bool) :
ℕ → ℕ → ℕ
Equations
source
def nat.lor  :
ℕ → ℕ → ℕ
Equations
source
def nat.land  :
ℕ → ℕ → ℕ
Equations
source
def nat.ldiff  :
ℕ → ℕ → ℕ
Equations
source
def nat.lxor  :
ℕ → ℕ → ℕ
Equations
source
@[simp]
theorem nat.binary_rec_zero {C : ℕ → Sort u} (z : C 0) (f : Π (b : bool) (n : ℕ), C n → C (nat.bit b n)) :
nat.binary_rec z f 0 = z

bitwise ops

source
theorem nat.bodd_bit (b : bool) (n : ℕ) :
(nat.bit b n).bodd = b
source
theorem nat.div2_bit (b : bool) (n : ℕ) :
(nat.bit b n).div2 = n
source
theorem nat.shiftl'_add (b : bool) (m n k : ℕ) :
nat.shiftl' b m (n + k) = nat.shiftl' b (nat.shiftl' b m n) k
source
theorem nat.shiftl_add (m n k : ℕ) :
m.shiftl (n + k) = (m.shiftl n).shiftl k
source
theorem nat.shiftr_add (m n k : ℕ) :
m.shiftr (n + k) = (m.shiftr n).shiftr k
source
theorem nat.shiftl'_sub (b : bool) (m : ℕ) {n k : ℕ} :
k ≤ n → nat.shiftl' b m (n - k) = (nat.shiftl' b m n).shiftr k
source
theorem nat.shiftl_sub (m : ℕ) {n k : ℕ} :
k ≤ n → m.shiftl (n - k) = (m.shiftl n).shiftr k
source
@[simp]
theorem nat.test_bit_zero (b : bool) (n : ℕ) :
(nat.bit b n).test_bit 0 = b
source
theorem nat.test_bit_succ (m : ℕ) (b : bool) (n : ℕ) :
(nat.bit b n).test_bit m.succ = n.test_bit m
source
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)
source
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
source
@[simp]
theorem nat.bitwise_zero_left (f : bool → bool → bool) (n : ℕ) :
nat.bitwise f 0 n = cond (f bool.ff bool.tt) n 0
source
@[simp]
theorem nat.bitwise_zero_right (f : bool → bool → bool) (h : f bool.ff bool.ff = bool.ff) (m : ℕ) :
nat.bitwise f m 0 = cond (f bool.tt bool.ff) m 0
source
@[simp]
theorem nat.bitwise_zero (f : bool → bool → bool) :
nat.bitwise f 0 0 = 0
source
@[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)
source
theorem nat.bitwise_swap {f : bool → bool → bool} (h : f bool.ff bool.ff = bool.ff) :
nat.bitwise (function.swap f) = function.swap (nat.bitwise f)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[simp]
theorem nat.test_bit_lor (m n k : ℕ) :
(m.lor n).test_bit k = m.test_bit k || n.test_bit k
source
@[simp]
theorem nat.test_bit_land (m n k : ℕ) :
(m.land n).test_bit k = m.test_bit k && n.test_bit k
source
@[simp]
theorem nat.test_bit_ldiff (m n k : ℕ) :
(m.ldiff n).test_bit k = m.test_bit k && !n.test_bit k
source
@[simp]
theorem nat.test_bit_lxor (m n k : ℕ) :
(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)