src/HOL/Algebra/Group.thy
changeset 14803 f7557773cc87
parent 14761 28b5eb4a867f
child 14852 fffab59e0050
     1.1 --- a/src/HOL/Algebra/Group.thy	Mon May 24 18:35:34 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 26 11:43:50 2004 +0200
     1.3 @@ -593,15 +593,15 @@
     1.4  
     1.5  subsection {* Isomorphisms *}
     1.6  
     1.7 -constdefs (structure G and H)
     1.8 -  iso :: "_ => _ => ('a => 'b) set"
     1.9 -  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    1.10 +constdefs
    1.11 +  iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
    1.12 +  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    1.13  
    1.14 -lemma iso_refl: "(%x. x) \<in> iso G G"
    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  
    1.18  lemma (in group) iso_sym:
    1.19 -     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
    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 @@ -609,15 +609,15 @@
    1.25  done
    1.26  
    1.27  lemma (in group) iso_trans: 
    1.28 -     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
    1.29 +     "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
    1.30  by (auto simp add: iso_def hom_compose bij_betw_compose)
    1.31  
    1.32  lemma DirProdGroup_commute_iso:
    1.33 -  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
    1.34 +  shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
    1.35  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    1.36  
    1.37  lemma DirProdGroup_assoc_iso:
    1.38 -  shows "(%(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<^sub>g H \<times>\<^sub>g I) (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
    1.39 +  shows "(%(x,y,z). (x,(y,z))) \<in> (G \<times>\<^sub>g H \<times>\<^sub>g I) \<cong> (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
    1.40  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    1.41  
    1.42