# HG changeset patch
# User haftmann
# Date 1605459118 0
# Node ID 4b2691211719d15aecc951732056386cedada784
# Parent  b519d819d376e7011caa9c9efd1edc354984379a
moved lemmas from AFP to distribution

diff -r b519d819d376 -r 4b2691211719 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sun Nov 15 22:26:13 2020 +0100
+++ b/src/HOL/Groups_List.thy	Sun Nov 15 16:51:58 2020 +0000
@@ -395,6 +395,12 @@
     by (simp add: horner_sum_eq_sum_funpow ac_simps)
 qed
 
+lemma horner_sum_append:
+  \<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close>
+  using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>]
+    atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>]
+  by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add)
+
 end
 
 context semiring_bit_shifts
@@ -433,7 +439,7 @@
 context unique_euclidean_semiring_with_bit_shifts
 begin
 
-lemma bit_horner_sum_bit_iff:
+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