|
nipkow@10305
|
1 |
%
|
|
nipkow@10305
|
2 |
\begin{isabellebody}%
|
|
nipkow@10305
|
3 |
\def\isabellecontext{Overloading{\isadigit{2}}}%
|
|
nipkow@10305
|
4 |
%
|
|
nipkow@10305
|
5 |
\begin{isamarkuptext}%
|
|
nipkow@10305
|
6 |
Of course this is not the only possible definition of the two relations.
|
|
nipkow@10305
|
7 |
Componentwise%
|
|
nipkow@10305
|
8 |
\end{isamarkuptext}%
|
|
nipkow@10305
|
9 |
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
|
|
nipkow@10305
|
10 |
\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
|
|
nipkow@10305
|
11 |
\isanewline
|
|
nipkow@10305
|
12 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
|
|
nipkow@10305
|
13 |
le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
|
|
nipkow@10305
|
14 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
|
|
nipkow@10305
|
15 |
\begin{isamarkuptext}%
|
|
nipkow@10305
|
16 |
%However, we retract the componetwise comparison of lists and return
|
|
nipkow@10305
|
17 |
|
|
nipkow@10305
|
18 |
Note: only one definition because based on name.%
|
|
nipkow@10305
|
19 |
\end{isamarkuptext}%
|
|
nipkow@10305
|
20 |
\isanewline
|
|
nipkow@10305
|
21 |
\end{isabellebody}%
|
|
nipkow@10305
|
22 |
%%% Local Variables:
|
|
nipkow@10305
|
23 |
%%% mode: latex
|
|
nipkow@10305
|
24 |
%%% TeX-master: "root"
|
|
nipkow@10305
|
25 |
%%% End:
|