author | nipkow |
Sun, 22 Mar 2009 19:36:04 +0100 | |
changeset 30649 | 57753e0ec1d4 |
parent 17914 | 99ead7a7eb42 |
permissions | -rw-r--r-- |
17914 | 1 |
(*<*)theory Overloading2 imports Overloading1 begin(*>*) |
10305 | 2 |
|
3 |
text{* |
|
4 |
Of course this is not the only possible definition of the two relations. |
|
10328 | 5 |
Componentwise comparison of lists of equal length also makes sense. This time |
6 |
the elements of the list must also be of class @{text ordrel} to permit their |
|
7 |
comparison: |
|
10305 | 8 |
*} |
9 |
||
10 |
instance list :: (ordrel)ordrel |
|
11 |
by intro_classes |
|
12 |
||
13 |
defs (overloaded) |
|
14 |
le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
|
15 |
size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
|
16 |
||
10328 | 17 |
text{*\noindent |
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
17914
diff
changeset
|
18 |
The infix function @{text"!"} yields the nth element of a list, starting with 0. |
11494 | 19 |
|
20 |
\begin{warn} |
|
21 |
A type constructor can be instantiated in only one way to |
|
12334 | 22 |
a given type class. For example, our two instantiations of @{text list} must |
23 |
reside in separate theories with disjoint scopes. |
|
11494 | 24 |
\end{warn} |
10396 | 25 |
*} |
26 |
||
10885 | 27 |
subsubsection{*Predefined Overloading*} |
10396 | 28 |
|
29 |
text{* |
|
30 |
HOL comes with a number of overloaded constants and corresponding classes. |
|
10978 | 31 |
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
10971 | 32 |
defined on all numeric types and sometimes on other types as well, for example |
11494 | 33 |
$-$ and @{text"\<le>"} on sets. |
10396 | 34 |
|
14357 | 35 |
In addition there is a special syntax for bounded quantifiers: |
10696 | 36 |
\begin{center} |
37 |
\begin{tabular}{lcl} |
|
14357 | 38 |
@{prop"\<forall>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |
39 |
@{prop"\<exists>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<exists>x. x \<le> y \<and> P x"} |
|
10696 | 40 |
\end{tabular} |
41 |
\end{center} |
|
42 |
And analogously for @{text"<"} instead of @{text"\<le>"}. |
|
10328 | 43 |
*}(*<*)end(*>*) |