src/HOL/Algebra/AbelCoset.thy

 theory AbelCoset
 imports Coset Ring
 begin
 
 
-section {* More Lifting from Groups to Abelian Groups *}
-
-subsection {* Definitions *}
+subsection {* More Lifting from Groups to Abelian Groups *}
+
+subsubsection {* Definitions *}
 
 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
   up with better syntax here *}
 
 no_notation Plus (infixr "<+>" 65)

   shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
 unfolding A_SET_INV_defs
 by (fold a_inv_def)
 
 
-subsection {* Cosets *}
+subsubsection {* Cosets *}
 
 lemma (in abelian_group) a_coset_add_assoc:
      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
       ==> (M +> g) +> h = M +> (g \<oplus> h)"
 by (rule group.coset_mult_assoc [OF a_group,

 by (rule group.rcos_self [OF a_group,
     folded a_r_coset_def, simplified monoid_record_simps])
 *)
 
 
-subsection {* Subgroups *}
+subsubsection {* Subgroups *}
 
 locale additive_subgroup = var H + struct G +
   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 lemma (in additive_subgroup) is_additive_subgroup:

      "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
 by (rule subgroup.m_inv_closed[OF a_subgroup,
     folded a_inv_def, simplified monoid_record_simps])
 
 
-subsection {* Normal additive subgroups *}
-
-subsubsection {* Definition of @{text "abelian_subgroup"} *}
+subsubsection {* Additive subgroups are normal *}
 
 text {* Every subgroup of an @{text "abelian_group"} is normal *}
 
 locale abelian_subgroup = additive_subgroup H G + abelian_group G +
   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

   -- {* generalizes @{text subgroup_mult_id} *}
 by (rule normal.rcosets_mult_eq [OF a_normal,
     folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
 
 
-subsection {* Congruence Relation *}
+subsubsection {* Congruence Relation *}
 
 lemma (in abelian_subgroup) a_equiv_rcong:
    shows "equiv (carrier G) (racong H)"
 by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
     folded a_r_congruent_def, simplified monoid_record_simps])

 by (rule group.lagrange [OF a_group,
     folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
     (fast intro!: additive_subgroup.a_subgroup)+
 
 
-subsection {* Factorization *}
+subsubsection {* Factorization *}
 
 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
 
 lemma A_FactGroup_def':
   fixes G (structure)

     folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
 
 text {* The isomorphism theorems have been omitted from lifting, at
   least for now *}
 
-subsection{*The First Isomorphism Theorem*}
+subsubsection{*The First Isomorphism Theorem*}
 
 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   range of that homomorphism.*}
 
 lemmas a_kernel_defs =

 lemma a_kernel_def':
   "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
 
 
-subsection {* Homomorphisms *}
+subsubsection {* Homomorphisms *}
 
 lemma abelian_group_homI:
   assumes "abelian_group G"
   assumes "abelian_group H"
   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)

    \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
           (| carrier = carrier H, mult = add H, one = zero H |)"
 by (rule group_hom.FactGroup_iso[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
-section {* Lemmas Lifted from CosetExt.thy *}
+subsubsection {* Cosets *}
 
 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
-
-subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
 
 lemma (in additive_subgroup) a_Hcarr [simp]:
   assumes hH: "h \<in> H"
   shows "h \<in> carrier G"
 by (rule subgroup.mem_carrier [OF a_subgroup,
     simplified monoid_record_simps]) (rule hH)
 
-
-subsection {* Lemmas for Right Cosets *}
 
 lemma (in abelian_subgroup) a_elemrcos_carrier:
   assumes acarr: "a \<in> carrier G"
       and a': "a' \<in> H +> a"
   shows "a' \<in> carrier G"

   shows "y \<in> H +> x"
 by (rule group.repr_independenceD [OF a_group a_subgroup,
     folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
 
 
-subsection {* Lemmas for the Set of Right Cosets *}
-
 lemma (in abelian_subgroup) a_rcosets_carrier:
   "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
 by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
     folded A_RCOSETS_def, simplified monoid_record_simps])
 
 
 
-subsection {* Addition of Subgroups *}
+subsubsection {* Addition of Subgroups *}
 
 lemma (in abelian_monoid) set_add_closed:
   assumes Acarr: "A \<subseteq> carrier G"
       and Bcarr: "B \<subseteq> carrier G"
   shows "A <+> B \<subseteq> carrier G"