author ballarin Fri, 02 May 2003 20:02:50 +0200 changeset 13949 0ce528cd6f19 parent 13948 8d5de16583ef child 13950 74f638d8a829
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
 src/HOL/Algebra/Group.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Module.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/README.html file | annotate | diff | comparison | revisions src/HOL/Algebra/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Algebra/UnivPoly.thy file | annotate | diff | comparison | revisions src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
--- a/src/HOL/Algebra/Group.thy	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri May 02 20:02:50 2003 +0200
@@ -6,14 +6,14 @@
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
*)

-header {* Algebraic Structures up to Commutative Groups *}

theory Group = FuncSet:

-axclass number < type
+(* axclass number < type

instance nat :: number ..
-instance int :: number ..
+instance int :: number .. *)

section {* From Magmas to Groups *}

@@ -416,12 +416,7 @@
and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"

declare (in subgroup) group.intro [intro]
-(*
-lemma (in subgroup) l_oneI [intro]:
-  includes l_one G
-  shows "l_one (G(| carrier := H |))"
-  by rule simp_all
-*)
+
lemma (in subgroup) group_axiomsI [intro]:
includes group G
shows "group_axioms (G(| carrier := H |))"
@@ -511,15 +506,6 @@
"G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
mult = mult (G \<times>\<^sub>s H),
one = (one G, one H) |)"
-(*
-  DirProdGroup ::
-    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
-    (infixr "\<times>\<^sub>g" 80)
-  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
-    mult = mult (G \<times>\<^sub>m H),
-    one = one (G \<times>\<^sub>m H),
-    m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
-*)

lemma DirProdSemigroup_magma:
includes magma G + magma H
@@ -659,7 +645,7 @@
with x show ?thesis by simp
qed

-section {* Commutative Structures *}
+subsection {* Commutative Structures *}

text {*
Naming convention: multiplicative structures that are commutative
--- a/src/HOL/Algebra/Module.thy	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/Module.thy	Fri May 02 20:02:50 2003 +0200
@@ -139,7 +139,7 @@
finally show ?thesis .
qed

-subsection {* Every Abelian Group is a Z-module *}
+subsection {* Every Abelian Group is a \$\mathbb{Z}\$-module *}

text {* Not finished. *}

--- a/src/HOL/Algebra/README.html	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/README.html	Fri May 02 20:02:50 2003 +0200
@@ -1,7 +1,61 @@
<!-- \$Id\$ -->

-<H2>Algebra: Theories of Rings and Polynomials</H2>
+<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
+
+This directory presents proofs in classical algebra.
+
+<H2>GroupTheory, including Sylow's Theorem</H2>
+
+<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: <UL> <LI>Theory <A
+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="CRing.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>Legacy Development of Rings using Axiomatic Type Classes</H2>

<P>This development of univariate polynomials is separated into an
abstract development of rings and the development of polynomials
@@ -16,7 +70,6 @@
following are available:

<PRE>
-  ringS:	Syntactic class
ring:		Commutative rings with one (including a summation
operator, which is needed for the polynomials)
domain:	Integral domains
@@ -39,51 +92,15 @@
<LI>Polynomials over an integral domain form an integral domain

- <P>Still missing are
-    Polynomials over a factorial domain form a factorial domain
-    (difficult), and polynomials over a field form a pid.
-
<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

<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>
+  Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.

<HR>

-<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999
-
-<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
+<P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
</BODY></HTML>
--- a/src/HOL/Algebra/ROOT.ML	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Fri May 02 20:02:50 2003 +0200
@@ -4,15 +4,25 @@
Author: Clemens Ballarin, started 24 September 1999
*)

-(* New development, based on explicit structures *)
+(*** New development, based on explicit structures ***)
+
+(* Preliminaries from set and number theory *)

no_document use_thy "FuncSet";
-use_thy "Sylow";		(* Groups *)
+no_document use_thy "Primes";
+
+(* Groups *)
+
+use_thy "FiniteProduct";	(* Product operator for commutative groups *)
+use_thy "Sylow";		(* Sylow's theorem *)
use_thy "Bij";			(* Automorphism Groups *)
+
+(* Rings *)
+
use_thy "UnivPoly";		(* Rings and polynomials *)

-(* Old development, based on axiomatic type classes.
-   Will be withdrawn in future. *)
+(*** Old development, based on axiomatic type classes.
+     Will be withdrawn in future. ***)

-with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
-with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
+with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
+with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)
--- a/src/HOL/Algebra/UnivPoly.thy	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri May 02 20:02:50 2003 +0200
@@ -9,8 +9,7 @@

section {* Univariate Polynomials *}

-subsection
-  {* Definition of the Constructor for Univariate Polynomials @{term UP} *}
+subsection {* The Constructor for Univariate Polynomials *}

(* Could alternatively use locale ...
locale bound = cring + var bound +
@@ -595,7 +594,7 @@
lemmas (in UP_cring) UP_smult_r_minus =
algebra.smult_r_minus [OF UP_algebra]

-subsection {* Further Lemmas Involving @{term monom} *}
+subsection {* Further lemmas involving monomials *}

lemma (in UP_cring) monom_zero [simp]:
"monom P \<zero> n = \<zero>\<^sub>2"
@@ -767,7 +766,7 @@
with R show "x = y" by simp
qed

-subsection {* The Degree Function *}
+subsection {* The degree function *}

constdefs
deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
@@ -1060,7 +1059,7 @@
Context.>> (fn thy => (simpset_ref_of thy :=
simpset_of thy setsubgoaler asm_simp_tac; thy)) *}

-subsection {* Polynomial over an Integral Domain are an Integral Domain *}
+subsection {* Polynomials over an integral domain form an integral domain *}

lemma domainI:
assumes cring: "cring R"
@@ -1134,13 +1133,13 @@
by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])

-subsection {* Evaluation Homomorphism *}
+subsection {* Evaluation Homomorphism and Universal Property*}

ML_setup {*
Context.>> (fn thy => (simpset_ref_of thy :=
simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}

-(* alternative congruence rule (more efficient)
+(* alternative congruence rule (possibly more efficient)
lemma (in abelian_monoid) finsum_cong2:
"[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
!!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
--- a/src/HOL/IsaMakefile	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/IsaMakefile	Fri May 02 20:02:50 2003 +0200
@@ -7,12 +7,11 @@
## targets

default: HOL
-images: HOL HOL-Real HOL-Hyperreal TLA
+images: HOL HOL-Algebra HOL-Real HOL-Hyperreal TLA

#Note: keep targets sorted (except for HOL-Library)
test: \
HOL-Library \
-  HOL-Algebra \
HOL-Auth \
HOL-AxClasses \
HOL-Bali \
@@ -340,6 +339,7 @@
HOL-Algebra: HOL \$(LOG)/HOL-Algebra.gz

\$(LOG)/HOL-Algebra.gz: \$(OUT)/HOL Algebra/ROOT.ML \
+  Library/Primes.thy Library/FuncSet.thy \
Algebra/Bij.thy \
Algebra/CRing.thy \
Algebra/Coset.thy \
@@ -357,12 +357,13 @@
Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
Algebra/abstract/order.ML \
+  Algebra/document/root.tex \
Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
Algebra/poly/Polynomial.thy \
Algebra/poly/UnivPoly2.ML Algebra/poly/UnivPoly2.thy \
Algebra/ringsimp.ML
-	@\$(ISATOOL) usedir \$(OUT)/HOL Algebra
+	@cd Algebra; \$(ISATOOL) usedir -b \$(OUT)/HOL HOL-Algebra

## HOL-Auth