src/HOL/Algebra/Group.thy

 lemma (in group) int_pow_mult:
   assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
 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"
   shows "(x [^] (n :: int)) [^] (m :: int) = x [^] (n * m :: int)"
 proof (cases)

   using assms unfolding hom_def by (auto simp add: Pi_iff)
 
 lemma (in group) hom_compose:
   "[|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)}"
 
 definition is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)

   using l_cancel_one by fastforce
 
 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