# HG changeset patch
# User haftmann
# Date 1583687269 0
# Node ID b612edee9b0cd19483b69cb7ebdff4f62b024a5a
# Parent  f10bffaa2bae4db5c58d80ee070ab5718c732841
more frugal simp rules for bit operations; more pervasive use of bit selector

diff -r f10bffaa2bae -r b612edee9b0c src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -88,7 +88,7 @@
 
 lemma [transfer_rule]:
   "((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
-  by (unfold of_bool_def [abs_def]) transfer_prover
+  by (unfold of_bool_def) transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_integer) int of_nat"
@@ -108,11 +108,11 @@
 
 lemma [transfer_rule]:
   "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
-  by (unfold Num.sub_def [abs_def]) transfer_prover
+  by (unfold Num.sub_def) transfer_prover
 
 lemma [transfer_rule]:
   "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
-  by (unfold power_def [abs_def]) transfer_prover
+  by (unfold power_def) transfer_prover
 
 end
 
@@ -218,13 +218,19 @@
 
 end
 
-lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
-  by (unfold min_def [abs_def]) transfer_prover
+context
+  includes lifting_syntax
+begin
 
 lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
-  by (unfold max_def [abs_def]) transfer_prover
+  \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) min min\<close>
+  by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) max max\<close>
+  by (unfold max_def) transfer_prover
+
+end
 
 lemma int_of_integer_min [simp]:
   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
@@ -304,9 +310,19 @@
 
 end
 
+context
+  includes lifting_syntax
+begin
+
 lemma [transfer_rule]:
-  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
-  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+  \<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 ..
 
@@ -372,10 +388,16 @@
 where
   [simp, code_post]: "Pos = numeral"
 
+context
+  includes lifting_syntax
+begin
+
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer numeral Pos"
+  \<open>((=) ===> pcr_integer) numeral Pos\<close>
   by simp transfer_prover
 
+end
+
 lemma Pos_fold [code_unfold]:
   "numeral Num.One = Pos Num.One"
   "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
@@ -386,9 +408,15 @@
 where
   [simp, code_abbrev]: "Neg n = - Pos n"
 
+context
+  includes lifting_syntax
+begin
+
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
-  by (simp add: Neg_def [abs_def]) transfer_prover
+  \<open>((=) ===> pcr_integer) (\<lambda>n. - numeral n) Neg\<close>
+  by (unfold Neg_def) transfer_prover
+
+end
 
 code_datatype "0::integer" Pos Neg
 
@@ -853,33 +881,39 @@
 
 instance natural :: Rings.dvd ..
 
+context
+  includes lifting_syntax
+begin
+
 lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
-  unfolding dvd_def by transfer_prover
+  \<open>(pcr_natural ===> pcr_natural ===> (\<longleftrightarrow>)) (dvd) (dvd)\<close>
+  by (unfold dvd_def) transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)"
-  by (unfold of_bool_def [abs_def]) transfer_prover
+  \<open>((\<longleftrightarrow>) ===> pcr_natural) of_bool of_bool\<close>
+  by (unfold of_bool_def) transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+  \<open>((=) ===> pcr_natural) (\<lambda>n. n) of_nat\<close>
 proof -
   have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
-    by (unfold of_nat_def [abs_def]) transfer_prover
+    by (unfold of_nat_def) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+  \<open>((=) ===> pcr_natural) numeral numeral\<close>
 proof -
-  have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+  have \<open>((=) ===> pcr_natural) numeral (\<lambda>n. of_nat (numeral n))\<close>
     by transfer_prover
   then show ?thesis by simp
 qed
 
 lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold power_def [abs_def]) transfer_prover
+  \<open>(pcr_natural ===> (=) ===> pcr_natural) (^) (^)\<close>
+  by (unfold power_def) transfer_prover
+
+end
 
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
@@ -921,13 +955,19 @@
 
 end
 
-lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold min_def [abs_def]) transfer_prover
+context
+  includes lifting_syntax
+begin
 
 lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold max_def [abs_def]) transfer_prover
+  \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) min min\<close>
+  by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) max max\<close>
+  by (unfold max_def) transfer_prover
+
+end
 
 lemma nat_of_natural_min [simp]:
   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
@@ -1001,9 +1041,19 @@
 
 end
 
+context
+  includes lifting_syntax
+begin
+
 lemma [transfer_rule]:
-  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+  \<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 ..
 
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -2002,6 +2002,10 @@
     by (simp add: of_nat_mod of_nat_diff)
 qed
 
+lemma of_bool_half_eq_0 [simp]:
+  \<open>of_bool b div 2 = 0\<close>
+  by simp
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Parity.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -168,6 +168,15 @@
     by simp
 qed
 
+lemma mask_eq_seq_sum:
+  \<open>2 ^ n - 1 = ((\<lambda>k. 1 + k * 2) ^^ n) 0\<close>
+proof -
+  have \<open>2 ^ n = ((\<lambda>k. 1 + k * 2) ^^ n) 0 + 1\<close>
+    by (induction n) (simp_all add: ac_simps mult_2)
+  then show ?thesis
+    by simp
+qed
+
 end
 
 class ring_parity = ring + semiring_parity
@@ -742,10 +751,14 @@
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
   by (simp add: bit_def)
 
-lemma bit_Suc [simp]:
+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)
 
+lemma bit_rec:
+  \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
+  by (cases n) (simp_all add: bit_Suc)
+
 lemma bit_0_eq [simp]:
   \<open>bit 0 = bot\<close>
   by (simp add: fun_eq_iff bit_def)
@@ -768,7 +781,7 @@
 
 lemma stable_imp_bit_iff_odd:
   \<open>bit a n \<longleftrightarrow> odd a\<close>
-  by (induction n) (simp_all add: stable)
+  by (induction n) (simp_all add: stable bit_Suc)
 
 end
 
@@ -781,11 +794,11 @@
 next
   case (rec a b)
   from rec.prems [of 1] have [simp]: \<open>b = odd a\<close>
-    by (simp add: rec.hyps)
+    by (simp add: rec.hyps bit_Suc)
   from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close>
     by simp
   have \<open>bit a n \<longleftrightarrow> odd a\<close> for n
-    using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp)
+    using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp bit_Suc)
   then have \<open>a div 2 = a\<close>
     by (rule rec.IH)
   then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close>
@@ -841,7 +854,7 @@
     from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
       by simp
     from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
-      using rec.prems [of \<open>Suc n\<close>] by simp
+      using rec.prems [of \<open>Suc n\<close>] by (simp add: bit_Suc)
     then have \<open>a = b div 2\<close>
       by (rule rec.IH)
     then have \<open>2 * a = 2 * (b div 2)\<close>
@@ -912,7 +925,7 @@
       moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
         by simp
       ultimately show ?thesis
-        by simp
+        by (simp add: bit_Suc)
     qed
   qed
 qed
@@ -1182,7 +1195,7 @@
   "take_bit 0 a = 0"
   by (simp add: take_bit_eq_mod)
 
-lemma take_bit_Suc [simp]:
+lemma take_bit_Suc:
   \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
 proof -
   have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
@@ -1193,13 +1206,17 @@
     using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
 qed
 
+lemma take_bit_rec:
+  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close>
+  by (cases n) (simp_all add: take_bit_Suc)
+
 lemma take_bit_of_0 [simp]:
   "take_bit n 0 = 0"
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_of_1 [simp]:
   "take_bit n 1 = of_bool (n > 0)"
-  by (cases n) simp_all
+  by (cases n) (simp_all add: take_bit_Suc)
 
 lemma drop_bit_of_0 [simp]:
   "drop_bit n 0 = 0"
@@ -1213,16 +1230,20 @@
   "drop_bit 0 = id"
   by (simp add: fun_eq_iff drop_bit_eq_div)
 
-lemma drop_bit_Suc [simp]:
+lemma drop_bit_Suc:
   "drop_bit (Suc n) a = drop_bit n (a div 2)"
   using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
 
+lemma drop_bit_rec:
+  "drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))"
+  by (cases n) (simp_all add: drop_bit_Suc)
+
 lemma drop_bit_half:
   "drop_bit n (a div 2) = drop_bit n a div 2"
-  by (induction n arbitrary: a) simp_all
+  by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)
 
 lemma drop_bit_of_bool [simp]:
-  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
+  "drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)"
   by (cases n) simp_all
 
 lemma take_bit_eq_0_imp_dvd:
@@ -1231,7 +1252,7 @@
 
 lemma even_take_bit_eq [simp]:
   \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
-  by (cases n) simp_all
+  by (simp add: take_bit_rec [of n a])
 
 lemma take_bit_take_bit [simp]:
   "take_bit m (take_bit n a) = take_bit (min m n) a"
@@ -1302,6 +1323,21 @@
   \<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)
 
+lemma stable_imp_drop_bit_eq:
+  \<open>drop_bit n a = a\<close>
+  if \<open>a div 2 = a\<close>
+  by (induction n) (simp_all add: that drop_bit_Suc)
+
+lemma stable_imp_take_bit_eq:
+  \<open>take_bit n a = (if even a then 0 else 2 ^ n - 1)\<close>
+    if \<open>a div 2 = a\<close>
+proof (rule bit_eqI)
+  fix m
+  assume \<open>2 ^ m \<noteq> 0\<close>
+  with that show \<open>bit (take_bit n a) m \<longleftrightarrow> bit (if even a then 0 else 2 ^ n - 1) m\<close>
+    by (simp add: bit_take_bit_iff bit_mask_iff stable_imp_bit_iff_odd)
+qed
+
 end
 
 instantiation nat :: semiring_bit_shifts
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -2072,7 +2072,7 @@
 begin
 
 lemma take_bit_sum:
-  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k a))))"
+  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
   for n :: nat
 proof (induction n arbitrary: a)
   case 0
@@ -2080,14 +2080,14 @@
     by simp
 next
   case (Suc n)
-  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a)))) = 
-    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))"
+  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) = 
+    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))"
     by (simp add: sum.atLeast_Suc_lessThan ac_simps)
-  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))
-    = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k (a div 2))))) * 2"
-    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double)
+  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))
+    = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
+    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
   finally show ?case
-    using Suc [of "a div 2"] by (simp add: ac_simps)
+    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc)
 qed
 
 end
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/String.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -21,6 +21,81 @@
 
 subsubsection \<open>Bytes as datatype\<close>
 
+context unique_euclidean_semiring_with_bit_shifts
+begin
+
+lemma bit_horner_sum_iff:
+  \<open>bit (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis
+      by simp
+  next
+    case (Suc m)
+    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
+    show ?thesis by simp
+  qed
+qed
+
+lemma take_bit_horner_sum_eq:
+  \<open>take_bit n (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) = foldr (\<lambda>b k. of_bool b + k * 2) (take n bs) 0\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis
+      by simp
+  next
+    case (Suc m)
+    with take_bit_rec [of n] Cons.prems Cons.IH [of m]
+    show ?thesis by (simp add: ac_simps)
+  qed
+qed
+
+lemma (in semiring_bit_shifts) take_bit_eq_horner_sum:
+  \<open>take_bit n a = foldr (\<lambda>b k. of_bool b + k * 2) (map (bit a) [0..<n]) 0\<close>
+proof (induction a arbitrary: n rule: bits_induct)
+  case (stable a)
+  have *: \<open>((\<lambda>k. k * 2) ^^ n) 0 = 0\<close>
+    by (induction n) simp_all
+  from stable have \<open>bit a = (\<lambda>_. odd a)\<close>
+    by (simp add: stable_imp_bit_iff_odd fun_eq_iff)
+  then have \<open>map (bit a) [0..<n] = replicate n (odd a)\<close>
+    by (simp add: map_replicate_const)
+  with stable show ?case
+    by (simp add: stable_imp_take_bit_eq mask_eq_seq_sum *)
+next
+  case (rec a b)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis
+      by simp
+  next
+    case (Suc m)
+    have \<open>map (bit (of_bool b + 2 * a)) [0..<Suc m] = b # map (bit (of_bool b + 2 * a)) [Suc 0..<Suc m]\<close>
+      by (simp only: upt_conv_Cons) simp
+    also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
+      by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
+    finally show ?thesis
+      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps)
+  qed
+qed
+
+end
+
 datatype char =
   Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
        (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
@@ -28,49 +103,37 @@
 context comm_semiring_1
 begin
 
-definition of_char :: "char \<Rightarrow> 'a"
-  where "of_char c = ((((((of_bool (digit7 c) * 2
-    + of_bool (digit6 c)) * 2
-    + of_bool (digit5 c)) * 2
-    + of_bool (digit4 c)) * 2
-    + of_bool (digit3 c)) * 2
-    + of_bool (digit2 c)) * 2
-    + of_bool (digit1 c)) * 2
-    + of_bool (digit0 c)"
+definition of_char :: \<open>char \<Rightarrow> 'a\<close>
+  where \<open>of_char c = foldr (\<lambda>b k. of_bool b + k * 2) 
+    [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c] 0\<close>
 
 lemma of_char_Char [simp]:
-  "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
-    foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0"
-  by (simp add: of_char_def ac_simps)
+  \<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
+    foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0\<close>
+  by (simp add: of_char_def)
 
 end
 
 context unique_euclidean_semiring_with_bit_shifts
 begin
 
-definition char_of :: "'a \<Rightarrow> char"
-  where "char_of n = Char (odd n) (odd (drop_bit 1 n))
-    (odd (drop_bit 2 n)) (odd (drop_bit 3 n))
-    (odd (drop_bit 4 n)) (odd (drop_bit 5 n))
-    (odd (drop_bit 6 n)) (odd (drop_bit 7 n))"
+definition char_of :: \<open>'a \<Rightarrow> char\<close>
+  where \<open>char_of n = Char (odd n) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close>
+
+lemma char_of_take_bit_eq:
+  \<open>char_of (take_bit n m) = char_of m\<close> if \<open>n \<ge> 8\<close>
+  using that by (simp add: char_of_def bit_take_bit_iff)
 
 lemma char_of_char [simp]:
-  "char_of (of_char c) = c"
-proof (cases c)
-  have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)"
-    if "n > 0" for q :: 'a and n :: nat and d :: bool
-    using that by (cases n) simp_all
-  case (Char d0 d1 d2 d3 d4 d5 d6 d7)
-  then show ?thesis
-    by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp
-qed
+  \<open>char_of (of_char c) = c\<close>
+  by (simp only: of_char_def char_of_def bit_horner_sum_iff) simp
 
 lemma char_of_comp_of_char [simp]:
   "char_of \<circ> of_char = id"
   by (simp add: fun_eq_iff)
 
 lemma inj_of_char:
-  "inj of_char"
+  \<open>inj of_char\<close>
 proof (rule injI)
   fix c d
   assume "of_char c = of_char d"
@@ -79,45 +142,61 @@
   then show "c = d"
     by simp
 qed
-  
+
+lemma of_char_eqI:
+  \<open>c = d\<close> if \<open>of_char c = of_char d\<close>
+  using that inj_of_char by (simp add: inj_eq)
+
 lemma of_char_eq_iff [simp]:
-  "of_char c = of_char d \<longleftrightarrow> c = d"
-  by (simp add: inj_eq inj_of_char)
+  \<open>of_char c = of_char d \<longleftrightarrow> c = d\<close>
+  by (auto intro: of_char_eqI)
 
 lemma of_char_of [simp]:
-  "of_char (char_of a) = a mod 256"
+  \<open>of_char (char_of a) = a mod 256\<close>
 proof -
-  have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}"
-    by auto
-  have "of_char (char_of (take_bit 8 a)) =
-    (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))"
-    by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit)
-  also have "\<dots> = take_bit 8 a"
-    using * take_bit_sum [of 8 a] by simp
-  also have "char_of(take_bit 8 a) = char_of a"
-    by (simp add: char_of_def drop_bit_take_bit)
-  finally show ?thesis
+  have \<open>[0..<8] = [0, Suc 0, 2, 3, 4, 5, 6, 7 :: nat]\<close>
+    by (simp add: upt_eq_Cons_conv)
+  then have \<open>[odd a, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close>
+    by simp
+  then have \<open>of_char (char_of a) = take_bit 8 a\<close>
+    by (simp only: char_of_def of_char_def char.sel take_bit_eq_horner_sum)
+  then show ?thesis
     by (simp add: take_bit_eq_mod)
 qed
 
 lemma char_of_mod_256 [simp]:
-  "char_of (n mod 256) = char_of n"
-  by (metis char_of_char of_char_of)
+  \<open>char_of (n mod 256) = char_of n\<close>
+  by (rule of_char_eqI) simp
 
 lemma of_char_mod_256 [simp]:
-  "of_char c mod 256 = of_char c"
-  by (metis char_of_char of_char_of)
+  \<open>of_char c mod 256 = of_char c\<close>
+proof -
+  have \<open>of_char (char_of (of_char c)) mod 256 = of_char (char_of (of_char c))\<close>
+    by (simp only: of_char_of) simp
+  then show ?thesis
+    by simp
+qed
 
 lemma char_of_quasi_inj [simp]:
-  "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256"
-  by (metis char_of_mod_256 of_char_of)
+  \<open>char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?Q
+  then show ?P
+    by (auto intro: of_char_eqI)
+next
+  assume ?P
+  then have \<open>of_char (char_of m) = of_char (char_of n)\<close>
+    by simp
+  then show ?Q
+    by simp
+qed
 
-lemma char_of_nat_eq_iff:
-  "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c"
-  by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce)
+lemma char_of_eq_iff:
+  \<open>char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c\<close>
+  by (auto intro: of_char_eqI simp add: take_bit_eq_mod)
 
 lemma char_of_nat [simp]:
-  "char_of (of_nat n) = char_of n"
+  \<open>char_of (of_nat n) = char_of n\<close>
   by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
 
 end
@@ -168,20 +247,20 @@
 begin
 
 lemma [transfer_rule]:
-  "(pcr_integer ===> (=)) (char_of :: int \<Rightarrow> char) (char_of :: integer \<Rightarrow> char)"
-  by (unfold char_of_def [abs_def]) transfer_prover
+  \<open>(pcr_integer ===> (=)) char_of char_of\<close>
+  by (unfold char_of_def) transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> pcr_integer) (of_char :: char \<Rightarrow> int) (of_char :: char \<Rightarrow> integer)"
-  by (unfold of_char_def [abs_def]) transfer_prover
+  \<open>((=) ===> pcr_integer) of_char of_char\<close>
+  by (unfold of_char_def) transfer_prover
 
 lemma [transfer_rule]:
-  "(pcr_natural ===> (=)) (char_of :: nat \<Rightarrow> char) (char_of :: natural \<Rightarrow> char)"
-  by (unfold char_of_def [abs_def]) transfer_prover
+  \<open>(pcr_natural ===> (=)) char_of char_of\<close>
+  by (unfold char_of_def) transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> pcr_natural) (of_char :: char \<Rightarrow> nat) (of_char :: char \<Rightarrow> natural)"
-  by (unfold of_char_def [abs_def]) transfer_prover
+  \<open>((=) ===> pcr_natural) of_char of_char\<close>
+  by (unfold of_char_def) transfer_prover
 
 end
 
@@ -326,7 +405,7 @@
      (q6, b6) = bit_cut_integer q5;
      (_, b7) = bit_cut_integer q6
     in Char b0 b1 b2 b3 b4 b5 b6 b7)"
-  by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div)
+  by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq bit_iff_odd_drop_bit drop_bit_eq_div)
 
 lemma integer_of_char_code [code]:
   "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
@@ -334,7 +413,7 @@
       of_bool b5) * 2 + of_bool b4) * 2 +
         of_bool b3) * 2 + of_bool b2) * 2 +
           of_bool b1) * 2 + of_bool b0"
-  by (simp only: integer_of_char_def of_char_def char.sel)
+  by (simp add: integer_of_char_def of_char_def)
 
 
 subsection \<open>Strings as dedicated type for target language code generation\<close>
@@ -361,8 +440,7 @@
 
 qualified lemma char_of_ascii_of [simp]:
   "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
-  by (cases c)
-    (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric])
+  by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_eq, simp)
 
 qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
   morphisms explode Abs_literal
@@ -632,9 +710,17 @@
   where [simp]: "Literal' = String.Literal"
 
 lemma [code]:
-  "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
-    [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s" 
-  unfolding Literal'_def by transfer (simp add: char_of_def)
+  \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
+    [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s\<close>
+proof -
+  have \<open>foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0 = of_char (Char b0 b1 b2 b3 b4 b5 b6 False)\<close>
+    by simp
+  moreover have \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
+    [of_char (Char b0 b1 b2 b3 b4 b5 b6 False)] + s\<close>
+    by (unfold Literal'_def) (transfer, simp only: list.simps comp_apply char_of_char, simp)
+  ultimately show ?thesis
+    by simp
+qed
 
 lemma [code_computation_unfold]:
   "String.Literal = Literal'"
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -1,4 +1,4 @@
-(*  Author:  Florian Haftmann, TUM
+ (*  Author:  Florian Haftmann, TUM
 *)
 
 section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>
@@ -44,11 +44,11 @@
 next
   case (Cons b bs)
   then show ?case
-    by (cases n) (simp_all add: ac_simps)
+    by (cases n) (simp_all add: ac_simps take_bit_Suc)
 qed
 
 lemma unsigned_of_bits_drop [simp]:
-  "unsigned_of_bits (drop n bs) = Parity.drop_bit n (unsigned_of_bits bs)"
+  "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)"
 proof (induction bs arbitrary: n)
   case Nil
   then show ?case
@@ -56,7 +56,7 @@
 next
   case (Cons b bs)
   then show ?case
-    by (cases n) simp_all
+    by (cases n) (simp_all add: drop_bit_Suc)
 qed
 
 lemma bit_unsigned_of_bits_iff:
@@ -68,7 +68,7 @@
 next
   case (Cons b bs)
   then show ?case
-    by (cases n) simp_all
+    by (cases n) (simp_all add: bit_Suc)
 qed
 
 primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
@@ -77,9 +77,9 @@
   | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
 
 lemma n_bits_of_eq_iff:
-  "n_bits_of n a = n_bits_of n b \<longleftrightarrow> Parity.take_bit n a = Parity.take_bit n b"
+  "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
   apply (induction n arbitrary: a b)
-   apply (auto elim!: evenE oddE)
+   apply (auto elim!: evenE oddE simp add: take_bit_Suc)
    apply (metis dvd_triv_right even_plus_one_iff)
   apply (metis dvd_triv_right even_plus_one_iff)
   done
@@ -97,8 +97,8 @@
 qed
 
 lemma unsigned_of_bits_n_bits_of [simp]:
-  "unsigned_of_bits (n_bits_of n a) = Parity.take_bit n a"
-  by (induction n arbitrary: a) (simp_all add: ac_simps)
+  "unsigned_of_bits (n_bits_of n a) = take_bit n a"
+  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc)
 
 end
 
@@ -236,7 +236,7 @@
 next
   case (Cons b bs)
   then show ?case
-    by (cases n; cases b; cases bs) simp_all
+    by (cases n; cases b; cases bs) (simp_all add: bit_Suc)
 qed
 
 lemma of_bits_append [simp]:
@@ -257,7 +257,7 @@
   by (auto simp add: of_bits_int_def)
 
 lemma of_bits_drop [simp]:
-  "of_bits (drop n bs) = Parity.drop_bit n (of_bits bs :: int)"
+  "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)"
     if "n < length bs"
 using that proof (induction bs arbitrary: n)
   case Nil
@@ -275,7 +275,7 @@
     with Cons.prems have "bs \<noteq> []"
       by auto
     with Suc Cons.IH [of n] Cons.prems show ?thesis
-      by (cases b) simp_all
+      by (cases b) (simp_all add: drop_bit_Suc)
   qed
 qed
 
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Bit_Operations.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -28,10 +28,6 @@
   are specified as definitional class operations.
 \<close>
 
-lemma stable_imp_drop_eq:
-  \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
-  by (induction n) (simp_all add: that)
-
 sublocale "and": semilattice \<open>(AND)\<close>
   by standard (auto simp add: bit_eq_iff bit_and_iff)
 
@@ -219,7 +215,7 @@
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close>
     by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma set_bit_Suc [simp]:
@@ -239,7 +235,7 @@
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *,
-        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
   qed
 qed
 
@@ -250,7 +246,7 @@
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close>
     by (simp add: bit_unset_bit_iff bit_double_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma unset_bit_Suc [simp]:
@@ -268,7 +264,7 @@
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *,
-         simp_all add: Suc)
+         simp_all add: Suc bit_Suc)
   qed
 qed
 
@@ -279,7 +275,7 @@
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close>
     by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma flip_bit_Suc [simp]:
@@ -299,7 +295,7 @@
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff,
-        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
   qed
 qed
 
@@ -348,7 +344,7 @@
 next
   case (Suc n)
   then show ?case
-    by (simp add: rec [of m n])
+    by (simp add: rec [of m n] bit_Suc)
 qed
 
 sublocale abel_semigroup F
@@ -461,7 +457,7 @@
 next
   case (Suc n)
   then show ?case
-    by (simp add: rec [of k l])
+    by (simp add: rec [of k l] bit_Suc)
 qed
 
 sublocale abel_semigroup F
@@ -514,7 +510,7 @@
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
-  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int)
+  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
 
 instance proof
   fix k l :: int and n :: nat
diff -r f10bffaa2bae -r b612edee9b0c src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/ex/Word.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -29,16 +29,16 @@
   then have "(k + 1) mod 2 = 1"
     by (simp add: even_iff_mod_2_eq_zero)
   with True show ?thesis
-    by (simp add: signed_take_bit_eq_take_bit)
+    by (simp add: signed_take_bit_eq_take_bit take_bit_Suc)
 next
   case False
   then show ?thesis
-    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
+    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one take_bit_Suc)
 qed
 
-lemma signed_take_bit_Suc [simp]:
+lemma signed_take_bit_Suc:
   "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
-  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
+  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps take_bit_Suc)
 
 lemma signed_take_bit_of_0 [simp]:
   "signed_take_bit n 0 = 0"
@@ -46,7 +46,7 @@
 
 lemma signed_take_bit_of_minus_1 [simp]:
   "signed_take_bit n (- 1) = - 1"
-  by (induct n) simp_all
+  by (induct n) (simp_all add: signed_take_bit_Suc)
 
 lemma signed_take_bit_eq_iff_take_bit_eq:
   "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
@@ -356,10 +356,10 @@
     by transfer simp
   show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
     for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd)
+    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
   show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
     for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd)
+    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
 qed
 
 
@@ -494,7 +494,7 @@
   have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
     by auto
   with False that show ?thesis
-    by (auto; transfer) simp_all
+    by transfer (simp add: eq_iff)
 next
   case True
   obtain n where length: \<open>LENGTH('a) = Suc n\<close>
@@ -533,7 +533,7 @@
         by (simp add: take_bit_eq_mod)
       with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
-        by auto
+        by (auto simp add: take_bit_Suc)
     qed
     ultimately show ?thesis
       by simp
@@ -592,7 +592,7 @@
   show \<open>(1 + a) div 2 = a div 2\<close>
     if \<open>even a\<close>
     for a :: \<open>'a word\<close>
-    using that by transfer (auto dest: le_Suc_ex)
+    using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc)
   show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
     for m n :: nat
     by transfer (simp, simp add: exp_div_exp_eq)