author paulson Mon Jul 02 16:42:37 2007 +0200 (2007-07-02) changeset 23525 c7ded89c2de0 parent 23524 123a45589e0a child 23526 936dc616a7fb
revised the discussion of type classes
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Jul 02 10:43:20 2007 +0200
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Mon Jul 02 16:42:37 2007 +0200
1.3 @@ -385,13 +385,14 @@
1.4  Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
1.5  These lemmas are available (as simprules if they were declared as such)
1.6  for all numeric types satisfying the necessary axioms. The theory defines
1.7 -the following type classes:
1.8 +dozens of type classes, such as the following:
1.9  \begin{itemize}
1.10  \item
1.11  \tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
1.12 -provides the operators \isa{+} and~\isa{*}, which are commutative and
1.13 -associative, with the usual distributive law and with \isa{0} and~\isa{1}
1.14 -as their respective identities. An \emph{ordered semiring} is also linearly
1.15 +provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}
1.16 +as their respective identities. The operators enjoy the usual distributive law,
1.17 +and addition (\isa{+}) is also commutative.
1.18 +An \emph{ordered semiring} is also linearly
1.19  ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
1.20  \item
1.21  \tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
1.22 @@ -409,12 +410,12 @@
1.23  division by zero.
1.24  \end{itemize}
1.25
1.26 -Theory \thydx{Ring_and_Field} proves over 250 lemmas, each of which
1.27 +Hundreds of basic lemmas are proved, each of which
1.28  holds for all types in the corresponding type class. In most
1.29 -cases, it is obvious whether a property is valid for a particular type. All
1.30 -abstract properties involving subtraction require a ring, and therefore do
1.31 -not hold for type \isa{nat}, although we have theorems such as
1.32 -\isa{diff_mult_distrib} proved specifically about subtraction on
1.33 +cases, it is obvious whether a property is valid for a particular type. No
1.34 +abstract properties involving subtraction hold for type \isa{nat};