--- a/doc-src/AxClass/generated/Product.tex Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Sun May 21 21:48:39 2000 +0200
@@ -1,16 +1,77 @@
\begin{isabelle}%
-\isanewline
-\isanewline
-\isacommand{theory}~Product~=~Main:\isanewline
-\isanewline
+%
+\isamarkupheader{Syntactic classes}
+\isacommand{theory}~Product~=~Main:%
+\begin{isamarkuptext}%
+\medskip\noindent There is still a feature of Isabelle's type system
+ left that we have not yet used: when declaring polymorphic constants
+ $c :: \sigma$, the type variables occurring in $\sigma$ may be
+ constrained by type classes (or even general sorts) in an arbitrary
+ way. Note that by default, in Isabelle/HOL the declaration $\TIMES
+ :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for
+ $\TIMES :: (\alpha::term) \To \alpha \To \alpha$. Since class $term$
+ is the universal class of HOL, this is not really a restriction at
+ all.
+
+ The $product$ class below provides a less degenerate example of
+ syntactic type classes.%
+\end{isamarkuptext}%
\isacommand{axclass}\isanewline
~~product~<~{"}term{"}\isanewline
\isacommand{consts}\isanewline
-~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)\isanewline
-\isanewline
+~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)%
+\begin{isamarkuptext}%
+Here class $product$ is defined as subclass of $term$ without any
+ additional axioms. This effects in logical equivalence of $product$
+ and $term$, as is reflected by the trivial introduction rule
+ generated for this definition.
+
+ \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
+ product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
+ term) \To \alpha \To \alpha$ anyway? In this particular case where
+ $product \equiv term$, it should be obvious that both declarations
+ are the same from the logic's point of view. It even makes the most
+ sense to remove sort constraints from constant declarations, as far
+ as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+
+ On the other hand there are syntactic differences, of course.
+ Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
+ arity $\tau :: product$ is part of the type signature. In our
+ example, this arity may be always added when required by means of an
+ $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+
+ \medskip Thus, we may observe the following discipline of using
+ syntactic classes. Overloaded polymorphic constants have their type
+ arguments restricted to an associated (logically trivial) class $c$.
+ Only immediately before \emph{specifying} these constants on a
+ certain type $\tau$ do we instantiate $\tau :: c$.
+
+ This is done for class $product$ and type $bool$ as follows.%
+\end{isamarkuptext}%
\isacommand{instance}~bool~::~product\isanewline
~~\isacommand{by}~intro\_classes\isanewline
\isacommand{defs}\isanewline
-~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}\isanewline
-\isanewline
+~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
+\begin{isamarkuptext}%
+The definition $prod_bool_def$ becomes syntactically well-formed only
+ after the arity $bool :: product$ is made known to the type checker.
+
+ \medskip It is very important to see that above $\DEFS$ are not
+ directly connected with $\isarkeyword{instance}$ at all! We were
+ just following our convention to specify $\TIMES$ on $bool$ after
+ having instantiated $bool :: product$. Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
+
+ \medskip While Isabelle type classes and those of Haskell are almost
+ the same as far as type-checking and type inference are concerned,
+ there are major semantic differences. Haskell classes require their
+ instances to \emph{provide operations} of certain \emph{names}.
+ Therefore, its \texttt{instance} has a \texttt{where} part that tells
+ the system what these ``member functions'' should be.
+
+ This style of \texttt{instance} won't make much sense in Isabelle,
+ because its meta-logic has no corresponding notion of ``providing
+ operations'' or ``names''.%
+\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%