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
```