moved lemmas from AFP to distribution
authorhaftmann
Sun, 15 Nov 2020 16:51:58 +0000
changeset 72856 4b2691211719
parent 72855 b519d819d376
child 72857 bafc0ec0e018
child 72859 429afd0d1a79
moved lemmas from AFP to distribution
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