# HG changeset patch
# User paulson
# Date 1051782858 -7200
# Node ID 9b34607cd83e40c234b3c49a98448afbfb9720d0
# Parent  83d842ccd4aac52b38a7512d0970ca733786a31c
new proofs about direct products, etc.

diff -r 83d842ccd4aa -r 9b34607cd83e src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu May 01 11:54:18 2003 +0200
@@ -348,7 +348,7 @@
   "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
   by (rule Units_inv_comm) auto                          
 
-lemma (in group) m_inv_equality:
+lemma (in group) inv_equality:
      "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
 apply (simp add: m_inv_def)
 apply (rule the_equality)
@@ -567,6 +567,27 @@
     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
       simp add: DirProdGroup_def DirProdSemigroup_def)
 
+lemma carrier_DirProdGroup [simp]:
+     "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
+  by (simp add: DirProdGroup_def DirProdSemigroup_def)
+
+lemma one_DirProdGroup [simp]:
+     "one (G \<times>\<^sub>g H) = (one G, one H)"
+  by (simp add: DirProdGroup_def DirProdSemigroup_def);
+
+lemma mult_DirProdGroup [simp]:
+     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
+  by (simp add: DirProdGroup_def DirProdSemigroup_def)
+
+lemma inv_DirProdGroup [simp]:
+  includes group G + group H
+  assumes g: "g \<in> carrier G"
+      and h: "h \<in> carrier H"
+  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
+  apply (rule group.inv_equality [OF DirProdGroup_group])
+  apply (simp_all add: prems group_def group.l_inv)
+  done
+
 subsection {* Homomorphisms *}
 
 constdefs
diff -r 83d842ccd4aa -r 9b34607cd83e src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html	Thu May 01 10:29:44 2003 +0200
+++ b/src/HOL/Algebra/README.html	Thu May 01 11:54:18 2003 +0200
@@ -48,6 +48,36 @@
 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
   Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
 
+<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
+
+<P>This directory presents proofs about group theory, by
+Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
+These theories use locales and were indeed the original motivation for
+locales.  However, this treatment of groups must still be regarded as
+experimental.  We can expect to see refinements in the future.
+
+Here is an outline of the directory's contents:
+
+<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
+semigroups, groups, homomorphisms and the subgroup relation.  It also defines
+the product of two groups.  It defines the factorization of a group and shows
+that the factorization a normal subgroup is a group.
+
+<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
+defines bijections over sets and operations on them and shows that they
+are a group.  It shows that automorphisms form a group.
+
+<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
+a few basic theorems.  Ring automorphisms are shown to form a group.
+
+<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
+contains a proof of the first Sylow theorem.
+
+<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
+abelian groups by a summation operator for finite sets (provided by
+Clemens Ballarin).
+</UL>
+
 <HR>
 <P>Last modified on $Date$