# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554292527 -3600
# Node ID 733e256ecdf3654f97462c059fc04c96cedc57dd
# Parent  3374d16efc61156c9ea7d9aed08dd6c5e54e50e5
new group theory material, mostly ported from HOL Light

diff -r 3374d16efc61 -r 733e256ecdf3 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed Apr 03 12:55:27 2019 +0100
@@ -1061,6 +1061,26 @@
   apply (simp add: kernel_def)
   done
 
+lemma iso_kernel_image:
+  assumes "group G" "group H"
+  shows "f \<in> iso G H \<longleftrightarrow> f \<in> hom G H \<and> kernel G H f = {\<one>\<^bsub>G\<^esub>} \<and> f ` carrier G = carrier H"
+    (is "?lhs = ?rhs")
+proof (intro iffI conjI)
+  assume f: ?lhs
+  show "f \<in> hom G H"
+    using Group.iso_iff f by blast
+  show "kernel G H f = {\<one>\<^bsub>G\<^esub>}"
+    using assms f Group.group_def hom_one
+    by (fastforce simp add: kernel_def iso_iff_mon_epi mon_iff_hom_one set_eq_iff)
+  show "f ` carrier G = carrier H"
+    by (meson Group.iso_iff f)
+next
+  assume ?rhs
+  with assms show ?lhs
+    by (auto simp: kernel_def iso_def bij_betw_def inj_on_one_iff')
+qed
+
+
 lemma (in group_hom) FactGroup_nonempty:
   assumes X: "X \<in> carrier (G Mod kernel G H h)"
   shows "X \<noteq> {}"
@@ -1083,7 +1103,7 @@
   proof -
     have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> N"
       using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
-         subgroup.rcos_module_imp that by fastforce
+         subgroup.rcos_module_imp that by metis 
     with h have xy: "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> kernel G H h"
       by blast
     have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
@@ -1221,7 +1241,6 @@
     using A G.inv_equality G.inv_inv by blast
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) inj_iff_trivial_ker:
   shows "inj_on h (carrier G) \<longleftrightarrow> kernel G H h = { \<one> }"
 proof
@@ -1236,7 +1255,6 @@
     using trivial_ker_imp_inj by simp
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) induced_group_hom':
   assumes "subgroup I G" shows "group_hom (G \<lparr> carrier := I \<rparr>) H h"
 proof -
@@ -1247,13 +1265,11 @@
     unfolding group_hom_def group_hom_axioms_def by auto
 qed
 
-(* NEW ========================================================================== *)
 lemma (in group_hom) inj_on_subgroup_iff_trivial_ker:
   assumes "subgroup I G"
   shows "inj_on h I \<longleftrightarrow> kernel (G \<lparr> carrier := I \<rparr>) H h = { \<one> }"
   using group_hom.inj_iff_trivial_ker[OF induced_group_hom'[OF assms]] by simp
 
-(* NEW ========================================================================== *)
 lemma set_mult_hom:
   assumes "h \<in> hom G H" "I \<subseteq> carrier G" and "J \<subseteq> carrier G"
   shows "h ` (I <#>\<^bsub>G\<^esub> J) = (h ` I) <#>\<^bsub>H\<^esub> (h ` J)"
@@ -1281,13 +1297,11 @@
   qed
 qed
 
-(* NEW ========================================================================== *)
 corollary coset_hom:
   assumes "h \<in> hom G H" "I \<subseteq> carrier G" "a \<in> carrier G"
   shows "h ` (a <#\<^bsub>G\<^esub> I) = h a <#\<^bsub>H\<^esub> (h ` I)" and "h ` (I #>\<^bsub>G\<^esub> a) = (h ` I) #>\<^bsub>H\<^esub> h a"
   unfolding l_coset_eq_set_mult r_coset_eq_set_mult using assms set_mult_hom[OF assms(1)] by auto
 
-(* NEW ========================================================================== *)
 corollary (in group_hom) set_mult_ker_hom:
   assumes "I \<subseteq> carrier G"
   shows "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I"
@@ -1305,8 +1319,145 @@
     using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+
 qed
 
+subsubsection\<open>Trivial homomorphisms\<close>
 
-subsection \<open>Theorems about Factor Groups and Direct product\<close>
+definition trivial_homomorphism where
+ "trivial_homomorphism G H f \<equiv> f \<in> hom G H \<and> (\<forall>x \<in> carrier G. f x = one H)"
+
+lemma trivial_homomorphism_kernel:
+   "trivial_homomorphism G H f \<longleftrightarrow> f \<in> hom G H \<and> kernel G H f = carrier G"
+  by (auto simp: trivial_homomorphism_def kernel_def)
+
+lemma (in group) trivial_homomorphism_image:
+   "trivial_homomorphism G H f \<longleftrightarrow> f \<in> hom G H \<and> f ` carrier G = {one H}"
+  by (auto simp: trivial_homomorphism_def) (metis one_closed rev_image_eqI)
+
+
+subsection \<open>Image kernel theorems\<close>
+
+lemma group_Int_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and "inj_on (g \<circ> f) (carrier G)" "group G" "group H" "group K"
+  shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+proof -
+  have "(f ` carrier G) \<inter> (kernel H K g) \<subseteq> {\<one>\<^bsub>H\<^esub>}"
+    using assms
+    apply (clarsimp simp: kernel_def o_def)
+    by (metis group.is_monoid hom_one inj_on_eq_iff monoid.one_closed)
+  moreover have "one H \<in> f ` carrier G"
+    by (metis f \<open>group G\<close> \<open>group H\<close> group.is_monoid hom_one image_iff monoid.one_closed)
+  moreover have "one H \<in> kernel H K g"
+    apply (simp add: kernel_def)
+    using g group.is_monoid hom_one \<open>group H\<close> \<open>group K\<close> by blast
+  ultimately show ?thesis
+    by blast
+qed
+
+
+lemma group_sum_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> f) ` (carrier G) = carrier K"
+     and "group G" "group H" "group K"
+  shows "set_mult H (f ` carrier G) (kernel H K g) = carrier H" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (auto simp: kernel_def set_mult_def)
+    by (meson Group.group_def assms(5) f hom_carrier image_eqI monoid.m_closed subset_iff)
+  have "\<exists>x\<in>carrier G. \<exists>z. z \<in> carrier H \<and> g z = \<one>\<^bsub>K\<^esub> \<and> y = f x \<otimes>\<^bsub>H\<^esub> z"
+    if y: "y \<in> carrier H" for y
+  proof -
+    have "g y \<in> carrier K"
+      using g hom_carrier that by blast
+    with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+      by (metis image_iff)
+    with assms have "inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y \<in> carrier H"
+      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+    moreover
+    have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = \<one>\<^bsub>K\<^esub>"
+    proof -
+      have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+      then have "g (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y) = g (inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>K\<^esub> g y"
+        by (simp add: hom_mult [OF g] y)
+      also have "\<dots> = inv\<^bsub>K\<^esub> (g (f x)) \<otimes>\<^bsub>K\<^esub> g y"
+        using assms x(1)
+        by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
+      also have "\<dots> = \<one>\<^bsub>K\<^esub>"
+        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2) by fastforce
+      finally show ?thesis .
+    qed
+    moreover
+    have "y = f x \<otimes>\<^bsub>H\<^esub> (inv\<^bsub>H\<^esub> f x \<otimes>\<^bsub>H\<^esub> y)"
+      using x y
+      by (metis (no_types, hide_lams) assms(5) f group.inv_solve_left group.subgroup_self hom_carrier image_subset_iff subgroup_def that)
+    ultimately
+    show ?thesis
+      using x y by force
+  qed
+  then show "?rhs \<subseteq> ?lhs"
+    by (auto simp: kernel_def set_mult_def)
+qed
+
+
+lemma group_sum_ker_image:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and eq: "(g \<circ> f) ` (carrier G) = carrier K"
+     and "group G" "group H" "group K"
+   shows "set_mult H (kernel H K g) (f ` carrier G) = carrier H" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (auto simp: kernel_def set_mult_def)
+    by (meson Group.group_def \<open>group H\<close> f hom_carrier image_eqI monoid.m_closed subset_iff)
+  have "\<exists>w\<in>carrier H. \<exists>x \<in> carrier G. g w = \<one>\<^bsub>K\<^esub> \<and> y = w \<otimes>\<^bsub>H\<^esub> f x"
+    if y: "y \<in> carrier H" for y
+  proof -
+    have "g y \<in> carrier K"
+      using g hom_carrier that by blast
+    with assms obtain x where x: "x \<in> carrier G" "(g \<circ> f) x = g y"
+      by (metis image_iff)
+    with assms have carr: "(y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<in> carrier H"
+      by (metis group.subgroup_self hom_carrier image_subset_iff subgroup_def y)
+    moreover
+    have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = \<one>\<^bsub>K\<^esub>"
+    proof -
+      have "inv\<^bsub>H\<^esub> f x \<in> carrier H"
+        by (meson \<open>group H\<close> f group.inv_closed hom_carrier image_subset_iff x(1))
+      then have "g (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) = g y \<otimes>\<^bsub>K\<^esub> g (inv\<^bsub>H\<^esub> f x)"
+        by (simp add: hom_mult [OF g] y)
+      also have "\<dots> = g y \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> (g (f x))"
+        using assms x(1)
+        by (metis (mono_tags, lifting) group_hom.hom_inv group_hom.intro group_hom_axioms.intro hom_carrier image_subset_iff)
+      also have "\<dots> = \<one>\<^bsub>K\<^esub>"
+        using \<open>g y \<in> carrier K\<close> assms(6) group.l_inv x(2)
+        by (simp add: group.r_inv)
+      finally show ?thesis .
+    qed
+    moreover
+    have "y = (y \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> f x) \<otimes>\<^bsub>H\<^esub> f x"
+      using x y by (meson \<open>group H\<close> carr f group.inv_solve_right hom_carrier image_subset_iff)
+    ultimately
+    show ?thesis
+      using x y by force
+  qed
+  then show "?rhs \<subseteq> ?lhs"
+    by (force simp: kernel_def set_mult_def)
+qed
+
+lemma group_semidirect_sum_ker_image:
+  assumes "(g \<circ> f) \<in> iso G K" "f \<in> hom G H" "g \<in> hom H K" "group G" "group H" "group K"
+  shows "(kernel H K g) \<inter> (f ` carrier G) = {\<one>\<^bsub>H\<^esub>}"
+        "kernel H K g <#>\<^bsub>H\<^esub> (f ` carrier G) = carrier H"
+  using assms
+  by (simp_all add: iso_iff_mon_epi group_Int_image_ker group_sum_ker_image epi_def mon_def Int_commute [of "kernel H K g"])
+
+lemma group_semidirect_sum_image_ker:
+  assumes f: "f \<in> hom G H" and g: "g \<in> hom H K" and iso: "(g \<circ> f) \<in> iso G K"
+     and "group G" "group H" "group K"
+   shows "(f ` carrier G) \<inter> (kernel H K g) = {\<one>\<^bsub>H\<^esub>}"
+          "f ` carrier G <#>\<^bsub>H\<^esub> (kernel H K g) = carrier H"
+  using group_Int_image_ker [OF f g] group_sum_image_ker [OF f g] assms
+  by (simp_all add: iso_def bij_betw_def)
+
+
+
+subsection \<open>Factor Groups and Direct product\<close>
 
 lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   assumes "group K"
diff -r 3374d16efc61 -r 733e256ecdf3 src/HOL/Algebra/Elementary_Groups.thy
--- a/src/HOL/Algebra/Elementary_Groups.thy	Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Elementary_Groups.thy	Wed Apr 03 12:55:27 2019 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Elementary_Groups
-imports Generated_Groups
+imports Generated_Groups Multiplicative_Group "HOL-Library.Infinite_Set"
 begin
 
 subsection\<open>Direct sum/product lemmas\<close>
@@ -379,4 +379,289 @@
    "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
   by (rule homI) (auto simp: int_pow_mult)
 
+subsection\<open>Additive group of integers modulo n (n = 0 gives just the integers)\<close>
+
+definition integer_mod_group :: "nat \<Rightarrow> int monoid"
+  where
+  "integer_mod_group n \<equiv>
+     if n = 0 then integer_group
+     else \<lparr>carrier = {0..<int n}, monoid.mult = (\<lambda>x y. (x+y) mod int n), one = 0\<rparr>"
+
+lemma carrier_integer_mod_group:
+  "carrier(integer_mod_group n) = (if n=0 then UNIV else {0..<int n})"
+  by (simp add: integer_mod_group_def)
+
+lemma one_integer_mod_group[simp]: "one(integer_mod_group n) = 0"
+  by (simp add: integer_mod_group_def)
+
+lemma mult_integer_mod_group[simp]: "monoid.mult(integer_mod_group n) = (\<lambda>x y. (x + y) mod int n)"
+  by (simp add: integer_mod_group_def integer_group_def)
+
+lemma group_integer_mod_group [simp]: "group (integer_mod_group n)"
+proof -
+  have *: "\<exists>y\<ge>0. y < int n \<and> (y + x) mod int n = 0" if "x < int n" "0 \<le> x" for x
+  proof (cases "x=0")
+    case False
+    with that show ?thesis
+      by (rule_tac x="int n - x" in exI) auto
+  qed (use that in auto)
+  show ?thesis
+    apply (rule groupI)
+        apply (auto simp: integer_mod_group_def Bex_def *, presburger+)
+    done
+qed
+
+lemma inv_integer_mod_group[simp]:
+  "x \<in> carrier (integer_mod_group n) \<Longrightarrow> m_inv(integer_mod_group n) x = (-x) mod int n"
+  by (rule group.inv_equality [OF group_integer_mod_group]) (auto simp: integer_mod_group_def add.commute mod_add_right_eq)
+
+
+lemma pow_integer_mod_group [simp]:
+  fixes m::nat
+  shows "pow (integer_mod_group n) x m = (int m * x) mod int n"
+proof (cases "n=0")
+  case False
+  show ?thesis
+    by (induction m) (auto simp: add.commute mod_add_right_eq distrib_left mult.commute)
+qed (simp add: integer_mod_group_def)
+
+lemma int_pow_integer_mod_group:
+  "pow (integer_mod_group n) x m = (m * x) mod int n"
+proof -
+  have "inv\<^bsub>integer_mod_group n\<^esub> (- (m * x) mod int n) = m * x mod int n"
+    by (simp add: carrier_integer_mod_group mod_minus_eq)
+  then show ?thesis
+    by (simp add: int_pow_def2)
+qed
+
+lemma abelian_integer_mod_group [simp]: "comm_group(integer_mod_group n)"
+  by (simp add: add.commute group.group_comm_groupI)
+
+lemma integer_mod_group_0 [simp]: "0 \<in> carrier(integer_mod_group n)"
+  by (simp add: integer_mod_group_def)
+
+lemma integer_mod_group_1 [simp]: "1 \<in> carrier(integer_mod_group n) \<longleftrightarrow> (n \<noteq> 1)"
+  by (auto simp: integer_mod_group_def)
+
+lemma trivial_integer_mod_group: "trivial_group(integer_mod_group n) \<longleftrightarrow> n = 1"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+  by (simp add: trivial_group_def carrier_integer_mod_group set_eq_iff split: if_split_asm) (presburger+)
+next
+  assume ?rhs
+  then show ?lhs
+    by (force simp: trivial_group_def carrier_integer_mod_group)
+qed
+
+
+subsection\<open>Cyclic groups\<close>
+
+lemma (in group) subgroup_of_powers:
+  "x \<in> carrier G \<Longrightarrow> subgroup (range (\<lambda>n::int. x [^] n)) G"
+  apply (auto simp: subgroup_def image_iff simp flip: int_pow_mult int_pow_neg)
+  apply (metis group.int_pow_diff int_pow_closed is_group r_inv)
+  done
+
+lemma (in group) carrier_subgroup_generated_by_singleton:
+  assumes "x \<in> carrier G"
+  shows "carrier(subgroup_generated G {x}) = (range (\<lambda>n::int. x [^] n))"
+proof
+  show "carrier (subgroup_generated G {x}) \<subseteq> range (\<lambda>n::int. x [^] n)"
+  proof (rule subgroup_generated_minimal)
+    show "subgroup (range (\<lambda>n::int. x [^] n)) G"
+      using assms subgroup_of_powers by blast
+    show "{x} \<subseteq> range (\<lambda>n::int. x [^] n)"
+      by clarify (metis assms int_pow_1 range_eqI)
+  qed
+  have x: "x \<in> carrier (subgroup_generated G {x})"
+    using assms subgroup_generated_subset_carrier_subset by auto
+  show "range (\<lambda>n::int. x [^] n) \<subseteq> carrier (subgroup_generated G {x})"
+  proof clarify
+    fix n :: "int"
+    show "x [^] n \<in> carrier (subgroup_generated G {x})"
+        by (simp add: x subgroup_int_pow_closed subgroup_subgroup_generated)
+  qed
+qed
+
+
+definition cyclic_group
+  where "cyclic_group G \<equiv> \<exists>x \<in> carrier G. subgroup_generated G {x} = G"
+
+lemma (in group) cyclic_group:
+  "cyclic_group G \<longleftrightarrow> (\<exists>x \<in> carrier G. carrier G = range (\<lambda>n::int. x [^] n))"
+proof -
+  have "\<And>x. \<lbrakk>x \<in> carrier G; carrier G = range (\<lambda>n::int. x [^] n)\<rbrakk>
+         \<Longrightarrow> \<exists>x\<in>carrier G. subgroup_generated G {x} = G"
+    by (rule_tac x=x in bexI) (auto simp: generate_pow subgroup_generated_def intro!: monoid.equality)
+  then show ?thesis
+    unfolding cyclic_group_def
+    using carrier_subgroup_generated_by_singleton by fastforce
+qed
+
+lemma cyclic_integer_group [simp]: "cyclic_group integer_group"
+proof -
+  have *: "int n \<in> generate integer_group {1}" for n
+  proof (induction n)
+    case 0
+    then show ?case
+    using generate.simps by force
+  next
+    case (Suc n)
+    then show ?case
+    by simp (metis generate.simps insert_subset integer_group_def monoid.simps(1) subsetI)
+  qed
+  have **: "i \<in> generate integer_group {1}" for i
+  proof (cases i rule: int_cases)
+    case (nonneg n)
+    then show ?thesis
+      by (simp add: *)
+  next
+    case (neg n)
+    then have "-i \<in> generate integer_group {1}"
+      by (metis "*" add.inverse_inverse)
+    then have "- (-i) \<in> generate integer_group {1}"
+      by (metis UNIV_I group.generate_m_inv_closed group_integer_group integer_group_def inv_integer_group partial_object.select_convs(1) subsetI)
+    then show ?thesis
+      by simp
+  qed
+  show ?thesis
+    unfolding cyclic_group_def
+    by (rule_tac x=1 in bexI)
+       (auto simp: carrier_subgroup_generated ** intro: monoid.equality)
+qed
+
+lemma nontrivial_integer_group [simp]: "\<not> trivial_group integer_group"
+  using integer_mod_group_def trivial_integer_mod_group by presburger
+
+
+lemma (in group) cyclic_imp_abelian_group:
+  "cyclic_group G \<Longrightarrow> comm_group G"
+  apply (auto simp: cyclic_group comm_group_def is_group intro!: monoid_comm_monoidI)
+  apply (metis add.commute int_pow_mult rangeI)
+  done
+
+lemma trivial_imp_cyclic_group:
+   "trivial_group G \<Longrightarrow> cyclic_group G"
+  by (metis cyclic_group_def group.subgroup_generated_group_carrier insertI1 trivial_group_def)
+
+lemma (in group) cyclic_group_alt:
+   "cyclic_group G \<longleftrightarrow> (\<exists>x. subgroup_generated G {x} = G)"
+proof safe
+  fix x
+  assume *: "subgroup_generated G {x} = G"
+  show "cyclic_group G"
+  proof (cases "x \<in> carrier G")
+    case True
+    then show ?thesis
+      using \<open>subgroup_generated G {x} = G\<close> cyclic_group_def by blast
+  next
+    case False
+    then show ?thesis
+      by (metis "*" Int_empty_right Int_insert_right_if0 carrier_subgroup_generated generate_empty trivial_group trivial_imp_cyclic_group)
+  qed
+qed (auto simp: cyclic_group_def)
+
+lemma (in group) cyclic_group_generated:
+  "cyclic_group (subgroup_generated G {x})"
+  using group.cyclic_group_alt group_subgroup_generated subgroup_generated2 by blast
+
+lemma (in group) cyclic_group_epimorphic_image:
+  assumes "h \<in> epi G H" "cyclic_group G" "group H"
+  shows "cyclic_group H"
+proof -
+  interpret h: group_hom
+    using assms
+    by (simp add: group_hom_def group_hom_axioms_def is_group epi_def)
+  obtain x where "x \<in> carrier G" and x: "carrier G = range (\<lambda>n::int. x [^] n)" and eq: "carrier H = h ` carrier G"
+    using assms by (auto simp: cyclic_group epi_def)
+  have "h ` carrier G = range (\<lambda>n::int. h x [^]\<^bsub>H\<^esub> n)"
+    by (metis (no_types, lifting) \<open>x \<in> carrier G\<close> h.hom_int_pow image_cong image_image x)
+  then show ?thesis
+    using \<open>x \<in> carrier G\<close> eq h.cyclic_group by blast
+qed
+
+lemma isomorphic_group_cyclicity:
+   "\<lbrakk>G \<cong> H; group G; group H\<rbrakk> \<Longrightarrow> cyclic_group G \<longleftrightarrow> cyclic_group H"
+  by (meson ex_in_conv group.cyclic_group_epimorphic_image group.iso_sym is_iso_def iso_iff_mon_epi)
+
+
+lemma (in group)
+  assumes "x \<in> carrier G"
+  shows finite_cyclic_subgroup:
+        "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> x [^] n = \<one>)" (is "?fin \<longleftrightarrow> ?nat1")
+    and infinite_cyclic_subgroup:
+        "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>m n::nat. x [^] m = x [^] n \<longrightarrow> m = n)" (is "\<not> ?fin \<longleftrightarrow> ?nateq")
+    and finite_cyclic_subgroup_int:
+        "finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<exists>i::int. i \<noteq> 0 \<and> x [^] i = \<one>)" (is "?fin \<longleftrightarrow> ?int1")
+    and infinite_cyclic_subgroup_int:
+        "infinite(carrier(subgroup_generated G {x})) \<longleftrightarrow> (\<forall>i j::int. x [^] i = x [^] j \<longrightarrow> i = j)" (is "\<not> ?fin \<longleftrightarrow> ?inteq")
+proof -
+  have 1: "\<not> ?fin" if ?nateq
+  proof -
+    have "infinite (range (\<lambda>n::nat. x [^] n))"
+      using that range_inj_infinite [of "(\<lambda>n::nat. x [^] n)"] by (auto simp: inj_on_def)
+    moreover have "range (\<lambda>n::nat. x [^] n) \<subseteq> range (\<lambda>i::int. x [^] i)"
+      apply clarify
+      by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
+    ultimately show ?thesis
+      using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
+  qed
+  have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
+    using eq [of "int m" "int n"]
+    by (simp add: int_pow_int mn)
+  have 3: ?nat1 if non: "\<not> ?inteq"
+  proof -
+    obtain i j::int where eq: "x [^] i = x [^] j" and "i \<noteq> j"
+      using non by auto
+    show ?thesis
+    proof (cases i j rule: linorder_cases)
+      case less
+      then have [simp]: "x [^] (j - i) = \<one>"
+        by (simp add: eq assms int_pow_diff)
+      show ?thesis
+        using less by (rule_tac x="nat (j-i)" in exI) auto
+    next
+      case greater
+      then have [simp]: "x [^] (i - j) = \<one>"
+        by (simp add: eq assms int_pow_diff)
+      then show ?thesis
+        using greater by (rule_tac x="nat (i-j)" in exI) auto
+    qed (use \<open>i \<noteq> j\<close> in auto)
+  qed
+  have 4: "\<exists>i::int. (i \<noteq> 0) \<and> x [^] i = \<one>" if "n \<noteq> 0" "x [^] n = \<one>" for n::nat
+    apply (rule_tac x="int n" in exI)
+    by (simp add: int_pow_int that)
+  have 5: "finite (carrier (subgroup_generated G {x}))" if "i \<noteq> 0" and 1: "x [^] i = \<one>" for i::int
+  proof -
+    obtain n::nat where n: "n > 0" "x [^] n = \<one>"
+      using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
+    have "x [^] a \<in> ([^]) x ` {0..<n}" for a::int
+    proof
+      show "x [^] a = x [^] nat (a mod int n)"
+        using n
+        by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
+      show "nat (a mod int n) \<in> {0..<n}"
+        using n  apply (simp add:  split: split_nat)
+        using Euclidean_Division.pos_mod_bound by presburger
+    qed
+    then have "carrier (subgroup_generated G {x}) \<subseteq> ([^]) x ` {0..<n}"
+      using carrier_subgroup_generated_by_singleton [OF assms] by auto
+    then show ?thesis
+      using finite_surj by blast
+  qed
+  show "?fin \<longleftrightarrow> ?nat1" "\<not> ?fin \<longleftrightarrow> ?nateq" "?fin \<longleftrightarrow> ?int1" "\<not> ?fin \<longleftrightarrow> ?inteq"
+    using 1 2 3 4 5 by meson+
+qed
+
+lemma (in group) finite_cyclic_subgroup_order:
+   "x \<in> carrier G \<Longrightarrow> finite(carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x \<noteq> 0"
+  by (simp add: finite_cyclic_subgroup ord_eq_0)
+
+lemma (in group) infinite_cyclic_subgroup_order:
+   "x \<in> carrier G \<Longrightarrow> infinite (carrier(subgroup_generated G {x})) \<longleftrightarrow> ord x = 0"
+  by (simp add: finite_cyclic_subgroup_order)
+
+
 end
diff -r 3374d16efc61 -r 733e256ecdf3 src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Wed Apr 03 12:55:27 2019 +0100
@@ -2,12 +2,14 @@
     Author:     Paulo Emílio de Vilhena
 *)
 
+section \<open>Generated Groups\<close>
+
 theory Generated_Groups
   imports Group Coset
   
 begin
 
-section \<open>Generated Groups\<close>
+subsection \<open>Generated Groups\<close>
 
 inductive_set generate :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
   for G and H where
@@ -17,7 +19,7 @@
   | eng:  "h1 \<in> generate G H \<Longrightarrow> h2 \<in> generate G H \<Longrightarrow> h1 \<otimes>\<^bsub>G\<^esub> h2 \<in> generate G H"
 
 
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
 
 lemma (in group) generate_consistent:
   assumes "K \<subseteq> H" "subgroup H G" shows "generate (G \<lparr> carrier := H \<rparr>) K = generate G K"
@@ -195,9 +197,9 @@
 qed
 
 
-section \<open>Derived Subgroup\<close>
+subsection \<open>Derived Subgroup\<close>
 
-subsection \<open>Definitions\<close>
+subsubsection \<open>Definitions\<close>
 
 abbreviation derived_set :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where "derived_set G H \<equiv>
@@ -207,7 +209,7 @@
   "derived G H = generate G (derived_set G H)"
 
 
-subsection \<open>Basic Properties\<close>
+subsubsection \<open>Basic Properties\<close>
 
 lemma (in group) derived_set_incl:
   assumes "K \<subseteq> H" "subgroup H G" shows "derived_set G K \<subseteq> H"
@@ -444,7 +446,7 @@
   using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)
 
 
-subsection \<open>Generated subgroup of a group\<close>
+subsubsection \<open>Generated subgroup of a group\<close>
 
 definition subgroup_generated :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> ('a, 'b) monoid_scheme"
   where "subgroup_generated G S = G\<lparr>carrier := generate G (carrier G \<inter> S)\<rparr>"
@@ -600,4 +602,114 @@
   "kernel G (subgroup_generated H S) f = kernel G H f"
   by (simp add: kernel_def)
 
+subsection \<open>And homomorphisms\<close>
+
+lemma (in group) hom_from_subgroup_generated:
+   "h \<in> hom G H \<Longrightarrow> h \<in> hom(subgroup_generated G A) H"
+  apply (simp add: hom_def carrier_subgroup_generated Pi_iff)
+  apply (metis group.generate_in_carrier inf_le1 is_group)
+  done
+
+lemma hom_into_subgroup:
+   "\<lbrakk>h \<in> hom G G'; h ` (carrier G) \<subseteq> H\<rbrakk> \<Longrightarrow> h \<in> hom G (subgroup_generated G' H)"
+  by (auto simp: hom_def carrier_subgroup_generated Pi_iff generate.incl image_subset_iff)
+
+lemma hom_into_subgroup_eq_gen:
+    "group G \<Longrightarrow>
+     h \<in> hom K (subgroup_generated G H)
+ \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> carrier(subgroup_generated G H)"
+  using group.carrier_subgroup_generated_subset [of G H] by (auto simp: hom_def)
+
+lemma hom_into_subgroup_eq:
+   "\<lbrakk>subgroup H G; group G\<rbrakk>
+    \<Longrightarrow> (h \<in> hom K (subgroup_generated G H) \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> H)"
+  by (simp add: hom_into_subgroup_eq_gen image_subset_iff subgroup.carrier_subgroup_generated_subgroup)
+
+lemma (in group_hom) hom_between_subgroups:
+  assumes "h ` A \<subseteq> B"
+  shows "h \<in> hom (subgroup_generated G A) (subgroup_generated H B)"
+proof -
+  have [simp]: "group G" "group H"
+    by (simp_all add: G.is_group H.is_group)
+  have "x \<in> generate G (carrier G \<inter> A) \<Longrightarrow> h x \<in> generate H (carrier H \<inter> B)" for x
+  proof (induction x rule: generate.induct)
+    case (incl h)
+    then show ?case
+      by (meson IntE IntI assms generate.incl hom_closed image_subset_iff)
+  next
+    case (inv h)
+    then show ?case
+      by (metis G.inv_closed G.inv_inv IntE IntI assms generate.simps hom_inv image_subset_iff local.inv_closed)
+  next
+    case (eng h1 h2)
+    then show ?case
+      by (metis G.generate_in_carrier generate.simps inf.cobounded1 local.hom_mult)
+  qed (auto simp: generate.intros)
+  then have "h ` carrier (subgroup_generated G A) \<subseteq> carrier (subgroup_generated H B)"
+    using group.carrier_subgroup_generated_subset [of G A]
+    by (auto simp: carrier_subgroup_generated)
+  then show ?thesis
+    by (simp add: hom_into_subgroup_eq_gen group.hom_from_subgroup_generated homh)
+qed
+
+lemma (in group_hom) subgroup_generated_by_image:
+  assumes "S \<subseteq> carrier G"
+  shows "carrier (subgroup_generated H (h ` S)) = h ` (carrier(subgroup_generated G S))"
+proof
+  have "x \<in> generate H (carrier H \<inter> h ` S) \<Longrightarrow> x \<in> h ` generate G (carrier G \<inter> S)" for x
+  proof (erule generate.induct)
+    show "\<one>\<^bsub>H\<^esub> \<in> h ` generate G (carrier G \<inter> S)"
+      using generate.one by force
+  next
+    fix f
+    assume "f \<in> carrier H \<inter> h ` S"
+    with assms show "f \<in> h ` generate G (carrier G \<inter> S)" "inv\<^bsub>H\<^esub> f \<in> h ` generate G (carrier G \<inter> S)"
+       apply (auto simp: Int_absorb1 generate.incl)
+      apply (metis generate.simps hom_inv imageI subsetCE)
+      done
+  next
+    fix h1 h2
+    assume
+      "h1 \<in> generate H (carrier H \<inter> h ` S)" "h1 \<in> h ` generate G (carrier G \<inter> S)"
+      "h2 \<in> generate H (carrier H \<inter> h ` S)" "h2 \<in> h ` generate G (carrier G \<inter> S)"
+    then show "h1 \<otimes>\<^bsub>H\<^esub> h2 \<in> h ` generate G (carrier G \<inter> S)"
+      using H.subgroupE(4) group.generate_is_subgroup subgroup_img_is_subgroup
+      by (simp add: G.generate_is_subgroup)
+  qed
+  then
+  show "carrier (subgroup_generated H (h ` S)) \<subseteq> h ` carrier (subgroup_generated G S)"
+    by (auto simp: carrier_subgroup_generated)
+next
+  have "h ` S \<subseteq> carrier H"
+    by (metis (no_types) assms hom_closed image_subset_iff subsetCE)
+  then show "h ` carrier (subgroup_generated G S) \<subseteq> carrier (subgroup_generated H (h ` S))"
+    apply (clarsimp simp: carrier_subgroup_generated)
+    by (metis Int_absorb1 assms generate_img imageI)
+qed
+
+lemma (in group_hom) iso_between_subgroups:
+  assumes "h \<in> iso G H" "S \<subseteq> carrier G" "h ` S = T"
+  shows "h \<in> iso (subgroup_generated G S) (subgroup_generated H T)"
+  using assms
+  by (metis G.carrier_subgroup_generated_subset Group.iso_iff hom_between_subgroups inj_on_subset subgroup_generated_by_image subsetI)
+
+lemma (in group) subgroup_generated_group_carrier:
+  "subgroup_generated G (carrier G) = G"
+proof (rule monoid.equality)
+  show "carrier (subgroup_generated G (carrier G)) = carrier G"
+    by (simp add: subgroup.carrier_subgroup_generated_subgroup subgroup_self)
+qed (auto simp: subgroup_generated_def)
+
+lemma iso_onto_image:
+  assumes "group G" "group H"
+  shows
+   "f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> hom G H \<and> inj_on f (carrier G)"
+  using assms
+  apply (auto simp: iso_def bij_betw_def hom_into_subgroup_eq_gen carrier_subgroup_generated hom_carrier generate.incl Int_absorb1 Int_absorb2)
+  by (metis group.generateI group.subgroupE(1) group.subgroup_self group_hom.generate_img group_hom.intro group_hom_axioms.intro)
+
+lemma (in group) iso_onto_image:
+   "group H \<Longrightarrow> f \<in> iso G (subgroup_generated H (f ` carrier G)) \<longleftrightarrow> f \<in> mon G H"
+  by (simp add: mon_def epi_def hom_into_subgroup_eq_gen iso_onto_image)
+
 end
\ No newline at end of file
diff -r 3374d16efc61 -r 733e256ecdf3 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Apr 03 00:07:26 2019 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Apr 03 12:55:27 2019 +0100
@@ -186,7 +186,10 @@
 locale group = monoid +
   assumes Units: "carrier G <= Units G"
 
-lemma (in group) is_group: "group G" by (rule group_axioms)
+lemma (in group) is_group [iff]: "group G" by (rule group_axioms)
+
+lemma (in group) is_monoid [iff]: "monoid G"
+  by (rule monoid_axioms)
 
 theorem groupI:
   fixes G (structure)
@@ -825,6 +828,9 @@
 lemma mult_DirProd [simp]: "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   by (simp add: DirProd_def)
 
+lemma mult_DirProd': "x \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> y = (fst x \<otimes>\<^bsub>G\<^esub> fst y, snd x \<otimes>\<^bsub>H\<^esub> snd y)"
+  by (subst mult_DirProd [symmetric]) simp
+
 lemma DirProd_assoc: "(G \<times>\<times> H \<times>\<times> I) = (G \<times>\<times> (H \<times>\<times> I))"
   by auto
 
@@ -858,7 +864,7 @@
   ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
 qed
 
-subsection \<open>Homomorphisms and Isomorphisms\<close>
+subsection \<open>Homomorphisms (mono and epi) and Isomorphisms\<close>
 
 definition
   hom :: "_ => _ => ('a => 'b) set" where
@@ -923,6 +929,14 @@
 corollary iso_refl [simp]: "G \<cong> G"
   using iso_set_refl unfolding is_iso_def by auto
 
+lemma iso_iff:
+   "h \<in> iso G H \<longleftrightarrow> h \<in> hom G H \<and> h ` (carrier G) = carrier H \<and> inj_on h (carrier G)"
+  by (auto simp: iso_def hom_def bij_betw_def)
+
+lemma iso_imp_homomorphism:
+   "h \<in> iso G H \<Longrightarrow> h \<in> hom G H"
+  by (simp add: iso_iff)
+
 lemma trivial_hom:
    "group H \<Longrightarrow> (\<lambda>x. one H) \<in> hom G H"
   by (auto simp: hom_def Group.group_def)
@@ -965,7 +979,6 @@
     by (simp add: Group.iso_def bij_betw_inv_into h)
 qed
 
-
 corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
@@ -979,6 +992,50 @@
 lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
   using bij_betw_same_card  unfolding is_iso_def iso_def by auto
 
+lemma iso_finite: "G \<cong> H \<Longrightarrow> finite(carrier G) \<longleftrightarrow> finite(carrier H)"
+  by (auto simp: is_iso_def iso_def bij_betw_finite)
+
+lemma mon_compose:
+   "\<lbrakk>f \<in> mon G H; g \<in> mon H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> mon G K"
+  by (auto simp: mon_def intro: hom_compose comp_inj_on inj_on_subset [OF _ hom_carrier])
+
+lemma mon_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> mon G K\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+  using inj_on_imageI2 by (auto simp: mon_def)
+
+lemma epi_compose:
+   "\<lbrakk>f \<in> epi G H; g \<in> epi H K\<rbrakk> \<Longrightarrow> (g \<circ> f) \<in> epi G K"
+  using hom_compose by (force simp: epi_def hom_compose simp flip: image_image)
+
+lemma epi_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> epi G K\<rbrakk> \<Longrightarrow> g \<in> epi H K"
+  by (fastforce simp: epi_def hom_def Pi_iff image_def set_eq_iff)
+
+lemma iso_compose_rev:
+   "\<lbrakk>f \<in> hom G H; g \<in> hom H K; (g \<circ> f) \<in> iso G K\<rbrakk> \<Longrightarrow> f \<in> mon G H \<and> g \<in> epi H K"
+  unfolding iso_iff_mon_epi using mon_compose_rev epi_compose_rev by blast
+
+lemma epi_iso_compose_rev:
+  assumes "f \<in> epi G H" "g \<in> hom H K" "(g \<circ> f) \<in> iso G K"
+  shows "f \<in> iso G H \<and> g \<in> iso H K"
+proof
+  show "f \<in> iso G H"
+    by (metis (no_types, lifting) assms epi_def iso_compose_rev iso_iff_mon_epi mem_Collect_eq)
+  then have "f \<in> hom G H \<and> bij_betw f (carrier G) (carrier H)"
+    using Group.iso_def \<open>f \<in> Group.iso G H\<close> by blast
+  then have "bij_betw g (carrier H) (carrier K)"
+    using Group.iso_def assms(3) bij_betw_comp_iff by blast
+  then show "g \<in> iso H K"
+    using Group.iso_def assms(2) by blast
+qed
+
+lemma mon_left_invertible:
+   "\<lbrakk>f \<in> hom G H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> f \<in> mon G H"
+  by (simp add: mon_def inj_on_def) metis
+
+lemma epi_right_invertible:
+   "\<lbrakk>g \<in> hom H G; f \<in> carrier G \<rightarrow> carrier H; \<And>x. x \<in> carrier G \<Longrightarrow> g(f x) = x\<rbrakk> \<Longrightarrow> g \<in> epi H G"
+  by (force simp: Pi_iff epi_iff_subset image_subset_iff_funcset subset_iff)
 
 lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
@@ -1109,6 +1166,43 @@
   ultimately show ?thesis by simp
 qed
 
+subsubsection \<open>HOL Light's concept of an isomorphism pair\<close>
+
+definition group_isomorphisms
+  where
+ "group_isomorphisms G H f g \<equiv>
+        f \<in> hom G H \<and> g \<in> hom H G \<and>
+        (\<forall>x \<in> carrier G. g(f x) = x) \<and>
+        (\<forall>y \<in> carrier H. f(g y) = y)"
+
+lemma group_isomorphisms_sym: "group_isomorphisms G H f g \<Longrightarrow> group_isomorphisms H G g f"
+  by (auto simp: group_isomorphisms_def)
+
+lemma group_isomorphisms_imp_iso: "group_isomorphisms G H f g \<Longrightarrow> f \<in> iso G H"
+by (auto simp: iso_def inj_on_def image_def group_isomorphisms_def hom_def bij_betw_def Pi_iff, metis+)
+
+lemma (in group) iso_iff_group_isomorphisms:
+  "f \<in> iso G H \<longleftrightarrow> (\<exists>g. group_isomorphisms G H f g)"
+proof safe
+  show "\<exists>g. group_isomorphisms G H f g" if "f \<in> Group.iso G H"
+    unfolding group_isomorphisms_def
+  proof (intro exI conjI)
+    let ?g = "inv_into (carrier G) f"
+    show "\<forall>x\<in>carrier G. ?g (f x) = x"
+      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_left mem_Collect_eq that)
+    show "\<forall>y\<in>carrier H. f (?g y) = y"
+      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_right mem_Collect_eq that)
+  qed (use Group.iso_def iso_set_sym that in \<open>blast+\<close>)
+next
+  fix g
+  assume "group_isomorphisms G H f g"
+  then show "f \<in> Group.iso G H"
+    by (auto simp: iso_def group_isomorphisms_def hom_in_carrier intro: bij_betw_byWitness)
+qed
+
+
+subsubsection \<open>Involving direct products\<close>
+
 lemma DirProd_commute_iso_set:
   shows "(\<lambda>(x,y). (y,x)) \<in> iso (G \<times>\<times> H) (H \<times>\<times> G)"
   by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
@@ -1141,6 +1235,53 @@
   shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
   using DirProd_iso_set_trans assms unfolding is_iso_def by blast
 
+lemma hom_pairwise: "f \<in> hom G (DirProd H K) \<longleftrightarrow> (fst \<circ> f) \<in> hom G H \<and> (snd \<circ> f) \<in> hom G K"
+  apply (auto simp: hom_def mult_DirProd' dest: Pi_mem)
+   apply (metis Product_Type.mem_Times_iff comp_eq_dest_lhs funcset_mem)
+  by (metis mult_DirProd prod.collapse)
+
+lemma hom_paired:
+   "(\<lambda>x. (f x,g x)) \<in> hom G (DirProd H K) \<longleftrightarrow> f \<in> hom G H \<and> g \<in> hom G K"
+  by (simp add: hom_pairwise o_def)
+
+lemma hom_paired2:
+  assumes "group G" "group H"
+  shows "(\<lambda>(x,y). (f x,g y)) \<in> hom (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> hom G G' \<and> g \<in> hom H H'"
+  using assms
+  by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)
+
+lemma image_paired_Times:
+   "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+  by auto
+
+lemma iso_paired2:
+  assumes "group G" "group H"
+  shows "(\<lambda>(x,y). (f x,g y)) \<in> iso (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> iso G G' \<and> g \<in> iso H H'"
+  using assms
+  by (fastforce simp add: iso_def inj_on_def bij_betw_def hom_paired2 image_paired_Times
+      times_eq_iff group_def monoid.carrier_not_empty)
+
+lemma hom_of_fst:
+  assumes "group H"
+  shows "(f \<circ> fst) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom G K"
+proof -
+  interpret group H
+    by (rule assms)
+  show ?thesis
+    using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+lemma hom_of_snd:
+  assumes "group G"
+  shows "(f \<circ> snd) \<in> hom (DirProd G H) K \<longleftrightarrow> f \<in> hom H K"
+proof -
+  interpret group G
+    by (rule assms)
+  show ?thesis
+    using one_closed by (auto simp: hom_def Pi_def)
+qed
+
+
 subsection\<open>The locale for a homomorphism between two groups\<close>
 
 text\<open>Basis for homomorphism proofs: we assume two groups \<^term>\<open>G\<close> and
@@ -1172,7 +1313,8 @@
 proof -
   have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
     by (simp add: hom_mult [symmetric] del: hom_mult)
-  then show ?thesis by (simp del: r_one)
+  then show ?thesis
+    by (metis H.Units_eq H.Units_l_cancel H.one_closed local.one_closed)
 qed
 
 lemma hom_one:
@@ -1383,6 +1525,11 @@
   finally show "x \<otimes>\<^bsub>(?h_img)\<^esub> y = y \<otimes>\<^bsub>(?h_img)\<^esub> x" .
 qed
 
+lemma (in comm_group) hom_group_mult:
+  assumes "f \<in> hom H G" "g \<in> hom H G"
+ shows "(\<lambda>x. f x \<otimes>\<^bsub>G\<^esub> g x) \<in> hom H G"
+    using assms by (auto simp: hom_def Pi_def m_ac)
+
 lemma (in comm_group) hom_imp_img_comm_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "comm_group (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)"
@@ -1465,10 +1612,6 @@
   "subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
   by (erule subgroup.subgroup_is_group) (rule group_axioms)
 
-lemma (in group) is_monoid [intro, simp]:
-  "monoid G"
-  by (auto intro: monoid.intro m_assoc)
-
 lemma (in group) subgroup_mult_equality:
   "\<lbrakk> subgroup H G; h1 \<in> H; h2 \<in> H \<rbrakk> \<Longrightarrow>  h1 \<otimes>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h2 = h1 \<otimes> h2"
   unfolding subgroup_def by simp