# HG changeset patch
# User paulson
# Date 1554210112 -3600
# Node ID b5574e88092be5c213cf6154663f69fb61fa8e72
# Parent  6ae9505d693a459e35be86141ffa0b69b0d0ef06# Parent  e8da1fe4d61c45b5a73748e6f9de5ba666a8bd49
merged

diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Algebra.thy
--- a/src/HOL/Algebra/Algebra.thy	Tue Apr 02 13:22:16 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Algebra/Algebra.thy *)
 
 theory Algebra
-  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
+  imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
 begin
 end
diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Apr 02 13:22:16 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -203,6 +203,10 @@
    "\<lbrakk>h \<in> hom G H; group G; group H\<rbrakk> \<Longrightarrow> inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
   using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast
 
+lemma mon_iff_hom_one:
+   "\<lbrakk>group G; group H\<rbrakk> \<Longrightarrow> f \<in> mon G H \<longleftrightarrow> f \<in> hom G H \<and> (\<forall>x. x \<in> carrier G \<and> f x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>\<^bsub>G\<^esub>)"
+  by (auto simp: mon_def inj_on_one_iff')
+
 lemma (in group_hom) iso_iff: "h \<in> iso G H \<longleftrightarrow> carrier H \<subseteq> h ` carrier G \<and> (\<forall>x\<in>carrier G. h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)"
   by (auto simp: iso_def bij_betw_def inj_on_one_iff)
 
@@ -374,7 +378,7 @@
 subsection \<open>Normal subgroups\<close>
 
 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
-  by (simp add: normal_def subgroup_def)
+  by (rule normal.axioms(1))
 
 lemma (in group) normalI:
   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
@@ -396,6 +400,14 @@
   shows "x \<otimes> h \<otimes> (inv x) \<in> H"
   using assms inv_op_closed1 by (metis inv_closed inv_inv)
 
+lemma (in comm_group) normal_iff_subgroup:
+  "N \<lhd> G \<longleftrightarrow> subgroup N G"
+proof
+  assume "subgroup N G"
+  then show "N \<lhd> G"
+    by unfold_locales (auto simp: subgroupE subgroup.one_closed l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+qed (simp add: normal_imp_subgroup)
+
 
 text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in group) normal_inv_iff:
@@ -925,8 +937,14 @@
 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
 done
 
-lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
-  by (simp add: FactGroup_def)
+lemma carrier_FactGroup: "carrier(G Mod N) = (\<lambda>x. r_coset G N x) ` carrier G"
+  by (auto simp: FactGroup_def RCOSETS_def)
+
+lemma one_FactGroup [simp]: "one(G Mod N) = N"
+  by (auto simp: FactGroup_def)
+
+lemma mult_FactGroup [simp]: "monoid.mult (G Mod N) = set_mult G"
+  by (auto simp: FactGroup_def)
 
 lemma (in normal) inv_FactGroup:
   assumes "X \<in> carrier (G Mod H)"
@@ -951,6 +969,79 @@
   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
 
 
+lemma (in comm_group) set_mult_commute:
+  assumes "N \<subseteq> carrier G" "x \<in> rcosets N" "y \<in> rcosets N"
+  shows "x <#> y = y <#> x"
+  using assms unfolding set_mult_def RCOSETS_def
+  by auto (metis m_comm r_coset_subset_G subsetCE)+
+
+lemma (in comm_group) abelian_FactGroup:
+  assumes "subgroup N G" shows "comm_group(G Mod N)"
+proof (rule group.group_comm_groupI)
+  have "N \<lhd> G"
+    by (simp add: assms normal_iff_subgroup)
+  then show "Group.group (G Mod N)"
+    by (simp add: normal.factorgroup_is_group)
+  fix x :: "'a set" and y :: "'a set"
+  assume "x \<in> carrier (G Mod N)" "y \<in> carrier (G Mod N)"
+  then show "x \<otimes>\<^bsub>G Mod N\<^esub> y = y \<otimes>\<^bsub>G Mod N\<^esub> x"
+    apply (simp add: FactGroup_def subgroup_def)
+    apply (rule set_mult_commute)
+    using assms apply (auto simp: subgroup_def)
+    done
+qed
+
+
+lemma FactGroup_universal:
+  assumes "h \<in> hom G H" "N \<lhd> G"
+    and h: "\<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G; r_coset G N x = r_coset G N y\<rbrakk> \<Longrightarrow> h x = h y"
+  obtains g
+  where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+  obtain g where g: "\<And>x. x \<in> carrier G \<Longrightarrow> h x = g(r_coset G N x)"
+    using h function_factors_left_gen [of "\<lambda>x. x \<in> carrier G" "r_coset G N" h] by blast
+  show thesis
+  proof
+    show "g \<in> hom (G Mod N) H"
+    proof (rule homI)
+      show "g (u \<otimes>\<^bsub>G Mod N\<^esub> v) = g u \<otimes>\<^bsub>H\<^esub> g v"
+        if "u \<in> carrier (G Mod N)" "v \<in> carrier (G Mod N)" for u v
+      proof -
+        from that
+        obtain x y where xy: "x \<in> carrier G" "u = r_coset G N x" "y \<in> carrier G"  "v = r_coset G N y"
+          by (auto simp: carrier_FactGroup)
+        then have "h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+           by (metis hom_mult [OF \<open>h \<in> hom G H\<close>])
+        then show ?thesis
+          by (metis Coset.mult_FactGroup xy \<open>N \<lhd> G\<close> g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
+      qed
+    qed (use \<open>h \<in> hom G H\<close> in \<open>auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g\<close>)
+  qed (auto simp flip: g)
+qed
+
+
+lemma (in normal) FactGroup_pow:
+  fixes k::nat
+  assumes "a \<in> carrier G"
+  shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+proof (induction k)
+  case 0
+  then show ?case
+    by (simp add: r_coset_def)
+next
+  case (Suc k)
+  then show ?case
+    by (simp add: assms rcos_sum)
+qed
+
+lemma (in normal) FactGroup_int_pow:
+  fixes k::int
+  assumes "a \<in> carrier G"
+  shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+  by (metis Group.group.axioms(1) image_eqI is_group monoid.nat_pow_closed int_pow_def2 assms
+         FactGroup_pow carrier_FactGroup inv_FactGroup rcos_inv)
+
+
 subsection\<open>The First Isomorphism Theorem\<close>
 
 text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
@@ -983,6 +1074,30 @@
 qed
 
 
+lemma (in group_hom) FactGroup_universal_kernel:
+  assumes "N \<lhd> G" and h: "N \<subseteq> kernel G H h"
+  obtains g where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+  have "h x = h y"
+    if "x \<in> carrier G" "y \<in> carrier G" "r_coset G N x = r_coset G N y" for x y
+  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
+    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)"
+      by (simp add: that)
+    also have "\<dots> = \<one>\<^bsub>H\<^esub>"
+      using xy by (simp add: kernel_def)
+    finally have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = \<one>\<^bsub>H\<^esub>" .
+    then show ?thesis
+      using H.inv_equality that by fastforce
+  qed
+  with FactGroup_universal [OF homh \<open>N \<lhd> G\<close>] that show thesis
+    by metis
+qed
+
 lemma (in group_hom) FactGroup_the_elem_mem:
   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
   shows "the_elem (h`X) \<in> carrier H"
diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Elementary_Groups.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Elementary_Groups.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -0,0 +1,382 @@
+section \<open>Elementary Group Constructions\<close>
+
+(*  Title:      HOL/Algebra/Elementary_Groups.thy
+    Author:     LC Paulson, ported from HOL Light
+*)
+
+theory Elementary_Groups
+imports Generated_Groups
+begin
+
+subsection\<open>Direct sum/product lemmas\<close>
+
+locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B
+begin
+
+lemma subset_one: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> A \<inter> B = {\<one>}"
+  by  auto
+
+lemma sub_id_iff: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>)"
+        (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>)"
+  proof (intro ballI iffI impI)
+    fix x y
+    assume "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B" "x \<otimes> inv y = \<one>"
+    then have "y = x"
+      using group.inv_equality group_l_invI by fastforce
+    then show "x = \<one> \<and> inv y = \<one>"
+      using \<open>A \<inter> B \<subseteq> {\<one>}\<close> \<open>x \<in> A\<close> \<open>y \<in> B\<close> by fastforce
+  next
+    assume "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>"
+    then show "A \<inter> B \<subseteq> {\<one>}"
+      by auto
+  qed
+  also have "\<dots> = ?rhs"
+    by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def)
+  finally show ?thesis .
+qed
+
+lemma cancel: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+        (is "?lhs = ?rhs")
+proof -
+  have "(\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>) = ?rhs"
+    (is "?med = _")
+  proof (intro ballI iffI impI)
+    fix x y x' y'
+    assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>"
+      and AB: "x \<in> A" "y \<in> B" "x' \<in> A" "y' \<in> B" and eq: "x \<otimes> y = x' \<otimes> y'"
+    then have carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
+      using AG.subset BG.subset by auto
+    then have "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = inv x' \<otimes> (x \<otimes> y) \<otimes> inv y'"
+      by (simp add: m_assoc)
+    also have "\<dots> = \<one>"
+      using carr  by (simp add: eq) (simp add: m_assoc)
+    finally have 1: "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = \<one>" .
+    show "x = x' \<and> y = y'"
+      using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality)
+  next
+    fix x y
+    assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y'"
+      and xy: "x \<in> A" "y \<in> B" "x \<otimes> y = \<one>"
+    show "x = \<one> \<and> y = \<one>"
+      by (rule *) (use xy in auto)
+  qed
+  then show ?thesis
+    by (simp add: sub_id_iff)
+qed
+
+lemma commuting_imp_normal1:
+  assumes sub: "carrier G \<subseteq> A <#> B"
+     and mult: "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+   shows "A \<lhd> G"
+proof -
+  have AB: "A \<subseteq> carrier G \<and> B \<subseteq> carrier G"
+    by (simp add: AG.subset BG.subset)
+  have "A #> x = x <# A"
+    if x: "x \<in> carrier G" for x
+  proof -
+    obtain a b where xeq: "x = a \<otimes> b" and "a \<in> A" "b \<in> B" and carr: "a \<in> carrier G" "b \<in> carrier G"
+      using x sub AB by (force simp: set_mult_def)
+    have Ab: "A <#> {b} = {b} <#> A"
+      using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close> mult
+      by (force simp: set_mult_def m_assoc subset_iff)
+    have "A #> x = A <#> {a \<otimes> b}"
+      by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq)
+    also have "\<dots> = A <#> {a} <#> {b}"
+      using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close>
+      by (auto simp: set_mult_def m_assoc subset_iff)
+    also have "\<dots> = {a} <#> A <#> {b}"
+      by (metis AG.rcos_const AG.subgroup_axioms \<open>a \<in> A\<close> coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier)
+    also have "\<dots> = {a} <#> {b} <#> A"
+      by (simp add: is_group carr group.set_mult_assoc AB Ab)
+    also have "\<dots> = {x} <#> A"
+      by (auto simp: set_mult_def xeq)
+    finally show "A #> x = x <# A"
+      by (simp add: l_coset_eq_set_mult)
+  qed
+  then show ?thesis
+    by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group)
+qed
+
+lemma commuting_imp_normal2:
+  assumes"carrier G \<subseteq> A <#> B"  "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+  shows "B \<lhd> G"
+proof (rule group_disjoint_sum.commuting_imp_normal1)
+  show "group_disjoint_sum G B A"
+  proof qed
+next
+  show "carrier G \<subseteq> B <#> A"
+    using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast
+qed (use assms in auto)
+
+
+lemma (in group) normal_imp_commuting:
+  assumes "A \<lhd> G" "B \<lhd> G" "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B"
+  shows "x \<otimes> y = y \<otimes> x"
+proof -
+  interpret AG: normal A G
+    using assms by auto
+  interpret BG: normal B G
+    using assms by auto
+  interpret group_disjoint_sum G A B
+  proof qed
+  have * [rule_format]: "(\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+    using cancel assms by (auto simp: normal_def)
+  have carr: "x \<in> carrier G" "y \<in> carrier G"
+    using assms AG.subset BG.subset by auto
+  then show ?thesis
+    using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x]
+    by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis \<open>x \<in> A\<close> \<open>y \<in> B\<close>)
+qed
+
+lemma normal_eq_commuting:
+  assumes "carrier G \<subseteq> A <#> B" "A \<inter> B \<subseteq> {\<one>}"
+  shows "A \<lhd> G \<and> B \<lhd> G \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+  by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting)
+
+lemma (in group) hom_group_mul_rev:
+  assumes "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G"
+          (is "?h \<in> hom ?P G")
+   and "x \<in> carrier G" "y \<in> carrier G" "x \<in> A" "y \<in> B"
+ shows "x \<otimes> y = y \<otimes> x"
+proof -
+  interpret P: group_hom ?P G ?h
+    by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group)
+  have xy: "(x,y) \<in> carrier ?P"
+    by (auto simp: assms carrier_subgroup_generated generate.incl)
+  have "x \<otimes> (x \<otimes> (y \<otimes> y)) = x \<otimes> (y \<otimes> (x \<otimes> y))"
+    using P.hom_mult [OF xy xy] by (simp add: m_assoc assms)
+  then have "x \<otimes> (y \<otimes> y) = y \<otimes> (x \<otimes> y)"
+    using assms by simp
+  then show ?thesis
+    by (simp add: assms flip: m_assoc)
+qed
+
+lemma hom_group_mul_eq:
+   "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using hom_group_mul_rev AG.subset BG.subset by blast
+next
+  assume R: ?rhs
+  have subG: "generate G (carrier G \<inter> A) \<subseteq> carrier G" for A
+    by (simp add: generate_incl)
+  have *: "x \<otimes> u \<otimes> (y \<otimes> v) = x \<otimes> y \<otimes> (u \<otimes> v)"
+    if eq [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x"
+      and gen: "x \<in> generate G (carrier G \<inter> A)" "y \<in> generate G (carrier G \<inter> B)"
+      "u \<in> generate G (carrier G \<inter> A)" "v \<in> generate G (carrier G \<inter> B)"
+    for x y u v
+  proof -
+    have "u \<otimes> y = y \<otimes> u"
+      by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4))
+    then have "x \<otimes> u \<otimes> y = x \<otimes> y \<otimes> u"
+      using gen by (simp add: m_assoc subsetD [OF subG])
+    then show ?thesis
+      using gen by (simp add: subsetD [OF subG] flip: m_assoc)
+  qed
+  show ?lhs
+    using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *)
+qed
+
+
+lemma epi_group_mul_eq:
+   "(\<lambda>(x,y). x \<otimes> y) \<in> epi (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+  have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+    by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+  have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+    by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+  have "(((\<lambda>(x, y). x \<otimes> y) ` (generate G (carrier G \<inter> A) \<times> generate G (carrier G \<inter> B)))) = ((A <#> B))"
+    by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB])
+  then show ?thesis
+    by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated)
+qed
+
+lemma mon_group_mul_eq:
+    "(\<lambda>(x,y). x \<otimes> y) \<in> mon (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> A \<inter> B = {\<one>} \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+  have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+    by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+  have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+    by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+  show ?thesis
+    apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one)
+     apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup)
+    using cancel apply blast+
+    done
+qed
+
+lemma iso_group_mul_alt:
+    "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+  by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq)
+
+lemma iso_group_mul_eq:
+    "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> A \<lhd> G \<and> B \<lhd> G"
+  by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong)
+
+
+lemma (in group) iso_group_mul_gen:
+  assumes "A \<lhd> G" "B \<lhd> G"
+  shows "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+     \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G"
+proof -
+  interpret group_disjoint_sum G A B
+    using assms by (auto simp: group_disjoint_sum_def normal_def)
+  show ?thesis
+    by (simp add: subset_one iso_group_mul_eq assms)
+qed
+
+
+lemma iso_group_mul:
+  assumes "comm_group G"
+  shows "((\<lambda>(x,y). x \<otimes> y) \<in> iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G
+     \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G)"
+proof (rule iso_group_mul_gen)
+  interpret comm_group
+    by (rule assms)
+  show "A \<lhd> G"
+    by (simp add: AG.subgroup_axioms subgroup_imp_normal)
+  show "B \<lhd> G"
+    by (simp add: BG.subgroup_axioms subgroup_imp_normal)
+qed
+
+end
+
+
+subsection\<open>The one-element group on a given object\<close>
+
+definition singleton_group :: "'a \<Rightarrow> 'a monoid"
+  where "singleton_group a = \<lparr>carrier = {a}, monoid.mult = (\<lambda>x y. a), one = a\<rparr>"
+
+lemma singleton_group [simp]: "group (singleton_group a)"
+  unfolding singleton_group_def by (auto intro: groupI)
+
+lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)"
+  by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def)
+
+lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}"
+  by (auto simp: singleton_group_def)
+
+lemma (in group) hom_into_singleton_iff [simp]:
+  "h \<in> hom G (singleton_group a) \<longleftrightarrow> h \<in> carrier G \<rightarrow> {a}"
+  by (auto simp: hom_def singleton_group_def)
+
+declare group.hom_into_singleton_iff [simp]
+
+lemma (in group) id_hom_singleton: "id \<in> hom (singleton_group \<one>) G"
+  by (simp add: hom_def singleton_group_def)
+
+subsection\<open>Similarly, trivial groups\<close>
+
+definition trivial_group :: "('a, 'b) monoid_scheme \<Rightarrow> bool"
+  where "trivial_group G \<equiv> group G \<and> carrier G = {one G}"
+
+lemma trivial_imp_finite_group:
+   "trivial_group G \<Longrightarrow> finite(carrier G)"
+  by (simp add: trivial_group_def)
+
+lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)"
+  by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def)
+
+lemma (in group) trivial_group_subset:
+   "trivial_group G \<longleftrightarrow> carrier G \<subseteq> {one G}"
+  using is_group trivial_group_def by fastforce
+
+lemma (in group) trivial_group: "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G = {a})"
+  unfolding trivial_group_def using one_closed is_group by fastforce
+
+lemma (in group) trivial_group_alt:
+   "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G \<subseteq> {a})"
+  by (auto simp: trivial_group)
+
+lemma (in group) trivial_group_subgroup_generated:
+  assumes "S \<subseteq> {one G}"
+  shows "trivial_group(subgroup_generated G S)"
+proof -
+  have "carrier (subgroup_generated G S) \<subseteq> {\<one>}"
+    using generate_empty generate_one subset_singletonD assms
+    by (fastforce simp add: carrier_subgroup_generated)
+  then show ?thesis
+    by (simp add: group.trivial_group_subset)
+qed
+
+lemma (in group) trivial_group_subgroup_generated_eq:
+  "trivial_group(subgroup_generated G s) \<longleftrightarrow> carrier G \<inter> s \<subseteq> {one G}"
+  apply (rule iffI)
+   apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl)
+  by (metis subgroup_generated_restrict trivial_group_subgroup_generated)
+
+lemma isomorphic_group_triviality1:
+  assumes "G \<cong> H" "group H" "trivial_group G"
+  shows "trivial_group H"
+  using assms
+  by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one)
+
+lemma isomorphic_group_triviality:
+  assumes "G \<cong> H" "group G" "group H"
+  shows "trivial_group G \<longleftrightarrow> trivial_group H"
+  by (meson assms group.iso_sym isomorphic_group_triviality1)
+
+lemma (in group_hom) kernel_from_trivial_group:
+   "trivial_group G \<Longrightarrow> kernel G H h = carrier G"
+  by (auto simp: trivial_group_def kernel_def)
+
+lemma (in group_hom) image_from_trivial_group:
+   "trivial_group G \<Longrightarrow> h ` carrier G = {one H}"
+  by (auto simp: trivial_group_def)
+
+lemma (in group_hom) kernel_to_trivial_group:
+   "trivial_group H \<Longrightarrow> kernel G H h = carrier G"
+  unfolding kernel_def trivial_group_def
+  using hom_closed by blast
+
+
+subsection\<open>The additive group of integers\<close>
+
+definition integer_group
+  where "integer_group = \<lparr>carrier = UNIV, monoid.mult = (+), one = (0::int)\<rparr>"
+
+lemma group_integer_group [simp]: "group integer_group"
+  unfolding integer_group_def
+proof (rule groupI; simp)
+  show "\<And>x::int. \<exists>y. y + x = 0"
+  by presburger
+qed
+
+lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
+  by (auto simp: integer_group_def)
+
+lemma one_integer_group [simp]: "\<one>\<^bsub>integer_group\<^esub> = 0"
+  by (auto simp: integer_group_def)
+
+lemma mult_integer_group [simp]: "x \<otimes>\<^bsub>integer_group\<^esub> y = x + y"
+  by (auto simp: integer_group_def)
+
+lemma inv_integer_group [simp]: "inv\<^bsub>integer_group\<^esub> x = -x"
+  by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma abelian_integer_group: "comm_group integer_group"
+  by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma group_nat_pow_integer_group [simp]:
+  fixes n::nat and x::int
+  shows "pow integer_group x n = int n * x"
+  by (induction n) (auto simp: integer_group_def algebra_simps)
+
+lemma group_int_pow_integer_group [simp]:
+  fixes n::int and x::int
+  shows "pow integer_group x n = n * x"
+  by (simp add: int_pow_def2)
+
+lemma (in group) hom_integer_group_pow:
+   "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
+  by (rule homI) (auto simp: int_pow_mult)
+
+end
diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Tue Apr 02 13:22:16 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -452,6 +452,19 @@
 lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)"
   by (auto simp: subgroup_generated_def)
 
+lemma (in group) subgroup_generated_subset_carrier_subset:
+   "S \<subseteq> carrier G \<Longrightarrow> S \<subseteq> carrier(subgroup_generated G S)"
+  by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI)
+
+lemma (in group) subgroup_generated_minimal:
+   "\<lbrakk>subgroup H G; S \<subseteq> H\<rbrakk> \<Longrightarrow> carrier(subgroup_generated G S) \<subseteq> H"
+  by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2)
+
+lemma (in group) carrier_subgroup_generated_subset:
+   "carrier (subgroup_generated G A) \<subseteq> carrier G"
+  apply (clarsimp simp: carrier_subgroup_generated)
+  by (meson Int_lower1 generate_in_carrier)
+
 lemma (in group) group_subgroup_generated [simp]: "group (subgroup_generated G S)"
     unfolding subgroup_generated_def
     by (simp add: generate_is_subgroup subgroup_imp_group)
@@ -520,7 +533,6 @@
   "carrier (subgroup_generated G H) = H"
   by (auto simp: generate.incl carrier_subgroup_generated elim: generate.induct)
 
-
 lemma (in group) subgroup_subgroup_generated_iff:
    "subgroup H (subgroup_generated G B) \<longleftrightarrow> subgroup H G \<and> H \<subseteq> carrier(subgroup_generated G B)"
  (is "?lhs = ?rhs")
@@ -542,6 +554,9 @@
     by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl)
 qed
 
+lemma (in group) subgroup_subgroup_generated:
+   "subgroup (carrier(subgroup_generated G S)) G"
+  using group.subgroup_self group_subgroup_generated subgroup_subgroup_generated_iff by blast
 
 lemma pow_subgroup_generated:
    "pow (subgroup_generated G S) = (pow G :: 'a \<Rightarrow> nat \<Rightarrow> 'a)"
@@ -552,6 +567,19 @@
     by force
 qed
 
+lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S"
+proof -
+  have *: "\<And>A. carrier G \<inter> A \<subseteq> carrier (subgroup_generated (subgroup_generated G A) A)"
+    by (metis (no_types, hide_lams) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff)
+  show ?thesis
+  apply (auto intro!: monoid.equality)
+    using group.carrier_subgroup_generated_subset group_subgroup_generated apply blast
+     apply (metis (no_types, hide_lams) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal
+        subgroup_generated_restrict subgroup_subgroup_generated_iff subset_eq)
+    apply (simp add: subgroup_generated_def)
+    done
+qed
+
 lemma (in group) int_pow_subgroup_generated:
   fixes n::int
   assumes "x \<in> carrier (subgroup_generated G S)"
@@ -560,7 +588,7 @@
   have "x [^] nat (- n) \<in> carrier (subgroup_generated G S)"
     by (metis assms group.is_monoid group_subgroup_generated monoid.nat_pow_closed pow_subgroup_generated)
   then show ?thesis
-    by (simp add: int_pow_def2 pow_subgroup_generated)
+    by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated)
 qed
 
 lemma kernel_from_subgroup_generated [simp]:
diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Apr 02 13:22:16 2019 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -471,12 +471,12 @@
 proof -
   have [simp]: "-i - j = -j - i" by simp
   show ?thesis
-    by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
+    by (auto simp: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult)
 qed
 
 lemma (in group) int_pow_inv:
   "x \<in> carrier G \<Longrightarrow> (inv x) [^] (i :: int) = inv (x [^] i)"
-  by (simp add: nat_pow_inv int_pow_def2)
+  by (metis int_pow_def2 nat_pow_inv)
 
 lemma (in group) int_pow_pow:
   assumes "x \<in> carrier G"
@@ -873,6 +873,10 @@
   "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 by (fastforce simp add: hom_def compose_def)
 
+lemma (in group) restrict_hom_iff [simp]:
+  "(\<lambda>x. if x \<in> carrier G then f x else g x) \<in> hom G H \<longleftrightarrow> f \<in> hom G H"
+  by (simp add: hom_def Pi_iff)
+
 definition iso :: "_ => _ => ('a => 'b) set"
   where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
 
@@ -1582,4 +1586,6 @@
 lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
   using r_cancel_one by fastforce
 
+declare pow_nat [simp] (*causes looping if added above, especially with int_pow_def2*)
+
 end
diff -r 6ae9505d693a -r b5574e88092b src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Apr 02 13:22:16 2019 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Apr 02 14:01:52 2019 +0100
@@ -448,13 +448,12 @@
     proof (cases "k < 0")
       assume "\<not> k < 0"
       hence "b = a [^] (nat k)"
-        by (simp add: int_pow_def2 k)
+        by (simp add: k)
       thus ?thesis by blast
     next
       assume "k < 0"
       hence b: "b = inv (a [^] (nat (- k)))"
-        using k int_pow_def2[of G] by auto
-
+        using k \<open>a \<in> carrier G\<close> by (auto simp: int_pow_neg)
       obtain m where m: "ord a * m \<ge> nat (- k)"
         by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
       hence "a [^] (ord a * m) = \<one>"