3 \def\isabellecontext{Overloading{\isadigit{2}}}%
7 Of course this is not the only possible definition of the two relations.
8 Componentwise comparison of lists of equal length also makes sense. This time
9 the elements of the list must also be of class \isa{ordrel} to permit their
13 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
15 \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
18 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
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
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%
22 \begin{isamarkuptext}%
24 The infix function \isa{{\isacharbang}} yields the nth element of a list.
27 A type constructor can be instantiated in only one way to
28 a given type class. For example, our two instantiations of \isa{list} must
29 reside in separate theories with disjoint scopes.
34 \isamarkupsubsubsection{Predefined Overloading%
38 \begin{isamarkuptext}%
39 HOL comes with a number of overloaded constants and corresponding classes.
40 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
41 defined on all numeric types and sometimes on other types as well, for example
42 $-$ and \isa{{\isasymle}} on sets.
44 In addition there is a special syntax for bounded quantifiers:
47 \isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
48 \isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
51 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
58 %%% TeX-master: "root"