toNat thms

opencompl · Dec 9, 2024 · 4f21275 · 4f21275
1 parent 520d4b6
commit 4f21275
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -2889,6 +2889,11 @@ theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
   · simp
     omega
 
+@[simp]
+theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
+    (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
+  simp only [rotateLeft, rotateLeftAux, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
 /-! ## Rotate Right -/
 
 /--
@@ -3026,6 +3031,12 @@ theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
     simp [h₁]
   · simp [show w = 0 by omega]
 
+@[simp]
+theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
+  simp only [rotateRight, rotateRightAux, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
+
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by