src/HOL/Algebra/Group.thy
 changeset 14761 28b5eb4a867f parent 14751 0d7850e27fed child 14803 f7557773cc87
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed May 19 11:29:47 2004 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 19 11:30:18 2004 +0200
1.3 @@ -10,6 +10,7 @@
1.4
1.5  theory Group = FuncSet + Lattice:
1.6
1.7 +
1.8  section {* From Magmas to Groups *}
1.9
1.10  text {*
1.11 @@ -195,6 +196,10 @@
1.12  locale group = monoid +
1.13    assumes Units: "carrier G <= Units G"
1.14
1.15 +
1.16 +lemma (in group) is_group: "group G"
1.17 +  by (rule group.intro [OF prems])
1.18 +
1.19  theorem groupI:
1.20    includes struct G
1.21    assumes m_closed [simp]:
1.22 @@ -552,7 +557,7 @@
1.23    apply (simp_all add: prems group_def group.l_inv)
1.24    done
1.25
1.26 -subsection {* Homomorphisms *}
1.27 +subsection {* Isomorphisms *}
1.28
1.29  constdefs (structure G and H)
1.30    hom :: "_ => _ => ('a => 'b) set"
1.31 @@ -561,8 +566,7 @@
1.32        (\<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.33
1.34  lemma (in semigroup) hom:
1.35 -  includes semigroup G
1.36 -  shows "semigroup (| carrier = hom G G, mult = op o |)"
1.37 +     "semigroup (| carrier = hom G G, mult = op o |)"
1.38  proof (rule semigroup.intro)
1.39    show "magma (| carrier = hom G G, mult = op o |)"
1.40      by (rule magma.intro) (simp add: Pi_def hom_def)
1.41 @@ -580,15 +584,43 @@
1.42    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
1.43    by (auto simp add: hom_def funcset_mem)
1.44
1.45 -lemma compose_hom:
1.46 -     "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
1.47 -      ==> compose (carrier G) h h' \<in> hom G G"
1.48 -apply (simp (no_asm_simp) add: hom_def)
1.49 -apply (intro conjI)
1.50 - apply (force simp add: funcset_compose hom_def)
1.51 -apply (simp add: compose_def group.axioms hom_mult funcset_mem)
1.52 +lemma (in group) hom_compose:
1.53 +     "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
1.54 +apply (auto simp add: hom_def funcset_compose)
1.55 +apply (simp add: compose_def funcset_mem)
1.56  done
1.57
1.58 +
1.59 +subsection {* Isomorphisms *}
1.60 +
1.61 +constdefs (structure G and H)
1.62 +  iso :: "_ => _ => ('a => 'b) set"
1.63 +  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
1.64 +
1.65 +lemma iso_refl: "(%x. x) \<in> iso G G"
1.66 +by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
1.67 +
1.68 +lemma (in group) iso_sym:
1.69 +     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
1.70 +apply (simp add: iso_def bij_betw_Inv)
1.71 +apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
1.72 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
1.73 +apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
1.74 +done
1.75 +
1.76 +lemma (in group) iso_trans:
1.77 +     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
1.78 +by (auto simp add: iso_def hom_compose bij_betw_compose)
1.79 +
1.80 +lemma DirProdGroup_commute_iso:
1.81 +  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
1.82 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
1.83 +
1.84 +lemma DirProdGroup_assoc_iso:
1.85 +  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.86 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
1.87 +
1.88 +
1.89  locale group_hom = group G + group H + var h +
1.90    assumes homh: "h \<in> hom G H"
1.91    notes hom_mult [simp] = hom_mult [OF homh]
1.92 @@ -692,7 +724,7 @@
1.93        x \<otimes> y = y \<otimes> x"
1.94    shows "comm_group G"
1.95    by (fast intro: comm_group.intro comm_semigroup_axioms.intro
1.96 -    group.axioms prems)
1.97 +                  is_group prems)
1.98
1.99  lemma comm_groupI:
1.100    includes struct G
1.101 @@ -736,14 +768,10 @@
1.102  lemma (in group) subgroup_inv_equality:
1.103    "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
1.104  apply (rule_tac inv_equality [THEN sym])
1.105 -  apply (rule group.l_inv [OF subgroup_imp_group, simplified])
1.106 -   apply assumption+
1.107 - apply (rule subsetD [OF subgroup.subset])
1.108 -  apply assumption+
1.109 -apply (rule subsetD [OF subgroup.subset])
1.110 - apply assumption
1.111 -apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified])
1.112 -  apply assumption+
1.113 +  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
1.114 + apply (rule subsetD [OF subgroup.subset], assumption+)
1.115 +apply (rule subsetD [OF subgroup.subset], assumption)
1.116 +apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
1.117  done
1.118
1.119  theorem (in group) subgroups_Inter:
```