products/sources/formale sprachen/Isabelle/HOL/Algebra/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lattice.thy   Sprache: HTML

Original von: Isabelle©
 products/sources/formale sprachen/Isabelle/HOL/Algebra/README.html


<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<HTML>

<HEAD>
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
  <TITLE>HOL/Algebra/README.html</TITLE>
</HEAD>

<BODY>

<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>

This directory contains proofs in classical algebra.  It is intended
as a base for any algebraic development in Isabelle.  Emphasis is on
reusability.  This is achieved by modelling algebraic structures
as first-class citizens of the logic (not axiomatic type classes, say).
The library is expected to grow in future releases of Isabelle.
Contributions are welcome.

<H2>GroupTheory, including Sylow's Theorem

<P>These proofs are mainly by Florian Kammüller.  (Later, Larry
Paulson simplified some of the proofs.)  These theories were indeed
the original motivation for locales.

Here is an outline of the directory's contents:
  • Theory
    HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
    groups, commutative monoids, commutative groups, homomorphisms and the
    subgroup relation.  It also defines the product of two groups
    (This theory was reimplemented by Clemens Ballarin).

    <LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
    commutative groups by a product operator for finite sets (provided by
    Clemens Ballarin).

    <LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> 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="Exponent.html"><CODE>Exponent</CODE></A> the
         combinatorial argument underlying Sylow's first theorem.

    <LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
    contains a proof of the first Sylow theorem.
    </UL>

    <H2>Rings and Polynomials</H2>

    <UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
    defines Abelian monoids and groups.  The difference to commutative
          structures is merely notational:  the binary operation is
          addition rather than multiplication.  Commutative rings are
          obtained by inheriting properties from Abelian groups and
          commutative monoids.  Further structures in the algebraic
          hierarchy of rings: integral domain.

    <LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
    introduces the notion of a R-left-module over an Abelian group, where
     R is a ring.

    <LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
    constructs univariate polynomials over rings and integral domains.
       Degree function.  Universal Property.
    </UL>

    <H2>Development of Polynomials using Type Classes</H2>

    <P>A development of univariate polynomials for HOL's ring classes
    is available at <CODE>HOL/Library/Polynomial</CODE>.

    <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

    <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
      Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.

    <ADDRESS>
    <P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
    </ADDRESS>
    </BODY>
    </HTML>

    ¤ Dauer der Verarbeitung: 0.21 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff