src/HOL/Algebra/AbelCoset.thy
 changeset 27717 21bbd410ba04 parent 27611 2c01c0bdb385 child 28823 dcbef866c9e2
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Aug 01 17:41:37 2008 +0200
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Aug 01 18:10:52 2008 +0200
1.3 @@ -9,9 +9,9 @@
1.4  begin
1.5
1.6
1.7 -section {* More Lifting from Groups to Abelian Groups *}
1.8 +subsection {* More Lifting from Groups to Abelian Groups *}
1.9
1.10 -subsection {* Definitions *}
1.11 +subsubsection {* Definitions *}
1.12
1.13  text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
1.14    up with better syntax here *}
1.15 @@ -102,7 +102,7 @@
1.16  by (fold a_inv_def)
1.17
1.18
1.19 -subsection {* Cosets *}
1.20 +subsubsection {* Cosets *}
1.21
1.22  lemma (in abelian_group) a_coset_add_assoc:
1.23       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
1.24 @@ -178,7 +178,7 @@
1.25  *)
1.26
1.27
1.28 -subsection {* Subgroups *}
1.29 +subsubsection {* Subgroups *}
1.30
1.31  locale additive_subgroup = var H + struct G +
1.32    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.33 @@ -214,9 +214,7 @@
1.34      folded a_inv_def, simplified monoid_record_simps])
1.35
1.36
1.37 -subsection {* Normal additive subgroups *}
1.38 -
1.39 -subsubsection {* Definition of @{text "abelian_subgroup"} *}
1.40 +subsubsection {* Additive subgroups are normal *}
1.41
1.42  text {* Every subgroup of an @{text "abelian_group"} is normal *}
1.43
1.44 @@ -385,7 +383,7 @@
1.45      folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
1.46
1.47
1.48 -subsection {* Congruence Relation *}
1.49 +subsubsection {* Congruence Relation *}
1.50
1.51  lemma (in abelian_subgroup) a_equiv_rcong:
1.52     shows "equiv (carrier G) (racong H)"
1.53 @@ -446,7 +444,7 @@
1.54      (fast intro!: additive_subgroup.a_subgroup)+
1.55
1.56
1.57 -subsection {* Factorization *}
1.58 +subsubsection {* Factorization *}
1.59
1.60  lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
1.61
1.62 @@ -518,7 +516,7 @@
1.63  text {* The isomorphism theorems have been omitted from lifting, at
1.64    least for now *}
1.65
1.66 -subsection{*The First Isomorphism Theorem*}
1.67 +subsubsection{*The First Isomorphism Theorem*}
1.68
1.69  text{*The quotient by the kernel of a homomorphism is isomorphic to the
1.70    range of that homomorphism.*}
1.71 @@ -531,7 +529,7 @@
1.72  by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
1.73
1.74
1.75 -subsection {* Homomorphisms *}
1.76 +subsubsection {* Homomorphisms *}
1.77
1.78  lemma abelian_group_homI:
1.79    assumes "abelian_group G"
1.80 @@ -640,12 +638,10 @@
1.81  by (rule group_hom.FactGroup_iso[OF a_group_hom,
1.82      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
1.83
1.84 -section {* Lemmas Lifted from CosetExt.thy *}
1.85 +subsubsection {* Cosets *}
1.86
1.87  text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
1.88
1.89 -subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
1.90 -
1.91  lemma (in additive_subgroup) a_Hcarr [simp]:
1.92    assumes hH: "h \<in> H"
1.93    shows "h \<in> carrier G"
1.94 @@ -653,8 +649,6 @@
1.95      simplified monoid_record_simps]) (rule hH)
1.96
1.97
1.98 -subsection {* Lemmas for Right Cosets *}
1.99 -
1.100  lemma (in abelian_subgroup) a_elemrcos_carrier:
1.101    assumes acarr: "a \<in> carrier G"
1.102        and a': "a' \<in> H +> a"
1.103 @@ -722,8 +716,6 @@
1.104      folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
1.105
1.106
1.107 -subsection {* Lemmas for the Set of Right Cosets *}
1.108 -
1.109  lemma (in abelian_subgroup) a_rcosets_carrier:
1.110    "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
1.111  by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
1.112 @@ -731,7 +723,7 @@
1.113
1.114
1.115
1.116 -subsection {* Addition of Subgroups *}
1.117 +subsubsection {* Addition of Subgroups *}
1.118
1.119  lemma (in abelian_monoid) set_add_closed:
1.120    assumes Acarr: "A \<subseteq> carrier G"
```