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