diff -r 571909ef3103 -r 095dce9892e8 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -425,7 +425,20 @@
 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)
+  by(simp add: int_pow_def nat_pow_def)
+
+lemma pow_nat:
+  assumes "i\<ge>0"
+  shows "x [^]\<^bsub>G\<^esub> nat i = x [^]\<^bsub>G\<^esub> i"
+proof (cases i rule: int_cases)
+  case (nonneg n)
+  then show ?thesis
+    by (simp add: int_pow_int)
+next
+  case (neg n)
+  then show ?thesis
+    using assms by linarith
+qed
 
 lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
   by (simp add: int_pow_def)
@@ -450,6 +463,9 @@
   "x \<in> carrier G \<Longrightarrow> x [^] (-i::int) = inv (x [^] i)"
   by (simp add: int_pow_def2)
 
+lemma (in group) int_pow_neg_int: "x \<in> carrier G \<Longrightarrow> x [^] -(int n) = inv (x [^] n)"
+  by (simp add: int_pow_neg int_pow_int)
+
 lemma (in group) int_pow_mult:
   assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
 proof -
@@ -502,6 +518,38 @@
   by(simp add: inj_on_def)
 
 
+lemma (in monoid) group_commutes_pow:
+  fixes n::nat
+  shows "\<lbrakk>x \<otimes> y = y \<otimes> x; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x [^] n \<otimes> y = y \<otimes> x [^] n"
+  apply (induction n, auto)
+  by (metis m_assoc nat_pow_closed)
+
+lemma (in monoid) pow_mult_distrib:
+  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
+proof (induct n)
+  case (Suc n)
+  have "x \<otimes> (y [^] n \<otimes> y) = y [^] n \<otimes> x \<otimes> y"
+    by (simp add: eq group_commutes_pow m_assoc xy)
+  then show ?case
+    using assms Suc.hyps m_assoc by auto
+qed auto
+
+lemma (in group) int_pow_mult_distrib:
+  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+proof (cases i rule: int_cases)
+  case (nonneg n)
+  then show ?thesis
+    by (metis eq int_pow_int pow_mult_distrib xy)
+next
+  case (neg n)
+  then show ?thesis
+    unfolding neg
+    apply (simp add: xy int_pow_neg_int del: of_nat_Suc)
+    by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
+qed
+
 subsection \<open>Submonoids\<close>
 
 locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -852,7 +900,7 @@
 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"
+corollary iso_refl [simp]: "G \<cong> G"
   using iso_set_refl unfolding is_iso_def by auto
 
 lemma trivial_hom:
@@ -901,11 +949,11 @@
 corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
-lemma (in group) iso_set_trans:
-  "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
-  by (auto simp add: iso_def hom_compose bij_betw_compose)
+lemma iso_set_trans:
+  "\<lbrakk>h \<in> Group.iso G H; i \<in> Group.iso H I\<rbrakk> \<Longrightarrow> i \<circ> h \<in> Group.iso G I"
+  by (force simp: iso_def hom_compose intro: bij_betw_trans)
 
-corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
+corollary iso_trans [trans]: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   using iso_set_trans unfolding is_iso_def by blast
 
 lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
@@ -1081,6 +1129,8 @@
   fixes h
   assumes homh [simp]: "h \<in> hom G H"
 
+declare group_hom.homh [simp]
+
 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"
 proof -
@@ -1170,14 +1220,21 @@
   using subgroup.subgroup_is_group[OF assms is_group]
         is_group subgroup.subset[OF assms] by auto
 
-lemma (in group_hom) nat_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_nat_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
   by (induction n) auto
 
-lemma (in group_hom) int_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_int_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
-  using nat_pow_hom by (simp add: int_pow_def2)
+  using hom_nat_pow by (simp add: int_pow_def2)
 
+lemma hom_nat_pow:
+  "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
+  by (simp add: group_hom.hom_nat_pow group_hom_axioms_def group_hom_def)
+
+lemma hom_int_pow:
+  "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
+  by (simp add: group_hom.hom_int_pow group_hom_axioms.intro group_hom_def)
 
 subsection \<open>Commutative Structures\<close>
 
@@ -1225,11 +1282,6 @@
   shows "comm_monoid G"
   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
 
-lemma (in comm_monoid) nat_pow_distr:
-  "[| x \<in> carrier G; y \<in> carrier G |] ==>
-  (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
-  by (induct n) (simp, simp add: m_ac)
-
 lemma (in comm_monoid) submonoid_is_comm_monoid :
   assumes "submonoid H G"
   shows "comm_monoid (G\<lparr>carrier := H\<rparr>)"
@@ -1279,6 +1331,17 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   by (simp add: m_ac inv_mult_group)
 
+lemma (in comm_monoid) nat_pow_distrib:
+  fixes n::nat
+  assumes "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] n = x [^] n \<otimes> y [^] n"
+  by (simp add: assms pow_mult_distrib m_comm)
+
+lemma (in comm_group) int_pow_distrib:
+  assumes "x \<in> carrier G" "y \<in> carrier G"
+  shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+  by (simp add: assms int_pow_mult_distrib m_comm)
+
 lemma (in comm_monoid) hom_imp_img_comm_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "h \<in> hom G H"
   shows "comm_monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "comm_monoid ?h_img")