merged

--- a/src/HOL/Algebra/Coset.thy	Tue Jan 29 16:13:11 2019 +0100
+++ b/src/HOL/Algebra/Coset.thy	Tue Jan 29 17:33:40 2019 +0100
@@ -38,6 +38,9 @@
   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
   "H \<lhd> G \<equiv> normal H G"
 
+lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
+  by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+
 (*Next two lemmas contributed by Martin Baillon.*)
 
 lemma l_coset_eq_set_mult:
@@ -196,6 +199,17 @@
   ultimately show ?thesis by blast
 qed
 
+lemma (in group_hom) inj_on_one_iff:
+   "inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
+using G.solve_equation G.subgroup_self by (force simp: inj_on_def)
+
+lemma inj_on_one_iff':
+   "\<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 (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)
+
 lemma (in group) repr_independence:
   assumes "y \<in> H #> x" "x \<in> carrier G" "subgroup H G"
   shows "H #> x = H #> y" using assms

--- a/src/HOL/Algebra/Generated_Groups.thy	Tue Jan 29 16:13:11 2019 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy	Tue Jan 29 17:33:40 2019 +0100
@@ -137,17 +137,24 @@
   show "generate G { a } \<subseteq> { a [^] (k :: int) | k. k \<in> UNIV }"
   proof
     fix h assume "h \<in> generate G { a }" hence "\<exists>k :: int. h = a [^] k"
-    proof (induction, metis int_pow_0[of a], metis singletonD int_pow_1[OF assms])
+    proof (induction)
+      case one
+      then show ?case
+        using int_pow_0 [of G] by metis
+    next
+      case (incl h)
+      then show ?case
+        by (metis assms int_pow_1 singletonD)
+    next
       case (inv h)
-      hence "inv h = a [^] ((- 1) :: int)"
-        using assms unfolding int_pow_def2 by simp
-      thus ?case
-        by blast 
+      then show ?case
+        by (metis assms int_pow_1 int_pow_neg singletonD)
     next
-      case eng thus ?case
+      case (eng h1 h2)
+      then show ?case
         using assms by (metis int_pow_mult)
     qed
-    thus "h \<in> { a [^] (k :: int) | k. k \<in> UNIV }"
+    then show "h \<in> { a [^] (k :: int) | k. k \<in> UNIV }"
       by blast
   qed
 qed
@@ -436,4 +443,124 @@
   assumes "K \<subseteq> carrier G" shows "(derived H ^^ n) (h ` K) = h ` ((derived G ^^ n) K)"
   using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)
 
+
+subsection \<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>"
+
+lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)"
+  by (auto simp: subgroup_generated_def)
+
+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)
+
+lemma (in group) abelian_subgroup_generated:
+  assumes "comm_group G"
+  shows "comm_group (subgroup_generated G S)" (is "comm_group ?GS")
+proof (rule group.group_comm_groupI)
+  show "Group.group ?GS"
+    by simp
+next
+  fix x y
+  assume "x \<in> carrier ?GS" "y \<in> carrier ?GS"
+  with assms show "x \<otimes>\<^bsub>?GS\<^esub> y = y \<otimes>\<^bsub>?GS\<^esub> x"
+    apply (simp add: subgroup_generated_def)
+    by (meson Int_lower1 comm_groupE(4) generate_in_carrier)
+qed
+
+lemma (in group) subgroup_of_subgroup_generated:
+  assumes "H \<subseteq> B" "subgroup H G"
+    shows "subgroup H (subgroup_generated G B)"
+proof unfold_locales
+  fix x
+  assume "x \<in> H"
+  with assms show "inv\<^bsub>subgroup_generated G B\<^esub> x \<in> H"
+    unfolding subgroup_generated_def
+    by (metis IntI Int_commute Int_lower2 generate.incl generate_is_subgroup m_inv_consistent subgroup_def subsetCE)
+next
+  show "H \<subseteq> carrier (subgroup_generated G B)"
+    using assms apply (auto simp: carrier_subgroup_generated)
+    by (metis Int_iff generate.incl inf.orderE subgroup.mem_carrier)
+qed (use assms in \<open>auto simp: subgroup_generated_def subgroup_def\<close>)
+
+lemma carrier_subgroup_generated_alt:
+  assumes "Group.group G" "S \<subseteq> carrier G"
+  shows "carrier (subgroup_generated G S) = \<Inter>{H. subgroup H G \<and> carrier G \<inter> S \<subseteq> H}"
+  using assms by (auto simp: group.generate_minimal subgroup_generated_def)
+
+lemma one_subgroup_generated [simp]: "\<one>\<^bsub>subgroup_generated G S\<^esub> = \<one>\<^bsub>G\<^esub>"
+  by (auto simp: subgroup_generated_def)
+
+lemma mult_subgroup_generated [simp]: "mult (subgroup_generated G S) = mult G"
+  by (auto simp: subgroup_generated_def)
+
+lemma (in group) inv_subgroup_generated [simp]:
+  assumes "f \<in> carrier (subgroup_generated G S)"
+  shows "inv\<^bsub>subgroup_generated G S\<^esub> f = inv f"
+proof (rule group.inv_equality)
+  show "Group.group (subgroup_generated G S)"
+    by simp
+  have [simp]: "f \<in> carrier G"
+    by (metis Int_lower1 assms carrier_subgroup_generated generate_in_carrier)
+  show "inv f \<otimes>\<^bsub>subgroup_generated G S\<^esub> f = \<one>\<^bsub>subgroup_generated G S\<^esub>"
+    by (simp add: assms)
+  show "f \<in> carrier (subgroup_generated G S)"
+    using assms by (simp add: generate.incl subgroup_generated_def)
+  show "inv f \<in> carrier (subgroup_generated G S)"
+    using assms by (simp add: subgroup_generated_def generate_m_inv_closed)
+qed
+
+lemma subgroup_generated_restrict [simp]:
+   "subgroup_generated G (carrier G \<inter> S) = subgroup_generated G S"
+  by (simp add: subgroup_generated_def)
+
+lemma (in subgroup) carrier_subgroup_generated_subgroup [simp]:
+  "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")
+proof
+  assume L: ?lhs
+  then have Hsub: "H \<subseteq> generate G (carrier G \<inter> B)"
+    by (simp add: subgroup_def subgroup_generated_def)
+  then have H: "H \<subseteq> carrier G" "H \<subseteq> carrier(subgroup_generated G B)"
+    unfolding carrier_subgroup_generated
+    using generate_incl by blast+
+  with Hsub have "subgroup H G"
+    by (metis Int_commute Int_lower2 L carrier_subgroup_generated generate_consistent
+        generate_is_subgroup inf.orderE subgroup.carrier_subgroup_generated_subgroup subgroup_generated_def)
+  with H show ?rhs
+    by blast
+next
+  assume ?rhs
+  then show ?lhs
+    by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl)
+qed
+
+
+lemma pow_subgroup_generated:
+   "pow (subgroup_generated G S) = (pow G :: 'a \<Rightarrow> nat \<Rightarrow> 'a)"
+proof -
+  have "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n" for x and n::nat
+    by (induction n) auto
+  then show ?thesis
+    by force
+qed
+
+lemma (in group) int_pow_subgroup_generated:
+  fixes n::int
+  assumes "x \<in> carrier (subgroup_generated G S)"
+  shows "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n"
+proof -
+  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)
+qed
+
 end
\ No newline at end of file

--- a/src/HOL/Algebra/Group.thy	Tue Jan 29 16:13:11 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Tue Jan 29 17:33:40 2019 +0100
@@ -30,24 +30,6 @@
   \<comment> \<open>The set of invertible elements\<close>
   where "Units G = {y. y \<in> carrier G \<and> (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
 
-consts
-  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "[^]\<index>" 75)
-
-overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
-begin
-  definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
-end
-
-overloading int_pow == "pow :: [_, 'a, int] => 'a"
-begin
-  definition "int_pow G a z =
-   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
-    in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
-end
-
-lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
-by(simp add: int_pow_def nat_pow_def)
-
 locale monoid =
   fixes G (structure)
   assumes m_closed [intro, simp]:
@@ -191,46 +173,6 @@
 lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
 by auto
 
-text \<open>Power\<close>
-
-lemma (in monoid) nat_pow_closed [intro, simp]:
-  "x \<in> carrier G ==> x [^] (n::nat) \<in> carrier G"
-  by (induct n) (simp_all add: nat_pow_def)
-
-lemma (in monoid) nat_pow_0 [simp]:
-  "x [^] (0::nat) = \<one>"
-  by (simp add: nat_pow_def)
-
-lemma (in monoid) nat_pow_Suc [simp]:
-  "x [^] (Suc n) = x [^] n \<otimes> x"
-  by (simp add: nat_pow_def)
-
-lemma (in monoid) nat_pow_one [simp]:
-  "\<one> [^] (n::nat) = \<one>"
-  by (induct n) simp_all
-
-lemma (in monoid) nat_pow_mult:
-  "x \<in> carrier G ==> x [^] (n::nat) \<otimes> x [^] m = x [^] (n + m)"
-  by (induct m) (simp_all add: m_assoc [THEN sym])
-
-lemma (in monoid) nat_pow_comm:
-  "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
-  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
-
-lemma (in monoid) nat_pow_Suc2:
-  "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
-  using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
-  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
-
-lemma (in monoid) nat_pow_pow:
-  "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
-  by (induct m) (simp, simp add: nat_pow_mult add.commute)
-
-lemma (in monoid) nat_pow_consistent:
-  "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
-  unfolding nat_pow_def by simp
-
-
 (* Jacobson defines submonoid here. *)
 (* Jacobson defines the order of a monoid here. *)
 
@@ -340,6 +282,20 @@
 
 subsection \<open>Cancellation Laws and Basic Properties\<close>
 
+lemma (in group) inv_eq_1_iff [simp]:
+  assumes "x \<in> carrier G" shows "inv\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> \<longleftrightarrow> x = \<one>\<^bsub>G\<^esub>"
+proof -
+  have "x = \<one>" if "inv x = \<one>"
+  proof -
+    have "inv x \<otimes> x = \<one>"
+      using assms l_inv by blast
+    then show "x = \<one>"
+      using that assms by simp
+  qed
+  then show ?thesis
+    by auto
+qed
+
 lemma (in group) r_inv [simp]:
   "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
   by simp
@@ -374,30 +330,114 @@
      "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
   using inv_unique r_inv by blast
 
-(* Contributed by Joachim Breitner *)
 lemma (in group) inv_solve_left:
   "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = inv b \<otimes> c \<longleftrightarrow> c = b \<otimes> a"
   by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+
+lemma (in group) inv_solve_left':
+  "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> inv b \<otimes> c = a \<longleftrightarrow> c = b \<otimes> a"
+  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+
 lemma (in group) inv_solve_right:
   "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
   by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
 
-text \<open>Power\<close>
+lemma (in group) inv_solve_right':
+  "\<lbrakk>a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> b \<otimes> inv c = a \<longleftrightarrow> b = a \<otimes> c"
+  by (auto simp: m_assoc)
+  
+
+subsection \<open>Power\<close>
+
+consts
+  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "[^]\<index>" 75)
+
+overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
+begin
+  definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+end
+
+lemma (in monoid) nat_pow_closed [intro, simp]:
+  "x \<in> carrier G ==> x [^] (n::nat) \<in> carrier G"
+  by (induct n) (simp_all add: nat_pow_def)
+
+lemma (in monoid) nat_pow_0 [simp]:
+  "x [^] (0::nat) = \<one>"
+  by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_Suc [simp]:
+  "x [^] (Suc n) = x [^] n \<otimes> x"
+  by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_one [simp]:
+  "\<one> [^] (n::nat) = \<one>"
+  by (induct n) simp_all
+
+lemma (in monoid) nat_pow_mult:
+  "x \<in> carrier G ==> x [^] (n::nat) \<otimes> x [^] m = x [^] (n + m)"
+  by (induct m) (simp_all add: m_assoc [THEN sym])
+
+lemma (in monoid) nat_pow_comm:
+  "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
+  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
+
+lemma (in monoid) nat_pow_Suc2:
+  "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
+  using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
+  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
 
-lemma (in group) int_pow_def2:
-  "a [^] (z::int) = (if z < 0 then inv (a [^] (nat (-z))) else a [^] (nat z))"
-  by (simp add: int_pow_def nat_pow_def Let_def)
+lemma (in monoid) nat_pow_pow:
+  "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
+  by (induct m) (simp, simp add: nat_pow_mult add.commute)
+
+lemma (in monoid) nat_pow_consistent:
+  "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
+  unfolding nat_pow_def by simp
+
+lemma nat_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::nat) = \<one>\<^bsub>G\<^esub>"
+  by (simp add: nat_pow_def)
+
+lemma nat_pow_Suc [simp]: "x [^]\<^bsub>G\<^esub> (Suc n) = (x [^]\<^bsub>G\<^esub> n)\<otimes>\<^bsub>G\<^esub> x"
+  by (simp add: nat_pow_def)
 
-lemma (in group) int_pow_0 [simp]:
-  "x [^] (0::int) = \<one>"
-  by (simp add: int_pow_def2)
+lemma (in group) nat_pow_inv:
+  assumes "x \<in> carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
+proof (induction i)
+  case 0 thus ?case by simp
+next
+  case (Suc i)
+  have "(inv x) [^] Suc i = ((inv x) [^] i) \<otimes> inv x"
+    by simp
+  also have " ... = (inv (x [^] i)) \<otimes> inv x"
+    by (simp add: Suc.IH Suc.prems)
+  also have " ... = inv (x \<otimes> (x [^] i))"
+    by (simp add: assms inv_mult_group)
+  also have " ... = inv (x [^] (Suc i))"
+    using assms nat_pow_Suc2 by auto
+  finally show ?case .
+qed
+
+overloading int_pow == "pow :: [_, 'a, int] => 'a"
+begin
+  definition "int_pow G a z =
+   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+    in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+end
+
+lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
+by(simp add: int_pow_def nat_pow_def)
+
+lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
+  by (simp add: int_pow_def)
+
+lemma int_pow_def2: "a [^]\<^bsub>G\<^esub> z =
+   (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> (nat (-z))) else a [^]\<^bsub>G\<^esub> (nat z))"
+  by (simp add: int_pow_def nat_pow_def)
 
 lemma (in group) int_pow_one [simp]:
   "\<one> [^] (z::int) = \<one>"
   by (simp add: int_pow_def2)
 
-(* The following are contributed by Joachim Breitner *)
-
 lemma (in group) int_pow_closed [intro, simp]:
   "x \<in> carrier G ==> x [^] (i::int) \<in> carrier G"
   by (simp add: int_pow_def2)
@@ -418,23 +458,6 @@
     by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
 qed
 
-lemma (in group) nat_pow_inv:
-  assumes "x \<in> carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
-proof (induction i)
-  case 0 thus ?case by simp
-next
-  case (Suc i)
-  have "(inv x) [^] Suc i = ((inv x) [^] i) \<otimes> inv x"
-    by simp
-  also have " ... = (inv (x [^] i)) \<otimes> inv x"
-    by (simp add: Suc.IH Suc.prems)
-  also have " ... = inv (x \<otimes> (x [^] i))"
-    by (simp add: assms inv_mult_group)
-  also have " ... = inv (x [^] (Suc i))"
-    using assms nat_pow_Suc2 by auto
-  finally show ?case .
-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)
@@ -446,7 +469,7 @@
   assume n_ge: "n \<ge> 0" thus ?thesis
   proof (cases)
     assume m_ge: "m \<ge> 0" thus ?thesis
-      using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2
+      using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2 [where G=G]
       by (simp add: mult_less_0_iff nat_mult_distrib)
   next
     assume m_lt: "\<not> m \<ge> 0" 
@@ -592,7 +615,7 @@
   assumes "subgroup H G" shows "H \<subseteq> Units (G \<lparr> carrier := H \<rparr>)"
   using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp
 
-lemma (in group) m_inv_consistent:
+lemma (in group) m_inv_consistent [simp]:
   assumes "subgroup H G" "x \<in> H"
   shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
   using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
@@ -603,16 +626,16 @@
 proof (cases)
   assume ge: "n \<ge> 0"
   hence "x [^] n = x [^] (nat n)"
-    using int_pow_def2 by auto
+    using int_pow_def2 [of G] by auto
   also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat n)"
     using nat_pow_consistent by simp
   also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
-    using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] ge by auto
+    by (metis ge int_nat_eq int_pow_int)
   finally show ?thesis .
 next
   assume "\<not> n \<ge> 0" hence lt: "n < 0" by simp
   hence "x [^] n = inv (x [^] (nat (- n)))"
-    using int_pow_def2 by auto
+    using int_pow_def2 [of G] by auto
   also have " ... = (inv x) [^] (nat (- n))"
     by (metis assms nat_pow_inv subgroup.mem_carrier)
   also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
@@ -620,7 +643,7 @@
   also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
     using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
   also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
-    using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] lt by auto
+    by (simp add: int_pow_def2 lt)
   finally show ?thesis .
 qed
 
@@ -781,6 +804,17 @@
     {h. h \<in> carrier G \<rightarrow> carrier H \<and>
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
 
+lemma homI:
+  "\<lbrakk>\<And>x. x \<in> carrier G \<Longrightarrow> h x \<in> carrier H;
+    \<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y\<rbrakk> \<Longrightarrow> h \<in> hom G H"
+  by (auto simp: hom_def)
+
+lemma hom_carrier: "h \<in> hom G H \<Longrightarrow> h ` carrier G \<subseteq> carrier H"
+  by (auto simp: hom_def)
+
+lemma hom_in_carrier: "\<lbrakk>h \<in> hom G H; x \<in> carrier G\<rbrakk> \<Longrightarrow> h x \<in> carrier H"
+  by (auto simp: hom_def)
+
 lemma hom_compose:
   "\<lbrakk> f \<in> hom G H; g \<in> hom H I \<rbrakk> \<Longrightarrow> g \<circ> f \<in> hom G I"
   unfolding hom_def by (auto simp add: Pi_iff)
@@ -793,20 +827,50 @@
   "[|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)
 
-definition
-  iso :: "_ => _ => ('a => 'b) set"
+definition iso :: "_ => _ => ('a => 'b) set"
   where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
 
-definition
-  is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
+definition is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
   where "G \<cong> H = (iso G H  \<noteq> {})"
 
+definition mon where "mon G H = {f \<in> hom G H. inj_on f (carrier G)}"
+
+definition epi where "epi G H = {f \<in> hom G H. f ` (carrier G) = carrier H}"
+
+lemma isoI:
+  "\<lbrakk>h \<in> hom G H; bij_betw h (carrier G) (carrier H)\<rbrakk> \<Longrightarrow> h \<in> iso G H"
+  by (auto simp: iso_def)
+
+lemma epi_iff_subset:
+   "f \<in> epi G G' \<longleftrightarrow> f \<in> hom G G' \<and> carrier G' \<subseteq> f ` carrier G"
+  by (auto simp: epi_def hom_def)
+
+lemma iso_iff_mon_epi: "f \<in> iso G H \<longleftrightarrow> f \<in> mon G H \<and> f \<in> epi G H"
+  by (auto simp: iso_def mon_def epi_def bij_betw_def)
+
 lemma iso_set_refl: "(\<lambda>x. x) \<in> iso G G"
   by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
 
+lemma id_iso: "id \<in> iso G G"
+  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+
 corollary iso_refl : "G \<cong> G"
   using iso_set_refl unfolding is_iso_def by auto
 
+lemma trivial_hom:
+   "group H \<Longrightarrow> (\<lambda>x. one H) \<in> hom G H"
+  by (auto simp: hom_def Group.group_def)
+
+lemma (in group) hom_eq:
+  assumes "f \<in> hom G H" "\<And>x. x \<in> carrier G \<Longrightarrow> f' x = f x"
+  shows "f' \<in> hom G H"
+  using assms by (auto simp: hom_def)
+
+lemma (in group) iso_eq:
+  assumes "f \<in> iso G H" "\<And>x. x \<in> carrier G \<Longrightarrow> f' x = f x"
+  shows "f' \<in> iso G H"
+  using assms  by (fastforce simp: iso_def inj_on_def bij_betw_def hom_eq image_iff)
+
 lemma (in group) iso_set_sym:
   assumes "h \<in> iso G H"
   shows "inv_into (carrier G) h \<in> iso H G"
@@ -846,10 +910,8 @@
 corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   using iso_set_trans unfolding is_iso_def by blast
 
-(* NEW ====================================================================== *)
 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
-(* ========================================================================== *)
 
 
 (* Next four lemmas contributed by Paulo. *)
@@ -1015,12 +1077,13 @@
   shows "G \<times>\<times> H \<cong> G2 \<times>\<times> I"
   using DirProd_iso_set_trans assms unfolding is_iso_def by blast
 
+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
   \<^term>\<open>H\<close>, with a homomorphism \<^term>\<open>h\<close> between them\<close>
 locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +
   fixes h
-  assumes homh: "h \<in> hom G H"
+  assumes homh [simp]: "h \<in> hom G H"
 
 lemma (in group_hom) hom_mult [simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
@@ -1036,7 +1099,7 @@
   with homh [unfolded hom_def] show ?thesis by auto
 qed
 
-lemma (in group_hom) one_closed [simp]: "h \<one> \<in> carrier H"
+lemma (in group_hom) one_closed: "h \<one> \<in> carrier H"
   by simp
 
 lemma (in group_hom) hom_one [simp]: "h \<one> = \<one>\<^bsub>H\<^esub>"
@@ -1046,6 +1109,16 @@
   then show ?thesis by (simp del: r_one)
 qed
 
+lemma hom_one:
+  assumes "h \<in> hom G H" "group G" "group H"
+  shows "h (one G) = one H"
+  apply (rule group_hom.hom_one)
+  by (simp add: assms group_hom_axioms_def group_hom_def)
+
+lemma hom_mult:
+  "\<lbrakk>h \<in> hom G H; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+  by (auto simp: hom_def)
+
 lemma (in group_hom) inv_closed [simp]:
   "x \<in> carrier G ==> h (inv x) \<in> carrier H"
   by simp
@@ -1110,7 +1183,7 @@
 
 lemma (in group_hom) int_pow_hom:
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
-  using int_pow_def2 nat_pow_hom by (simp add: G.int_pow_def2)
+  using nat_pow_hom by (simp add: int_pow_def2)
 
 
 subsection \<open>Commutative Structures\<close>

--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jan 29 16:13:11 2019 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jan 29 17:33:40 2019 +0100
@@ -433,7 +433,7 @@
     fix b assume "b \<in> { a [^] k | k. k \<in> (UNIV :: nat set) }"
     then obtain k :: nat where "b = a [^] k" by blast
     hence "b = a [^] (int k)"
-      using int_pow_def2 by auto
+      by (simp add: int_pow_int)
     thus "b \<in> generate G { a }"
       unfolding generate_pow[OF assms(2)] by blast
   qed
@@ -447,12 +447,12 @@
     proof (cases "k < 0")
       assume "\<not> k < 0"
       hence "b = a [^] (nat k)"
-        using k int_pow_def2 by auto
+        by (simp add: int_pow_def2 k)
       thus ?thesis by blast
     next
       assume "k < 0"
       hence b: "b = inv (a [^] (nat (- k)))"
-        using k int_pow_def2 by auto
+        using k int_pow_def2[of G] by auto
 
       obtain m where m: "ord a * m \<ge> nat (- k)"
         by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)