diff -r fe7238c01809 -r 7fa796a773a5 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Dec 19 22:19:27 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Dec 19 15:13:33 2024 +0100
@@ -136,6 +136,18 @@
   is Int.nat
   .
 
+lemma nat_of_integer_0 [simp]:
+  \<open>nat_of_integer 0 = 0\<close>
+  by transfer simp
+
+lemma nat_of_integer_1 [simp]:
+  \<open>nat_of_integer 1 = 1\<close>
+  by transfer simp
+
+lemma nat_of_integer_numeral [simp]:
+  \<open>nat_of_integer (numeral n) = numeral n\<close>
+  by transfer simp
+
 lemma nat_of_integer_of_nat [simp]:
   "nat_of_integer (of_nat n) = n"
   by transfer simp
@@ -1249,7 +1261,7 @@
 
 lemma [code]:
   \<open>integer_of_natural (mask n) = mask n\<close>
-  by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+  by transfer (simp add: mask_eq_exp_minus_1)
 
 lemma [code_abbrev]:
   "natural_of_integer (Code_Numeral.Pos k) = numeral k"