# HG changeset patch
# User wenzelm
# Date 1592663792 -7200
# Node ID 9d98a39aa509b7185c5e4c35b959b2c2c02b822d
# Parent  e18e9ac8c2051910725631b7c9ab22833a3d8a26# Parent  34be842f35310ccfe8692f536c374024a54412d1
merged

diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -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"
diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -123,7 +123,7 @@
       (simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
 qed
 
-lemma take_bit_eq_mask [code]:
+lemma take_bit_eq_mask:
   \<open>take_bit n a = a AND mask n\<close>
   by (rule bit_eqI)
     (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
@@ -194,16 +194,14 @@
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
     apply standard
-         apply (simp_all add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
-      apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
+         apply (simp_all add: bit_eq_iff)
+       apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
     done
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
-    apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
-         apply (simp_all add: bit_exp_iff, simp_all add: bit_def)
-        apply (metis local.bit_exp_iff local.bits_div_by_0)
-       apply (metis local.bit_exp_iff local.bits_div_by_0)
+    apply (simp add: fun_eq_iff bit_eq_iff bit.xor_def)
+    apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_xor_iff exp_eq_0_imp_not_bit)
     done
 qed
 
@@ -636,20 +634,6 @@
 
 unbundle integer.lifting natural.lifting
 
-context
-  includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_integer [transfer_rule]:
-  \<open>((pcr_integer :: int \<Rightarrow> integer \<Rightarrow> bool) ===> (=)) bit bit\<close>
-  by (unfold bit_def) transfer_prover
-
-lemma transfer_rule_bit_natural [transfer_rule]:
-  \<open>((pcr_natural :: nat \<Rightarrow> natural \<Rightarrow> bool) ===> (=)) bit bit\<close>
-  by (unfold bit_def) transfer_prover
-
-end
-
 instantiation integer :: ring_bit_operations
 begin
 
@@ -742,7 +726,7 @@
     beyond the boundary.  The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close>
     represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary.
 
-  \<^item> The projection on a single bit is then @{thm bit_def [where ?'a = int, no_vars]}.
+  \<^item> The projection on a single bit is then @{thm bit_iff_odd [where ?'a = int, no_vars]}.
 
   \<^item> This leads to the most fundamental properties of bit values:
 
diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/Library/Z2.thy
--- a/src/HOL/Library/Z2.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/Library/Z2.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -194,15 +194,19 @@
 
 end
 
-instance bit :: semiring_bits
+instantiation bit :: semiring_bits
+begin
+
+definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where [simp]: \<open>bit_bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close>
+
+instance
   apply standard
-                apply (auto simp add: power_0_left power_add)
-  apply (metis bit_not_1_iff of_bool_eq(2))
+                apply (auto simp add: power_0_left power_add set_iff)
+   apply (metis bit_not_1_iff of_bool_eq(2))
   done
 
-lemma bit_bit_iff [simp]:
-  \<open>bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close> for b :: bit
-  by (cases b; cases n) (simp_all add: bit_Suc)
+end
 
 instantiation bit :: semiring_bit_shifts
 begin
@@ -213,8 +217,11 @@
 definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
   where \<open>drop_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
 
+definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where \<open>take_bit n b = (if n = 0 then 0 else b)\<close> for b :: bit
+
 instance
-  by standard (simp_all add: push_bit_bit_def drop_bit_bit_def)
+  by standard (simp_all add: push_bit_bit_def drop_bit_bit_def take_bit_bit_def)
 
 end
 
diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/Parity.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -727,8 +727,16 @@
     and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
     and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
     and even_mult_exp_div_exp_iff: \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> m > n \<or> 2 ^ n = 0 \<or> (m \<le> n \<and> even (a div 2 ^ (n - m)))\<close>
+  fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
+  assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 begin
 
+text \<open>
+  Having \<^const>\<open>bit\<close> as definitional class operation
+  takes into account that specific instances can be implemented
+  differently wrt. code generation.
+\<close>
+
 lemma bits_div_by_0 [simp]:
   \<open>a div 0 = 0\<close>
   by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
@@ -782,16 +790,13 @@
   \<open>1 mod 2 = 1\<close>
   by (simp add: mod2_eq_if)
 
-definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
-  where \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
-
 lemma bit_0 [simp]:
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
-  by (simp add: bit_def)
+  by (simp add: bit_iff_odd)
 
 lemma bit_Suc:
   \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
-  using div_exp_eq [of a 1 n] by (simp add: bit_def)
+  using div_exp_eq [of a 1 n] by (simp add: bit_iff_odd)
 
 lemma bit_rec:
   \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
@@ -799,7 +804,7 @@
 
 lemma bit_0_eq [simp]:
   \<open>bit 0 = bot\<close>
-  by (simp add: fun_eq_iff bit_def)
+  by (simp add: fun_eq_iff bit_iff_odd)
 
 context
   fixes a
@@ -850,7 +855,7 @@
 
 lemma exp_eq_0_imp_not_bit:
   \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
-  using that by (simp add: bit_def)
+  using that by (simp add: bit_iff_odd)
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. 2 ^ n \<noteq> 0 \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
@@ -912,7 +917,7 @@
 
 lemma bit_exp_iff:
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
-  by (auto simp add: bit_def exp_div_exp_eq)
+  by (auto simp add: bit_iff_odd exp_div_exp_eq)
 
 lemma bit_1_iff:
   \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
@@ -924,7 +929,7 @@
 
 lemma even_bit_succ_iff:
   \<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close>
-  using that by (cases \<open>n = 0\<close>) (simp_all add: bit_def)
+  using that by (cases \<open>n = 0\<close>) (simp_all add: bit_iff_odd)
 
 lemma odd_bit_iff_bit_pred:
   \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
@@ -938,7 +943,7 @@
 lemma bit_double_iff:
   \<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
   using even_mult_exp_div_exp_iff [of a 1 n]
-  by (cases n, auto simp add: bit_def ac_simps)
+  by (cases n, auto simp add: bit_iff_odd ac_simps)
 
 lemma bit_eq_rec:
   \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
@@ -970,11 +975,11 @@
 
 lemma bit_mod_2_iff [simp]:
   \<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
-  by (cases a rule: parity_cases) (simp_all add: bit_def)
+  by (cases a rule: parity_cases) (simp_all add: bit_iff_odd)
 
 lemma bit_mask_iff:
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
-  by (simp add: bit_def even_mask_div_iff not_le)
+  by (simp add: bit_iff_odd even_mask_div_iff not_le)
 
 lemma bit_Numeral1_iff [simp]:
   \<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
@@ -1011,7 +1016,13 @@
   qed
 qed
 
-instance nat :: semiring_bits
+instantiation nat :: semiring_bits
+begin
+
+definition bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>bit_nat m n \<longleftrightarrow> odd (m div 2 ^ n)\<close>
+
+instance
 proof
   show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
     and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
@@ -1048,7 +1059,9 @@
     apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
     apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc)
     done
-qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff bit_nat_def)
+
+end
 
 lemma int_bit_induct [case_names zero minus even odd]:
   "P k" if zero_int: "P 0"
@@ -1107,7 +1120,13 @@
   qed
 qed
 
-instance int :: semiring_bits
+instantiation int :: semiring_bits
+begin
+
+definition bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>bit_int k n \<longleftrightarrow> odd (k div 2 ^ n)\<close>
+
+instance
 proof
   show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
     and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
@@ -1169,18 +1188,19 @@
     apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
     apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2))
     done
-qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le bit_int_def)
+
+end
 
 class semiring_bit_shifts = semiring_bits +
   fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
   fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
+  fixes take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  assumes take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
 begin
 
-definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
-
 text \<open>
   Logically, \<^const>\<open>push_bit\<close>,
   \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
@@ -1188,14 +1208,14 @@
   would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
   algebraic relationships between those operations.
   Having
-  \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
+  them as definitional class operations
   takes into account that specific instances of these can be implemented
   differently wrt. code generation.
 \<close>
 
 lemma bit_iff_odd_drop_bit:
   \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
-  by (simp add: bit_def drop_bit_eq_div)
+  by (simp add: bit_iff_odd drop_bit_eq_div)
 
 lemma even_drop_bit_iff_not_bit:
   \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
@@ -1359,15 +1379,15 @@
 
 lemma bit_push_bit_iff:
   \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close>
-  by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff)
+  by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
 
 lemma bit_drop_bit_eq:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
-  by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div)
+  by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
 
 lemma bit_take_bit_iff:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
-  by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div)
+  by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
 
 lemma stable_imp_drop_bit_eq:
   \<open>drop_bit n a = a\<close>
@@ -1419,12 +1439,11 @@
 definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
   where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
 
-instance proof
-  show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat
-    by (simp add: push_bit_nat_def)
-  show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
-    by (simp add: drop_bit_nat_def)
-qed
+definition take_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>take_bit_nat n m = m mod 2 ^ n\<close>
+
+instance
+  by standard (simp_all add: push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
 
 end
 
@@ -1437,12 +1456,11 @@
 definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>drop_bit_int n k = k div 2 ^ n\<close>
 
-instance proof
-  show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
-    by (simp add: push_bit_int_def)
-  show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
-    by (simp add: drop_bit_int_def)
-qed
+definition take_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>take_bit_int n k = k mod 2 ^ n\<close>
+
+instance
+  by standard (simp_all add: push_bit_int_def drop_bit_int_def take_bit_int_def)
 
 end
 
@@ -1538,7 +1556,7 @@
   also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
     by (simp add: of_nat_div)
   finally show ?thesis
-    by (simp add: bit_def semiring_bits_class.bit_def)
+    by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
 qed
 
 lemma of_nat_push_bit:
@@ -1631,20 +1649,24 @@
   by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
 
 lemma take_bit_minus:
-  "take_bit n (- (take_bit n k)) = take_bit n (- k)"
+  \<open>take_bit n (- take_bit n k) = take_bit n (- k)\<close>
     for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
 
 lemma take_bit_diff:
-  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
+  \<open>take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)\<close>
     for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
 
 lemma take_bit_nonnegative [simp]:
-  "take_bit n k \<ge> 0"
+  \<open>take_bit n k \<ge> 0\<close>
     for k :: int
   by (simp add: take_bit_eq_mod)
 
+lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
+  \<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
+  by simp
+
 lemma take_bit_minus_small_eq:
   \<open>take_bit n (- k) = 2 ^ n - k\<close> if \<open>0 < k\<close> \<open>k \<le> 2 ^ n\<close> for k :: int
 proof -
diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/Word/Word.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -662,8 +662,29 @@
     (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
       simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
 
-instance word :: (len) semiring_bits
+instantiation word :: (len) semiring_bits
+begin
+
+lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
+  is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
 proof
+  fix k l :: int and n :: nat
+  assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
+  proof (cases \<open>n < LENGTH('a)\<close>)
+    case True
+    from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
+      by simp
+    then show ?thesis
+      by (simp add: bit_take_bit_iff)
+  next
+    case False
+    then show ?thesis
+      by simp
+  qed
+qed
+
+instance proof
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
   for P and a :: \<open>'a word\<close>
@@ -682,6 +703,8 @@
     with rec [of a True] show ?case
       using bit_word_half_eq [of a True] by (simp add: ac_simps)
   qed
+  show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
+    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
   show \<open>0 div a = 0\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
@@ -747,21 +770,6 @@
   qed
 qed
 
-context
-  includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_word [transfer_rule]:
-  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
-proof -
-  let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
-  have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
-    by (unfold bit_def) transfer_prover
-  also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
-    by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
-  finally show ?thesis .
-qed
-
 end
 
 instantiation word :: (len) semiring_bit_shifts
@@ -788,11 +796,17 @@
   is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
   by (simp add: take_bit_eq_mod)
 
+lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
+  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
+
 instance proof
-  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
+  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
     by transfer (simp add: push_bit_eq_mult)
-  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
+  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
     by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
+  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
+    by transfer (auto simp flip: take_bit_eq_mod)
 qed
 
 end
@@ -916,6 +930,10 @@
   \<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close>
   by (simp add: shiftr_word_eq)
 
+lemma [code]:
+  \<open>take_bit n a = a AND Bit_Operations.mask n\<close> for a :: \<open>'a::len word\<close>
+  by (fact take_bit_eq_mask)
+
 lemma [code_abbrev]:
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
   by (fact push_bit_of_1)
@@ -944,12 +962,9 @@
   \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
   by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)
 
-definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
-  where [code_abbrev]: \<open>bit_word = bit\<close>
-
-lemma bit_word_iff [code]:
-  \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
-  by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
+lemma bit_word_iff_drop_bit_and [code]:
+  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+  by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
 
 
 subsection \<open>Shift operations\<close>
diff -r 34be842f3531 -r 9d98a39aa509 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sat Jun 20 16:18:33 2020 +0200
+++ b/src/HOL/ex/Word.thy	Sat Jun 20 16:36:32 2020 +0200
@@ -548,8 +548,29 @@
     (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
       simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
 
-instance word :: (len) semiring_bits
+instantiation word :: (len) semiring_bits
+begin
+
+lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
+  is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
 proof
+  fix k l :: int and n :: nat
+  assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
+  proof (cases \<open>n < LENGTH('a)\<close>)
+    case True
+    from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
+      by simp
+    then show ?thesis
+      by (simp add: bit_take_bit_iff)
+  next
+    case False
+    then show ?thesis
+      by simp
+  qed
+qed
+
+instance proof
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
   for P and a :: \<open>'a word\<close>
@@ -566,6 +587,8 @@
     with rec [of a True] show ?case
       using bit_word_half_eq [of a True] by (simp add: ac_simps)
   qed
+  show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
+    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
   show \<open>0 div a = 0\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
@@ -631,21 +654,6 @@
   qed
 qed
 
-context
-  includes lifting_syntax
-begin
-
-lemma transfer_rule_bit_word [transfer_rule]:
-  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
-proof -
-  let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
-  have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
-    by (unfold bit_def) transfer_prover
-  also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
-    by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
-  finally show ?thesis .
-qed
-
 end
 
 instantiation word :: (len) semiring_bit_shifts
@@ -672,11 +680,17 @@
   is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
   by (simp add: take_bit_eq_mod)
 
+lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
+  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
+
 instance proof
   show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
     by transfer (simp add: push_bit_eq_mult)
   show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
     by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
+  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
+    by transfer (auto simp flip: take_bit_eq_mod)
 qed
 
 end
@@ -723,12 +737,9 @@
   \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
   by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero)
 
-definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
-  where [code_abbrev]: \<open>bit_word = bit\<close>
-
-lemma bit_word_iff [code]:
-  \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
-  by (simp add: bit_word_def bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
+lemma bit_word_iff_drop_bit_and [code]:
+  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
+  by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
 
 lifting_update word.lifting
 lifting_forget word.lifting