author | nipkow |
Sun, 22 Mar 2009 19:36:04 +0100 | |
changeset 30649 | 57753e0ec1d4 |
parent 19654 | 2c02a8054616 |
permissions | -rw-r--r-- |
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 |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
19654
diff
changeset
|
49 |
The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0. |
11494 | 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: |