doc-src/AxClass/Group/document/Product.tex

change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems

%
\begin{isabellebody}%
\def\isabellecontext{Product}%
%
\isamarkupheader{Syntactic classes%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\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 \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 \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
  universal class of HOL, this is not really a constraint at all.

 The \isa{product} class below provides a less degenerate example of
 syntactic type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{axclass}\isamarkupfalse%
\isanewline
\ \ product\ {\isasymsubseteq}\ type\isanewline
\isacommand{consts}\isamarkupfalse%
\isanewline
\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
Here class \isa{product} is defined as subclass of \isa{type}
  without any additional axioms.  This effects in logical equivalence
  of \isa{product} and \isa{type}, as is reflected by the trivial
  introduction rule generated for this definition.

  \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}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case where \isa{product\ {\isasymequiv}\ type}, 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 \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 $\INSTANCE$ with the default proof $\DDOT$.

  \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
  \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 \isa{product} and type \isa{bool} as
  follows.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
\ bool\ {\isacharcolon}{\isacharcolon}\ product%
\isadelimproof
\ %
\endisadelimproof
%
\isatagproof
\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isanewline
\isacommand{defs}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}%
\begin{isamarkuptext}%
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 $\INSTANCE$ at all!  We were 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,
 there are important 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} 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}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: