src/HOL/Int.thy

--- a/src/HOL/Int.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Int.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -2102,6 +2102,10 @@
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
 
+lemma sub_BitM_One_eq:
+  \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
+  by (cases n) simp_all
+
 text \<open>Implementations.\<close>
 
 lemma one_int_code [code]: "1 = Pos Num.One"