From 4f212754c19728014a0852e51e19ba908d612971 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sat, 7 Dec 2024 23:12:50 -0800
Subject: [PATCH] toNat thms

---
 src/Init/Data/BitVec/Lemmas.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 590bfcb7a7ad..d5327a79f620 100644
--- 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