# HG changeset patch # User ballarin # Date 1051898570 -7200 # Node ID 0ce528cd6f19c0dab356d89252dc7dbd64f9265f # Parent 8d5de16583efa252eef1905b6e2e48c0544f7770 HOL-Algebra complete for release Isabelle2003 (modulo section headers). diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/Algebra/Group.thy --- 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 *} +header {* 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 \ H ==> inv x \ 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 \\<^sub>g H == (| carrier = carrier (G \\<^sub>s H), mult = mult (G \\<^sub>s H), one = (one G, one H) |)" -(* - DirProdGroup :: - "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \ 'b) group" - (infixr "\\<^sub>g" 80) - "G \\<^sub>g H == (| carrier = carrier (G \\<^sub>m H), - mult = mult (G \\<^sub>m H), - one = one (G \\<^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 diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/Algebra/Module.thy --- 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. *} diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/Algebra/README.html --- 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 @@ HOL/Algebra/README.html -

Algebra: Theories of Rings and Polynomials

Algebra --- Classical Algebra, using Explicit Structures and Locales

+ +This directory presents proofs in classical algebra. + +

GroupTheory, including Sylow's Theorem

+ +

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 Group 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). + +
Theory FiniteProduct extends +commutative groups by a product operator for finite sets (provided by +Clemens Ballarin). + +
Theory Coset defines +the factorization of a group and shows that the factorization a normal +subgroup is a group. + +
Theory Bij +defines bijections over sets and operations on them and shows that they +are a group. It shows that automorphisms form a group. + +
Theory Exponent the + combinatorial argument underlying Sylow's first theorem. + +
Theory Sylow +contains a proof of the first Sylow theorem. +

+ +

Rings and Polynomials

+ +

Theory CRing +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. + +
Theory Module +introduces the notion of a R-left-module over an Abelian group, where + R is a ring. + +
Theory UnivPoly +constructs univariate polynomials over rings and integral domains. + Degree function. Universal Property. +

+ +

Legacy Development of Rings using Axiomatic Type Classes

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:

-  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 @@
 Polynomials over an integral domain form an integral domain
 
 
- Still missing are
-    Polynomials over a factorial domain form a factorial domain
-    (difficult), and polynomials over a field form a pid.
-
 
[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
 
 
[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
-  Author's PhD thesis, 1999.
-
-
GroupTheory -- Group Theory using Locales, including Sylow's Theorem
-
-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:
-
-
 Theory Group 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.
-
-
Theory Bij
-defines bijections over sets and operations on them and shows that they
-are a group.  It shows that automorphisms form a group.
-
-
Theory Ring defines rings and proves
-a few basic theorems.  Ring automorphisms are shown to form a group.
-
-
Theory Sylow
-contains a proof of the first Sylow theorem.
-
-
Theory Summation Extends
-abelian groups by a summation operator for finite sets (provided by
-Clemens Ballarin).
-
+  Author's PhD thesis, 1999.
 
 
 Last modified on $Date$
 
 

-Clemens Ballarin.  Karlsruhe, October 1999
-
-ballarin@ira.uka.de
+
Clemens Ballarin.
 
 
diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/Algebra/ROOT.ML
--- 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*)
diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/Algebra/UnivPoly.thy
--- 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 \ n = \\<^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 _ "\", 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 \ A ==> f i \ carrier G = True; A = B;
   !!i. i \ B ==> f i = g i |] ==> finsum G f A = finsum G g B"
diff -r 8d5de16583ef -r 0ce528cd6f19 src/HOL/IsaMakefile
--- 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