20 |
20 |
21 subsubsection{*Predefined Overloading*} |
21 subsubsection{*Predefined Overloading*} |
22 |
22 |
23 text{* |
23 text{* |
24 HOL comes with a number of overloaded constants and corresponding classes. |
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 |
25 The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are |
26 defined on all numeric types and sometimes on other types as well, for example |
26 defined on all numeric types and sometimes on other types as well, for example |
27 @{text"-"}, @{text"\<le>"} and @{text"<"} on sets. |
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::minus) \<Rightarrow> 'a"} \\ |
|
38 @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
|
39 @{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
|
40 @{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
|
41 @{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
|
42 @{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\ |
|
43 @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\ |
|
44 @{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\ |
|
45 @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
|
46 @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\ |
|
47 @{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
|
48 @{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\ |
|
49 @{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} & |
|
50 @{text LEAST}$~x.~P$ |
|
51 \end{tabular} |
|
52 \caption{Overloaded Constants in HOL} |
|
53 \label{tab:overloading} |
|
54 \end{center} |
|
55 \end{table} |
|
56 |
28 |
57 In addition there is a special input syntax for bounded quantifiers: |
29 In addition there is a special input syntax for bounded quantifiers: |
58 \begin{center} |
30 \begin{center} |
59 \begin{tabular}{lcl} |
31 \begin{tabular}{lcl} |
60 @{text"\<forall>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |
32 @{text"\<forall>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\ |