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