wneuper/isa: doc-src/TutorialI/Types/document/Overloading2.tex@0d36ace55e5a

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Overloading{\isadigit{2}}}%

4 %

     5 \begin{isamarkuptext}%

     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

     9 comparison:%

    10 \end{isamarkuptext}%

    11 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline

    12 \isacommand{by}\ intro{\isacharunderscore}classes\isanewline

    13 \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}%

    18 \noindent

    19 The infix function \isa{{\isacharbang}} yields the nth element of a list.%

    20 \end{isamarkuptext}%

    21 %

    22 \isamarkupsubsubsection{Predefined overloading%

    23 }

    24 %

    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}. They are

    28 defined on all numeric types and somtimes on other types as well, for example

    29 \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.

    31 \begin{table}[htbp]

    32 \begin{center}

    33 \begin{tabular}{lll}

    34 Constant & Type & Syntax \\

    35 \hline

    36 \isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\

    37 \isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\

    38 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\

    39 \isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\

    40 \isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\

    41 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\

    42 \isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\

    43 \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\

    44 \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\

    45 \isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\

    46 \isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\

    47 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &

    48 \isa{LEAST}$~x.~P$

    49 \end{tabular}

    50 \caption{Overloaded constants in HOL}

    51 \label{tab:overloading}

    52 \end{center}

    53 \end{table}

    55 In addition there is a special input syntax for bounded quantifiers:

    56 \begin{center}

    57 \begin{tabular}{lcl}

    58 \isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\

    59 \isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}

    60 \end{tabular}

    61 \end{center}

    62 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.

    63 The form on the left is translated into the one on the right upon input but it is not

    64 translated back upon output.%

    65 \end{isamarkuptext}%

    66 \end{isabellebody}%

    67 %%% Local Variables:

    68 %%% mode: latex

    69 %%% TeX-master: "root"

    70 %%% End:

author	nipkow
	Tue, 02 Jan 2001 11:03:37 +0100
changeset 10761	0d36ace55e5a
parent 10696	76d7f6c9a14c
child 10878	b254d5ad6dd4
permissions	-rw-r--r--