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 ***
     1 (*<*)theory Overloading2 = Overloading1:(*>*)
     2 
     3 text{*
     4 Of course this is not the only possible definition of the two relations.
     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:
     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 
    17 text{*\noindent
    18 The infix function @{text"!"} yields the nth element of a list.
    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"} \\
    40 @{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} & $\mid~\mid$\\
    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"} \\
    44 @{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"}
    45 \end{tabular}
    46 \caption{Overloaded constants in HOL}
    47 \label{tab:overloading}
    48 \end{center}
    49 \end{table}
    50 *}(*<*)end(*>*)