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: