# HG changeset patch
# User haftmann
# Date 1605435183 0
# Node ID c7bc3e70a8c77dc7773140b2161b8a0bb2582898
# Parent  00fce84413db8bd806976832638771d571156106
official collection for bit projection simplifications

diff -r 00fce84413db -r c7bc3e70a8c7 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Sun Nov 15 13:08:13 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Sun Nov 15 10:13:03 2020 +0000
@@ -16,9 +16,9 @@
     and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close>  59)
     and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
     and mask :: \<open>nat \<Rightarrow> 'a\<close>
-  assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
-    and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
-    and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+  assumes bit_and_iff [bit_simps]: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+    and bit_or_iff [bit_simps]: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+    and bit_xor_iff [bit_simps]: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
     and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
 begin
 
@@ -119,7 +119,7 @@
   \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
   by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
 
-lemma bit_mask_iff:
+lemma bit_mask_iff [bit_simps]:
   \<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
   by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
 
@@ -182,7 +182,7 @@
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
-  assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+  assumes bit_not_iff [bit_simps]: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
   assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
 begin
 
@@ -205,7 +205,7 @@
   \<open>- a = NOT a + 1\<close>
   using not_eq_complement [of a] by simp
 
-lemma bit_minus_iff:
+lemma bit_minus_iff [bit_simps]:
   \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
   by (simp add: minus_eq_not_minus_1 bit_not_iff)
 
@@ -213,7 +213,7 @@
   "even (NOT a) \<longleftrightarrow> odd a"
   using bit_not_iff [of a 0] by auto
 
-lemma bit_not_exp_iff:
+lemma bit_not_exp_iff [bit_simps]:
   \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
   by (auto simp add: bit_not_iff bit_exp_iff)
 
@@ -221,9 +221,9 @@
   \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
   by (simp add: bit_minus_iff)
 
-lemma bit_minus_exp_iff:
+lemma bit_minus_exp_iff [bit_simps]:
   \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
-  oops
+  by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
 
 lemma bit_minus_2_iff [simp]:
   \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
@@ -361,7 +361,7 @@
 definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>flip_bit n a = a XOR push_bit n 1\<close>
 
-lemma bit_set_bit_iff:
+lemma bit_set_bit_iff [bit_simps]:
   \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
   by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff)
 
@@ -369,7 +369,7 @@
   \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
   using bit_set_bit_iff [of m a 0] by auto
 
-lemma bit_unset_bit_iff:
+lemma bit_unset_bit_iff [bit_simps]:
   \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
   by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
 
@@ -377,7 +377,7 @@
   \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
   using bit_unset_bit_iff [of m a 0] by auto
 
-lemma bit_flip_bit_iff:
+lemma bit_flip_bit_iff [bit_simps]:
   \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
   by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
 
@@ -583,7 +583,7 @@
   \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
   by (simp add: not_int_def)
 
-lemma bit_not_int_iff:
+lemma bit_not_int_iff [bit_simps]:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
   for k :: int
   by (simp add: bit_not_int_iff' not_int_def)
@@ -973,7 +973,7 @@
   \<open>even (of_int k) \<longleftrightarrow> even k\<close>
   by (induction k rule: int_bit_induct) simp_all
 
-lemma bit_of_int_iff:
+lemma bit_of_int_iff [bit_simps]:
   \<open>bit (of_int k) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit k n\<close>
 proof (cases \<open>(2::'a) ^ n = 0\<close>)
   case True
@@ -1157,7 +1157,7 @@
 definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>concat_bit n k l = take_bit n k OR push_bit n l\<close>
 
-lemma bit_concat_bit_iff:
+lemma bit_concat_bit_iff [bit_simps]:
   \<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close>
   by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps)
 
@@ -1259,7 +1259,7 @@
   \<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
   by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
 
-lemma bit_signed_take_bit_iff:
+lemma bit_signed_take_bit_iff [bit_simps]:
   \<open>bit (signed_take_bit m a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit a (min m n)\<close>
   by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
     (use exp_eq_0_imp_not_bit in blast)
@@ -1560,11 +1560,11 @@
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-    by (auto simp add: bit_nat_iff and_nat_def bit_and_iff less_le bit_eq_iff)
+    by (simp add: and_nat_def bit_simps)
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-    by (auto simp add: bit_nat_iff or_nat_def bit_or_iff less_le bit_eq_iff)
+    by (simp add: or_nat_def bit_simps)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-    by (auto simp add: bit_nat_iff xor_nat_def bit_xor_iff less_le bit_eq_iff)
+    by (simp add: xor_nat_def bit_simps)
 qed (simp add: mask_nat_def)
 
 end
diff -r 00fce84413db -r c7bc3e70a8c7 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Nov 15 13:08:13 2020 +0000
+++ b/src/HOL/Library/Word.thy	Sun Nov 15 10:13:03 2020 +0000
@@ -1065,7 +1065,7 @@
 context semiring_bits
 begin
 
-lemma bit_unsigned_iff:
+lemma bit_unsigned_iff [bit_simps]:
   \<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
@@ -1175,7 +1175,7 @@
 context ring_bit_operations
 begin
 
-lemma bit_signed_iff:
+lemma bit_signed_iff [bit_simps]:
   \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: bit)
@@ -1779,10 +1779,10 @@
   \<open>shiftl1 = (*) 2\<close>
   by (rule ext, transfer) simp
 
-lemma bit_shiftl1_iff:
+lemma bit_shiftl1_iff [bit_simps]:
   \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
     for w :: \<open>'a::len word\<close>
-  by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps)
+  by (simp add: shiftl1_eq_mult_2 bit_double_iff not_le) (simp add: ac_simps)
 
 lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
   \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
@@ -1793,7 +1793,7 @@
   \<open>shiftr1 w = w div 2\<close>
   by transfer simp
 
-lemma bit_shiftr1_iff:
+lemma bit_shiftr1_iff [bit_simps]:
   \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
   by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff)
 
@@ -1820,7 +1820,7 @@
   \<open>setBit w n = set_bit n w\<close>
   by transfer simp
 
-lemma bit_setBit_iff:
+lemma bit_setBit_iff [bit_simps]:
   \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
   for w :: \<open>'a::len word\<close>
   by transfer (auto simp add: bit_set_bit_iff)
@@ -1833,7 +1833,7 @@
   \<open>clearBit w n = unset_bit n w\<close>
   by transfer simp
 
-lemma bit_clearBit_iff:
+lemma bit_clearBit_iff [bit_simps]:
   \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
   for w :: \<open>'a::len word\<close>
   by transfer (auto simp add: bit_unset_bit_iff)
@@ -1913,7 +1913,7 @@
   using signed_take_bit_decr_length_iff
   by (simp add: take_bit_drop_bit) force
 
-lemma bit_signed_drop_bit_iff:
+lemma bit_signed_drop_bit_iff [bit_simps]:
   \<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
@@ -2025,7 +2025,7 @@
     by simp
 qed
 
-lemma bit_word_rotr_iff:
+lemma bit_word_rotr_iff [bit_simps]:
   \<open>bit (word_rotr m w) n \<longleftrightarrow>
     n < LENGTH('a) \<and> bit w ((n + m) mod LENGTH('a))\<close>
   for w :: \<open>'a::len word\<close>
@@ -2057,13 +2057,13 @@
     by simp
 qed
 
-lemma bit_word_rotl_iff:
+lemma bit_word_rotl_iff [bit_simps]:
   \<open>bit (word_rotl m w) n \<longleftrightarrow>
     n < LENGTH('a) \<and> bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff)
 
-lemma bit_word_roti_iff:
+lemma bit_word_roti_iff [bit_simps]:
   \<open>bit (word_roti k w) n \<longleftrightarrow>
     n < LENGTH('a) \<and> bit w (nat ((int n + k) mod int LENGTH('a)))\<close>
   for w :: \<open>'a::len word\<close>
@@ -2130,7 +2130,7 @@
   for a :: \<open>'a::len word\<close> and b :: \<open>'b::len word\<close>
   by transfer (simp add: concat_bit_take_bit_eq)
 
-lemma bit_word_cat_iff:
+lemma bit_word_cat_iff [bit_simps]:
   \<open>bit (word_cat v w :: 'c::len word) n \<longleftrightarrow> n < LENGTH('c) \<and> (if n < LENGTH('b) then bit w n else bit v (n - LENGTH('b)))\<close> 
   for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close>
   by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff)
@@ -3623,7 +3623,7 @@
 lemmas word_and_le1 = xtrans(3) [OF word_ao_absorbs (4) [symmetric] le_word_or2]
 lemmas word_and_le2 = xtrans(3) [OF word_ao_absorbs (8) [symmetric] le_word_or2]
 
-lemma bit_horner_sum_bit_word_iff:
+lemma bit_horner_sum_bit_word_iff [bit_simps]:
   \<open>bit (horner_sum of_bool (2 :: 'a::len word) bs) n
     \<longleftrightarrow> n < min LENGTH('a) (length bs) \<and> bs ! n\<close>
   by transfer (simp add: bit_horner_sum_bit_iff)
@@ -3631,7 +3631,7 @@
 definition word_reverse :: \<open>'a::len word \<Rightarrow> 'a word\<close>
   where \<open>word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..<LENGTH('a)]))\<close>
 
-lemma bit_word_reverse_iff:
+lemma bit_word_reverse_iff [bit_simps]:
   \<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close>
   for w :: \<open>'a::len word\<close>
   by (cases \<open>n < LENGTH('a)\<close>)
@@ -3698,7 +3698,7 @@
   apply (simp add: drop_bit_take_bit min_def)
   done
 
-lemma bit_sshiftr1_iff:
+lemma bit_sshiftr1_iff [bit_simps]:
   \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
@@ -3714,7 +3714,7 @@
   using sint_signed_drop_bit_eq [of 1 w]
   by (simp add: drop_bit_Suc sshiftr1_eq_signed_drop_bit_Suc_0) 
 
-lemma bit_bshiftr1_iff:
+lemma bit_bshiftr1_iff [bit_simps]:
   \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
@@ -3813,7 +3813,7 @@
 context
 begin
 
-qualified lemma bit_mask_iff:
+qualified lemma bit_mask_iff [bit_simps]:
   \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
   by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
 
@@ -3945,7 +3945,7 @@
     then ucast (drop_bit (LENGTH('a) - n) w)
     else push_bit (n - LENGTH('a)) (ucast w))\<close>
 
-lemma bit_slice1_iff:
+lemma bit_slice1_iff [bit_simps]:
   \<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
     \<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
   for w :: \<open>'a::len word\<close>
@@ -3955,7 +3955,7 @@
 definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
   where \<open>slice n = slice1 (LENGTH('a) - n)\<close>
 
-lemma bit_slice_iff:
+lemma bit_slice_iff [bit_simps]:
   \<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: slice_def word_size bit_slice1_iff)
@@ -4008,7 +4008,7 @@
 definition revcast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
   where \<open>revcast = slice1 LENGTH('b)\<close>
 
-lemma bit_revcast_iff:
+lemma bit_revcast_iff [bit_simps]:
   \<open>bit (revcast w :: 'b::len word) n \<longleftrightarrow> LENGTH('b) - LENGTH('a) \<le> n \<and> n < LENGTH('b)
     \<and> bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\<close>
   for w :: \<open>'a::len word\<close>
diff -r 00fce84413db -r c7bc3e70a8c7 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Nov 15 13:08:13 2020 +0000
+++ b/src/HOL/Parity.thy	Sun Nov 15 10:13:03 2020 +0000
@@ -906,15 +906,17 @@
   \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
   by (auto intro: bit_eqI)
 
-lemma bit_exp_iff:
+named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
+
+lemma bit_exp_iff [bit_simps]:
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
   by (auto simp add: bit_iff_odd exp_div_exp_eq)
 
-lemma bit_1_iff:
+lemma bit_1_iff [bit_simps]:
   \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
   using bit_exp_iff [of 0 n] by simp
 
-lemma bit_2_iff:
+lemma bit_2_iff [bit_simps]:
   \<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
   using bit_exp_iff [of 1 n] by auto
 
@@ -931,7 +933,7 @@
   ultimately show ?thesis by (simp add: ac_simps)
 qed
 
-lemma bit_double_iff:
+lemma bit_double_iff [bit_simps]:
   \<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_iff_odd ac_simps)
@@ -1193,7 +1195,7 @@
 context semiring_bits
 begin
 
-lemma bit_of_bool_iff:
+lemma bit_of_bool_iff [bit_simps]:
   \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
 	by (simp add: bit_1_iff)
 
@@ -1201,7 +1203,7 @@
   \<open>even (of_nat n) \<longleftrightarrow> even n\<close>
   by (induction n rule: nat_bit_induct) simp_all
 
-lemma bit_of_nat_iff:
+lemma bit_of_nat_iff [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit m n\<close>
 proof (cases \<open>(2::'a) ^ n = 0\<close>)
   case True
@@ -1492,15 +1494,15 @@
   \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
   by (simp add: push_bit_eq_mult) auto
 
-lemma bit_push_bit_iff:
+lemma bit_push_bit_iff [bit_simps]:
   \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>
   by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff)
 
-lemma bit_drop_bit_eq:
+lemma bit_drop_bit_eq [bit_simps]:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
   by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)
 
-lemma bit_take_bit_iff:
+lemma bit_take_bit_iff [bit_simps]:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
   by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)
 
@@ -1763,7 +1765,7 @@
   "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
   by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
 
-lemma bit_of_nat_iff_bit [simp]:
+lemma bit_of_nat_iff_bit [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
 proof -
   have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
@@ -1778,7 +1780,7 @@
   \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
   by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
 
-lemma bit_push_bit_iff_of_nat_iff:
+lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
   \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
   by (auto simp add: bit_push_bit_iff)
 
@@ -1826,12 +1828,12 @@
     by (simp add: bit_Suc)
 qed
 
-lemma bit_minus_int_iff:
+lemma bit_minus_int_iff [bit_simps]:
   \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
   for k :: int
   using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
 
-lemma bit_nat_iff:
+lemma bit_nat_iff [bit_simps]:
   \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
 proof (cases \<open>k \<ge> 0\<close>)
   case True
@@ -1839,7 +1841,7 @@
   ultimately have \<open>k = int m\<close>
     by simp
   then show ?thesis
-    by (auto intro: ccontr)
+    by (simp add: bit_simps)
 next
   case False
   then show ?thesis
diff -r 00fce84413db -r c7bc3e70a8c7 src/HOL/String.thy
--- a/src/HOL/String.thy	Sun Nov 15 13:08:13 2020 +0000
+++ b/src/HOL/String.thy	Sun Nov 15 10:13:03 2020 +0000
@@ -121,7 +121,7 @@
 
 lemma char_of_nat [simp]:
   \<open>char_of (of_nat n) = char_of n\<close>
-  by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
+  by (simp add: char_of_def String.char_of_def drop_bit_of_nat bit_simps)
 
 end