author | wenzelm |
Mon, 29 Aug 2005 16:25:24 +0200 | |
changeset 17187 | 45bee2f6e61f |
parent 17181 | 5f42dd5e6570 |
child 27169 | 89d5f117add3 |
permissions | -rw-r--r-- |
10305 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Overloading}% |
|
17056 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
% |
|
11 |
\endisatagtheory |
|
12 |
{\isafoldtheory}% |
|
13 |
% |
|
14 |
\isadelimtheory |
|
15 |
% |
|
16 |
\endisadelimtheory |
|
17175 | 17 |
\isacommand{instance}\isamarkupfalse% |
18 |
\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline |
|
17056 | 19 |
% |
20 |
\isadelimproof |
|
21 |
% |
|
22 |
\endisadelimproof |
|
23 |
% |
|
24 |
\isatagproof |
|
17175 | 25 |
\isacommand{by}\isamarkupfalse% |
26 |
\ intro{\isacharunderscore}classes% |
|
17056 | 27 |
\endisatagproof |
28 |
{\isafoldproof}% |
|
29 |
% |
|
30 |
\isadelimproof |
|
31 |
% |
|
32 |
\endisadelimproof |
|
11866 | 33 |
% |
10305 | 34 |
\begin{isamarkuptext}% |
35 |
\noindent |
|
10328 | 36 |
This \isacommand{instance} declaration can be read like the declaration of |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
37 |
a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel}; |
11494 | 38 |
in other words, |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11866
diff
changeset
|
39 |
if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. |
10328 | 40 |
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
41 |
\isa{{\isacharless}{\isacharless}} on lists:% |
|
10305 | 42 |
\end{isamarkuptext}% |
17175 | 43 |
\isamarkuptrue% |
44 |
\isacommand{defs}\isamarkupfalse% |
|
45 |
\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
10305 | 46 |
prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
17175 | 47 |
\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequoteclose}\isanewline |
10305 | 48 |
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
17175 | 49 |
\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}% |
17056 | 50 |
\isadelimtheory |
51 |
% |
|
52 |
\endisadelimtheory |
|
53 |
% |
|
54 |
\isatagtheory |
|
55 |
% |
|
56 |
\endisatagtheory |
|
57 |
{\isafoldtheory}% |
|
58 |
% |
|
59 |
\isadelimtheory |
|
60 |
% |
|
61 |
\endisadelimtheory |
|
11866 | 62 |
\end{isabellebody}% |
10305 | 63 |
%%% Local Variables: |
64 |
%%% mode: latex |
|
65 |
%%% TeX-master: "root" |
|
66 |
%%% End: |