HOL-Algebra complete for release Isabelle2003 (modulo section headers).
authorballarin
Fri May 02 20:02:50 2003 +0200 (2003-05-02)
changeset 139490ce528cd6f19
parent 13948 8d5de16583ef
child 13950 74f638d8a829
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/README.html
src/HOL/Algebra/ROOT.ML
src/HOL/Algebra/UnivPoly.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Algebra/Group.thy	Fri May 02 16:43:36 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Fri May 02 20:02:50 2003 +0200
     1.3 @@ -6,14 +6,14 @@
     1.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     1.5  *)
     1.6  
     1.7 -header {* Algebraic Structures up to Commutative Groups *}
     1.8 +header {* Groups *}
     1.9  
    1.10  theory Group = FuncSet:
    1.11  
    1.12 -axclass number < type
    1.13 +(* axclass number < type
    1.14  
    1.15  instance nat :: number ..
    1.16 -instance int :: number ..
    1.17 +instance int :: number .. *)
    1.18  
    1.19  section {* From Magmas to Groups *}
    1.20  
    1.21 @@ -416,12 +416,7 @@
    1.22      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
    1.23  
    1.24  declare (in subgroup) group.intro [intro]
    1.25 -(*
    1.26 -lemma (in subgroup) l_oneI [intro]:
    1.27 -  includes l_one G
    1.28 -  shows "l_one (G(| carrier := H |))"
    1.29 -  by rule simp_all
    1.30 -*)
    1.31 +
    1.32  lemma (in subgroup) group_axiomsI [intro]:
    1.33    includes group G
    1.34    shows "group_axioms (G(| carrier := H |))"
    1.35 @@ -511,15 +506,6 @@
    1.36    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
    1.37      mult = mult (G \<times>\<^sub>s H),
    1.38      one = (one G, one H) |)"
    1.39 -(*
    1.40 -  DirProdGroup ::
    1.41 -    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
    1.42 -    (infixr "\<times>\<^sub>g" 80)
    1.43 -  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    1.44 -    mult = mult (G \<times>\<^sub>m H),
    1.45 -    one = one (G \<times>\<^sub>m H),
    1.46 -    m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
    1.47 -*)
    1.48  
    1.49  lemma DirProdSemigroup_magma:
    1.50    includes magma G + magma H
    1.51 @@ -659,7 +645,7 @@
    1.52    with x show ?thesis by simp
    1.53  qed
    1.54  
    1.55 -section {* Commutative Structures *}
    1.56 +subsection {* Commutative Structures *}
    1.57  
    1.58  text {*
    1.59    Naming convention: multiplicative structures that are commutative
     2.1 --- a/src/HOL/Algebra/Module.thy	Fri May 02 16:43:36 2003 +0200
     2.2 +++ b/src/HOL/Algebra/Module.thy	Fri May 02 20:02:50 2003 +0200
     2.3 @@ -139,7 +139,7 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 -subsection {* Every Abelian Group is a Z-module *}
     2.8 +subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
     2.9  
    2.10  text {* Not finished. *}
    2.11  
     3.1 --- a/src/HOL/Algebra/README.html	Fri May 02 16:43:36 2003 +0200
     3.2 +++ b/src/HOL/Algebra/README.html	Fri May 02 20:02:50 2003 +0200
     3.3 @@ -1,7 +1,61 @@
     3.4  <!-- $Id$ -->
     3.5  <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
     3.6  
     3.7 -<H2>Algebra: Theories of Rings and Polynomials</H2>
     3.8 +<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
     3.9 +
    3.10 +This directory presents proofs in classical algebra.  
    3.11 +
    3.12 +<H2>GroupTheory, including Sylow's Theorem</H2>
    3.13 +
    3.14 +<P>These proofs are mainly by Florian Kammüller.  (Later, Larry
    3.15 +Paulson simplified some of the proofs.)  These theories were indeed
    3.16 +the original motivation for locales.
    3.17 +
    3.18 +Here is an outline of the directory's contents: <UL> <LI>Theory <A
    3.19 +HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
    3.20 +groups, commutative monoids, commutative groups, homomorphisms and the
    3.21 +subgroup relation.  It also defines the product of two groups
    3.22 +(This theory was reimplemented by Clemens Ballarin).
    3.23 +
    3.24 +<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
    3.25 +commutative groups by a product operator for finite sets (provided by
    3.26 +Clemens Ballarin).
    3.27 +
    3.28 +<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
    3.29 +the factorization of a group and shows that the factorization a normal
    3.30 +subgroup is a group.
    3.31 +
    3.32 +<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
    3.33 +defines bijections over sets and operations on them and shows that they
    3.34 +are a group.  It shows that automorphisms form a group.
    3.35 +
    3.36 +<LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
    3.37 +	    combinatorial argument underlying Sylow's first theorem.
    3.38 +
    3.39 +<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
    3.40 +contains a proof of the first Sylow theorem.
    3.41 +</UL>
    3.42 +
    3.43 +<H2>Rings and Polynomials</H2>
    3.44 +
    3.45 +<UL><LI>Theory <A HREF="CRing.html"><CODE>CRing</CODE></A>
    3.46 +defines Abelian monoids and groups.  The difference to commutative
    3.47 +      structures is merely notational:  the binary operation is
    3.48 +      addition rather than multiplication.  Commutative rings are
    3.49 +      obtained by inheriting properties from Abelian groups and
    3.50 +      commutative monoids.  Further structures in the algebraic
    3.51 +      hierarchy of rings: integral domain.
    3.52 +
    3.53 +<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
    3.54 +introduces the notion of a R-left-module over an Abelian group, where
    3.55 +	R is a ring.
    3.56 +
    3.57 +<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
    3.58 +constructs univariate polynomials over rings and integral domains.
    3.59 +	  Degree function.  Universal Property.
    3.60 +</UL>
    3.61 +
    3.62 +<H2>Legacy Development of Rings using Axiomatic Type Classes</H2>
    3.63  
    3.64  <P>This development of univariate polynomials is separated into an
    3.65  abstract development of rings and the development of polynomials
    3.66 @@ -16,7 +70,6 @@
    3.67    following are available:
    3.68  
    3.69  <PRE>
    3.70 -  ringS:	Syntactic class
    3.71    ring:		Commutative rings with one (including a summation
    3.72  		operator, which is needed for the polynomials)
    3.73    domain:	Integral domains
    3.74 @@ -39,51 +92,15 @@
    3.75  <LI>Polynomials over an integral domain form an integral domain
    3.76  </MENU>
    3.77  
    3.78 - <P>Still missing are
    3.79 -    Polynomials over a factorial domain form a factorial domain
    3.80 -    (difficult), and polynomials over a field form a pid.
    3.81 -
    3.82  <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
    3.83  
    3.84  <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
    3.85 -  Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
    3.86 -
    3.87 -<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
    3.88 -
    3.89 -<P>This directory presents proofs about group theory, by
    3.90 -Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
    3.91 -These theories use locales and were indeed the original motivation for
    3.92 -locales.  However, this treatment of groups must still be regarded as
    3.93 -experimental.  We can expect to see refinements in the future.
    3.94 -
    3.95 -Here is an outline of the directory's contents:
    3.96 -
    3.97 -<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
    3.98 -semigroups, groups, homomorphisms and the subgroup relation.  It also defines
    3.99 -the product of two groups.  It defines the factorization of a group and shows
   3.100 -that the factorization a normal subgroup is a group.
   3.101 -
   3.102 -<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
   3.103 -defines bijections over sets and operations on them and shows that they
   3.104 -are a group.  It shows that automorphisms form a group.
   3.105 -
   3.106 -<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
   3.107 -a few basic theorems.  Ring automorphisms are shown to form a group.
   3.108 -
   3.109 -<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
   3.110 -contains a proof of the first Sylow theorem.
   3.111 -
   3.112 -<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
   3.113 -abelian groups by a summation operator for finite sets (provided by
   3.114 -Clemens Ballarin).
   3.115 -</UL>
   3.116 +  Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.
   3.117  
   3.118  <HR>
   3.119  <P>Last modified on $Date$
   3.120  
   3.121  <ADDRESS>
   3.122 -<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999
   3.123 -
   3.124 -<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
   3.125 +<P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
   3.126  </ADDRESS>
   3.127  </BODY></HTML>
     4.1 --- a/src/HOL/Algebra/ROOT.ML	Fri May 02 16:43:36 2003 +0200
     4.2 +++ b/src/HOL/Algebra/ROOT.ML	Fri May 02 20:02:50 2003 +0200
     4.3 @@ -4,15 +4,25 @@
     4.4      Author: Clemens Ballarin, started 24 September 1999
     4.5  *)
     4.6  
     4.7 -(* New development, based on explicit structures *)
     4.8 +(*** New development, based on explicit structures ***)
     4.9 +
    4.10 +(* Preliminaries from set and number theory *)
    4.11  
    4.12  no_document use_thy "FuncSet";
    4.13 -use_thy "Sylow";		(* Groups *)
    4.14 +no_document use_thy "Primes";
    4.15 +
    4.16 +(* Groups *)
    4.17 +
    4.18 +use_thy "FiniteProduct";	(* Product operator for commutative groups *)
    4.19 +use_thy "Sylow";		(* Sylow's theorem *)
    4.20  use_thy "Bij";			(* Automorphism Groups *)
    4.21 +
    4.22 +(* Rings *)
    4.23 +
    4.24  use_thy "UnivPoly";		(* Rings and polynomials *)
    4.25  
    4.26 -(* Old development, based on axiomatic type classes.
    4.27 -   Will be withdrawn in future. *)
    4.28 +(*** Old development, based on axiomatic type classes.
    4.29 +     Will be withdrawn in future. ***)
    4.30  
    4.31 -with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    4.32 -with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
    4.33 +with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
    4.34 +with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)
     5.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri May 02 16:43:36 2003 +0200
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri May 02 20:02:50 2003 +0200
     5.3 @@ -9,8 +9,7 @@
     5.4  
     5.5  section {* Univariate Polynomials *}
     5.6  
     5.7 -subsection
     5.8 -  {* Definition of the Constructor for Univariate Polynomials @{term UP} *}
     5.9 +subsection {* The Constructor for Univariate Polynomials *}
    5.10  
    5.11  (* Could alternatively use locale ...
    5.12  locale bound = cring + var bound +
    5.13 @@ -595,7 +594,7 @@
    5.14  lemmas (in UP_cring) UP_smult_r_minus =
    5.15    algebra.smult_r_minus [OF UP_algebra]
    5.16  
    5.17 -subsection {* Further Lemmas Involving @{term monom} *}
    5.18 +subsection {* Further lemmas involving monomials *}
    5.19  
    5.20  lemma (in UP_cring) monom_zero [simp]:
    5.21    "monom P \<zero> n = \<zero>\<^sub>2"
    5.22 @@ -767,7 +766,7 @@
    5.23    with R show "x = y" by simp
    5.24  qed
    5.25  
    5.26 -subsection {* The Degree Function *}
    5.27 +subsection {* The degree function *}
    5.28  
    5.29  constdefs
    5.30    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
    5.31 @@ -1060,7 +1059,7 @@
    5.32  Context.>> (fn thy => (simpset_ref_of thy :=
    5.33    simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    5.34  
    5.35 -subsection {* Polynomial over an Integral Domain are an Integral Domain *}
    5.36 +subsection {* Polynomials over an integral domain form an integral domain *}
    5.37  
    5.38  lemma domainI:
    5.39    assumes cring: "cring R"
    5.40 @@ -1134,13 +1133,13 @@
    5.41    by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
    5.42      inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
    5.43  
    5.44 -subsection {* Evaluation Homomorphism *}
    5.45 +subsection {* Evaluation Homomorphism and Universal Property*}
    5.46  
    5.47  ML_setup {*
    5.48  Context.>> (fn thy => (simpset_ref_of thy :=
    5.49    simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    5.50  
    5.51 -(* alternative congruence rule (more efficient)
    5.52 +(* alternative congruence rule (possibly more efficient)
    5.53  lemma (in abelian_monoid) finsum_cong2:
    5.54    "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
    5.55    !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
     6.1 --- a/src/HOL/IsaMakefile	Fri May 02 16:43:36 2003 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Fri May 02 20:02:50 2003 +0200
     6.3 @@ -7,12 +7,11 @@
     6.4  ## targets
     6.5  
     6.6  default: HOL
     6.7 -images: HOL HOL-Real HOL-Hyperreal TLA
     6.8 +images: HOL HOL-Algebra HOL-Real HOL-Hyperreal TLA
     6.9  
    6.10  #Note: keep targets sorted (except for HOL-Library)
    6.11  test: \
    6.12    HOL-Library \
    6.13 -  HOL-Algebra \
    6.14    HOL-Auth \
    6.15    HOL-AxClasses \
    6.16    HOL-Bali \
    6.17 @@ -340,6 +339,7 @@
    6.18  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
    6.19  
    6.20  $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
    6.21 +  Library/Primes.thy Library/FuncSet.thy \
    6.22    Algebra/Bij.thy \
    6.23    Algebra/CRing.thy \
    6.24    Algebra/Coset.thy \
    6.25 @@ -357,12 +357,13 @@
    6.26    Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
    6.27    Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
    6.28    Algebra/abstract/order.ML \
    6.29 +  Algebra/document/root.tex \
    6.30    Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
    6.31    Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
    6.32    Algebra/poly/Polynomial.thy \
    6.33    Algebra/poly/UnivPoly2.ML Algebra/poly/UnivPoly2.thy \
    6.34    Algebra/ringsimp.ML
    6.35 -	@$(ISATOOL) usedir $(OUT)/HOL Algebra
    6.36 +	@cd Algebra; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Algebra
    6.37  
    6.38  ## HOL-Auth
    6.39