# Theory FiniteProduct

```section ‹Product Operator for Commutative Monoids›

(*
Finite products in group theory. This theory is largely based on HOL/Algebra/FiniteProduct.thy.
--L C Paulson
*)

theory FiniteProduct
imports
"Jacobson_Basic_Algebra.Group_Theory"

begin

subsection ‹Products over Finite Sets›

context commutative_monoid begin

definition "M_ify x ≡ if x ∈ M then x else 𝟭"

definition "fincomp f A ≡ if finite A then Finite_Set.fold (λx y. f x ⋅ M_ify y) 𝟭 A else 𝟭"

lemma fincomp_empty [simp]: "fincomp f {} = 𝟭"

lemma fincomp_infinite[simp]: "infinite A ⟹ fincomp f A = 𝟭"

lemma left_commute: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ b ⋅ (a ⋅ c) = a ⋅ (b ⋅ c)"
using commutative by force

lemma comp_fun_commute_onI:
assumes "f ∈ F → M"
shows "comp_fun_commute_on F (λx y. f x ⋅ M_ify y)"
using assms
by (auto simp add: comp_fun_commute_on_def Pi_iff M_ify_def left_commute)

lemma fincomp_closed [simp]:
assumes "f ∈ F → M"
shows "fincomp f F ∈ M"
proof -
interpret comp_fun_commute_on F "λx y. f x ⋅ M_ify y"
show ?thesis
unfolding fincomp_def
by (smt (verit, ccfv_threshold) M_ify_def Pi_iff fold_graph_fold assms composition_closed equalityE fold_graph_closed_lemma unit_closed)
qed

lemma fincomp_insert [simp]:
assumes F: "finite F" "a ∉ F" and f: "f ∈ F → M" "f a ∈ M"
shows "fincomp f (insert a F) = f a ⋅ fincomp f F"
proof -
interpret comp_fun_commute_on "insert a F" "λx y. f x ⋅ M_ify y"
show ?thesis
using assms fincomp_closed commutative_monoid.M_ify_def commutative_monoid_axioms
qed

lemma fincomp_unit_eqI: "(⋀x. x ∈ A ⟹ f x = 𝟭) ⟹ fincomp f A = 𝟭"
proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
have "(λi. 𝟭) ∈ A → M" by auto
with insert show ?case by simp
qed simp

lemma fincomp_unit [simp]: "fincomp (λi. 𝟭) A = 𝟭"

lemma funcset_Int_left [simp, intro]:
"⟦f ∈ A → C; f ∈ B → C⟧ ⟹ f ∈ A Int B → C"
by fast

lemma funcset_Un_left [iff]:
"(f ∈ A Un B → C) = (f ∈ A → C ∧ f ∈ B → C)"
by fast

lemma fincomp_Un_Int:
"⟦finite A; finite B; g ∈ A → M; g ∈ B → M⟧ ⟹
fincomp g (A ∪ B) ⋅ fincomp g (A ∩ B) =
fincomp g A ⋅ fincomp g B"
― ‹The reversed orientation looks more natural, but LOOPS as a simprule!›
proof (induct set: finite)
case empty then show ?case by simp
next
case (insert a A)
then have "g a ∈ M" "g ∈ A → M" by blast+
with insert show ?case
by (simp add: Int_insert_left associative insert_absorb left_commute)
qed

lemma fincomp_Un_disjoint:
"⟦finite A; finite B; A ∩ B = {}; g ∈ A → M; g ∈ B → M⟧
⟹ fincomp g (A ∪ B) = fincomp g A ⋅ fincomp g B"
by (metis Pi_split_domain fincomp_Un_Int fincomp_closed fincomp_empty right_unit)

lemma fincomp_comp:
"⟦f ∈ A → M; g ∈ A → M⟧ ⟹ fincomp (λx. f x ⋅ g x) A = (fincomp f A ⋅ fincomp g A)"
proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
then have "f a ∈ M" "g ∈ A → M" "g a ∈ M" "f ∈ A → M" "(λx. f x ⋅ g x) ∈ A → M"
by blast+
then show ?case
by (simp add: insert associative left_commute)
qed simp

lemma fincomp_cong':
assumes "A = B" "g ∈ B → M" "⋀i. i ∈ B ⟹ f i = g i"
shows "fincomp f A = fincomp g B"
proof (cases "finite B")
case True
then have ?thesis
using assms
proof (induct arbitrary: A)
case empty thus ?case by simp
next
case (insert x B)
then have "fincomp f A = fincomp f (insert x B)" by simp
also from insert have "... = f x ⋅ fincomp f B"
also from insert have "... = g x ⋅ fincomp g B" by fastforce
also from insert have "... = fincomp g (insert x B)"
by (intro fincomp_insert [THEN sym]) auto
finally show ?case .
qed
with assms show ?thesis by simp
next
case False with assms show ?thesis by simp
qed

lemma fincomp_cong:
assumes "A = B" "g ∈ B → M" "⋀i. i ∈ B =simp=> f i = g i"
shows "fincomp f A = fincomp g B"
using assms unfolding simp_implies_def by (blast intro: fincomp_cong')

text ‹Usually, if this rule causes a failed congruence proof error,
the reason is that the premise ‹g ∈ B → M› cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.
For this reason, @{thm [source] fincomp_cong}
is not added to the simpset by default.
›

lemma fincomp_0 [simp]:
"f ∈ {0::nat} → M ⟹ fincomp f {..0} = f 0"

lemma fincomp_0': "f ∈ {..n} → M ⟹ (f 0) ⋅ fincomp f {Suc 0..n} = fincomp f {..n}"
by (metis Pi_split_insert_domain Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL atMost_atLeast0 finite_atLeastAtMost fincomp_insert le0)

lemma fincomp_Suc [simp]:
"f ∈ {..Suc n} → M ⟹ fincomp f {..Suc n} = (f (Suc n) ⋅ fincomp f {..n})"

lemma fincomp_Suc2:
"f ∈ {..Suc n} → M ⟹ fincomp f {..Suc n} = (fincomp (%i. f (Suc i)) {..n} ⋅ f 0)"
proof (induct n)
case 0 thus ?case by (simp add: Pi_def)
next
case Suc thus ?case
qed

lemma fincomp_Suc3:
assumes "f ∈ {..n :: nat} → M"
shows "fincomp f {.. n} = (f n) ⋅ fincomp f {..< n}"
proof (cases "n = 0")
case True thus ?thesis
using assms atMost_Suc by simp
next
case False
then obtain k where "n = Suc k"
using not0_implies_Suc by blast
thus ?thesis
using fincomp_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
qed

"f ∈ (h ` A) → M ⟹
inj_on h A ⟹ fincomp f (h ` A) = fincomp (λx. f (h x)) A"
proof (induct A rule: infinite_finite_induct)
case (infinite A)
hence "¬ finite (h ` A)"
using finite_imageD by blast
with ‹¬ finite A› show ?case by simp

assumes a [simp]: "a ∈ M"
shows "fincomp (λx. a) A = rec_nat 𝟭 (λu. (⋅) a) (card A)"
by (induct A rule: infinite_finite_induct) auto

lemma fincomp_singleton: ✐‹contributor ‹Jesus Aransay››
assumes i_in_A: "i ∈ A" and fin_A: "finite A" and f_Pi: "f ∈ A → M"
shows "fincomp (λj. if i = j then f j else 𝟭) A = f i"
using i_in_A fincomp_insert [of "A - {i}" i "(λj. if i = j then f j else 𝟭)"]
fin_A f_Pi fincomp_unit [of "A - {i}"]
fincomp_cong [of "A - {i}" "A - {i}" "(λj. if i = j then f j else 𝟭)" "(λi. 𝟭)"]
unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)

lemma fincomp_singleton_swap:
assumes i_in_A: "i ∈ A" and fin_A: "finite A" and f_Pi: "f ∈ A → M"
shows "fincomp (λj. if j = i then f j else 𝟭) A = f i"
using fincomp_singleton [OF assms] by (simp add: eq_commute)

lemma fincomp_mono_neutral_cong_left:
assumes "finite B"
and "A ⊆ B"
and 1: "⋀i. i ∈ B - A ⟹ h i = 𝟭"
and gh: "⋀x. x ∈ A ⟹ g x = h x"
and h: "h ∈ B → M"
shows "fincomp g A = fincomp h B"
proof-
have eq: "A ∪ (B - A) = B" using ‹A ⊆ B› by blast
have d: "A ∩ (B - A) = {}" using ‹A ⊆ B› by blast
from ‹finite B› ‹A ⊆ B› have f: "finite A" "finite (B - A)"
by (auto intro: finite_subset)
have "h ∈ A → M" "h ∈ B - A → M"
using assms by (auto simp: image_subset_iff_funcset)
moreover have "fincomp g A = fincomp h A ⋅ fincomp h (B - A)"
proof -
have "fincomp h (B - A) = 𝟭"
using "1" fincomp_unit_eqI by blast
moreover have "fincomp g A = fincomp h A"
using ‹h ∈ A → M› fincomp_cong' gh by blast
ultimately show ?thesis
by (simp add: ‹h ∈ A → M›)
qed
ultimately show ?thesis
by (simp add: fincomp_Un_disjoint [OF f d, unfolded eq])
qed

lemma fincomp_mono_neutral_cong_right:
assumes "finite B"
and "A ⊆ B" "⋀i. i ∈ B - A ⟹ g i = 𝟭" "⋀x. x ∈ A ⟹ g x = h x" "g ∈ B → M"
shows "fincomp g B = fincomp h A"
using assms  by (auto intro!: fincomp_mono_neutral_cong_left [symmetric])

lemma fincomp_mono_neutral_cong:
assumes [simp]: "finite B" "finite A"
and *: "⋀i. i ∈ B - A ⟹ h i = 𝟭" "⋀i. i ∈ A - B ⟹ g i = 𝟭"
and gh: "⋀x. x ∈ A ∩ B ⟹ g x = h x"
and g: "g ∈ A → M"
and h: "h ∈ B → M"
shows "fincomp g A = fincomp h B"
proof-
have "fincomp g A = fincomp g (A ∩ B)"
by (rule fincomp_mono_neutral_cong_right) (use assms in auto)
also have "… = fincomp h (A ∩ B)"
by (rule fincomp_cong) (use assms in auto)
also have "… = fincomp h B"
by (rule fincomp_mono_neutral_cong_left) (use assms in auto)
finally show ?thesis .
qed

lemma fincomp_UN_disjoint:
assumes
"finite I" "⋀i. i ∈ I ⟹ finite (A i)" "pairwise (λi j. disjnt (A i) (A j)) I"
"⋀i x. i ∈ I ⟹ x ∈ A i ⟹ g x ∈ M"
shows "fincomp g (⋃(A ` I)) = fincomp (λi. fincomp g (A i)) I"
using assms
proof (induction set: finite)
case empty
then show ?case
by force
next
case (insert i I)
then show ?case
unfolding pairwise_def disjnt_def
apply clarsimp
apply (subst fincomp_Un_disjoint)
apply (fastforce intro!: funcsetI fincomp_closed)+
done
qed

lemma fincomp_Union_disjoint:
"⟦finite C; ⋀A. A ∈ C ⟹ finite A ∧ (∀x∈A. f x ∈ M); pairwise disjnt C⟧ ⟹
fincomp f (⋃C) = fincomp (fincomp f) C"
by (frule fincomp_UN_disjoint [of C id f]) auto

end

subsection ‹Results for Abelian Groups›

context abelian_group begin

lemma fincomp_inverse:
"f ∈ A → G ⟹ fincomp (λx. inverse (f x)) A = inverse (fincomp f A)"
proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A)
then have "f a ∈ G" "f ∈ A → G" "(λx. inverse (f x)) ∈ A → G"
by blast+
with insert show ?case
qed simp

text ‹ Jeremy Avigad. This should be generalized to arbitrary groups, not just Abelian
ones, using Lagrange's theorem.›
lemma power_order_eq_one:
assumes fin [simp]: "finite G"
and a [simp]: "a ∈ G"
shows "rec_nat 𝟭 (λu. (⋅) a) (card G) = 𝟭"
proof -
have rec_G: "rec_nat 𝟭 (λu. (⋅) a) (card G) ∈ G"
by (metis Pi_I' a fincomp_closed fincomp_const)
have "⋀x. x ∈ G ⟹ x ∈ (⋅) a ` G"
by (metis a composition_closed imageI invertible invertible_inverse_closed invertible_right_inverse2)
with a have "(⋅) a ` G = G" by blast
then have "𝟭 ⋅ fincomp (λx. x) G = fincomp (λx. x) ((⋅) a ` G)"
by simp
also have "… = fincomp (λx. a ⋅ x) G"
using fincomp_reindex
by (subst (2) fincomp_reindex [symmetric]) (auto simp: inj_on_def)
also have "… = fincomp (λx. a) G ⋅ fincomp (λx. x) G"