# HG changeset patch
# User haftmann
# Date 1743942078 -7200
# Node ID 8b575e1fef3b88ee84f09527afb5158c8be4b00a
# Parent  04d4414b2c21a127a2843a3b86a0753b0c75300d
use existing implementations of bit operations if nat is implemented by target-language integer

diff -r 04d4414b2c21 -r 8b575e1fef3b NEWS
--- a/NEWS	Sun Apr 06 16:05:35 2025 +0200
+++ b/NEWS	Sun Apr 06 14:21:18 2025 +0200
@@ -43,6 +43,10 @@
 * Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
 Minor INCOMPATIBILITY.
 
+* If "HOL-Library.Code_Target_Nat" is imported, bit operations on nat are
+implemented by bit operations on target-language integer.
+Minor INCOMPATIBILITY.
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun
diff -r 04d4414b2c21 -r 8b575e1fef3b src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Apr 06 16:05:35 2025 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Apr 06 14:21:18 2025 +0200
@@ -11,7 +11,7 @@
 subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close>
 
 context
-includes natural.lifting and integer.lifting
+includes integer.lifting
 begin
 
 lift_definition Nat :: "integer \<Rightarrow> nat"
@@ -190,6 +190,60 @@
   "nat_of_integer (numeral k) = numeral k"
   including integer.lifting by (transfer, simp)+
 
+context
+  includes integer.lifting and bit_operations_syntax
+begin
+
+declare [[code drop: \<open>bit :: nat \<Rightarrow> _\<close>
+  \<open>and :: nat \<Rightarrow> _\<close> \<open>or :: nat \<Rightarrow> _\<close> \<open>xor :: nat \<Rightarrow> _\<close>
+  \<open>push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close> \<open>drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close> \<open>take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat\<close>]]
+
+lemma [code]:
+  \<open>bit m n \<longleftrightarrow> bit (integer_of_nat m) n\<close>
+  by transfer (simp add: bit_simps)
+
+lemma [code]:
+  \<open>integer_of_nat (m AND n) = integer_of_nat m AND integer_of_nat n\<close>
+  by transfer (simp add: of_nat_and_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (m OR n) = integer_of_nat m OR integer_of_nat n\<close>
+  by transfer (simp add: of_nat_or_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (m XOR n) = integer_of_nat m XOR integer_of_nat n\<close>
+  by transfer (simp add: of_nat_xor_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (push_bit n m) = push_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_push_bit)
+
+lemma [code]:
+  \<open>integer_of_nat (drop_bit n m) = drop_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_drop_bit)
+
+lemma [code]:
+  \<open>integer_of_nat (take_bit n m) = take_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_take_bit)
+
+lemma [code]:
+  \<open>integer_of_nat (mask n) = mask n\<close>
+  by transfer (simp add: of_nat_mask_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (set_bit n m) = set_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_set_bit_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (unset_bit n m) = unset_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_unset_bit_eq)
+
+lemma [code]:
+  \<open>integer_of_nat (flip_bit n m) = flip_bit n (integer_of_nat m)\<close>
+  by transfer (simp add: of_nat_flip_bit_eq)
+
+end
+
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith