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"