| author | wenzelm |
| Tue, 16 May 2006 20:28:02 +0200 | |
| changeset 19654 | 2c02a8054616 |
| parent 19288 | 85b684d3fdbd |
| child 30637 | 57753e0ec1d4 |
| permissions | -rw-r--r-- |
| nipkow@10305 | 1 |
% |
| nipkow@10305 | 2 |
\begin{isabellebody}%
|
| nipkow@10305 | 3 |
\def\isabellecontext{Overloading{\isadigit{2}}}%
|
| wenzelm@17056 | 4 |
% |
| wenzelm@17056 | 5 |
\isadelimtheory |
| wenzelm@17056 | 6 |
% |
| wenzelm@17056 | 7 |
\endisadelimtheory |
| wenzelm@17056 | 8 |
% |
| wenzelm@17056 | 9 |
\isatagtheory |
| wenzelm@17056 | 10 |
% |
| wenzelm@17056 | 11 |
\endisatagtheory |
| wenzelm@17056 | 12 |
{\isafoldtheory}%
|
| wenzelm@17056 | 13 |
% |
| wenzelm@17056 | 14 |
\isadelimtheory |
| wenzelm@17056 | 15 |
% |
| wenzelm@17056 | 16 |
\endisadelimtheory |
| nipkow@10305 | 17 |
% |
| nipkow@10305 | 18 |
\begin{isamarkuptext}%
|
| nipkow@10305 | 19 |
Of course this is not the only possible definition of the two relations. |
| nipkow@10328 | 20 |
Componentwise comparison of lists of equal length also makes sense. This time |
| nipkow@10328 | 21 |
the elements of the list must also be of class \isa{ordrel} to permit their
|
| nipkow@10328 | 22 |
comparison:% |
| nipkow@10305 | 23 |
\end{isamarkuptext}%
|
| wenzelm@17175 | 24 |
\isamarkuptrue% |
| wenzelm@17175 | 25 |
\isacommand{instance}\isamarkupfalse%
|
| wenzelm@17175 | 26 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
|
| wenzelm@17056 | 27 |
% |
| wenzelm@17056 | 28 |
\isadelimproof |
| wenzelm@17056 | 29 |
% |
| wenzelm@17056 | 30 |
\endisadelimproof |
| wenzelm@17056 | 31 |
% |
| wenzelm@17056 | 32 |
\isatagproof |
| wenzelm@17175 | 33 |
\isacommand{by}\isamarkupfalse%
|
| wenzelm@17175 | 34 |
\ intro{\isacharunderscore}classes%
|
| wenzelm@17056 | 35 |
\endisatagproof |
| wenzelm@17056 | 36 |
{\isafoldproof}%
|
| wenzelm@17056 | 37 |
% |
| wenzelm@17056 | 38 |
\isadelimproof |
| wenzelm@17056 | 39 |
\isanewline |
| wenzelm@17056 | 40 |
% |
| wenzelm@17056 | 41 |
\endisadelimproof |
| paulson@15481 | 42 |
\isanewline |
| wenzelm@17175 | 43 |
\isacommand{defs}\isamarkupfalse%
|
| wenzelm@17175 | 44 |
\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
| wenzelm@17175 | 45 |
le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
|
| wenzelm@17175 | 46 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
|
| nipkow@10305 | 47 |
\begin{isamarkuptext}%
|
| nipkow@10328 | 48 |
\noindent |
| paulson@11494 | 49 |
The infix function \isa{{\isacharbang}} yields the nth element of a list.
|
| paulson@11494 | 50 |
|
| paulson@11494 | 51 |
\begin{warn}
|
| paulson@11494 | 52 |
A type constructor can be instantiated in only one way to |
| paulson@11494 | 53 |
a given type class. For example, our two instantiations of \isa{list} must
|
| nipkow@12334 | 54 |
reside in separate theories with disjoint scopes. |
| paulson@11494 | 55 |
\end{warn}%
|
| nipkow@10396 | 56 |
\end{isamarkuptext}%
|
| wenzelm@11866 | 57 |
\isamarkuptrue% |
| nipkow@10396 | 58 |
% |
| paulson@10878 | 59 |
\isamarkupsubsubsection{Predefined Overloading%
|
| paulson@10397 | 60 |
} |
| wenzelm@11866 | 61 |
\isamarkuptrue% |
| nipkow@10396 | 62 |
% |
| nipkow@10396 | 63 |
\begin{isamarkuptext}%
|
| nipkow@10396 | 64 |
HOL comes with a number of overloaded constants and corresponding classes. |
| nipkow@10978 | 65 |
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
|
| nipkow@10971 | 66 |
defined on all numeric types and sometimes on other types as well, for example |
| paulson@11494 | 67 |
$-$ and \isa{{\isasymle}} on sets.
|
| nipkow@10396 | 68 |
|
| paulson@14379 | 69 |
In addition there is a special syntax for bounded quantifiers: |
| nipkow@10696 | 70 |
\begin{center}
|
| nipkow@10696 | 71 |
\begin{tabular}{lcl}
|
| wenzelm@19654 | 72 |
\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
|
| wenzelm@19654 | 73 |
\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
|
| nipkow@10696 | 74 |
\end{tabular}
|
| nipkow@10696 | 75 |
\end{center}
|
| paulson@14379 | 76 |
And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
|
| nipkow@10305 | 77 |
\end{isamarkuptext}%
|
| wenzelm@17175 | 78 |
\isamarkuptrue% |
| wenzelm@17056 | 79 |
% |
| wenzelm@17056 | 80 |
\isadelimtheory |
| wenzelm@17056 | 81 |
% |
| wenzelm@17056 | 82 |
\endisadelimtheory |
| wenzelm@17056 | 83 |
% |
| wenzelm@17056 | 84 |
\isatagtheory |
| wenzelm@17056 | 85 |
% |
| wenzelm@17056 | 86 |
\endisatagtheory |
| wenzelm@17056 | 87 |
{\isafoldtheory}%
|
| wenzelm@17056 | 88 |
% |
| wenzelm@17056 | 89 |
\isadelimtheory |
| wenzelm@17056 | 90 |
% |
| wenzelm@17056 | 91 |
\endisadelimtheory |
| nipkow@10305 | 92 |
\end{isabellebody}%
|
| nipkow@10305 | 93 |
%%% Local Variables: |
| nipkow@10305 | 94 |
%%% mode: latex |
| nipkow@10305 | 95 |
%%% TeX-master: "root" |
| nipkow@10305 | 96 |
%%% End: |