author | nipkow |
Wed, 24 Jan 2001 12:29:10 +0100 | |
changeset 10971 | 6852682eaf16 |
parent 10885 | 90695f46440b |
child 10978 | 5eebea8f359f |
permissions | -rw-r--r-- |
nipkow@10305 | 1 |
(*<*)theory Overloading2 = Overloading1:(*>*) |
nipkow@10305 | 2 |
|
nipkow@10305 | 3 |
text{* |
nipkow@10305 | 4 |
Of course this is not the only possible definition of the two relations. |
nipkow@10328 | 5 |
Componentwise comparison of lists of equal length also makes sense. This time |
nipkow@10328 | 6 |
the elements of the list must also be of class @{text ordrel} to permit their |
nipkow@10328 | 7 |
comparison: |
nipkow@10305 | 8 |
*} |
nipkow@10305 | 9 |
|
nipkow@10305 | 10 |
instance list :: (ordrel)ordrel |
nipkow@10305 | 11 |
by intro_classes |
nipkow@10305 | 12 |
|
nipkow@10305 | 13 |
defs (overloaded) |
nipkow@10305 | 14 |
le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
nipkow@10305 | 15 |
size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
nipkow@10305 | 16 |
|
nipkow@10328 | 17 |
text{*\noindent |
nipkow@10328 | 18 |
The infix function @{text"!"} yields the nth element of a list. |
nipkow@10396 | 19 |
*} |
nipkow@10396 | 20 |
|
paulson@10885 | 21 |
subsubsection{*Predefined Overloading*} |
nipkow@10396 | 22 |
|
nipkow@10396 | 23 |
text{* |
nipkow@10396 | 24 |
HOL comes with a number of overloaded constants and corresponding classes. |
nipkow@10396 | 25 |
The most important ones are listed in Table~\ref{tab:overloading}. They are |
nipkow@10971 | 26 |
defined on all numeric types and sometimes on other types as well, for example |
nipkow@10396 | 27 |
@{text"-"}, @{text"\<le>"} and @{text"<"} on sets. |
nipkow@10396 | 28 |
|
nipkow@10396 | 29 |
\begin{table}[htbp] |
nipkow@10396 | 30 |
\begin{center} |
nipkow@10396 | 31 |
\begin{tabular}{lll} |
nipkow@10396 | 32 |
Constant & Type & Syntax \\ |
nipkow@10396 | 33 |
\hline |
nipkow@10396 | 34 |
@{term 0} & @{text "'a::zero"} \\ |
nipkow@10396 | 35 |
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
nipkow@10396 | 36 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\ |
nipkow@10971 | 37 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\ |
nipkow@10396 | 38 |
@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
nipkow@10971 | 39 |
@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
nipkow@10971 | 40 |
@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
nipkow@10971 | 41 |
@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
nipkow@10971 | 42 |
@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
nipkow@10396 | 43 |
@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\ |
nipkow@10761 | 44 |
@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\ |
nipkow@10396 | 45 |
@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
nipkow@10396 | 46 |
@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
nipkow@10396 | 47 |
@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
nipkow@10761 | 48 |
@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
nipkow@10761 | 49 |
@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} & |
nipkow@10761 | 50 |
@{text LEAST}$~x.~P$ |
nipkow@10396 | 51 |
\end{tabular} |
paulson@10885 | 52 |
\caption{Overloaded Constants in HOL} |
nipkow@10396 | 53 |
\label{tab:overloading} |
nipkow@10396 | 54 |
\end{center} |
nipkow@10396 | 55 |
\end{table} |
nipkow@10696 | 56 |
|
nipkow@10696 | 57 |
In addition there is a special input syntax for bounded quantifiers: |
nipkow@10696 | 58 |
\begin{center} |
nipkow@10696 | 59 |
\begin{tabular}{lcl} |
nipkow@10696 | 60 |
@{text"\<forall>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |
nipkow@10696 | 61 |
@{text"\<exists>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<exists>x. x \<le> y \<and> P x"} |
nipkow@10696 | 62 |
\end{tabular} |
nipkow@10696 | 63 |
\end{center} |
nipkow@10696 | 64 |
And analogously for @{text"<"} instead of @{text"\<le>"}. |
nipkow@10696 | 65 |
The form on the left is translated into the one on the right upon input but it is not |
nipkow@10696 | 66 |
translated back upon output. |
nipkow@10328 | 67 |
*}(*<*)end(*>*) |