10305
|
1 |
(*<*)theory Overloading2 = Overloading1:(*>*)
|
|
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
|
|
18 |
The infix function @{text"!"} yields the nth element of a list.
|
10396
|
19 |
*}
|
|
20 |
|
|
21 |
subsubsection{*Predefined overloading*}
|
|
22 |
|
|
23 |
text{*
|
|
24 |
HOL comes with a number of overloaded constants and corresponding classes.
|
|
25 |
The most important ones are listed in Table~\ref{tab:overloading}. They are
|
|
26 |
defined on all numeric types and somtimes on other types as well, for example
|
|
27 |
@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
|
|
28 |
|
|
29 |
\begin{table}[htbp]
|
|
30 |
\begin{center}
|
|
31 |
\begin{tabular}{lll}
|
|
32 |
Constant & Type & Syntax \\
|
|
33 |
\hline
|
|
34 |
@{term 0} & @{text "'a::zero"} \\
|
|
35 |
@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
|
|
36 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
|
|
37 |
@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
|
|
38 |
@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
|
|
39 |
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
|
10761
|
40 |
@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
|
10396
|
41 |
@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
|
|
42 |
@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
|
|
43 |
@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
|
10761
|
44 |
@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
|
|
45 |
@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
|
|
46 |
@{text LEAST}$~x.~P$
|
10396
|
47 |
\end{tabular}
|
|
48 |
\caption{Overloaded constants in HOL}
|
|
49 |
\label{tab:overloading}
|
|
50 |
\end{center}
|
|
51 |
\end{table}
|
10696
|
52 |
|
|
53 |
In addition there is a special input syntax for bounded quantifiers:
|
|
54 |
\begin{center}
|
|
55 |
\begin{tabular}{lcl}
|
|
56 |
@{text"\<forall>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\
|
|
57 |
@{text"\<exists>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<exists>x. x \<le> y \<and> P x"}
|
|
58 |
\end{tabular}
|
|
59 |
\end{center}
|
|
60 |
And analogously for @{text"<"} instead of @{text"\<le>"}.
|
|
61 |
The form on the left is translated into the one on the right upon input but it is not
|
|
62 |
translated back upon output.
|
10328
|
63 |
*}(*<*)end(*>*)
|