doc-src/TutorialI/Types/Overloading2.thy
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10396 5ab08609e6c8
child 10696 76d7f6c9a14c
permissions -rw-r--r--
*** empty log message ***
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
nipkow@10396
    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@10396
    26
defined on all numeric types and somtimes 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@10396
    37
@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
nipkow@10396
    38
@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
nipkow@10396
    39
@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
nipkow@10654
    40
@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & $\mid~\mid$\\
nipkow@10396
    41
@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
nipkow@10396
    42
@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
nipkow@10396
    43
@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
nipkow@10654
    44
@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"}
nipkow@10396
    45
\end{tabular}
nipkow@10396
    46
\caption{Overloaded constants in HOL}
nipkow@10396
    47
\label{tab:overloading}
nipkow@10396
    48
\end{center}
nipkow@10396
    49
\end{table}
nipkow@10328
    50
*}(*<*)end(*>*)