nipkow@10305
|
1 |
%
|
nipkow@10305
|
2 |
\begin{isabellebody}%
|
nipkow@10305
|
3 |
\def\isabellecontext{Overloading{\isadigit{2}}}%
|
nipkow@10305
|
4 |
%
|
nipkow@10305
|
5 |
\begin{isamarkuptext}%
|
nipkow@10305
|
6 |
Of course this is not the only possible definition of the two relations.
|
nipkow@10328
|
7 |
Componentwise comparison of lists of equal length also makes sense. This time
|
nipkow@10328
|
8 |
the elements of the list must also be of class \isa{ordrel} to permit their
|
nipkow@10328
|
9 |
comparison:%
|
nipkow@10305
|
10 |
\end{isamarkuptext}%
|
nipkow@10305
|
11 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
|
nipkow@10305
|
12 |
\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
|
nipkow@10305
|
13 |
\isanewline
|
nipkow@10305
|
14 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
nipkow@10305
|
15 |
le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
|
nipkow@10305
|
16 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
|
nipkow@10305
|
17 |
\begin{isamarkuptext}%
|
nipkow@10328
|
18 |
\noindent
|
nipkow@10396
|
19 |
The infix function \isa{{\isacharbang}} yields the nth element of a list.%
|
nipkow@10396
|
20 |
\end{isamarkuptext}%
|
nipkow@10396
|
21 |
%
|
paulson@10397
|
22 |
\isamarkupsubsubsection{Predefined overloading%
|
paulson@10397
|
23 |
}
|
nipkow@10396
|
24 |
%
|
nipkow@10396
|
25 |
\begin{isamarkuptext}%
|
nipkow@10396
|
26 |
HOL comes with a number of overloaded constants and corresponding classes.
|
nipkow@10396
|
27 |
The most important ones are listed in Table~\ref{tab:overloading}. They are
|
nipkow@10396
|
28 |
defined on all numeric types and somtimes on other types as well, for example
|
nipkow@10396
|
29 |
\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
|
nipkow@10396
|
30 |
|
nipkow@10396
|
31 |
\begin{table}[htbp]
|
nipkow@10396
|
32 |
\begin{center}
|
nipkow@10396
|
33 |
\begin{tabular}{lll}
|
nipkow@10396
|
34 |
Constant & Type & Syntax \\
|
nipkow@10396
|
35 |
\hline
|
nipkow@10396
|
36 |
\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
|
nipkow@10396
|
37 |
\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
|
nipkow@10396
|
38 |
\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
|
nipkow@10396
|
39 |
\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
|
nipkow@10396
|
40 |
\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
|
nipkow@10396
|
41 |
\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
|
nipkow@10761
|
42 |
\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
|
nipkow@10396
|
43 |
\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
|
nipkow@10396
|
44 |
\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
|
nipkow@10396
|
45 |
\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
|
nipkow@10761
|
46 |
\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
|
nipkow@10761
|
47 |
\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
|
nipkow@10761
|
48 |
\isa{LEAST}$~x.~P$
|
nipkow@10396
|
49 |
\end{tabular}
|
nipkow@10396
|
50 |
\caption{Overloaded constants in HOL}
|
nipkow@10396
|
51 |
\label{tab:overloading}
|
nipkow@10396
|
52 |
\end{center}
|
nipkow@10696
|
53 |
\end{table}
|
nipkow@10696
|
54 |
|
nipkow@10696
|
55 |
In addition there is a special input syntax for bounded quantifiers:
|
nipkow@10696
|
56 |
\begin{center}
|
nipkow@10696
|
57 |
\begin{tabular}{lcl}
|
nipkow@10696
|
58 |
\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
|
nipkow@10696
|
59 |
\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
|
nipkow@10696
|
60 |
\end{tabular}
|
nipkow@10696
|
61 |
\end{center}
|
nipkow@10696
|
62 |
And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
|
nipkow@10696
|
63 |
The form on the left is translated into the one on the right upon input but it is not
|
nipkow@10696
|
64 |
translated back upon output.%
|
nipkow@10305
|
65 |
\end{isamarkuptext}%
|
nipkow@10305
|
66 |
\end{isabellebody}%
|
nipkow@10305
|
67 |
%%% Local Variables:
|
nipkow@10305
|
68 |
%%% mode: latex
|
nipkow@10305
|
69 |
%%% TeX-master: "root"
|
nipkow@10305
|
70 |
%%% End:
|