new proofs about direct products, etc.
authorpaulson
Thu May 01 11:54:18 2003 +0200 (2003-05-01)
changeset 139449b34607cd83e
parent 13943 83d842ccd4aa
child 13945 5433b2755e98
new proofs about direct products, etc.
src/HOL/Algebra/Group.thy
src/HOL/Algebra/README.html
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 01 11:54:18 2003 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
     1.5    by (rule Units_inv_comm) auto                          
     1.6  
     1.7 -lemma (in group) m_inv_equality:
     1.8 +lemma (in group) inv_equality:
     1.9       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    1.10  apply (simp add: m_inv_def)
    1.11  apply (rule the_equality)
    1.12 @@ -567,6 +567,27 @@
    1.13      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    1.14        simp add: DirProdGroup_def DirProdSemigroup_def)
    1.15  
    1.16 +lemma carrier_DirProdGroup [simp]:
    1.17 +     "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
    1.18 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.19 +
    1.20 +lemma one_DirProdGroup [simp]:
    1.21 +     "one (G \<times>\<^sub>g H) = (one G, one H)"
    1.22 +  by (simp add: DirProdGroup_def DirProdSemigroup_def);
    1.23 +
    1.24 +lemma mult_DirProdGroup [simp]:
    1.25 +     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
    1.26 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.27 +
    1.28 +lemma inv_DirProdGroup [simp]:
    1.29 +  includes group G + group H
    1.30 +  assumes g: "g \<in> carrier G"
    1.31 +      and h: "h \<in> carrier H"
    1.32 +  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
    1.33 +  apply (rule group.inv_equality [OF DirProdGroup_group])
    1.34 +  apply (simp_all add: prems group_def group.l_inv)
    1.35 +  done
    1.36 +
    1.37  subsection {* Homomorphisms *}
    1.38  
    1.39  constdefs
     2.1 --- a/src/HOL/Algebra/README.html	Thu May 01 10:29:44 2003 +0200
     2.2 +++ b/src/HOL/Algebra/README.html	Thu May 01 11:54:18 2003 +0200
     2.3 @@ -48,6 +48,36 @@
     2.4  <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
     2.5    Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
     2.6  
     2.7 +<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
     2.8 +
     2.9 +<P>This directory presents proofs about group theory, by
    2.10 +Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
    2.11 +These theories use locales and were indeed the original motivation for
    2.12 +locales.  However, this treatment of groups must still be regarded as
    2.13 +experimental.  We can expect to see refinements in the future.
    2.14 +
    2.15 +Here is an outline of the directory's contents:
    2.16 +
    2.17 +<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
    2.18 +semigroups, groups, homomorphisms and the subgroup relation.  It also defines
    2.19 +the product of two groups.  It defines the factorization of a group and shows
    2.20 +that the factorization a normal subgroup is a group.
    2.21 +
    2.22 +<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
    2.23 +defines bijections over sets and operations on them and shows that they
    2.24 +are a group.  It shows that automorphisms form a group.
    2.25 +
    2.26 +<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
    2.27 +a few basic theorems.  Ring automorphisms are shown to form a group.
    2.28 +
    2.29 +<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
    2.30 +contains a proof of the first Sylow theorem.
    2.31 +
    2.32 +<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
    2.33 +abelian groups by a summation operator for finite sets (provided by
    2.34 +Clemens Ballarin).
    2.35 +</UL>
    2.36 +
    2.37  <HR>
    2.38  <P>Last modified on $Date$
    2.39