Theory Semigroups_Big

(* Title:      Big Sum over Finite Sets in Abelian Semigroups
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

(*  Title:      HOL/Groups_Big.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
*)

section ‹Big Sum over Finite Sets in Abelian Semigroups›

theory Semigroups_Big
  imports Main
begin

text ‹
This theory is based on Isabelle/HOL's ‹Groups_Big.thy› written by T. Nipkow, L. C. Paulson, M. Wenzel and J. Avigad.
We have generalised a selection of its results from Abelian monoids to Abelian semigroups with an element that is a unit on the image of the semigroup operation.
›

subsection ‹Generic Abelian semigroup operation over a set›

locale abel_semigroup_set = abel_semigroup +
  fixes z :: 'a (‹❙1›)
  assumes z_neutral [simp]: "x ❙* y ❙* ❙1 = x ❙* y"
  assumes z_idem [simp]: "❙1 ❙* ❙1 = ❙1"
begin

interpretation comp_fun_commute f
  by standard (simp add: fun_eq_iff left_commute)

interpretation comp?: comp_fun_commute "f ∘ g"
  by (fact comp_comp_fun_commute)

definition F :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'a"
  where eq_fold: "F g A = Finite_Set.fold (f ∘ g) ❙1 A"

lemma infinite [simp]: "¬ finite A ⟹ F g A = ❙1"
  by (simp add: eq_fold)

lemma empty [simp]: "F g {} = ❙1"
  by (simp add: eq_fold)

lemma insert [simp]: "finite A ⟹ x ∉ A ⟹ F g (insert x A) = g x ❙* F g A"
  by (simp add: eq_fold)

lemma remove:
  assumes "finite A" and "x ∈ A"
  shows "F g A = g x ❙* F g (A - {x})"
proof -
  from ‹x ∈ A› obtain B where B: "A = insert x B" and "x ∉ B"
    by (auto dest: mk_disjoint_insert)
  moreover from ‹finite A› B have "finite B" by simp
  ultimately show ?thesis by simp
qed

lemma insert_remove: "finite A ⟹ F g (insert x A) = g x ❙* F g (A - {x})"
  by (cases "x ∈ A") (simp_all add: remove insert_absorb)

lemma insert_if: "finite A ⟹ F g (insert x A) = (if x ∈ A then F g A else g x ❙* F g A)"
  by (cases "x ∈ A") (simp_all add: insert_absorb)

lemma neutral: "∀x∈A. g x = ❙1 ⟹ F g A = ❙1"
  by (induct A rule: infinite_finite_induct) simp_all

lemma neutral_const [simp]: "F (λ_. ❙1) A = ❙1"
  by (simp add: neutral)

lemma F_one [simp]: "F g A ❙* ❙1 = F g A"
proof -
  have "⋀f b B. F f (insert (b::'b) B) ❙* ❙1 = F f (insert b B) ∨ infinite B"
    using insert_remove by fastforce
  then show ?thesis
    by (metis (no_types) all_not_in_conv empty z_idem infinite insert_if)
qed

lemma one_F [simp]: "❙1 ❙* F g A = F g A"
  using F_one commute by auto

lemma F_g_one [simp]: "F (λx . g x ❙* ❙1) A = F g A"
  apply (induct A rule: infinite_finite_induct)
  apply simp
  apply simp
  by (metis one_F assoc insert)

lemma union_inter:
  assumes "finite A" and "finite B"
  shows "F g (A ∪ B) ❙* F g (A ∩ B) = F g A ❙* F g B"
  ― ‹The reversed orientation looks more natural, but LOOPS as a simprule!›
  using assms
proof (induct A)
  case empty
  then show ?case by simp
next
  case (insert x A)
  then show ?case
    by (auto simp: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
qed

corollary union_inter_neutral:
  assumes "finite A" and "finite B"
    and "∀x ∈ A ∩ B. g x = ❙1"
  shows "F g (A ∪ B) = F g A ❙* F g B"
  using assms by (simp add: union_inter [symmetric] neutral)

corollary union_disjoint:
  assumes "finite A" and "finite B"
  assumes "A ∩ B = {}"
  shows "F g (A ∪ B) = F g A ❙* F g B"
  using assms by (simp add: union_inter_neutral)

lemma union_diff2:
  assumes "finite A" and "finite B"
  shows "F g (A ∪ B) = F g (A - B) ❙* F g (B - A) ❙* F g (A ∩ B)"
proof -
  have "A ∪ B = A - B ∪ (B - A) ∪ A ∩ B"
    by auto
  with assms show ?thesis
    by simp (subst union_disjoint, auto)+
qed

lemma subset_diff:
  assumes "B ⊆ A" and "finite A"
  shows "F g A = F g (A - B) ❙* F g B"
proof -
  from assms have "finite (A - B)" by auto
  moreover from assms have "finite B" by (rule finite_subset)
  moreover from assms have "(A - B) ∩ B = {}" by auto
  ultimately have "F g (A - B ∪ B) = F g (A - B) ❙* F g B" by (rule union_disjoint)
  moreover from assms have "A ∪ B = A" by auto
  ultimately show ?thesis by simp
qed

lemma setdiff_irrelevant:
  assumes "finite A"
  shows "F g (A - {x. g x = z}) = F g A"
  using assms by (induct A) (simp_all add: insert_Diff_if)

lemma not_neutral_contains_not_neutral:
  assumes "F g A ≠ ❙1"
  obtains a where "a ∈ A" and "g a ≠ ❙1"
proof -
  from assms have "∃a∈A. g a ≠ ❙1"
  proof (induct A rule: infinite_finite_induct)
    case infinite
    then show ?case by simp
  next
    case empty
    then show ?case by simp
  next
    case (insert a A)
    then show ?case by fastforce
  qed
  with that show thesis by blast
qed

lemma reindex:
  assumes "inj_on h A"
  shows "F g (h ` A) = F (g ∘ h) A"
proof (cases "finite A")
  case True
  with assms show ?thesis
    by (simp add: eq_fold fold_image comp_assoc)
next
  case False
  with assms have "¬ finite (h ` A)" by (blast dest: finite_imageD)
  with False show ?thesis by simp
qed

lemma cong [fundef_cong]:
  assumes "A = B"
  assumes g_h: "⋀x. x ∈ B ⟹ g x = h x"
  shows "F g A = F h B"
  using g_h unfolding ‹A = B›
  by (induct B rule: infinite_finite_induct) auto

lemma strong_cong [cong]:
  assumes "A = B" "⋀x. x ∈ B =simp=> g x = h x"
  shows "F (λx. g x) A = F (λx. h x) B"
  by (rule cong) (use assms in ‹simp_all add: simp_implies_def›)

lemma reindex_cong:
  assumes "inj_on l B"
  assumes "A = l ` B"
  assumes "⋀x. x ∈ B ⟹ g (l x) = h x"
  shows "F g A = F h B"
  using assms by (simp add: reindex)

lemma UNION_disjoint:
  assumes "finite I" and "∀i∈I. finite (A i)"
    and "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}"
  shows "F g (⋃(A ` I)) = F (λx. F g (A x)) I"
  apply (insert assms)
  apply (induct rule: finite_induct)
   apply simp
  apply atomize
  apply (subgoal_tac "∀i∈Fa. x ≠ i")
   prefer 2 apply blast
  apply (subgoal_tac "A x ∩ ⋃(A ` Fa) = {}")
   prefer 2 apply blast
  apply (simp add: union_disjoint)
  done

lemma Union_disjoint:
  assumes "∀A∈C. finite A" "∀A∈C. ∀B∈C. A ≠ B ⟶ A ∩ B = {}"
  shows "F g (⋃C) = (F ∘ F) g C"
proof (cases "finite C")
  case True
  from UNION_disjoint [OF this assms] show ?thesis by simp
next
  case False
  then show ?thesis by (auto dest: finite_UnionD intro: infinite)
qed

lemma distrib: "F (λx. g x ❙* h x) A = F g A ❙* F h A"
  by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)

lemma Sigma:
  "finite A ⟹ ∀x∈A. finite (B x) ⟹ F (λx. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
  apply (subst Sigma_def)
  apply (subst UNION_disjoint)
     apply assumption
    apply simp
   apply blast
  apply (rule cong)
   apply rule
  apply (simp add: fun_eq_iff)
  apply (subst UNION_disjoint)
     apply simp
    apply simp
   apply blast
  apply (simp add: comp_def)
  done

lemma related:
  assumes Re: "R ❙1 ❙1"
    and Rop: "∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 ⟶ R (x1 ❙* y1) (x2 ❙* y2)"
    and fin: "finite S"
    and R_h_g: "∀x∈S. R (h x) (g x)"
  shows "R (F h S) (F g S)"
  using fin by (rule finite_subset_induct) (use assms in auto)

lemma mono_neutral_cong_left:
  assumes "finite T"
    and "S ⊆ T"
    and "∀i ∈ T - S. h i = ❙1"
    and "⋀x. x ∈ S ⟹ g x = h x"
  shows "F g S = F h T"
proof-
  have eq: "T = S ∪ (T - S)" using ‹S ⊆ T› by blast
  have d: "S ∩ (T - S) = {}" using ‹S ⊆ T› by blast
  from ‹finite T› ‹S ⊆ T› have f: "finite S" "finite (T - S)"
    by (auto intro: finite_subset)
  show ?thesis using assms(4)
    by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
qed

lemma mono_neutral_cong_right:
  "finite T ⟹ S ⊆ T ⟹ ∀i ∈ T - S. g i = ❙1 ⟹ (⋀x. x ∈ S ⟹ g x = h x) ⟹
    F g T = F h S"
  by (auto intro!: mono_neutral_cong_left [symmetric])

lemma mono_neutral_left: "finite T ⟹ S ⊆ T ⟹ ∀i ∈ T - S. g i = ❙1 ⟹ F g S = F g T"
  by (blast intro: mono_neutral_cong_left)

lemma mono_neutral_right: "finite T ⟹ S ⊆ T ⟹ ∀i ∈ T - S. g i = ❙1 ⟹ F g T = F g S"
  by (blast intro!: mono_neutral_left [symmetric])

lemma mono_neutral_cong:
  assumes [simp]: "finite T" "finite S"
    and *: "⋀i. i ∈ T - S ⟹ h i = ❙1" "⋀i. i ∈ S - T ⟹ g i = ❙1"
    and gh: "⋀x. x ∈ S ∩ T ⟹ g x = h x"
 shows "F g S = F h T"
proof-
  have "F g S = F g (S ∩ T)"
    by(rule mono_neutral_right)(auto intro: *)
  also have "… = F h (S ∩ T)" using refl gh by(rule cong)
  also have "… = F h T"
    by(rule mono_neutral_left)(auto intro: *)
  finally show ?thesis .
qed

lemma reindex_bij_betw: "bij_betw h S T ⟹ F (λx. g (h x)) S = F g T"
  by (auto simp: bij_betw_def reindex)

lemma reindex_bij_witness:
  assumes witness:
    "⋀a. a ∈ S ⟹ i (j a) = a"
    "⋀a. a ∈ S ⟹ j a ∈ T"
    "⋀b. b ∈ T ⟹ j (i b) = b"
    "⋀b. b ∈ T ⟹ i b ∈ S"
  assumes eq:
    "⋀a. a ∈ S ⟹ h (j a) = g a"
  shows "F g S = F h T"
proof -
  have "bij_betw j S T"
    using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
  moreover have "F g S = F (λx. h (j x)) S"
    by (intro cong) (auto simp: eq)
  ultimately show ?thesis
    by (simp add: reindex_bij_betw)
qed

lemma reindex_bij_betw_not_neutral:
  assumes fin: "finite S'" "finite T'"
  assumes bij: "bij_betw h (S - S') (T - T')"
  assumes nn:
    "⋀a. a ∈ S' ⟹ g (h a) = z"
    "⋀b. b ∈ T' ⟹ g b = z"
  shows "F (λx. g (h x)) S = F g T"
proof -
  have [simp]: "finite S ⟷ finite T"
    using bij_betw_finite[OF bij] fin by auto
  show ?thesis
  proof (cases "finite S")
    case True
    with nn have "F (λx. g (h x)) S = F (λx. g (h x)) (S - S')"
      by (intro mono_neutral_cong_right) auto
    also have "… = F g (T - T')"
      using bij by (rule reindex_bij_betw)
    also have "… = F g T"
      using nn ‹finite S› by (intro mono_neutral_cong_left) auto
    finally show ?thesis .
  next
    case False
    then show ?thesis by simp
  qed
qed

lemma reindex_nontrivial:
  assumes "finite A"
    and nz: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟹ h x = h y ⟹ g (h x) = ❙1"
  shows "F g (h ` A) = F (g ∘ h) A"
proof (subst reindex_bij_betw_not_neutral [symmetric])
  show "bij_betw h (A - {x ∈ A. (g ∘ h) x = ❙1}) (h ` A - h ` {x ∈ A. (g ∘ h) x = ❙1})"
    using nz by (auto intro!: inj_onI simp: bij_betw_def)
qed (use ‹finite A› in auto)

lemma reindex_bij_witness_not_neutral:
  assumes fin: "finite S'" "finite T'"
  assumes witness:
    "⋀a. a ∈ S - S' ⟹ i (j a) = a"
    "⋀a. a ∈ S - S' ⟹ j a ∈ T - T'"
    "⋀b. b ∈ T - T' ⟹ j (i b) = b"
    "⋀b. b ∈ T - T' ⟹ i b ∈ S - S'"
  assumes nn:
    "⋀a. a ∈ S' ⟹ g a = z"
    "⋀b. b ∈ T' ⟹ h b = z"
  assumes eq:
    "⋀a. a ∈ S ⟹ h (j a) = g a"
  shows "F g S = F h T"
proof -
  have bij: "bij_betw j (S - (S' ∩ S)) (T - (T' ∩ T))"
    using witness by (intro bij_betw_byWitness[where f'=i]) auto
  have F_eq: "F g S = F (λx. h (j x)) S"
    by (intro cong) (auto simp: eq)
  show ?thesis
    unfolding F_eq using fin nn eq
    by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
qed

lemma delta_remove:
  assumes fS: "finite S"
  shows "F (λk. if k = a then b k else c k) S = (if a ∈ S then b a ❙* F c (S-{a}) else F c (S-{a}))"
proof -
  let ?f = "(λk. if k = a then b k else c k)"
  show ?thesis
  proof (cases "a ∈ S")
    case False
    then have "∀k∈S. ?f k = c k" by simp
    with False show ?thesis by simp
  next
    case True
    let ?A = "S - {a}"
    let ?B = "{a}"
    from True have eq: "S = ?A ∪ ?B" by blast
    have dj: "?A ∩ ?B = {}" by simp
    from fS have fAB: "finite ?A" "finite ?B" by auto
    have "F ?f S = F ?f ?A ❙* F ?f ?B"
      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
    with True show ?thesis
      using abel_semigroup_set.remove abel_semigroup_set_axioms fS by fastforce
  qed
qed

lemma delta [simp]:
  assumes fS: "finite S"
  shows "F (λk. if k = a then b k else ❙1) S = (if a ∈ S then b a ❙* ❙1 else ❙1)"
  by (simp add: delta_remove [OF assms])

lemma delta' [simp]:
  assumes fin: "finite S"
  shows "F (λk. if a = k then b k else ❙1) S = (if a ∈ S then b a ❙* ❙1 else ❙1)"
  using delta [OF fin, of a b, symmetric] by (auto intro: cong)

lemma If_cases:
  fixes P :: "'b ⇒ bool" and g h :: "'b ⇒ 'a"
  assumes fin: "finite A"
  shows "F (λx. if P x then h x else g x) A = F h (A ∩ {x. P x}) ❙* F g (A ∩ - {x. P x})"
proof -
  have a: "A = A ∩ {x. P x} ∪ A ∩ -{x. P x}" "(A ∩ {x. P x}) ∩ (A ∩ -{x. P x}) = {}"
    by blast+
  from fin have f: "finite (A ∩ {x. P x})" "finite (A ∩ -{x. P x})" by auto
  let ?g = "λx. if P x then h x else g x"
  from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis
    by (subst (1 2) cong) simp_all
qed

lemma cartesian_product: "F (λx. F (g x) B) A = F (case_prod g) (A × B)"
  apply (rule sym)
  apply (cases "finite A")
   apply (cases "finite B")
    apply (simp add: Sigma)
   apply (cases "A = {}")
    apply simp
   apply simp
   apply (auto intro: infinite dest: finite_cartesian_productD2)
  apply (cases "B = {}")
   apply (auto intro: infinite dest: finite_cartesian_productD1)
  done

lemma inter_restrict:
  assumes "finite A"
  shows "F g (A ∩ B) = F (λx. if x ∈ B then g x else ❙1) A"
proof -
  let ?g = "λx. if x ∈ A ∩ B then g x else ❙1"
  have "∀i∈A - A ∩ B. (if i ∈ A ∩ B then g i else ❙1) = ❙1" by simp
  moreover have "A ∩ B ⊆ A" by blast
  ultimately have "F ?g (A ∩ B) = F ?g A"
    using ‹finite A› by (intro mono_neutral_left) auto
  then show ?thesis by simp
qed

lemma inter_filter:
  "finite A ⟹ F g {x ∈ A. P x} = F (λx. if P x then g x else ❙1) A"
  by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)

lemma Union_comp:
  assumes "∀A ∈ B. finite A"
    and "⋀A1 A2 x. A1 ∈ B ⟹ A2 ∈ B ⟹ A1 ≠ A2 ⟹ x ∈ A1 ⟹ x ∈ A2 ⟹ g x = ❙1"
  shows "F g (⋃B) = (F ∘ F) g B"
  using assms
proof (induct B rule: infinite_finite_induct)
  case (infinite A)
  then have "¬ finite (⋃A)" by (blast dest: finite_UnionD)
  with infinite show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert A B)
  then have "finite A" "finite B" "finite (⋃B)" "A ∉ B"
    and "∀x∈A ∩ ⋃B. g x = ❙1"
    and H: "F g (⋃B) = (F ∘ F) g B" by auto
  then have "F g (A ∪ ⋃B) = F g A ❙* F g (⋃B)"
    by (simp add: union_inter_neutral)
  with ‹finite B› ‹A ∉ B› show ?case
    by (simp add: H)
qed

lemma swap: "F (λi. F (g i) B) A = F (λj. F (λi. g i j) A) B"
  unfolding cartesian_product
  by (rule reindex_bij_witness [where i = "λ(i, j). (j, i)" and j = "λ(i, j). (j, i)"]) auto

lemma swap_restrict:
  "finite A ⟹ finite B ⟹
    F (λx. F (g x) {y. y ∈ B ∧ R x y}) A = F (λy. F (λx. g x y) {x. x ∈ A ∧ R x y}) B"
  by (simp add: inter_filter) (rule swap)

lemma Plus:
  fixes A :: "'b set" and B :: "'c set"
  assumes fin: "finite A" "finite B"
  shows "F g (A <+> B) = F (g ∘ Inl) A ❙* F (g ∘ Inr) B"
proof -
  have "A <+> B = Inl ` A ∪ Inr ` B" by auto
  moreover from fin have "finite (Inl ` A)" "finite (Inr ` B)" by auto
  moreover have "Inl ` A ∩ Inr ` B = {}" by auto
  moreover have "inj_on Inl A" "inj_on Inr B" by (auto intro: inj_onI)
  ultimately show ?thesis
    using fin by (simp add: union_disjoint reindex)
qed

lemma same_carrier:
  assumes "finite C"
  assumes subset: "A ⊆ C" "B ⊆ C"
  assumes trivial: "⋀a. a ∈ C - A ⟹ g a = ❙1" "⋀b. b ∈ C - B ⟹ h b = ❙1"
  shows "F g A = F h B ⟷ F g C = F h C"
proof -
  have "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
    using ‹finite C› subset by (auto elim: finite_subset)
  from subset have [simp]: "A - (C - A) = A" by auto
  from subset have [simp]: "B - (C - B) = B" by auto
  from subset have "C = A ∪ (C - A)" by auto
  then have "F g C = F g (A ∪ (C - A))" by simp
  also have "… = F g (A - (C - A)) ❙* F g (C - A - A) ❙* F g (A ∩ (C - A))"
    using ‹finite A› ‹finite (C - A)› by (simp only: union_diff2)
  finally have *: "F g C = F g A" using trivial by simp
  from subset have "C = B ∪ (C - B)" by auto
  then have "F h C = F h (B ∪ (C - B))" by simp
  also have "… = F h (B - (C - B)) ❙* F h (C - B - B) ❙* F h (B ∩ (C - B))"
    using ‹finite B› ‹finite (C - B)› by (simp only: union_diff2)
  finally have "F h C = F h B"
    using trivial by simp
  with * show ?thesis by simp
qed

lemma same_carrierI:
  assumes "finite C"
  assumes subset: "A ⊆ C" "B ⊆ C"
  assumes trivial: "⋀a. a ∈ C - A ⟹ g a = ❙1" "⋀b. b ∈ C - B ⟹ h b = ❙1"
  assumes "F g C = F h C"
  shows "F g A = F h B"
  using assms same_carrier [of C A B] by simp

end


subsection ‹Generalized summation over a set›
text ‹Instead of @{term"∑x∈{x. P}. e"} we introduce the shorter ‹∑x|P. e›.›
no_notation Sum (‹∑›)

class ab_semigroup_add_0 = zero + ab_semigroup_add +
  assumes zero_neutral [simp]: "x + y + 0 = x + y"
  assumes zero_idem [simp]: "0 + 0 = 0"
begin

sublocale sum_0: abel_semigroup_set plus 0
  defines sum_0 = sum_0.F
  by unfold_locales simp_all

abbreviation Sum_0 (‹∑›)
  where "∑ ≡ sum_0 (λx. x)"

end

context comm_monoid_add
begin

subclass ab_semigroup_add_0
  by unfold_locales simp_all

end

text ‹Now: lots of fancy syntax. First, @{term "sum_0 (λx. e) A"} is written ‹∑x∈A. e›.›

no_syntax (ASCII)
  "_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  (‹(‹indent=3 notation=‹binder SUM››SUM (_/:_)./ _)› [0, 51, 10] 10)
no_syntax
  "_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  (‹(‹indent=2 notation=‹binder ∑››∑(_/∈_)./ _)› [0, 51, 10] 10)

syntax (ASCII)
  "_sum0" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  (‹(‹indent=3 notation=‹binder SUM››SUM (_/:_)./ _)› [0, 51, 10] 10)
syntax
  "_sum0" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  (‹(‹indent=2 notation=‹binder ∑››∑(_/∈_)./ _)› [0, 51, 10] 10)
syntax_consts
  "_sum0" ⇌ sum_0
translations ― ‹Beware of argument permutation!›
  "∑i∈A. b" ⇌ "CONST sum_0 (λi. b) A"

text ‹Instead of @{term"∑x∈{x. P}. e"} we introduce the shorter ‹∑x|P. e›.›

no_syntax (ASCII)
  "_qsum" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a"  (‹(‹indent=3 notation=‹binder SUM Collect››SUM _ |/ _./ _)› [0, 0, 10] 10)
no_syntax
  "_qsum" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a"  (‹(‹indent=2 notation=‹binder ∑ Collect››∑_ | (_)./ _)› [0, 0, 10] 10)

syntax (ASCII)
  "_qsum0" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a"  (‹(‹indent=3 notation=‹binder SUM Collect››SUM _ |/ _./ _)› [0, 0, 10] 10)
syntax
  "_qsum0" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a"  (‹(‹indent=2 notation=‹binder ∑ Collect››∑_ | (_)./ _)› [0, 0, 10] 10)
syntax_consts
  "_qsum0" ⇌ sum_0
translations
  "∑x|P. t" => "CONST sum_0 (λx. t) {x. P}"
print_translation ‹
  [(\<^const_syntax>‹sum_0›, K (Collect_binder_tr' \<^syntax_const>‹_qsum›))]
›

lemma (in ab_semigroup_add_0) sum_image_gen_0:
  assumes fin: "finite S"
  shows "sum_0 g S = sum_0 (λy. sum_0 g {x. x ∈ S ∧ f x = y}) (f ` S)"
proof -
  have "{y. y∈ f`S ∧ f x = y} = {f x}" if "x ∈ S" for x
    using that by auto
  then have "sum_0 g S = sum_0 (λx. sum_0 (λy. g x) {y. y∈ f`S ∧ f x = y}) S"
    by simp
  also have "… = sum_0 (λy. sum_0 g {x. x ∈ S ∧ f x = y}) (f ` S)"
    by (rule sum_0.swap_restrict [OF fin finite_imageI [OF fin]])
  finally show ?thesis .
qed


subsubsection ‹Properties in more restricted classes of structures›

lemma sum_Un2:
  assumes "finite (A ∪ B)"
  shows "sum_0 f (A ∪ B) = sum_0 f (A - B) + sum_0 f (B - A) + sum_0 f (A ∩ B)"
proof -
  have "A ∪ B = A - B ∪ (B - A) ∪ A ∩ B"
    by auto
  with assms show ?thesis
    by simp (subst sum_0.union_disjoint, auto)+
qed

class ordered_ab_semigroup_add_0 = ab_semigroup_add_0 + ordered_ab_semigroup_add
begin

lemma add_nonneg_nonneg [simp]: "0 ≤ a ⟹ 0 ≤ b ⟹ 0 ≤ a + b"
  using add_mono[of 0 a 0 b] by simp

lemma add_nonpos_nonpos: "a ≤ 0 ⟹ b ≤ 0 ⟹ a + b ≤ 0"
  using add_mono[of a 0 b 0] by simp

end

lemma (in ordered_ab_semigroup_add_0) sum_mono:
  "(⋀i. i∈K ⟹ f i ≤ g i) ⟹ (∑i∈K. f i) ≤ (∑i∈K. g i)"
  by (induct K rule: infinite_finite_induct) (use add_mono in auto)

lemma (in ordered_ab_semigroup_add_0) sum_mono_00:
  "(⋀i. i∈K ⟹ f i + 0 ≤ g i + 0) ⟹ (∑i∈K. f i) ≤ (∑i∈K. g i)"
proof (induct K rule: infinite_finite_induct)
  case (infinite A)
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
  proof -
    fix x :: 'b and F :: "'b set"
    assume a1: "finite F"
    assume a2: "x ∉ F"
    assume a3: "(⋀i. i ∈ F ⟹ f i + 0 ≤ g i + 0) ⟹ sum_0 f F ≤ sum_0 g F"
    assume a4: "⋀i. i ∈ insert x F ⟹ f i + 0 ≤ g i + 0"
    obtain bb :: 'b where
      f5: "bb ∈ F ∧ ¬ f bb + 0 ≤ g bb + 0 ∨ sum_0 f F ≤ sum_0 g F"
      using a3 by blast
    have "∀b. x ≠ b ∨ f b + 0 ≤ g b + 0"
      using a4 by simp
    then have "∀a aa. f x + 0 + a ≤ g x + 0 + aa ∨ ¬ a ≤ aa"
      using add_mono by blast
    then show "sum_0 f (insert x F) ≤ sum_0 g (insert x F)"
      using f5 a4 a2 a1 by (metis (no_types) add_assoc insert_iff sum_0.insert sum_0.one_F)
  qed
qed

lemma (in ordered_ab_semigroup_add_0) sum_mono_0:
  "(⋀i. i∈K ⟹ f i + 0 ≤ g i) ⟹ (∑i∈K. f i) ≤ (∑i∈K. g i)"
  apply (rule sum_mono_00)
  by (metis add_right_mono zero_neutral)

context ordered_ab_semigroup_add_0
begin

lemma sum_nonneg: "(⋀x. x ∈ A ⟹ 0 ≤ f x) ⟹ 0 ≤ sum_0 f A"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then have "0 + 0 ≤ f x + sum_0 f F" by (blast intro: add_mono)
  with insert show ?case by simp
qed

lemma sum_nonpos: "(⋀x. x ∈ A ⟹ f x ≤ 0) ⟹ sum_0 f A ≤ 0"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then have "f x + sum_0 f F ≤ 0 + 0" by (blast intro: add_mono)
  with insert show ?case by simp
qed

lemma sum_mono2:
  assumes fin: "finite B"
    and sub: "A ⊆ B"
    and nn: "⋀b. b ∈ B-A ⟹ 0 ≤ f b"
  shows "sum_0 f A ≤ sum_0 f B"
proof -
  have "sum_0 f A ≤ sum_0 f A + sum_0 f (B-A)"
    by (metis add_left_mono sum_0.F_one nn sum_nonneg)
  also from fin finite_subset[OF sub fin] have "… = sum_0 f (A ∪ (B-A))"
    by (simp add: sum_0.union_disjoint del: Un_Diff_cancel)
  also from sub have "A ∪ (B-A) = B" by blast
  finally show ?thesis .
qed

lemma sum_le_included:
  assumes "finite s" "finite t"
  and "∀y∈t. 0 ≤ g y" "(∀x∈s. ∃y∈t. i y = x ∧ f x ≤ g y)"
  shows "sum_0 f s ≤ sum_0 g t"
proof -
  have "sum_0 f s ≤ sum_0 (λy. sum_0 g {x. x∈t ∧ i x = y}) s"
  proof (rule sum_mono_0)
    fix y
    assume "y ∈ s"
    with assms obtain z where z: "z ∈ t" "y = i z" "f y ≤ g z" by auto
    hence "f y + 0 ≤ sum_0 g {z}"
      by (metis Diff_eq_empty_iff add_commute finite.simps add_left_mono sum_0.empty sum_0.insert_remove subset_insertI)
    also have "... ≤ sum_0 g {x ∈ t. i x = y}"
      apply (rule sum_mono2)
      using assms z by simp_all
    finally show "f y + 0 ≤ sum_0 g {x ∈ t. i x = y}" .
  qed
  also have "… ≤ sum_0 (λy. sum_0 g {x. x∈t ∧ i x = y}) (i ` t)"
    using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg)
  also have "… ≤ sum_0 g t"
    using assms by (auto simp: sum_image_gen_0[symmetric])
  finally show ?thesis .
qed

end

lemma sum_comp_morphism:
  "h 0 = 0 ⟹ (⋀x y. h (x + y) = h x + h y) ⟹ sum_0 (h ∘ g) A = h (sum_0 g A)"
  by (induct A rule: infinite_finite_induct) simp_all

lemma sum_cong_Suc:
  assumes "0 ∉ A" "⋀x. Suc x ∈ A ⟹ f (Suc x) = g (Suc x)"
  shows "sum_0 f A = sum_0 g A"
proof (rule sum_0.cong)
  fix x
  assume "x ∈ A"
  with assms(1) show "f x = g x"
    by (cases x) (auto intro!: assms(2))
qed simp_all

end