10305
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Overloading{\isadigit{2}}}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
10305
|
17 |
%
|
|
18 |
\begin{isamarkuptext}%
|
|
19 |
Of course this is not the only possible definition of the two relations.
|
10328
|
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
|
|
22 |
comparison:%
|
10305
|
23 |
\end{isamarkuptext}%
|
17175
|
24 |
\isamarkuptrue%
|
|
25 |
\isacommand{instance}\isamarkupfalse%
|
|
26 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
|
17056
|
27 |
%
|
|
28 |
\isadelimproof
|
|
29 |
%
|
|
30 |
\endisadelimproof
|
|
31 |
%
|
|
32 |
\isatagproof
|
17175
|
33 |
\isacommand{by}\isamarkupfalse%
|
|
34 |
\ intro{\isacharunderscore}classes%
|
17056
|
35 |
\endisatagproof
|
|
36 |
{\isafoldproof}%
|
|
37 |
%
|
|
38 |
\isadelimproof
|
|
39 |
\isanewline
|
|
40 |
%
|
|
41 |
\endisadelimproof
|
15481
|
42 |
\isanewline
|
17175
|
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}%
|
10305
|
47 |
\begin{isamarkuptext}%
|
10328
|
48 |
\noindent
|
11494
|
49 |
The infix function \isa{{\isacharbang}} yields the nth element of a list.
|
|
50 |
|
|
51 |
\begin{warn}
|
|
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
|
12334
|
54 |
reside in separate theories with disjoint scopes.
|
11494
|
55 |
\end{warn}%
|
10396
|
56 |
\end{isamarkuptext}%
|
11866
|
57 |
\isamarkuptrue%
|
10396
|
58 |
%
|
10878
|
59 |
\isamarkupsubsubsection{Predefined Overloading%
|
10397
|
60 |
}
|
11866
|
61 |
\isamarkuptrue%
|
10396
|
62 |
%
|
|
63 |
\begin{isamarkuptext}%
|
|
64 |
HOL comes with a number of overloaded constants and corresponding classes.
|
10978
|
65 |
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
|
10971
|
66 |
defined on all numeric types and sometimes on other types as well, for example
|
11494
|
67 |
$-$ and \isa{{\isasymle}} on sets.
|
10396
|
68 |
|
14379
|
69 |
In addition there is a special syntax for bounded quantifiers:
|
10696
|
70 |
\begin{center}
|
|
71 |
\begin{tabular}{lcl}
|
19654
|
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}}
|
10696
|
74 |
\end{tabular}
|
|
75 |
\end{center}
|
14379
|
76 |
And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
|
10305
|
77 |
\end{isamarkuptext}%
|
17175
|
78 |
\isamarkuptrue%
|
17056
|
79 |
%
|
|
80 |
\isadelimtheory
|
|
81 |
%
|
|
82 |
\endisadelimtheory
|
|
83 |
%
|
|
84 |
\isatagtheory
|
|
85 |
%
|
|
86 |
\endisatagtheory
|
|
87 |
{\isafoldtheory}%
|
|
88 |
%
|
|
89 |
\isadelimtheory
|
|
90 |
%
|
|
91 |
\endisadelimtheory
|
10305
|
92 |
\end{isabellebody}%
|
|
93 |
%%% Local Variables:
|
|
94 |
%%% mode: latex
|
|
95 |
%%% TeX-master: "root"
|
|
96 |
%%% End:
|