more efficient conversions for symbolic representations

--- a/src/HOL/Code_Numeral.thy	Sun Apr 20 16:45:09 2025 +0200
+++ b/src/HOL/Code_Numeral.thy	Mon Apr 21 08:24:58 2025 +0200
@@ -837,6 +837,12 @@
      in if j = 0 then l' else l' + 1)"
   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
+lemma int_of_integer_code_nbe [code nbe]:
+  "int_of_integer 0 = 0"
+  "int_of_integer (Pos n) = Int.Pos n"
+  "int_of_integer (Neg n) = Int.Neg n"
+  by simp_all
+
 lemma integer_of_int_code [code]:
   "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
      else if k = 0 then 0
@@ -846,6 +852,12 @@
      in if j = 0 then l else l + 1)"
   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
+lemma integer_of_int_code_nbe [code nbe]:
+  "integer_of_int 0 = 0"
+  "integer_of_int (Int.Pos n) = Pos n"
+  "integer_of_int (Int.Neg n) = Neg n"
+  by simp_all
+
 hide_const (open) Pos Neg sub dup divmod_abs
 
 context