--- 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"