Session Finitely_Generated_Abelian_Groups

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 "(yJ. {x  y}) = (⊗) x ` J" using image_def[of "(⊗) x" J] by blast
  ultimately show "card (hJ. {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
    by (simp add: step.hyps(1) step.hyps(2))
  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  (yJ. {a  y})  (yJ. {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 "(hH. kJ. {h  k}) = (kJ. hH. {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 [^]Gcarrier := H b = a [^]G (b::nat)"
  by (simp add: nat_pow_def)

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 (Gcarrier := 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 (Gcarrier := 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 "(Gcarrier := 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 (Gcarrier := 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 (Gcarrier := H)" by blast
  show "comm_monoid (Gcarrier := 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"
    by (simp add: int_pow_int)
  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 (Gcarrier := H) x = ord x"
  using nat_pow_consistent ord_def group.ord_def[of "(Gcarrier := 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 "𝟭Gcarrier := 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
    by (simp add: normal_imp_subgroup subgroup.rcos_const) 
  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 (xA. generate G {x}) = generate G A"
proof
  have "A  (xA. generate G {x})" using generate.incl by force
  thus "generate G A  generate G (xA. generate G {x})" using mono_generate by presburger
  have "x. x  A  generate G {x}  generate G A" using mono_generate by auto
  hence "(xA. generate G {x})  generate G A" by blast
  thus "generate G (xA. 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)}  (SA. 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  (SA. generate G (f S))" using M by blast
  qed
  thus "generate G ( {generate G {x} |x. x   (f ` A)})  generate G (SA. generate G (f S))"
    using mono_generate by simp
  have a: "generate G (SA. 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 "(SA. generate G (f S))  generate G ( (f ` A))" by blast
    then have "generate G (SA. generate G (f S))  generate G (generate G ( (f ` A)))"
      using mono_generate by meson
    thus "generate G (SA. 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 (SA. 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 (Gcarrier := 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" "aA. 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" "aA. 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"
      by (simp add: DeMoivre)
  next
    fix m assume m: "m > 0" "m < n"
    have "cis (2 * pi / n) ^ m = cis (2 * pi * m / n)"
      by (simp add: DeMoivre algebra_simps)
    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 (Gcarrier := H)" "subgroup K (Gcarrier := 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 (Gcarrier := H) A B"
proof -
  interpret H: group "Gcarrier := H" using subgroup.subgroup_is_group assms by blast
  have "𝟭G = 𝟭Gcarrier := 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 (aJ. (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)  (yF. (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 = (aF. (H #> a))"
      unfolding set_mult_def using r_coset_def[of G H] by auto
    ultimately have "card(H #> x) + card(yF. (H #> y))
                   = card((H #> x)  (yF. (H #> y))) + card((H #> x)  (yF. (H #> y)))"
      using card_Un_Int by auto
    then have "card(H #> x) + card(yF. (H #> y)) = card((H #> x)  (yF. (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"
      by (simp add: i)
    ultimately show ?case using cF by simp
  qed
  moreover have "H <#> J = (aJ. (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"
  by (simp add: generate_subgroup_id IDirProds_def)

lemma (in comm_group) IDirProds_Un:
  assumes "iA. subgroup (S i) G" "jB. 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" "iI. subgroup (S i) G" "iI. 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" "iI. subgroup (S i) G"
          "iI. 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) = (iI. 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})))"

text ‹Some lemmas about compl_fam›.›

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 (ggs - {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 "iA. 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" "iI. 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 "igs. 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 (Gcarrier := H) f S"
proof (cases "finite S")
  case True
  interpret H: comm_group "Gcarrier := 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 (Gcarrier := 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 Gcarrier := H finprod (Gcarrier := H) f F"
      by auto
    moreover have "finprod (Gcarrier := H) f (insert x F) = "
    proof(intro H.finprod_insert[OF i(1, 2)])
      show "f  F  carrier (Gcarrier := H)" "f x  carrier (Gcarrier := 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) ` PiE 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 ags. 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 ags. 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 ags. 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 ags. generate G {a})" "g = finprod G i gs" by blast
      from gh obtain j where j: "j  (ΠE ags. 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 ags. 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  (PiE 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) ` PiE gs (λa. generate G {a})
      = (λx. finprod G x gs) ` Pi gs (λa. generate G {a})"
  proof
    have "PiE gs (λa. generate G {a})  Pi gs (λa. generate G {a})" by blast
    thus "(λx. finprod G x gs) ` PiE 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) ` PiE 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  PiE gs (λa. generate G {a})" using f(2) by simp
      ultimately show "x  (λx. finprod G x gs) ` PiE 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) ` (Π ags. 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) ` (Π ags. generate G {a})"
    then obtain f where f: "f  (Π ags. 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). ags. f a = a [^] h a" by meson
    then obtain h where h: "ags. 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 "kgenerate 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: "ags. a [^] h a = f a" "f  (Π ags. 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) ` (Π ags. 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) ` (PiE I S)" (is "?DP = ?fp")
proof
  show "?fp  ?DP"
  proof
    fix x
    assume x: "x  ?fp"
    then obtain f where f: "f  (PiE 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  PiE 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  PiE 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  PiE 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  PiE I S" "a = finprod G f I" by blast
      from e obtain g where g: "g  PiE 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 = (λaI. 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)  PiE 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) ` (PiE I S)"
  proof
    have "PiE I S  Pi I S" by blast
    thus "(λx. finprod G x I) ` PiE 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) ` PiE 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  PiE I S" using f(2) by simp
      ultimately show "x  (λx. finprod G x I) ` PiE 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)  (Π aB. 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)  (Π aA. 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 "iI. 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 = 𝟭  (iI. 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 = 𝟭  (iI. 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  PiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭))"
proof
  show "compl_fam S I  fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
    using triv_finprod_iff_compl_fam_Pi[OF assms] by auto
  have "fPiE I S. finprod G f I = 𝟭  (iI. f i = 𝟭)
     fPi I S. finprod G f I = 𝟭  (iI. f i = 𝟭)"
  proof(rule+)
    fix f i
    assume f: "f  Pi I S" "finprod G f I = 𝟭" and i: "i  I"
    assume allf: "fPiE I S. finprod G f I = 𝟭  (iI. 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  PiE I S" using f by simp
    ultimately show "f i = 𝟭" using allf f i by metis
  qed
  thus "fPiE I S. finprod G f I = 𝟭  (iI. 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   "(xA. yB x. g x y) = (zSigma A B. case z of (x, y)  g x y)"
  using assms
proof (induction A rule: finite_induct)
  case (insert x A)
  have "(zSigma (insert x A) B. case z of (x, y)  g x y) =
          (zPair x ` B x. case z of (x, y)  g x y)  (zSigma 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 "(zSigma A B. case z of (x, y)  g x y) = (xA. yB x. g x y)"
    using insert.prems insert.hyps by (subst insert.IH [symmetric]) auto
  also have "(zPair x ` B x. case z of (x, y)  g x y) = (yB 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 "igs  {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 ags - {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})) ` (Π ags - {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 "invH (h x)  I" using subgroup.m_inv_closed assms by fast
    moreover have "inv x  carrier G" using x by simp
    moreover have "invH (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
      by (simp add: local.hom_nat_pow)
    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 "Hcarrier := h ` (carrier G)" using subgroup.subgroup_is_group by blast
  interpret h: group_hom G "Hcarrier := h ` (carrier G)"
    by (unfold_locales, unfold hom_def, auto)
  interpret k: subgroup "kernel G (Hcarrier := h ` carrier G) h" G using h.subgroup_kernel by blast
  from h.FactGroup_iso
  have "G Mod kernel G (Hcarrier := h ` carrier G) h  Hcarrier := h ` carrier G" by auto
  hence "card (h ` (carrier G)) = order (G Mod kernel G (Hcarrier := h ` carrier G) h)"
    using iso_same_card unfolding order_def by fastforce
  moreover have "order (G Mod kernel G (Hcarrier := h ` carrier G) h)
                 * card (kernel G (Hcarrier := h ` carrier G) h) = order G"
    using G.lagrange[OF k.subgroup_axioms] unfolding order_def FactGroup_def by force
  moreover have "kernel G (Hcarrier := 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 (Gcarrier := generate G A0)"
  assumes "a A. A  carrier G; a  carrier G - generate G A; A0  A;
           P (Gcarrier := generate G A)  P (Gcarrier := 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 (Gcarrier := 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 (Gcarrier := 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 (Gcarrier := 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 (Gcarrier := H)"
proof -
  interpret G': group "Gcarrier := 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
    by (metis add.commute gen_closed)
  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 (Gcarrier := generate G {a}) a"
proof (intro group.cyclic_groupI0)
  show "group (Gcarrier := generate G {a})"
    by (intro subgroup.subgroup_is_group group.generate_is_subgroup, use assms in simp_all)
  show "a  carrier (Gcarrier := generate G {a})" using generate.incl[of a "{a}"] by auto
  show "carrier (Gcarrier := generate G {a}) = generate (Gcarrier := 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 (Gcarrier := generate G {a}) (Hcarrier := generate H {b})"
proof
  interpret H: group H by fact
  let ?A = "Gcarrier := generate G {a}"
  let ?B = "Hcarrier := 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
        by (simp add: o group.int_pow_eq)  
      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 = PiE I (carrier  G),
                   monoid.mult = (λx y. restrict (λi. x i G i y i) I),
                   one = restrict (λi. 𝟭G i) I "

text ‹Basic lemmas about DirProds›.›

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':
  "iI  𝟭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
    by (simp add: assms group.is_monoid)
  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. invG i (x i)) I  carrier (DirProds G I)" using x group.inv_closed[OF assms]
    unfolding DirProds_def by fastforce 
  moreover have "restrict (λi. invG 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 "ycarrier (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: "jI. 𝟭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 "ycarrier (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)  (iI. 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