Theory Karatsuba.Monoid_Sums
section "Sums in Monoids"
theory Monoid_Sums
imports "HOL-Algebra.Ring" "Expander_Graphs.Extra_Congruence_Method" Karatsuba_Preliminaries "HOL-Library.Multiset" "HOL-Number_Theory.Residues" Karatsuba_Sum_Lemmas
begin
text "This section contains a version of @{term sum_list} for entries in some abelian monoid.
Contrary to @{term sum_list}, which is defined for the type class @{class comm_monoid_add}, this
version is for the locale @{locale abelian_monoid}.
After the definition, some simple lemmas about sums are proven for this sum function."
context abelian_monoid
begin
fun monoid_sum_list :: "['c ⇒ 'a, 'c list] ⇒ 'a" where
"monoid_sum_list f [] = 𝟬"
| "monoid_sum_list f (x # xs) = f x ⊕ monoid_sum_list f xs"
lemma "monoid_sum_list f xs = foldr (⊕) (map f xs) 𝟬"
by (induction xs) simp_all
end
text "The syntactic sugar used for @{const finsum} is adapted accordingly."
syntax
"_monoid_sum_list" :: "index ⇒ idt ⇒ 'c list ⇒ 'c ⇒ 'a"
("(3⨁__←_. _)" [1000, 0, 51, 10] 10)
translations
"⨁⇘G⇙i←xs. b" ⇌ "CONST abelian_monoid.monoid_sum_list G (λi. b) xs"
context abelian_monoid
begin
lemma monoid_sum_list_finsum:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes "distinct xs"
shows "(⨁i ← xs. f i) = (⨁i ∈ set xs. f i)"
using assms
proof (induction xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case using finsum_insert[of "set xs" a f] by simp
qed
lemma monoid_sum_list_cong:
assumes "⋀i. i ∈ set xs ⟹ f i = g i"
shows "(⨁i ← xs. f i) = (⨁i ← xs. g i)"
using assms by (induction xs) simp_all
lemma monoid_sum_list_closed[simp]:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
shows "(⨁i ← xs. f i) ∈ carrier G"
using assms by (induction xs) simp_all
lemma monoid_sum_list_add_in:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes "⋀i. i ∈ set xs ⟹ g i ∈ carrier G"
shows "(⨁i ← xs. f i) ⊕ (⨁i ← xs. g i) =
(⨁i ← xs. f i ⊕ g i)"
using assms
proof (induction xs)
case (Cons a xs)
have "(⨁i ← (a # xs). f i) ⊕ (⨁i ← (a # xs). g i)
= (f a ⊕ (⨁i ← xs. f i)) ⊕ (g a ⊕ (⨁i ← xs. g i))"
by simp
also have "... = (f a ⊕ g a) ⊕ ((⨁i ← xs. f i) ⊕ (⨁i ← xs. g i))"
using a_comm a_assoc Cons.prems by simp
also have "... = (f a ⊕ g a) ⊕ (⨁i ← xs. f i ⊕ g i)"
using Cons by simp
finally show ?case by simp
qed simp
lemma monoid_sum_list_0[simp]: "(⨁i ← xs. 𝟬) = 𝟬"
by (induction xs) simp_all
lemma monoid_sum_list_swap:
assumes[simp]: "⋀i j. i ∈ set xs ⟹ j ∈ set ys ⟹ f i j ∈ carrier G"
shows "(⨁i ← xs. (⨁j ← ys. f i j)) =
(⨁j ← ys. (⨁i ← xs. f i j))"
using assms
proof (induction xs arbitrary: ys)
case (Cons a xs)
have "(⨁i ← (a # xs). (⨁j ← ys. f i j))
= (⨁j ← ys. f a j) ⊕ (⨁i ← xs. (⨁j ← ys. f i j))"
by simp
also have "... = (⨁j ← ys. f a j) ⊕ (⨁j ← ys. (⨁i ← xs. f i j))"
using Cons by simp
also have "... = (⨁j ← ys. f a j ⊕ (⨁i ← xs. f i j))"
using monoid_sum_list_add_in[of ys "λj. f a j" "λj. (⨁i ← xs. f i j)"] Cons.prems by simp
finally show ?case by simp
qed simp
lemma monoid_sum_list_index_transformation:
"(⨁i ← (map g xs). f i) = (⨁i ← xs. f (g i))"
by (induction xs) simp_all
lemma monoid_sum_list_index_shift_0:
"(⨁i ← [c..<c+n]. f i) = (⨁i ← [0..<n]. f (c + i))"
using monoid_sum_list_index_transformation[of f "λi. c + i" "[0..<n]"]
by (simp add: add.commute map_add_upt)
lemma monoid_sum_list_index_shift:
"(⨁l ← [a..<b]. f (l+c)) = (⨁l ← [(a+c)..<(b+c)]. f l)"
using monoid_sum_list_index_transformation[of f "λi. i + c" "[a..<b]"]
by (simp add: map_add_const_upt)
lemma monoid_sum_list_app:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes "⋀i. i ∈ set ys ⟹ f i ∈ carrier G"
shows "(⨁i ← xs @ ys. f i) = (⨁i ← xs. f i) ⊕ (⨁i ← ys. f i)"
using assms
by (induction xs) (simp_all add: a_assoc)
lemma monoid_sum_list_app':
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes "⋀i. i ∈ set ys ⟹ f i ∈ carrier G"
assumes "xs @ ys = zs"
shows "(⨁i ← zs. f i) = (⨁i ← xs. f i) ⊕ (⨁i ← ys. f i)"
using monoid_sum_list_app assms by blast
lemma :
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes "⋀i. i ∈ set ys ⟹ f i ∈ carrier G"
assumes "f x ∈ carrier G"
shows "(⨁i ← xs @ x # ys. f i) = f x ⊕ (⨁i ← (xs @ ys). f i)"
proof -
have "(⨁i ← xs @ x # ys. f i) = (⨁i ← xs. f i) ⊕ f x ⊕ (⨁i ← ys. f i)"
using assms monoid_sum_list_app[of xs f "x # ys"]
using a_assoc by auto
also have "... = f x ⊕ ((⨁i ← xs. f i) ⊕ (⨁i ← ys. f i))"
using assms a_assoc a_comm by auto
finally show ?thesis using monoid_sum_list_app[of xs f ys] assms by algebra
qed
lemma monoid_sum_list_Suc:
assumes "⋀i. i < Suc r ⟹ f i ∈ carrier G"
shows "(⨁i ← [0..<Suc r]. f i) = (⨁i ← [0..<r]. f i) ⊕ f r"
using assms monoid_sum_list_app[of "[0..<r]" f "[r]"]
by simp
lemma bij_betw_diff_singleton: "a ∈ A ⟹ b ∈ B ⟹ bij_betw f A B ⟹ f a = b ⟹ bij_betw f (A - {a}) (B - {b})"
by (metis (no_types, lifting) DiffE Diff_Diff_Int Diff_cancel Diff_empty Int_insert_right_if1 Un_Diff_Int notIn_Un_bij_betw3 singleton_iff)
lemma "a ∈ A ⟹ bij_betw f A B ⟹ bij_betw f (A - {a}) (B - {f a})"
using bij_betw_diff_singleton[of a A "f a" B f]
by (simp add: bij_betwE)
lemma monoid_sum_list_multiset_eq:
assumes "mset xs = mset ys"
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
shows "(⨁i ← xs. f i) = (⨁i ← ys. f i)"
using assms
proof (induction xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons a xs)
then have "a ∈ set ys" using mset_eq_setD by fastforce
then obtain ys1 ys2 where "ys = ys1 @ a # ys2" by (meson split_list)
with Cons.prems have 1: "mset xs = mset (ys1 @ ys2)" by simp
from Cons.prems mset_eq_setD have "⋀i. i ∈ set ys ⟹ f i ∈ carrier G" by blast
then have[simp]: "⋀i. i ∈ set ys1 ⟹ f i ∈ carrier G" "f a ∈ carrier G" "⋀i. i ∈ set ys2 ⟹ f i ∈ carrier G"
using ‹ys = ys1 @ a # ys2› by simp_all
from 1 have "(⨁i ← xs. f i) = (⨁i ← (ys1 @ ys2). f i)"
using Cons by simp
also have "... = (⨁i ← ys1. f i) ⊕ (⨁i ← ys2. f i)"
by (intro monoid_sum_list_app) simp_all
also have "f a ⊕ ... = (⨁i ← ys1. f i) ⊕ (f a ⊕ (⨁i ← ys2. f i))"
using a_comm a_assoc monoid_sum_list_closed by simp
also have "... = (⨁i ← ys1. f i) ⊕ (⨁i ← (a # ys2). f i)"
by simp
also have "... = (⨁i ← ys. f i)"
unfolding ‹ys = ys1 @ a # ys2›
by (intro monoid_sum_list_app[symmetric]) auto
finally show ?case by simp
qed
lemma monoid_sum_list_index_permutation:
assumes "distinct xs"
assumes "distinct ys ∨ length xs = length ys"
assumes "bij_betw f (set xs) (set ys)"
assumes "⋀i. i ∈ set ys ⟹ g i ∈ carrier G"
shows "(⨁i ← ys. g i) = (⨁i ← xs. g (f i))"
using assms
proof (induction xs arbitrary: ys)
case Nil
then have "ys = []" using bij_betw_same_card by fastforce
then show ?case by simp
next
case (Cons a xs)
then have "length ys = length (a # xs)" "distinct ys"
by (metis bij_betw_same_card distinct_card, metis bij_betw_same_card distinct_card card_distinct)
have 0: "⋀i. i ∈ set (a # xs) ⟹ g (f i) ∈ carrier G"
proof -
fix i
assume "i ∈ set (a # xs)"
then have "f i ∈ set ys" using Cons.prems(3) by (simp add: bij_betw_apply)
then show "g (f i) ∈ carrier G" using Cons.prems(4) by blast
qed
define b where "b = f a"
then have "b ∈ set ys" using Cons(4) bij_betw_apply by fastforce
then obtain ys1 ys2 where "ys = ys1 @ b # ys2" by (meson split_list)
then have "b ∉ set ys1" "b ∉ set ys2" using ‹distinct ys› by simp_all
have "bij_betw f (set xs) (set (ys1 @ ys2))"
using ‹ys = ys1 @ b # ys2› Cons(4) b_def
using bij_betw_diff_singleton[of a "set (a # xs)" "f a" "set ys" f]
using Cons.prems(1) ‹distinct ys› by auto
moreover have "length (ys1 @ ys2) = length xs" using ‹length ys = length (a # xs)› ‹ys = ys1 @ b # ys2›
by simp
ultimately have 1: "(⨁i ← (ys1@ys2). g i) = (⨁i ← xs. g (f i))" using Cons.IH[of "ys1@ys2"] Cons.prems(4)
using Cons.prems(1) 0 ‹ys = ys1 @ b # ys2› by auto
have "(⨁i ← (a # xs). g (f i)) = g b ⊕ (⨁i ← xs. g (f i))"
using ‹b = f a› by simp
also have "... = g b ⊕ (⨁i ← (ys1@ys2). g i)" using 1 by simp
also have "... = (⨁i ← (ys1@b#ys2). g i)"
apply (intro monoid_sum_list_extract[symmetric])
using Cons.prems(4) ‹ys = ys1 @ b # ys2› by simp_all
finally show "(⨁i ← ys. g i) = (⨁i ← (a # xs). g (f i))"
using ‹ys = ys1 @ b # ys2› by simp
qed
lemma monoid_sum_list_split:
assumes[simp]: "⋀i. i < b + c ⟹ f i ∈ carrier G"
shows "(⨁l ← [0..<b]. f l) ⊕ (⨁l ← [b..< b + c]. f l) = (⨁l ← [0..< b + c]. f l)"
using monoid_sum_list_app[of "[0..<b]" f "[b..< b + c]", symmetric]
using upt_add_eq_append[of 0 b c]
by simp
lemma monoid_sum_list_splice:
assumes[simp]: "⋀i. i < 2 * n ⟹ f i ∈ carrier G"
shows "(⨁i ← [0..< 2 * n]. f i) = (⨁i ← [0..<n]. f (2*i)) ⊕ (⨁i ← [0..<n]. f (2*i+1))"
proof -
let ?es = "filter even [0..< 2 * n]"
let ?os = "filter odd [0..< 2 * n]"
have 1: "(⨁i ← [0..< 2 * n]. f i) = (⨁i ∈ {0..< 2 * n}. f i)"
using monoid_sum_list_finsum[of "[0..< 2 * n]" f] by simp
let ?E = "{i ∈ {0..<2*n}. even i}"
let ?O = "{i ∈ {0..<2*n}. odd i}"
have "?E ∩ ?O = {}" by blast
moreover have "?E ∪ ?O = {0..<2*n}" by blast
ultimately have "(⨁i ∈ {0..<2*n}. f i) = (⨁i ∈ ?E. f i) ⊕ (⨁i ∈ ?O. f i)"
using finsum_Un_disjoint[of ?E ?O f] assms by auto
moreover have "?E = set ?es" "?O = set ?os" by simp_all
ultimately have "(⨁i ∈ {0..<2*n}. f i) = (⨁i ∈ set ?es. f i) ⊕ (⨁i ∈ set ?os. f i)"
by presburger
also have "(⨁i ∈ set ?es. f i) = (⨁i ← ?es. f i)"
using monoid_sum_list_finsum[of ?es f] by simp
also have "... = (⨁i ← [0..<n]. f (2*i))"
using monoid_sum_list_index_transformation[of f "λi. 2 * i" "[0..<n]"]
using filter_even_upt_even
by algebra
also have "(⨁i ∈ set ?os. f i) = (⨁i ← ?os. f i)"
using monoid_sum_list_finsum[of ?os f] by simp
also have "... = (⨁i ← [0..<n]. f (2*i + 1))"
using monoid_sum_list_index_transformation[of f "λi. 2 * i + 1" "[0..<n]"]
using filter_odd_upt_even
by algebra
finally show ?thesis using 1 by presburger
qed
lemma monoid_sum_list_even_odd_split:
assumes "even (n::nat)"
assumes "⋀i. i < n ⟹ f i ∈ carrier G"
shows "(⨁i ← [0..<n]. f i) = (⨁i ← [0..< n div 2]. f (2*i)) ⊕ (⨁i ← [0..< n div 2]. f (2*i+1))"
using assms monoid_sum_list_splice by auto
end
context abelian_group
begin
lemma monoid_sum_list_minus_in:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
shows "⊖ (⨁i ← xs. f i) = (⨁i ← xs. ⊖ f i)"
using assms by (induction xs) (simp_all add: minus_add)
lemma monoid_sum_list_diff_in:
assumes[simp]: "⋀i. i ∈ set xs ⟹ f i ∈ carrier G"
assumes[simp]: "⋀i. i ∈ set xs ⟹ g i ∈ carrier G"
shows "(⨁i ← xs. f i) ⊖ (⨁i ← xs. g i) =
(⨁i ← xs. f i ⊖ g i)"
proof -
have "(⨁i ← xs. f i) ⊖ (⨁i ← xs. g i) = (⨁i ← xs. f i) ⊕ (⊖ (⨁i ← xs. g i))"
unfolding minus_eq by simp
also have "... = (⨁i ← xs. f i) ⊕ (⨁i ← xs. ⊖ g i)"
using monoid_sum_list_minus_in[of xs g] by simp
also have "... = (⨁i ← xs. f i ⊕ (⊖ g i))"
using monoid_sum_list_add_in[of xs f] by simp
finally show ?thesis unfolding minus_eq .
qed
end
context ring
begin
lemma monoid_sum_list_const:
assumes[simp]: "c ∈ carrier R"
shows "(⨁i ← xs. c) = (nat_embedding (length xs)) ⊗ c"
apply (induction xs)
using a_comm l_distr by auto
lemma monoid_sum_list_in_right:
assumes "y ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ y) = (⨁i ← xs. f i) ⊗ y"
using assms by (induction xs) (simp_all add: l_distr)
lemma monoid_sum_list_in_left:
assumes "y ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
shows "(⨁i ← xs. y ⊗ f i) = y ⊗ (⨁i ← xs. f i)"
using assms by (induction xs) (simp_all add: r_distr)
lemma monoid_sum_list_prod:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "⋀i. i ∈ set ys ⟹ g i ∈ carrier R"
shows "(⨁i ← xs. f i) ⊗ (⨁j ← ys. g j) = (⨁i ← xs. (⨁j ← ys. f i ⊗ g j))"
proof -
have "(⨁i ← xs. f i) ⊗ (⨁j ← ys. g j) = (⨁i ← xs. f i ⊗ (⨁j ← ys. g j))"
apply (intro monoid_sum_list_in_right[symmetric])
using assms by simp_all
also have "... = (⨁i ← xs. (⨁j ← ys. f i ⊗ g j))"
apply (intro monoid_sum_list_cong monoid_sum_list_in_left[symmetric])
using assms by simp_all
finally show ?thesis .
qed
subsection ‹Kronecker delta›
definition delta where
"delta i j = (if i = j then 𝟭 else 𝟬)"
lemma delta_closed[simp]: "delta i j ∈ carrier R"
unfolding delta_def by simp
lemma delta_sym: "delta i j = delta j i"
unfolding delta_def by simp
lemma delta_refl[simp]: "delta i i = 𝟭"
unfolding delta_def by simp
lemma monoid_sum_list_delta[simp]:
assumes[simp]: "⋀i. i < n ⟹ f i ∈ carrier R"
assumes[simp]: "j < n"
shows "(⨁i ← [0..<n]. delta i j ⊗ f i) = f j"
proof -
from assms have 0: "[0..<n] = [0..<j] @ j # [Suc j..<n]"
by (metis le_add1 le_add_same_cancel1 less_imp_add_positive upt_add_eq_append upt_conv_Cons)
then have "[0..<n] = [0..<j] @ [j] @ [Suc j..<n]"
by simp
moreover have 1: "⋀i. i ∈ set [0..<j] ⟹ delta i j ⊗ f i ∈ carrier R"
using 0 assms delta_closed m_closed atLeastLessThan_iff
by (metis le_add1 less_imp_add_positive linorder_le_less_linear set_upt upt_conv_Nil)
moreover have 2: "⋀i. i ∈ set ([j] @ [Suc j..<n]) ⟹ delta i j ⊗ f i ∈ carrier R"
using 0 assms delta_closed m_closed
by auto
ultimately have "(⨁i ← [0..<n]. delta i j ⊗ f i) = (⨁i ← [0..<j]. delta i j ⊗ f i) ⊕ (⨁i ← [j] @ [Suc j..<n]. delta i j ⊗ f i)"
using monoid_sum_list_app[of "[0..<j]" "λi. delta i j ⊗ f i" "[j] @ [Suc j..<n]"]
by presburger
also have "(⨁i ← [j] @ [Suc j..<n]. delta i j ⊗ f i) = (⨁i ← [j]. delta i j ⊗ f i) ⊕ (⨁i ← [Suc j..<n]. delta i j ⊗ f i)"
using 2 monoid_sum_list_app[of "[j]" "λi. delta i j ⊗ f i" "[Suc j..<n]"]
by simp
also have "(⨁i ← [0..<j]. delta i j ⊗ f i) = 𝟬"
using monoid_sum_list_0[of "[0..<j]"] monoid_sum_list_cong[of "[0..<j]" "λi. 𝟬" "λi. delta i j ⊗ f i"]
unfolding delta_def using ‹j < n› by simp
also have "(⨁i ← [Suc j..<n]. delta i j ⊗ f i) = 𝟬"
using monoid_sum_list_0[of "[Suc j..<n]"] monoid_sum_list_cong[of "[Suc j..<n]" "λi. 𝟬" "λi. delta i j ⊗ f i"]
unfolding delta_def by simp
also have "(⨁i ← [j]. delta i j ⊗ f i) = f j" by simp
finally show ?thesis by simp
qed
lemma mononid_sum_list_only_delta[simp]:
"j < n ⟹ (⨁i ← [0..<n]. delta i j) = 𝟭"
using monoid_sum_list_delta[of n "λi. 𝟭" j] by simp
subsection ‹Power sums›
lemma geo_monoid_list_sum:
assumes[simp]: "x ∈ carrier R"
shows "(𝟭 ⊖ x) ⊗ (⨁l ← [0..<r]. x [^] l) = (𝟭 ⊖ x [^] r)"
using assms
proof (induction r)
case 0
then show ?case using assms by (simp, algebra)
next
case (Suc r)
have "(𝟭 ⊖ x) ⊗ (⨁l ← [(0::nat)..< Suc r]. x [^] l) = (𝟭 ⊖ x) ⊗ (x [^] r ⊕ (⨁l ← [0..<r]. x [^] l))"
using monoid_sum_list_Suc[of r "λl. x [^] l"] a_comm
by simp
also have "... = (𝟭 ⊖ x) ⊗ x [^] r ⊕ (𝟭 ⊖ x) ⊗ (⨁l ← [0..<r]. x [^] l)"
using r_distr by auto
also have "... = x [^] r ⊖ x [^] (Suc r) ⊕ (𝟭 ⊖ x) ⊗ (⨁l ← [0..<r]. x [^] l)"
apply (intro arg_cong2[where f = "(⊕)"] refl)
unfolding minus_eq
l_distr[OF one_closed a_inv_closed[OF ‹x ∈ carrier R›] nat_pow_closed[OF ‹x ∈ carrier R›]]
using ‹x ∈ carrier R›
using l_minus nat_pow_Suc2 by force
also have "... = x [^] r ⊖ x [^] (Suc r) ⊕ (𝟭 ⊖ x [^] r)"
using Suc by presburger
also have "... = 𝟭 ⊖ x [^] (Suc r)"
using one_closed minus_add assms nat_pow_closed[of x] by algebra
finally show ?case .
qed
text "rewrite @{thm nat_pow_pow} and @{thm mult.commute} inside power sum"
lemma monoid_pow_sum_nat_pow_pow:
assumes "x ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ x [^] ((g i :: nat) * h i)) = (⨁i ← xs. f i ⊗ (x [^] h i) [^] g i)"
apply (intro_cong "[cong_tag_2 (⊗)]" more: monoid_sum_list_cong refl)
using nat_pow_pow[OF assms] by (simp add: mult.commute)
end
context cring
begin
text "Split a power sum at some term"
lemma monoid_pow_sum_list_split:
assumes "l + k = n"
assumes "⋀i. i < n ⟹ f i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← [0..<n]. f i ⊗ x [^] i) =
(⨁i ← [0..<l]. f i ⊗ x [^] i) ⊕
x [^] l ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ x [^] i)"
proof -
have "(⨁i ← [0..<n]. f i ⊗ x [^] i) =
(⨁i ← [0..<l]. f i ⊗ x [^] i) ⊕
(⨁i ← [l..<n]. f i ⊗ x [^] i)"
apply (intro monoid_sum_list_app' m_closed nat_pow_closed upt_add_eq_append'[symmetric])
using assms by simp_all
also have "(⨁i ← [l..<n]. f i ⊗ x [^] i) =
(⨁i ← [0..<k]. f (l + i) ⊗ x [^] (l + i))"
using monoid_sum_list_index_shift_0[of _ l "n-l"] ‹l + k = n›
by fastforce
also have "... = (⨁i ← [0..<k]. x [^] l ⊗ (f (l + i) ⊗ x [^] i))"
apply (intro monoid_sum_list_cong)
using assms m_comm m_assoc nat_pow_mult[symmetric, OF ‹x ∈ carrier R›] by simp
also have "... = x [^] l ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ x [^] i)"
apply (intro monoid_sum_list_in_left m_closed nat_pow_closed)
using assms by simp_all
finally show ?thesis .
qed
text "split power sum at term, more general"
lemma monoid_pow_sum_split:
assumes "l + k = n"
assumes "⋀i. i < n ⟹ f i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← [0..<n]. f i ⊗ x [^] (i * c)) =
(⨁i ← [0..<l]. f i ⊗ x [^] (i * c)) ⊕
x [^] (l * c) ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ x [^] (i * c))"
proof -
have "(⨁i ← [0..<n]. f i ⊗ x [^] (i * c)) = (⨁i ← [0..<n]. f i ⊗ (x [^] c) [^] i)"
by (intro monoid_pow_sum_nat_pow_pow ‹x ∈ carrier R›)
also have "... = (⨁i ← [0..<l]. f i ⊗ (x [^] c) [^] i) ⊕
(x [^] c) [^] l ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ (x [^] c) [^] i)"
by (intro monoid_pow_sum_list_split assms nat_pow_closed) argo
also have "... = (⨁i ← [0..<l]. f i ⊗ x [^] (i * c)) ⊕
x [^] (c * l) ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ x [^] (i * c))"
by (intro_cong "[cong_tag_2 (⊕), cong_tag_2 (⊗)]" more: monoid_pow_sum_nat_pow_pow[symmetric] nat_pow_pow ‹x ∈ carrier R›)
also have "... = (⨁i ← [0..<l]. f i ⊗ x [^] (i * c)) ⊕
x [^] (l * c) ⊗ (⨁i ← [0..<k]. f (l + i) ⊗ x [^] (i * c))"
by (intro_cong "[cong_tag_2 (⊕), cong_tag_2 (⊗), cong_tag_2 ([^])]" more: refl mult.commute)
finally show ?thesis .
qed
subsubsection "Algebraic operations"
text "addition"
lemma monoid_pow_sum_add:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ g i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ x [^] (i::nat)) ⊕ (⨁i ← xs. g i ⊗ x [^] i) = (⨁i ← xs. (f i ⊕ g i) ⊗ x [^] i)"
proof -
have "(⨁i ← xs. f i ⊗ x [^] i) ⊕ (⨁i ← xs. g i ⊗ x [^] i) =
(⨁i ← xs. (f i ⊗ x [^] i) ⊕ (g i ⊗ x [^] i))"
apply (intro monoid_sum_list_add_in m_closed nat_pow_closed assms) by assumption+
also have "... = (⨁i ← xs. (f i ⊕ g i) ⊗ x [^] i)"
apply (intro monoid_sum_list_cong l_distr[symmetric] nat_pow_closed assms) by assumption+
finally show ?thesis .
qed
lemma monoid_pow_sum_add':
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ g i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ x [^] ((i::nat) * c)) ⊕ (⨁i ← xs. g i ⊗ x [^] (i * c)) = (⨁i ← xs. (f i ⊕ g i) ⊗ x [^] (i * c))"
proof -
have "(⨁i ← xs. f i ⊗ x [^] ((i::nat) * c)) ⊕ (⨁i ← xs. g i ⊗ x [^] (i * c)) =
(⨁i ← xs. (f i ⊗ (x [^] c) [^] i)) ⊕ (⨁i ← xs. (g i ⊗ (x [^] c) [^] i))"
by (intro_cong "[cong_tag_2 (⊕)]" more: monoid_pow_sum_nat_pow_pow ‹x ∈ carrier R›)
also have "... = (⨁i ← xs. (f i ⊕ g i) ⊗ (x [^] c) [^] i)"
apply (intro monoid_pow_sum_add nat_pow_closed) using assms by simp_all
also have "... = (⨁i ← xs. (f i ⊕ g i) ⊗ x [^] (i * c))"
by (intro monoid_pow_sum_nat_pow_pow[symmetric] ‹x ∈ carrier R›)
finally show ?thesis .
qed
text "unary minus"
lemma monoid_pow_sum_minus:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "x ∈ carrier R"
shows "⊖ (⨁i ← xs. f i ⊗ x [^] (i :: nat)) = (⨁i ← xs. (⊖ f i) ⊗ x [^] i)"
proof -
have "⊖ (⨁i ← xs. f i ⊗ x [^] (i :: nat)) = (⨁i ← xs. ⊖ (f i ⊗ x [^] (i :: nat)))"
apply (intro monoid_sum_list_minus_in m_closed nat_pow_closed assms) by assumption
also have "... = (⨁i ← xs. (⊖ f i) ⊗ x [^] i)"
apply (intro monoid_sum_list_cong l_minus[symmetric] nat_pow_closed assms) by assumption
finally show ?thesis .
qed
text "minus"
lemma monoid_pow_sum_diff:
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ g i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ x [^] (i::nat)) ⊖ (⨁i ← xs. g i ⊗ x [^] (i :: nat)) =
(⨁i ← xs. (f i ⊖ g i) ⊗ x [^] i)"
using assms
by (simp add: minus_eq monoid_pow_sum_add[symmetric] monoid_pow_sum_minus)
lemma monoid_pow_sum_diff':
assumes "⋀i. i ∈ set xs ⟹ f i ∈ carrier R"
assumes "⋀i. i ∈ set xs ⟹ g i ∈ carrier R"
assumes "x ∈ carrier R"
shows "(⨁i ← xs. f i ⊗ x [^] ((i::nat) * c)) ⊖ (⨁i ← xs. g i ⊗ x [^] (i * c)) =
(⨁i ← xs. (f i ⊖ g i) ⊗ x [^] (i * c))"
proof -
have "(⨁i ← xs. f i ⊗ x [^] ((i::nat) * c)) ⊖ (⨁i ← xs. g i ⊗ x [^] (i * c)) =
(⨁i ← xs. f i ⊗ (x [^] c) [^] i) ⊖ (⨁i ← xs. g i ⊗ (x [^] c) [^] i)"
by (intro_cong "[cong_tag_2 (λi j. i ⊖ j)]" more: monoid_pow_sum_nat_pow_pow ‹x ∈ carrier R›)
also have "... = (⨁i ← xs. (f i ⊖ g i) ⊗ (x [^] c) [^] i)"
apply (intro monoid_pow_sum_diff nat_pow_closed) using assms by simp_all
also have "... = (⨁i ← xs. (f i ⊖ g i) ⊗ x [^] (i * c))"
by (intro monoid_pow_sum_nat_pow_pow[symmetric] ‹x ∈ carrier R›)
finally show ?thesis .
qed
end
subsection "@{term monoid_sum_list} in the context @{locale residues}"
context residues
begin
lemma monoid_sum_list_eq_sum_list:
"(⨁⇘R⇙ i ← xs. f i) = (∑i ← xs. f i) mod m"
apply (induction xs)
subgoal by (simp add: zero_cong)
subgoal for a xs by (simp add: mod_add_right_eq res_add_eq)
done
lemma monoid_sum_list_mod_in:
"(⨁⇘R⇙ i ← xs. f i) = (⨁⇘R⇙ i ← xs. (f i) mod m)"
by (induction xs) (simp_all add: mod_add_left_eq res_add_eq)
lemma monoid_sum_list_eq_sum_list':
"(⨁⇘R⇙ i ← xs. f i mod m) = (∑i ← xs. f i) mod m"
using monoid_sum_list_eq_sum_list monoid_sum_list_mod_in by metis
end
end