3 \def\isabellecontext{Overloading{\isadigit{2}}}%
6 Of course this is not the only possible definition of the two relations.
7 Componentwise comparison of lists of equal length also makes sense. This time
8 the elements of the list must also be of class \isa{ordrel} to permit their
11 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
12 \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
14 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
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
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}%
17 \begin{isamarkuptext}%
19 The infix function \isa{{\isacharbang}} yields the nth element of a list.%
22 \isamarkupsubsubsection{Predefined Overloading%
25 \begin{isamarkuptext}%
26 HOL comes with a number of overloaded constants and corresponding classes.
27 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
28 defined on all numeric types and sometimes on other types as well, for example
29 \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
31 In addition there is a special input syntax for bounded quantifiers:
34 \isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
35 \isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
38 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
39 The form on the left is translated into the one on the right upon input.
40 For technical reasons, it is not translated back upon output.%
45 %%% TeX-master: "root"