diff -r 235173749448 -r d45f5d4c41bd src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jun 19 18:44:36 2020 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Jun 20 05:56:28 2020 +0000
@@ -296,40 +296,34 @@
 instantiation integer :: semiring_bit_shifts
 begin
 
+lift_definition bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool\<close>
+  is bit .
+
 lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
-  is \<open>push_bit\<close> .
+  is push_bit .
 
 lift_definition drop_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
-  is \<open>drop_bit\<close> .
+  is drop_bit .
+
+lift_definition take_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
-context
-  includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
-  \<open>(pcr_integer ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
-  by (unfold bit_def) transfer_prover
-
-lemma [transfer_rule]:
-  \<open>((=) ===> pcr_integer ===> pcr_integer) take_bit take_bit\<close>
-  by (unfold take_bit_eq_mod) transfer_prover
-
-end
-
 instance integer :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
+  \<open>bit k n \<longleftrightarrow> odd (drop_bit n k)\<close>
   \<open>push_bit n k = k * 2 ^ n\<close>
-  \<open>drop_bit n k = k div 2 ^ n\<close> for k :: integer
-  by (fact push_bit_eq_mult drop_bit_eq_div)+
+  \<open>drop_bit n k = k div 2 ^ n\<close>
+  \<open>take_bit n k = k mod 2 ^ n\<close> for k :: integer
+  by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
@@ -1027,40 +1021,34 @@
 instantiation natural :: semiring_bit_shifts
 begin
 
+lift_definition bit_natural :: \<open>natural \<Rightarrow> nat \<Rightarrow> bool\<close>
+  is bit .
+
 lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
-  is \<open>push_bit\<close> .
+  is push_bit .
 
 lift_definition drop_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
-  is \<open>drop_bit\<close> .
+  is drop_bit .
+
+lift_definition take_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+  (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
-context
-  includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
-  \<open>(pcr_natural ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
-  by (unfold bit_def) transfer_prover
-
-lemma [transfer_rule]:
-  \<open>((=) ===> pcr_natural ===> pcr_natural) take_bit take_bit\<close>
-  by (unfold take_bit_eq_mod) transfer_prover
-
-end
-
 instance natural :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
+  \<open>bit m n \<longleftrightarrow> odd (drop_bit n m)\<close>
   \<open>push_bit n m = m * 2 ^ n\<close>
-  \<open>drop_bit n m = m div 2 ^ n\<close> for m :: natural
-  by (fact push_bit_eq_mult drop_bit_eq_div)+
+  \<open>drop_bit n m = m div 2 ^ n\<close>
+  \<open>take_bit n m = m mod 2 ^ n\<close> for m :: natural
+  by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"