Bitwise operations on integers #

Recursors #

Int.bitCasesOn: Parity disjunction. Something is true/defined on ℤ if it's true/defined for even and for odd values.

bitwise ops #

source

@[simp]

theorem Int.bodd_zero :

Int.bodd 0 = false

source

@[simp]

theorem Int.bodd_one :

Int.bodd 1 = true

source

theorem Int.bodd_two :

Int.bodd 2 = false

source

@[simp]

theorem Int.bodd_coe (n : ℕ) :

Int.bodd ↑n = Nat.bodd n

source

@[simp]

theorem Int.bodd_subNatNat (m : ℕ) (n : ℕ) :

Int.bodd (Int.subNatNat m n) = xor (Nat.bodd m) (Nat.bodd n)

source

@[simp]

theorem Int.bodd_negOfNat (n : ℕ) :

Int.bodd (Int.negOfNat n) = Nat.bodd n

source

@[simp]

theorem Int.bodd_neg (n : ℤ) :

Int.bodd (-n) = Int.bodd n

source

@[simp]

theorem Int.bodd_add (m : ℤ) (n : ℤ) :

Int.bodd (m + n) = xor (Int.bodd m) (Int.bodd n)

source

@[simp]

theorem Int.bodd_mul (m : ℤ) (n : ℤ) :

Int.bodd (m * n) = (Int.bodd m && Int.bodd n)

source

theorem Int.bodd_add_div2 (n : ℤ) :

(bif Int.bodd n then 1 else 0) + 2 * Int.div2 n = n

source

theorem Int.div2_val (n : ℤ) :

Int.div2 n = n / 2

source

@[deprecated]

theorem Int.bit0_val (n : ℤ) :

bit0 n = 2 * n

source

@[deprecated]

theorem Int.bit1_val (n : ℤ) :

bit1 n = 2 * n + 1

source

theorem Int.bit_val (b : Bool) (n : ℤ) :

Int.bit b n = 2 * n + bif b then 1 else 0

source

theorem Int.bit_decomp (n : ℤ) :

Int.bit (Int.bodd n) (Int.div2 n) = n

source

def Int.bitCasesOn {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

Int.bitCasesOn n h = Eq.mpr (_ : C n = C (Int.bit (Int.bodd n) (Int.div2 n))) (h (Int.bodd n) (Int.div2 n))

Instances For

source

@[simp]

theorem Int.bit_zero :

Int.bit false 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_negSucc (b : Bool) (n : ℕ) :

Int.bit b (Int.negSucc n) = Int.negSucc (Nat.bit (!b) n)

source

@[simp]

theorem Int.bodd_bit (b : Bool) (n : ℤ) :

Int.bodd (Int.bit b n) = b

source

@[simp, deprecated]

theorem Int.bodd_bit0 (n : ℤ) :

Int.bodd (bit0 n) = false

source

@[simp, deprecated]

theorem Int.bodd_bit1 (n : ℤ) :

Int.bodd (bit1 n) = true

source

@[deprecated]

theorem Int.bit0_ne_bit1 (m : ℤ) (n : ℤ) :

bit0 m ≠ bit1 n

source

@[deprecated]

theorem Int.bit1_ne_bit0 (m : ℤ) (n : ℤ) :

bit1 m ≠ bit0 n

source

@[deprecated]

theorem Int.bit1_ne_zero (m : ℤ) :

bit1 m ≠ 0

source

@[simp]

theorem Int.testBit_zero (b : Bool) (n : ℤ) :

Int.testBit (Int.bit b n) 0 = b

source

@[simp]

theorem Int.testBit_succ (m : ℕ) (b : Bool) (n : ℤ) :

Int.testBit (Int.bit b n) (Nat.succ m) = Int.testBit n m

source

theorem Int.bitwise_or :

Int.bitwise or = Int.lor

source

theorem Int.bitwise_and :

Int.bitwise and = Int.land

source

theorem Int.bitwise_diff :

(Int.bitwise fun a b => a && !b) = Int.ldiff'

source

theorem Int.bitwise_xor :

Int.bitwise xor = 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.lor (Int.bit a m) (Int.bit b n) = Int.bit (a || b) (Int.lor m n)

source

@[simp]

theorem Int.land_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) :

Int.land (Int.bit a m) (Int.bit b n) = Int.bit (a && b) (Int.land m n)

source

@[simp]

theorem Int.ldiff_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) :

Int.ldiff' (Int.bit a m) (Int.bit b n) = Int.bit (a && !b) (Int.ldiff' m n)

source

@[simp]

theorem Int.lxor_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) :

Int.lxor' (Int.bit a m) (Int.bit b n) = Int.bit (xor a b) (Int.lxor' m n)

source

@[simp]

theorem Int.lnot_bit (b : Bool) (n : ℤ) :

Int.lnot (Int.bit b n) = Int.bit (!b) (Int.lnot n)

source

@[simp]

theorem Int.testBit_bitwise (f : Bool → Bool → Bool) (m : ℤ) (n : ℤ) (k : ℕ) :

Int.testBit (Int.bitwise f m n) k = f (Int.testBit m k) (Int.testBit n k)

source

@[simp]

theorem Int.testBit_lor (m : ℤ) (n : ℤ) (k : ℕ) :

Int.testBit (Int.lor m n) k = (Int.testBit m k || Int.testBit n k)

source

@[simp]

theorem Int.testBit_land (m : ℤ) (n : ℤ) (k : ℕ) :

Int.testBit (Int.land m n) k = (Int.testBit m k && Int.testBit n k)

source

@[simp]

theorem Int.testBit_ldiff (m : ℤ) (n : ℤ) (k : ℕ) :

Int.testBit (Int.ldiff' m n) k = (Int.testBit m k && !Int.testBit n k)

source

@[simp]

theorem Int.testBit_lxor (m : ℤ) (n : ℤ) (k : ℕ) :

Int.testBit (Int.lxor' m n) k = xor (Int.testBit m k) (Int.testBit n k)

source

@[simp]

theorem Int.testBit_lnot (n : ℤ) (k : ℕ) :

Int.testBit (Int.lnot n) k = !Int.testBit n k

source

@[simp]

theorem Int.shiftLeft_neg (m : ℤ) (n : ℤ) :

m <<< (-n) = m >>> n

source

@[simp]

theorem Int.shiftRight_neg (m : ℤ) (n : ℤ) :

m >>> (-n) = m <<< n

source

@[simp]

theorem Int.shiftLeft_coe_nat (m : ℕ) (n : ℕ) :

↑m <<< ↑n = ↑(m <<< n)

source

@[simp]

theorem Int.shiftRight_coe_nat (m : ℕ) (n : ℕ) :

↑m >>> ↑n = ↑(m >>> n)

source

@[simp]

theorem Int.shiftLeft_negSucc (m : ℕ) (n : ℕ) :

Int.negSucc m <<< ↑n = Int.negSucc (Nat.shiftLeft' true m n)

source

@[simp]

theorem Int.shiftRight_negSucc (m : ℕ) (n : ℕ) :

Int.negSucc m >>> ↑n = Int.negSucc (m >>> n)

source

theorem Int.shiftRight_add (m : ℤ) (n : ℕ) (k : ℕ) :

m >>> (↑n + ↑k) = m >>> ↑n >>> ↑k

bitwise ops #

source

theorem Int.shiftLeft_add (m : ℤ) (n : ℕ) (k : ℤ) :

m <<< (↑n + k) = m <<< ↑n <<< k

source

theorem Int.shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) :

m <<< (↑n - k) = m <<< ↑n >>> k

source

theorem Int.shiftLeft_eq_mul_pow (m : ℤ) (n : ℕ) :

m <<< ↑n = m * ↑(2 ^ n)

source

theorem Int.shiftRight_eq_div_pow (m : ℤ) (n : ℕ) :

m >>> ↑n = m / ↑(2 ^ n)

source

theorem Int.one_shiftLeft (n : ℕ) :

1 <<< ↑n = ↑(2 ^ n)

source

@[simp]

theorem Int.zero_shiftLeft (n : ℤ) :

0 <<< n = 0

source

@[simp]

theorem Int.zero_shiftRight (n : ℤ) :

0 >>> n = 0