Theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups

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

theory Finite_And_Cyclic_Groups
  imports Group_Hom Generated_Groups_Extend General_Auxiliary
begin

subsection ‹Finite groups›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Finite abelian groups›

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

locale finite_comm_group = finite_group + comm_group

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

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

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


subsection ‹Cyclic groups›

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

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

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

text ‹Every cyclic group is commutative/abelian.›

sublocale cyclic_group ⊆ comm_group
proof(unfold_locales)
  fix x y
  assume "x ∈ carrier G" "y ∈ carrier G"
  then obtain a b where ab:"x = gen [^] (a::int)" "y = gen [^] (b::int)"
    using elem_is_gen_pow by presburger
  then have "x ⊗ y = gen [^] (a + b)" by (simp add: int_pow_mult)                 
  also have "… = y ⊗ x" using ab int_pow_mult
    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 (G⦇carrier := generate G {a}⦈) a"
proof (intro group.cyclic_groupI0)
  show "group (G⦇carrier := generate G {a}⦈)"
    by (intro subgroup.subgroup_is_group group.generate_is_subgroup, use assms in simp_all)
  show "a ∈ carrier (G⦇carrier := generate G {a}⦈)" using generate.incl[of a "{a}"] by auto
  show "carrier (G⦇carrier := generate G {a}⦈) = generate (G⦇carrier := generate G {a}⦈) {a}"
    using assms
    by (simp add: generate_consistent generate.incl group.generate_is_subgroup)
qed

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

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

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

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

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

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

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

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


subsection ‹Finite cyclic groups›

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

locale finite_cyclic_group = finite_group + cyclic_group

sublocale finite_cyclic_group ⊆ finite_comm_group
  by unfold_locales

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

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

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

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

subsection ‹‹get_exp› - discrete logarithm›

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

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

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

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

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

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

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

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

text ‹One well-known logarithmic identity.›

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

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

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

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

lemma (in cyclic_group) iso_cyclic_groups_same_order:
  assumes "cyclic_group H h" "order G = order H"
  shows "G ≅ H"
proof(intro is_isoI)
  interpret H: cyclic_group H h by fact
  define f where "f = (λa. h [^]⇘H⇙ get_exp gen a)"
  from assms(2) have o: "ord gen = H.ord h" using ord_gen_is_group_order H.ord_gen_is_group_order
    by simp
  have "∀k ∈ (UNIV::int set). f (gen [^] k) = h [^]⇘H⇙ k"
  proof
    fix k
    assume k: "k ∈ (UNIV::int set)"
    have "gen [^] k = gen [^] (SOME x::int. gen [^] k = gen [^] x)"
      by(intro someI_ex[of "λx::int. gen [^] k = gen [^] x"]; blast)
    moreover have "(SOME x::int. gen [^] k = gen [^] x) = (SOME x::int. h [^]⇘H⇙ k = h [^]⇘H⇙ x)"
    proof -
      have "gen [^] k = gen [^] x ⟷ h [^]⇘H⇙ k = h [^]⇘H⇙ x" for x::int
        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