feat: IntX operations and conversion theory (#7592)
This PR adds theory about signed finite integers relating operations and conversion functions.
This commit is contained in:
Markus Himmel
GitHub
parent
7bd9375804
commit
17c18752ff
7 changed files with 4403 additions and 64 deletions
|
|
@ -12,11 +12,6 @@ macro "declare_bitwise_int_theorems" typeName:ident bits:term:arg : command =>
|
|||
`(
|
||||
namespace $typeName
|
||||
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec.srem b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
|
||||
@[simp, int_toBitVec] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
|
||||
|
|
@ -57,30 +52,6 @@ theorem Bool.toBitVec_toISize {b : Bool} :
|
|||
· apply BitVec.eq_of_toNat_eq
|
||||
simp [toISize]
|
||||
|
||||
@[simp] theorem UInt8.toInt8_add (a b : UInt8) : (a + b).toInt8 = a.toInt8 + b.toInt8 := rfl
|
||||
@[simp] theorem UInt16.toInt16_add (a b : UInt16) : (a + b).toInt16 = a.toInt16 + b.toInt16 := rfl
|
||||
@[simp] theorem UInt32.toInt32_add (a b : UInt32) : (a + b).toInt32 = a.toInt32 + b.toInt32 := rfl
|
||||
@[simp] theorem UInt64.toInt64_add (a b : UInt64) : (a + b).toInt64 = a.toInt64 + b.toInt64 := rfl
|
||||
@[simp] theorem USize.toISize_add (a b : USize) : (a + b).toISize = a.toISize + b.toISize := rfl
|
||||
|
||||
@[simp] theorem UInt8.toInt8_neg (a : UInt8) : (-a).toInt8 = -a.toInt8 := rfl
|
||||
@[simp] theorem UInt16.toInt16_neg (a : UInt16) : (-a).toInt16 = -a.toInt16 := rfl
|
||||
@[simp] theorem UInt32.toInt32_neg (a : UInt32) : (-a).toInt32 = -a.toInt32 := rfl
|
||||
@[simp] theorem UInt64.toInt64_neg (a : UInt64) : (-a).toInt64 = -a.toInt64 := rfl
|
||||
@[simp] theorem USize.toISize_neg (a : USize) : (-a).toISize = -a.toISize := rfl
|
||||
|
||||
@[simp] theorem UInt8.toInt8_sub (a b : UInt8) : (a - b).toInt8 = a.toInt8 - b.toInt8 := rfl
|
||||
@[simp] theorem UInt16.toInt16_sub (a b : UInt16) : (a - b).toInt16 = a.toInt16 - b.toInt16 := rfl
|
||||
@[simp] theorem UInt32.toInt32_sub (a b : UInt32) : (a - b).toInt32 = a.toInt32 - b.toInt32 := rfl
|
||||
@[simp] theorem UInt64.toInt64_sub (a b : UInt64) : (a - b).toInt64 = a.toInt64 - b.toInt64 := rfl
|
||||
@[simp] theorem USize.toISize_sub (a b : USize) : (a - b).toISize = a.toISize - b.toISize := rfl
|
||||
|
||||
@[simp] theorem UInt8.toInt8_mul (a b : UInt8) : (a * b).toInt8 = a.toInt8 * b.toInt8 := rfl
|
||||
@[simp] theorem UInt16.toInt16_mul (a b : UInt16) : (a * b).toInt16 = a.toInt16 * b.toInt16 := rfl
|
||||
@[simp] theorem UInt32.toInt32_mul (a b : UInt32) : (a * b).toInt32 = a.toInt32 * b.toInt32 := rfl
|
||||
@[simp] theorem UInt64.toInt64_mul (a b : UInt64) : (a * b).toInt64 = a.toInt64 * b.toInt64 := rfl
|
||||
@[simp] theorem USize.toISize_mul (a b : USize) : (a * b).toISize = a.toISize * b.toISize := rfl
|
||||
|
||||
@[simp] theorem UInt8.toInt8_and (a b : UInt8) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := rfl
|
||||
@[simp] theorem UInt16.toInt16_and (a b : UInt16) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := rfl
|
||||
@[simp] theorem UInt32.toInt32_and (a b : UInt32) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := rfl
|
||||
|
|
@ -104,3 +75,686 @@ theorem Bool.toBitVec_toISize {b : Bool} :
|
|||
@[simp] theorem UInt32.toInt32_not (a : UInt32) : (~~~a).toInt32 = ~~~a.toInt32 := rfl
|
||||
@[simp] theorem UInt64.toInt64_not (a : UInt64) : (~~~a).toInt64 = ~~~a.toInt64 := rfl
|
||||
@[simp] theorem USize.toISize_not (a : USize) : (~~~a).toISize = ~~~a.toISize := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_and (a b : Int8) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8 := rfl
|
||||
@[simp] theorem Int16.toUInt16_and (a b : Int16) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16 := rfl
|
||||
@[simp] theorem Int32.toUInt32_and (a b : Int32) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32 := rfl
|
||||
@[simp] theorem Int64.toUInt64_and (a b : Int64) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64 := rfl
|
||||
@[simp] theorem ISize.toUSize_and (a b : ISize) : (a &&& b).toUSize = a.toUSize &&& b.toUSize := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_or (a b : Int8) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8 := rfl
|
||||
@[simp] theorem Int16.toUInt16_or (a b : Int16) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16 := rfl
|
||||
@[simp] theorem Int32.toUInt32_or (a b : Int32) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32 := rfl
|
||||
@[simp] theorem Int64.toUInt64_or (a b : Int64) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64 := rfl
|
||||
@[simp] theorem ISize.toUSize_or (a b : ISize) : (a ||| b).toUSize = a.toUSize ||| b.toUSize := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_xor (a b : Int8) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8 := rfl
|
||||
@[simp] theorem Int16.toUInt16_xor (a b : Int16) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16 := rfl
|
||||
@[simp] theorem Int32.toUInt32_xor (a b : Int32) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32 := rfl
|
||||
@[simp] theorem Int64.toUInt64_xor (a b : Int64) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64 := rfl
|
||||
@[simp] theorem ISize.toUSize_xor (a b : ISize) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize := rfl
|
||||
|
||||
@[simp] theorem Int8.toUInt8_not (a : Int8) : (~~~a).toUInt8 = ~~~a.toUInt8 := rfl
|
||||
@[simp] theorem Int16.toUInt16_not (a : Int16) : (~~~a).toUInt16 = ~~~a.toUInt16 := rfl
|
||||
@[simp] theorem Int32.toUInt32_not (a : Int32) : (~~~a).toUInt32 = ~~~a.toUInt32 := rfl
|
||||
@[simp] theorem Int64.toUInt64_not (a : Int64) : (~~~a).toUInt64 = ~~~a.toUInt64 := rfl
|
||||
@[simp] theorem ISize.toUSize_not (a : ISize) : (~~~a).toUSize = ~~~a.toUSize := rfl
|
||||
|
||||
@[simp] theorem Int8.toInt16_and (a b : Int8) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt32_and (a b : Int8) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt64_and (a b : Int8) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toISize_and (a b : Int8) : (a &&& b).toISize = a.toISize &&& b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt8_and (a b : Int16) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt32_and (a b : Int16) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt64_and (a b : Int16) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toISize_and (a b : Int16) : (a &&& b).toISize = a.toISize &&& b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt8_and (a b : Int32) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt16_and (a b : Int32) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt64_and (a b : Int32) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toISize_and (a b : Int32) : (a &&& b).toISize = a.toISize &&& b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem ISize.toInt8_and (a b : ISize) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt16_and (a b : ISize) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt32_and (a b : ISize) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt64_and (a b : ISize) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int64.toInt8_and (a b : Int64) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt16_and (a b : Int64) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt32_and (a b : Int64) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toISize_and (a b : Int64) : (a &&& b).toISize = a.toISize &&& b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int8.toInt16_or (a b : Int8) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt32_or (a b : Int8) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt64_or (a b : Int8) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toISize_or (a b : Int8) : (a ||| b).toISize = a.toISize ||| b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt8_or (a b : Int16) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt32_or (a b : Int16) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt64_or (a b : Int16) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toISize_or (a b : Int16) : (a ||| b).toISize = a.toISize ||| b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt8_or (a b : Int32) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt16_or (a b : Int32) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt64_or (a b : Int32) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toISize_or (a b : Int32) : (a ||| b).toISize = a.toISize ||| b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem ISize.toInt8_or (a b : ISize) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt16_or (a b : ISize) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt32_or (a b : ISize) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt64_or (a b : ISize) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int64.toInt8_or (a b : Int64) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt16_or (a b : Int64) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt32_or (a b : Int64) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toISize_or (a b : Int64) : (a ||| b).toISize = a.toISize ||| b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int8.toInt16_xor (a b : Int8) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt32_xor (a b : Int8) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toInt64_xor (a b : Int8) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int8.toISize_xor (a b : Int8) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int16.toInt8_xor (a b : Int16) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt32_xor (a b : Int16) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toInt64_xor (a b : Int16) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int16.toISize_xor (a b : Int16) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int32.toInt8_xor (a b : Int32) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt16_xor (a b : Int32) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt64_xor (a b : Int32) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toISize_xor (a b : Int32) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem ISize.toInt8_xor (a b : ISize) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt16_xor (a b : ISize) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt32_xor (a b : ISize) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt64_xor (a b : ISize) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64 := Int64.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int64.toInt8_xor (a b : Int64) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt16_xor (a b : Int64) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt32_xor (a b : Int64) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toISize_xor (a b : Int64) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
theorem Int8.not_eq_neg_add (a : Int8) : ~~~a = -a - 1 := Int8.toBitVec_inj.1 (by simpa using BitVec.not_eq_neg_add _)
|
||||
theorem Int16.not_eq_neg_add (a : Int16) : ~~~a = -a - 1 := Int16.toBitVec_inj.1 (by simpa using BitVec.not_eq_neg_add _)
|
||||
theorem Int32.not_eq_neg_add (a : Int32) : ~~~a = -a - 1 := Int32.toBitVec_inj.1 (by simpa using BitVec.not_eq_neg_add _)
|
||||
theorem Int64.not_eq_neg_add (a : Int64) : ~~~a = -a - 1 := Int64.toBitVec_inj.1 (by simpa using BitVec.not_eq_neg_add _)
|
||||
theorem ISize.not_eq_neg_add (a : ISize) : ~~~a = -a - 1 := ISize.toBitVec_inj.1 (by simpa using BitVec.not_eq_neg_add _)
|
||||
|
||||
@[simp] theorem Int8.toInt_not (a : Int8) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 8) := by simp [Int8.not_eq_neg_add]
|
||||
@[simp] theorem Int16.toInt_not (a : Int16) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 16) := by simp [Int16.not_eq_neg_add]
|
||||
@[simp] theorem Int32.toInt_not (a : Int32) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 32) := by simp [Int32.not_eq_neg_add]
|
||||
@[simp] theorem Int64.toInt_not (a : Int64) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 64) := by simp [Int64.not_eq_neg_add]
|
||||
@[simp] theorem ISize.toInt_not (a : ISize) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ System.Platform.numBits) := by
|
||||
simp [ISize.not_eq_neg_add, toInt_neg]
|
||||
|
||||
@[simp] theorem Int16.toInt8_not (a : Int16) : (~~~a).toInt8 = ~~~a.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int32.toInt8_not (a : Int32) : (~~~a).toInt8 = ~~~a.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt8_not (a : Int64) : (~~~a).toInt8 = ~~~a.toInt8 := Int8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt8_not (a : ISize) : (~~~a).toInt8 = ~~~a.toInt8 := Int8.toBitVec_inj.1 (by simp [System.Platform.numBits_pos])
|
||||
|
||||
@[simp] theorem Int32.toInt16_not (a : Int32) : (~~~a).toInt16 = ~~~a.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem Int64.toInt16_not (a : Int64) : (~~~a).toInt16 = ~~~a.toInt16 := Int16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt16_not (a : ISize) : (~~~a).toInt16 = ~~~a.toInt16 := Int16.toBitVec_inj.1 (by simp [System.Platform.numBits_pos])
|
||||
|
||||
@[simp] theorem Int64.toInt32_not (a : Int64) : (~~~a).toInt32 = ~~~a.toInt32 := Int32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem ISize.toInt32_not (a : ISize) : (~~~a).toInt32 = ~~~a.toInt32 := Int32.toBitVec_inj.1 (by simp [System.Platform.numBits_pos])
|
||||
|
||||
@[simp] theorem Int64.toISize_not (a : Int64) : (~~~a).toISize = ~~~a.toISize := ISize.toBitVec_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_and (a b : BitVec 8) : Int8.ofBitVec (a &&& b) = Int8.ofBitVec a &&& Int8.ofBitVec b := rfl
|
||||
@[simp] theorem Int16.ofBitVec_and (a b : BitVec 16) : Int16.ofBitVec (a &&& b) = Int16.ofBitVec a &&& Int16.ofBitVec b := rfl
|
||||
@[simp] theorem Int32.ofBitVec_and (a b : BitVec 32) : Int32.ofBitVec (a &&& b) = Int32.ofBitVec a &&& Int32.ofBitVec b := rfl
|
||||
@[simp] theorem Int64.ofBitVec_and (a b : BitVec 64) : Int64.ofBitVec (a &&& b) = Int64.ofBitVec a &&& Int64.ofBitVec b := rfl
|
||||
@[simp] theorem ISize.ofBitVec_and (a b : BitVec System.Platform.numBits) : ISize.ofBitVec (a &&& b) = ISize.ofBitVec a &&& ISize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_or (a b : BitVec 8) : Int8.ofBitVec (a ||| b) = Int8.ofBitVec a ||| Int8.ofBitVec b := rfl
|
||||
@[simp] theorem Int16.ofBitVec_or (a b : BitVec 16) : Int16.ofBitVec (a ||| b) = Int16.ofBitVec a ||| Int16.ofBitVec b := rfl
|
||||
@[simp] theorem Int32.ofBitVec_or (a b : BitVec 32) : Int32.ofBitVec (a ||| b) = Int32.ofBitVec a ||| Int32.ofBitVec b := rfl
|
||||
@[simp] theorem Int64.ofBitVec_or (a b : BitVec 64) : Int64.ofBitVec (a ||| b) = Int64.ofBitVec a ||| Int64.ofBitVec b := rfl
|
||||
@[simp] theorem ISize.ofBitVec_or (a b : BitVec System.Platform.numBits) : ISize.ofBitVec (a ||| b) = ISize.ofBitVec a ||| ISize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_xor (a b : BitVec 8) : Int8.ofBitVec (a ^^^ b) = Int8.ofBitVec a ^^^ Int8.ofBitVec b := rfl
|
||||
@[simp] theorem Int16.ofBitVec_xor (a b : BitVec 16) : Int16.ofBitVec (a ^^^ b) = Int16.ofBitVec a ^^^ Int16.ofBitVec b := rfl
|
||||
@[simp] theorem Int32.ofBitVec_xor (a b : BitVec 32) : Int32.ofBitVec (a ^^^ b) = Int32.ofBitVec a ^^^ Int32.ofBitVec b := rfl
|
||||
@[simp] theorem Int64.ofBitVec_xor (a b : BitVec 64) : Int64.ofBitVec (a ^^^ b) = Int64.ofBitVec a ^^^ Int64.ofBitVec b := rfl
|
||||
@[simp] theorem ISize.ofBitVec_xor (a b : BitVec System.Platform.numBits) : ISize.ofBitVec (a ^^^ b) = ISize.ofBitVec a ^^^ ISize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_not (a : BitVec 8) : Int8.ofBitVec (~~~a) = ~~~Int8.ofBitVec a := rfl
|
||||
@[simp] theorem Int16.ofBitVec_not (a : BitVec 16) : Int16.ofBitVec (~~~a) = ~~~Int16.ofBitVec a := rfl
|
||||
@[simp] theorem Int32.ofBitVec_not (a : BitVec 32) : Int32.ofBitVec (~~~a) = ~~~Int32.ofBitVec a := rfl
|
||||
@[simp] theorem Int64.ofBitVec_not (a : BitVec 64) : Int64.ofBitVec (~~~a) = ~~~Int64.ofBitVec a := rfl
|
||||
@[simp] theorem ISize.ofBitVec_not (a : BitVec System.Platform.numBits) : ISize.ofBitVec (~~~a) = ~~~ISize.ofBitVec a := rfl
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_intMin : Int8.ofBitVec (BitVec.intMin 8) = Int8.minValue := rfl
|
||||
@[simp] theorem Int16.ofBitVec_intMin : Int16.ofBitVec (BitVec.intMin 16) = Int16.minValue := rfl
|
||||
@[simp] theorem Int32.ofBitVec_intMin : Int32.ofBitVec (BitVec.intMin 32) = Int32.minValue := rfl
|
||||
@[simp] theorem Int64.ofBitVec_intMin : Int64.ofBitVec (BitVec.intMin 64) = Int64.minValue := rfl
|
||||
@[simp] theorem ISize.ofBitVec_intMin : ISize.ofBitVec (BitVec.intMin System.Platform.numBits) = ISize.minValue :=
|
||||
ISize.toBitVec_inj.1 (by simp [BitVec.intMin_eq_neg_two_pow])
|
||||
|
||||
@[simp] theorem Int8.ofBitVec_intMax : Int8.ofBitVec (BitVec.intMax 8) = Int8.maxValue := rfl
|
||||
@[simp] theorem Int16.ofBitVec_intMax : Int16.ofBitVec (BitVec.intMax 16) = Int16.maxValue := rfl
|
||||
@[simp] theorem Int32.ofBitVec_intMax : Int32.ofBitVec (BitVec.intMax 32) = Int32.maxValue := rfl
|
||||
@[simp] theorem Int64.ofBitVec_intMax : Int64.ofBitVec (BitVec.intMax 64) = Int64.maxValue := rfl
|
||||
@[simp] theorem ISize.ofBitVec_intMax : ISize.ofBitVec (BitVec.intMax System.Platform.numBits) = ISize.maxValue :=
|
||||
ISize.toInt_inj.1 (by rw [toInt_ofBitVec, BitVec.toInt_intMax, toInt_maxValue])
|
||||
|
||||
theorem Int8.neg_eq_not_add (a : Int8) : -a = ~~~a + 1 := Int8.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem Int16.neg_eq_not_add (a : Int16) : -a = ~~~a + 1 := Int16.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem Int32.neg_eq_not_add (a : Int32) : -a = ~~~a + 1 := Int32.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem Int64.neg_eq_not_add (a : Int64) : -a = ~~~a + 1 := Int64.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem ISize.neg_eq_not_add (a : ISize) : -a = ~~~a + 1 := ISize.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
|
||||
theorem Int8.not_eq_neg_sub (a : Int8) : ~~~a = -a - 1 := Int8.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem Int16.not_eq_neg_sub (a : Int16) : ~~~a = -a - 1 := Int16.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem Int32.not_eq_neg_sub (a : Int32) : ~~~a = -a - 1 := Int32.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem Int64.not_eq_neg_sub (a : Int64) : ~~~a = -a - 1 := Int64.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem ISize.not_eq_neg_sub (a : ISize) : ~~~a = -a - 1 := ISize.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
|
||||
theorem Int8.or_assoc (a b c : Int8) : a ||| b ||| c = a ||| (b ||| c) := Int8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem Int16.or_assoc (a b c : Int16) : a ||| b ||| c = a ||| (b ||| c) := Int16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem Int32.or_assoc (a b c : Int32) : a ||| b ||| c = a ||| (b ||| c) := Int32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem Int64.or_assoc (a b c : Int64) : a ||| b ||| c = a ||| (b ||| c) := Int64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem ISize.or_assoc (a b c : ISize) : a ||| b ||| c = a ||| (b ||| c) := ISize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := Int8) (· ||| ·) := ⟨Int8.or_assoc⟩
|
||||
instance : Std.Associative (α := Int16) (· ||| ·) := ⟨Int16.or_assoc⟩
|
||||
instance : Std.Associative (α := Int32) (· ||| ·) := ⟨Int32.or_assoc⟩
|
||||
instance : Std.Associative (α := Int64) (· ||| ·) := ⟨Int64.or_assoc⟩
|
||||
instance : Std.Associative (α := ISize) (· ||| ·) := ⟨ISize.or_assoc⟩
|
||||
|
||||
theorem Int8.or_comm (a b : Int8) : a ||| b = b ||| a := Int8.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem Int16.or_comm (a b : Int16) : a ||| b = b ||| a := Int16.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem Int32.or_comm (a b : Int32) : a ||| b = b ||| a := Int32.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem Int64.or_comm (a b : Int64) : a ||| b = b ||| a := Int64.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem ISize.or_comm (a b : ISize) : a ||| b = b ||| a := ISize.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := Int8) (· ||| ·) := ⟨Int8.or_comm⟩
|
||||
instance : Std.Commutative (α := Int16) (· ||| ·) := ⟨Int16.or_comm⟩
|
||||
instance : Std.Commutative (α := Int32) (· ||| ·) := ⟨Int32.or_comm⟩
|
||||
instance : Std.Commutative (α := Int64) (· ||| ·) := ⟨Int64.or_comm⟩
|
||||
instance : Std.Commutative (α := ISize) (· ||| ·) := ⟨ISize.or_comm⟩
|
||||
|
||||
@[simp] theorem Int8.or_self {a : Int8} : a ||| a = a := Int8.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem Int16.or_self {a : Int16} : a ||| a = a := Int16.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem Int32.or_self {a : Int32} : a ||| a = a := Int32.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem Int64.or_self {a : Int64} : a ||| a = a := Int64.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem ISize.or_self {a : ISize} : a ||| a = a := ISize.toBitVec_inj.1 BitVec.or_self
|
||||
|
||||
instance : Std.IdempotentOp (α := Int8) (· ||| ·) := ⟨fun _ => Int8.or_self⟩
|
||||
instance : Std.IdempotentOp (α := Int16) (· ||| ·) := ⟨fun _ => Int16.or_self⟩
|
||||
instance : Std.IdempotentOp (α := Int32) (· ||| ·) := ⟨fun _ => Int32.or_self⟩
|
||||
instance : Std.IdempotentOp (α := Int64) (· ||| ·) := ⟨fun _ => Int64.or_self⟩
|
||||
instance : Std.IdempotentOp (α := ISize) (· ||| ·) := ⟨fun _ => ISize.or_self⟩
|
||||
|
||||
@[simp] theorem Int8.or_zero {a : Int8} : a ||| 0 = a := Int8.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem Int16.or_zero {a : Int16} : a ||| 0 = a := Int16.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem Int32.or_zero {a : Int32} : a ||| 0 = a := Int32.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem Int64.or_zero {a : Int64} : a ||| 0 = a := Int64.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem ISize.or_zero {a : ISize} : a ||| 0 = a := ISize.toBitVec_inj.1 BitVec.or_zero
|
||||
|
||||
@[simp] theorem Int8.zero_or {a : Int8} : 0 ||| a = a := Int8.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem Int16.zero_or {a : Int16} : 0 ||| a = a := Int16.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem Int32.zero_or {a : Int32} : 0 ||| a = a := Int32.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem Int64.zero_or {a : Int64} : 0 ||| a = a := Int64.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem ISize.zero_or {a : ISize} : 0 ||| a = a := ISize.toBitVec_inj.1 BitVec.zero_or
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := Int8) (· ||| ·) 0 where
|
||||
right_id _ := Int8.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int16) (· ||| ·) 0 where
|
||||
right_id _ := Int16.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int32) (· ||| ·) 0 where
|
||||
right_id _ := Int32.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int64) (· ||| ·) 0 where
|
||||
right_id _ := Int64.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := ISize) (· ||| ·) 0 where
|
||||
right_id _ := ISize.or_zero
|
||||
|
||||
@[simp] theorem Int8.neg_one_or {a : Int8} : -1 ||| a = -1 := by
|
||||
rw [← Int8.toBitVec_inj, Int8.toBitVec_or, Int8.toBitVec_neg, Int8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem Int16.neg_one_or {a : Int16} : -1 ||| a = -1 := by
|
||||
rw [← Int16.toBitVec_inj, Int16.toBitVec_or, Int16.toBitVec_neg, Int16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem Int32.neg_one_or {a : Int32} : -1 ||| a = -1 := by
|
||||
rw [← Int32.toBitVec_inj, Int32.toBitVec_or, Int32.toBitVec_neg, Int32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem Int64.neg_one_or {a : Int64} : -1 ||| a = -1 := by
|
||||
rw [← Int64.toBitVec_inj, Int64.toBitVec_or, Int64.toBitVec_neg, Int64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem ISize.neg_one_or {a : ISize} : -1 ||| a = -1 := by
|
||||
rw [← ISize.toBitVec_inj, ISize.toBitVec_or, ISize.toBitVec_neg, ISize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
|
||||
@[simp] theorem Int8.or_neg_one {a : Int8} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem Int16.or_neg_one {a : Int16} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem Int32.or_neg_one {a : Int32} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem Int64.or_neg_one {a : Int64} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem ISize.or_neg_one {a : ISize} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
|
||||
@[simp] theorem Int8.or_eq_zero_iff {a b : Int8} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.or_eq_zero_iff {a b : Int16} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.or_eq_zero_iff {a b : Int32} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.or_eq_zero_iff {a b : Int64} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.or_eq_zero_iff {a b : ISize} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← ISize.toBitVec_inj]
|
||||
|
||||
theorem Int8.and_assoc (a b c : Int8) : a &&& b &&& c = a &&& (b &&& c) := Int8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem Int16.and_assoc (a b c : Int16) : a &&& b &&& c = a &&& (b &&& c) := Int16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem Int32.and_assoc (a b c : Int32) : a &&& b &&& c = a &&& (b &&& c) := Int32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem Int64.and_assoc (a b c : Int64) : a &&& b &&& c = a &&& (b &&& c) := Int64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem ISize.and_assoc (a b c : ISize) : a &&& b &&& c = a &&& (b &&& c) := ISize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := Int8) (· &&& ·) := ⟨Int8.and_assoc⟩
|
||||
instance : Std.Associative (α := Int16) (· &&& ·) := ⟨Int16.and_assoc⟩
|
||||
instance : Std.Associative (α := Int32) (· &&& ·) := ⟨Int32.and_assoc⟩
|
||||
instance : Std.Associative (α := Int64) (· &&& ·) := ⟨Int64.and_assoc⟩
|
||||
instance : Std.Associative (α := ISize) (· &&& ·) := ⟨ISize.and_assoc⟩
|
||||
|
||||
theorem Int8.and_comm (a b : Int8) : a &&& b = b &&& a := Int8.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem Int16.and_comm (a b : Int16) : a &&& b = b &&& a := Int16.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem Int32.and_comm (a b : Int32) : a &&& b = b &&& a := Int32.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem Int64.and_comm (a b : Int64) : a &&& b = b &&& a := Int64.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem ISize.and_comm (a b : ISize) : a &&& b = b &&& a := ISize.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := Int8) (· &&& ·) := ⟨Int8.and_comm⟩
|
||||
instance : Std.Commutative (α := Int16) (· &&& ·) := ⟨Int16.and_comm⟩
|
||||
instance : Std.Commutative (α := Int32) (· &&& ·) := ⟨Int32.and_comm⟩
|
||||
instance : Std.Commutative (α := Int64) (· &&& ·) := ⟨Int64.and_comm⟩
|
||||
instance : Std.Commutative (α := ISize) (· &&& ·) := ⟨ISize.and_comm⟩
|
||||
|
||||
@[simp] theorem Int8.and_self {a : Int8} : a &&& a = a := Int8.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem Int16.and_self {a : Int16} : a &&& a = a := Int16.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem Int32.and_self {a : Int32} : a &&& a = a := Int32.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem Int64.and_self {a : Int64} : a &&& a = a := Int64.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem ISize.and_self {a : ISize} : a &&& a = a := ISize.toBitVec_inj.1 BitVec.and_self
|
||||
|
||||
instance : Std.IdempotentOp (α := Int8) (· &&& ·) := ⟨fun _ => Int8.and_self⟩
|
||||
instance : Std.IdempotentOp (α := Int16) (· &&& ·) := ⟨fun _ => Int16.and_self⟩
|
||||
instance : Std.IdempotentOp (α := Int32) (· &&& ·) := ⟨fun _ => Int32.and_self⟩
|
||||
instance : Std.IdempotentOp (α := Int64) (· &&& ·) := ⟨fun _ => Int64.and_self⟩
|
||||
instance : Std.IdempotentOp (α := ISize) (· &&& ·) := ⟨fun _ => ISize.and_self⟩
|
||||
|
||||
@[simp] theorem Int8.and_zero {a : Int8} : a &&& 0 = 0 := Int8.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem Int16.and_zero {a : Int16} : a &&& 0 = 0 := Int16.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem Int32.and_zero {a : Int32} : a &&& 0 = 0 := Int32.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem Int64.and_zero {a : Int64} : a &&& 0 = 0 := Int64.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem ISize.and_zero {a : ISize} : a &&& 0 = 0 := ISize.toBitVec_inj.1 BitVec.and_zero
|
||||
|
||||
@[simp] theorem Int8.zero_and {a : Int8} : 0 &&& a = 0 := Int8.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem Int16.zero_and {a : Int16} : 0 &&& a = 0 := Int16.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem Int32.zero_and {a : Int32} : 0 &&& a = 0 := Int32.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem Int64.zero_and {a : Int64} : 0 &&& a = 0 := Int64.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem ISize.zero_and {a : ISize} : 0 &&& a = 0 := ISize.toBitVec_inj.1 BitVec.zero_and
|
||||
|
||||
@[simp] theorem Int8.neg_one_and {a : Int8} : -1 &&& a = a := by
|
||||
rw [← Int8.toBitVec_inj, Int8.toBitVec_and, Int8.toBitVec_neg, Int8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem Int16.neg_one_and {a : Int16} : -1 &&& a = a := by
|
||||
rw [← Int16.toBitVec_inj, Int16.toBitVec_and, Int16.toBitVec_neg, Int16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem Int32.neg_one_and {a : Int32} : -1 &&& a = a := by
|
||||
rw [← Int32.toBitVec_inj, Int32.toBitVec_and, Int32.toBitVec_neg, Int32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem Int64.neg_one_and {a : Int64} : -1 &&& a = a := by
|
||||
rw [← Int64.toBitVec_inj, Int64.toBitVec_and, Int64.toBitVec_neg, Int64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem ISize.neg_one_and {a : ISize} : -1 &&& a = a := by
|
||||
rw [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
|
||||
@[simp] theorem Int8.and_neg_one {a : Int8} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem Int16.and_neg_one {a : Int16} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem Int32.and_neg_one {a : Int32} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem Int64.and_neg_one {a : Int64} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem ISize.and_neg_one {a : ISize} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := Int8) (· &&& ·) (-1) where
|
||||
right_id _ := Int8.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := Int16) (· &&& ·) (-1) where
|
||||
right_id _ := Int16.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := Int32) (· &&& ·) (-1) where
|
||||
right_id _ := Int32.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := Int64) (· &&& ·) (-1) where
|
||||
right_id _ := Int64.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := ISize) (· &&& ·) (-1) where
|
||||
right_id _ := ISize.and_neg_one
|
||||
|
||||
@[simp] theorem Int8.and_eq_neg_one_iff {a b : Int8} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← Int8.toBitVec_inj, Int8.toBitVec_and, Int8.toBitVec_neg, Int8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem Int16.and_eq_neg_one_iff {a b : Int16} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← Int16.toBitVec_inj, Int16.toBitVec_and, Int16.toBitVec_neg, Int16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem Int32.and_eq_neg_one_iff {a b : Int32} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← Int32.toBitVec_inj, Int32.toBitVec_and, Int32.toBitVec_neg, Int32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem Int64.and_eq_neg_one_iff {a b : Int64} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← Int64.toBitVec_inj, Int64.toBitVec_and, Int64.toBitVec_neg, Int64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem ISize.and_eq_neg_one_iff {a b : ISize} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
|
||||
theorem Int8.xor_assoc (a b c : Int8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem Int16.xor_assoc (a b c : Int16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem Int32.xor_assoc (a b c : Int32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem Int64.xor_assoc (a b c : Int64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem ISize.xor_assoc (a b c : ISize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := ISize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := Int8) (· ^^^ ·) := ⟨Int8.xor_assoc⟩
|
||||
instance : Std.Associative (α := Int16) (· ^^^ ·) := ⟨Int16.xor_assoc⟩
|
||||
instance : Std.Associative (α := Int32) (· ^^^ ·) := ⟨Int32.xor_assoc⟩
|
||||
instance : Std.Associative (α := Int64) (· ^^^ ·) := ⟨Int64.xor_assoc⟩
|
||||
instance : Std.Associative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_assoc⟩
|
||||
|
||||
theorem Int8.xor_comm (a b : Int8) : a ^^^ b = b ^^^ a := Int8.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem Int16.xor_comm (a b : Int16) : a ^^^ b = b ^^^ a := Int16.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem Int32.xor_comm (a b : Int32) : a ^^^ b = b ^^^ a := Int32.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem Int64.xor_comm (a b : Int64) : a ^^^ b = b ^^^ a := Int64.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem ISize.xor_comm (a b : ISize) : a ^^^ b = b ^^^ a := ISize.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := Int8) (· ^^^ ·) := ⟨Int8.xor_comm⟩
|
||||
instance : Std.Commutative (α := Int16) (· ^^^ ·) := ⟨Int16.xor_comm⟩
|
||||
instance : Std.Commutative (α := Int32) (· ^^^ ·) := ⟨Int32.xor_comm⟩
|
||||
instance : Std.Commutative (α := Int64) (· ^^^ ·) := ⟨Int64.xor_comm⟩
|
||||
instance : Std.Commutative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_comm⟩
|
||||
|
||||
@[simp] theorem Int8.xor_self {a : Int8} : a ^^^ a = 0 := Int8.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem Int16.xor_self {a : Int16} : a ^^^ a = 0 := Int16.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem Int32.xor_self {a : Int32} : a ^^^ a = 0 := Int32.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem Int64.xor_self {a : Int64} : a ^^^ a = 0 := Int64.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem ISize.xor_self {a : ISize} : a ^^^ a = 0 := ISize.toBitVec_inj.1 BitVec.xor_self
|
||||
|
||||
@[simp] theorem Int8.xor_zero {a : Int8} : a ^^^ 0 = a := Int8.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem Int16.xor_zero {a : Int16} : a ^^^ 0 = a := Int16.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem Int32.xor_zero {a : Int32} : a ^^^ 0 = a := Int32.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem Int64.xor_zero {a : Int64} : a ^^^ 0 = a := Int64.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem ISize.xor_zero {a : ISize} : a ^^^ 0 = a := ISize.toBitVec_inj.1 BitVec.xor_zero
|
||||
|
||||
@[simp] theorem Int8.zero_xor {a : Int8} : 0 ^^^ a = a := Int8.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem Int16.zero_xor {a : Int16} : 0 ^^^ a = a := Int16.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem Int32.zero_xor {a : Int32} : 0 ^^^ a = a := Int32.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem Int64.zero_xor {a : Int64} : 0 ^^^ a = a := Int64.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem ISize.zero_xor {a : ISize} : 0 ^^^ a = a := ISize.toBitVec_inj.1 BitVec.zero_xor
|
||||
|
||||
@[simp] theorem Int8.neg_one_xor {a : Int8} : -1 ^^^ a = ~~~a := by
|
||||
rw [← Int8.toBitVec_inj, Int8.toBitVec_xor, Int8.toBitVec_neg, Int8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int8.toBitVec_not]
|
||||
@[simp] theorem Int16.neg_one_xor {a : Int16} : -1 ^^^ a = ~~~a := by
|
||||
rw [← Int16.toBitVec_inj, Int16.toBitVec_xor, Int16.toBitVec_neg, Int16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int16.toBitVec_not]
|
||||
@[simp] theorem Int32.neg_one_xor {a : Int32} : -1 ^^^ a = ~~~a := by
|
||||
rw [← Int32.toBitVec_inj, Int32.toBitVec_xor, Int32.toBitVec_neg, Int32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int32.toBitVec_not]
|
||||
@[simp] theorem Int64.neg_one_xor {a : Int64} : -1 ^^^ a = ~~~a := by
|
||||
rw [← Int64.toBitVec_inj, Int64.toBitVec_xor, Int64.toBitVec_neg, Int64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, Int64.toBitVec_not]
|
||||
@[simp] theorem ISize.neg_one_xor {a : ISize} : -1 ^^^ a = ~~~a := by
|
||||
rw [← ISize.toBitVec_inj, ISize.toBitVec_xor, ISize.toBitVec_neg, ISize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, ISize.toBitVec_not]
|
||||
|
||||
@[simp] theorem Int8.xor_neg_one {a : Int8} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem Int16.xor_neg_one {a : Int16} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem Int32.xor_neg_one {a : Int32} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem Int64.xor_neg_one {a : Int64} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem ISize.xor_neg_one {a : ISize} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := Int8) (· ^^^ ·) 0 where
|
||||
right_id _ := Int8.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int16) (· ^^^ ·) 0 where
|
||||
right_id _ := Int16.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int32) (· ^^^ ·) 0 where
|
||||
right_id _ := Int32.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := Int64) (· ^^^ ·) 0 where
|
||||
right_id _ := Int64.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := ISize) (· ^^^ ·) 0 where
|
||||
right_id _ := ISize.xor_zero
|
||||
|
||||
@[simp] theorem Int8.xor_eq_zero_iff {a b : Int8} : a ^^^ b = 0 ↔ a = b := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.xor_eq_zero_iff {a b : Int16} : a ^^^ b = 0 ↔ a = b := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.xor_eq_zero_iff {a b : Int32} : a ^^^ b = 0 ↔ a = b := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.xor_eq_zero_iff {a b : Int64} : a ^^^ b = 0 ↔ a = b := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.xor_eq_zero_iff {a b : ISize} : a ^^^ b = 0 ↔ a = b := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.xor_left_inj {a b : Int8} (c : Int8) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.xor_left_inj {a b : Int16} (c : Int16) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.xor_left_inj {a b : Int32} (c : Int32) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.xor_left_inj {a b : Int64} (c : Int64) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.xor_left_inj {a b : ISize} (c : ISize) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.xor_right_inj {a b : Int8} (c : Int8) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.xor_right_inj {a b : Int16} (c : Int16) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.xor_right_inj {a b : Int32} (c : Int32) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.xor_right_inj {a b : Int64} (c : Int64) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.xor_right_inj {a b : ISize} (c : ISize) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.not_zero : ~~~(0 : Int8) = -1 := rfl
|
||||
@[simp] theorem Int16.not_zero : ~~~(0 : Int16) = -1 := rfl
|
||||
@[simp] theorem Int32.not_zero : ~~~(0 : Int32) = -1 := rfl
|
||||
@[simp] theorem Int64.not_zero : ~~~(0 : Int64) = -1 := rfl
|
||||
@[simp] theorem ISize.not_zero : ~~~(0 : ISize) = -1 := by simp [ISize.not_eq_neg_sub]
|
||||
|
||||
@[simp] theorem Int8.not_neg_one : ~~~(-1 : Int8) = 0 := rfl
|
||||
@[simp] theorem Int16.not_neg_one : ~~~(-1 : Int16) = 0 := rfl
|
||||
@[simp] theorem Int32.not_neg_one : ~~~(-1 : Int32) = 0 := rfl
|
||||
@[simp] theorem Int64.not_neg_one : ~~~(-1 : Int64) = 0 := rfl
|
||||
@[simp] theorem ISize.not_neg_one : ~~~(-1 : ISize) = 0 := by simp [ISize.not_eq_neg_sub]
|
||||
|
||||
@[simp] theorem Int8.not_not {a : Int8} : ~~~(~~~a) = a := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.not_not {a : Int16} : ~~~(~~~a) = a := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.not_not {a : Int32} : ~~~(~~~a) = a := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.not_not {a : Int64} : ~~~(~~~a) = a := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.not_not {a : ISize} : ~~~(~~~a) = a := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.not_inj {a b : Int8} : ~~~a = ~~~b ↔ a = b := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.not_inj {a b : Int16} : ~~~a = ~~~b ↔ a = b := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.not_inj {a b : Int32} : ~~~a = ~~~b ↔ a = b := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.not_inj {a b : Int64} : ~~~a = ~~~b ↔ a = b := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.not_inj {a b : ISize} : ~~~a = ~~~b ↔ a = b := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.and_not_self {a : Int8} : a &&& ~~~a = 0 := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.and_not_self {a : Int16} : a &&& ~~~a = 0 := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.and_not_self {a : Int32} : a &&& ~~~a = 0 := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.and_not_self {a : Int64} : a &&& ~~~a = 0 := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.and_not_self {a : ISize} : a &&& ~~~a = 0 := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.not_and_self {a : Int8} : ~~~a &&& a = 0 := by simp [Int8.and_comm]
|
||||
@[simp] theorem Int16.not_and_self {a : Int16} : ~~~a &&& a = 0 := by simp [Int16.and_comm]
|
||||
@[simp] theorem Int32.not_and_self {a : Int32} : ~~~a &&& a = 0 := by simp [Int32.and_comm]
|
||||
@[simp] theorem Int64.not_and_self {a : Int64} : ~~~a &&& a = 0 := by simp [Int64.and_comm]
|
||||
@[simp] theorem ISize.not_and_self {a : ISize} : ~~~a &&& a = 0 := by simp [ISize.and_comm]
|
||||
|
||||
@[simp] theorem Int8.or_not_self {a : Int8} : a ||| ~~~a = -1 := by
|
||||
rw [← Int8.toBitVec_inj, Int8.toBitVec_or, Int8.toBitVec_not, BitVec.or_not_self,
|
||||
Int8.toBitVec_neg, Int8.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem Int16.or_not_self {a : Int16} : a ||| ~~~a = -1 := by
|
||||
rw [← Int16.toBitVec_inj, Int16.toBitVec_or, Int16.toBitVec_not, BitVec.or_not_self,
|
||||
Int16.toBitVec_neg, Int16.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem Int32.or_not_self {a : Int32} : a ||| ~~~a = -1 := by
|
||||
rw [← Int32.toBitVec_inj, Int32.toBitVec_or, Int32.toBitVec_not, BitVec.or_not_self,
|
||||
Int32.toBitVec_neg, Int32.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem Int64.or_not_self {a : Int64} : a ||| ~~~a = -1 := by
|
||||
rw [← Int64.toBitVec_inj, Int64.toBitVec_or, Int64.toBitVec_not, BitVec.or_not_self,
|
||||
Int64.toBitVec_neg, Int64.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem ISize.or_not_self {a : ISize} : a ||| ~~~a = -1 := by
|
||||
rw [← ISize.toBitVec_inj, ISize.toBitVec_or, ISize.toBitVec_not, BitVec.or_not_self,
|
||||
ISize.toBitVec_neg, ISize.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
|
||||
@[simp] theorem Int8.not_or_self {a : Int8} : ~~~a ||| a = -1 := by simp [Int8.or_comm]
|
||||
@[simp] theorem Int16.not_or_self {a : Int16} : ~~~a ||| a = -1 := by simp [Int16.or_comm]
|
||||
@[simp] theorem Int32.not_or_self {a : Int32} : ~~~a ||| a = -1 := by simp [Int32.or_comm]
|
||||
@[simp] theorem Int64.not_or_self {a : Int64} : ~~~a ||| a = -1 := by simp [Int64.or_comm]
|
||||
@[simp] theorem ISize.not_or_self {a : ISize} : ~~~a ||| a = -1 := by simp [ISize.or_comm]
|
||||
|
||||
theorem Int8.not_eq_comm {a b : Int8} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem Int16.not_eq_comm {a b : Int16} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem Int32.not_eq_comm {a b : Int32} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem Int64.not_eq_comm {a b : Int64} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem ISize.not_eq_comm {a b : ISize} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.not_eq_comm]
|
||||
|
||||
@[simp] theorem Int8.ne_not_self {a : Int8} : a ≠ ~~~a := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.ne_not_self {a : Int16} : a ≠ ~~~a := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.ne_not_self {a : Int32} : a ≠ ~~~a := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.ne_not_self {a : Int64} : a ≠ ~~~a := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.ne_not_self {a : ISize} : a ≠ ~~~a := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.not_ne_self {a : Int8} : ~~~a ≠ a := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.not_ne_self {a : Int16} : ~~~a ≠ a := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.not_ne_self {a : Int32} : ~~~a ≠ a := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.not_ne_self {a : Int64} : ~~~a ≠ a := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.not_ne_self {a : ISize} : ~~~a ≠ a := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
theorem Int8.not_xor {a b : Int8} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem Int16.not_xor {a b : Int16} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem Int32.not_xor {a b : Int32} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem Int64.not_xor {a b : Int64} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem ISize.not_xor {a b : ISize} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.not_xor_left]
|
||||
|
||||
theorem Int8.xor_not {a b : Int8} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem Int16.xor_not {a b : Int16} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem Int32.xor_not {a b : Int32} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem Int64.xor_not {a b : Int64} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem ISize.xor_not {a b : ISize} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.not_xor_right]
|
||||
|
||||
@[simp] theorem Int8.shiftLeft_zero {a : Int8} : a <<< 0 = a := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.shiftLeft_zero {a : Int16} : a <<< 0 = a := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.shiftLeft_zero {a : Int32} : a <<< 0 = a := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.shiftLeft_zero {a : Int64} : a <<< 0 = a := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.shiftLeft_zero {a : ISize} : a <<< 0 = a := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.zero_shiftLeft {a : Int8} : 0 <<< a = 0 := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.zero_shiftLeft {a : Int16} : 0 <<< a = 0 := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.zero_shiftLeft {a : Int32} : 0 <<< a = 0 := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.zero_shiftLeft {a : Int64} : 0 <<< a = 0 := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.zero_shiftLeft {a : ISize} : 0 <<< a = 0 := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
theorem Int8.shiftLeft_xor {a b c : Int8} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem Int16.shiftLeft_xor {a b c : Int16} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem Int32.shiftLeft_xor {a b c : Int32} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem Int64.shiftLeft_xor {a b c : Int64} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem ISize.shiftLeft_xor {a b c : ISize} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
|
||||
theorem Int8.shiftLeft_and {a b c : Int8} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem Int16.shiftLeft_and {a b c : Int16} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem Int32.shiftLeft_and {a b c : Int32} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem Int64.shiftLeft_and {a b c : Int64} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem ISize.shiftLeft_and {a b c : ISize} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
|
||||
theorem Int8.shiftLeft_or {a b c : Int8} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem Int16.shiftLeft_or {a b c : Int16} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem Int32.shiftLeft_or {a b c : Int32} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem Int64.shiftLeft_or {a b c : Int64} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem ISize.shiftLeft_or {a b c : ISize} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
|
||||
@[simp] theorem Int8.neg_one_shiftLeft_and_shiftLeft {a b : Int8} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← Int8.shiftLeft_and]
|
||||
@[simp] theorem Int16.neg_one_shiftLeft_and_shiftLeft {a b : Int16} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← Int16.shiftLeft_and]
|
||||
@[simp] theorem Int32.neg_one_shiftLeft_and_shiftLeft {a b : Int32} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← Int32.shiftLeft_and]
|
||||
@[simp] theorem Int64.neg_one_shiftLeft_and_shiftLeft {a b : Int64} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← Int64.shiftLeft_and]
|
||||
@[simp] theorem ISize.neg_one_shiftLeft_and_shiftLeft {a b : ISize} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← ISize.shiftLeft_and]
|
||||
|
||||
@[simp] theorem Int8.neg_one_shiftLeft_or_shiftLeft {a b : Int8} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int8.shiftLeft_or]
|
||||
@[simp] theorem Int16.neg_one_shiftLeft_or_shiftLeft {a b : Int16} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int16.shiftLeft_or]
|
||||
@[simp] theorem Int32.neg_one_shiftLeft_or_shiftLeft {a b : Int32} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int32.shiftLeft_or]
|
||||
@[simp] theorem Int64.neg_one_shiftLeft_or_shiftLeft {a b : Int8} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int64.shiftLeft_or]
|
||||
@[simp] theorem ISize.neg_one_shiftLeft_or_shiftLeft {a b : ISize} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← ISize.shiftLeft_or]
|
||||
|
||||
@[simp] theorem Int8.shiftRight_zero {a : Int8} : a >>> 0 = a := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.shiftRight_zero {a : Int16} : a >>> 0 = a := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.shiftRight_zero {a : Int32} : a >>> 0 = a := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.shiftRight_zero {a : Int64} : a >>> 0 = a := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.shiftRight_zero {a : ISize} : a >>> 0 = a := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem Int8.zero_shiftRight {a : Int8} : 0 >>> a = 0 := by simp [← Int8.toBitVec_inj]
|
||||
@[simp] theorem Int16.zero_shiftRight {a : Int16} : 0 >>> a = 0 := by simp [← Int16.toBitVec_inj]
|
||||
@[simp] theorem Int32.zero_shiftRight {a : Int32} : 0 >>> a = 0 := by simp [← Int32.toBitVec_inj]
|
||||
@[simp] theorem Int64.zero_shiftRight {a : Int64} : 0 >>> a = 0 := by simp [← Int64.toBitVec_inj]
|
||||
@[simp] theorem ISize.zero_shiftRight {a : ISize} : 0 >>> a = 0 := by simp [← ISize.toBitVec_inj]
|
||||
|
||||
theorem Int8.shiftRight_xor {a b c : Int8} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.sshiftRight_xor_distrib]
|
||||
theorem Int16.shiftRight_xor {a b c : Int16} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.sshiftRight_xor_distrib]
|
||||
theorem Int32.shiftRight_xor {a b c : Int32} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.sshiftRight_xor_distrib]
|
||||
theorem Int64.shiftRight_xor {a b c : Int64} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.sshiftRight_xor_distrib]
|
||||
theorem ISize.shiftRight_xor {a b c : ISize} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.sshiftRight_xor_distrib]
|
||||
|
||||
theorem Int8.shiftRight_and {a b c : Int8} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.sshiftRight_and_distrib]
|
||||
theorem Int16.shiftRight_and {a b c : Int16} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.sshiftRight_and_distrib]
|
||||
theorem Int32.shiftRight_and {a b c : Int32} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.sshiftRight_and_distrib]
|
||||
theorem Int64.shiftRight_and {a b c : Int64} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.sshiftRight_and_distrib]
|
||||
theorem ISize.shiftRight_and {a b c : ISize} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.sshiftRight_and_distrib]
|
||||
|
||||
theorem Int8.shiftRight_or {a b c : Int8} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← Int8.toBitVec_inj, BitVec.sshiftRight_or_distrib]
|
||||
theorem Int16.shiftRight_or {a b c : Int16} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← Int16.toBitVec_inj, BitVec.sshiftRight_or_distrib]
|
||||
theorem Int32.shiftRight_or {a b c : Int32} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← Int32.toBitVec_inj, BitVec.sshiftRight_or_distrib]
|
||||
theorem Int64.shiftRight_or {a b c : Int64} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← Int64.toBitVec_inj, BitVec.sshiftRight_or_distrib]
|
||||
theorem ISize.shiftRight_or {a b c : ISize} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← ISize.toBitVec_inj, BitVec.sshiftRight_or_distrib]
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -229,7 +229,6 @@ theorem Bool.toBitVec_toUSize {b : Bool} :
|
|||
@[simp] theorem USize.toFin_shiftLeft (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toFin = a.toFin <<< b.toFin :=
|
||||
Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := System.Platform.numBits) hb])
|
||||
|
||||
|
||||
theorem UInt8.shiftLeft_eq_shiftLeft_mod (a b : UInt8) : a <<< b = a <<< (b % 8) := UInt8.toBitVec_inj.1 (by simp)
|
||||
theorem UInt16.shiftLeft_eq_shiftLeft_mod (a b : UInt16) : a <<< b = a <<< (b % 16) := UInt16.toBitVec_inj.1 (by simp)
|
||||
theorem UInt32.shiftLeft_eq_shiftLeft_mod (a b : UInt32) : a <<< b = a <<< (b % 32) := UInt32.toBitVec_inj.1 (by simp)
|
||||
|
|
@ -423,3 +422,904 @@ theorem USize.toUInt64_shiftLeft_of_lt (a b : USize) (hb : b.toNat < System.Plat
|
|||
There is no reasonable statement for`UInt16.toUInt8_shiftRight`; in fact for `a b : UInt16` the
|
||||
expression `(a >>> b).toUInt8` is not a function of `a.toUInt8` and `b.toUInt8`.
|
||||
-/
|
||||
|
||||
@[simp] theorem UInt8.ofFin_and (a b : Fin UInt8.size) : UInt8.ofFin (a &&& b) = UInt8.ofFin a &&& UInt8.ofFin b := UInt8.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofFin_and (a b : Fin UInt16.size) : UInt16.ofFin (a &&& b) = UInt16.ofFin a &&& UInt16.ofFin b := UInt16.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofFin_and (a b : Fin UInt32.size) : UInt32.ofFin (a &&& b) = UInt32.ofFin a &&& UInt32.ofFin b := UInt32.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofFin_and (a b : Fin UInt64.size) : UInt64.ofFin (a &&& b) = UInt64.ofFin a &&& UInt64.ofFin b := UInt64.toFin_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofFin_and (a b : Fin USize.size) : USize.ofFin (a &&& b) = USize.ofFin a &&& USize.ofFin b := USize.toFin_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_and (a b : BitVec 8) : UInt8.ofBitVec (a &&& b) = UInt8.ofBitVec a &&& UInt8.ofBitVec b := rfl
|
||||
@[simp] theorem UInt16.ofBitVec_and (a b : BitVec 16) : UInt16.ofBitVec (a &&& b) = UInt16.ofBitVec a &&& UInt16.ofBitVec b := rfl
|
||||
@[simp] theorem UInt32.ofBitVec_and (a b : BitVec 32) : UInt32.ofBitVec (a &&& b) = UInt32.ofBitVec a &&& UInt32.ofBitVec b := rfl
|
||||
@[simp] theorem UInt64.ofBitVec_and (a b : BitVec 64) : UInt64.ofBitVec (a &&& b) = UInt64.ofBitVec a &&& UInt64.ofBitVec b := rfl
|
||||
@[simp] theorem USize.ofBitVec_and (a b : BitVec System.Platform.numBits) : USize.ofBitVec (a &&& b) = USize.ofBitVec a &&& USize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem UInt8.ofNat_and (a b : Nat) : UInt8.ofNat (a &&& b) = UInt8.ofNat a &&& UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp [UInt8.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt16.ofNat_and (a b : Nat) : UInt16.ofNat (a &&& b) = UInt16.ofNat a &&& UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp [UInt16.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt32.ofNat_and (a b : Nat) : UInt32.ofNat (a &&& b) = UInt32.ofNat a &&& UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp [UInt32.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt64.ofNat_and (a b : Nat) : UInt64.ofNat (a &&& b) = UInt64.ofNat a &&& UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp [UInt64.toBitVec_ofNat'])
|
||||
@[simp] theorem USize.ofNat_and (a b : Nat) : USize.ofNat (a &&& b) = USize.ofNat a &&& USize.ofNat b :=
|
||||
USize.toBitVec_inj.1 (by simp [USize.toBitVec_ofNat'])
|
||||
|
||||
@[simp] theorem UInt8.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) :
|
||||
UInt8.ofNatLT (a &&& b) (Nat.and_lt_two_pow _ hb) = UInt8.ofNatLT a ha &&& UInt8.ofNatLT b hb := by
|
||||
simp [UInt8.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt16.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) :
|
||||
UInt16.ofNatLT (a &&& b) (Nat.and_lt_two_pow _ hb) = UInt16.ofNatLT a ha &&& UInt16.ofNatLT b hb := by
|
||||
simp [UInt16.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt32.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) :
|
||||
UInt32.ofNatLT (a &&& b) (Nat.and_lt_two_pow _ hb) = UInt32.ofNatLT a ha &&& UInt32.ofNatLT b hb := by
|
||||
simp [UInt32.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt64.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) :
|
||||
UInt64.ofNatLT (a &&& b) (Nat.and_lt_two_pow _ hb) = UInt64.ofNatLT a ha &&& UInt64.ofNatLT b hb := by
|
||||
simp [UInt64.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt8.ofFin_or (a b : Fin UInt8.size) : UInt8.ofFin (a ||| b) = UInt8.ofFin a ||| UInt8.ofFin b := UInt8.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofFin_or (a b : Fin UInt16.size) : UInt16.ofFin (a ||| b) = UInt16.ofFin a ||| UInt16.ofFin b := UInt16.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofFin_or (a b : Fin UInt32.size) : UInt32.ofFin (a ||| b) = UInt32.ofFin a ||| UInt32.ofFin b := UInt32.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofFin_or (a b : Fin UInt64.size) : UInt64.ofFin (a ||| b) = UInt64.ofFin a ||| UInt64.ofFin b := UInt64.toFin_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofFin_or (a b : Fin USize.size) : USize.ofFin (a ||| b) = USize.ofFin a ||| USize.ofFin b := USize.toFin_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_or (a b : BitVec 8) : UInt8.ofBitVec (a ||| b) = UInt8.ofBitVec a ||| UInt8.ofBitVec b := rfl
|
||||
@[simp] theorem UInt16.ofBitVec_or (a b : BitVec 16) : UInt16.ofBitVec (a ||| b) = UInt16.ofBitVec a ||| UInt16.ofBitVec b := rfl
|
||||
@[simp] theorem UInt32.ofBitVec_or (a b : BitVec 32) : UInt32.ofBitVec (a ||| b) = UInt32.ofBitVec a ||| UInt32.ofBitVec b := rfl
|
||||
@[simp] theorem UInt64.ofBitVec_or (a b : BitVec 64) : UInt64.ofBitVec (a ||| b) = UInt64.ofBitVec a ||| UInt64.ofBitVec b := rfl
|
||||
@[simp] theorem USize.ofBitVec_or (a b : BitVec System.Platform.numBits) : USize.ofBitVec (a ||| b) = USize.ofBitVec a ||| USize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem UInt8.ofNat_or (a b : Nat) : UInt8.ofNat (a ||| b) = UInt8.ofNat a ||| UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp [UInt8.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt16.ofNat_or (a b : Nat) : UInt16.ofNat (a ||| b) = UInt16.ofNat a ||| UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp [UInt16.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt32.ofNat_or (a b : Nat) : UInt32.ofNat (a ||| b) = UInt32.ofNat a ||| UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp [UInt32.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt64.ofNat_or (a b : Nat) : UInt64.ofNat (a ||| b) = UInt64.ofNat a ||| UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp [UInt64.toBitVec_ofNat'])
|
||||
@[simp] theorem USize.ofNat_or (a b : Nat) : USize.ofNat (a ||| b) = USize.ofNat a ||| USize.ofNat b :=
|
||||
USize.toBitVec_inj.1 (by simp [USize.toBitVec_ofNat'])
|
||||
|
||||
@[simp] theorem UInt8.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) :
|
||||
UInt8.ofNatLT (a ||| b) (Nat.or_lt_two_pow ha hb) = UInt8.ofNatLT a ha ||| UInt8.ofNatLT b hb := by
|
||||
simp [UInt8.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt16.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) :
|
||||
UInt16.ofNatLT (a ||| b) (Nat.or_lt_two_pow ha hb) = UInt16.ofNatLT a ha ||| UInt16.ofNatLT b hb := by
|
||||
simp [UInt16.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt32.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) :
|
||||
UInt32.ofNatLT (a ||| b) (Nat.or_lt_two_pow ha hb) = UInt32.ofNatLT a ha ||| UInt32.ofNatLT b hb := by
|
||||
simp [UInt32.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt64.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) :
|
||||
UInt64.ofNatLT (a ||| b) (Nat.or_lt_two_pow ha hb) = UInt64.ofNatLT a ha ||| UInt64.ofNatLT b hb := by
|
||||
simp [UInt64.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt8.ofFin_xor (a b : Fin UInt8.size) : UInt8.ofFin (a ^^^ b) = UInt8.ofFin a ^^^ UInt8.ofFin b := UInt8.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofFin_xor (a b : Fin UInt16.size) : UInt16.ofFin (a ^^^ b) = UInt16.ofFin a ^^^ UInt16.ofFin b := UInt16.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofFin_xor (a b : Fin UInt32.size) : UInt32.ofFin (a ^^^ b) = UInt32.ofFin a ^^^ UInt32.ofFin b := UInt32.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofFin_xor (a b : Fin UInt64.size) : UInt64.ofFin (a ^^^ b) = UInt64.ofFin a ^^^ UInt64.ofFin b := UInt64.toFin_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofFin_xor (a b : Fin USize.size) : USize.ofFin (a ^^^ b) = USize.ofFin a ^^^ USize.ofFin b := USize.toFin_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_xor (a b : BitVec 8) : UInt8.ofBitVec (a ^^^ b) = UInt8.ofBitVec a ^^^ UInt8.ofBitVec b := rfl
|
||||
@[simp] theorem UInt16.ofBitVec_xor (a b : BitVec 16) : UInt16.ofBitVec (a ^^^ b) = UInt16.ofBitVec a ^^^ UInt16.ofBitVec b := rfl
|
||||
@[simp] theorem UInt32.ofBitVec_xor (a b : BitVec 32) : UInt32.ofBitVec (a ^^^ b) = UInt32.ofBitVec a ^^^ UInt32.ofBitVec b := rfl
|
||||
@[simp] theorem UInt64.ofBitVec_xor (a b : BitVec 64) : UInt64.ofBitVec (a ^^^ b) = UInt64.ofBitVec a ^^^ UInt64.ofBitVec b := rfl
|
||||
@[simp] theorem USize.ofBitVec_xor (a b : BitVec System.Platform.numBits) : USize.ofBitVec (a ^^^ b) = USize.ofBitVec a ^^^ USize.ofBitVec b := rfl
|
||||
|
||||
@[simp] theorem UInt8.ofNat_xor (a b : Nat) : UInt8.ofNat (a ^^^ b) = UInt8.ofNat a ^^^ UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp [UInt8.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt16.ofNat_xor (a b : Nat) : UInt16.ofNat (a ^^^ b) = UInt16.ofNat a ^^^ UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp [UInt16.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt32.ofNat_xor (a b : Nat) : UInt32.ofNat (a ^^^ b) = UInt32.ofNat a ^^^ UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp [UInt32.toBitVec_ofNat'])
|
||||
@[simp] theorem UInt64.ofNat_xor (a b : Nat) : UInt64.ofNat (a ^^^ b) = UInt64.ofNat a ^^^ UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp [UInt64.toBitVec_ofNat'])
|
||||
@[simp] theorem USize.ofNat_xor (a b : Nat) : USize.ofNat (a ^^^ b) = USize.ofNat a ^^^ USize.ofNat b :=
|
||||
USize.toBitVec_inj.1 (by simp [USize.toBitVec_ofNat'])
|
||||
|
||||
@[simp] theorem UInt8.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) :
|
||||
UInt8.ofNatLT (a ^^^ b) (Nat.xor_lt_two_pow ha hb) = UInt8.ofNatLT a ha ^^^ UInt8.ofNatLT b hb := by
|
||||
simp [UInt8.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt16.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) :
|
||||
UInt16.ofNatLT (a ^^^ b) (Nat.xor_lt_two_pow ha hb) = UInt16.ofNatLT a ha ^^^ UInt16.ofNatLT b hb := by
|
||||
simp [UInt16.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt32.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) :
|
||||
UInt32.ofNatLT (a ^^^ b) (Nat.xor_lt_two_pow ha hb) = UInt32.ofNatLT a ha ^^^ UInt32.ofNatLT b hb := by
|
||||
simp [UInt32.ofNatLT_eq_ofNat]
|
||||
@[simp] theorem UInt64.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) :
|
||||
UInt64.ofNatLT (a ^^^ b) (Nat.xor_lt_two_pow ha hb) = UInt64.ofNatLT a ha ^^^ UInt64.ofNatLT b hb := by
|
||||
simp [UInt64.ofNatLT_eq_ofNat]
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_not (a : BitVec 8) : UInt8.ofBitVec (~~~a) = ~~~UInt8.ofBitVec a := rfl
|
||||
@[simp] theorem UInt16.ofBitVec_not (a : BitVec 16) : UInt16.ofBitVec (~~~a) = ~~~UInt16.ofBitVec a := rfl
|
||||
@[simp] theorem UInt32.ofBitVec_not (a : BitVec 32) : UInt32.ofBitVec (~~~a) = ~~~UInt32.ofBitVec a := rfl
|
||||
@[simp] theorem UInt64.ofBitVec_not (a : BitVec 64) : UInt64.ofBitVec (~~~a) = ~~~UInt64.ofBitVec a := rfl
|
||||
@[simp] theorem USize.ofBitVec_not (a : BitVec System.Platform.numBits) : USize.ofBitVec (~~~a) = ~~~USize.ofBitVec a := rfl
|
||||
|
||||
@[simp] theorem UInt8.ofFin_rev (a : Fin UInt8.size) : UInt8.ofFin a.rev = ~~~UInt8.ofFin a := UInt8.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofFin_rev (a : Fin UInt16.size) : UInt16.ofFin a.rev = ~~~UInt16.ofFin a := UInt16.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofFin_rev (a : Fin UInt32.size) : UInt32.ofFin a.rev = ~~~UInt32.ofFin a := UInt32.toFin_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofFin_rev (a : Fin UInt64.size) : UInt64.ofFin a.rev = ~~~UInt64.ofFin a := UInt64.toFin_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofFin_rev (a : Fin USize.size) : USize.ofFin a.rev = ~~~USize.ofFin a := USize.toFin_inj.1 (by simp)
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_shiftLeft (a : BitVec 8) (b : Nat) (hb : b < 8) : UInt8.ofBitVec (a <<< b) = UInt8.ofBitVec a <<< UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt16.ofBitVec_shiftLeft (a : BitVec 16) (b : Nat) (hb : b < 16) : UInt16.ofBitVec (a <<< b) = UInt16.ofBitVec a <<< UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt32.ofBitVec_shiftLeft (a : BitVec 32) (b : Nat) (hb : b < 32) : UInt32.ofBitVec (a <<< b) = UInt32.ofBitVec a <<< UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt64.ofBitVec_shiftLeft (a : BitVec 64) (b : Nat) (hb : b < 64) : UInt64.ofBitVec (a <<< b) = UInt64.ofBitVec a <<< UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem USize.ofBitVec_shiftLeft (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) :
|
||||
USize.ofBitVec (a <<< b) = USize.ofBitVec a <<< USize.ofNat b := by
|
||||
apply USize.toBitVec_inj.1
|
||||
simp only [USize.toBitVec_shiftLeft, BitVec.natCast_eq_ofNat, BitVec.shiftLeft_eq',
|
||||
BitVec.toNat_umod, toNat_toBitVec, toNat_ofNat', BitVec.toNat_ofNat, Nat.mod_two_pow_self]
|
||||
rw [Nat.mod_mod_of_dvd _ (by cases System.Platform.numBits_eq <;> simp_all), Nat.mod_eq_of_lt hb]
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_shiftLeft_mod (a : BitVec 8) (b : Nat) : UInt8.ofBitVec (a <<< (b % 8)) = UInt8.ofBitVec a <<< UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofBitVec_shiftLeft_mod (a : BitVec 16) (b : Nat) : UInt16.ofBitVec (a <<< (b % 16)) = UInt16.ofBitVec a <<< UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofBitVec_shiftLeft_mod (a : BitVec 32) (b : Nat) : UInt32.ofBitVec (a <<< (b % 32)) = UInt32.ofBitVec a <<< UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofBitVec_shiftLeft_mod (a : BitVec 64) (b : Nat) : UInt64.ofBitVec (a <<< (b % 64)) = UInt64.ofBitVec a <<< UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofBitVec_shiftLeft_mod (a : BitVec System.Platform.numBits) (b : Nat) :
|
||||
USize.ofBitVec (a <<< (b % System.Platform.numBits)) = USize.ofBitVec a <<< USize.ofNat b := by
|
||||
apply USize.toBitVec_inj.1
|
||||
simp only [USize.toBitVec_shiftLeft, BitVec.natCast_eq_ofNat, BitVec.shiftLeft_eq',
|
||||
BitVec.toNat_umod, toNat_toBitVec, toNat_ofNat', BitVec.toNat_ofNat, Nat.mod_two_pow_self]
|
||||
rw [Nat.mod_mod_of_dvd _ (by cases System.Platform.numBits_eq <;> simp_all)]
|
||||
|
||||
@[simp] theorem UInt8.ofFin_shiftLeft (a b : Fin UInt8.size) (hb : b < 8) : UInt8.ofFin (a <<< b) = UInt8.ofFin a <<< UInt8.ofFin b :=
|
||||
UInt8.toFin_inj.1 (by simp [UInt8.toFin_shiftLeft (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt16.ofFin_shiftLeft (a b : Fin UInt16.size) (hb : b < 16) : UInt16.ofFin (a <<< b) = UInt16.ofFin a <<< UInt16.ofFin b :=
|
||||
UInt16.toFin_inj.1 (by simp [UInt16.toFin_shiftLeft (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt32.ofFin_shiftLeft (a b : Fin UInt32.size) (hb : b < 32) : UInt32.ofFin (a <<< b) = UInt32.ofFin a <<< UInt32.ofFin b :=
|
||||
UInt32.toFin_inj.1 (by simp [UInt32.toFin_shiftLeft (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt64.ofFin_shiftLeft (a b : Fin UInt64.size) (hb : b < 64) : UInt64.ofFin (a <<< b) = UInt64.ofFin a <<< UInt64.ofFin b :=
|
||||
UInt64.toFin_inj.1 (by simp [UInt64.toFin_shiftLeft (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem USize.ofFin_shiftLeft (a b : Fin USize.size) (hb : b < System.Platform.numBits) : USize.ofFin (a <<< b) = USize.ofFin a <<< USize.ofFin b :=
|
||||
USize.toFin_inj.1 (by simp [USize.toFin_shiftLeft (ofFin a) (ofFin b) hb])
|
||||
|
||||
@[simp] theorem UInt8.ofFin_shiftLeft_mod (a b : Fin UInt8.size) : UInt8.ofFin (a <<< (b % 8)) = UInt8.ofFin a <<< UInt8.ofFin b :=
|
||||
UInt8.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt16.ofFin_shiftLeft_mod (a b : Fin UInt16.size) : UInt16.ofFin (a <<< (b % 16)) = UInt16.ofFin a <<< UInt16.ofFin b :=
|
||||
UInt16.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt32.ofFin_shiftLeft_mod (a b : Fin UInt32.size) : UInt32.ofFin (a <<< (b % 32)) = UInt32.ofFin a <<< UInt32.ofFin b :=
|
||||
UInt32.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt64.ofFin_shiftLeft_mod (a b : Fin UInt64.size) : UInt64.ofFin (a <<< (b % 64)) = UInt64.ofFin a <<< UInt64.ofFin b :=
|
||||
UInt64.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem USize.ofFin_shiftLeft_mod (a b : Fin USize.size) :
|
||||
USize.ofFin (a <<< (b % ⟨System.Platform.numBits, by cases System.Platform.numBits_eq <;> simp_all [USize.size]⟩)) = USize.ofFin a <<< USize.ofFin b := by
|
||||
apply USize.toFin_inj.1
|
||||
rw [toFin_ofFin, USize.shiftLeft_eq_shiftLeft_mod, USize.toFin_shiftLeft, toFin_ofFin, USize.toFin_mod,
|
||||
toFin_ofFin, toFin_ofNat', ← Fin.ofNat'_val_eq_self ⟨System.Platform.numBits, _⟩]
|
||||
rw [USize.toNat_mod, toNat_ofNat']
|
||||
cases System.Platform.numBits_eq <;> simpa [*] using Nat.mod_lt _ (by decide)
|
||||
|
||||
@[simp] theorem UInt8.ofNat_shiftLeft (a b : Nat) (hb : b < 8) :
|
||||
UInt8.ofNat (a <<< b) = UInt8.ofNat a <<< UInt8.ofNat b := by
|
||||
rw [UInt8.ofNat_eq_iff_mod_eq_toNat, UInt8.toNat_shiftLeft, toNat_ofNat', toNat_ofNat',
|
||||
Nat.mod_mod_of_dvd _ (by decide), Nat.mod_eq_of_lt hb, Nat.mod_two_pow_shiftLeft_mod_two_pow]
|
||||
@[simp] theorem UInt16.ofNat_shiftLeft (a b : Nat) (hb : b < 16) :
|
||||
UInt16.ofNat (a <<< b) = UInt16.ofNat a <<< UInt16.ofNat b := by
|
||||
rw [UInt16.ofNat_eq_iff_mod_eq_toNat, UInt16.toNat_shiftLeft, toNat_ofNat', toNat_ofNat',
|
||||
Nat.mod_mod_of_dvd _ (by decide), Nat.mod_eq_of_lt hb, Nat.mod_two_pow_shiftLeft_mod_two_pow]
|
||||
@[simp] theorem UInt32.ofNat_shiftLeft (a b : Nat) (hb : b < 32) :
|
||||
UInt32.ofNat (a <<< b) = UInt32.ofNat a <<< UInt32.ofNat b := by
|
||||
rw [UInt32.ofNat_eq_iff_mod_eq_toNat, UInt32.toNat_shiftLeft, toNat_ofNat', toNat_ofNat',
|
||||
Nat.mod_mod_of_dvd _ (by decide), Nat.mod_eq_of_lt hb, Nat.mod_two_pow_shiftLeft_mod_two_pow]
|
||||
@[simp] theorem UInt64.ofNat_shiftLeft (a b : Nat) (hb : b < 64) :
|
||||
UInt64.ofNat (a <<< b) = UInt64.ofNat a <<< UInt64.ofNat b := by
|
||||
rw [UInt64.ofNat_eq_iff_mod_eq_toNat, UInt64.toNat_shiftLeft, toNat_ofNat', toNat_ofNat',
|
||||
Nat.mod_mod_of_dvd _ (by decide), Nat.mod_eq_of_lt hb, Nat.mod_two_pow_shiftLeft_mod_two_pow]
|
||||
@[simp] theorem USize.ofNat_shiftLeft (a b : Nat) (hb : b < System.Platform.numBits) :
|
||||
USize.ofNat (a <<< b) = USize.ofNat a <<< USize.ofNat b := by
|
||||
rw [USize.ofNat_eq_iff_mod_eq_toNat, USize.toNat_shiftLeft, toNat_ofNat', toNat_ofNat',
|
||||
Nat.mod_mod_of_dvd _ _, Nat.mod_eq_of_lt hb, Nat.mod_two_pow_shiftLeft_mod_two_pow]
|
||||
cases System.Platform.numBits_eq <;> simp_all
|
||||
|
||||
@[simp] theorem UInt8.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < UInt8.size) (hb : b < 8) :
|
||||
UInt8.ofNatLT (a <<< b) ha = UInt8.ofNatLT a (Nat.lt_of_shiftLeft_lt ha) <<< UInt8.ofNatLT b (Nat.lt_trans hb (by decide)) := by
|
||||
simp [UInt8.ofNatLT_eq_ofNat, UInt8.ofNat_shiftLeft a b hb]
|
||||
@[simp] theorem UInt16.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < UInt16.size) (hb : b < 16) :
|
||||
UInt16.ofNatLT (a <<< b) ha = UInt16.ofNatLT a (Nat.lt_of_shiftLeft_lt ha) <<< UInt16.ofNatLT b (Nat.lt_trans hb (by decide)) := by
|
||||
simp [UInt16.ofNatLT_eq_ofNat, UInt16.ofNat_shiftLeft a b hb]
|
||||
@[simp] theorem UInt32.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < UInt32.size) (hb : b < 32) :
|
||||
UInt32.ofNatLT (a <<< b) ha = UInt32.ofNatLT a (Nat.lt_of_shiftLeft_lt ha) <<< UInt32.ofNatLT b (Nat.lt_trans hb (by decide)) := by
|
||||
simp [UInt32.ofNatLT_eq_ofNat, UInt32.ofNat_shiftLeft a b hb]
|
||||
@[simp] theorem UInt64.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < UInt64.size) (hb : b < 64) :
|
||||
UInt64.ofNatLT (a <<< b) ha = UInt64.ofNatLT a (Nat.lt_of_shiftLeft_lt ha) <<< UInt64.ofNatLT b (Nat.lt_trans hb (by decide)) := by
|
||||
simp [UInt64.ofNatLT_eq_ofNat, UInt64.ofNat_shiftLeft a b hb]
|
||||
@[simp] theorem USize.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < USize.size) (hb : b < System.Platform.numBits) :
|
||||
USize.ofNatLT (a <<< b) ha = USize.ofNatLT a (Nat.lt_of_shiftLeft_lt ha) <<< USize.ofNatLT b (Nat.lt_trans hb Nat.lt_two_pow_self) := by
|
||||
simp [USize.ofNatLT_eq_ofNat, USize.ofNat_shiftLeft a b hb]
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_shiftRight (a : BitVec 8) (b : Nat) (hb : b < 8) : UInt8.ofBitVec (a >>> b) = UInt8.ofBitVec a >>> UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt16.ofBitVec_shiftRight (a : BitVec 16) (b : Nat) (hb : b < 16) : UInt16.ofBitVec (a >>> b) = UInt16.ofBitVec a >>> UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt32.ofBitVec_shiftRight (a : BitVec 32) (b : Nat) (hb : b < 32) : UInt32.ofBitVec (a >>> b) = UInt32.ofBitVec a >>> UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem UInt64.ofBitVec_shiftRight (a : BitVec 64) (b : Nat) (hb : b < 64) : UInt64.ofBitVec (a >>> b) = UInt64.ofBitVec a >>> UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp [Nat.mod_eq_of_lt hb])
|
||||
@[simp] theorem USize.ofBitVec_shiftRight (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) :
|
||||
USize.ofBitVec (a >>> b) = USize.ofBitVec a >>> USize.ofNat b := by
|
||||
apply USize.toBitVec_inj.1
|
||||
simp only [USize.toBitVec_shiftRight, BitVec.natCast_eq_ofNat, BitVec.ushiftRight_eq',
|
||||
BitVec.toNat_umod, toNat_toBitVec, toNat_ofNat', BitVec.toNat_ofNat, Nat.mod_two_pow_self]
|
||||
rw [Nat.mod_mod_of_dvd _ (by cases System.Platform.numBits_eq <;> simp_all), Nat.mod_eq_of_lt hb]
|
||||
|
||||
@[simp] theorem UInt8.ofBitVec_shiftRight_mod (a : BitVec 8) (b : Nat) : UInt8.ofBitVec (a >>> (b % 8)) = UInt8.ofBitVec a >>> UInt8.ofNat b :=
|
||||
UInt8.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt16.ofBitVec_shiftRight_mod (a : BitVec 16) (b : Nat) : UInt16.ofBitVec (a >>> (b % 16)) = UInt16.ofBitVec a >>> UInt16.ofNat b :=
|
||||
UInt16.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt32.ofBitVec_shiftRight_mod (a : BitVec 32) (b : Nat) : UInt32.ofBitVec (a >>> (b % 32)) = UInt32.ofBitVec a >>> UInt32.ofNat b :=
|
||||
UInt32.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem UInt64.ofBitVec_shiftRight_mod (a : BitVec 64) (b : Nat) : UInt64.ofBitVec (a >>> (b % 64)) = UInt64.ofBitVec a >>> UInt64.ofNat b :=
|
||||
UInt64.toBitVec_inj.1 (by simp)
|
||||
@[simp] theorem USize.ofBitVec_shiftRight_mod (a : BitVec System.Platform.numBits) (b : Nat) :
|
||||
USize.ofBitVec (a >>> (b % System.Platform.numBits)) = USize.ofBitVec a >>> USize.ofNat b := by
|
||||
apply USize.toBitVec_inj.1
|
||||
simp only [USize.toBitVec_shiftRight, BitVec.natCast_eq_ofNat, BitVec.ushiftRight_eq',
|
||||
BitVec.toNat_umod, toNat_toBitVec, toNat_ofNat', BitVec.toNat_ofNat, Nat.mod_two_pow_self]
|
||||
rw [Nat.mod_mod_of_dvd _ (by cases System.Platform.numBits_eq <;> simp_all)]
|
||||
|
||||
@[simp] theorem UInt8.ofFin_shiftRight (a b : Fin UInt8.size) (hb : b < 8) : UInt8.ofFin (a >>> b) = UInt8.ofFin a >>> UInt8.ofFin b :=
|
||||
UInt8.toFin_inj.1 (by simp [UInt8.toFin_shiftRight (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt16.ofFin_shiftRight (a b : Fin UInt16.size) (hb : b < 16) : UInt16.ofFin (a >>> b) = UInt16.ofFin a >>> UInt16.ofFin b :=
|
||||
UInt16.toFin_inj.1 (by simp [UInt16.toFin_shiftRight (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt32.ofFin_shiftRight (a b : Fin UInt32.size) (hb : b < 32) : UInt32.ofFin (a >>> b) = UInt32.ofFin a >>> UInt32.ofFin b :=
|
||||
UInt32.toFin_inj.1 (by simp [UInt32.toFin_shiftRight (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem UInt64.ofFin_shiftRight (a b : Fin UInt64.size) (hb : b < 64) : UInt64.ofFin (a >>> b) = UInt64.ofFin a >>> UInt64.ofFin b :=
|
||||
UInt64.toFin_inj.1 (by simp [UInt64.toFin_shiftRight (ofFin a) (ofFin b) hb])
|
||||
@[simp] theorem USize.ofFin_shiftRight (a b : Fin USize.size) (hb : b < System.Platform.numBits) : USize.ofFin (a >>> b) = USize.ofFin a >>> USize.ofFin b :=
|
||||
USize.toFin_inj.1 (by simp [USize.toFin_shiftRight (ofFin a) (ofFin b) hb])
|
||||
|
||||
@[simp] theorem UInt8.ofFin_shiftRight_mod (a b : Fin UInt8.size) : UInt8.ofFin (a >>> (b % 8)) = UInt8.ofFin a >>> UInt8.ofFin b :=
|
||||
UInt8.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt16.ofFin_shiftRight_mod (a b : Fin UInt16.size) : UInt16.ofFin (a >>> (b % 16)) = UInt16.ofFin a >>> UInt16.ofFin b :=
|
||||
UInt16.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt32.ofFin_shiftRight_mod (a b : Fin UInt32.size) : UInt32.ofFin (a >>> (b % 32)) = UInt32.ofFin a >>> UInt32.ofFin b :=
|
||||
UInt32.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem UInt64.ofFin_shiftRight_mod (a b : Fin UInt64.size) : UInt64.ofFin (a >>> (b % 64)) = UInt64.ofFin a >>> UInt64.ofFin b :=
|
||||
UInt64.toNat_inj.1 (by simp; rfl)
|
||||
@[simp] theorem USize.ofFin_shiftRight_mod (a b : Fin USize.size) :
|
||||
USize.ofFin (a >>> (b % ⟨System.Platform.numBits, by cases System.Platform.numBits_eq <;> simp_all [USize.size]⟩)) = USize.ofFin a >>> USize.ofFin b := by
|
||||
apply USize.toFin_inj.1
|
||||
rw [toFin_ofFin, USize.shiftRight_eq_shiftRight_mod, USize.toFin_shiftRight, toFin_ofFin, USize.toFin_mod,
|
||||
toFin_ofFin, toFin_ofNat', ← Fin.ofNat'_val_eq_self ⟨System.Platform.numBits, _⟩]
|
||||
rw [USize.toNat_mod, toNat_ofNat']
|
||||
cases System.Platform.numBits_eq <;> simpa [*] using Nat.mod_lt _ (by decide)
|
||||
|
||||
theorem UInt8.neg_eq_not_add (a : UInt8) : -a = ~~~a + 1 := UInt8.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem UInt16.neg_eq_not_add (a : UInt16) : -a = ~~~a + 1 := UInt16.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem UInt32.neg_eq_not_add (a : UInt32) : -a = ~~~a + 1 := UInt32.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem UInt64.neg_eq_not_add (a : UInt64) : -a = ~~~a + 1 := UInt64.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
theorem USize.neg_eq_not_add (a : USize) : -a = ~~~a + 1 := USize.toBitVec_inj.1 (BitVec.neg_eq_not_add _)
|
||||
|
||||
theorem UInt8.not_eq_neg_sub (a : UInt8) : ~~~a = -a - 1 := UInt8.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem UInt16.not_eq_neg_sub (a : UInt16) : ~~~a = -a - 1 := UInt16.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem UInt32.not_eq_neg_sub (a : UInt32) : ~~~a = -a - 1 := UInt32.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem UInt64.not_eq_neg_sub (a : UInt64) : ~~~a = -a - 1 := UInt64.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
theorem USize.not_eq_neg_sub (a : USize) : ~~~a = -a - 1 := USize.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
|
||||
|
||||
theorem UInt8.or_assoc (a b c : UInt8) : a ||| b ||| c = a ||| (b ||| c) := UInt8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem UInt16.or_assoc (a b c : UInt16) : a ||| b ||| c = a ||| (b ||| c) := UInt16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem UInt32.or_assoc (a b c : UInt32) : a ||| b ||| c = a ||| (b ||| c) := UInt32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem UInt64.or_assoc (a b c : UInt64) : a ||| b ||| c = a ||| (b ||| c) := UInt64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
theorem USize.or_assoc (a b c : USize) : a ||| b ||| c = a ||| (b ||| c) := USize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := UInt8) (· ||| ·) := ⟨UInt8.or_assoc⟩
|
||||
instance : Std.Associative (α := UInt16) (· ||| ·) := ⟨UInt16.or_assoc⟩
|
||||
instance : Std.Associative (α := UInt32) (· ||| ·) := ⟨UInt32.or_assoc⟩
|
||||
instance : Std.Associative (α := UInt64) (· ||| ·) := ⟨UInt64.or_assoc⟩
|
||||
instance : Std.Associative (α := USize) (· ||| ·) := ⟨USize.or_assoc⟩
|
||||
|
||||
theorem UInt8.or_comm (a b : UInt8) : a ||| b = b ||| a := UInt8.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem UInt16.or_comm (a b : UInt16) : a ||| b = b ||| a := UInt16.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem UInt32.or_comm (a b : UInt32) : a ||| b = b ||| a := UInt32.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem UInt64.or_comm (a b : UInt64) : a ||| b = b ||| a := UInt64.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
theorem USize.or_comm (a b : USize) : a ||| b = b ||| a := USize.toBitVec_inj.1 (BitVec.or_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := UInt8) (· ||| ·) := ⟨UInt8.or_comm⟩
|
||||
instance : Std.Commutative (α := UInt16) (· ||| ·) := ⟨UInt16.or_comm⟩
|
||||
instance : Std.Commutative (α := UInt32) (· ||| ·) := ⟨UInt32.or_comm⟩
|
||||
instance : Std.Commutative (α := UInt64) (· ||| ·) := ⟨UInt64.or_comm⟩
|
||||
instance : Std.Commutative (α := USize) (· ||| ·) := ⟨USize.or_comm⟩
|
||||
|
||||
@[simp] theorem UInt8.or_self {a : UInt8} : a ||| a = a := UInt8.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem UInt16.or_self {a : UInt16} : a ||| a = a := UInt16.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem UInt32.or_self {a : UInt32} : a ||| a = a := UInt32.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem UInt64.or_self {a : UInt64} : a ||| a = a := UInt64.toBitVec_inj.1 BitVec.or_self
|
||||
@[simp] theorem USize.or_self {a : USize} : a ||| a = a := USize.toBitVec_inj.1 BitVec.or_self
|
||||
|
||||
instance : Std.IdempotentOp (α := UInt8) (· ||| ·) := ⟨fun _ => UInt8.or_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt16) (· ||| ·) := ⟨fun _ => UInt16.or_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt32) (· ||| ·) := ⟨fun _ => UInt32.or_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt64) (· ||| ·) := ⟨fun _ => UInt64.or_self⟩
|
||||
instance : Std.IdempotentOp (α := USize) (· ||| ·) := ⟨fun _ => USize.or_self⟩
|
||||
|
||||
@[simp] theorem UInt8.or_zero {a : UInt8} : a ||| 0 = a := UInt8.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem UInt16.or_zero {a : UInt16} : a ||| 0 = a := UInt16.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem UInt32.or_zero {a : UInt32} : a ||| 0 = a := UInt32.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem UInt64.or_zero {a : UInt64} : a ||| 0 = a := UInt64.toBitVec_inj.1 BitVec.or_zero
|
||||
@[simp] theorem USize.or_zero {a : USize} : a ||| 0 = a := USize.toBitVec_inj.1 BitVec.or_zero
|
||||
|
||||
@[simp] theorem UInt8.zero_or {a : UInt8} : 0 ||| a = a := UInt8.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem UInt16.zero_or {a : UInt16} : 0 ||| a = a := UInt16.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem UInt32.zero_or {a : UInt32} : 0 ||| a = a := UInt32.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem UInt64.zero_or {a : UInt64} : 0 ||| a = a := UInt64.toBitVec_inj.1 BitVec.zero_or
|
||||
@[simp] theorem USize.zero_or {a : USize} : 0 ||| a = a := USize.toBitVec_inj.1 BitVec.zero_or
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := UInt8) (· ||| ·) 0 where
|
||||
right_id _ := UInt8.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt16) (· ||| ·) 0 where
|
||||
right_id _ := UInt16.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt32) (· ||| ·) 0 where
|
||||
right_id _ := UInt32.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt64) (· ||| ·) 0 where
|
||||
right_id _ := UInt64.or_zero
|
||||
instance : Std.LawfulCommIdentity (α := USize) (· ||| ·) 0 where
|
||||
right_id _ := USize.or_zero
|
||||
|
||||
@[simp] theorem UInt8.neg_one_or {a : UInt8} : -1 ||| a = -1 := by
|
||||
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_or, UInt8.toBitVec_neg, UInt8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem UInt16.neg_one_or {a : UInt16} : -1 ||| a = -1 := by
|
||||
rw [← UInt16.toBitVec_inj, UInt16.toBitVec_or, UInt16.toBitVec_neg, UInt16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem UInt32.neg_one_or {a : UInt32} : -1 ||| a = -1 := by
|
||||
rw [← UInt32.toBitVec_inj, UInt32.toBitVec_or, UInt32.toBitVec_neg, UInt32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem UInt64.neg_one_or {a : UInt64} : -1 ||| a = -1 := by
|
||||
rw [← UInt64.toBitVec_inj, UInt64.toBitVec_or, UInt64.toBitVec_neg, UInt64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
@[simp] theorem USize.neg_one_or {a : USize} : -1 ||| a = -1 := by
|
||||
rw [← USize.toBitVec_inj, USize.toBitVec_or, USize.toBitVec_neg, USize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
|
||||
|
||||
@[simp] theorem UInt8.or_neg_one {a : UInt8} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem UInt16.or_neg_one {a : UInt16} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem UInt32.or_neg_one {a : UInt32} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem UInt64.or_neg_one {a : UInt64} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
@[simp] theorem USize.or_neg_one {a : USize} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
|
||||
|
||||
@[simp] theorem UInt8.or_eq_zero_iff {a b : UInt8} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.or_eq_zero_iff {a b : UInt16} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.or_eq_zero_iff {a b : UInt32} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.or_eq_zero_iff {a b : UInt64} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.or_eq_zero_iff {a b : USize} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
|
||||
simp [← USize.toBitVec_inj]
|
||||
|
||||
theorem UInt8.and_assoc (a b c : UInt8) : a &&& b &&& c = a &&& (b &&& c) := UInt8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem UInt16.and_assoc (a b c : UInt16) : a &&& b &&& c = a &&& (b &&& c) := UInt16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem UInt32.and_assoc (a b c : UInt32) : a &&& b &&& c = a &&& (b &&& c) := UInt32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem UInt64.and_assoc (a b c : UInt64) : a &&& b &&& c = a &&& (b &&& c) := UInt64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
theorem USize.and_assoc (a b c : USize) : a &&& b &&& c = a &&& (b &&& c) := USize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := UInt8) (· &&& ·) := ⟨UInt8.and_assoc⟩
|
||||
instance : Std.Associative (α := UInt16) (· &&& ·) := ⟨UInt16.and_assoc⟩
|
||||
instance : Std.Associative (α := UInt32) (· &&& ·) := ⟨UInt32.and_assoc⟩
|
||||
instance : Std.Associative (α := UInt64) (· &&& ·) := ⟨UInt64.and_assoc⟩
|
||||
instance : Std.Associative (α := USize) (· &&& ·) := ⟨USize.and_assoc⟩
|
||||
|
||||
theorem UInt8.and_comm (a b : UInt8) : a &&& b = b &&& a := UInt8.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem UInt16.and_comm (a b : UInt16) : a &&& b = b &&& a := UInt16.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem UInt32.and_comm (a b : UInt32) : a &&& b = b &&& a := UInt32.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem UInt64.and_comm (a b : UInt64) : a &&& b = b &&& a := UInt64.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
theorem USize.and_comm (a b : USize) : a &&& b = b &&& a := USize.toBitVec_inj.1 (BitVec.and_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := UInt8) (· &&& ·) := ⟨UInt8.and_comm⟩
|
||||
instance : Std.Commutative (α := UInt16) (· &&& ·) := ⟨UInt16.and_comm⟩
|
||||
instance : Std.Commutative (α := UInt32) (· &&& ·) := ⟨UInt32.and_comm⟩
|
||||
instance : Std.Commutative (α := UInt64) (· &&& ·) := ⟨UInt64.and_comm⟩
|
||||
instance : Std.Commutative (α := USize) (· &&& ·) := ⟨USize.and_comm⟩
|
||||
|
||||
@[simp] theorem UInt8.and_self {a : UInt8} : a &&& a = a := UInt8.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem UInt16.and_self {a : UInt16} : a &&& a = a := UInt16.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem UInt32.and_self {a : UInt32} : a &&& a = a := UInt32.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem UInt64.and_self {a : UInt64} : a &&& a = a := UInt64.toBitVec_inj.1 BitVec.and_self
|
||||
@[simp] theorem USize.and_self {a : USize} : a &&& a = a := USize.toBitVec_inj.1 BitVec.and_self
|
||||
|
||||
instance : Std.IdempotentOp (α := UInt8) (· &&& ·) := ⟨fun _ => UInt8.and_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt16) (· &&& ·) := ⟨fun _ => UInt16.and_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt32) (· &&& ·) := ⟨fun _ => UInt32.and_self⟩
|
||||
instance : Std.IdempotentOp (α := UInt64) (· &&& ·) := ⟨fun _ => UInt64.and_self⟩
|
||||
instance : Std.IdempotentOp (α := USize) (· &&& ·) := ⟨fun _ => USize.and_self⟩
|
||||
|
||||
@[simp] theorem UInt8.and_zero {a : UInt8} : a &&& 0 = 0 := UInt8.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem UInt16.and_zero {a : UInt16} : a &&& 0 = 0 := UInt16.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem UInt32.and_zero {a : UInt32} : a &&& 0 = 0 := UInt32.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem UInt64.and_zero {a : UInt64} : a &&& 0 = 0 := UInt64.toBitVec_inj.1 BitVec.and_zero
|
||||
@[simp] theorem USize.and_zero {a : USize} : a &&& 0 = 0 := USize.toBitVec_inj.1 BitVec.and_zero
|
||||
|
||||
@[simp] theorem UInt8.zero_and {a : UInt8} : 0 &&& a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem UInt16.zero_and {a : UInt16} : 0 &&& a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem UInt32.zero_and {a : UInt32} : 0 &&& a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem UInt64.zero_and {a : UInt64} : 0 &&& a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_and
|
||||
@[simp] theorem USize.zero_and {a : USize} : 0 &&& a = 0 := USize.toBitVec_inj.1 BitVec.zero_and
|
||||
|
||||
@[simp] theorem UInt8.neg_one_and {a : UInt8} : -1 &&& a = a := by
|
||||
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_and, UInt8.toBitVec_neg, UInt8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem UInt16.neg_one_and {a : UInt16} : -1 &&& a = a := by
|
||||
rw [← UInt16.toBitVec_inj, UInt16.toBitVec_and, UInt16.toBitVec_neg, UInt16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem UInt32.neg_one_and {a : UInt32} : -1 &&& a = a := by
|
||||
rw [← UInt32.toBitVec_inj, UInt32.toBitVec_and, UInt32.toBitVec_neg, UInt32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem UInt64.neg_one_and {a : UInt64} : -1 &&& a = a := by
|
||||
rw [← UInt64.toBitVec_inj, UInt64.toBitVec_and, UInt64.toBitVec_neg, UInt64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
@[simp] theorem USize.neg_one_and {a : USize} : -1 &&& a = a := by
|
||||
rw [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
|
||||
|
||||
@[simp] theorem UInt8.and_neg_one {a : UInt8} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem UInt16.and_neg_one {a : UInt16} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem UInt32.and_neg_one {a : UInt32} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem UInt64.and_neg_one {a : UInt64} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
@[simp] theorem USize.and_neg_one {a : USize} : a &&& -1 = a := by rw [and_comm, neg_one_and]
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := UInt8) (· &&& ·) (-1) where
|
||||
right_id _ := UInt8.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := UInt16) (· &&& ·) (-1) where
|
||||
right_id _ := UInt16.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := UInt32) (· &&& ·) (-1) where
|
||||
right_id _ := UInt32.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := UInt64) (· &&& ·) (-1) where
|
||||
right_id _ := UInt64.and_neg_one
|
||||
instance : Std.LawfulCommIdentity (α := USize) (· &&& ·) (-1) where
|
||||
right_id _ := USize.and_neg_one
|
||||
|
||||
@[simp] theorem UInt8.and_eq_neg_one_iff {a b : UInt8} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← UInt8.toBitVec_inj, UInt8.toBitVec_and, UInt8.toBitVec_neg, UInt8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem UInt16.and_eq_neg_one_iff {a b : UInt16} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← UInt16.toBitVec_inj, UInt16.toBitVec_and, UInt16.toBitVec_neg, UInt16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem UInt32.and_eq_neg_one_iff {a b : UInt32} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← UInt32.toBitVec_inj, UInt32.toBitVec_and, UInt32.toBitVec_neg, UInt32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem UInt64.and_eq_neg_one_iff {a b : UInt64} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← UInt64.toBitVec_inj, UInt64.toBitVec_and, UInt64.toBitVec_neg, UInt64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
@[simp] theorem USize.and_eq_neg_one_iff {a b : USize} : a &&& b = -1 ↔ a = -1 ∧ b = -1 := by
|
||||
simp only [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
|
||||
|
||||
theorem UInt8.xor_assoc (a b c : UInt8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem UInt16.xor_assoc (a b c : UInt16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem UInt32.xor_assoc (a b c : UInt32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem UInt64.xor_assoc (a b c : UInt64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
theorem USize.xor_assoc (a b c : USize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := USize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
|
||||
|
||||
instance : Std.Associative (α := UInt8) (· ^^^ ·) := ⟨UInt8.xor_assoc⟩
|
||||
instance : Std.Associative (α := UInt16) (· ^^^ ·) := ⟨UInt16.xor_assoc⟩
|
||||
instance : Std.Associative (α := UInt32) (· ^^^ ·) := ⟨UInt32.xor_assoc⟩
|
||||
instance : Std.Associative (α := UInt64) (· ^^^ ·) := ⟨UInt64.xor_assoc⟩
|
||||
instance : Std.Associative (α := USize) (· ^^^ ·) := ⟨USize.xor_assoc⟩
|
||||
|
||||
theorem UInt8.xor_comm (a b : UInt8) : a ^^^ b = b ^^^ a := UInt8.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem UInt16.xor_comm (a b : UInt16) : a ^^^ b = b ^^^ a := UInt16.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem UInt32.xor_comm (a b : UInt32) : a ^^^ b = b ^^^ a := UInt32.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem UInt64.xor_comm (a b : UInt64) : a ^^^ b = b ^^^ a := UInt64.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
theorem USize.xor_comm (a b : USize) : a ^^^ b = b ^^^ a := USize.toBitVec_inj.1 (BitVec.xor_comm _ _)
|
||||
|
||||
instance : Std.Commutative (α := UInt8) (· ^^^ ·) := ⟨UInt8.xor_comm⟩
|
||||
instance : Std.Commutative (α := UInt16) (· ^^^ ·) := ⟨UInt16.xor_comm⟩
|
||||
instance : Std.Commutative (α := UInt32) (· ^^^ ·) := ⟨UInt32.xor_comm⟩
|
||||
instance : Std.Commutative (α := UInt64) (· ^^^ ·) := ⟨UInt64.xor_comm⟩
|
||||
instance : Std.Commutative (α := USize) (· ^^^ ·) := ⟨USize.xor_comm⟩
|
||||
|
||||
@[simp] theorem UInt8.xor_self {a : UInt8} : a ^^^ a = 0 := UInt8.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem UInt16.xor_self {a : UInt16} : a ^^^ a = 0 := UInt16.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem UInt32.xor_self {a : UInt32} : a ^^^ a = 0 := UInt32.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem UInt64.xor_self {a : UInt64} : a ^^^ a = 0 := UInt64.toBitVec_inj.1 BitVec.xor_self
|
||||
@[simp] theorem USize.xor_self {a : USize} : a ^^^ a = 0 := USize.toBitVec_inj.1 BitVec.xor_self
|
||||
|
||||
@[simp] theorem UInt8.xor_zero {a : UInt8} : a ^^^ 0 = a := UInt8.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem UInt16.xor_zero {a : UInt16} : a ^^^ 0 = a := UInt16.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem UInt32.xor_zero {a : UInt32} : a ^^^ 0 = a := UInt32.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem UInt64.xor_zero {a : UInt64} : a ^^^ 0 = a := UInt64.toBitVec_inj.1 BitVec.xor_zero
|
||||
@[simp] theorem USize.xor_zero {a : USize} : a ^^^ 0 = a := USize.toBitVec_inj.1 BitVec.xor_zero
|
||||
|
||||
@[simp] theorem UInt8.zero_xor {a : UInt8} : 0 ^^^ a = a := UInt8.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem UInt16.zero_xor {a : UInt16} : 0 ^^^ a = a := UInt16.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem UInt32.zero_xor {a : UInt32} : 0 ^^^ a = a := UInt32.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem UInt64.zero_xor {a : UInt64} : 0 ^^^ a = a := UInt64.toBitVec_inj.1 BitVec.zero_xor
|
||||
@[simp] theorem USize.zero_xor {a : USize} : 0 ^^^ a = a := USize.toBitVec_inj.1 BitVec.zero_xor
|
||||
|
||||
@[simp] theorem UInt8.neg_one_xor {a : UInt8} : -1 ^^^ a = ~~~a := by
|
||||
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_xor, UInt8.toBitVec_neg, UInt8.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt8.toBitVec_not]
|
||||
@[simp] theorem UInt16.neg_one_xor {a : UInt16} : -1 ^^^ a = ~~~a := by
|
||||
rw [← UInt16.toBitVec_inj, UInt16.toBitVec_xor, UInt16.toBitVec_neg, UInt16.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt16.toBitVec_not]
|
||||
@[simp] theorem UInt32.neg_one_xor {a : UInt32} : -1 ^^^ a = ~~~a := by
|
||||
rw [← UInt32.toBitVec_inj, UInt32.toBitVec_xor, UInt32.toBitVec_neg, UInt32.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt32.toBitVec_not]
|
||||
@[simp] theorem UInt64.neg_one_xor {a : UInt64} : -1 ^^^ a = ~~~a := by
|
||||
rw [← UInt64.toBitVec_inj, UInt64.toBitVec_xor, UInt64.toBitVec_neg, UInt64.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, UInt64.toBitVec_not]
|
||||
@[simp] theorem USize.neg_one_xor {a : USize} : -1 ^^^ a = ~~~a := by
|
||||
rw [← USize.toBitVec_inj, USize.toBitVec_xor, USize.toBitVec_neg, USize.toBitVec_one,
|
||||
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, USize.toBitVec_not]
|
||||
|
||||
@[simp] theorem UInt8.xor_neg_one {a : UInt8} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem UInt16.xor_neg_one {a : UInt16} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem UInt32.xor_neg_one {a : UInt32} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem UInt64.xor_neg_one {a : UInt64} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
@[simp] theorem USize.xor_neg_one {a : USize} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
|
||||
|
||||
instance : Std.LawfulCommIdentity (α := UInt8) (· ^^^ ·) 0 where
|
||||
right_id _ := UInt8.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt16) (· ^^^ ·) 0 where
|
||||
right_id _ := UInt16.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt32) (· ^^^ ·) 0 where
|
||||
right_id _ := UInt32.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := UInt64) (· ^^^ ·) 0 where
|
||||
right_id _ := UInt64.xor_zero
|
||||
instance : Std.LawfulCommIdentity (α := USize) (· ^^^ ·) 0 where
|
||||
right_id _ := USize.xor_zero
|
||||
|
||||
@[simp] theorem UInt8.xor_eq_zero_iff {a b : UInt8} : a ^^^ b = 0 ↔ a = b := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.xor_eq_zero_iff {a b : UInt16} : a ^^^ b = 0 ↔ a = b := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.xor_eq_zero_iff {a b : UInt32} : a ^^^ b = 0 ↔ a = b := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.xor_eq_zero_iff {a b : UInt64} : a ^^^ b = 0 ↔ a = b := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.xor_eq_zero_iff {a b : USize} : a ^^^ b = 0 ↔ a = b := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.xor_left_inj {a b : UInt8} (c : UInt8) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.xor_left_inj {a b : UInt16} (c : UInt16) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.xor_left_inj {a b : UInt32} (c : UInt32) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.xor_left_inj {a b : UInt64} (c : UInt64) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.xor_left_inj {a b : USize} (c : USize) : (a ^^^ c = b ^^^ c) ↔ a = b := by
|
||||
simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.xor_right_inj {a b : UInt8} (c : UInt8) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.xor_right_inj {a b : UInt16} (c : UInt16) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.xor_right_inj {a b : UInt32} (c : UInt32) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.xor_right_inj {a b : UInt64} (c : UInt64) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.xor_right_inj {a b : USize} (c : USize) : (c ^^^ a = c ^^^ b) ↔ a = b := by
|
||||
simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.not_zero : ~~~(0 : UInt8) = -1 := rfl
|
||||
@[simp] theorem UInt16.not_zero : ~~~(0 : UInt16) = -1 := rfl
|
||||
@[simp] theorem UInt32.not_zero : ~~~(0 : UInt32) = -1 := rfl
|
||||
@[simp] theorem UInt64.not_zero : ~~~(0 : UInt64) = -1 := rfl
|
||||
@[simp] theorem USize.not_zero : ~~~(0 : USize) = -1 := by simp [USize.not_eq_neg_sub]
|
||||
|
||||
@[simp] theorem UInt8.not_neg_one : ~~~(-1 : UInt8) = 0 := rfl
|
||||
@[simp] theorem UInt16.not_neg_one : ~~~(-1 : UInt16) = 0 := rfl
|
||||
@[simp] theorem UInt32.not_neg_one : ~~~(-1 : UInt32) = 0 := rfl
|
||||
@[simp] theorem UInt64.not_neg_one : ~~~(-1 : UInt64) = 0 := rfl
|
||||
@[simp] theorem USize.not_neg_one : ~~~(-1 : USize) = 0 := by simp [USize.not_eq_neg_sub]
|
||||
|
||||
@[simp] theorem UInt8.not_not {a : UInt8} : ~~~(~~~a) = a := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.not_not {a : UInt16} : ~~~(~~~a) = a := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.not_not {a : UInt32} : ~~~(~~~a) = a := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.not_not {a : UInt64} : ~~~(~~~a) = a := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.not_not {a : USize} : ~~~(~~~a) = a := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.not_inj {a b : UInt8} : ~~~a = ~~~b ↔ a = b := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.not_inj {a b : UInt16} : ~~~a = ~~~b ↔ a = b := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.not_inj {a b : UInt32} : ~~~a = ~~~b ↔ a = b := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.not_inj {a b : UInt64} : ~~~a = ~~~b ↔ a = b := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.not_inj {a b : USize} : ~~~a = ~~~b ↔ a = b := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.and_not_self {a : UInt8} : a &&& ~~~a = 0 := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.and_not_self {a : UInt16} : a &&& ~~~a = 0 := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.and_not_self {a : UInt32} : a &&& ~~~a = 0 := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.and_not_self {a : UInt64} : a &&& ~~~a = 0 := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.and_not_self {a : USize} : a &&& ~~~a = 0 := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.not_and_self {a : UInt8} : ~~~a &&& a = 0 := by simp [UInt8.and_comm]
|
||||
@[simp] theorem UInt16.not_and_self {a : UInt16} : ~~~a &&& a = 0 := by simp [UInt16.and_comm]
|
||||
@[simp] theorem UInt32.not_and_self {a : UInt32} : ~~~a &&& a = 0 := by simp [UInt32.and_comm]
|
||||
@[simp] theorem UInt64.not_and_self {a : UInt64} : ~~~a &&& a = 0 := by simp [UInt64.and_comm]
|
||||
@[simp] theorem USize.not_and_self {a : USize} : ~~~a &&& a = 0 := by simp [USize.and_comm]
|
||||
|
||||
@[simp] theorem UInt8.or_not_self {a : UInt8} : a ||| ~~~a = -1 := by
|
||||
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_or, UInt8.toBitVec_not, BitVec.or_not_self,
|
||||
UInt8.toBitVec_neg, UInt8.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem UInt16.or_not_self {a : UInt16} : a ||| ~~~a = -1 := by
|
||||
rw [← UInt16.toBitVec_inj, UInt16.toBitVec_or, UInt16.toBitVec_not, BitVec.or_not_self,
|
||||
UInt16.toBitVec_neg, UInt16.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem UInt32.or_not_self {a : UInt32} : a ||| ~~~a = -1 := by
|
||||
rw [← UInt32.toBitVec_inj, UInt32.toBitVec_or, UInt32.toBitVec_not, BitVec.or_not_self,
|
||||
UInt32.toBitVec_neg, UInt32.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem UInt64.or_not_self {a : UInt64} : a ||| ~~~a = -1 := by
|
||||
rw [← UInt64.toBitVec_inj, UInt64.toBitVec_or, UInt64.toBitVec_not, BitVec.or_not_self,
|
||||
UInt64.toBitVec_neg, UInt64.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
@[simp] theorem USize.or_not_self {a : USize} : a ||| ~~~a = -1 := by
|
||||
rw [← USize.toBitVec_inj, USize.toBitVec_or, USize.toBitVec_not, BitVec.or_not_self,
|
||||
USize.toBitVec_neg, USize.toBitVec_one, BitVec.negOne_eq_allOnes]
|
||||
|
||||
@[simp] theorem UInt8.not_or_self {a : UInt8} : ~~~a ||| a = -1 := by simp [UInt8.or_comm]
|
||||
@[simp] theorem UInt16.not_or_self {a : UInt16} : ~~~a ||| a = -1 := by simp [UInt16.or_comm]
|
||||
@[simp] theorem UInt32.not_or_self {a : UInt32} : ~~~a ||| a = -1 := by simp [UInt32.or_comm]
|
||||
@[simp] theorem UInt64.not_or_self {a : UInt64} : ~~~a ||| a = -1 := by simp [UInt64.or_comm]
|
||||
@[simp] theorem USize.not_or_self {a : USize} : ~~~a ||| a = -1 := by simp [USize.or_comm]
|
||||
|
||||
theorem UInt8.not_eq_comm {a b : UInt8} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem UInt16.not_eq_comm {a b : UInt16} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem UInt32.not_eq_comm {a b : UInt32} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem UInt64.not_eq_comm {a b : UInt64} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.not_eq_comm]
|
||||
theorem USize.not_eq_comm {a b : USize} : ~~~a = b ↔ a = ~~~b := by
|
||||
simp [← USize.toBitVec_inj, BitVec.not_eq_comm]
|
||||
|
||||
@[simp] theorem UInt8.ne_not_self {a : UInt8} : a ≠ ~~~a := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.ne_not_self {a : UInt16} : a ≠ ~~~a := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.ne_not_self {a : UInt32} : a ≠ ~~~a := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.ne_not_self {a : UInt64} : a ≠ ~~~a := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.ne_not_self {a : USize} : a ≠ ~~~a := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.not_ne_self {a : UInt8} : ~~~a ≠ a := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.not_ne_self {a : UInt16} : ~~~a ≠ a := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.not_ne_self {a : UInt32} : ~~~a ≠ a := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.not_ne_self {a : UInt64} : ~~~a ≠ a := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.not_ne_self {a : USize} : ~~~a ≠ a := by simp [← USize.toBitVec_inj]
|
||||
|
||||
theorem UInt8.not_xor {a b : UInt8} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem UInt16.not_xor {a b : UInt16} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem UInt32.not_xor {a b : UInt32} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem UInt64.not_xor {a b : UInt64} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.not_xor_left]
|
||||
theorem USize.not_xor {a b : USize} : ~~~a ^^^ b = ~~~(a ^^^ b) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.not_xor_left]
|
||||
|
||||
theorem UInt8.xor_not {a b : UInt8} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem UInt16.xor_not {a b : UInt16} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem UInt32.xor_not {a b : UInt32} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem UInt64.xor_not {a b : UInt64} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.not_xor_right]
|
||||
theorem USize.xor_not {a b : USize} : a ^^^ ~~~b = ~~~(a ^^^ b) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.not_xor_right]
|
||||
|
||||
@[simp] theorem UInt8.shiftLeft_zero {a : UInt8} : a <<< 0 = a := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.shiftLeft_zero {a : UInt16} : a <<< 0 = a := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.shiftLeft_zero {a : UInt32} : a <<< 0 = a := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.shiftLeft_zero {a : UInt64} : a <<< 0 = a := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.shiftLeft_zero {a : USize} : a <<< 0 = a := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.zero_shiftLeft {a : UInt8} : 0 <<< a = 0 := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.zero_shiftLeft {a : UInt16} : 0 <<< a = 0 := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.zero_shiftLeft {a : UInt32} : 0 <<< a = 0 := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.zero_shiftLeft {a : UInt64} : 0 <<< a = 0 := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.zero_shiftLeft {a : USize} : 0 <<< a = 0 := by simp [← USize.toBitVec_inj]
|
||||
|
||||
theorem UInt8.shiftLeft_xor {a b c : UInt8} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem UInt16.shiftLeft_xor {a b c : UInt16} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem UInt32.shiftLeft_xor {a b c : UInt32} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem UInt64.shiftLeft_xor {a b c : UInt64} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
theorem USize.shiftLeft_xor {a b c : USize} : (a ^^^ b) <<< c = (a <<< c) ^^^ (b <<< c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.shiftLeft_xor_distrib]
|
||||
|
||||
theorem UInt8.shiftLeft_and {a b c : UInt8} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem UInt16.shiftLeft_and {a b c : UInt16} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem UInt32.shiftLeft_and {a b c : UInt32} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem UInt64.shiftLeft_and {a b c : UInt64} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
theorem USize.shiftLeft_and {a b c : USize} : (a &&& b) <<< c = (a <<< c) &&& (b <<< c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.shiftLeft_and_distrib]
|
||||
|
||||
theorem UInt8.shiftLeft_or {a b c : UInt8} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem UInt16.shiftLeft_or {a b c : UInt16} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem UInt32.shiftLeft_or {a b c : UInt32} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem UInt64.shiftLeft_or {a b c : UInt64} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
theorem USize.shiftLeft_or {a b c : USize} : (a ||| b) <<< c = (a <<< c) ||| (b <<< c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.shiftLeft_or_distrib]
|
||||
|
||||
theorem UInt8.shiftLeft_add_of_toNat_lt {a b c : UInt8} (h : b.toNat + c.toNat < 8) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
simp [← UInt8.toBitVec_inj, Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (show b.toNat < 8 by omega),
|
||||
Nat.mod_eq_of_lt (show c.toNat < 8 by omega), BitVec.shiftLeft_add]
|
||||
theorem UInt16.shiftLeft_add_of_toNat_lt {a b c : UInt16} (h : b.toNat + c.toNat < 16) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
simp [← UInt16.toBitVec_inj, Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (show b.toNat < 16 by omega),
|
||||
Nat.mod_eq_of_lt (show c.toNat < 16 by omega), BitVec.shiftLeft_add]
|
||||
theorem UInt32.shiftLeft_add_of_toNat_lt {a b c : UInt32} (h : b.toNat + c.toNat < 32) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
simp [← UInt32.toBitVec_inj, Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (show b.toNat < 32 by omega),
|
||||
Nat.mod_eq_of_lt (show c.toNat < 32 by omega), BitVec.shiftLeft_add]
|
||||
theorem UInt64.shiftLeft_add_of_toNat_lt {a b c : UInt64} (h : b.toNat + c.toNat < 64) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
simp [← UInt64.toBitVec_inj, Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (show b.toNat < 64 by omega),
|
||||
Nat.mod_eq_of_lt (show c.toNat < 64 by omega), BitVec.shiftLeft_add]
|
||||
theorem USize.shiftLeft_add_of_toNat_lt {a b c : USize}
|
||||
(h : b.toNat + c.toNat < System.Platform.numBits) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
simp only [← USize.toBitVec_inj, USize.toBitVec_shiftLeft, USize.toBitVec_add,
|
||||
BitVec.natCast_eq_ofNat, BitVec.shiftLeft_eq', BitVec.toNat_umod, BitVec.toNat_add,
|
||||
toNat_toBitVec, BitVec.toNat_ofNat, Nat.mod_two_pow_self]
|
||||
rw [Nat.mod_eq_of_lt, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt, BitVec.shiftLeft_add]
|
||||
· omega
|
||||
· omega
|
||||
· exact Nat.lt_trans h Nat.lt_two_pow_self
|
||||
· exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h
|
||||
|
||||
theorem UInt8.shiftLeft_add {a b c : UInt8} (hb : b < 8) (hc : c < 8) (hbc : b + c < 8) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
apply UInt8.shiftLeft_add_of_toNat_lt
|
||||
have hb : b.toNat < 8 := by simpa [lt_iff_toNat_lt] using hb
|
||||
have hc : c.toNat < 8 := by simpa [lt_iff_toNat_lt] using hc
|
||||
simp only [lt_iff_toNat_lt, UInt8.toNat_add, Nat.reducePow, UInt8.reduceToNat] at hbc
|
||||
rwa [Nat.mod_eq_of_lt (by omega)] at hbc
|
||||
theorem UInt16.shiftLeft_add {a b c : UInt16} (hb : b < 16) (hc : c < 16) (hbc : b + c < 16) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
apply UInt16.shiftLeft_add_of_toNat_lt
|
||||
have hb : b.toNat < 16 := by simpa [lt_iff_toNat_lt] using hb
|
||||
have hc : c.toNat < 16 := by simpa [lt_iff_toNat_lt] using hc
|
||||
simp only [lt_iff_toNat_lt, UInt16.toNat_add, Nat.reducePow, UInt16.reduceToNat] at hbc
|
||||
rwa [Nat.mod_eq_of_lt (by omega)] at hbc
|
||||
theorem UInt32.shiftLeft_add {a b c : UInt32} (hb : b < 32) (hc : c < 32) (hbc : b + c < 32) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
apply UInt32.shiftLeft_add_of_toNat_lt
|
||||
have hb : b.toNat < 32 := by simpa [lt_iff_toNat_lt] using hb
|
||||
have hc : c.toNat < 32 := by simpa [lt_iff_toNat_lt] using hc
|
||||
simp only [lt_iff_toNat_lt, UInt32.toNat_add, Nat.reducePow, UInt32.reduceToNat] at hbc
|
||||
rwa [Nat.mod_eq_of_lt (by omega)] at hbc
|
||||
theorem UInt64.shiftLeft_add {a b c : UInt64} (hb : b < 64) (hc : c < 64) (hbc : b + c < 64) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
apply UInt64.shiftLeft_add_of_toNat_lt
|
||||
have hb : b.toNat < 64 := by simpa [lt_iff_toNat_lt] using hb
|
||||
have hc : c.toNat < 64 := by simpa [lt_iff_toNat_lt] using hc
|
||||
simp only [lt_iff_toNat_lt, UInt64.toNat_add, Nat.reducePow, UInt64.reduceToNat] at hbc
|
||||
rwa [Nat.mod_eq_of_lt (by omega)] at hbc
|
||||
theorem USize.shiftLeft_add {a b c : USize} (hb : b < USize.ofNat System.Platform.numBits)
|
||||
(hc : c < USize.ofNat System.Platform.numBits) (hbc : b + c < USize.ofNat System.Platform.numBits) :
|
||||
a <<< (b + c) = (a <<< b) <<< c := by
|
||||
apply USize.shiftLeft_add_of_toNat_lt
|
||||
have hb : b.toNat < System.Platform.numBits := by simpa [lt_iff_toNat_lt] using hb
|
||||
have hc : c.toNat < System.Platform.numBits := by simpa [lt_iff_toNat_lt] using hc
|
||||
simp only [lt_iff_toNat_lt, USize.toNat_add, toNat_ofNat', Nat.mod_two_pow_self] at hbc
|
||||
rwa [Nat.mod_eq_of_lt] at hbc
|
||||
cases System.Platform.numBits_eq <;> simp_all <;> omega
|
||||
|
||||
@[simp] theorem UInt8.neg_one_shiftLeft_and_shiftLeft {a b : UInt8} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← UInt8.shiftLeft_and]
|
||||
@[simp] theorem UInt16.neg_one_shiftLeft_and_shiftLeft {a b : UInt16} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← UInt16.shiftLeft_and]
|
||||
@[simp] theorem UInt32.neg_one_shiftLeft_and_shiftLeft {a b : UInt32} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← UInt32.shiftLeft_and]
|
||||
@[simp] theorem UInt64.neg_one_shiftLeft_and_shiftLeft {a b : UInt64} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← UInt64.shiftLeft_and]
|
||||
@[simp] theorem USize.neg_one_shiftLeft_and_shiftLeft {a b : USize} :
|
||||
(-1) <<< b &&& a <<< b = a <<< b := by simp [← USize.shiftLeft_and]
|
||||
|
||||
@[simp] theorem UInt8.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt8.shiftLeft_or]
|
||||
@[simp] theorem UInt16.neg_one_shiftLeft_or_shiftLeft {a b : UInt16} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt16.shiftLeft_or]
|
||||
@[simp] theorem UInt32.neg_one_shiftLeft_or_shiftLeft {a b : UInt32} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt32.shiftLeft_or]
|
||||
@[simp] theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt64.shiftLeft_or]
|
||||
@[simp] theorem USize.neg_one_shiftLeft_or_shiftLeft {a b : USize} :
|
||||
(-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← USize.shiftLeft_or]
|
||||
|
||||
@[simp] theorem UInt8.shiftRight_zero {a : UInt8} : a >>> 0 = a := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.shiftRight_zero {a : UInt16} : a >>> 0 = a := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.shiftRight_zero {a : UInt32} : a >>> 0 = a := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.shiftRight_zero {a : UInt64} : a >>> 0 = a := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.shiftRight_zero {a : USize} : a >>> 0 = a := by simp [← USize.toBitVec_inj]
|
||||
|
||||
@[simp] theorem UInt8.zero_shiftRight {a : UInt8} : 0 >>> a = 0 := by simp [← UInt8.toBitVec_inj]
|
||||
@[simp] theorem UInt16.zero_shiftRight {a : UInt16} : 0 >>> a = 0 := by simp [← UInt16.toBitVec_inj]
|
||||
@[simp] theorem UInt32.zero_shiftRight {a : UInt32} : 0 >>> a = 0 := by simp [← UInt32.toBitVec_inj]
|
||||
@[simp] theorem UInt64.zero_shiftRight {a : UInt64} : 0 >>> a = 0 := by simp [← UInt64.toBitVec_inj]
|
||||
@[simp] theorem USize.zero_shiftRight {a : USize} : 0 >>> a = 0 := by simp [← USize.toBitVec_inj]
|
||||
|
||||
theorem UInt8.shiftRight_xor {a b c : UInt8} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.ushiftRight_xor_distrib]
|
||||
theorem UInt16.shiftRight_xor {a b c : UInt16} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.ushiftRight_xor_distrib]
|
||||
theorem UInt32.shiftRight_xor {a b c : UInt32} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.ushiftRight_xor_distrib]
|
||||
theorem UInt64.shiftRight_xor {a b c : UInt64} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.ushiftRight_xor_distrib]
|
||||
theorem USize.shiftRight_xor {a b c : USize} : (a ^^^ b) >>> c = (a >>> c) ^^^ (b >>> c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.ushiftRight_xor_distrib]
|
||||
|
||||
theorem UInt8.shiftRight_and {a b c : UInt8} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.ushiftRight_and_distrib]
|
||||
theorem UInt16.shiftRight_and {a b c : UInt16} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.ushiftRight_and_distrib]
|
||||
theorem UInt32.shiftRight_and {a b c : UInt32} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.ushiftRight_and_distrib]
|
||||
theorem UInt64.shiftRight_and {a b c : UInt64} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.ushiftRight_and_distrib]
|
||||
theorem USize.shiftRight_and {a b c : USize} : (a &&& b) >>> c = (a >>> c) &&& (b >>> c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.ushiftRight_and_distrib]
|
||||
|
||||
theorem UInt8.shiftRight_or {a b c : UInt8} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← UInt8.toBitVec_inj, BitVec.ushiftRight_or_distrib]
|
||||
theorem UInt16.shiftRight_or {a b c : UInt16} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← UInt16.toBitVec_inj, BitVec.ushiftRight_or_distrib]
|
||||
theorem UInt32.shiftRight_or {a b c : UInt32} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← UInt32.toBitVec_inj, BitVec.ushiftRight_or_distrib]
|
||||
theorem UInt64.shiftRight_or {a b c : UInt64} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← UInt64.toBitVec_inj, BitVec.ushiftRight_or_distrib]
|
||||
theorem USize.shiftRight_or {a b c : USize} : (a ||| b) >>> c = (a >>> c) ||| (b >>> c) := by
|
||||
simp [← USize.toBitVec_inj, BitVec.ushiftRight_or_distrib]
|
||||
|
||||
theorem UInt8.and_le_right {a b : UInt8} : a &&& b ≤ b := by
|
||||
simpa [UInt8.le_iff_toNat_le] using Nat.and_le_right
|
||||
theorem UInt16.and_le_right {a b : UInt16} : a &&& b ≤ b := by
|
||||
simpa [UInt16.le_iff_toNat_le] using Nat.and_le_right
|
||||
theorem UInt32.and_le_right {a b : UInt32} : a &&& b ≤ b := by
|
||||
simpa [UInt32.le_iff_toNat_le] using Nat.and_le_right
|
||||
theorem UInt64.and_le_right {a b : UInt64} : a &&& b ≤ b := by
|
||||
simpa [UInt64.le_iff_toNat_le] using Nat.and_le_right
|
||||
theorem USize.and_le_right {a b : USize} : a &&& b ≤ b := by
|
||||
simpa [USize.le_iff_toNat_le] using Nat.and_le_right
|
||||
|
||||
theorem UInt8.and_le_left {a b : UInt8} : a &&& b ≤ a := by
|
||||
simpa [UInt8.le_iff_toNat_le] using Nat.and_le_left
|
||||
theorem UInt16.and_le_left {a b : UInt16} : a &&& b ≤ a := by
|
||||
simpa [UInt16.le_iff_toNat_le] using Nat.and_le_left
|
||||
theorem UInt32.and_le_left {a b : UInt32} : a &&& b ≤ a := by
|
||||
simpa [UInt32.le_iff_toNat_le] using Nat.and_le_left
|
||||
theorem UInt64.and_le_left {a b : UInt64} : a &&& b ≤ a := by
|
||||
simpa [UInt64.le_iff_toNat_le] using Nat.and_le_left
|
||||
theorem USize.and_le_left {a b : USize} : a &&& b ≤ a := by
|
||||
simpa [USize.le_iff_toNat_le] using Nat.and_le_left
|
||||
|
||||
theorem UInt8.left_le_or {a b : UInt8} : a ≤ a ||| b := by
|
||||
simpa [UInt8.le_iff_toNat_le] using Nat.left_le_or
|
||||
theorem UInt16.left_le_or {a b : UInt16} : a ≤ a ||| b := by
|
||||
simpa [UInt16.le_iff_toNat_le] using Nat.left_le_or
|
||||
theorem UInt32.left_le_or {a b : UInt32} : a ≤ a ||| b := by
|
||||
simpa [UInt32.le_iff_toNat_le] using Nat.left_le_or
|
||||
theorem UInt64.left_le_or {a b : UInt64} : a ≤ a ||| b := by
|
||||
simpa [UInt64.le_iff_toNat_le] using Nat.left_le_or
|
||||
theorem USize.left_le_or {a b : USize} : a ≤ a ||| b := by
|
||||
simpa [USize.le_iff_toNat_le] using Nat.left_le_or
|
||||
|
||||
theorem UInt8.right_le_or {a b : UInt8} : b ≤ a ||| b := by
|
||||
simpa [UInt8.le_iff_toNat_le] using Nat.right_le_or
|
||||
theorem UInt16.right_le_or {a b : UInt16} : b ≤ a ||| b := by
|
||||
simpa [UInt16.le_iff_toNat_le] using Nat.right_le_or
|
||||
theorem UInt32.right_le_or {a b : UInt32} : b ≤ a ||| b := by
|
||||
simpa [UInt32.le_iff_toNat_le] using Nat.right_le_or
|
||||
theorem UInt64.right_le_or {a b : UInt64} : b ≤ a ||| b := by
|
||||
simpa [UInt64.le_iff_toNat_le] using Nat.right_le_or
|
||||
theorem USize.right_le_or {a b : USize} : b ≤ a ||| b := by
|
||||
simpa [USize.le_iff_toNat_le] using Nat.right_le_or
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -3,12 +3,12 @@ namespace LongNamespaceExample
|
|||
|
||||
def x := 10
|
||||
|
||||
#check LongN
|
||||
--^ textDocument/completion
|
||||
#check LongNam
|
||||
--^ textDocument/completion
|
||||
end LongNamespaceExample
|
||||
|
||||
#check LongN
|
||||
--^ textDocument/completion
|
||||
#check LongNam
|
||||
--^ textDocument/completion
|
||||
end Foo
|
||||
|
||||
#check Foo.
|
||||
|
|
@ -18,5 +18,5 @@ end Foo
|
|||
--^ textDocument/completion
|
||||
open Foo
|
||||
|
||||
#check LongN
|
||||
--^ textDocument/completion
|
||||
#check LongNam
|
||||
--^ textDocument/completion
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 5, "character": 12}}
|
||||
"position": {"line": 5, "character": 14}}
|
||||
{"items":
|
||||
[{"label": "LongNamespaceExample",
|
||||
"kind": 9,
|
||||
|
|
@ -7,11 +7,11 @@
|
|||
"data":
|
||||
{"params":
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 5, "character": 12}},
|
||||
"position": {"line": 5, "character": 14}},
|
||||
"cPos": 0}}],
|
||||
"isIncomplete": false}
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 9, "character": 12}}
|
||||
"position": {"line": 9, "character": 14}}
|
||||
{"items":
|
||||
[{"label": "LongNamespaceExample",
|
||||
"kind": 9,
|
||||
|
|
@ -19,7 +19,7 @@
|
|||
"data":
|
||||
{"params":
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 9, "character": 12}},
|
||||
"position": {"line": 9, "character": 14}},
|
||||
"cPos": 0}}],
|
||||
"isIncomplete": false}
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
|
|
@ -47,7 +47,7 @@
|
|||
"cPos": 0}}],
|
||||
"isIncomplete": false}
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 20, "character": 12}}
|
||||
"position": {"line": 20, "character": 14}}
|
||||
{"items":
|
||||
[{"label": "LongNamespaceExample",
|
||||
"kind": 9,
|
||||
|
|
@ -55,6 +55,6 @@
|
|||
"data":
|
||||
{"params":
|
||||
{"textDocument": {"uri": "file:///compNamespace.lean"},
|
||||
"position": {"line": 20, "character": 12}},
|
||||
"position": {"line": 20, "character": 14}},
|
||||
"cPos": 0}}],
|
||||
"isIncomplete": false}
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ example : Int8.toInt (-8) + 8 = 0 := by simp +ground only
|
|||
#check_simp x = - (-2) ~> x = 2
|
||||
#check_simp x = -0 ~> x = 0
|
||||
#check_simp x = - (-0) ~> x = 0
|
||||
#check_simp x = - (-128) ~> x = -128
|
||||
#check_simp x = - (-128) ~> x = 128
|
||||
#check_simp x = - (-127) ~> x = 127
|
||||
#check_simp x = 2 + 3 ~> x = 5
|
||||
#check_simp x = -3 + 2 ~> x = -1
|
||||
|
|
@ -82,7 +82,7 @@ example : Int16.toInt (-16) + 16 = 0 := by simp +ground only
|
|||
#check_simp x = - (-2) ~> x = 2
|
||||
#check_simp x = -0 ~> x = 0
|
||||
#check_simp x = - (-0) ~> x = 0
|
||||
#check_simp x = - (-32768) ~> x = -32768
|
||||
#check_simp x = - (-32768) ~> x = 32768
|
||||
#check_simp x = - (-32767) ~> x = 32767
|
||||
#check_simp x = 2 + 3 ~> x = 5
|
||||
#check_simp x = -3 + 2 ~> x = -1
|
||||
|
|
@ -120,7 +120,7 @@ example : Int32.toInt (-32) + 32 = 0 := by simp +ground only
|
|||
#check_simp x = - (-2) ~> x = 2
|
||||
#check_simp x = -0 ~> x = 0
|
||||
#check_simp x = - (-0) ~> x = 0
|
||||
#check_simp x = - (-2147483648) ~> x = -2147483648
|
||||
#check_simp x = - (-2147483648) ~> x = 2147483648
|
||||
#check_simp x = - (-2147483647) ~> x = 2147483647
|
||||
#check_simp x = 2 + 3 ~> x = 5
|
||||
#check_simp x = -3 + 2 ~> x = -1
|
||||
|
|
@ -158,7 +158,7 @@ example : Int64.toInt (-64) + 64 = 0 := by simp +ground only
|
|||
#check_simp x = - (-2) ~> x = 2
|
||||
#check_simp x = -0 ~> x = 0
|
||||
#check_simp x = - (-0) ~> x = 0
|
||||
#check_simp x = - (-9223372036854775808) ~> x = -9223372036854775808
|
||||
#check_simp x = - (-9223372036854775808) ~> x = 9223372036854775808
|
||||
#check_simp x = - (-9223372036854775807) ~> x = 9223372036854775807
|
||||
#check_simp x = 2 + 3 ~> x = 5
|
||||
#check_simp x = -3 + 2 ~> x = -1
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue