Logics/document/HOL.tex

120 function types, is overloaded with arity {\tt(term,\thinspace
176   Where function types are involved, Isabelle's unification code does not
456         & range of a function \\[1ex]
570 avoid complications involving function types in unification.  The isomorphisms
751 %definition, $f$ is the abstraction function and $A$ is the set of valid
864   \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
882 rules.  Reasoning about function composition (the operator~\sdx{o}) and the
955 {Chap.\ts\ref{chap:simplification}}), there is a special infix function
1150   \cdx{Suc}     & $nat \To nat$ & & successor function\\
1240 %define a higher-order function, we can easily Ackermann's function, which
1537 involving function spaces, we may also define infinitely branching datatypes, e.g.
1654 For a datatype with function types such as \texttt{'a tree}, the induction rule
1715 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
1717 Theory \texttt{NatArith} declares a generic function \texttt{size} of type
1800 \section{Old-style recursive function definitions}\label{sec:HOL:recursive}
1821 Here is a simple example, the Fibonacci function.  The first line declares
1833 With \texttt{recdef}, function definitions may be incomplete, and patterns may
1836 For missing patterns, the function is defined to return a default value.
1838 %For example, here is a declaration of the list function \cdx{hd}:
1844 %Because this function is not recursive, we may supply the empty well-founded
1847 The well-founded relation defines a notion of ``smaller'' for the function's
1851 If the function's argument has type~$\tau$, then $\prec$ has to be a relation
1865   Typically, $f$ takes the recursive function's arguments (as a tuple) and
1866   returns a result expressed in terms of the function \texttt{size}.  It is
1867   called a \textbf{measure function}.  Recall that \texttt{size} is overloaded
1887 common divisor.  The measure function, $\lambda(m,n). n$, specifies that the
1896 recdef {\it function} {\it rel}
1903 \item \textit{function} is the name of the function, either as an \textit{id}
1920   left-hand side must have the form $f\,t$, where $f$ is the function and $t$
1939 conditions afterwards.  The function \texttt{Tfl.tgoalw} is like the standard
1940 function \texttt{goalw}, which sets up a goal to prove, but its argument
1953 only be proved by complicated reasoning involving the recursive function
1956 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
1975 the recursive function.  For the \texttt{gcd} function above, the induction
1982 function.  It usually makes the induction hypothesis available at all
1999 of~$\alpha$.  This version states that for every function from $\alpha$ to