# Theory Set_Multiplication

(*
File:     Set_Multiplication.thy
Author:   Joseph Thommes, TU München
*)
section ‹Set Multiplication›

theory Set_Multiplication
imports "HOL-Algebra.Algebra"
begin

text ‹This theory/section is of auxiliary nature and is mainly used to establish a connection
between the set multiplication and the multiplication of subgroups via the ‹IDirProd› (although this
particular notion is introduced later). However, as in every section of this entry, there are some
lemmas that do not have any further usage in this entry, but are of interest just by themselves.›

lemma (in group) set_mult_union:
"A <#> (B ∪ C) = (A <#> B) ∪ (A <#> C)"
unfolding set_mult_def by auto

lemma (in group) set_mult_card_single_el_eq:
assumes "J ⊆ carrier G" "x ∈ carrier G"
shows "card (l_coset G x J) = card J" unfolding l_coset_def
proof -
have "card ((⊗) x  J) = card J"
using inj_on_cmult[of x] card_image[of "(⊗) x" J] assms inj_on_subset[of "(⊗) x" "carrier G" J]
by blast
moreover have "(⋃y∈J. {x ⊗ y}) = (⊗) x  J" using image_def[of "(⊗) x" J] by blast
ultimately show "card (⋃h∈J. {x ⊗ h}) = card J" by presburger
qed

text ‹We find an upper bound for the cardinality of a set product.›

lemma (in group) set_mult_card_le:
assumes "finite H" "H ⊆ carrier G" "J ⊆ carrier G"
shows "card (H <#> J) ≤ card H * card J"
using assms
proof (induction "card H" arbitrary: H)
case 0
then have "H = {}" by force
then show ?case using set_mult_def[of G H J] by simp
next
case (Suc n)
then obtain a where a_def: "a ∈ H" by fastforce
then have c_n: "card (H - {a}) = n" using Suc by force
then have "card ((H - {a}) <#> J) ≤ card (H - {a}) * card J" using Suc by blast
moreover have "card ({a} <#> J) = card J"
using Suc(4, 5) a_def set_mult_card_single_el_eq[of J a] l_coset_eq_set_mult[of G a J] by auto
moreover have "H <#> J = (H - {a} <#> J) ∪ ({a} <#> J)" using set_mult_def[of G _ J] a_def by auto
moreover have "card (H - {a}) * card J + card J = Suc n * card J" using c_n mult_Suc by presburger
ultimately show ?case using card_Un_le[of "H - {a} <#> J" "{a} <#> J"] c_n ‹Suc n = card H› by auto
qed

lemma (in group) set_mult_finite:
assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G"
shows "finite (H <#> J)"
using assms set_mult_def[of G H J] by auto

text ‹The next lemma allows us to later to derive that two finite subgroups $J$ and $H$ are complementary
if and only if their product has the cardinality $|J| \cdot |H|$.›

lemma (in group) set_mult_card_eq_impl_empty_inter:
assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J"
shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a  J) ∩ ((⊗) b  J) = {}"
using assms
proof (induction H rule: finite_induct)
case empty
then show ?case by fast
next
case step: (insert x H)
from step have x_c: "x ∈ carrier G" by simp
from step have H_c: "H ⊆ carrier G" by simp
from set_mult_card_single_el_eq[of J x] have card_x: "card ({x} <#> J) = card J"
using ‹J ⊆ carrier G› x_c l_coset_eq_set_mult by metis
moreover have ins: "(insert x H) <#> J = (H <#> J) ∪ ({x} <#> J)"
using set_mult_def[of G _ J] by auto
ultimately have "card (H <#> J) ≥ card H * card J"
using card_Un_le[of "H <#> J" "{x} <#> J"] ‹card (insert x H <#> J) = card (insert x H) * card J›
then have card_eq:"card (H <#> J) = card H * card J"
using set_mult_card_le[of H J] step H_c by linarith
then have ih: "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ ((⊗) a  J) ∩ ((⊗) b  J) = {}"
using step H_c by presburger

have "card (insert x H) * card J = card H * card J + card J" using ‹x ∉ H› using step by simp
then have "({x} <#> J) ∩ (H <#> J) = {}"
using card_eq card_x ins card_Un_Int[of "H <#> J" "{x} <#> J"] step set_mult_finite by auto
then have "⋀a. a ∈ H ⟹ (⋃y∈J. {a ⊗ y}) ∩ (⋃y∈J. {x ⊗ y}) = {}"
using set_mult_def[of G _ J] by blast
then have "⋀a b. ⟦a ∈ (insert x H); b ∈ (insert x H); a ≠ b⟧ ⟹ ((⊗) a  J) ∩ ((⊗) b  J) = {}"
using ‹x ∉ H› ih by blast
then show ?case using step by algebra
qed

lemma (in group) set_mult_card_eq_impl_empty_inter':
assumes "finite H" "finite J" "H ⊆ carrier G" "J ⊆ carrier G" "card (H <#> J) = card H * card J"
shows "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ (l_coset G a J) ∩ (l_coset G b J) = {}"
unfolding l_coset_def
using set_mult_card_eq_impl_empty_inter image_def[of "(⊗) _" J] assms by blast

lemma (in comm_group) set_mult_comm:
assumes "H ⊆ carrier G" "J ⊆ carrier G"
shows "(H <#> J) = (J <#> H)"
unfolding set_mult_def
proof -
have 1: "⋀a b. ⟦a ∈ carrier G; b ∈ carrier G⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using m_comm by simp
then have "⋀a b.⟦a ∈ H; b ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms by auto
moreover have "⋀a b.⟦b ∈ H; a ∈ J⟧ ⟹ {a ⊗ b} = {b ⊗ a}" using assms 1 by auto
ultimately show "(⋃h∈H. ⋃k∈J. {h ⊗ k}) = (⋃k∈J. ⋃h∈H. {k ⊗ h})"  by fast
qed

lemma (in group) set_mult_one_imp_inc:
assumes "𝟭 ∈ A" "A ⊆ carrier G" "B ⊆ carrier G"
shows "B ⊆ (B <#> A)"
proof
fix x
assume "x ∈ B"
thus "x ∈ (B <#> A)" using assms unfolding set_mult_def by force
qed

text ‹In all cases, we know that the product of two sets is always contained in the subgroup
generated by them.›
lemma (in group) set_mult_subset_generate:
assumes "A ⊆ carrier G" "B ⊆ carrier G"
shows "A <#> B ⊆ generate G (A ∪ B)"
proof
fix x
assume "x ∈ A <#> B"
then obtain a b where ab: "a ∈ A" "b ∈ B" "x = a ⊗ b" unfolding set_mult_def by blast
then have "a ∈ generate G (A ∪ B)" "b ∈ generate G (A ∪ B)"
using generate.incl[of _ "A ∪ B" G] by simp+
thus "x ∈ generate G (A ∪ B)" using ab generate.eng by metis
qed

text ‹In the case of subgroups, the set product is just the subgroup generated by both
of the subgroups.›

lemma (in comm_group) set_mult_eq_generate_subgroup:
assumes "subgroup H G" "subgroup J G"
shows "generate G (H ∪ J) = H <#> J" (is "?L = ?R")
proof
show "?L ⊆ ?R"
proof
fix x
assume "x ∈ ?L"
then show "x ∈ ?R"
proof(induction rule: generate.induct)
case one
have "𝟭 ⊗ 𝟭 = 𝟭" using nat_pow_one[of 2] by simp
thus ?case
using assms subgroup.one_closed[OF assms(1)]
subgroup.one_closed[OF assms(2)] set_mult_def[of G H J] by fastforce
next
case (incl x)
have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto
have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto
have lx: "x ⊗ 𝟭 = x" using r_one[of x] incl subgroup.subset assms by blast
have rx: "𝟭 ⊗ x = x" using l_one[of x] incl subgroup.subset assms by blast
show ?case
proof (cases "x ∈ H")
case True
then show ?thesis using set_mult_def J1 lx by fastforce
next
case False
then show ?thesis using set_mult_def H1 rx incl by fastforce
qed
next
case (inv h)
then have inv_in:"(inv h) ∈ H ∪ J" (is "?iv ∈ H ∪ J")
using assms subgroup.m_inv_closed[of _ G h] by (cases "h ∈ H"; blast)
have H1: "𝟭 ∈ H" using assms subgroup.one_closed by auto
have J1: "𝟭 ∈ J" using assms subgroup.one_closed by auto
have lx: "?iv ⊗ 𝟭 = ?iv" using r_one[of "?iv"] subgroup.subset inv_in assms by blast
have rx: "𝟭 ⊗ ?iv = ?iv" using l_one[of "?iv"] incl subgroup.subset inv_in assms by blast
show ?case
proof (cases "?iv ∈ H")
case True
then show ?thesis using set_mult_def[of G H J] J1 lx by fastforce
next
case False
then show ?thesis using set_mult_def[of G H J] H1 rx inv_in by fastforce
qed
next
case (eng h g)
from eng(3) obtain a b where aH: "a ∈ H" and bJ: "b ∈ J" and h_def: "h = a ⊗ b"
using set_mult_def[of G H J] by fast
have a_carr: "a ∈ carrier G" by (metis subgroup.mem_carrier assms(1) aH)
have b_carr: "b ∈ carrier G" by (metis subgroup.mem_carrier assms(2) bJ)
from eng(4) obtain c d where cH: "c ∈ H" and dJ: "d ∈ J" and g_def: "g = c ⊗ d"
using set_mult_def[of G H J] by fast
have c_carr: "c ∈ carrier G" by (metis subgroup.mem_carrier assms(1) cH)
have d_carr: "d ∈ carrier G" by (metis subgroup.mem_carrier assms(2) dJ)
then have "h ⊗ g = (a ⊗ c) ⊗ (b ⊗ d)"
using a_carr b_carr c_carr d_carr g_def h_def m_assoc m_comm by force
moreover have "a ⊗ c ∈ H" using assms(1) aH cH subgroup.m_closed by fast
moreover have "b ⊗ d ∈ J" using assms(2) bJ dJ subgroup.m_closed by fast
ultimately show ?case using set_mult_def by fast
qed
qed
next
show "?R ⊆ ?L" using set_mult_subset_generate[of H J] subgroup.subset assms by blast
qed

end

# Theory Miscellaneous_Groups

(*
File:     Miscellaneous_Groups.thy
Author:   Joseph Thommes, TU München
*)
section ‹Miscellaneous group facts›

theory Miscellaneous_Groups
imports Set_Multiplication
begin

text ‹As the name suggests, this section contains several smaller lemmas about groups.›

(* Manuel Eberl *)
lemma (in subgroup) nat_pow_closed [simp,intro]: "a ∈ H ⟹ pow G a (n::nat) ∈ H"
by (induction n) (auto simp: nat_pow_def)

(* Manuel Eberl *)
lemma nat_pow_modify_carrier: "a [^]⇘G⦇carrier := H⦈⇙ b = a [^]⇘G⇙ (b::nat)"

lemma (in group) subgroup_card_dvd_group_ord:
assumes "subgroup H G"
shows "card H dvd order G"
using Coset.group.lagrange[of G H] assms group_axioms by (metis dvd_triv_right)

lemma (in group) subgroup_card_eq_order:
assumes "subgroup H G"
shows "card H = order (G⦇carrier := H⦈)"
unfolding order_def by simp

lemma (in group) finite_subgroup_card_neq_0:
assumes "subgroup H G" "finite H"
shows "card H ≠ 0"
using subgroup_nonempty assms by auto

lemma (in group) subgroup_order_dvd_group_order:
assumes "subgroup H G"
shows "order (G⦇carrier := H⦈) dvd order G"
by (metis subgroup_card_dvd_group_ord[of H] assms subgroup_card_eq_order)

lemma (in group) sub_subgroup_dvd_card:
assumes "subgroup H G" "subgroup J G" "J ⊆ H"
shows "card J dvd card H"
by (metis subgroup_incl[of J H] subgroup_card_eq_order[of H]
group.subgroup_card_dvd_group_ord[of "(G⦇carrier := H⦈)" J] assms
subgroup.subgroup_is_group[of H G] group_axioms)

lemma (in group) inter_subgroup_dvd_card:
assumes "subgroup H G" "subgroup J G"
shows "card (H ∩ J) dvd card H"
using subgroups_Inter_pair[of H J] assms sub_subgroup_dvd_card[of H "H ∩ J"] by blast

lemma (in group) subgroups_card_coprime_inter_card_one:
assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
shows "card (H ∩ J) = 1"
proof -
from assms inter_subgroup_dvd_card have "is_unit (card (H ∩ J))" unfolding coprime_def
by (meson Int_lower2 sub_subgroup_dvd_card subgroup_Int)
then show ?thesis by simp
qed

lemma (in group) coset_neq_imp_empty_inter:
assumes "subgroup H G" "a ∈ carrier G" "b ∈ carrier G"
shows "H #> a ≠ H #> b ⟹ (H #> a) ∩ (H #> b) = {}"
by (metis Int_emptyI assms repr_independence)

lemma (in comm_group) subgroup_is_comm_group:
assumes "subgroup H G"
shows "comm_group (G⦇carrier := H⦈)" unfolding comm_group_def
proof
interpret H: subgroup H G by fact
interpret H: submonoid H G using H.subgroup_is_submonoid .
show "Group.group (G⦇carrier := H⦈)" by blast
show "comm_monoid (G⦇carrier := H⦈)" using submonoid_is_comm_monoid H.submonoid_axioms by blast
qed

lemma (in group) pow_int_mod_ord:
assumes [simp]:"a ∈ carrier G" "ord a ≠ 0"
shows "a [^] (n::int) = a [^] (n mod ord a)"
proof -
obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
using mod_div_decomp by blast
hence "a [^] n = (a [^] int (ord a)) [^] q ⊗ a [^] r"
using assms(1) int_pow_mult int_pow_pow
by (metis mult_of_nat_commute)
also have "… = 𝟭 [^] q ⊗ a [^] r"
also have "… = a [^] r" by simp
finally show ?thesis using d(2) by blast
qed

lemma (in group) pow_nat_mod_ord:
assumes [simp]:"a ∈ carrier G" "ord a ≠ 0"
shows "a [^] (n::nat) = a [^] (n mod ord a)"
proof -
obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
using mod_div_decomp by blast
hence "a [^] n = (a [^] ord a) [^] q ⊗ a [^] r"
using assms(1) nat_pow_mult nat_pow_pow by presburger
also have "… = 𝟭 [^] q ⊗ a [^] r" by auto
also have "… = a [^] r" by simp
finally show ?thesis using d(2) by blast
qed

lemma (in group) ord_min:
assumes "m ≥ 1" "x ∈ carrier G" "x [^] m = 𝟭"
shows   "ord x ≤ m"
using assms pow_eq_id by auto

(* Manuel Eberl *)
lemma (in group) bij_betw_mult_left[intro]:
assumes [simp]: "x ∈ carrier G"
shows "bij_betw (λy. x ⊗ y) (carrier G) (carrier G)"
by (intro bij_betwI[where ?g = "λy. inv x ⊗ y"])
(auto simp: m_assoc [symmetric])

(* Manuel Eberl *)
lemma (in subgroup) inv_in_iff:
assumes "x ∈ carrier G" "group G"
shows   "inv x ∈ H ⟷ x ∈ H"
proof safe
assume "inv x ∈ H"
hence "inv (inv x) ∈ H" by blast
also have "inv (inv x) = x"
by (intro group.inv_inv) (use assms in auto)
finally show "x ∈ H" .
qed auto

(* Manuel Eberl *)
lemma (in subgroup) mult_in_cancel_left:
assumes "y ∈ carrier G" "x ∈ H" "group G"
shows   "x ⊗ y ∈ H ⟷ y ∈ H"
proof safe
assume "x ⊗ y ∈ H"
hence "inv x ⊗ (x ⊗ y) ∈ H"
using assms by blast
also have "inv x ⊗ (x ⊗ y) = y"
using assms by (simp add: ‹x ⊗ y ∈ H› group.inv_solve_left')
finally show "y ∈ H" .
qed (use assms in auto)

(* Manuel Eberl *)
lemma (in subgroup) mult_in_cancel_right:
assumes "x ∈ carrier G" "y ∈ H" "group G"
shows   "x ⊗ y ∈ H ⟷ x ∈ H"
proof safe
assume "x ⊗ y ∈ H"
hence "(x ⊗ y) ⊗ inv y ∈ H"
using assms by blast
also have "(x ⊗ y) ⊗ inv y = x"
using assms by (simp add: ‹x ⊗ y ∈ H› group.inv_solve_right')
finally show "x ∈ H" .
qed (use assms in auto)

lemma (in group) (* Manuel Eberl *)
assumes "x ∈ carrier G" and "x [^] n = 𝟭" and "n > 0"
shows   ord_le: "ord x ≤ n" and ord_pos: "ord x > 0"
proof -
have "ord x dvd n"
using pow_eq_id[of x n] assms by auto
thus "ord x ≤ n" "ord x > 0"
using assms by (auto intro: dvd_imp_le)
qed

lemma (in group) ord_conv_Least: (* Manuel Eberl *)
assumes "x ∈ carrier G" "∃n::nat > 0. x [^] n = 𝟭"
shows   "ord x = (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)"
proof (rule antisym)
show "ord x ≤ (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)"
using assms LeastI_ex[OF assms(2)] by (intro ord_le) auto
show "ord x ≥ (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)"
using assms by (intro Least_le) (auto intro: pow_ord_eq_1 ord_pos)
qed

lemma (in group) ord_conv_Gcd: (* Manuel Eberl *)
assumes "x ∈ carrier G"
shows   "ord x = Gcd {n. x [^] n = 𝟭}"
by (rule sym, rule Gcd_eqI) (use assms in ‹auto simp: pow_eq_id›)

lemma (in group) subgroup_ord_eq:
assumes "subgroup H G" "x ∈ H"
shows "group.ord (G⦇carrier := H⦈) x = ord x"
using nat_pow_consistent ord_def group.ord_def[of "(G⦇carrier := H⦈)" x]
subgroup.subgroup_is_group[of H G] assms by simp

lemma (in group) ord_FactGroup:
assumes "subgroup P G" "group (G Mod P)"
shows "order (G Mod P) * card P = order G"
using lagrange[of P] FactGroup_def[of G P] assms order_def[of "(G Mod P)"] by fastforce

lemma (in group) one_is_same:
assumes "subgroup H G"
shows "𝟭⇘G⦇carrier := H⦈⇙ = 𝟭"
by simp

lemma (in group) kernel_FactGroup:
assumes "P ⊲ G"
shows "kernel G (G Mod P) (λx. P #> x) = P"
proof(rule equalityI; rule subsetI)
fix x
assume "x ∈ kernel G (G Mod P) ((#>) P)"
then have "P #> x = 𝟭⇘G Mod P⇙" "x ∈ carrier G" unfolding kernel_def by simp+
with coset_join1[of P x] show "x ∈ P" using assms unfolding normal_def by simp
next
fix x
assume x:"x ∈ P"
then have xc: "x ∈ carrier G" using assms subgroup.subset unfolding normal_def by fast
from x have "P #> x = P" using assms
thus "x ∈ kernel G (G Mod P) ((#>) P)" unfolding kernel_def using xc by simp
qed

lemma (in group) sub_subgroup_coprime:
assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
and "subgroup sH G" "subgroup sJ G" "sH ⊆ H" "sJ ⊆ J"
shows "coprime (card sH) (card sJ)"
using assms by (meson coprime_divisors sub_subgroup_dvd_card)

lemma (in group) pow_eq_nat_mod:
assumes "a ∈ carrier G" "a [^] n = a [^] m"
shows "n mod (ord a) = m mod (ord a)"
proof -
from assms have "a [^] (n - m) = 𝟭" using pow_eq_div2 by blast
hence "ord a dvd n - m" using assms(1) pow_eq_id by blast
thus ?thesis
by (metis assms mod_eq_dvd_iff_nat nat_le_linear pow_eq_div2 pow_eq_id)
qed

lemma (in group) pow_eq_int_mod:
fixes n m::int
assumes "a ∈ carrier G" "a [^] n = a [^] m"
shows "n mod (ord a) = m mod (ord a)"
proof -
from assms have "a [^] (n - m) = 𝟭" using int_pow_closed int_pow_diff r_inv by presburger
hence "ord a dvd n - m" using assms(1) int_pow_eq_id by blast
thus ?thesis by (meson mod_eq_dvd_iff)
qed

end

# Theory Generated_Groups_Extend

(*
File:     Generated_Groups_Extend.thy
Author:   Joseph Thommes, TU München
*)
section ‹Generated Groups›

theory Generated_Groups_Extend
imports Miscellaneous_Groups "HOL-Algebra.Algebra"
begin

text ‹This section extends the lemmas and facts about ‹generate›. Starting with a basic fact.›

lemma (in group) generate_sincl:
"A ⊆ generate G A"
using generate.incl by fast

text ‹The following lemmas reflect some of the idempotence characteristics of ‹generate› and have
proved useful at several occasions.›

lemma (in group) generate_idem:
assumes "A ⊆ carrier G"
shows "generate G (generate G A) = generate G A"
using assms generateI group.generate_is_subgroup by blast

lemma (in group) generate_idem':
assumes "A ⊆ carrier G" "B ⊆ carrier G"
shows "generate G (generate G A ∪ B) = generate G (A ∪ B)"
proof
show "generate G (generate G A ∪ B) ⊆ generate G (A ∪ B)"
proof -
have "generate G A ∪ B ⊆ generate G (A ∪ B)"
proof -
have "generate G A ⊆ generate G (A ∪ B)" using mono_generate by simp
moreover have "B ⊆ generate G (A ∪ B)" by (simp add: generate.incl subset_iff)
ultimately show ?thesis by simp
qed
then have "generate G (generate G A ∪ B) ⊆ generate G (generate G (A ∪ B))"
using mono_generate by auto
with generate_idem[of "A ∪ B"] show ?thesis using assms by simp
qed
show "generate G (A ∪ B) ⊆ generate G (generate G A ∪ B)"
proof -
have "A ⊆ generate G A" using generate.incl by fast
thus ?thesis using mono_generate[of "A ∪ B" "generate G A ∪ B"] by blast
qed
qed

lemma (in group) generate_idem'_right:
assumes "A ⊆ carrier G" "B ⊆ carrier G"
shows "generate G (A ∪ generate G B) = generate G (A ∪ B)"
using generate_idem'[OF assms(2) assms(1)] by (simp add: sup_commute)

lemma (in group) generate_idem_Un:
assumes "A ⊆ carrier G"
shows "generate G (⋃x∈A. generate G {x}) = generate G A"
proof
have "A ⊆ (⋃x∈A. generate G {x})" using generate.incl by force
thus "generate G A ⊆ generate G (⋃x∈A. generate G {x})" using mono_generate by presburger
have "⋀x. x ∈ A ⟹ generate G {x} ⊆ generate G A" using mono_generate by auto
hence "(⋃x∈A. generate G {x}) ⊆ generate G A" by blast
thus "generate G (⋃x∈A. generate G {x}) ⊆ generate G A"
using generate_idem[OF assms] mono_generate by blast
qed

lemma (in group) generate_idem_fUn:
assumes "f A ⊆ carrier G"
shows "generate G (⋃ {generate G {x} |x. x ∈ f A}) = generate G (f A)"
proof
have "f A ⊆ ⋃ {generate G {x} |x. x ∈ f A}"
proof
fix x
assume x: "x ∈ f A"
have "x ∈ generate G {x}" using generate.incl by fast
thus "x ∈ ⋃ {generate G {x} |x. x ∈ f A}" using x by blast
qed
thus "generate G (f A) ⊆ generate G (⋃ {generate G {x} |x. x ∈ f A})" using mono_generate by auto
have "⋀x. x ∈ f A ⟹ generate G {x} ⊆ generate G (f A)" using mono_generate by simp
hence "(⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)" by blast
with mono_generate[OF this] show "generate G (⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)"
using generate_idem[OF assms] by simp
qed

lemma (in group) generate_idem_fim_Un:
assumes "⋃(f  A) ⊆ carrier G"
shows "generate G (⋃S ∈ A. generate G (f S)) = generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f  A)})"
proof

have "⋀S. S ∈ A ⟹ generate G (f S) = generate G (⋃ {generate G {x} |x. x ∈ f S})"
using generate_idem_fUn[of f] assms by blast
then have "generate G (⋃S ∈ A. generate G (f S))
= generate G (⋃S ∈ A. generate G (⋃ {generate G {x} |x. x ∈ f S}))" by simp

have "⋃ {generate G {x} |x. x ∈ ⋃ (f  A)} ⊆ (⋃S∈A. generate G (f S))"
proof
fix x
assume x: "x ∈ ⋃ {generate G {x} |x. x ∈ ⋃ (f  A)}"
then obtain a where a: "x ∈ generate G {a}" "a ∈ ⋃ (f  A)" by blast
then obtain M where M: "a ∈ f M" "M ∈ A" by blast
then have "generate G {a} ⊆ generate G (f M)"
using generate.incl[OF M(1), of G] mono_generate[of "{a}" "generate G (f M)"]
generate_idem assms by auto
then have "x ∈ generate G (f M)" using a by blast
thus "x ∈ (⋃S∈A. generate G (f S))" using M by blast
qed
thus "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f  A)}) ⊆ generate G (⋃S∈A. generate G (f S))"
using mono_generate by simp
have a: "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f  A))"
proof -
have "⋀S. S ∈ A ⟹ generate G (f S) ⊆ generate G (⋃ (f  A))"
using mono_generate[of _ "⋃ (f  A)"] by blast
then have "(⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f  A))" by blast
then have "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (generate G (⋃ (f  A)))"
using mono_generate by meson
thus "generate G (⋃S∈A. generate G (f S)) ⊆  generate G (⋃ (f  A))"
using generate_idem assms by blast
qed
have "⋃ {generate G {x} |x. x ∈ ⋃ (f  A)} = (⋃x∈⋃ (f  A). generate G {x})" by blast
with generate_idem_Un[OF assms]
have "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f  A)}) = generate G (⋃ (f  A))" by simp
with a show "generate G (⋃S∈A. generate G (f S))
⊆ generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f  A)})" by blast
qed

text ‹The following two rules allow for convenient proving of the equality of two generated sets.›

lemma (in group) generate_eqI:
assumes "A ⊆ carrier G" "B ⊆ carrier G" "A ⊆ generate G B" "B ⊆ generate G A"
shows "generate G A = generate G B"
using assms generate_idem by (metis generate_idem' inf_sup_aci(5) sup.absorb2)

lemma (in group) generate_one_switched_eqI:
assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}"
and "b ∈ generate G A" "a ∈ generate G B"
shows "generate G A = generate G B"
proof(intro generate_eqI)
show "A ⊆ carrier G" by fact
show "B ⊆ carrier G" using assms generate_incl by blast
show "A ⊆ generate G B" using assms generate_sincl[of B] by blast
show "B ⊆ generate G A" using assms generate_sincl[of A] by blast
qed

lemma (in group) generate_subset_eqI:
assumes "A ⊆ carrier G" "B ⊆ A" "A - B ⊆ generate G B"
shows "generate G A = generate G B"
proof
show "generate G B ⊆ generate G A" by (intro mono_generate, fact)
show "generate G A ⊆ generate G B"
proof(subst generate_idem[of "B", symmetric])
show "generate G A ⊆ generate G (generate G B)"
by (intro mono_generate, use assms generate_sincl[of B] in auto)
qed (use assms in blast)
qed

text ‹Some smaller lemmas about ‹generate›.›

lemma (in group) generate_subset_change_eqI:
assumes "A ⊆ carrier G" "B ⊆ carrier G" "C ⊆ carrier G" "generate G A = generate G B"
shows "generate G (A ∪ C) = generate G (B ∪ C)"
by (metis assms generate_idem')

lemma (in group) generate_subgroup_id:
assumes "subgroup H G"
shows "generate G H = H"
using assms generateI by auto

lemma (in group) generate_consistent':
assumes "subgroup H G" "A ⊆ H"
shows "∀x ∈ A. generate G {x} = generate (G⦇carrier := H⦈) {x}"
using generate_consistent assms by auto

lemma (in group) generate_singleton_one:
assumes "generate G {a} = {𝟭}"
shows "a = 𝟭"
using generate.incl[of a "{a}" G] assms by auto

lemma (in group) generate_inv_eq:
assumes "a ∈ carrier G"
shows "generate G {a} = generate G {inv a}"
by (intro generate_eqI;
use assms generate.inv[of a] generate.inv[of "inv a" "{inv a}" G] inv_inv[OF assms] in auto)

lemma (in group) generate_eq_imp_subset:
assumes "generate G A = generate G B"
shows "A ⊆ generate G B"
using generate.incl assms by fast

text ‹The neutral element does not play a role when generating a subgroup.›

lemma (in group) generate_one_irrel:
"generate G A = generate G (A ∪ {𝟭})"
proof
show "generate G A ⊆ generate G (A ∪ {𝟭})" by (intro mono_generate, blast)
show "generate G (A ∪ {𝟭}) ⊆ generate G A"
proof(rule subsetI)
show "x ∈ generate G A" if "x ∈ generate G (A ∪ {𝟭})" for x using that
by (induction rule: generate.induct;
use generate.one generate.incl generate.inv generate.eng in auto)
qed
qed

lemma (in group) generate_one_irrel':
"generate G A = generate G (A - {𝟭})"
using generate_one_irrel by (metis Un_Diff_cancel2)

text ‹Also, we can express the subgroup generated by a singleton with finite order using just its
powers up to its order.›

lemma (in group) generate_nat_pow:
assumes "ord a ≠ 0" "a ∈ carrier G"
shows "generate G {a} = {a [^] k |k. k ∈ {0..ord a - 1}}"
using assms generate_pow_nat ord_elems_inf_carrier by auto

lemma (in group) generate_nat_pow':
assumes "ord a ≠ 0" "a ∈ carrier G"
shows "generate G {a} = {a [^] k |k. k ∈ {1..ord a}}"
proof -
have "{a [^] k |k. k ∈ {1..ord a}} = {a [^] k |k. k ∈ {0..ord a - 1}}"
proof -
have "a [^] k ∈ {a [^] k |k. k ∈ {0..ord a - 1}}" if "k ∈ {1..ord a}" for k
using that pow_nat_mod_ord[OF assms(2, 1), of "ord a"] assms by (cases "k = ord a"; force)
moreover have "a [^] k ∈ {a [^] k |k. k ∈ {1..ord a}}" if "k ∈ {0..ord a - 1}" for k
proof(cases "k = 0")
case True
hence "a [^] k = a [^] ord a" using pow_ord_eq_1[OF assms(2)] by auto
moreover have "ord a ∈ {1..ord a}"
using assms unfolding atLeastAtMost_def atLeast_def atMost_def by auto
ultimately show ?thesis by blast
next
case False
then show ?thesis using that by auto
qed
ultimately show ?thesis by blast
qed
with generate_nat_pow[OF assms] show ?thesis by simp
qed

end

# Theory General_Auxiliary

(*
File:     General_Auxiliary.thy
Author:   Joseph Thommes, TU München; Manuel Eberl, TU München
*)
section ‹Auxiliary lemmas›

theory General_Auxiliary
imports "HOL-Algebra.Algebra"
begin

lemma inter_imp_subset: "A ∩ B = A ⟹ A ⊆ B"
by blast

lemma card_inter_eq:
assumes "finite A" "card (A ∩ B) = card A"
shows "A ⊆ B"
proof -
have "A ∩ B ⊆ A" by blast
with assms have "A ∩ B = A" using card_subset_eq by blast
thus ?thesis by blast
qed

lemma coprime_eq_empty_prime_inter:
assumes "(n::nat) ≠ 0" "m ≠ 0"
shows "coprime n m ⟷ (prime_factors n) ∩ (prime_factors m) = {}"
proof
show "coprime n m ⟹ prime_factors n ∩ prime_factors m = {}"
proof (rule ccontr)
assume cp: "coprime n m"
assume pf: "prime_factors n ∩ prime_factors m ≠ {}"
then obtain p where p: "p ∈ prime_factors n" "p ∈ prime_factors m" by blast
then have p_dvd: "p dvd n" "p dvd m" by blast+
moreover have "¬is_unit p" using p using not_prime_unit by blast
ultimately show "False" using cp unfolding coprime_def by simp
qed
assume assm: "prime_factors n ∩ prime_factors m = {}"
show "coprime n m" unfolding coprime_def
proof
fix c
show "c dvd n ⟶ c dvd m ⟶ is_unit c"
proof(rule; rule)
assume c: "c dvd n" "c dvd m"
then have "prime_factors c ⊆ prime_factors n" "prime_factors c ⊆ prime_factors m"
using assms dvd_prime_factors by blast+
then have "prime_factors c = {}" using assm by blast
thus "is_unit c" using assms c
by (metis dvd_0_left_iff prime_factorization_empty_iff set_mset_eq_empty_iff)
qed
qed
qed

lemma prime_factors_Prod:
assumes "finite S" "⋀a. a ∈ S ⟹ f a ≠ 0"
shows "prime_factors (prod f S) = ⋃(prime_factors  f  S)"
using assms
proof(induction S rule: finite_induct)
case empty
then show ?case by simp
next
case i: (insert x F)
from i have x: "f x ≠ 0" by blast
from i have F: "prod f F ≠ 0" by simp
from i have "prime_factors(prod f F) = ⋃ (prime_factors  f  F)" by blast
moreover have "prod f (insert x F) = (prod f F) * f x" using i mult.commute by force
ultimately
have "prime_factors (prod f (insert x F)) = (⋃(prime_factors  f  F)) ∪ prime_factors (f x)"
using prime_factors_product[OF F x] by argo
thus ?case by force
qed

lemma lcm_is_Min_multiple_nat:
assumes "c ≠ 0" "(a::nat) dvd c" "(b::nat) dvd c"
shows "c ≥ lcm a b"
using lcm_least[of a c b] assms by fastforce

lemma diff_prime_power_imp_coprime:
assumes "p ≠ q" "Factorial_Ring.prime (p::nat)" "Factorial_Ring.prime q"
shows "coprime (p ^ (n::nat)) (q ^ m)"
using assms
by (metis power_0 power_one_right prime_dvd_power prime_imp_power_coprime_nat
prime_nat_iff prime_power_inj'')

lemma "finite (prime_factors x)"
using finite_set_mset by blast

lemma card_ge_1_two_diff:
assumes "card A > 1"
obtains x y where "x ∈ A" "y ∈ A" "x ≠ y"
proof -
have fA: "finite A" using assms by (metis card.infinite not_one_less_zero)
from assms obtain x where x: "x ∈ A" by fastforce
with assms fA have "card (A - {x}) > 0" by simp
then obtain y where y: "y ∈ (A - {x})" by (metis card_gt_0_iff ex_in_conv)
thus ?thesis using that[of x y] x by blast
qed

lemma infinite_two_diff:
assumes "infinite A"
obtains x y where "x ∈ A" "y ∈ A" "x ≠ y"
proof -
from assms obtain x where x: "x ∈ A" by fastforce
from assms have "infinite (A - {x})" by simp
then obtain y where y: "y ∈ (A - {x})"
by (metis ex_in_conv finite.emptyI)
show ?thesis using that[of x y] using x y by blast
qed

lemma Inf_le:
"Inf A ≤ x" if "x ∈ (A::nat set)" for x
proof (cases "A = {}")
case True
then show ?thesis using that by simp
next
case False
hence "Inf A ≤ Inf {x}" using that by (simp add: cInf_lower)
also have "… = x" by simp
finally show "Inf A ≤ x" by blast
qed

lemma switch_elem_card_le:
assumes "a ∈ A"
shows "card (A - {a} ∪ {b}) ≤ card A"
using assms
by (metis Diff_insert_absorb Set.set_insert Un_commute card.infinite card_insert_disjoint
card_mono finite_insert insert_is_Un insert_subset order_refl)

lemma pairwise_coprime_dvd:
assumes "finite A" "pairwise coprime A" "(n::nat) = prod id A" "∀a∈A. a dvd j"
shows "n dvd j"
using assms
proof (induction A arbitrary: n)
case i: (insert x F)
have "prod id F dvd j" "x dvd j" using i unfolding pairwise_def by auto
moreover have "coprime (prod id F) x"
by (metis i(2, 4) id_apply pairwise_insert prod_coprime_left)
ultimately show ?case using i(1, 2, 5) by (simp add: coprime_commute divides_mult)
qed simp

lemma pairwise_coprime_dvd':
assumes "finite A" "⋀i j. ⟦i ∈ A; j ∈ A; i ≠ j⟧ ⟹ coprime (f i) (f j)"
"(n::nat) = prod f A" "∀a∈A. f a dvd j"
shows "n dvd j"
using assms
proof (induction A arbitrary: n)
case i: (insert x F)
have "prod f F dvd j" "f x dvd j" using i unfolding pairwise_def by auto
moreover have "coprime (prod f F) (f x)" by(intro prod_coprime_left, use i in blast)
ultimately show ?case using i by (simp add: coprime_commute divides_mult)
qed simp

lemma transp_successively_remove1:
assumes "transp f" "successively f l"
shows "successively f (remove1 a l)" using assms(2)
proof(induction l rule: induct_list012)
case (3 x y zs)
from 3(3)[unfolded successively.simps] have fs: "f x y" "successively f (y # zs)" by auto
moreover from this(2) successively.simps have s: "successively f zs" by(cases zs, auto)
ultimately have s2: "successively f (remove1 a zs)" "successively f (remove1 a (y # zs))"
using 3 by auto
consider (x) "x = a" | (y) "y = a ∧ x ≠ a" | (zs) "a ≠ x ∧ a ≠ y" by blast
thus ?case
proof (cases)
case x
then show ?thesis using 3 by simp
next
case y
then show ?thesis
proof (cases zs)
case Nil
then show ?thesis using fs by simp
next
case (Cons a list)
hence "f y a" using fs by simp
hence "f x a" using fs(1) assms(1)[unfolded transp_def] by blast
then show ?thesis using Cons y s by auto
qed
next
case zs
then show ?thesis using s2 fs by auto
qed
qed auto

lemma exp_one_2pi_iff:
fixes x::real shows "exp (2 * of_real pi * 𝗂 * x) = 1 ⟷ x ∈ ℤ"
proof -
have c: "cis (2 * x * pi) = 1 ⟷ x ∈ ℤ"
by (auto simp: complex_eq_iff sin_times_pi_eq_0 cos_one_2pi_int, meson Ints_cases)
have "exp (2 * of_real pi * 𝗂 * x) = exp (𝗂 * complex_of_real (2 * x * pi))"
proof -
have "2 * of_real pi * 𝗂 * x = 𝗂 * complex_of_real (2 * x * pi)" by simp
thus ?thesis by argo
qed
also from cis_conv_exp have "… = cis (2 * x * pi)" by simp
finally show ?thesis using c by simp
qed

(* Manuel Eberl *)
lemma of_int_divide_in_Ints_iff:
assumes "b ≠ 0"
shows   "(of_int a / of_int b :: 'a :: field_char_0) ∈ ℤ ⟷ b dvd a"
proof
assume *: "(of_int a / of_int b :: 'a :: field_char_0) ∈ ℤ"
from * obtain n where "of_int a / of_int b = (of_int n :: 'a)"
by (elim Ints_cases)
hence "of_int (b * n) = (of_int a :: 'a)"
using assms by (subst of_int_mult) (auto simp: field_simps)
hence "b * n = a"
by (subst (asm) of_int_eq_iff)
thus "b dvd a" by auto
qed auto

(* Manuel Eberl *)
lemma of_nat_divide_in_Ints_iff:
assumes "b ≠ 0"
shows   "(of_nat a / of_nat b :: 'a :: field_char_0) ∈ ℤ ⟷ b dvd a"
using of_int_divide_in_Ints_iff[of "int b" "int a"] assms by simp

lemma true_nth_unity_root:
fixes n::nat
obtains x::complex where "x ^ n = 1" "⋀m. ⟦0<m; m<n⟧ ⟹ x ^ m ≠ 1"
proof(cases "n = 0")
case False
show ?thesis
proof (rule that)
show "cis (2 * pi / n) ^ n = 1"
next
fix m assume m: "m > 0" "m < n"
have "cis (2 * pi / n) ^ m = cis (2 * pi * m / n)"
also have "… = 1 ⟷ real m / real n ∈ ℤ"
using exp_one_2pi_iff[of "m / n"] by (simp add: cis_conv_exp algebra_simps)
also have "… ⟷ n dvd m"
using m by (subst of_nat_divide_in_Ints_iff) auto
also have "¬n dvd m"
using m by auto
finally show "cis (2 * pi / real n) ^ m ≠ 1" .
qed
qed simp

lemma finite_bij_betwI:
assumes "finite A" "finite B" "inj_on f A" "f ∈ A → B" "card A = card B"
shows "bij_betw f A B"
proof (intro bij_betw_imageI)
show "inj_on f A" by fact
show "f  A = B"
proof -
have "card (f  A) = card B" using assms by (simp add: card_image)
moreover have "f  A ⊆ B" using assms by blast
ultimately show ?thesis using assms by (meson card_subset_eq)
qed
qed

lemma powi_mod:
"x powi m = x powi (m mod n)" if "x ^ n = 1" "n > 0" for x::complex and m::int
proof -
have xnz: "x ≠ 0" using that by (metis zero_neq_one zero_power)
obtain k::int where k: "m = k*n + (m mod n)" using div_mod_decomp_int by blast
have "x powi m = x powi (k*n) * x powi (m mod n)" by (subst k, intro power_int_add, use xnz in auto)
moreover have "x powi (k*n) = 1" using that
by (metis mult.commute power_int_1_left power_int_mult power_int_of_nat)
ultimately show ?thesis by force
qed

(* Manuel Eberl *)
lemma Sigma_insert: "Sigma (insert x A) B = (λy. (x, y))  B x ∪ Sigma A B"
by auto

end

# Theory IDirProds

(*
File:     IDirProds.thy
Author:   Joseph Thommes, TU München
*)
section ‹Internal direct product›

theory IDirProds
imports Generated_Groups_Extend General_Auxiliary
begin

subsection ‹Complementarity›

text ‹We introduce the notion of complementarity, that plays a central role in the internal
direct group product and prove some basic properties about it.›

definition (in group) complementary :: "'a set ⇒ 'a set ⇒ bool" where
"complementary H1 H2 ⟷ H1 ∩ H2 = {𝟭}"

lemma (in group) complementary_symm: "complementary A B ⟷ complementary B A"
unfolding complementary_def by blast

lemma (in group) subgroup_carrier_complementary:
assumes "complementary H J" "subgroup I (G⦇carrier := H⦈)" "subgroup K (G⦇carrier := J⦈)"
shows "complementary I K"
proof -
have "𝟭 ∈ I"  "𝟭 ∈ K" using subgroup.one_closed assms by fastforce+
moreover have "I ∩ K ⊆ H ∩ J" using subgroup.subset assms by force
ultimately show ?thesis using assms unfolding complementary_def by blast
qed

lemma (in group) subgroup_subset_complementary:
assumes "subgroup H G" "subgroup J G" "subgroup I G"
and "I ⊆ J" "complementary H J"
shows "complementary H I"
by (intro subgroup_carrier_complementary[OF assms(5), of H I] subgroup_incl, use assms in auto)

lemma (in group) complementary_subgroup_iff:
assumes "subgroup H G"
shows "complementary A B ⟷ group.complementary (G⦇carrier := H⦈) A B"
proof -
interpret H: group "G⦇carrier := H⦈" using subgroup.subgroup_is_group assms by blast
have "𝟭⇘G⇙ = 𝟭⇘G⦇carrier := H⦈⇙" by simp
then show ?thesis unfolding complementary_def H.complementary_def by simp
qed

lemma (in group) subgroups_card_coprime_imp_compl:
assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
shows "complementary H J" unfolding complementary_def
proof -
interpret JH: subgroup "(H ∩ J)" G using assms subgroups_Inter_pair by blast
from subgroups_card_coprime_inter_card_one[OF assms] show "H ∩ J = {𝟭}" using JH.one_closed
by (metis card_1_singletonE singletonD)
qed

lemma (in group) prime_power_complementary_groups:
assumes "Factorial_Ring.prime p" "Factorial_Ring.prime q" "p ≠ q"
and "subgroup P G" "card P = p ^ x"
and "subgroup Q G" "card Q = q ^ y"
shows "complementary P Q"
proof -
from assms have "coprime (card P) (card Q)"
by (metis coprime_power_right_iff primes_coprime coprime_def)
then show ?thesis using subgroups_card_coprime_imp_compl assms complementary_def by blast
qed

text ‹With the previous work from the theory about set multiplication we can characterize
complementarity of two subgroups in abelian groups by the cardinality of their product.›

lemma (in comm_group) compl_imp_diff_cosets:
assumes "subgroup H G" "subgroup J G" "finite H" "finite J"
and "complementary H J"
shows "⋀a b. ⟦a ∈ J; b ∈ J; a ≠ b⟧ ⟹ (H #> a) ≠ (H #> b)"
proof (rule ccontr; safe)
fix a b
assume ab: "a ∈ J" "b ∈ J" "a ≠ b"
then have [simp]: "a ∈ carrier G" "b ∈ carrier G" using assms subgroup.subset by auto
assume "H #> a = H #> b"
then have "a ⊗ inv b ∈ H" using assms(1, 2) ab
by (metis comm_group_axioms comm_group_def rcos_self
subgroup.mem_carrier subgroup.rcos_module_imp)
moreover have "a ⊗ inv b ∈ J"
by (rule subgroup.m_closed[OF assms(2) ab(1) subgroup.m_inv_closed[OF assms(2) ab(2)]])
moreover have "a ⊗ inv b ≠ 𝟭" using ab inv_equality by fastforce
ultimately have "H ∩ J ≠ {𝟭}" by blast
thus False using assms(5) unfolding complementary_def by blast
qed

lemma (in comm_group) finite_sub_card_eq_mult_imp_comp:
assumes "subgroup H G" "subgroup J G" "finite H" "finite J"
and "card (H <#> J) = (card J * card H)"
shows "complementary H J"
unfolding complementary_def
proof (rule ccontr)
assume "H ∩ J ≠ {𝟭}"
have "𝟭 ∈ H" using subgroup.one_closed assms(1) by blast
moreover have "𝟭 ∈ J" using subgroup.one_closed assms(2) by blast
ultimately have "𝟭 ∈ (H ∩ J)" by blast

then obtain a where a_def: "a ∈ (H ∩ J) ∧ a ≠ 𝟭" using ‹H ∩ J ≠ {𝟭}› by blast
then have aH: "a ∈ H" by blast
then have a_inv_H: "inv a ∈ H ∧ inv a ≠ 𝟭" using assms(1)
by (meson a_def inv_eq_1_iff subgroup.mem_carrier subgroupE(3))
from a_def have aJ: "a ∈ J" by blast
then have a_inv_J: "inv a ∈ J ∧ inv a ≠ 𝟭" using assms(2)
by (meson a_def inv_eq_1_iff subgroup.mem_carrier subgroupE(3))
from a_def have a_c: "a ∈ carrier G" using subgroup.subset[of J G] assms(2) by blast

from set_mult_card_eq_impl_empty_inter'[of H J]
have empty: "⋀a b. ⟦a ∈ H; b ∈ H; a ≠ b⟧ ⟹ (l_coset G a J) ∩ (l_coset G b J) = {}"
using assms subgroup.subset[of _ G] by simp

have "𝟭 ∈ 𝟭 <# J" using ‹𝟭 ∈ J› unfolding l_coset_def by force
moreover have "𝟭 ∈ a <# J" using a_inv_J aJ a_c assms ‹𝟭 ∈ J› coset_join3 by blast
ultimately have "(l_coset G 𝟭 J) ∩ (l_coset G a J) ≠ {}" by blast

then show "False" using empty[of "𝟭" a] a_def aH ‹𝟭 ∈ H› by blast
qed

lemma (in comm_group) finite_sub_comp_imp_card_eq_mult:
assumes "subgroup H G" "subgroup J G" "finite H" "finite J"
and "complementary H J"
shows "card (H <#> J) = card J * card H"
proof -
have carr: "H ⊆ carrier G" "J ⊆ carrier G" using assms subgroup.subset by auto

from coset_neq_imp_empty_inter[OF assms(1)] compl_imp_diff_cosets[OF assms(1,2)]
have em_inter: "⋀a b. ⟦a ∈ J; b ∈ J; a ≠ b⟧ ⟹ (H #> a) ∩ (H #> b) = {}"
by (meson assms subgroup.mem_carrier)

have "card (⋃a∈J. (H #> a)) = card J * card H" using assms(4) carr(2) em_inter
proof (induction J rule: finite_induct)
case empty
then show ?case by auto
next
case i: (insert x F)
then have cF:"card (⋃ ((#>) H  F)) = card F * card H" by blast
have xc[simp]: "x ∈ carrier G" using i(4) by simp
let ?J = "insert x F"
from i(2, 4, 5) have em:"(H #> x) ∩ (⋃y∈F. (H #> y)) = {}" by auto
have "finite (H #> x)"
by (meson carr(1) rcosetsI rcosets_finite assms(3) xc)
moreover have "finite (H <#> F)" using set_mult_finite[OF assms(3) i(1) carr(1)] i(4) by blast
moreover have "H <#> F = (⋃a∈F. (H #> a))"
unfolding set_mult_def using r_coset_def[of G H] by auto
ultimately have "card(H #> x) + card(⋃y∈F. (H #> y))
= card((H #> x) ∪ (⋃y∈F. (H #> y))) + card((H #> x) ∩ (⋃y∈F. (H #> y)))"
using card_Un_Int by auto
then have "card(H #> x) + card(⋃y∈F. (H #> y)) = card((H #> x) ∪ (⋃y∈F. (H #> y)))"
using i(5) em by simp
moreover have "card (H #> x) = card H"
using card_rcosets_equal[of _ H] rcosetsI[of H] carr(1) xc by metis
moreover have "card (insert x F) * card H = card F * card H + card H"
ultimately show ?case using cF by simp
qed
moreover have "H <#> J = (⋃a∈J. (H #> a))"
unfolding set_mult_def using r_coset_def[of G H] by auto
ultimately show "card (H <#> J) = card J * card H" by argo
qed

lemma (in comm_group) finite_sub_comp_iff_card_eq_mult:
assumes "subgroup H G" "subgroup J G" "finite H" "finite J"
shows "card (H <#> J) = card J * card H  ⟷ complementary H J"
using finite_sub_comp_imp_card_eq_mult[OF assms] finite_sub_card_eq_mult_imp_comp[OF assms]
by blast

subsection ‹‹IDirProd› - binary internal direct product›

text ‹We introduce the internal direct product formed by two subgroups (so in its binary form).›

definition IDirProd :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ 'a set ⇒ 'a set" where
"IDirProd G Y Z = generate G (Y ∪ Z)"

text ‹Some trivial lemmas about the binary internal direct product.›

lemma (in group) IDirProd_comm:
"IDirProd G A B = IDirProd G B A"
unfolding IDirProd_def by (simp add: sup_commute)

lemma (in group) IDirProd_empty_right:
assumes "A ⊆ carrier G"
shows "IDirProd G A {} = generate G A"
unfolding IDirProd_def by simp

lemma (in group) IDirProd_empty_left:
assumes "A ⊆ carrier G"
shows "IDirProd G {} A = generate G A"
unfolding IDirProd_def by simp

lemma (in group) IDirProd_one_right:
assumes "A ⊆ carrier G"
shows "IDirProd G A {𝟭} = generate G A"
unfolding IDirProd_def
proof
interpret sA: subgroup "(generate G A)" G using assms generate_is_subgroup by simp
interpret sAone: subgroup "(generate G (A ∪ {𝟭}))" G using assms generate_is_subgroup by simp
show "generate G (A ∪ {𝟭}) ⊆ generate G A"
using generate_subgroup_incl[of "A ∪ {𝟭}" "generate G A"]
generate.incl assms sA.one_closed sA.subgroup_axioms by fast
show "generate G A ⊆ generate G (A ∪ {𝟭})"
using mono_generate[of A "A ∪ {𝟭}"] by blast
qed

lemma (in group) IDirProd_one_left:
assumes "A ⊆ carrier G"
shows "IDirProd G {𝟭} A = generate G A"
using IDirProd_one_right[of A] assms unfolding IDirProd_def by force

lemma (in group) IDirProd_is_subgroup:
assumes "Y ⊆ carrier G" "Z ⊆ carrier G"
shows "subgroup (IDirProd G Y Z) G"
unfolding IDirProd_def using generate_is_subgroup[of "Y ∪ Z"] assms by simp

text ‹Using the theory about set multiplication we can also show the connection of the underlying
set in the internal direct product with the set multiplication in the case of an abelian group.
Together with the facts about complementarity and the set multiplication we can characterize
complementarity by the cardinality of the internal direct product and vice versa.›

lemma (in comm_group) IDirProd_eq_subgroup_mult:
assumes "subgroup H G" "subgroup J G"
shows "IDirProd G H J = H <#> J"
unfolding IDirProd_def
by (rule set_mult_eq_generate_subgroup[OF assms])

lemma (in comm_group) finite_sub_comp_iff_card_eq_IDirProd:
assumes "subgroup H G" "subgroup J G" "finite H" "finite J"
shows "card (IDirProd G H J) = card J * card H  ⟷ complementary H J"
using finite_sub_comp_iff_card_eq_mult IDirProd_eq_subgroup_mult assms by presburger

subsection ‹‹IDirProds› - indexed internal direct product›

text ‹The indexed version of the internal direct product acting on a family of subgroups.›

definition IDirProds :: "('a, 'b) monoid_scheme ⇒ ('c ⇒ 'a set) ⇒ 'c set ⇒ 'a set" where
"IDirProds G S I = generate G (⋃(S  I))"

text ‹Lemmas about the indexed internal direct product.›

lemma (in group) IDirProds_incl:
assumes "i ∈ I"
shows "S i ⊆ IDirProds G S I"
unfolding IDirProds_def using assms generate.incl[of _ "⋃(S  I)" G] by blast

lemma (in group) IDirProds_empty:
"IDirProds G S {} = {𝟭}"
unfolding IDirProds_def using generate_empty by simp

lemma (in group) IDirProds_is_subgroup:
assumes "⋃(S  I) ⊆ (carrier G)"
shows "subgroup (IDirProds G S I) G"
unfolding IDirProds_def using generate_is_subgroup[of "⋃(S  I)"] assms by auto

lemma (in group) IDirProds_subgroup_id: "subgroup (S i) G ⟹ IDirProds G S {i} = S i"

lemma (in comm_group) IDirProds_Un:
assumes "∀i∈A. subgroup (S i) G" "∀j∈B. subgroup (S j) G"
shows   "IDirProds G S (A ∪ B) = IDirProds G S A <#> IDirProds G S B"
proof -
have subset: "⋃ (S  A) ⊆ carrier G" "⋃ (S  B) ⊆ carrier G"
using subgroup.subset assms(1, 2) by blast+
have "IDirProds G S A <#> IDirProds G S B = IDirProd G (IDirProds G S A) (IDirProds G S B)"
using assms by (intro IDirProd_eq_subgroup_mult [symmetric] IDirProds_is_subgroup subset)
also have "… = generate G (⋃ (S  A) ∪ IDirProds G S B)"
unfolding IDirProds_def IDirProd_def by (intro generate_idem' generate_incl subset)
also have "… = generate G (⋃(S  A) ∪ ⋃(S  B))"
unfolding IDirProds_def IDirProd_def
by (intro generate_idem'_right generate_incl subset)
also have "⋃(S  A) ∪ ⋃(S  B) = ⋃(S  (A ∪ B))"
by blast
also have "generate G … = IDirProds G S (A ∪ B)"
unfolding IDirProds_def ..
finally show ?thesis ..
qed

lemma (in comm_group) IDirProds_finite:
assumes "finite I" "∀i∈I. subgroup (S i) G" "∀i∈I. finite (S i)"
shows "finite (IDirProds G S I)" using assms
proof (induction I rule: finite_induct)
case empty
thus ?case using IDirProds_empty[of S] by simp
next
case i: (insert x I)
interpret Sx: subgroup "S x" G using i by blast
have cx: "(S x) ⊆ carrier G" by force
have cI: "⋃(S  I) ⊆ carrier G" using i subgroup.subset by blast
interpret subgroup "IDirProds G S I" G using IDirProds_is_subgroup[OF cI] .
have cIP: "(IDirProds G S I) ⊆ carrier G" by force
from i have f: "finite (S x)" "finite (IDirProds G S I)" "finite {x}" by blast+
from IDirProds_Un[of "{x}" S I]
have "IDirProds G S ({x} ∪ I) = IDirProds G S {x} <#> IDirProds G S I" using i by blast
also have "… = S x <#> IDirProds G S I"
using IDirProds_subgroup_id[of S x] Sx.subgroup_axioms by force
also have "finite (…)" using set_mult_finite[OF f(1, 2) cx cIP] .
finally show ?case unfolding insert_def by simp
qed

lemma (in comm_group) IDirProds_compl_imp_compl:
assumes "∀i ∈ I. subgroup (S i) G" and "subgroup H G"
assumes "complementary H (IDirProds G S I)" "i ∈ I"
shows   "complementary H (S i)"
proof -
have "S i ⊆ IDirProds G S I" using assms IDirProds_incl by fast
then have "H ∩ (S i) ⊆ H ∩ IDirProds G S I" by blast
moreover have "𝟭 ∈ H ∩ (S i)" using subgroup.one_closed assms by auto
ultimately show "complementary H (S i)" using assms(3) unfolding complementary_def by blast
qed

text ‹Using the knowledge about the binary internal direct product, we can - in case that all
subgroups in the family have coprime orders - also derive the cardinality of the indexed internal
direct product.›

lemma (in comm_group) IDirProds_card:
assumes "finite I" "∀i∈I. subgroup (S i) G"
"∀i∈I. finite (S i)" "pairwise (λx y. coprime (card (S x)) (card (S y))) I"
shows "card (IDirProds G S I) = (∏i ∈ I. card (S i))" using assms
proof (induction I rule: finite_induct)
case empty
then show ?case using IDirProds_empty[of S] by simp
next
case i: (insert x I)
have sx: "subgroup (S x) G" using i(4) by blast
have cx: "(S x) ⊆ carrier G" using subgroup.subset[OF sx] .
have fx: "finite (S x)" using i by blast
have cI: "⋃(S  I) ⊆ carrier G" using subgroup.subset[of _ G] i(4) by blast
from generate_is_subgroup[OF this] have sIP: "subgroup (IDirProds G S I) G"
unfolding IDirProds_def .
then have cIP: "(IDirProds G S I) ⊆ carrier G" using subgroup.subset by blast
have fIP: "finite (IDirProds G S I)" using IDirProds_finite[OF i(1)] i by blast

from i have ih: "card (IDirProds G S I) = (∏i∈I. card (S i))" unfolding pairwise_def by blast
hence cop: "coprime (card (IDirProds G S I)) (card (S x))"
proof -
have cFI0: "card (IDirProds G S I) ≠ 0" using finite_subgroup_card_neq_0[OF sIP fIP] .
moreover have cx0: "card (S x) ≠ 0" using finite_subgroup_card_neq_0[OF sx fx] .
moreover have  "prime_factors (card (IDirProds G S I)) ∩ prime_factors (card (S x)) = {}"
proof (rule ccontr)
have n0: "⋀i. i ∈ I ⟹ card (S i) ≠ 0" using finite_subgroup_card_neq_0 i(4, 5) by blast
assume "prime_factors (card (IDirProds G S I)) ∩ prime_factors (card (S x)) ≠ {}"
moreover have "prime_factors (card (IDirProds G S I)) = ⋃(prime_factors  (card ∘ S)  I)"
using n0 prime_factors_Prod[OF i(1), of "card ∘ S"] by (subst ih; simp)
moreover have "⋀i. i ∈ I ⟹ prime_factors (card (S i)) ∩ prime_factors (card (S x)) = {}"
proof -
fix i
assume ind: "i ∈ I"
then have coPx: "coprime (card (S i)) (card (S x))"
using i(2, 6) unfolding pairwise_def by auto
have "card (S i) ≠ 0" using n0 ind by blast
from coprime_eq_empty_prime_inter[OF this cx0]
show "prime_factors (card (S i)) ∩ prime_factors (card (S x)) = {}" using coPx by blast
qed
ultimately show "False" by auto
qed
ultimately show ?thesis using coprime_eq_empty_prime_inter by blast
qed
have "card (IDirProds G S (insert x I)) = card (S x) * card (IDirProds G S I)"
proof -
from finite_sub_comp_iff_card_eq_IDirProd[OF sIP sx fIP fx]
subgroups_card_coprime_imp_compl[OF sIP sx cop]
have "card (IDirProd G (IDirProds G S I) (S x)) = card (S x) * card (IDirProds G S I)" by blast
moreover have "generate G (⋃ (S  insert x I)) = generate G (generate G (⋃ (S  I)) ∪ S x)"
by (simp add: Un_commute cI cx generate_idem'_right)
ultimately show ?thesis unfolding IDirProds_def IDirProd_def by argo
qed
also have "… = card (S x) * prod (card ∘ S) I" using ih by simp
also have "… = prod (card ∘ S) ({x} ∪ I)" using i.hyps by auto
finally show ?case by simp
qed

subsection "Complementary family of subgroups"

text ‹The notion of a complementary family is introduced. Note that the subgroups are complementary
not only to the other subgroups but to the product of the other subgroups.›

definition (in group) compl_fam :: "('c ⇒ 'a set) ⇒ 'c set ⇒ bool" where
"compl_fam S I = (∀i ∈ I. complementary (S i) (IDirProds G S (I - {i})))"

lemma (in group) compl_fam_empty[simp]: "compl_fam S {}"
unfolding compl_fam_def by simp

lemma (in group) compl_fam_cong:
assumes "compl_fam (f ∘ g) A" "inj_on g A"
shows "compl_fam f (g  A)"
proof -
have "((f ∘ g)  (A - {i})) =  (f  (g  A - {g i}))" if "i ∈ A" for i
using assms that unfolding inj_on_def comp_def by blast
thus ?thesis using assms unfolding compl_fam_def IDirProds_def complementary_def by simp
qed

text ‹We now connect ‹compl_fam› with ‹generate› as this will be its main application.›

lemma (in comm_group) compl_fam_imp_generate_inj:
assumes "gs ⊆ carrier G" "compl_fam (λg. generate G {g}) gs"
shows "inj_on (λg. generate G {g}) gs"
proof(rule, rule ccontr)
fix x y
assume xy: "x ∈ gs" "y ∈ gs" "x ≠ y"
have gen: "generate G (⋃g∈gs - {y}. generate G {g}) = generate G (gs - {y})"
by (intro generate_idem_Un, use assms in blast)
assume g: "generate G {x} = generate G {y}"
with xy have "generate G {y} ⊆ generate G (gs - {y})" using mono_generate[of "{x}" "gs - {y}"] by auto
with xy have gyo: "generate G {y} = {𝟭}" using assms(2) generate.one gen
unfolding compl_fam_def complementary_def IDirProds_def by blast
hence yo: "y = 𝟭" using generate_singleton_one by simp
from gyo g generate_singleton_one have xo: "x = 𝟭" by simp
from xy yo xo show False by blast
qed

lemma (in comm_group) compl_fam_generate_subset:
assumes "compl_fam (λg. generate G {g}) gs"
"gs ⊆ carrier G" "A ⊆ gs"
shows "compl_fam (λg. generate G {g}) A"
proof(unfold compl_fam_def complementary_def IDirProds_def, subst generate_idem_Un)
show "⋀i. A - {i} ⊆ carrier G" using assms by blast
have "generate G {i} ∩ generate G (A - {i}) = {𝟭}" if "i ∈ A" for i
proof -
have "𝟭 ∈ generate G {i} ∩ generate G (A - {i})" using generate.one by blast
moreover have "generate G (A - {i}) ⊆ generate G (gs - {i})"
by (intro mono_generate, use assms in fast)
moreover have "generate G {i} ∩ generate G (gs - {i}) = {𝟭}"
using assms that generate_idem_Un[of "gs - {i}"]
unfolding compl_fam_def IDirProds_def complementary_def by blast
ultimately show ?thesis by blast
qed
thus "∀i∈A. generate G {i} ∩ generate G (A - {i}) = {𝟭}" by auto
qed

subsection ‹‹is_idirprod››

text ‹In order to identify a group as the internal direct product of a family of subgroups, they all
have to be normal subgroups, complementary to the product of the rest of the subgroups and generate
all of the group - this is captured in the definition of ‹is_idirprod›.›

definition (in group) is_idirprod :: "'a set ⇒ ('c ⇒ 'a set) ⇒ 'c set ⇒ bool" where
"is_idirprod A S I = ((∀i ∈ I. S i ⊲ G) ∧ A = IDirProds G S I ∧ compl_fam S I)"

text ‹Very basic lemmas about ‹is_idirprod›.›

lemma (in comm_group) is_idirprod_subgroup_suffices:
assumes "A = IDirProds G S I" "∀i∈I. subgroup (S i) G" "compl_fam S I"
shows "is_idirprod A S I"
unfolding is_idirprod_def using assms subgroup_imp_normal by blast

lemma (in comm_group) is_idirprod_generate:
assumes "A = generate G gs" "gs ⊆ carrier G" "compl_fam (λg. generate G {g}) gs"
shows "is_idirprod A (λg. generate G {g}) gs"
proof(intro is_idirprod_subgroup_suffices)
show "A = IDirProds G (λg. generate G {g}) gs"
using assms generate_idem_Un[OF assms(2)] unfolding IDirProds_def by argo
show "∀i∈gs. subgroup (generate G {i}) G" using assms generate_is_subgroup by auto
show "compl_fam (λg. generate G {g}) gs" by fact
qed

lemma (in comm_group) is_idirprod_imp_compl_fam[simp]:
assumes "is_idirprod A S I"
shows "compl_fam S I"
using assms unfolding is_idirprod_def by blast

lemma (in comm_group) is_idirprod_generate_imp_generate[simp]:
assumes "is_idirprod A (λg. generate G {g}) gs"
shows "A = generate G gs"
proof -
have "gs ⊆ carrier G"
proof
show "g ∈ carrier G" if "g ∈ gs" for g
proof -
interpret g: subgroup "generate G {g}" G
using assms that normal_imp_subgroup unfolding is_idirprod_def by blast
show ?thesis using g.subset generate.incl by fast
qed
qed
thus ?thesis using assms generate_idem_Un unfolding is_idirprod_def IDirProds_def by presburger
qed

end

# Theory Finite_Product_Extend

(*
File:     Finite_Product_Extend.thy
Author:   Joseph Thommes, TU München; Manuel Eberl, TU München
*)
section ‹Finite Product›

theory Finite_Product_Extend
imports IDirProds
begin

text ‹In this section, some general facts about ‹finprod› as well as some tailored for the rest of
this entry are proven.›

text ‹It is often needed to split a product in a single factor and the rest. Thus these two lemmas.›

lemma (in comm_group) finprod_minus:
assumes "a ∈ A" "f ∈ A → carrier G" "finite A"
shows "finprod G f A = f a ⊗ finprod G f (A - {a})"
proof -
from assms have "A = insert a (A - {a})" by blast
then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
finally show ?thesis .
qed

lemma (in comm_group) finprod_minus_symm:
assumes "a ∈ A" "f ∈ A → carrier G" "finite A"
shows "finprod G f A = finprod G f (A - {a}) ⊗ f a"
proof -
from assms have "A = insert a (A - {a})" by blast
then have "finprod G f A = finprod G f (insert a (A - {a}))" by simp
also have "… = f a ⊗ finprod G f (A - {a})" using assms by (intro finprod_insert, auto)
also have "… = finprod G f (A - {a}) ⊗ f a"
by (intro m_comm, use assms in blast, intro finprod_closed, use assms in blast)
finally show ?thesis .
qed

text ‹This makes it very easy to show the following trivial fact.›

lemma (in comm_group) finprod_singleton:
assumes "f x ∈ carrier G" "finprod G f {x} = a"
shows "f x = a"
proof -
have "finprod G f {x} = f x ⊗ finprod G f {}" using finprod_minus[of x "{x}" f] assms by auto
thus ?thesis using assms by simp
qed

text ‹The finite product is consistent and closed concerning subgroups.›

lemma (in comm_group) finprod_subgroup:
assumes "f ∈ S → H" "subgroup H G"
shows "finprod G f S = finprod (G⦇carrier := H⦈) f S"
proof (cases "finite S")
case True
interpret H: comm_group "G⦇carrier := H⦈" using subgroup_is_comm_group[OF assms(2)] .
show ?thesis using True assms
proof (induction S rule: finite_induct)
case empty
then show ?case using finprod_empty H.finprod_empty by simp
next
case i: (insert x F)
then have "finprod G f F = finprod (G⦇carrier := H⦈) f F" by blast
moreover have "finprod G f (insert x F) = f x ⊗ finprod G f F"
proof(intro finprod_insert[OF i(1, 2), of f])
show "f ∈ F → carrier G" "f x ∈ carrier G" using i(4) subgroup.subset[OF i(5)] by blast+
qed
ultimately have "finprod G f (insert x F) = f x ⊗⇘G⦇carrier := H⦈⇙ finprod (G⦇carrier := H⦈) f F"
by auto
moreover have "finprod (G⦇carrier := H⦈) f (insert x F) = …"
proof(intro H.finprod_insert[OF i(1, 2)])
show "f ∈ F → carrier (G⦇carrier := H⦈)" "f x ∈ carrier (G⦇carrier := H⦈)" using i(4) by auto
qed
ultimately show ?case by simp
qed
next
case False
then show ?thesis unfolding finprod_def by simp
qed

lemma (in comm_group) finprod_closed_subgroup:
assumes "subgroup H G" "f ∈ A → H"
shows "finprod G f A ∈ H"
using assms(2)
proof (induct A rule: infinite_finite_induct)
case (infinite A)
then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
case empty
then show ?case using subgroup.one_closed[OF assms(1)] by auto
next
case i: (insert x F)
from finprod_insert[OF i(1, 2), of f] i have fi: "finprod G f (insert x F) = f x ⊗ finprod G f F"
using subgroup.subset[OF assms(1)] by blast
from i have "finprod G f F ∈ H" "f x ∈ H" by blast+
with fi show ?case using subgroup.m_closed[OF assms(1)] by presburger
qed

text ‹It also does not matter if we exponentiate all elements taking part in the product or the
result of the product.›

lemma (in comm_group) finprod_exp:
assumes "A ⊆ carrier G" "f ∈ A → carrier G"
shows "(finprod G f A) [^] (k::int) = finprod G ((λa. a [^] k) ∘ f) A"
using assms
proof(induction A rule: infinite_finite_induct)
case i: (insert x F)
hence ih: "finprod G f F [^] k = finprod G ((λa. a [^] k) ∘ f) F" by blast
have fpc: "finprod G f F ∈ carrier G" by (intro finprod_closed, use i in auto)
have fxc: "f x ∈ carrier G" using i by auto
have "finprod G f (insert x F) = f x ⊗ finprod G f F" by (intro finprod_insert, use i in auto)
hence "finprod G f (insert x F) [^] k = (f x ⊗ finprod G f F) [^] k" by simp
also have "… = f x [^] k ⊗ finprod G f F [^] k" using fpc fxc int_pow_distrib by blast
also have "… = ((λa. a [^] k) ∘ f) x ⊗ finprod G ((λa. a [^] k) ∘ f) F" using ih by simp
also have "… = finprod G ((λa. a [^] k) ∘ f) (insert x F)"
by (intro finprod_insert[symmetric], use i in auto)
finally show ?case .
qed auto

text ‹Some lemmas concerning different combinations of functions in the usage of ‹finprod›.›

lemma (in comm_group) finprod_cong_split:
assumes "⋀a. a ∈ A ⟹ f a ⊗ g a = h a"
and "f ∈ A → carrier G" "g ∈ A → carrier G" "h ∈ A → carrier G"
shows "finprod G h A = finprod G f A ⊗ finprod G g A" using assms
proof(induct A rule: infinite_finite_induct)
case (infinite A)
then show ?case by simp
next
case empty
then show ?case by simp
next
case i: (insert x F)
then have iH: "finprod G h F = finprod G f F ⊗ finprod G g F" by fast
have f: "finprod G f (insert x F) = f x ⊗ finprod G f F"
by (intro finprod_insert[OF i(1, 2), of f]; use i(5) in simp)
have g: "finprod G g (insert x F) = g x ⊗ finprod G g F"
by (intro finprod_insert[OF i(1, 2), of g]; use i(6) in simp)
have h: "finprod G h (insert x F) = h x ⊗ finprod G h F"
by (intro finprod_insert[OF i(1, 2), of h]; use i(7) in simp)
also have "… = h x ⊗ (finprod G f F ⊗ finprod G g F)" using iH by argo
also have "… = f x ⊗ g x ⊗ (finprod G f F ⊗ finprod G g F)" using i(4) by simp
also have "… = f x ⊗ finprod G f F ⊗ (g x ⊗ finprod G g F)" using m_comm m_assoc i(5-7) by simp
also have "… = finprod G f (insert x F) ⊗ finprod G g (insert x F)" using f g by argo
finally show ?case .
qed

lemma (in comm_group) finprod_comp:
assumes "inj_on g A" "(f ∘ g)  A ⊆ carrier G"
shows "finprod G f (g  A) = finprod G (f ∘ g) A"
using finprod_reindex[OF _ assms(1), of f] using assms(2) unfolding comp_def by blast

text ‹The subgroup generated by a set of generators (in an abelian group) is exactly the set of
elements that can be written as a finite product using only powers of these elements.›

lemma (in comm_group) generate_eq_finprod_PiE_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G x gs)  Pi⇩E gs (λa. generate G {a})" (is "?g = ?fp")
proof
show "?g ⊆ ?fp"
proof
fix x
assume x: "x ∈ ?g"
thus "x ∈ ?fp"
proof (induction rule: generate.induct)
case one
show ?case
proof
let ?r = "restrict (λ_. 𝟭) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one by auto
show "𝟭 = finprod G ?r gs" by(intro finprod_one_eqI[symmetric], simp)
qed
next
case g: (incl g)
show ?case
proof
let ?r = "restrict ((λ_. 𝟭)(g := g)) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one generate.incl[of g "{g}" G]
by fastforce
show "g = finprod G ?r gs"
proof -
have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})"
by (intro finprod_minus, use assms g in auto)
moreover have "?r g = g" using g by simp
moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
ultimately show ?thesis using assms g by auto
qed
qed
next
case g: (inv g)
show ?case
proof
let ?r = "restrict ((λ_. 𝟭)(g := inv g)) gs"
show "?r ∈ (Π⇩E a∈gs. generate G {a})" using generate.one generate.inv[of g "{g}" G]
by fastforce
show "inv g = finprod G ?r gs"
proof -
have "finprod G ?r gs = ?r g ⊗ finprod G ?r (gs - {g})"
by (intro finprod_minus, use assms g in auto)
moreover have "?r g = inv g" using g by simp
moreover have "finprod G ?r (gs - {g}) = 𝟭" by(rule finprod_one_eqI; use g in simp)
ultimately show ?thesis using assms g by auto
qed
qed
next
case gh: (eng g h)
from gh obtain i where i: "i ∈ (Π⇩E a∈gs. generate G {a})" "g = finprod G i gs" by blast
from gh obtain j where j: "j ∈ (Π⇩E a∈gs. generate G {a})" "h = finprod G j gs" by blast
from i j have "g ⊗ h = finprod G i gs ⊗ finprod G j gs" by blast
also have "… = finprod G (λa. i a ⊗ j a) gs"
proof(intro finprod_multf[symmetric]; rule)
fix x
assume x: "x ∈ gs"
have "i x ∈ generate G {x}" "j x ∈ generate G {x}"using i(1) j(1) x by blast+
thus "i x ∈ carrier G" "j x ∈ carrier G" using generate_incl[of "{x}"] x assms(2) by blast+
qed
also have "… = finprod G (restrict (λa. i a ⊗ j a) gs) gs"
proof(intro finprod_cong)
have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto
have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto
have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g
using generate.eng[OF ip[OF that] jp[OF that]] .
thus "((λa. i a ⊗ j a) ∈ gs → carrier G) = True" using generate_incl assms(2) by blast
qed auto
finally have "g ⊗ h = finprod G (restrict (λa. i a ⊗ j a) gs) gs" .
moreover have "(restrict (λa. i a ⊗ j a) gs) ∈ (Π⇩E a∈gs. generate G {a})"
proof -
have ip: "i g ∈ generate G {g}" if "g ∈ gs" for g using i that by auto
have jp: "j g ∈ generate G {g}" if "g ∈ gs" for g using j that by auto
have "i g ⊗ j g ∈ generate G {g}" if "g ∈ gs" for g
using generate.eng[OF ip[OF that] jp[OF that]] .
thus ?thesis by auto
qed
ultimately show ?case using i j by blast
qed
qed
show "?fp ⊆ ?g"
proof
fix x
assume x: "x ∈ ?fp"
then obtain f where f: "f ∈ (Pi⇩E gs (λa. generate G {a}))" "x = finprod G f gs" by blast
have sg: "subgroup ?g G" by(intro generate_is_subgroup, fact)
have "finprod G f gs ∈ ?g"
proof(intro finprod_closed_subgroup[OF sg])
have "f g ∈ generate G gs" if "g ∈ gs" for g
proof -
have "f g ∈ generate G {g}" using f(1) that by auto
moreover have "generate G {g} ⊆ generate G gs" by(intro mono_generate, use that in simp)
ultimately show ?thesis by fast
qed
thus "f ∈ gs → generate G gs" by simp
qed
thus "x ∈ ?g" using f by blast
qed
qed

lemma (in comm_group) generate_eq_finprod_Pi_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G x gs)  Pi gs (λa. generate G {a})" (is "?g = ?fp")
proof -
have "(λx. finprod G x gs)  Pi⇩E gs (λa. generate G {a})
= (λx. finprod G x gs)  Pi gs (λa. generate G {a})"
proof
have "Pi⇩E gs (λa. generate G {a}) ⊆ Pi gs (λa. generate G {a})" by blast
thus "(λx. finprod G x gs)  Pi⇩E gs (λa. generate G {a})
⊆ (λx. finprod G x gs)  Pi gs (λa. generate G {a})" by blast
show "(λx. finprod G x gs)  Pi gs (λa. generate G {a})
⊆ (λx. finprod G x gs)  Pi⇩E gs (λa. generate G {a})"
proof
fix x
assume x: "x ∈ (λx. finprod G x gs)  Pi gs (λa. generate G {a})"
then obtain f where f: "x = finprod G f gs" "f ∈ Pi gs (λa. generate G {a})" by blast
moreover have "finprod G f gs = finprod G (restrict f gs) gs"
proof(intro finprod_cong)
have "f g ∈ carrier G" if "g ∈ gs" for g
using that f(2) mono_generate[of "{g}" gs] generate_incl[OF assms(2)] by fast
thus "(f ∈ gs → carrier G) = True" by blast
qed auto
moreover have "restrict f gs ∈ Pi⇩E gs (λa. generate G {a})" using f(2) by simp
ultimately show "x ∈ (λx. finprod G x gs)  Pi⇩E gs (λa. generate G {a})" by blast
qed
qed
with generate_eq_finprod_PiE_image[OF assms] show ?thesis by auto
qed

lemma (in comm_group) generate_eq_finprod_Pi_int_image:
assumes "finite gs" "gs ⊆ carrier G"
shows "generate G gs = (λx. finprod G (λg. g [^] x g) gs)  Pi gs (λ_. (UNIV::int set))"
proof -
from generate_eq_finprod_Pi_image[OF assms]
have "generate G gs = (λx. finprod G x gs)  (Π a∈gs. generate G {a})" .
also have "… = (λx. finprod G (λg. g [^] x g) gs)  Pi gs (λ_. (UNIV::int set))"
proof(rule; rule)
fix x
assume x: "x ∈ (λx. finprod G x gs)  (Π a∈gs. generate G {a})"
then obtain f where f: "f ∈ (Π a∈gs. generate G {a})" "x = finprod G f gs" by blast
hence "∃k::int. f a = a [^] k" if "a ∈ gs" for a using generate_pow[of a] that assms(2) by blast
hence "∃(h::'a ⇒ int). ∀a∈gs. f a = a [^] h a" by meson
then obtain h where h: "∀a∈gs. f a = a [^] h a" "h ∈ gs → (UNIV :: int set)" by auto
have "finprod G (λg. g [^] h g) gs = finprod G f gs"
by (intro finprod_cong, use int_pow_closed h assms(2) in auto)
with f have "x = finprod G (λg. g [^] h g) gs" by argo
with h(2) show "x ∈ (λx. finprod G (λg. g [^] x g) gs)  (gs → (UNIV::int set))" by auto
next
fix x
assume x: "x ∈ (λx. finprod G (λg. g [^] x g) gs)  (gs → (UNIV::int set))"
then obtain h where h: "x = finprod G (λg. g [^] h g) gs" "h ∈ gs → (UNIV :: int set)" by blast
hence "∃k∈generate G {a}. a [^] h a = k" if "a ∈ gs" for a
using generate_pow[of a] that assms(2) by blast
then obtain f where f: "∀a∈gs. a [^] h a = f a" "f ∈ (Π a∈gs. generate G {a})" by fast
have "finprod G f gs = finprod G (λg. g [^] h g) gs"
proof(intro finprod_cong)
have "f a ∈ carrier G" if "a ∈ gs" for a
using generate_incl[of "{a}"] assms(2) that f(2) by fast
thus "(f ∈ gs → carrier G) = True" by blast
qed (use f in auto)
with h have "x = finprod G f gs" by argo
with f(2) show "x ∈ (λx. finprod G x gs)  (Π a∈gs. generate G {a})" by blast
qed
finally show ?thesis .
qed

lemma (in comm_group) IDirProds_eq_finprod_PiE:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "IDirProds G S I = (λx. finprod G x I)  (Pi⇩E I S)" (is "?DP = ?fp")
proof
show "?fp ⊆ ?DP"
proof
fix x
assume x: "x ∈ ?fp"
then obtain f where f: "f ∈ (Pi⇩E I S)" "x = finprod G f I" by blast
have sDP: "subgroup ?DP G"
by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
have "finprod G f I ∈ ?DP"
proof(intro finprod_closed_subgroup[OF sDP])
have "f i ∈ IDirProds G S I" if "i ∈ I" for i
proof
show "f i ∈ (S i)" using f(1) that by auto
show "(S i) ⊆ IDirProds G S I" by (intro IDirProds_incl[OF that])
qed
thus "f ∈ I → IDirProds G S I" by simp
qed
thus "x ∈ ?DP" using f by blast
qed
show "?DP ⊆ ?fp"
proof(unfold IDirProds_def; rule subsetI)
fix x
assume x: "x ∈ generate G (⋃(S  I))"
thus "x ∈ ?fp" using assms
proof (induction rule: generate.induct)
case one
define g where g: "g = (λx. if x ∈ I then 𝟭 else undefined)"
then have "g ∈ Pi⇩E I S"
using subgroup.one_closed[OF one(2)] by auto
moreover have "finprod G g I = 𝟭" by (intro finprod_one_eqI; use g in simp)
ultimately show ?case unfolding image_def by (auto; metis)
next
case i: (incl h)
from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast
define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := h)"
with j have "hf ∈ Pi⇩E I S"
using subgroup.one_closed[OF i(3)] by force
moreover have "finprod G hf I = h"
proof -
have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})"
by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
moreover have "hf j = h" using hf_def by simp
moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
qed
ultimately show ?case unfolding image_def by (auto; metis)
next
case i: (inv h)
from i obtain j where j: "j ∈ I" "h ∈ (S j)" by blast
have ih: "inv h ∈ (S j)" using subgroup.m_inv_closed[OF i(3)[OF j(1)] j(2)] .
define hf where "hf = (λx. (if x ∈ I then 𝟭 else undefined))(j := inv h)"
with j ih have "hf ∈ Pi⇩E I S"
using subgroup.one_closed[OF i(3)] by force
moreover have "finprod G hf I = inv h"
proof -
have "finprod G hf I = hf j ⊗ finprod G hf (I - {j})"
by (intro finprod_minus, use assms hf_def subgroup.subset[OF i(3)[OF j(1)]] j in auto)
moreover have "hf j = inv h" using hf_def by simp
moreover have "finprod G hf (I - {j}) = 𝟭" by (rule finprod_one_eqI; use hf_def in simp)
ultimately show ?thesis using subgroup.subset[OF i(3)[OF j(1)]] j(2) by auto
qed
ultimately show ?case unfolding image_def by (auto; metis)
next
case e: (eng a b)
from e obtain f where f: "f ∈ Pi⇩E I S" "a = finprod G f I" by blast
from e obtain g where g: "g ∈ Pi⇩E I S" "b = finprod G g I" by blast
from f g have "a ⊗ b = finprod G f I ⊗ finprod G g I" by blast
also have "… = finprod G (λa. f a ⊗ g a) I"
proof(intro finprod_multf[symmetric])
have "⋃(S  I) ⊆ carrier G" using subgroup.subset[OF e(6)] by blast
thus "f ∈ I → carrier G" "g ∈ I → carrier G"
using f(1) g(1) unfolding PiE_def Pi_def by auto
qed
also have "… = finprod G (restrict (λa. f a ⊗ g a) I) I"
proof(intro finprod_cong)
show "I = I" by simp
show "⋀i. i ∈ I =simp=> f i ⊗ g i = (λa∈I. f a ⊗ g a) i" by simp
have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto
have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto
have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i
using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
thus "((λa. f a ⊗ g a) ∈ I → carrier G) = True" using subgroup.subset[OF e(6)] by auto
qed
finally have "a ⊗ b = finprod G (restrict (λa. f a ⊗ g a) I) I" .
moreover have "(restrict (λa. f a ⊗ g a) I) ∈ Pi⇩E I S"
proof -
have fp: "f i ∈ (S i)" if "i ∈ I" for i using f that by auto
have gp: "g i ∈ (S i)" if "i ∈ I" for i using g that by auto
have "f i ⊗ g i ∈ (S i)" if "i ∈ I" for i
using subgroup.m_closed[OF e(6)[OF that] fp[OF that] gp[OF that]] .
thus ?thesis by auto
qed
ultimately show ?case using f g by blast
qed
qed
qed

lemma (in comm_group) IDirProds_eq_finprod_Pi:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "IDirProds G S I = (λx. finprod G x I)  (Pi I S)" (is "?DP = ?fp")
proof -
have "(λx. finprod G x I)  (Pi I S) = (λx. finprod G x I)  (Pi⇩E I S)"
proof
have "Pi⇩E I S ⊆ Pi I S" by blast
thus "(λx. finprod G x I)  Pi⇩E I S ⊆ (λx. finprod G x I)  Pi I S" by blast
show "(λx. finprod G x I)  Pi I S ⊆ (λx. finprod G x I)  Pi⇩E I S"
proof
fix x
assume x: "x ∈ (λx. finprod G x I)  Pi I S"
then obtain f where f: "x = finprod G f I" "f ∈ Pi I S" by blast
moreover have "finprod G f I = finprod G (restrict f I) I"
by (intro finprod_cong; use f(2) subgroup.subset[OF assms(2)] in fastforce)
moreover have "restrict f I ∈ Pi⇩E I S" using f(2) by simp
ultimately show "x ∈ (λx. finprod G x I)  Pi⇩E I S" by blast
qed
qed
with IDirProds_eq_finprod_PiE[OF assms] show ?thesis by auto
qed

text ‹If we switch one element from a set of generators, the generated set stays the same if both
elements can be generated from the others together with the switched element respectively.›

lemma (in comm_group) generate_one_switched_exp_eqI:
assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}"
and "f ∈ A → (UNIV::int set)" "g ∈ B → (UNIV::int set)"
and "a = finprod G (λx. x [^] g x) B" "b = finprod G (λx. x [^] f x) A"
shows "generate G A = generate G B"
proof(intro generate_one_switched_eqI[OF assms(1, 2, 3)]; cases "finite A")
case True
hence fB: "finite B" using assms(3) by blast
have cB: "B ⊆ carrier G"
proof -
have "b ∈ carrier G"
by (subst assms(7), intro finprod_closed, use assms(1, 4) int_pow_closed in fast)
thus ?thesis using assms(1, 3) by blast
qed
show "a ∈ generate G B"
proof(subst generate_eq_finprod_Pi_image[OF fB cB], rule)
show "a = finprod G (λx. x [^] g x) B" by fact
have "x [^] g x ∈ generate G {x}" if "x ∈ B" for x using generate_pow[of x] cB that by blast
thus "(λx. x [^] g x) ∈ (Π a∈B. generate G {a})" unfolding Pi_def by blast
qed
show "b ∈ generate G A"
proof(subst generate_eq_finprod_Pi_image[OF True assms(1)], rule)
show "b = finprod G (λx. x [^] f x) A" by fact
have "x [^] f x ∈ generate G {x}" if "x ∈ A" for x
using generate_pow[of x] assms(1) that by blast
thus "(λx. x [^] f x) ∈ (Π a∈A. generate G {a})" unfolding Pi_def by blast
qed
next
case False
hence b: "b = 𝟭" using assms(7) unfolding finprod_def by simp
from False assms(3) have "infinite B" by simp
hence a: "a = 𝟭" using assms(6) unfolding finprod_def by simp
show "a ∈ generate G B" using generate.one a by blast
show "b ∈ generate G A" using generate.one b by blast
qed

text ‹We can characterize a complementary family of subgroups when the only way to form the neutral
element as a product of picked elements from each subgroup is to pick the neutral element from each
subgroup.›

lemma (in comm_group) compl_fam_imp_triv_finprod:
assumes "compl_fam S I" "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
and "finprod G f I = 𝟭" "f ∈ Pi I S"
shows "∀i∈I. f i = 𝟭"
proof (rule ccontr; clarify)
from assms(5) have f: "f i ∈ (S i)" if "i ∈ I" for i using that by fastforce
fix i
assume i: "i ∈ I"
have si: "subgroup (S i) G" using assms(3)[OF i] .
consider (triv) "(S i) = {𝟭}" | (not_triv) "(S i) ≠ {𝟭}" by blast
thus "f i = 𝟭"
proof (cases)
case triv
then show ?thesis using f[OF i] by blast
next
case not_triv
show ?thesis
proof (rule ccontr)
have fc: "f i ∈ carrier G" using f[OF i] subgroup.subset[OF si] by blast
assume no: "f i ≠ 𝟭"
have fH: "f i ∈ (S i)" using f[OF i] .
from subgroup.m_inv_closed[OF si this] have ifi: "inv (f i) ∈ (S i)" .
moreover have "inv (f i) ≠ 𝟭" using no fc by simp
moreover have "inv (f i) = finprod G f (I - {i})"
proof -
have "𝟭 = finprod G f I" using assms(4) by simp
also have "… = finprod G f (insert i (I - {i}))"
proof -
have "I = insert i (I - {i})" using i by fast
thus ?thesis by simp
qed
also have "… = f i ⊗ finprod G f (I - {i})"
proof(intro finprod_insert)
show "finite (I - {i})" using assms(2) by blast
show "i ∉ I - {i}" by blast
show "f ∈ I - {i} → carrier G" using assms(3) f subgroup.subset by blast
show "f i ∈ carrier G" by fact
qed
finally have o: "𝟭 = f i ⊗ finprod G f (I - {i})" .
show ?thesis
proof(intro inv_equality)
show "f i ∈ carrier G" by fact
show "finprod G f (I - {i}) ∈ carrier G"
by (intro finprod_closed; use assms(3) f subgroup.subset in blast)
from m_comm[OF this fc] o show "finprod G f (I - {i}) ⊗ f i = 𝟭" by simp
qed
qed
moreover have "finprod G f (I - {i}) ∈ IDirProds G S (I - {i})"
proof (intro finprod_closed_subgroup IDirProds_is_subgroup)
show "⋃ (S  (I - {i})) ⊆ carrier G" using assms(3) subgroup.subset by auto
have "f j ∈ (IDirProds G S (I - {i}))" if "j ∈ (I - {i})" for j
using IDirProds_incl[OF that] f that by blast
thus "f ∈ I - {i} → IDirProds G S (I - {i})" by blast
qed
ultimately have "¬complementary (S i) (IDirProds G S (I - {i}))"
unfolding complementary_def by auto
thus False using assms(1) i unfolding compl_fam_def by blast
qed
qed
qed

lemma (in comm_group) triv_finprod_imp_compl_fam:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
and "∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
shows "compl_fam S I"
proof (unfold compl_fam_def; rule)
fix k
assume k: "k ∈ I"
let ?DP = "IDirProds G S (I - {k})"
show "complementary (S k) ?DP"
proof (rule ccontr; unfold complementary_def)
have sk: "subgroup (S k) G" using assms(2)[OF k] .
have sDP: "subgroup ?DP G"
by (intro IDirProds_is_subgroup; use subgroup.subset[OF assms(2)] in blast)
assume a: "(S k) ∩ IDirProds G S (I - {k}) ≠ {𝟭}"
then obtain x where x: "x ∈ (S k)" "x ∈ IDirProds G S (I - {k})" "x ≠ 𝟭"
using subgroup.one_closed sk sDP by blast
then have "x ∈ (λx. finprod G x (I - {k}))  (Pi (I - {k}) S)"
using IDirProds_eq_finprod_Pi[of "(I - {k})"] assms(1, 2) by blast
then obtain ht where ht: "finprod G ht (I - {k}) = x" "ht ∈ Pi (I - {k}) S" by blast
define h where h: "h = (ht(k := inv x))"
then have hPi: "h ∈ Pi I S" using ht subgroup.m_inv_closed[OF assms(2)[OF k] x(1)] by auto
have "finprod G h (I - {k}) = x"
proof (subst ht(1)[symmetric], intro finprod_cong)
show "I - {k} = I - {k}" by simp
show "(h ∈ I - {k} → carrier G) = True" using h ht(2) subgroup.subset[OF assms(2)]
unfolding Pi_def id_def by auto
show "⋀i. i ∈ I - {k} =simp=> h i = ht i" using ht(2) h by simp
qed
moreover have "finprod G h I = h k ⊗ finprod G h (I - {k})"
by (intro finprod_minus; use k assms hPi subgroup.subset[OF assms(2)] Pi_def in blast)
ultimately have "finprod G h I = inv x ⊗ x" using h by simp
then have "finprod G h I = 𝟭" using subgroup.subset[OF sk] x(1) by auto
moreover have "h k ≠ 𝟭" using h x(3) subgroup.subset[OF sk] x(1) by force
ultimately show False using assms(3) k hPi by blast
qed
qed

lemma (in comm_group) triv_finprod_iff_compl_fam_Pi:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "compl_fam S I ⟷ (∀f ∈ Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))"
using compl_fam_imp_triv_finprod triv_finprod_imp_compl_fam assms by blast

lemma (in comm_group) triv_finprod_iff_compl_fam_PiE:
assumes "finite I" "⋀i. i ∈ I ⟹ subgroup (S i) G"
shows "compl_fam S I ⟷ (∀f ∈ Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭))"
proof
show "compl_fam S I ⟹ ∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
using triv_finprod_iff_compl_fam_Pi[OF assms] by auto
have "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)
⟹ ∀f∈Pi I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
proof(rule+)
fix f i
assume f: "f ∈ Pi I S" "finprod G f I = 𝟭" and i: "i ∈ I"
assume allf: "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭)"
have "f i = restrict f I i" using i by simp
moreover have "finprod G (restrict f I) I = finprod G f I"
using f subgroup.subset[OF assms(2)] unfolding Pi_def by (intro finprod_cong; auto)
moreover have "restrict f I ∈ Pi⇩E I S" using f by simp
ultimately show "f i = 𝟭" using allf f i by metis
qed
thus "∀f∈Pi⇩E I S. finprod G f I = 𝟭 ⟶ (∀i∈I. f i = 𝟭) ⟹ compl_fam S I"
using triv_finprod_iff_compl_fam_Pi[OF assms] by presburger
qed

text ‹The finite product also distributes when nested.›

(* Manuel Eberl, TODO: move to library *)
lemma (in comm_monoid) finprod_Sigma:
assumes "finite A" "⋀x. x ∈ A ⟹ finite (B x)"
assumes "⋀x y. x ∈ A ⟹ y ∈ B x ⟹ g x y ∈ carrier G"
shows   "(⨂x∈A. ⨂y∈B x. g x y) = (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)"
using assms
proof (induction A rule: finite_induct)
case (insert x A)
have "(⨂z∈Sigma (insert x A) B. case z of (x, y) ⇒ g x y) =
(⨂z∈Pair x  B x. case z of (x, y) ⇒ g x y) ⊗ (⨂z∈Sigma A B. case z of (x, y) ⇒ g x y)"
unfolding Sigma_insert using insert.prems insert.hyps
by (subst finprod_Un_disjoint) auto
also have "(⨂z∈Sigma A B. case z of (x, y) ⇒ g x y) = (⨂x∈A. ⨂y∈B x. g x y)"
using insert.prems insert.hyps by (subst insert.IH [symmetric]) auto
also have "(⨂z∈Pair x  B x. case z of (x, y) ⇒ g x y) = (⨂y∈B x. g x y)"
using insert.prems insert.hyps by (subst finprod_reindex) (auto intro: inj_onI)
finally show ?case
using insert.hyps insert.prems by simp
qed auto

text ‹With the now proven facts, we are able to provide criterias to inductively construct a
group that is the internal direct product of a set of generators.›

(* belongs to IDirProd, but uses finprod stuff *)
lemma (in comm_group) idirprod_generate_ind:
assumes "finite gs" "gs ⊆ carrier G" "g ∈ carrier G"
"is_idirprod (generate G gs) (λg. generate G {g}) gs"
"complementary (generate G {g}) (generate G gs)"
shows "is_idirprod (generate G (gs ∪ {g})) (λg. generate G {g}) (gs ∪ {g})"
proof(cases "g ∈ gs")
case True
hence "gs = (gs ∪ {g})" by blast
thus ?thesis using assms(4) by auto
next
case gngs: False
show ?thesis
proof (intro is_idirprod_subgroup_suffices)
have gsgc: "gs ∪ {g} ⊆ carrier G" using assms(2, 3) by blast
thus "generate G (gs ∪ {g}) = IDirProds G (λg. generate G {g}) (gs ∪ {g})"
unfolding IDirProds_def using generate_idem_Un by presburger
show "∀i∈gs ∪ {g}. subgroup (generate G {i}) G" using generate_is_subgroup gsgc by auto
have sg: "subgroup (generate G {g}) G" by (intro generate_is_subgroup, use assms(3) in blast)
from assms(4) is_idirprod_def have ih: "∀x. x ∈ gs ⟶ generate G {x} ⊲ G"
"compl_fam (λg. generate G {g}) gs"
by fastforce+
hence ca: "complementary (generate G {a}) (generate G (gs - {a}))" if "a ∈ gs" for a
unfolding compl_fam_def IDirProds_def
using gsgc generate_idem_Un[of "gs - {a}"] that by fastforce
have aux: "gs ∪ {g} - {i} ⊆ carrier G" for i using gsgc by blast
show "compl_fam (λg. generate G {g}) (gs ∪ {g})"
proof(unfold compl_fam_def IDirProds_def, subst generate_idem_Un[OF aux],
rule, rule ccontr)
fix h
assume h: "h ∈ gs ∪ {g}"
assume c: "¬ complementary (generate G {h}) (generate G (gs ∪ {g} - {h}))"
show "False"
proof (cases "h = g")
case True
with c have "¬ complementary (generate G {g}) (generate G (gs - {g}))" by auto
moreover have "complementary (generate G {g}) (generate G (gs - {g}))"
by (rule subgroup_subset_complementary[OF generate_is_subgroup generate_is_subgroup[of gs]
generate_is_subgroup mono_generate], use assms(2, 3, 5) in auto)
ultimately show False by blast
next
case hng: False
hence h: "h ∈ gs" "h ≠ g" using h by blast+
hence "gs ∪ {g} - {h} = gs - {h} ∪ {g}" by blast
with c have c: "¬ complementary (generate G {h}) (generate G (gs - {h} ∪ {g}))" by argo
then obtain k where k: "k ∈ generate G {h}" "k ∈ generate G (gs - {h} ∪ {g})" "k ≠ 𝟭"
unfolding complementary_def using generate.one by blast
with ca have kngh: "k ∉ generate G (gs - {h})" using h unfolding complementary_def by blast
from k(2) generate_eq_finprod_PiE_image[of "gs - {h} ∪ {g}"] assms(1) gsgc
obtain f where f:
"k = finprod G f (gs - {h} ∪ {g})" "f ∈ (Π⇩E a∈gs - {h} ∪ {g}. generate G {a})"
by blast
have fg: "f a ∈ generate G {a}" if "a ∈ (gs - {h} ∪ {g})" for a using that f(2) by blast
have fc: "f a ∈ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a
proof -
have "generate G {a} ⊆ carrier G" if "a ∈ (gs - {h} ∪ {g})" for a
using that generate_incl[of "{a}"] gsgc by blast
thus "f a ∈ carrier G" using that fg by auto
qed
have kp: "k = f g ⊗ finprod G f (gs - {h})"
proof -
have "(gs - {h} ∪ {g}) = insert g (gs - {h})" by fast
moreover have "finprod G f (insert g (gs - {h})) = f g ⊗ finprod G f (gs - {h})"
by (intro finprod_insert, use fc assms(1) gngs in auto)
ultimately show ?thesis using f(1) by argo
qed
have fgsh: "finprod G f (gs - {h}) ∈ generate G (gs - {h})"
proof(intro finprod_closed_subgroup[OF generate_is_subgroup])
show "gs - {h} ⊆ carrier G" using gsgc by blast
have "f a ∈ generate G (gs - {h})" if "a ∈ (gs - {h})" for a
using mono_generate[of "{a}" "gs - {h}"] fg that by blast
thus "f ∈ gs - {h} → generate G (gs - {h})" by blast
qed
have "f g ⊗ finprod G f (gs - {h}) ∉ generate G gs"
proof
assume fpgs: "f g ⊗ finprod G f (gs - {h}) ∈ generate G gs"
from fgsh have fgsgs: "finprod G f (gs - {h}) ∈ generate G gs"
using mono_generate[of "gs - {h}" gs] by blast
have fPi: "f ∈ (Π a∈(gs - {h}). generate G {a})" using f by blast
have gI: "generate G (gs - {h})
= (λx. finprod G x (gs - {h}))  (Π a∈gs - {h}. generate G {a})"
using generate_eq_finprod_Pi_image[of "gs - {h}"] assms(1, 2) by blast
have fgno: "f g ≠ 𝟭"
proof (rule ccontr)
assume o: "¬ f g ≠ 𝟭"
hence kf: "k = finprod G f (gs - {h})" using kp finprod_closed fc by auto
hence "k ∈ generate G (gs - {h})" using fPi gI by blast
thus False using k ca h unfolding complementary_def by blast
qed
from fpgs have "f g ∈ generate G gs"
using subgroup.mult_in_cancel_right[OF generate_is_subgroup[OF assms(2)] fc[of g] fgsgs]
by blast
with fgno assms(5) fg[of g] show "False" unfolding complementary_def by blast
qed
moreover have "k ∈ generate G gs" using k(1) mono_generate[of "{h}" gs] h(1) by blast
ultimately show False using kp by blast
qed
qed
qed
qed

end

# Theory Group_Hom

(*
File:     Group_Hom.thy
Author:   Joseph Thommes, TU München
*)
section ‹Group Homomorphisms›

theory Group_Hom
imports Set_Multiplication
begin

text ‹This section extends the already existing library about group homomorphisms in HOL-Algebra by
some useful lemmas. These were mainly inspired by the needs that arised throughout the other proofs.›

lemma (in group_hom) generate_hom:
assumes "A ⊆ carrier G"
shows "h  (generate G A) = generate H (h  A)"
using assms group_hom.generate_img group_hom_axioms by blast

text ‹For two elements with the same image we can find an element in the kernel that maps one of the
two elements on the other by multiplication.›

lemma (in group_hom) kernel_assoc_elem:
assumes "x ∈ carrier G" "y ∈ carrier G" "h x = h y"
obtains z where "x = y ⊗⇘G⇙ z" "z ∈ kernel G H h"
proof -
have c: "inv y ⊗⇘G⇙ x ∈ carrier G" using assms by simp
then have e: "x = y ⊗⇘G⇙ (inv y ⊗⇘G⇙ x)" using assms G.m_assoc
using G.inv_solve_left by blast
then have "h x = h (y ⊗⇘G⇙ (inv y ⊗⇘G⇙ x))" by simp
then have "h x = h y ⊗⇘H⇙ h (inv y ⊗⇘G⇙ x)" using c assms by simp
then have "𝟭⇘H⇙ = h (inv y ⊗⇘G⇙ x)" using assms by simp
then have "(inv y ⊗⇘G⇙ x) ∈ kernel G H h" unfolding kernel_def using c by simp
thus ?thesis using e that by blast
qed

text ‹This can then be used to characterize the pre-image of a set $A$ under homomorphism as a
product of $A$ itself with the kernel of the homomorphism.›

lemma (in group_hom) vimage_eq_set_mult_kern_right:
assumes "A ⊆ carrier G"
shows "{x ∈ carrier G. h x ∈ h  A} = A <#> kernel G H h"
proof(intro equalityI subsetI)
fix x
assume assm: "x ∈ A <#> kernel G H h"
then have xc: "x ∈ carrier G" unfolding kernel_def set_mult_def using assms by blast
from assm obtain a b where ab: "a ∈ A" "b ∈ kernel G H h" "x = a ⊗⇘G⇙ b"
unfolding set_mult_def by blast
then have abc: "a ∈ carrier G" "b ∈ carrier G" unfolding kernel_def using assms by auto
from ab have "h x = h (a ⊗⇘G⇙ b)" by blast
also have "… = h a ⊗⇘H⇙ h b" using abc by simp
also have "… = h a ⊗⇘H⇙ 𝟭⇘H⇙" using ab(2) unfolding kernel_def by simp
also have "… = h a" using abc by simp
also have "… ∈ h  A" using ab by blast
finally have "h x ∈ h  A" .
thus "x ∈ {x ∈ carrier G. h x ∈ h  A}" using xc by blast
next
fix x
assume "x ∈ {x ∈ carrier G. h x ∈ h  A}"
then have x: "x ∈ carrier G" "h x ∈ h  A" by simp+
then obtain y where y: "y ∈ A" "h x = h y" "y ∈ carrier G" using assms by auto
with kernel_assoc_elem obtain z where "x = y ⊗⇘G⇙ z" "z ∈ kernel G H h" using x by metis
thus "x ∈ A <#> kernel G H h" unfolding set_mult_def using y by blast
qed

lemma (in group_hom) vimage_subset_generate_kern:
assumes "A ⊆ carrier G"
shows "{x ∈ carrier G. h x ∈ h  A} ⊆ generate G (A ∪ kernel G H h)"
using vimage_eq_set_mult_kern_right[of A] G.set_mult_subset_generate[of "A" "kernel G H h"] assms
unfolding kernel_def by blast

text ‹The preimage of a subgroup under a homomorphism is also a subgroup.›

lemma (in group_hom) subgroup_vimage_is_subgroup:
assumes "subgroup I H"
shows "subgroup {x ∈ carrier G. h x ∈ I} G" (is "subgroup ?J G")
proof
show "?J ⊆ carrier G" by blast
show "𝟭 ∈ ?J" using subgroup.one_closed[of I H] assms by simp
fix x
assume x: "x ∈ ?J"
then have hx: "h x ∈ I" by blast
show "inv x ∈ ?J"
proof -
from hx have "inv⇘H⇙ (h x) ∈ I" using subgroup.m_inv_closed assms by fast
moreover have "inv x ∈ carrier G" using x by simp
moreover have "inv⇘H⇙ (h x) = h (inv x)" using x by auto
ultimately show "inv x ∈ ?J" by simp
qed
fix y
assume y: "y ∈ ?J"
then have hy: "h y ∈ I" by blast
show "x ⊗ y ∈ {x ∈ carrier G. h x ∈ I}"
proof -
have "h (x ⊗ y) = h x ⊗⇘H⇙ h y" using x y by simp
also have "… ∈ I" using hx hy assms subgroup.m_closed by fast
finally have "h (x ⊗ y) ∈ I" .
moreover have "x ⊗ y ∈ carrier G" using x y by simp
ultimately show ?thesis by blast
qed
qed

lemma (in group_hom) iso_kernel:
assumes "h ∈ iso G H"
shows "kernel G H h = {𝟭⇘G⇙}"
unfolding kernel_def using assms
using hom_one iso_iff by blast

✐‹contributor ‹Paulo Emílio de Vilhena›› (* adapted by Joseph Thommes *)
lemma (in group_hom) induced_group_hom_same_group:
assumes "subgroup I G"
shows "group_hom (G ⦇ carrier := I ⦈) H h"
proof -
have "h ∈ hom (G ⦇ carrier := I ⦈) H"
using homh subgroup.mem_carrier[OF assms] unfolding hom_def by auto
thus ?thesis
unfolding group_hom_def group_hom_axioms_def
using subgroup.subgroup_is_group[OF assms G.is_group] by simp
qed

text ‹The order of an element under a homomorphism divides the order of the element.›

lemma (in group_hom) hom_ord_dvd_ord:
assumes "a ∈ carrier G"
shows "H.ord (h a) dvd G.ord a"
proof -
have "h a [^]⇘H⇙ (G.ord a) = h (a [^]⇘G⇙ G.ord a)"
using assms local.hom_nat_pow by presburger
also have "… = h (𝟭⇘G⇙)" using G.pow_ord_eq_1 assms by simp
also have "… = 𝟭⇘H⇙" by simp
finally have "h a [^]⇘H⇙ G.ord a = 𝟭⇘H⇙" .
then show ?thesis using pow_eq_id assms by simp
qed

text ‹In particular, this implies that the image of an element with a finite order also will have a
finite order.›

lemma (in group_hom) finite_ord_stays_finite:
assumes "a ∈ carrier G" "G.ord a ≠ 0"
shows "H.ord (h a) ≠ 0"
using hom_ord_dvd_ord assms by fastforce

text ‹For injective homomorphisms, the order stays the same.›

lemma (in group_hom) inj_imp_ord_eq:
assumes "a ∈ carrier G" "inj_on h (carrier G)" "G.ord a ≠ 0"
shows "H.ord (h a) = G.ord a"
proof (rule antisym)
show "H.ord (h a) ≤ G.ord a" using hom_ord_dvd_ord assms by force
show "G.ord a ≤ H.ord (h a)"
proof -
have "𝟭⇘H⇙ = h (a [^]⇘G⇙ H.ord(h a))" using H.pow_ord_eq_1 assms
then have "a [^]⇘G⇙ H.ord (h a) = 𝟭⇘G⇙" using assms inj_on_one_iff by simp
then have "G.ord a dvd H.ord (h a)" using G.pow_eq_id assms(1) by blast
thus ?thesis using assms finite_ord_stays_finite by fastforce
qed
qed

lemma (in group_hom) one_in_kernel:
"𝟭 ∈ kernel G H h"
using subgroup.one_closed subgroup_kernel by blast

lemma hom_in_carr:
assumes "f ∈ hom G H"
shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H"
using assms unfolding hom_def bij_betw_def by blast

lemma iso_in_carr:
assumes "f ∈ iso G H"
shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H"
using assms unfolding iso_def bij_betw_def by blast

lemma triv_iso:
assumes "group G" "group H" "carrier G = {𝟭⇘G⇙}" "carrier H = {𝟭⇘H⇙}"
shows "G ≅ H"
proof(unfold is_iso_def iso_def)
interpret G: group G by fact
interpret H: group H by fact
let ?f = "λ_. 𝟭⇘H⇙"
have "?f ∈ hom G H" by (intro homI, auto)
moreover have "bij_betw ?f (carrier G) (carrier H)" unfolding bij_betw_def
using assms(3, 4) by auto
ultimately show "{h ∈ hom G H. bij_betw h (carrier G) (carrier H)} ≠ {}" by blast
qed

text ‹The cardinality of the image of a group homomorphism times the cardinality of its kernel is
equal to the group order. This is basically another form of Lagrange's theorem.›

lemma (in group_hom) image_kernel_product: "card (h  (carrier G)) * card (kernel G H h) = order G"
proof -
interpret G: group G by simp
interpret H: group H by simp
interpret ih: subgroup "h  (carrier G)" H using img_is_subgroup by blast
interpret ih: group "H⦇carrier := h  (carrier G)⦈" using subgroup.subgroup_is_group by blast
interpret h: group_hom G "H⦇carrier := h  (carrier G)⦈"
by (unfold_locales, unfold hom_def, auto)
interpret k: subgroup "kernel G (H⦇carrier := h  carrier G⦈) h" G using h.subgroup_kernel by blast
from h.FactGroup_iso
have "G Mod kernel G (H⦇carrier := h  carrier G⦈) h ≅ H⦇carrier := h  carrier G⦈" by auto
hence "card (h  (carrier G)) = order (G Mod kernel G (H⦇carrier := h  carrier G⦈) h)"
using iso_same_card unfolding order_def by fastforce
moreover have "order (G Mod kernel G (H⦇carrier := h  carrier G⦈) h)
* card (kernel G (H⦇carrier := h  carrier G⦈) h) = order G"
using G.lagrange[OF k.subgroup_axioms] unfolding order_def FactGroup_def by force
moreover have "kernel G (H⦇carrier := h  carrier G⦈) h = kernel G H h"
unfolding kernel_def by auto
ultimately show ?thesis by argo
qed

end

# Theory Finite_And_Cyclic_Groups

(*
File:     Finite_And_Cyclic_Groups.thy
Author:   Joseph Thommes, TU München; Manuel Eberl, TU München
*)
section ‹Finite and cyclic groups›

theory Finite_And_Cyclic_Groups
imports Group_Hom Generated_Groups_Extend General_Auxiliary
begin

subsection ‹Finite groups›

text ‹We define the notion of finite groups and prove some trivial facts about them.›

locale finite_group = group +
assumes fin[simp]: "finite (carrier G)"

(* Manuel Eberl *)
lemma (in finite_group) ord_pos:
assumes "x ∈ carrier G"
shows   "ord x > 0"
using ord_ge_1[of x] assms by auto

lemma (in finite_group) order_gt_0 [simp,intro]: "order G > 0"
by (subst order_gt_0_iff_finite) auto

lemma (in finite_group) finite_ord_conv_Least:
assumes "x ∈ carrier G"
shows "ord x = (LEAST n::nat. 0 < n ∧ x [^] n = 𝟭)"
using pow_order_eq_1 order_gt_0_iff_finite ord_conv_Least assms by auto

lemma (in finite_group) non_trivial_group_ord_gr_1:
assumes "carrier G ≠ {𝟭}"
shows "∃e ∈ carrier G. ord e > 1"
proof -
from one_closed obtain e where e: "e ≠ 𝟭" "e ∈ carrier G" using assms carrier_not_empty by blast
thus ?thesis using ord_eq_1[of e] le_neq_implies_less ord_ge_1 by fastforce
qed

(* Manuel Eberl *)
lemma (in finite_group) max_order_elem:
obtains a where "a ∈ carrier G" "∀x ∈ carrier G. ord x ≤ ord a"
proof -
have "∃x. x ∈ carrier G ∧ (∀y. y ∈ carrier G ⟶ ord y ≤ ord x)"
proof (rule ex_has_greatest_nat[of _ 𝟭 _ "order G + 1"], safe)
show "𝟭 ∈ carrier G"
by auto
next
fix x assume "x ∈ carrier G"
hence "ord x ≤ order G"
by (intro ord_le_group_order fin)
also have "… < order G + 1"
by simp
finally show "ord x < order G + 1" .
qed
thus ?thesis using that by blast
qed

lemma (in finite_group) iso_imp_finite:
assumes "G ≅ H" "group H"
shows "finite_group H"
proof -
interpret H: group H by fact
show ?thesis
proof(unfold_locales)
show "finite (carrier H)" using iso_same_card[OF assms(1)]
by (metis card_gt_0_iff order_def order_gt_0)
qed
qed

lemma (in finite_group) finite_FactGroup:
assumes "H ⊲ G"
shows "finite_group (G Mod H)"
proof -
interpret H: normal H G by fact
interpret Mod: group "G Mod H" using H.factorgroup_is_group .
show ?thesis
by (unfold_locales, unfold FactGroup_def RCOSETS_def, simp)
qed

lemma (in finite_group) bigger_subgroup_is_group:
assumes "subgroup H G" "card H ≥ order G"
shows "H = carrier G"
using subgroup.subset fin assms by (metis card_seteq order_def)

text ‹All generated subgroups of a finite group are obviously also finite.›

lemma (in finite_group) finite_generate:
assumes "A ⊆ carrier G"
shows "finite (generate G A)"
using generate_incl[of A] rev_finite_subset[of "carrier G" "generate G A"] assms by simp

text ‹We also provide an induction rule for finite groups inspired by Manuel Eberl's AFP entry
"Dirichlet L-Functions and Dirichlet's Theorem" and the contained theory "Group\_Adjoin". A property
that is true for a subgroup generated by some set and stays true when adjoining an element, is also
true for the whole group.›

lemma (in finite_group) generate_induct[consumes 1, case_names base adjoin]:
assumes "A0 ⊆ carrier G"
assumes "A0 ⊆ carrier G ⟹ P (G⦇carrier := generate G A0⦈)"
assumes "⋀a A. ⟦A ⊆ carrier G; a ∈ carrier G - generate G A; A0 ⊆ A;
P (G⦇carrier := generate G A⦈)⟧ ⟹ P (G⦇carrier := generate G (A ∪ {a})⦈)"
shows "P G"
proof -
define A where A: "A = carrier G"
hence gA: "generate G A = carrier G"
using generate_incl[of "carrier G"] generate_sincl[of "carrier G"] by simp
hence "finite A" using fin A by argo
moreover have "A0 ⊆ A" using assms(1) A by argo
moreover have "A ⊆ carrier G" using A by simp
moreover have "generate G A0 ⊆ generate G A" using gA generate_incl[OF assms(1)] by argo
ultimately have "P (G⦇carrier := generate G A⦈)" using assms(2, 3)
proof (induction "A" taking: card rule: measure_induct_rule)
case (less A)
then show ?case
proof(cases "generate G A0 = generate G A")
case True
thus ?thesis using less by force
next
case gA0: False
with less(3) have s: "A0 ⊂ A" by blast
then obtain a where a: "a ∈ A - A0" by blast
have P1: "P (G⦇carrier := generate G (A - {a})⦈)"
proof(rule less(1))
show "card (A - {a}) < card A" using a less(2) by (meson DiffD1 card_Diff1_less)
show "A0 ⊆ A - {a}" using a s by blast
thus "generate G A0 ⊆ generate G (A - {a})" using mono_generate by presburger
qed (use less a s in auto)
show ?thesis
proof (cases "generate G A = generate G (A - {a})")
case True
then show ?thesis using P1 by simp
next
case False
have "a ∈ carrier G - generate G (A - {a})"
proof -
have "a ∉ generate G (A - {a})"
proof
assume a2: "a ∈ generate G (A - {a})"
have "generate G (A - {a}) = generate G A"
proof (rule equalityI)
show "generate G (A - {a}) ⊆ generate G A" using mono_generate by auto
show "generate G A ⊆ generate G (A - {a})"
proof(subst (2) generate_idem[symmetric])
show "generate G A ⊆ generate G (generate G (A - {a}))"
by (intro mono_generate, use generate_sincl[of "A - {a}"] a2 in blast)
qed (use less in auto)
qed
with False show False by argo
qed
with a less show ?thesis by fast
qed
from less(7)[OF _ this _ P1] less(4) s a have "P (G⦇carrier := generate G (A - {a} ∪ {a})⦈)"
by blast
moreover have "A - {a} ∪ {a} = A" using a by blast
ultimately show ?thesis by auto
qed
qed
qed
with gA show ?thesis by simp
qed

subsection ‹Finite abelian groups›

text ‹Another trivial locale: the finite abelian group with some trivial facts.›

locale finite_comm_group = finite_group + comm_group

lemma (in finite_comm_group) iso_imp_finite_comm:
assumes "G ≅ H" "group H"
shows "finite_comm_group H"
proof -
interpret H: group H by fact
interpret H: comm_group H by (intro iso_imp_comm_group[OF assms(1)], unfold_locales)
interpret H: finite_group H by (intro iso_imp_finite[OF assms(1)], unfold_locales)
show ?thesis by unfold_locales
qed

lemma (in finite_comm_group) finite_comm_FactGroup:
assumes "subgroup H G"
shows "finite_comm_group (G Mod H)"
unfolding finite_comm_group_def
proof(safe)
show "finite_group (G Mod H)" using finite_FactGroup[OF subgroup_imp_normal[OF assms]] .
show "comm_group (G Mod H)" by (simp add: abelian_FactGroup assms)
qed

(* Manuel Eberl *)
lemma (in finite_comm_group) subgroup_imp_finite_comm_group:
assumes "subgroup H G"
shows   "finite_comm_group (G⦇carrier := H⦈)"
proof -
interpret G': group "G⦇carrier := H⦈" by (intro subgroup_imp_group) fact+
interpret H: subgroup H G by fact
show ?thesis by standard (use finite_subset[OF H.subset] in ‹auto simp: m_comm›)
qed

subsection ‹Cyclic groups›

text ‹Now, the central notion of a cyclic group is introduced: a group generated
by a single element.›

locale cyclic_group = group +
fixes gen :: "'a"
assumes gen_closed[intro, simp]: "gen ∈ carrier G"
assumes generator: "carrier G = generate G {gen}"

lemma (in cyclic_group) elem_is_gen_pow:
assumes "x ∈ carrier G"
shows "∃n :: int. x = gen [^] n"
proof -
from generator have x_g:"x ∈ generate G {gen}" using assms by fast
with generate_pow[of gen] show ?thesis using gen_closed by blast
qed

text ‹Every cyclic group is commutative/abelian.›

sublocale cyclic_group ⊆ comm_group
proof(unfold_locales)
fix x y
assume "x ∈ carrier G" "y ∈ carrier G"
then obtain a b where ab:"x = gen [^] (a::int)" "y = gen [^] (b::int)"
using elem_is_gen_pow by presburger
then have "x ⊗ y = gen [^] (a + b)" by (simp add: int_pow_mult)
also have "… = y ⊗ x" using ab int_pow_mult
finally show "x ⊗ y = y ⊗ x" .
qed

text ‹Some trivial intro rules for showing that a group is cyclic.›

lemma (in group) cyclic_groupI0:
assumes "a ∈ carrier G" "carrier G = generate G {a}"
shows "cyclic_group G a"
using assms by (unfold_locales; auto)

lemma (in group) cyclic_groupI1:
assumes "a ∈ carrier G" "carrier G ⊆ generate G {a}"
shows "cyclic_group G a"
using assms by (unfold_locales, use generate_incl[of "{a}"] in auto)

lemma (in group) cyclic_groupI2:
assumes "a ∈ carrier G"
shows "cyclic_group (G⦇carrier := generate G {a}⦈) a"
proof (intro group.cyclic_groupI0)
show "group (G⦇carrier := generate G {a}⦈)"
by (intro subgroup.subgroup_is_group group.generate_is_subgroup, use assms in simp_all)
show "a ∈ carrier (G⦇carrier := generate G {a}⦈)" using generate.incl[of a "{a}"] by auto
show "carrier (G⦇carrier := generate G {a}⦈) = generate (G⦇carrier := generate G {a}⦈) {a}"
using assms
by (simp add: generate_consistent generate.incl group.generate_is_subgroup)
qed

text ‹The order of the generating element is always the same as the group order.›

lemma (in cyclic_group) ord_gen_is_group_order:
shows "ord gen = order G"
proof (cases "finite (carrier G)")
case True
with generator show "ord gen = order G"
using generate_pow_card[of gen] order_def[of G] gen_closed by simp
next
case False
thus ?thesis
using generate_pow_card generator order_def[of G] card_eq_0_iff[of "carrier G"] by force
qed

text ‹In the case of a finite group, it is sufficient to have one element of group order to know
that the group is cyclic.›

lemma (in finite_group) element_ord_generates_cyclic:
assumes "a ∈ carrier G" "ord a = order G"
shows "cyclic_group G a"
proof (unfold_locales)
show "a ∈ carrier G" using assms(1) by simp
show "carrier G = generate G {a}"
using assms bigger_subgroup_is_group[OF generate_is_subgroup]
by (metis empty_subsetI fin generate_pow_card insert_subset ord_le_group_order)
qed

text ‹Another useful fact is that a group of prime order is also cyclic.›

lemma (in group) prime_order_group_is_cyc:
assumes "Factorial_Ring.prime (order G)"
obtains g where "cyclic_group G g"
proof (unfold_locales)
obtain p where order_p: "order G = p" and p_prime: "Factorial_Ring.prime p" using assms by blast
then have "card (carrier G) ≥ 2" by (simp add: order_def prime_ge_2_nat)
then obtain a where a_in: "a ∈ carrier G" and a_not_one: "a ≠ 𝟭" using one_unique
by (metis (no_types, lifting) card_2_iff' obtain_subset_with_card_n subset_iff)
interpret fin: finite_group G
using assms order_gt_0_iff_finite unfolding order_def by unfold_locales auto
have "ord a dvd p" using a_in order_p ord_dvd_group_order by blast
hence "ord a = p" using prime_nat_iff[of p] p_prime ord_eq_1 a_in a_not_one by blast
then interpret cyclic_group G a
using fin.element_ord_generates_cyclic order_p a_in by simp
show ?thesis using that cyclic_group_axioms .
qed

text ‹What follows is an induction principle for cyclic groups: a predicate is true for all elements
of the group if it is true for all elements that can be formed by the generating element by just
multiplication and if it also holds under the forming of the inverse (as we by this cover
all elements of the group),›

(* Manuel Eberl *)
lemma (in cyclic_group) generator_induct [consumes 1, case_names generate inv]:
assumes x: "x ∈ carrier G"
assumes IH1: "⋀n::nat. P (gen [^] n)"
assumes IH2: "⋀x. x ∈ carrier G ⟹ P x ⟹ P (inv x)"
shows   "P x"
proof -
from x obtain n :: int where n: "x = gen [^] n"
using elem_is_gen_pow[of x] by auto
show ?thesis
proof (cases "n ≥ 0")
case True
have "P (gen [^] nat n)"
by (rule IH1)
with True n show ?thesis by simp
next
case False
have "P (inv (gen [^] nat (-n)))"
by (intro IH1 IH2) auto
also have "gen [^] nat (-n) = gen [^] (-n)"
using False by simp
also have "inv … = x"
using n by (simp add: int_pow_neg)
finally show ?thesis .
qed
qed

subsection ‹Finite cyclic groups›

text ‹Additionally, the notion of the finite cyclic group is introduced.›

locale finite_cyclic_group = finite_group + cyclic_group

sublocale finite_cyclic_group ⊆ finite_comm_group
by unfold_locales

lemma (in finite_cyclic_group) ord_gen_gt_zero:
"ord gen > 0"
using ord_ge_1[OF fin gen_closed] by simp

text ‹In order to prove something about an element in a finite abelian group, it is possible to show
this property for the neutral element or the generating element and inductively for the elements
that are formed by multiplying with the generator.›

lemma (in finite_cyclic_group) generator_induct0 [consumes 1, case_names one step]:
assumes x: "x ∈ carrier G"
assumes IH1: "P 𝟭"
assumes IH2: "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)"
shows   "P x"
proof -
from ord_gen_gt_zero generate_nat_pow[OF _ gen_closed] obtain n::nat where n: "x = gen [^] n"
using generator x by blast
thus ?thesis by (induction n arbitrary: x, use assms in auto)
qed

lemma (in finite_cyclic_group) generator_induct1 [consumes 1, case_names gen step]:
assumes x: "x ∈ carrier G"
assumes IH1: "P gen"
assumes IH2: "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)"
shows   "P x"
proof(rule generator_induct0[OF x])
show "⋀x. ⟦x ∈ carrier G; P x⟧ ⟹ P (x ⊗ gen)" using IH2 by blast
have "P x" if "n > 0" "x = gen [^] n" for n::nat and x using that
by (induction n arbitrary: x; use assms in fastforce)
from this[OF ord_pos[OF gen_closed] pow_ord_eq_1[OF gen_closed, symmetric]] show "P 𝟭" .
qed

subsection ‹‹get_exp› - discrete logarithm›

text ‹What now follows is the discrete logarithm for groups. It is used at several times througout
this entry and is initially used to show that two cyclic groups of the same order are isomorphic.›

definition (in group) get_exp where
"get_exp g = (λa. SOME k::int. a = g [^] k)"

text ‹For each element with itself as the basis the discrete logarithm indeed does what expected.
This is not the strongest possible statement, but sufficient for our needs.›

lemma (in group) get_exp_self_fulfills:
assumes "a ∈ carrier G"
shows "a = a [^] get_exp a a"
proof -
have "a = a [^] (1::int)" using assms by auto
moreover have "a [^] (1::int) = a [^] (SOME x::int. a [^] (1::int) = a [^] x)"
by (intro someI_ex[of "λx::int. a [^] (1::int) = a [^] x"]; blast)
ultimately show ?thesis unfolding get_exp_def by simp
qed

lemma (in group) get_exp_self:
assumes "a ∈ carrier G"
shows "get_exp a a mod ord a = (1::int) mod ord a"
by (intro pow_eq_int_mod[OF assms], use get_exp_self_fulfills[OF assms] assms in auto)

text ‹For cyclic groups, the discrete logarithm "works" for every element.›

lemma (in cyclic_group) get_exp_fulfills:
assumes "a ∈ carrier G"
shows "a = gen [^] get_exp gen a"
proof -
from elem_is_gen_pow[OF assms] obtain k::int where k: "a = gen [^] k" by blast
moreover have "gen [^] k = gen [^] (SOME x::int. gen [^] k = gen [^] x)"
by(intro someI_ex[of "λx::int. gen [^] k = gen [^] x"]; blast)
ultimately show ?thesis unfolding get_exp_def by blast
qed

lemma (in cyclic_group) get_exp_non_zero:
assumes"b ∈ carrier G" "b ≠ 𝟭"
shows "get_exp gen b ≠ 0"
using assms get_exp_fulfills[OF assms(1)] by auto

text ‹One well-known logarithmic identity.›

lemma (in cyclic_group) get_exp_mult_mod:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "get_exp gen (a ⊗ b) mod (ord gen) = (get_exp gen a + get_exp gen b) mod (ord gen)"
proof (intro pow_eq_int_mod[OF gen_closed])
from get_exp_fulfills[of "a ⊗ b"] have "gen [^] get_exp gen (a ⊗ b) = a ⊗ b" using assms by simp
moreover have "gen [^] (get_exp gen a + get_exp gen b) = a ⊗ b"
proof -
have "gen [^] (get_exp gen a + get_exp gen b) = gen [^] (get_exp gen a) ⊗ gen [^] (get_exp gen b)"
using int_pow_mult by blast
with get_exp_fulfills assms show ?thesis by simp
qed
ultimately show "gen [^] get_exp gen (a ⊗ b) = gen [^] (get_exp gen a + get_exp gen b)" by simp
qed

text ‹We now show that all functions from a group generated by 'a' to a group generated by 'b'
that map elements from $a^k$ to $b^k$ in the other group are in fact isomorphisms between these two
groups.›

lemma (in group) iso_cyclic_groups_generate:
assumes "a ∈ carrier G" "b ∈ carrier H" "group.ord G a = group.ord H b" "group H"
shows "{f. ∀k ∈ (UNIV::int set). f (a [^] k) = b [^]⇘H⇙ k}
⊆ iso (G⦇carrier := generate G {a}⦈) (H⦇carrier := generate H {b}⦈)"
proof
interpret H: group H by fact
let ?A = "G⦇carrier := generate G {a}⦈"
let ?B = "H⦇carrier := generate H {b}⦈"
interpret A: cyclic_group ?A a by (intro group.cyclic_groupI2; use assms(1) in simp)
interpret B: cyclic_group ?B b by (intro group.cyclic_groupI2; use assms(2) in simp)
have sA: "subgroup (generate G {a}) G" by (intro generate_is_subgroup, use assms(1) in simp)
have sB: "subgroup (generate H {b}) H" by (intro H.generate_is_subgroup, use assms(2) in simp)
fix x
assume x: "x ∈ {f. ∀k∈(UNIV::int set). f (a [^] k) = b [^]⇘H⇙ k}"
have hom: "x ∈ hom ?A ?B"
proof (intro homI)
fix c
assume c: "c ∈ carrier ?A"
from A.elem_is_gen_pow[OF this] obtain k::int where k: "c = a [^] k"
using int_pow_consistent[OF sA generate.incl[of a]] by auto
with x have "x c = b [^]⇘H⇙ k" by blast
thus "x c ∈ carrier ?B"
using B.int_pow_closed H.int_pow_consistent[OF sB] generate.incl[of b "{b}" H] by simp
fix d
assume d: "d ∈ carrier ?A"
from A.elem_is_gen_pow[OF this] obtain l::int where l: "d = a [^] l"
using int_pow_consistent[OF sA generate.incl[of a]] by auto
with k have "c ⊗ d = a [^] (k + l)" by (simp add: int_pow_mult assms(1))
with x have "x (c ⊗⇘?A⇙ d) = b [^]⇘H⇙ (k + l)" by simp
also have "… = b [^]⇘H⇙ k ⊗⇘H⇙ b [^]⇘H⇙ l" by (simp add: H.int_pow_mult assms(2))
finally show "x (c ⊗⇘?A⇙ d) = x c ⊗⇘?B⇙ x d" using x k l by simp
qed
then interpret xgh: group_hom ?A ?B x unfolding group_hom_def group_hom_axioms_def by blast
have "kernel ?A ?B x = {𝟭}"
proof(intro equalityI)
show "{𝟭} ⊆ kernel ?A ?B x" using xgh.one_in_kernel by auto
have "c = 𝟭" if "c ∈ kernel ?A ?B x" for c
proof -
from that have c: "c ∈ carrier ?A" unfolding kernel_def by blast
from A.elem_is_gen_pow[OF this] obtain k::int where k: "c = a [^] k"
using int_pow_consistent[OF sA generate.incl[of a]] by auto
moreover have "x c = 𝟭⇘H⇙" using that x unfolding kernel_def by auto
ultimately have "𝟭⇘H⇙ = b [^]⇘H⇙ k" using x by simp
with assms(3) have "a [^] k = 𝟭"
using int_pow_eq_id[OF assms(1), of k] H.int_pow_eq_id[OF assms(2), of k] by simp
thus "c = 𝟭" using k by blast
qed
thus "kernel ?A ?B x ⊆ {𝟭}" by blast
qed
moreover have "carrier ?B ⊆ x  carrier ?A"
proof
fix c
assume c: "c ∈ carrier ?B"
from B.elem_is_gen_pow[OF this] obtain k::int where k: "c = b [^]⇘H⇙ k"
using H.int_pow_consistent[OF sB generate.incl[of b]] by auto
then have "x (a [^] k) = c" using x by blast
moreover have "a [^] k ∈ carrier ?A"
using int_pow_consistent[OF sA generate.incl[of a]] A.int_pow_closed generate.incl[of a]
by fastforce
ultimately show "c ∈ x  carrier ?A" by blast
qed
ultimately show "x ∈ iso ?A ?B" using hom xgh.iso_iff unfolding kernel_def by auto
qed

text ‹This is then used to derive the isomorphism of two cyclic groups of the same order as a
direct consequence.›

lemma (in cyclic_group) iso_cyclic_groups_same_order:
assumes "cyclic_group H h" "order G = order H"
shows "G ≅ H"
proof(intro is_isoI)
interpret H: cyclic_group H h by fact
define f where "f = (λa. h [^]⇘H⇙ get_exp gen a)"
from assms(2) have o: "ord gen = H.ord h" using ord_gen_is_group_order H.ord_gen_is_group_order
by simp
have "∀k ∈ (UNIV::int set). f (gen [^] k) = h [^]⇘H⇙ k"
proof
fix k
assume k: "k ∈ (UNIV::int set)"
have "gen [^] k = gen [^] (SOME x::int. gen [^] k = gen [^] x)"
by(intro someI_ex[of "λx::int. gen [^] k = gen [^] x"]; blast)
moreover have "(SOME x::int. gen [^] k = gen [^] x) = (SOME x::int. h [^]⇘H⇙ k = h [^]⇘H⇙ x)"
proof -
have "gen [^] k = gen [^] x ⟷ h [^]⇘H⇙ k = h [^]⇘H⇙ x" for x::int
thus ?thesis by simp
qed
moreover have "h [^]⇘H⇙ k = h [^]⇘H⇙ (SOME x::int. h [^]⇘H⇙ k = h [^]⇘H⇙ x)"
by(intro someI_ex[of "λx::int. h [^]⇘H⇙ k = h [^]⇘H⇙ x"]; blast)
ultimately show "f (gen [^] k) = h [^]⇘H⇙ k" unfolding f_def get_exp_def by metis
qed
thus "f ∈ iso G H"
using iso_cyclic_groups_generate[OF gen_closed H.gen_closed o H.is_group]
by (auto simp flip: generator H.generator)
qed

subsection ‹Integer modular groups›

text ‹We show that ‹integer_mod_group› (written as ‹Z n›) is in fact a cyclic group.
For $n \neq 1$ it is generated by $1$ and in the other case by $0$.›

notation integer_mod_group ("Z")

lemma Zn_neq1_cyclic_group:
assumes "n ≠ 1"
shows "cyclic_group (Z n) 1"
proof(unfold cyclic_group_def cyclic_group_axioms_def, safe)
show "group (Z n)" using group_integer_mod_group .
then interpret group "Z n" .
show oc: "1 ∈ carrier (Z n)"
unfolding integer_mod_group_def integer_group_def using assms by force
show "x ∈ generate (Z n) {1}" if "x ∈ carrier (Z n)" for x
using generate_pow[OF oc] that int_pow_integer_mod_group solve_equation subgroup_self
by fastforce
show "x ∈ carrier (Z n)" if "x ∈ generate (Z n) {1}" for x using generate_incl[of "{1}"] that oc
by fast
qed

lemma Z1_cyclic_group: "cyclic_group (Z 1) 0"
proof(unfold cyclic_group_def cyclic_group_axioms_def, safe)
show "group (Z 1)" using group_integer_mod_group .
then interpret group "Z 1" .
show "0 ∈ carrier (Z 1)" unfolding integer_mod_group_def by simp
thus "x ∈ carrier (Z 1)" if "x ∈ generate (Z 1) {0}" for x using generate_incl[of "{0}"] that
by fast
show "x ∈ generate (Z 1) {0}" if "x ∈ carrier (Z 1)" for x
proof -
from that have "x = 0" unfolding integer_mod_group_def by auto
with generate.one[of "Z 1" "{0}"] show "x ∈ generate (Z 1) {0}" unfolding integer_mod_group_def
by simp
qed
qed

lemma Zn_cyclic_group:
obtains x where "cyclic_group (Z n) x"
using Z1_cyclic_group Zn_neq1_cyclic_group by metis

text ‹Moreover, its order is just $n$.›

lemma Zn_order: "order (Z n) = n"
by (unfold integer_mod_group_def integer_group_def order_def, auto)

text ‹Consequently, ‹Z n› is isomorphic to any cyclic group of order $n$.›

lemma (in cyclic_group) Zn_iso:
assumes "order G = n"
shows "G ≅ Z n"
using Zn_order Zn_cyclic_group iso_cyclic_groups_same_order assms by metis

no_notation integer_mod_group ("Z")
end

# Theory DirProds

(*
File:     DirProds.thy
Author:   Joseph Thommes, TU München
*)
section ‹Direct group product›

theory DirProds
imports Finite_Product_Extend Group_Hom Finite_And_Cyclic_Groups
begin

notation integer_mod_group ("Z")

text ‹The direct group product is defined component-wise and provided in an indexed way.›

definition DirProds :: "('a ⇒ ('b, 'c) monoid_scheme) ⇒ 'a set ⇒ ('a ⇒ 'b) monoid" where
"DirProds G I = ⦇ carrier = Pi⇩E I (carrier ∘ G),
monoid.mult = (λx y. restrict (λi. x i ⊗⇘G i⇙ y i) I),
one = restrict (λi. 𝟭⇘G i⇙) I ⦈"

lemma DirProds_empty:
"carrier (DirProds f {}) = {𝟭⇘DirProds f {}⇙}"
unfolding DirProds_def by auto

lemma DirProds_order:
assumes "finite I"
shows "order (DirProds G I) = prod (order ∘ G) I"
unfolding order_def DirProds_def using assms by (simp add: card_PiE)

lemma DirProds_in_carrI:
assumes "⋀i. i ∈ I ⟹ x i ∈ carrier (G i)" "⋀i. i ∉ I ⟹ x i = undefined"
shows "x ∈ carrier (DirProds G I)"
unfolding DirProds_def using assms by auto

lemma comp_in_carr:
assumes "x ∈ carrier (DirProds G I)" "i ∈ I"
shows "x i ∈ carrier (G i)"
using assms unfolding DirProds_def by auto

lemma comp_mult:
assumes "i ∈ I"
shows "(x ⊗⇘DirProds G I⇙ y) i = (x i ⊗⇘G i⇙ y i)"
using assms unfolding DirProds_def by simp

lemma comp_exp_nat:
fixes k::nat
assumes "i ∈ I"
shows "(x [^]⇘DirProds G I⇙ k) i = x i [^]⇘G i⇙ k"
proof (induction k)
case 0
then show ?case using assms unfolding DirProds_def by simp
next
case i: (Suc k)
have "(x [^]⇘DirProds G I⇙ k ⊗⇘DirProds G I⇙ x) i = (x [^]⇘DirProds G I⇙ k) i ⊗⇘G i⇙ x i"
by(rule comp_mult[OF assms])
also from i have "… = x i [^]⇘G i⇙ k ⊗⇘G i⇙ x i" by simp
also have "… = x i [^]⇘G i⇙ Suc k" by simp
finally show ?case by simp
qed

lemma DirProds_m_closed:
assumes "x ∈ carrier (DirProds G I)" "y ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ group (G i)"
shows "x ⊗⇘DirProds G I⇙ y ∈ carrier (DirProds G I)"
using assms monoid.m_closed[OF group.is_monoid[OF assms(3)]] unfolding DirProds_def by fastforce

lemma partial_restr:
assumes "a ∈ carrier (DirProds G I)" "J ⊆ I"
shows "restrict a J ∈ carrier (DirProds G J)"
using assms unfolding DirProds_def by auto

lemma eq_parts_imp_eq:
assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "⋀i. i ∈ I ⟹ a i = b i"
shows "a = b"
using assms unfolding DirProds_def by fastforce

lemma mult_restr:
assumes "a ∈ carrier (DirProds G I)" "b ∈ carrier (DirProds G I)" "J ⊆ I"
shows "a ⊗⇘DirProds G J⇙ b = restrict (a ⊗⇘DirProds G I⇙ b) J"
using assms unfolding DirProds_def by force

lemma DirProds_one:
assumes "x ∈ carrier (DirProds G I)"
shows "(∀i ∈ I. x i = 𝟭⇘G i⇙) ⟷ x = 𝟭⇘DirProds G I⇙"
using assms unfolding DirProds_def by fastforce

lemma DirProds_one':
"i∈I ⟹ 𝟭⇘DirProds G I⇙ i = 𝟭⇘G i⇙"
unfolding DirProds_def by simp

lemma DirProds_one'':
"𝟭⇘DirProds G I⇙ = restrict (λi. 𝟭⇘G i⇙) I"
by (unfold DirProds_def, simp)

lemma DirProds_mult:
"(⊗⇘DirProds G I⇙) = (λx y. restrict (λi. x i ⊗⇘G i⇙ y i) I)"
unfolding DirProds_def by simp

lemma DirProds_one_iso: "(λx. x G) ∈ iso (DirProds f {G}) (f G)"
proof (intro isoI homI)
show "bij_betw (λx. x G) (carrier (DirProds f {G})) (carrier (f G))"
proof (unfold bij_betw_def, rule)
show "inj_on (λx. x G) (carrier (DirProds f {G}))"
by (intro inj_onI, unfold DirProds_def PiE_def Pi_def extensional_def, fastforce)
show "(λx. x G)  carrier (DirProds f {G}) = carrier (f G)"
proof(intro equalityI subsetI)
show "x ∈ carrier (f G)" if "x ∈ (λx. x G)  carrier (DirProds f {G})" for x
using that unfolding DirProds_def by auto
show "x ∈ (λx. x G)  carrier (DirProds f {G})" if xc: "x ∈ carrier (f G)" for x
proof
show "(λk∈{G}. x) ∈ carrier (DirProds f {G})" unfolding DirProds_def using xc by auto
moreover show "x = (λk∈{G}. x) G" by simp
qed
qed
qed
qed (unfold DirProds_def PiE_def Pi_def extensional_def, auto)

lemma DirProds_one_cong: "(DirProds f {G}) ≅ (f G)"
using DirProds_one_iso is_isoI by fast

lemma DirProds_one_iso_sym: "(λx. (λ_∈{G}. x)) ∈ iso (f G) (DirProds f {G})"
proof (intro isoI homI)
show "bij_betw (λx. λ_∈{G}. x) (carrier (f G)) (carrier (DirProds f {G}))"
proof (unfold bij_betw_def, rule)
show "inj_on (λx. (λ_∈{G}. x)) (carrier (f G))"
by (intro inj_onI, metis imageI image_constant image_restrict_eq member_remove remove_def)
show "(λx. (λ_∈{G}. x))  carrier (f G) = carrier (DirProds f {G})"
unfolding DirProds_def by fastforce
qed
qed (unfold DirProds_def, auto)

lemma DirProds_one_cong_sym: "(f G) ≅ (DirProds f {G})"
using DirProds_one_iso_sym is_isoI by fast

text ‹The direct product is a group iff all factors are groups.›

lemma DirProds_is_group:
assumes "⋀i. i ∈ I ⟹ group (G i)"
shows "group (DirProds G I)"
proof(rule groupI)
show one_closed: "𝟭⇘DirProds G I⇙ ∈ carrier (DirProds G I)" unfolding DirProds_def
fix x
assume x: "x ∈ carrier (DirProds G I)"
have one_: "⋀i. i ∈ I ⟹ 𝟭⇘G i⇙ = 𝟭⇘DirProds G I⇙ i" unfolding DirProds_def by simp
have "⋀i. i ∈ I ⟹ 𝟭⇘DirProds G I⇙ i ⊗⇘G i⇙ x i = x i"
proof -
fix i
assume i: "i ∈ I"
interpret group "G i" using assms[OF i] .
have "x i ∈ carrier (G i)" using x i comp_in_carr by fast
thus "𝟭⇘DirProds G I⇙ i ⊗⇘G i⇙ x i = x i" by(subst one_[OF i, symmetric]; simp)
qed
with one_ x show "𝟭⇘DirProds G I⇙ ⊗⇘DirProds G I⇙ x = x" unfolding DirProds_def by force
have "restrict (λi. inv⇘G i⇙ (x i)) I ∈ carrier (DirProds G I)" using x group.inv_closed[OF assms]
unfolding DirProds_def by fastforce
moreover have "restrict (λi. inv⇘G i⇙ (x i)) I ⊗⇘DirProds G I⇙ x = 𝟭⇘DirProds G I⇙"
using x group.l_inv[OF assms] unfolding DirProds_def by fastforce
ultimately show "∃y∈carrier (DirProds G I). y ⊗⇘DirProds G I⇙ x = 𝟭⇘DirProds G I⇙" by blast
fix y
assume y: "y ∈ carrier (DirProds G I)"
from DirProds_m_closed[OF x y assms] show m_closed: "x ⊗⇘DirProds G I⇙ y ∈ carrier (DirProds G I)"
by blast
fix z
assume z: "z ∈ carrier (DirProds G I)"
have "⋀i. i ∈ I ⟹ (x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i
= (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i"
proof -
fix i
assume i: "i ∈ I"
have "(x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i = (x ⊗⇘DirProds G I⇙ y) i ⊗⇘G i⇙ z i"
using assms by (simp add: comp_mult i m_closed z)
also have "… = x i ⊗⇘G i⇙ y i ⊗⇘G i⇙ z i" by (simp add: assms comp_mult i x y)
also have "… = x i ⊗⇘G i⇙ (y i ⊗⇘G i⇙ z i)" using i assms x y z
by (meson Group.group_def comp_in_carr monoid.m_assoc)
also have "… = (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i" by (simp add: DirProds_def i)
finally show "(x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z) i
= (x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)) i" .
qed
thus "x ⊗⇘DirProds G I⇙ y ⊗⇘DirProds G I⇙ z = x ⊗⇘DirProds G I⇙ (y ⊗⇘DirProds G I⇙ z)"
unfolding DirProds_def by auto
qed

lemma DirProds_obtain_elem_carr:
assumes "group (DirProds G I)" "i ∈ I" "x ∈ carrier (G i)"
obtains k where "k ∈ carrier (DirProds G I)" "k i = x"
proof -
interpret DP: group "DirProds G I" by fact
from comp_in_carr[OF DP.one_closed] DirProds_one' have ao: "∀j∈I. 𝟭⇘G j⇙ ∈ carrier (G j)" by metis
let ?r = "restrict ((λj. 𝟭⇘G j⇙)(i := x)) I"
have "?r ∈ carrier (DirProds G I)"
unfolding DirProds_def PiE_def Pi_def using assms(2, 3) ao by auto
moreover have "?r i = x" using assms(2) by simp
ultimately show "(⋀k. ⟦k ∈ carrier (DirProds G I); k i = x⟧ ⟹ thesis) ⟹ thesis" by blast
qed

lemma DirProds_group_imp_groups:
assumes "group (DirProds G I)" and i: "i ∈ I"
shows "group (G i)"
proof (intro groupI)
let ?DP = "DirProds G I"
interpret DP: group ?DP by fact
show "𝟭⇘G i⇙ ∈ carrier (G i)" using DirProds_one' comp_in_carr[OF DP.one_closed i] i by metis
show "x ⊗⇘G i⇙ y ∈ carrier (G i)" if "x ∈ carrier (G i)" "y ∈ carrier (G i)" for x y
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
from DirProds_obtain_elem_carr[OF assms that(2)] obtain l where l: "l ∈ carrier ?DP" "l i = y" .
have "k ⊗⇘?DP⇙ l ∈ carrier ?DP" using k l by fast
from comp_in_carr[OF this i] comp_mult[OF i] show ?thesis using k l by metis
qed
show "x ⊗⇘G i⇙ y ⊗⇘G i⇙ z = x ⊗⇘G i⇙ (y ⊗⇘G i⇙ z)"
if x: "x ∈ carrier (G i)" and y: "y ∈ carrier (G i)" and z: "z ∈ carrier (G i)" for x y z
proof -
from DirProds_obtain_elem_carr[OF assms x] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
from DirProds_obtain_elem_carr[OF assms y] obtain l where l: "l ∈ carrier ?DP" "l i = y" .
from DirProds_obtain_elem_carr[OF assms z] obtain m where m: "m ∈ carrier ?DP" "m i = z" .
have "x ⊗⇘G i⇙ y ⊗⇘G i⇙ z = (k i) ⊗⇘G i⇙ (l i) ⊗⇘G i⇙ (m i)" using k l m by argo
also have "… = (k ⊗⇘?DP⇙ l ⊗⇘?DP⇙ m) i" using comp_mult[OF i] k l m by metis
also have "… = (k ⊗⇘?DP⇙ (l ⊗⇘?DP⇙ m)) i"
proof -
have "k ⊗⇘?DP⇙ l ⊗⇘?DP⇙ m = k ⊗⇘?DP⇙ (l ⊗⇘?DP⇙ m)" using DP.m_assoc[OF k(1) l(1) m(1)] .
thus ?thesis by simp
qed
also have "… = (k i) ⊗⇘G i⇙ ((l i) ⊗⇘G i⇙ (m i))" using comp_mult[OF i] k l m by metis
finally show ?thesis using k l m by blast
qed
show "𝟭⇘G i⇙ ⊗⇘G i⇙ x = x" if "x ∈ carrier (G i)" for x
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
hence "𝟭⇘?DP⇙ ⊗⇘?DP⇙ k = k" by simp
with comp_mult k DirProds_one[OF DP.one_closed] that i show ?thesis by metis
qed
show "∃y∈carrier (G i). y ⊗⇘G i⇙ x = 𝟭⇘G i⇙" if "x ∈ carrier (G i)" for x
proof -
from DirProds_obtain_elem_carr[OF assms that(1)] obtain k where k: "k ∈ carrier ?DP" "k i = x" .
hence ic: "inv⇘?DP⇙ k ∈ carrier ?DP" by simp
have "inv⇘?DP⇙ k ⊗⇘?DP⇙ k = 𝟭⇘?DP⇙" using k by simp
hence "(inv⇘?DP⇙ k) i ⊗⇘G i⇙ k i= 𝟭⇘G i⇙" using comp_mult[OF i] DirProds_one'[OF i] by metis
with k(2) comp_in_carr[OF ic i] show ?thesis by blast
qed
qed

lemma DirProds_group_iff: "group (DirProds G I) ⟷ (∀i∈I. group (G i))"
using DirProds_is_group DirProds_group_imp_groups by metis

lemma comp_inv:
assumes "group (DirProds G I)" and x: "x ∈ carrier (DirProds G I)" and i: "i ∈ I"
shows "(inv⇘(DirProds G I)⇙ x) i = inv⇘(G i)⇙ (x i)"
proof -
interpret DP: group "DirProds G I" by fact
interpret Gi: group "G i" using DirProds_group_imp_groups[OF DP.is_group i] .
have ixc: "inv⇘(DirProds G I)⇙ x ∈ carrier (DirProds G I)" using x by blast
hence `