src/HOL/Algebra/Group.thy

   Author: Clemens Ballarin, started 4 February 2003
 
 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>")
 

 
 lemma (in group) l_inv [simp]:
   "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]:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    (x \<otimes> y = x \<otimes> z) = (y = z)"

 
 lemma (in group) int_pow_one [simp]:
   "\<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]:
   "x \<in> H \<Longrightarrow> x \<in> carrier G"

 
 (*
 lemma (in monoid) Units_subgroup:
   "subgroup (Units G) G"
 *)
+
 
 subsection {* Direct Products *}
 
 constdefs
   DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid"  (infixr "\<times>\<times>" 80)

      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 apply (auto simp add: hom_def funcset_compose) 
 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)}"
 
 lemma iso_refl: "(%x. x) \<in> G \<cong> G"

     by (simp add: hom_mult [symmetric] del: hom_mult)
   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   with x show ?thesis by (simp del: H.r_inv)
 qed
 
+
 subsection {* Commutative Structures *}
 
 text {*
   Naming convention: multiplicative structures that are commutative
   are called \emph{commutative}, additive structures are called
   \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"
 
 lemma (in comm_monoid) m_lcomm:

 
 lemma (in comm_group) inv_mult:
   "[| 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} *}
 
 theorem (in group) subgroups_partial_order:
   "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"