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}; 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.