src/HOL/Algebra/Group.thy
changeset 20318 0e0ea63fe768
parent 19984 29bb4659f80a
child 21041 60e418260b4d
--- a/src/HOL/Algebra/Group.thy	Thu Aug 03 14:53:57 2006 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Aug 03 14:57:26 2006 +0200
@@ -6,19 +6,17 @@
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
 
-header {* Groups *}
-
 theory Group imports FuncSet Lattice begin
 
 
 section {* Monoids and Groups *}
 
+subsection {* Definitions *}
+
 text {*
   Definitions follow \cite{Jacobson:1985}.
 *}
 
-subsection {* Definitions *}
-
 record 'a monoid =  "'a partial_object" +
   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
   one     :: 'a ("\<one>\<index>")
@@ -291,6 +289,7 @@
   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   using Units_l_inv by simp
 
+
 subsection {* Cancellation Laws and Basic Properties *}
 
 lemma (in group) l_cancel [simp]:
@@ -373,15 +372,19 @@
   "\<one> (^) (z::int) = \<one>"
   by (simp add: int_pow_def2)
 
+
 subsection {* Subgroups *}
 
 locale subgroup =
   fixes H and G (structure)
   assumes subset: "H \<subseteq> carrier G"
     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
-    and  one_closed [simp]: "\<one> \<in> H"
+    and one_closed [simp]: "\<one> \<in> H"
     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
 
+lemma (in subgroup) is_subgroup:
+  "subgroup H G" .
+
 declare (in subgroup) group.intro [intro]
 
 lemma (in subgroup) mem_carrier [simp]:
@@ -440,6 +443,7 @@
   "subgroup (Units G) G"
 *)
 
+
 subsection {* Direct Products *}
 
 constdefs
@@ -524,9 +528,6 @@
 apply (simp add: compose_def funcset_mem)
 done
 
-
-subsection {* Isomorphisms *}
-
 constdefs
   iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
   "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
@@ -590,6 +591,7 @@
   with x show ?thesis by (simp del: H.r_inv)
 qed
 
+
 subsection {* Commutative Structures *}
 
 text {*
@@ -598,8 +600,6 @@
   \emph{Abelian}.
 *}
 
-subsection {* Definition *}
-
 locale comm_monoid = monoid +
   assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
 
@@ -679,7 +679,8 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   by (simp add: m_ac inv_mult_group)
 
-subsection {* Lattice of subgroups of a group *}
+
+subsection {* The Lattice of Subgroups of a Group *}
 
 text_raw {* \label{sec:subgroup-lattice} *}