src/ZF/ex/Group.thy
changeset 19931 fb32b43e7f80
parent 16417 9bc16273c2d4
child 21233 5a5c8ea5f66a
     1.1 --- a/src/ZF/ex/Group.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/ZF/ex/Group.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -89,8 +89,7 @@
     1.4    assumes inv_ex:
     1.5       "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
     1.6  
     1.7 -lemma (in group) is_group [simp]: "group(G)"
     1.8 -  by (rule group.intro [OF prems]) 
     1.9 +lemma (in group) is_group [simp]: "group(G)" .
    1.10  
    1.11  theorem groupI:
    1.12    includes struct G
    1.13 @@ -328,7 +327,7 @@
    1.14        and h: "h \<in> carrier(H)"
    1.15    shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
    1.16    apply (rule group.inv_equality [OF DirProdGroup_group])
    1.17 -  apply (simp_all add: prems group_def group.l_inv)
    1.18 +  apply (simp_all add: prems group.l_inv)
    1.19    done
    1.20  
    1.21  subsection {* Isomorphisms *}
    1.22 @@ -636,8 +635,7 @@
    1.23  
    1.24  lemma (in group) normalI: 
    1.25    "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
    1.26 -apply (simp add: normal_def normal_axioms_def, auto) 
    1.27 -  by (blast intro: prems)
    1.28 +  by (simp add: normal_def normal_axioms_def)
    1.29  
    1.30  lemma (in normal) inv_op_closed1:
    1.31       "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
    1.32 @@ -822,8 +820,8 @@
    1.33  lemma (in normal) rcos_mult_step3:
    1.34       "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
    1.35        \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
    1.36 -by (simp add: setmult_rcos_assoc coset_mult_assoc
    1.37 -              subgroup_mult_id subset prems)
    1.38 +  by (simp add: setmult_rcos_assoc coset_mult_assoc
    1.39 +              subgroup_mult_id subset prems normal.axioms)
    1.40  
    1.41  lemma (in normal) rcos_sum:
    1.42       "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
    1.43 @@ -833,7 +831,7 @@
    1.44  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
    1.45    -- {* generalizes @{text subgroup_mult_id} *}
    1.46    by (auto simp add: RCOSETS_def subset
    1.47 -        setmult_rcos_assoc subgroup_mult_id prems)
    1.48 +        setmult_rcos_assoc subgroup_mult_id prems normal.axioms)
    1.49  
    1.50  
    1.51  subsubsection{*Two distinct right cosets are disjoint*}
    1.52 @@ -1008,7 +1006,7 @@
    1.53  
    1.54  lemma (in normal) rcosets_inv_mult_group_eq:
    1.55       "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
    1.56 -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
    1.57 +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms)
    1.58  
    1.59  theorem (in normal) factorgroup_is_group:
    1.60    "group (G Mod H)"