Theory 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."

(* adapted from finsum syntax definition *)
syntax
  "_monoid_sum_list" :: "index ⇒ idt ⇒ 'c list ⇒ 'c ⇒ 'a"
      (‹(3⨁__←_. _)› [1000, 0, 51, 10] 10)
syntax_consts
  "_monoid_sum_list" ⇌ abelian_monoid.monoid_sum_list
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 monoid_sum_list_extract:
  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