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 {} = 𝟭"
  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