doc-src/TutorialI/Types/document/Overloading2.tex

removed vars_of, concls_of;
removed additional rule instantiation argument;
proper enumeration of type rules;
append possibilities of set and type rules (analogous to elim-intro in 'rule');

%
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{2}}}%
%
\begin{isamarkuptext}%
Of course this is not the only possible definition of the two relations.
Componentwise comparison of lists of equal length also makes sense. This time
the elements of the list must also be of class \isa{ordrel} to permit their
comparison:%
\end{isamarkuptext}%
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
\isanewline
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
The infix function \isa{{\isacharbang}} yields the nth element of a list.

\begin{warn}
A type constructor can be instantiated in only one way to
a given type class.  For example, our two instantiations of \isa{list} must
reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
\end{warn}%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Predefined Overloading%
}
%
\begin{isamarkuptext}%
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
$-$ and \isa{{\isasymle}} on sets.

In addition there is a special input syntax for bounded quantifiers:
\begin{center}
\begin{tabular}{lcl}
\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
\end{tabular}
\end{center}
And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
The form on the left is translated into the one on the right upon input.
For technical reasons, it is not translated back upon output.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: