Int.bitwise_bit
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)
The theorem `Int.bitwise_bit` establishes a property of the `Int.bitwise` function and the `Int.bit` function. It states that for any boolean function `f`, any two boolean values `a` and `b`, and any two integers `m` and `n`, the result of applying `Int.bitwise` to the integers obtained by appending `a` and `b` to `m` and `n` respectively using `Int.bit`, is the same as the integer obtained by appending the result of applying `f` to `a` and `b` to the result of applying `Int.bitwise` to `m` and `n`.
In other words, you can either append the bits to the integers first and then apply the bitwise operation, or apply the bitwise operation first and then append the resulting bit, and you end up with the same result.
More concisely: For any boolean function `f` and integers `m`, `n`, `a`, and `b`, `Int.bitwise m (Int.bit a m) Int.bit b n` is equal to `Int.bitwise (Int.bit a m @ Int.bit b n) (m + n)`.
|
Int.bit_val
theorem Int.bit_val : ∀ (b : Bool) (n : ℤ), Int.bit b n = 2 * n + bif b then 1 else 0
This theorem, `Int.bit_val`, asserts that for any boolean `b` and integer `n`, the function `Int.bit b n`, which appends the digit `b` to the binary representation of `n`, results in the value `2 * n + bif b then 1 else 0`. In other words, the function effectively doubles `n` and adds `1` if `b` is true (representing the binary digit `1`) or adds `0` if `b` is false (representing the binary digit `0`). This is reflective of how binary numbers are calculated from their representation.
More concisely: For any boolean `b` and integer `n`, `Int.bit b n` equals `2 * n + if b then 1 else 0`.
|
Int.bodd_neg
theorem Int.bodd_neg : ∀ (n : ℤ), (-n).bodd = n.bodd
The theorem `Int.bodd_neg` states that for all integers `n`, the function `Int.bodd` applied to the negation of `n` is equal to `Int.bodd` applied to `n` itself. In other words, the parity (oddness or evenness) of an integer remains the same when its sign is flipped.
More concisely: For all integers n, Int.bodd (-\_) n = Int.bodd n.
|
Int.bit_coe_nat
theorem Int.bit_coe_nat : ∀ (b : Bool) (n : ℕ), Int.bit b ↑n = ↑(Nat.bit b n)
This theorem states that for any boolean value `b` and natural number `n`, the operation of appending the bit `b` to the binary representation of the integer version of `n` (i.e., `Int.bit b ↑n`) is equal to the operation of appending the bit `b` to the binary representation of `n` itself (i.e., `Nat.bit b n`), where the result is then converted to an integer. In other words, whether we first convert `n` to an integer and then append the bit, or first append the bit and then convert to an integer, the result is the same.
More concisely: For any boolean value `b` and natural number `n`, `Int.bit b (Nat.toInt n)` equals `Nat.bit b n`.
|
Int.bit_negSucc
theorem Int.bit_negSucc : ∀ (b : Bool) (n : ℕ), Int.bit b (Int.negSucc n) = Int.negSucc (Nat.bit (!b) n)
The theorem `Int.bit_negSucc` states that for all boolean `b` and natural number `n`, appending the bit `b` to the binary representation of the integer `Int.negSucc n` results in the same integer as appending the bit `!b` (the negation of `b`) to the binary representation of the natural number `n` and then taking `Int.negSucc` of the result. In other words, it relates the binary representation of negative integers with the binary representation of natural numbers considering the bit negation operation.
More concisely: For all natural numbers `n` and booleans `b`, `Int.negSucc (bit_not b) ^ Int.toBin (n : Int) = Int.negSucc (Int.toBin (b ^ n))`, where `^` denotes concatenation and `Int.toBin` converts an integer to its binary representation as a string.
|
Int.testBit_bitwise
theorem Int.testBit_bitwise :
∀ (f : Bool → Bool → Bool) (m n : ℤ) (k : ℕ), (Int.bitwise f m n).testBit k = f (m.testBit k) (n.testBit k) := by
sorry
This theorem states that for any Boolean function `f`, any two integers `m` and `n`, and any natural number `k`, the `k+1`-st least significant bit of the result of applying `f` bitwise to `m` and `n` is equal to the result of applying `f` to the `k+1`-st least significant bits of `m` and `n`. In other words, it states that the function `Int.bitwise` applies the function `f` to each pair of corresponding bits in `m` and `n` and its result's `k+1`-st least significant bit can be computed by applying `f` to the `k+1`-st least significant bits of `m` and `n`.
More concisely: For any Boolean function `f`, the `k+1`-th bit of `Int.bitwise f m n` is equal to `f` applied to the `k+1`-th bits of `m` and `n`.
|