# Theory HOL-Library.Groups_Big_Fun

```(* Author: Florian Haftmann, TU Muenchen *)

section ‹Big sum and product over function bodies›

theory Groups_Big_Fun
imports
Main
begin

subsection ‹Abstract product›

locale comm_monoid_fun = comm_monoid
begin

definition G :: "('b ⇒ 'a) ⇒ 'a"
where
expand_set: "G g = comm_monoid_set.F f ❙1 g {a. g a ≠ ❙1}"

interpretation F: comm_monoid_set f "❙1"
..

lemma expand_superset:
assumes "finite A" and "{a. g a ≠ ❙1} ⊆ A"
shows "G g = F.F g A"
using F.mono_neutral_right assms expand_set by fastforce

lemma conditionalize:
assumes "finite A"
shows "F.F g A = G (λa. if a ∈ A then g a else ❙1)"
using assms
by (smt (verit, ccfv_threshold) Diff_iff F.mono_neutral_cong_right expand_set mem_Collect_eq subsetI)

lemma neutral [simp]:
"G (λa. ❙1) = ❙1"

lemma update [simp]:
assumes "finite {a. g a ≠ ❙1}"
assumes "g a = ❙1"
shows "G (g(a := b)) = b ❙* G g"
proof (cases "b = ❙1")
case True with ‹g a = ❙1› show ?thesis
by (simp add: expand_set) (rule F.cong, auto)
next
case False
moreover have "{a'. a' ≠ a ⟶ g a' ≠ ❙1} = insert a {a. g a ≠ ❙1}"
by auto
moreover from ‹g a = ❙1› have "a ∉ {a. g a ≠ ❙1}"
by simp
moreover have "F.F (λa'. if a' = a then b else g a') {a. g a ≠ ❙1} = F.F g {a. g a ≠ ❙1}"
by (rule F.cong) (auto simp add: ‹g a = ❙1›)
ultimately show ?thesis using ‹finite {a. g a ≠ ❙1}› by (simp add: expand_set)
qed

lemma infinite [simp]:
"¬ finite {a. g a ≠ ❙1} ⟹ G g = ❙1"

lemma cong [cong]:
assumes "⋀a. g a = h a"
shows "G g = G h"
using assms by (simp add: expand_set)

lemma not_neutral_obtains_not_neutral:
assumes "G g ≠ ❙1"
obtains a where "g a ≠ ❙1"
using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)

lemma reindex_cong:
assumes "bij l"
assumes "g ∘ l = h"
shows "G g = G h"
proof -
from assms have unfold: "h = g ∘ l" by simp
from ‹bij l› have "inj l" by (rule bij_is_inj)
then have "inj_on l {a. h a ≠ ❙1}" by (rule subset_inj_on) simp
moreover from ‹bij l› have "{a. g a ≠ ❙1} = l ` {a. h a ≠ ❙1}"
by (auto simp add: image_Collect unfold elim: bij_pointE)
moreover have "⋀x. x ∈ {a. h a ≠ ❙1} ⟹ g (l x) = h x"
ultimately have "F.F g {a. g a ≠ ❙1} = F.F h {a. h a ≠ ❙1}"
by (rule F.reindex_cong)
then show ?thesis by (simp add: expand_set)
qed

lemma distrib:
assumes "finite {a. g a ≠ ❙1}" and "finite {a. h a ≠ ❙1}"
shows "G (λa. g a ❙* h a) = G g ❙* G h"
proof -
from assms have "finite ({a. g a ≠ ❙1} ∪ {a. h a ≠ ❙1})" by simp
moreover have "{a. g a ❙* h a ≠ ❙1} ⊆ {a. g a ≠ ❙1} ∪ {a. h a ≠ ❙1}"
by auto (drule sym, simp)
ultimately show ?thesis
using assms
by (simp add: expand_superset [of "{a. g a ≠ ❙1} ∪ {a. h a ≠ ❙1}"] F.distrib)
qed

lemma swap:
assumes "finite C"
assumes subset: "{a. ∃b. g a b ≠ ❙1} × {b. ∃a. g a b ≠ ❙1} ⊆ C" (is "?A × ?B ⊆ C")
shows "G (λa. G (g a)) = G (λb. G (λa. g a b))"
proof -
from ‹finite C› subset
have "finite ({a. ∃b. g a b ≠ ❙1} × {b. ∃a. g a b ≠ ❙1})"
by (rule rev_finite_subset)
then have fins:
"finite {b. ∃a. g a b ≠ ❙1}" "finite {a. ∃b. g a b ≠ ❙1}"
have subsets: "⋀a. {b. g a b ≠ ❙1} ⊆ {b. ∃a. g a b ≠ ❙1}"
"⋀b. {a. g a b ≠ ❙1} ⊆ {a. ∃b. g a b ≠ ❙1}"
"{a. F.F (g a) {b. ∃a. g a b ≠ ❙1} ≠ ❙1} ⊆ {a. ∃b. g a b ≠ ❙1}"
"{a. F.F (λaa. g aa a) {a. ∃b. g a b ≠ ❙1} ≠ ❙1} ⊆ {b. ∃a. g a b ≠ ❙1}"
by (auto elim: F.not_neutral_contains_not_neutral)
from F.swap have
"F.F (λa. F.F (g a) {b. ∃a. g a b ≠ ❙1}) {a. ∃b. g a b ≠ ❙1} =
F.F (λb. F.F (λa. g a b) {a. ∃b. g a b ≠ ❙1}) {b. ∃a. g a b ≠ ❙1}" .
with subsets fins have "G (λa. F.F (g a) {b. ∃a. g a b ≠ ❙1}) =
G (λb. F.F (λa. g a b) {a. ∃b. g a b ≠ ❙1})"
by (auto simp add: expand_superset [of "{b. ∃a. g a b ≠ ❙1}"]
expand_superset [of "{a. ∃b. g a b ≠ ❙1}"])
with subsets fins show ?thesis
by (auto simp add: expand_superset [of "{b. ∃a. g a b ≠ ❙1}"]
expand_superset [of "{a. ∃b. g a b ≠ ❙1}"])
qed

lemma cartesian_product:
assumes "finite C"
assumes subset: "{a. ∃b. g a b ≠ ❙1} × {b. ∃a. g a b ≠ ❙1} ⊆ C" (is "?A × ?B ⊆ C")
shows "G (λa. G (g a)) = G (λ(a, b). g a b)"
proof -
from subset ‹finite C› have fin_prod: "finite (?A × ?B)"
by (rule finite_subset)
from fin_prod have "finite ?A" and "finite ?B"
have *: "G (λa. G (g a)) =
(F.F (λa. F.F (g a) {b. ∃a. g a b ≠ ❙1}) {a. ∃b. g a b ≠ ❙1})"
using ‹finite ?A› ‹finite ?B› expand_superset
by (smt (verit, del_insts) Collect_mono local.cong not_neutral_obtains_not_neutral)
have **: "{p. (case p of (a, b) ⇒ g a b) ≠ ❙1} ⊆ ?A × ?B"
by auto
show ?thesis
using ‹finite C› expand_superset
using "*" ** F.cartesian_product fin_prod by force
qed

lemma cartesian_product2:
assumes fin: "finite D"
assumes subset: "{(a, b). ∃c. g a b c ≠ ❙1} × {c. ∃a b. g a b c ≠ ❙1} ⊆ D" (is "?AB × ?C ⊆ D")
shows "G (λ(a, b). G (g a b)) = G (λ(a, b, c). g a b c)"
proof -
have bij: "bij (λ(a, b, c). ((a, b), c))"
by (auto intro!: bijI injI simp add: image_def)
have "{p. ∃c. g (fst p) (snd p) c ≠ ❙1} × {c. ∃p. g (fst p) (snd p) c ≠ ❙1} ⊆ D"
by auto (insert subset, blast)
with fin have "G (λp. G (g (fst p) (snd p))) = G (λ(p, c). g (fst p) (snd p) c)"
by (rule cartesian_product)
then have "G (λ(a, b). G (g a b)) = G (λ((a, b), c). g a b c)"
also have "G (λ((a, b), c). g a b c) = G (λ(a, b, c). g a b c)"
using bij by (rule reindex_cong [of "λ(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
finally show ?thesis .
qed

lemma delta [simp]:
"G (λb. if b = a then g b else ❙1) = g a"
proof -
have "{b. (if b = a then g b else ❙1) ≠ ❙1} ⊆ {a}" by auto
then show ?thesis by (simp add: expand_superset [of "{a}"])
qed

lemma delta' [simp]:
"G (λb. if a = b then g b else ❙1) = g a"
proof -
have "(λb. if a = b then g b else ❙1) = (λb. if b = a then g b else ❙1)"
then have "G (λb. if a = b then g b else ❙1) = G (λb. if b = a then g b else ❙1)"
by (simp cong del: cong)
then show ?thesis by simp
qed

end

subsection ‹Concrete sum›

begin

sublocale Sum_any: comm_monoid_fun plus 0
rewrites "comm_monoid_set.F plus 0 = sum"
defines Sum_any = Sum_any.G
proof -
show "comm_monoid_fun plus 0" ..
then interpret Sum_any: comm_monoid_fun plus 0 .
from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
qed

end

syntax (ASCII)
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_add"    ("(3∑_. _)" [0, 10] 10)
translations
"∑a. b" ⇌ "CONST Sum_any (λa. b)"

lemma Sum_any_left_distrib:
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a ≠ 0}"
shows "Sum_any g * r = (∑n. g n * r)"
by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_left sum_distrib_right)

lemma Sum_any_right_distrib:
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a ≠ 0}"
shows "r * Sum_any g = (∑n. r * g n)"
by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_right sum_distrib_left)

lemma Sum_any_product:
fixes f g :: "'b ⇒ 'a::semiring_0"
assumes "finite {a. f a ≠ 0}" and "finite {b. g b ≠ 0}"
shows "Sum_any f * Sum_any g = (∑a. ∑b. f a * g b)"
proof -
have "∀a. (∑b. a * g b) = a * Sum_any g"
then show ?thesis
qed

lemma Sum_any_eq_zero_iff [simp]:
fixes f :: "'a ⇒ nat"
assumes "finite {a. f a ≠ 0}"
shows "Sum_any f = 0 ⟷ f = (λ_. 0)"
using assms by (simp add: Sum_any.expand_set fun_eq_iff)

subsection ‹Concrete product›

context comm_monoid_mult
begin

sublocale Prod_any: comm_monoid_fun times 1
rewrites "comm_monoid_set.F times 1 = prod"
defines Prod_any = Prod_any.G
proof -
show "comm_monoid_fun times 1" ..
then interpret Prod_any: comm_monoid_fun times 1 .
from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
qed

end

syntax (ASCII)
"_Prod_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
syntax
"_Prod_any" :: "pttrn ⇒ 'a ⇒ 'a::comm_monoid_mult"  ("(3∏_. _)" [0, 10] 10)
translations
"∏a. b" == "CONST Prod_any (λa. b)"

lemma Prod_any_zero:
fixes f :: "'b ⇒ 'a :: comm_semiring_1"
assumes "finite {a. f a ≠ 1}"
assumes "f a = 0"
shows "(∏a. f a) = 0"
proof -
from ‹f a = 0› have "f a ≠ 1" by simp
with ‹f a = 0› have "∃a. f a ≠ 1 ∧ f a = 0" by blast
with ‹finite {a. f a ≠ 1}› show ?thesis
qed

lemma Prod_any_not_zero:
fixes f :: "'b ⇒ 'a :: comm_semiring_1"
assumes "finite {a. f a ≠ 1}"
assumes "(∏a. f a) ≠ 0"
shows "f a ≠ 0"
using assms Prod_any_zero [of f] by blast

lemma power_Sum_any:
assumes "finite {a. f a ≠ 0}"
shows "c ^ (∑a. f a) = (∏a. c ^ f a)"
proof -
have "{a. c ^ f a ≠ 1} ⊆ {a. f a ≠ 0}"
by (auto intro: ccontr)
with assms show ?thesis
by (simp add: Sum_any.expand_set Prod_any.expand_superset power_sum)
qed

end
```