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

(* adapted from finsum syntax definition *)
syntax
  "_monoid_sum_list" :: "index  idt  'c list  'c  'a"
      ("(3___. _)" [1000, 0, 51, 10] 10)
translations
  "Gixs. 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:
"(Ri  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:
"(Ri  xs. f i) = (Ri  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':
"(Ri  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