Theory Finite_Composite

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 Finite_Composite
  imports  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


subsection ‹Transfer between two commutative monoids›

text ‹@{const commutative_monoid.fincomp} depends on the ∗‹carrier› as well as on the operation,
  through @{const commutative_monoid.M_ify}, so two structures whose operations agree do not
  automatically have the same finite composites, and
  @{thm [source] commutative_monoid.fincomp_cong'} --- which stays within one monoid --- does not
  apply.  What is true is the following: if the smaller carrier is contained in the larger, the
  operations agree there, the unit is shared, and the function composed takes its values in the
  smaller carrier, then the composites agree.  This is what allows a sum computed inside a
  substructure to be read in the ambient structure, and in particular what makes evaluation of a
  polynomial independent of which of two nested structures it is performed in.›
text ‹The other direction of the same gap: a finite composite may be pushed ∗‹along a
  homomorphism›.  HOL-Algebra gets the corresponding fact for polynomial evaluation free from
  ‹ring_hom_ring.eval_hom'›; the carrier-set layer has no homomorphism apparatus at this level, so it
  is proved here directly, by the same finite induction as the transfer lemma below.›
lemma fincomp_hom:
  assumes M: "commutative_monoid M f e" and N: "commutative_monoid N g d"
    and hM: "⋀x. x ∈ M ⟹ h x ∈ N"
    and he: "h e = d"
    and hf: "⋀x y. ⟦ x ∈ M; y ∈ M ⟧ ⟹ h (f x y) = g (h x) (h y)"
    and k: "k ∈ A → M"
  shows "h (commutative_monoid.fincomp M f e k A)
       = commutative_monoid.fincomp N g d (λi. h (k i)) A"
proof (cases "finite A")
  case False
  then show ?thesis
    using he by (simp add: commutative_monoid.fincomp_infinite [OF M]
                           commutative_monoid.fincomp_infinite [OF N])
next
  case True
  then show ?thesis using k
  proof (induction A rule: finite_induct)
    case empty
    then show ?case
      using he by (simp add: commutative_monoid.fincomp_empty [OF M]
                             commutative_monoid.fincomp_empty [OF N])
  next
    case (insert a A)
    have kA: "k ∈ A → M" and ka: "k a ∈ M" using insert.prems by auto
    have hkA: "(λi. h (k i)) ∈ A → N" using kA hM by auto
    have hka: "h (k a) ∈ N" using ka by (rule hM)
    have clM: "commutative_monoid.fincomp M f e k A ∈ M"
      by (rule commutative_monoid.fincomp_closed [OF M kA])
    have "h (commutative_monoid.fincomp M f e k (insert a A))
          = h (f (k a) (commutative_monoid.fincomp M f e k A))"
      by (simp add: commutative_monoid.fincomp_insert
                      [OF M insert.hyps(1) insert.hyps(2) kA ka])
    also have "… = g (h (k a)) (h (commutative_monoid.fincomp M f e k A))"
      by (rule hf [OF ka clM])
    also have "… = g (h (k a)) (commutative_monoid.fincomp N g d (λi. h (k i)) A)"
      using insert.IH [OF kA] by simp
    also have "… = commutative_monoid.fincomp N g d (λi. h (k i)) (insert a A)"
      by (rule commutative_monoid.fincomp_insert
                 [OF N insert.hyps(1) insert.hyps(2) hkA hka, symmetric])
    finally show ?case .
  qed
qed

lemma fincomp_transfer:
  assumes M: "commutative_monoid M f e" and N: "commutative_monoid N g e"
    and sub: "M ⊆ N"
    and agree: "⋀x y. ⟦ x ∈ M; y ∈ M ⟧ ⟹ f x y = g x y"
    and h: "h ∈ A → M"
  shows "commutative_monoid.fincomp M f e h A = commutative_monoid.fincomp N g e h A"
proof (cases "finite A")
  case False
  then show ?thesis
    by (simp add: commutative_monoid.fincomp_infinite [OF M]
                  commutative_monoid.fincomp_infinite [OF N])
next
  case True
  then show ?thesis using h
  proof (induction A rule: finite_induct)
    case empty
    then show ?case
      by (simp add: commutative_monoid.fincomp_empty [OF M]
                    commutative_monoid.fincomp_empty [OF N])
  next
    case (insert a A)
    have hA: "h ∈ A → M" and ha: "h a ∈ M" using insert.prems by auto
    then have hAN: "h ∈ A → N" and haN: "h a ∈ N" using sub by auto
    have clM: "commutative_monoid.fincomp M f e h A ∈ M"
      by (rule commutative_monoid.fincomp_closed [OF M hA])
    have "commutative_monoid.fincomp M f e h (insert a A)
          = f (h a) (commutative_monoid.fincomp M f e h A)"
      by (rule commutative_monoid.fincomp_insert [OF M insert.hyps(1) insert.hyps(2) hA ha])
    also have "… = g (h a) (commutative_monoid.fincomp M f e h A)"
      using agree [OF ha clM] by simp
    also have "… = g (h a) (commutative_monoid.fincomp N g e h A)"
      using insert.IH [OF hA] by simp
    also have "… = commutative_monoid.fincomp N g e h (insert a A)"
      by (rule commutative_monoid.fincomp_insert
                 [OF N insert.hyps(1) insert.hyps(2) hAN haN, symmetric])
    finally show ?case .
  qed
qed

end