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