author | wenzelm |
Sun, 21 Oct 2001 19:49:29 +0200 | |
changeset 11866 | fbd097aec213 |
parent 11494 | 23a118849801 |
child 12334 | 60bf75e157e4 |
permissions | -rw-r--r-- |
nipkow@10305 | 1 |
% |
nipkow@10305 | 2 |
\begin{isabellebody}% |
nipkow@10305 | 3 |
\def\isabellecontext{Overloading{\isadigit{2}}}% |
wenzelm@11866 | 4 |
\isamarkupfalse% |
nipkow@10305 | 5 |
% |
nipkow@10305 | 6 |
\begin{isamarkuptext}% |
nipkow@10305 | 7 |
Of course this is not the only possible definition of the two relations. |
nipkow@10328 | 8 |
Componentwise comparison of lists of equal length also makes sense. This time |
nipkow@10328 | 9 |
the elements of the list must also be of class \isa{ordrel} to permit their |
nipkow@10328 | 10 |
comparison:% |
nipkow@10305 | 11 |
\end{isamarkuptext}% |
wenzelm@11866 | 12 |
\isamarkuptrue% |
nipkow@10305 | 13 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline |
wenzelm@11866 | 14 |
\isamarkupfalse% |
nipkow@10305 | 15 |
\isacommand{by}\ intro{\isacharunderscore}classes\isanewline |
nipkow@10305 | 16 |
\isanewline |
wenzelm@11866 | 17 |
\isamarkupfalse% |
nipkow@10305 | 18 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
nipkow@10305 | 19 |
le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline |
wenzelm@11866 | 20 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
wenzelm@11866 | 21 |
% |
nipkow@10305 | 22 |
\begin{isamarkuptext}% |
nipkow@10328 | 23 |
\noindent |
paulson@11494 | 24 |
The infix function \isa{{\isacharbang}} yields the nth element of a list. |
paulson@11494 | 25 |
|
paulson@11494 | 26 |
\begin{warn} |
paulson@11494 | 27 |
A type constructor can be instantiated in only one way to |
paulson@11494 | 28 |
a given type class. For example, our two instantiations of \isa{list} must |
paulson@11494 | 29 |
reside in separate theories with disjoint scopes.\REMARK{Tobias, please check} |
paulson@11494 | 30 |
\end{warn}% |
nipkow@10396 | 31 |
\end{isamarkuptext}% |
wenzelm@11866 | 32 |
\isamarkuptrue% |
nipkow@10396 | 33 |
% |
paulson@10878 | 34 |
\isamarkupsubsubsection{Predefined Overloading% |
paulson@10397 | 35 |
} |
wenzelm@11866 | 36 |
\isamarkuptrue% |
nipkow@10396 | 37 |
% |
nipkow@10396 | 38 |
\begin{isamarkuptext}% |
nipkow@10396 | 39 |
HOL comes with a number of overloaded constants and corresponding classes. |
nipkow@10978 | 40 |
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
nipkow@10971 | 41 |
defined on all numeric types and sometimes on other types as well, for example |
paulson@11494 | 42 |
$-$ and \isa{{\isasymle}} on sets. |
nipkow@10396 | 43 |
|
nipkow@10696 | 44 |
In addition there is a special input syntax for bounded quantifiers: |
nipkow@10696 | 45 |
\begin{center} |
nipkow@10696 | 46 |
\begin{tabular}{lcl} |
nipkow@11196 | 47 |
\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\ |
nipkow@11196 | 48 |
\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x} |
nipkow@10696 | 49 |
\end{tabular} |
nipkow@10696 | 50 |
\end{center} |
nipkow@10696 | 51 |
And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}. |
nipkow@11277 | 52 |
The form on the left is translated into the one on the right upon input. |
nipkow@11277 | 53 |
For technical reasons, it is not translated back upon output.% |
nipkow@10305 | 54 |
\end{isamarkuptext}% |
wenzelm@11866 | 55 |
\isamarkuptrue% |
wenzelm@11866 | 56 |
\isamarkupfalse% |
nipkow@10305 | 57 |
\end{isabellebody}% |
nipkow@10305 | 58 |
%%% Local Variables: |
nipkow@10305 | 59 |
%%% mode: latex |
nipkow@10305 | 60 |
%%% TeX-master: "root" |
nipkow@10305 | 61 |
%%% End: |