# HG changeset patch
# User haftmann
# Date 1594490949 0
# Node ID 9b4135e8bade14f730f529c10a3e7af0e16bd789
# Parent  08348e364739b0b76d6bcba9e4a8a1bad4b2f0aa
a generic horner sum operation

diff -r 08348e364739 -r 9b4135e8bade src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sat Jul 11 18:09:08 2020 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sat Jul 11 18:09:09 2020 +0000
@@ -494,8 +494,12 @@
 
 subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
 
-definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
-  where "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
+definition poly :: \<open>'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>poly p a = horner_sum id a (coeffs p)\<close>
+
+lemma poly_eq_fold_coeffs:
+  \<open>poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)\<close>
+  by (induction p) (auto simp add: fun_eq_iff poly_def)
 
 lemma poly_0 [simp]: "poly 0 x = 0"
   by (simp add: poly_def)
@@ -575,7 +579,7 @@
 
 lemma poly_monom: "poly (monom a n) x = a * x ^ n"
   for a x :: "'a::comm_semiring_1"
-  by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_def)
+  by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_eq_fold_coeffs)
 
 lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
   by (auto simp: poly_eq_iff)
diff -r 08348e364739 -r 9b4135e8bade src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sat Jul 11 18:09:08 2020 +0000
+++ b/src/HOL/Groups_List.thy	Sat Jul 11 18:09:09 2020 +0000
@@ -339,6 +339,123 @@
 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"
diff -r 08348e364739 -r 9b4135e8bade src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Jul 11 18:09:08 2020 +0000
+++ b/src/HOL/Parity.thy	Sat Jul 11 18:09:09 2020 +0000
@@ -172,15 +172,6 @@
     by simp
 qed
 
-lemma mask_eq_seq_sum:
-  \<open>2 ^ n - 1 = ((\<lambda>k. 1 + k * 2) ^^ n) 0\<close>
-proof -
-  have \<open>2 ^ n = ((\<lambda>k. 1 + k * 2) ^^ n) 0 + 1\<close>
-    by (induction n) (simp_all add: ac_simps mult_2)
-  then show ?thesis
-    by simp
-qed
-
 end
 
 class ring_parity = ring + semiring_parity
diff -r 08348e364739 -r 9b4135e8bade src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Jul 11 18:09:08 2020 +0000
+++ b/src/HOL/String.thy	Sat Jul 11 18:09:09 2020 +0000
@@ -21,81 +21,6 @@
 
 subsubsection \<open>Bytes as datatype\<close>
 
-context unique_euclidean_semiring_with_bit_shifts
-begin
-
-lemma bit_horner_sum_iff:
-  \<open>bit (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) 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_eq:
-  \<open>take_bit n (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) = foldr (\<lambda>b k. of_bool b + k * 2) (take n bs) 0\<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 take_bit_rec [of n] Cons.prems Cons.IH [of m]
-    show ?thesis by (simp add: ac_simps)
-  qed
-qed
-
-lemma (in semiring_bit_shifts) take_bit_eq_horner_sum:
-  \<open>take_bit n a = foldr (\<lambda>b k. of_bool b + k * 2) (map (bit a) [0..<n]) 0\<close>
-proof (induction a arbitrary: n rule: bits_induct)
-  case (stable a)
-  have *: \<open>((\<lambda>k. k * 2) ^^ n) 0 = 0\<close>
-    by (induction n) simp_all
-  from stable have \<open>bit a = (\<lambda>_. odd a)\<close>
-    by (simp add: stable_imp_bit_iff_odd fun_eq_iff)
-  then have \<open>map (bit a) [0..<n] = replicate n (odd a)\<close>
-    by (simp add: map_replicate_const)
-  with stable show ?case
-    by (simp add: stable_imp_take_bit_eq mask_eq_seq_sum *)
-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
-
 datatype char =
   Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
        (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
@@ -104,12 +29,11 @@
 begin
 
 definition of_char :: \<open>char \<Rightarrow> 'a\<close>
-  where \<open>of_char c = foldr (\<lambda>b k. of_bool b + k * 2) 
-    [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c] 0\<close>
+  where \<open>of_char c = horner_sum of_bool 2 [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c]\<close>
 
 lemma of_char_Char [simp]:
   \<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
-    foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0\<close>
+    horner_sum of_bool 2 [b0, b1, b2, b3, b4, b5, b6, b7]\<close>
   by (simp add: of_char_def)
 
 end
@@ -126,7 +50,7 @@
 
 lemma char_of_char [simp]:
   \<open>char_of (of_char c) = c\<close>
-  by (simp only: of_char_def char_of_def bit_horner_sum_iff) simp
+  by (simp only: of_char_def char_of_def bit_horner_sum_bit_iff) simp
 
 lemma char_of_comp_of_char [simp]:
   "char_of \<circ> of_char = id"
@@ -159,7 +83,7 @@
   then have \<open>[odd a, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close>
     by simp
   then have \<open>of_char (char_of a) = take_bit 8 a\<close>
-    by (simp only: char_of_def of_char_def char.sel take_bit_eq_horner_sum)
+    by (simp only: char_of_def of_char_def char.sel horner_sum_bit_eq_take_bit)
   then show ?thesis
     by (simp add: take_bit_eq_mod)
 qed
@@ -440,7 +364,7 @@
 
 qualified lemma char_of_ascii_of [simp]:
   "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
-  by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_eq, simp)
+  by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_bit_eq, simp)
 
 qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
   morphisms explode Abs_literal
diff -r 08348e364739 -r 9b4135e8bade src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Sat Jul 11 18:09:08 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Sat Jul 11 18:09:09 2020 +0000
@@ -13,12 +13,8 @@
 context comm_semiring_1
 begin
  
-primrec radix_value :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a"
-  where "radix_value f b [] = 0"
-  | "radix_value f b (a # as) = f a + radix_value f b as * b"
-
 abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a"
-  where "unsigned_of_bits \<equiv> radix_value of_bool 2"
+  where "unsigned_of_bits \<equiv> horner_sum of_bool 2"
 
 lemma unsigned_of_bits_replicate_False [simp]:
   "unsigned_of_bits (replicate n False) = 0"