1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Overloading}% |
3 \def\isabellecontext{Overloading}% |
|
4 \isamarkupfalse% |
4 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline |
5 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline |
5 \isacommand{by}\ intro{\isacharunderscore}classes% |
6 \isamarkupfalse% |
|
7 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
|
8 % |
6 \begin{isamarkuptext}% |
9 \begin{isamarkuptext}% |
7 \noindent |
10 \noindent |
8 This \isacommand{instance} declaration can be read like the declaration of |
11 This \isacommand{instance} declaration can be read like the declaration of |
9 a function on types. The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel}; |
12 a function on types. The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel}; |
10 in other words, |
13 in other words, |
11 if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
14 if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
12 Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
15 Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
13 \isa{{\isacharless}{\isacharless}} on lists:% |
16 \isa{{\isacharless}{\isacharless}} on lists:% |
14 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
|
18 \isamarkuptrue% |
15 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
19 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
16 prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
20 prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
17 \ \ {\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 |
21 \ \ {\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 |
18 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
22 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
19 \ \ {\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}\end{isabellebody}% |
23 \ \ {\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}\isamarkupfalse% |
|
24 \isamarkupfalse% |
|
25 \end{isabellebody}% |
20 %%% Local Variables: |
26 %%% Local Variables: |
21 %%% mode: latex |
27 %%% mode: latex |
22 %%% TeX-master: "root" |
28 %%% TeX-master: "root" |
23 %%% End: |
29 %%% End: |