diff -r fb9c119e5b49 -r d804e93ae9ff src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sun Aug 01 23:18:13 2021 +0200
+++ b/src/HOL/Groups_List.thy	Mon Aug 02 10:01:06 2021 +0000
@@ -403,80 +403,6 @@
 
 end
 
-context semiring_bit_shifts
-begin
-
-lemma horner_sum_bit_eq_take_bit:
-  \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
-proof (induction a arbitrary: n rule: bits_induct)
-  case (stable a)
-  moreover have \<open>bit a = (\<lambda>_. odd a)\<close>
-    using stable by (simp add: stable_imp_bit_iff_odd fun_eq_iff)
-  moreover have \<open>{q. q < n} = {0..<n}\<close>
-    by auto
-  ultimately show ?case
-    by (simp add: stable_imp_take_bit_eq horner_sum_eq_sum mask_eq_sum_exp)
-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_all add: ac_simps mod_2_eq_odd)
-  qed
-qed
-
-end
-
-context unique_euclidean_semiring_with_bit_shifts
-begin
-
-lemma bit_horner_sum_bit_iff [bit_simps]:
-  \<open>bit (horner_sum of_bool 2 bs) 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_bit_eq:
-  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
-
-end
-
-lemma horner_sum_of_bool_2_less:
-  \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close>
-proof -
-  have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close>
-    by (rule sum_mono) simp
-  also have \<open>\<dots> = 2 ^ length bs - 1\<close>
-    by (induction bs) simp_all
-  finally show ?thesis
-    by (simp add: horner_sum_eq_sum)
-qed
-
 
 subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close>