revised the discussion of type classes
authorpaulson
Mon Jul 02 16:42:37 2007 +0200 (2007-07-02)
changeset 23525c7ded89c2de0
parent 23524 123a45589e0a
child 23526 936dc616a7fb
revised the discussion of type classes
doc-src/TutorialI/Types/numerics.tex
     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};
    1.35 +instead, theorems such as
    1.36 +\isa{diff_mult_distrib} are proved specifically about subtraction on
    1.37  type~\isa{nat}. All abstract properties involving division require a field.
    1.38  Obviously, all properties involving orderings required an ordered
    1.39  structure.