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'"