src/HOL/Groups_List.thy

     using mono add_mono by blast
   thus ?case by simp
 qed
 
 
+subsection \<open>Horner sums\<close>
+
+context comm_semiring_0
+begin
+
+definition horner_sum :: \<open>('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a\<close>
+  where horner_sum_foldr: \<open>horner_sum f a xs = foldr (\<lambda>x b. f x + a * b) xs 0\<close>
+
+lemma horner_sum_simps [simp]:
+  \<open>horner_sum f a [] = 0\<close>
+  \<open>horner_sum f a (x # xs) = f x + a * horner_sum f a xs\<close>
+  by (simp_all add: horner_sum_foldr)
+
+lemma horner_sum_eq_sum_funpow:
+  \<open>horner_sum f a xs = (\<Sum>n = 0..<length xs. ((*) a ^^ n) (f (xs ! n)))\<close>
+proof (induction xs)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs)
+  then show ?case
+    by (simp add: sum.atLeast0_lessThan_Suc_shift sum_distrib_left del: sum.op_ivl_Suc)
+qed
+
+end
+
+context
+  includes lifting_syntax
+begin
+
+lemma horner_sum_transfer [transfer_rule]:
+  \<open>((B ===> A) ===> A ===> list_all2 B ===> A) horner_sum horner_sum\<close>
+  if [transfer_rule]: \<open>A 0 0\<close>
+    and [transfer_rule]: \<open>(A ===> A ===> A) (+) (+)\<close>
+    and [transfer_rule]: \<open>(A ===> A ===> A) (*) (*)\<close>
+  by (unfold horner_sum_foldr) transfer_prover
+
+end
+
+context comm_semiring_1
+begin
+
+lemma horner_sum_eq_sum:
+  \<open>horner_sum f a xs = (\<Sum>n = 0..<length xs. f (xs ! n) * a ^ n)\<close>
+proof -
+  have \<open>(*) a ^^ n = (*) (a ^ n)\<close> for n
+    by (induction n) (simp_all add: ac_simps)
+  then show ?thesis
+    by (simp add: horner_sum_eq_sum_funpow ac_simps)
+qed
+
+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 add: ac_simps mod_2_eq_odd)
+  qed
+qed
+
+end
+
+context unique_euclidean_semiring_with_bit_shifts
+begin
+
+lemma bit_horner_sum_bit_iff:
+  \<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
+
+
 subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close>
 
 lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   by (induct n) (auto simp add: comp_def length_concat sum_list_triv)