diff -r 12dce58bcd3f -r 1b5178abaf97 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Oct 04 11:18:39 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Oct 04 15:25:47 2018 +0100
@@ -781,6 +781,19 @@
     {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)}"
 
+
+(* NEW ========================================================================== *)
+lemma hom_trans:
+  "\<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)
+(* ============================================================================== *)
+
+(* NEW ============================================================================ *)
+lemma (in group) hom_restrict:
+  assumes "h \<in> hom G H" and "\<And>g. g \<in> carrier G \<Longrightarrow> h g = t g" shows "t \<in> hom G H"
+  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)
@@ -838,6 +851,12 @@
 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. *)
 
 lemma (in monoid) hom_imp_img_monoid: