Documentation

Init.Data.SInt.Bitwise

source
def commandDeclare_bitwise_int_theorems__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Int8.toBitVec_and (a b : Int8) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_xor (a b : Int8) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_sub {a b : Int8} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_div {a b : Int8} :
    (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_shiftLeft (a b : Int8) :
    (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 8
    source
    @[simp]
    theorem Int8.toBitVec_mod {a b : Int8} :
    (a % b).toBitVec = a.toBitVec.srem b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_shiftRight (a b : Int8) :
    (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 8)
    source
    @[simp]
    theorem Int8.toBitVec_mul {a b : Int8} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_or (a b : Int8) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_abs (a : Int8) :
    a.abs.toBitVec = a.toBitVec.abs
    source
    @[simp]
    theorem Int8.toBitVec_add {a b : Int8} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem Int8.toBitVec_not {a : Int8} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_div {a b : Int16} :
    (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_xor (a b : Int16) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_not {a : Int16} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_mod {a b : Int16} :
    (a % b).toBitVec = a.toBitVec.srem b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_or (a b : Int16) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_shiftLeft (a b : Int16) :
    (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 16
    source
    @[simp]
    theorem Int16.toBitVec_add {a b : Int16} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_shiftRight (a b : Int16) :
    (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 16)
    source
    @[simp]
    theorem Int16.toBitVec_and (a b : Int16) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_abs (a : Int16) :
    a.abs.toBitVec = a.toBitVec.abs
    source
    @[simp]
    theorem Int16.toBitVec_sub {a b : Int16} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem Int16.toBitVec_mul {a b : Int16} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_div {a b : Int32} :
    (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_xor (a b : Int32) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_and (a b : Int32) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_shiftLeft (a b : Int32) :
    (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 32
    source
    @[simp]
    theorem Int32.toBitVec_shiftRight (a b : Int32) :
    (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 32)
    source
    @[simp]
    theorem Int32.toBitVec_mod {a b : Int32} :
    (a % b).toBitVec = a.toBitVec.srem b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_not {a : Int32} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_add {a b : Int32} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_mul {a b : Int32} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_abs (a : Int32) :
    a.abs.toBitVec = a.toBitVec.abs
    source
    @[simp]
    theorem Int32.toBitVec_or (a b : Int32) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem Int32.toBitVec_sub {a b : Int32} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_mod {a b : Int64} :
    (a % b).toBitVec = a.toBitVec.srem b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_add {a b : Int64} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_sub {a b : Int64} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_abs (a : Int64) :
    a.abs.toBitVec = a.toBitVec.abs
    source
    @[simp]
    theorem Int64.toBitVec_shiftRight (a b : Int64) :
    (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 64)
    source
    @[simp]
    theorem Int64.toBitVec_and (a b : Int64) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_not {a : Int64} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_or (a b : Int64) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_shiftLeft (a b : Int64) :
    (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 64
    source
    @[simp]
    theorem Int64.toBitVec_div {a b : Int64} :
    (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_mul {a b : Int64} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem Int64.toBitVec_xor (a b : Int64) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_shiftLeft (a b : ISize) :
    (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits
    source
    @[simp]
    theorem ISize.toBitVec_not {a : ISize} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_shiftRight (a b : ISize) :
    (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits)
    source
    @[simp]
    theorem ISize.toBitVec_mod {a b : ISize} :
    (a % b).toBitVec = a.toBitVec.srem b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_abs (a : ISize) :
    a.abs.toBitVec = a.toBitVec.abs
    source
    @[simp]
    theorem ISize.toBitVec_div {a b : ISize} :
    (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_mul {a b : ISize} :
    (a * b).toBitVec = a.toBitVec * b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_add {a b : ISize} :
    (a + b).toBitVec = a.toBitVec + b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_and (a b : ISize) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_xor (a b : ISize) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_sub {a b : ISize} :
    (a - b).toBitVec = a.toBitVec - b.toBitVec
    source
    @[simp]
    theorem ISize.toBitVec_or (a b : ISize) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem Bool.toBitVec_toInt8 {b : Bool} :
    b.toInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toInt16 {b : Bool} :
    b.toInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toInt32 {b : Bool} :
    b.toInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toInt64 {b : Bool} :
    b.toInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toISize {b : Bool} :
    b.toISize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)