3 \def\isabellecontext{Overloading{\isadigit{2}}}%
18 \begin{isamarkuptext}%
19 Of course this is not the only possible definition of the two relations.
20 Componentwise comparison of lists of equal length also makes sense. This time
21 the elements of the list must also be of class \isa{ordrel} to permit their
25 \isacommand{instance}\isamarkupfalse%
26 \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
33 \isacommand{by}\isamarkupfalse%
34 \ intro{\isacharunderscore}classes%
43 \isacommand{defs}\isamarkupfalse%
44 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
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
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}%
47 \begin{isamarkuptext}%
49 The infix function \isa{{\isacharbang}} yields the nth element of a list.
52 A type constructor can be instantiated in only one way to
53 a given type class. For example, our two instantiations of \isa{list} must
54 reside in separate theories with disjoint scopes.
59 \isamarkupsubsubsection{Predefined Overloading%
63 \begin{isamarkuptext}%
64 HOL comes with a number of overloaded constants and corresponding classes.
65 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
66 defined on all numeric types and sometimes on other types as well, for example
67 $-$ and \isa{{\isasymle}} on sets.
69 In addition there is a special syntax for bounded quantifiers:
72 \isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
73 \isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
76 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
95 %%% TeX-master: "root"