10305
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Overloading}%
|
|
4 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
|
|
5 |
\isacommand{by}\ intro{\isacharunderscore}classes%
|
|
6 |
\begin{isamarkuptext}%
|
|
7 |
\noindent
|
|
8 |
This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
|
|
9 |
\isa{{\isacharless}{\isacharless}} on lists.%
|
|
10 |
\end{isamarkuptext}%
|
|
11 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
12 |
prefix{\isacharunderscore}def{\isacharcolon}\isanewline
|
|
13 |
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
|
|
14 |
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
|
|
15 |
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}%
|
|
16 |
\begin{isamarkuptext}%
|
|
17 |
We could also have made the second definition non-overloaded once and for
|
|
18 |
all: \isa{x\ {\isacharless}{\isacharless}\ y\ {\isasymequiv}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}. This would have saved us writing
|
|
19 |
many similar definitions at different types, but it would also have fixed
|
|
20 |
that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and never the other way
|
|
21 |
around. Below you will see why we want to avoid this asymmetry.%
|
|
22 |
\end{isamarkuptext}%
|
|
23 |
\end{isabellebody}%
|
|
24 |
%%% Local Variables:
|
|
25 |
%%% mode: latex
|
|
26 |
%%% TeX-master: "root"
|
|
27 |
%%% End:
|