Documentation

Init.Data.UInt.Bitwise

source
def commandDeclare_bitwise_uint_theorems__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem UInt8.toBitVec_add {a b : UInt8} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[deprecated UInt8.toNat_and (since := "2024-11-28")]
    theorem UInt8.and_toNat (a b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt8.toNat_xor (a b : UInt8) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_and (a b : UInt8) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_or (a b : UInt8) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt8.toNat_shiftRight (a b : UInt8) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 8)
    source
    @[simp]
    theorem UInt8.toBitVec_not {a : UInt8} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_shiftLeft (a b : UInt8) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt8.toNat_shiftLeft (a b : UInt8) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 8) % 2 ^ 8
    source
    @[simp]
    theorem UInt8.toBitVec_mod {a b : UInt8} :
    (a % b).toBitVec = a.toBitVec % b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_and (a b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_shiftRight (a b : UInt8) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt8.toBitVec_sub {a b : UInt8} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_div {a b : UInt8} :
    (a / b).toBitVec = a.toBitVec / b.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_xor (a b : UInt8) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_or (a b : UInt8) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_mul {a b : UInt8} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_xor (a b : UInt16) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_div {a b : UInt16} :
    (a / b).toBitVec = a.toBitVec / b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_and (a b : UInt16) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_shiftRight (a b : UInt16) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toBitVec_sub {a b : UInt16} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_shiftRight (a b : UInt16) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 16)
    source
    @[simp]
    theorem UInt16.toNat_and (a b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_mod {a b : UInt16} :
    (a % b).toBitVec = a.toBitVec % b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_or (a b : UInt16) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_shiftLeft (a b : UInt16) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toBitVec_xor (a b : UInt16) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_or (a b : UInt16) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_not {a : UInt16} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[deprecated UInt16.toNat_and (since := "2024-11-28")]
    theorem UInt16.and_toNat (a b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt16.toNat_shiftLeft (a b : UInt16) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16
    source
    @[simp]
    theorem UInt16.toBitVec_mul {a b : UInt16} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_add {a b : UInt16} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_shiftRight (a b : UInt32) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toBitVec_xor (a b : UInt32) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_and (a b : UInt32) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_sub {a b : UInt32} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_shiftLeft (a b : UInt32) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 32
    source
    @[simp]
    theorem UInt32.toNat_or (a b : UInt32) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_div {a b : UInt32} :
    (a / b).toBitVec = a.toBitVec / b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_mod {a b : UInt32} :
    (a % b).toBitVec = a.toBitVec % b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_add {a b : UInt32} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_mul {a b : UInt32} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[deprecated UInt32.toNat_and (since := "2024-11-28")]
    theorem UInt32.and_toNat (a b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_or (a b : UInt32) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_shiftRight (a b : UInt32) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 32)
    source
    @[simp]
    theorem UInt32.toBitVec_shiftLeft (a b : UInt32) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toBitVec_not {a : UInt32} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_and (a b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.toNat_xor (a b : UInt32) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_shiftLeft (a b : UInt64) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 64)
    source
    @[simp]
    theorem UInt64.toBitVec_add {a b : UInt64} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_or (a b : UInt64) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_xor (a b : UInt64) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_xor (a b : UInt64) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_not {a : UInt64} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_sub {a b : UInt64} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_or (a b : UInt64) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_mul {a b : UInt64} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_shiftLeft (a b : UInt64) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 64) % 2 ^ 64
    source
    @[simp]
    theorem UInt64.toNat_shiftRight (a b : UInt64) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 64)
    source
    @[deprecated UInt64.toNat_and (since := "2024-11-28")]
    theorem UInt64.and_toNat (a b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt64.toNat_and (a b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_shiftRight (a b : UInt64) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 64)
    source
    @[simp]
    theorem UInt64.toBitVec_and (a b : UInt64) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_mod {a b : UInt64} :
    (a % b).toBitVec = a.toBitVec % b.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_div {a b : UInt64} :
    (a / b).toBitVec = a.toBitVec / b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_div {a b : USize} :
    (a / b).toBitVec = a.toBitVec / b.toBitVec
    source
    @[simp]
    theorem USize.toNat_shiftRight (a b : USize) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % System.Platform.numBits)
    source
    @[simp]
    theorem USize.toBitVec_or (a b : USize) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem USize.toNat_shiftLeft (a b : USize) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits
    source
    @[simp]
    theorem USize.toBitVec_mod {a b : USize} :
    (a % b).toBitVec = a.toBitVec % b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_shiftRight (a b : USize) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toNat_or (a b : USize) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem USize.toBitVec_xor (a b : USize) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_mul {a b : USize} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_sub {a b : USize} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_and (a b : USize) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[deprecated USize.toNat_and (since := "2024-11-28")]
    theorem USize.and_toNat (a b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem USize.toBitVec_shiftLeft (a b : USize) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toBitVec_not {a : USize} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem USize.toNat_xor (a b : USize) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem USize.toNat_and (a b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem USize.toBitVec_add {a b : USize} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem Bool.toBitVec_toUInt8 {b : Bool} :
    b.toUInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt16 {b : Bool} :
    b.toUInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt32 {b : Bool} :
    b.toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt64 {b : Bool} :
    b.toUInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUSize {b : Bool} :
    b.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)