--- a/src/HOL/Library/Code_Binary_Nat.thy Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Thu Jun 26 17:25:29 2025 +0200
@@ -43,8 +43,6 @@
context
begin
-declare [[code drop: "plus :: nat \<Rightarrow> _"]]
-
lemma plus_nat_code [code]:
"nat_of_num k + nat_of_num l = nat_of_num (k + l)"
"m + 0 = (m::nat)"
@@ -79,24 +77,18 @@
Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def
sub_non_positive nat_add_distrib sub_non_negative)
-declare [[code drop: "minus :: nat \<Rightarrow> _"]]
-
lemma minus_nat_code [code]:
"nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
"m - 0 = (m::nat)"
"0 - n = (0::nat)"
by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
-declare [[code drop: "times :: nat \<Rightarrow> _"]]
-
lemma times_nat_code [code]:
"nat_of_num k * nat_of_num l = nat_of_num (k * l)"
"m * 0 = (0::nat)"
"0 * n = (0::nat)"
by (simp_all add: nat_of_num_numeral)
-declare [[code drop: "HOL.equal :: nat \<Rightarrow> _"]]
-
lemma equal_nat_code [code]:
"HOL.equal 0 (0::nat) \<longleftrightarrow> True"
"HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
@@ -108,24 +100,18 @@
"HOL.equal (n::nat) n \<longleftrightarrow> True"
by (rule equal_refl)
-declare [[code drop: "less_eq :: nat \<Rightarrow> _"]]
-
lemma less_eq_nat_code [code]:
"0 \<le> (n::nat) \<longleftrightarrow> True"
"nat_of_num k \<le> 0 \<longleftrightarrow> False"
"nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
by (simp_all add: nat_of_num_numeral)
-declare [[code drop: "less :: nat \<Rightarrow> _"]]
-
lemma less_nat_code [code]:
"(m::nat) < 0 \<longleftrightarrow> False"
"0 < nat_of_num l \<longleftrightarrow> True"
"nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
by (simp_all add: nat_of_num_numeral)
-declare [[code drop: Euclidean_Rings.divmod_nat]]
-
lemma divmod_nat_code [code]:
"Euclidean_Rings.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
"Euclidean_Rings.divmod_nat m 0 = (0, m)"
@@ -137,8 +123,6 @@
subsection \<open>Conversions\<close>
-declare [[code drop: of_nat]]
-
lemma of_nat_code [code]:
"of_nat 0 = 0"
"of_nat (nat_of_num k) = numeral k"