author paulson Wed May 19 11:30:18 2004 +0200 (2004-05-19) changeset 14761 28b5eb4a867f parent 14760 a08e916f4946 child 14762 bd349ff7907a
 src/HOL/Algebra/Bij.thy file | annotate | diff | revisions src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Bij.thy	Wed May 19 11:29:47 2004 +0200
1.2 +++ b/src/HOL/Algebra/Bij.thy	Wed May 19 11:30:18 2004 +0200
1.3 @@ -133,7 +133,8 @@
1.4    apply (blast intro: dest: id_in_auto)
1.5   apply (simp del: restrict_apply
1.6               add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
1.7 -apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
1.8 +apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
1.9 +                      compose_Bij)
1.10  done
1.11
1.12  theorem AutoGroup: "group G ==> group (AutoGroup G)"
```
```     2.1 --- a/src/HOL/Algebra/Coset.thy	Wed May 19 11:29:47 2004 +0200
2.2 +++ b/src/HOL/Algebra/Coset.thy	Wed May 19 11:30:18 2004 +0200
2.3 @@ -502,8 +502,7 @@
2.4  lemma (in group) inv_FactGroup:
2.5       "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
2.6  apply (rule group.inv_equality [OF factorgroup_is_group])
2.7 -apply (simp_all add: FactGroup_def setinv_closed
2.8 -    setrcos_inv_mult_group_eq group.intro [OF prems])
2.9 +apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
2.10  done
2.11
2.12  text{*The coset map is a homomorphism from @{term G} to the quotient group
2.13 @@ -511,7 +510,6 @@
2.14  lemma (in group) r_coset_hom_Mod:
2.15    assumes N: "N <| G"
2.16    shows "(r_coset G N) \<in> hom G (G Mod N)"
2.17 -by (simp add: FactGroup_def rcosets_def Pi_def hom_def
2.18 -           rcos_sum group.intro prems)
2.19 +by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N)
2.20
2.21  end
```
```     3.1 --- a/src/HOL/Algebra/Group.thy	Wed May 19 11:29:47 2004 +0200
3.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 19 11:30:18 2004 +0200
3.3 @@ -10,6 +10,7 @@
3.4
3.5  theory Group = FuncSet + Lattice:
3.6
3.7 +
3.8  section {* From Magmas to Groups *}
3.9
3.10  text {*
3.11 @@ -195,6 +196,10 @@
3.12  locale group = monoid +
3.13    assumes Units: "carrier G <= Units G"
3.14
3.15 +
3.16 +lemma (in group) is_group: "group G"
3.17 +  by (rule group.intro [OF prems])
3.18 +
3.19  theorem groupI:
3.20    includes struct G
3.21    assumes m_closed [simp]:
3.22 @@ -552,7 +557,7 @@
3.23    apply (simp_all add: prems group_def group.l_inv)
3.24    done
3.25
3.26 -subsection {* Homomorphisms *}
3.27 +subsection {* Isomorphisms *}
3.28
3.29  constdefs (structure G and H)
3.30    hom :: "_ => _ => ('a => 'b) set"
3.31 @@ -561,8 +566,7 @@
3.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)}"
3.33
3.34  lemma (in semigroup) hom:
3.35 -  includes semigroup G
3.36 -  shows "semigroup (| carrier = hom G G, mult = op o |)"
3.37 +     "semigroup (| carrier = hom G G, mult = op o |)"
3.38  proof (rule semigroup.intro)
3.39    show "magma (| carrier = hom G G, mult = op o |)"
3.40      by (rule magma.intro) (simp add: Pi_def hom_def)
3.41 @@ -580,15 +584,43 @@
3.42    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
3.43    by (auto simp add: hom_def funcset_mem)
3.44
3.45 -lemma compose_hom:
3.46 -     "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
3.47 -      ==> compose (carrier G) h h' \<in> hom G G"
3.48 -apply (simp (no_asm_simp) add: hom_def)
3.49 -apply (intro conjI)
3.50 - apply (force simp add: funcset_compose hom_def)
3.51 -apply (simp add: compose_def group.axioms hom_mult funcset_mem)
3.52 +lemma (in group) hom_compose:
3.53 +     "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
3.54 +apply (auto simp add: hom_def funcset_compose)
3.55 +apply (simp add: compose_def funcset_mem)
3.56  done
3.57
3.58 +
3.59 +subsection {* Isomorphisms *}
3.60 +
3.61 +constdefs (structure G and H)
3.62 +  iso :: "_ => _ => ('a => 'b) set"
3.63 +  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
3.64 +
3.65 +lemma iso_refl: "(%x. x) \<in> iso G G"
3.66 +by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
3.67 +
3.68 +lemma (in group) iso_sym:
3.69 +     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
3.70 +apply (simp add: iso_def bij_betw_Inv)
3.71 +apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
3.72 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
3.73 +apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
3.74 +done
3.75 +
3.76 +lemma (in group) iso_trans:
3.77 +     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
3.78 +by (auto simp add: iso_def hom_compose bij_betw_compose)
3.79 +
3.80 +lemma DirProdGroup_commute_iso:
3.81 +  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
3.82 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
3.83 +
3.84 +lemma DirProdGroup_assoc_iso:
3.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))"
3.86 +by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
3.87 +
3.88 +
3.89  locale group_hom = group G + group H + var h +
3.90    assumes homh: "h \<in> hom G H"
3.91    notes hom_mult [simp] = hom_mult [OF homh]
3.92 @@ -692,7 +724,7 @@
3.93        x \<otimes> y = y \<otimes> x"
3.94    shows "comm_group G"
3.95    by (fast intro: comm_group.intro comm_semigroup_axioms.intro
3.96 -    group.axioms prems)
3.97 +                  is_group prems)
3.98
3.99  lemma comm_groupI:
3.100    includes struct G
3.101 @@ -736,14 +768,10 @@
3.102  lemma (in group) subgroup_inv_equality:
3.103    "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
3.104  apply (rule_tac inv_equality [THEN sym])
3.105 -  apply (rule group.l_inv [OF subgroup_imp_group, simplified])
3.106 -   apply assumption+
3.107 - apply (rule subsetD [OF subgroup.subset])
3.108 -  apply assumption+
3.109 -apply (rule subsetD [OF subgroup.subset])
3.110 - apply assumption
3.111 -apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified])
3.112 -  apply assumption+
3.113 +  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
3.114 + apply (rule subsetD [OF subgroup.subset], assumption+)
3.115 +apply (rule subsetD [OF subgroup.subset], assumption)
3.116 +apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
3.117  done
3.118
3.119  theorem (in group) subgroups_Inter:
```