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 {} = 𝟭" by (simp add: fincomp_def) lemma fincomp_infinite[simp]: "infinite A ⟹ fincomp f A = 𝟭" by (simp add: fincomp_def) 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" by (simp add: assms comp_fun_commute_onI) 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" by (simp add: comp_fun_commute_onI f) show ?thesis using assms fincomp_closed commutative_monoid.M_ify_def commutative_monoid_axioms by (fastforce simp add: fincomp_def) 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 = 𝟭" by (simp add: fincomp_unit_eqI) 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" by (simp add: Pi_iff) 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" by (simp add: Pi_def) 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})" by (simp add: Pi_def atMost_Suc) 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 by (simp add: associative Pi_def) 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 lemma fincomp_reindex: ✐‹contributor ‹Jeremy Avigad›› "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 qed (auto simp add: Pi_def) lemma fincomp_const: ✐‹contributor ‹Jeremy Avigad›› 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 by (simp add: commutative inverse_composition_commute) 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" by (simp add: fincomp_comp) also have "fincomp (λx. a) G = rec_nat 𝟭 (λu. (⋅) a) (card G)" by (simp add: fincomp_const) finally show ?thesis by (metis commutative fincomp_closed funcset_id invertible invertible_left_cancel rec_G unit_closed) qed end end