Initial simp sets

We add various mathlib lemmas to the simp sets defined in Interval.Tactic.Init.

theorem UInt64.apply_ite_toNat (c : Prop) {d : Decidable c} (x y : UInt64) : (if c then x else y).toNat = if c then x.toNat else y.toNat

theorem UInt64.apply_ite_toBitVec (c : Prop) {d : Decidable c} (x y : UInt64) : (if c then x else y).toBitVec = if c then x.toBitVec else y.toBitVec

theorem UInt64.apply_ite_toInt64 (c : Prop) {d : Decidable c} (x y : UInt64) : (if c then x else y).toInt64 = if c then x.toInt64 else y.toInt64

theorem Int64.apply_ite_toBitVec (c : Prop) {d : Decidable c} (x y : Int64) : (if c then x else y).toBitVec = if c then x.toBitVec else y.toBitVec

theorem BitVec.apply_ite_toInt (c : Prop) {d : Decidable c} (x y : BitVec 64) : (if c then x else y).toInt = if c then x.toInt else y.toInt

theorem BitVec.apply_ite_toNat (c : Prop) {d : Decidable c} (x y : BitVec 64) : (if c then x else y).toNat = if c then x.toNat else y.toNat

theorem Int.apply_ite_toNat (c : Prop) {d : Decidable c} (x y : ℤ) : (if c then x else y).toNat = if c then x.toNat else y.toNat

theorem BitVec.toNat_natCast (n : ℕ) : (↑n).toNat = n % 2 ^ 64

theorem BitVec.neg_eq_op {n : BitVec 64} : n.neg = -n

theorem BitVec.ofInt_inj_of_lt (n : ℕ) {x y : ℤ} (n0 : 0 < n) (x0 : -2 ^ (n - 1) ≤ x) (x1 : x < 2 ^ (n - 1)) (y0 : -2 ^ (n - 1) ≤ y) (y1 : y < 2 ^ (n - 1)) : x = y ↔ BitVec.ofInt n x = BitVec.ofInt n y