--- a/doc-src/AxClass/generated/Product.tex Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Tue Oct 03 18:55:23 2000 +0200
@@ -7,63 +7,66 @@
\begin{isamarkuptext}%
\medskip\noindent There is still a feature of Isabelle's type system
left that we have not yet discussed. When declaring polymorphic
- constants $c :: \sigma$, the type variables occurring in $\sigma$ may
- be constrained by type classes (or even general sorts) in an
+ constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
+ 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 constraint
- at all.
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the
+ universal class of HOL, this is not really a constraint at all.
- The $product$ class below provides a less degenerate example of
+ The \isa{product} class below provides a less degenerate example of
syntactic type classes.%
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
\ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
\isacommand{consts}\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
+\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
\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.
+Here class \isa{product} is defined as subclass of \isa{term}
+ without any additional axioms. This effects in logical equivalence
+ of \isa{product} and \isa{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}.
+ \medskip So what is the difference of declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway? In this particular case
+ where \isa{product\ {\isasymequiv}\ 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}$.
+ Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+ type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ 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$.
+ arguments restricted to an associated (logically trivial) class
+ \isa{c}. Only immediately before \emph{specifying} these constants
+ on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
- This is done for class $product$ and type $bool$ as follows.%
+ This is done for class \isa{product} and type \isa{bool} as
+ follows.%
\end{isamarkuptext}%
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\isanewline
\ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
\begin{isamarkuptext}%
-The definition $prod_bool_def$ becomes syntactically well-formed only
- after the arity $bool :: product$ is made known to the type checker.
+The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
+ well-formed only after the arity \isa{bool\ {\isasymColon}\ 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}.
+ just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
+ after having instantiated \isa{bool\ {\isasymColon}\ 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,
@@ -72,9 +75,9 @@
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's
- meta-logic, because there is no internal notion of ``providing
- operations'' or even ``names of functions''.%
+ This style of \texttt{instance} would not make much sense in
+ Isabelle's meta-logic, because there is no internal notion of
+ ``providing operations'' or even ``names of functions''.%
\end{isamarkuptext}%
\isacommand{end}\end{isabellebody}%
%%% Local Variables: