src/HOL/Algebra/Group.thy
changeset 31754 b5260f5272a4
parent 31727 2621a957d417
child 32960 69916a850301
child 32988 d1d4d7a08a66
     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Jun 22 08:17:52 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Jun 22 20:59:12 2009 +0200
     1.3 @@ -542,10 +542,8 @@
     1.4        (\<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)}"
     1.5  
     1.6  lemma (in group) hom_compose:
     1.7 -     "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
     1.8 -apply (auto simp add: hom_def funcset_compose) 
     1.9 -apply (simp add: compose_def Pi_def)
    1.10 -done
    1.11 +  "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    1.12 +by (fastsimp simp add: hom_def compose_def)
    1.13  
    1.14  constdefs
    1.15    iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
    1.16 @@ -568,7 +566,7 @@
    1.17  
    1.18  lemma DirProd_commute_iso:
    1.19    shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
    1.20 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
    1.21 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
    1.22  
    1.23  lemma DirProd_assoc_iso:
    1.24    shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
    1.25 @@ -592,7 +590,7 @@
    1.26    "x \<in> carrier G ==> h x \<in> carrier H"
    1.27  proof -
    1.28    assume "x \<in> carrier G"
    1.29 -  with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
    1.30 +  with homh [unfolded hom_def] show ?thesis by auto
    1.31  qed
    1.32  
    1.33  lemma (in group_hom) one_closed [simp]: