src/HOL/Algebra/Group.thy
changeset 31727 2621a957d417
parent 30729 461ee3e49ad3
child 31754 b5260f5272a4
     1.1 --- a/src/HOL/Algebra/Group.thy	Fri Jun 19 20:22:46 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Fri Jun 19 22:49:12 2009 +0200
     1.3 @@ -544,7 +544,7 @@
     1.4  lemma (in group) hom_compose:
     1.5       "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
     1.6  apply (auto simp add: hom_def funcset_compose) 
     1.7 -apply (simp add: compose_def funcset_mem)
     1.8 +apply (simp add: compose_def Pi_def)
     1.9  done
    1.10  
    1.11  constdefs
    1.12 @@ -552,14 +552,14 @@
    1.13    "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    1.14  
    1.15  lemma iso_refl: "(%x. x) \<in> G \<cong> G"
    1.16 -by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    1.17 +by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
    1.18  
    1.19  lemma (in group) iso_sym:
    1.20       "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
    1.21  apply (simp add: iso_def bij_betw_Inv) 
    1.22  apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    1.23   prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    1.24 -apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f) 
    1.25 +apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
    1.26  done
    1.27  
    1.28  lemma (in group) iso_trans: 
    1.29 @@ -568,11 +568,11 @@
    1.30  
    1.31  lemma DirProd_commute_iso:
    1.32    shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
    1.33 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    1.34 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
    1.35  
    1.36  lemma DirProd_assoc_iso:
    1.37    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.38 -by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    1.39 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
    1.40  
    1.41  
    1.42  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
    1.43 @@ -592,7 +592,7 @@
    1.44    "x \<in> carrier G ==> h x \<in> carrier H"
    1.45  proof -
    1.46    assume "x \<in> carrier G"
    1.47 -  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
    1.48 +  with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
    1.49  qed
    1.50  
    1.51  lemma (in group_hom) one_closed [simp]: