%

\begin{isabellebody}%

\def\isabellecontext{Partial}%

\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent Throughout this tutorial, we have emphasized

that all functions in HOL are total.  We cannot hope to define

truly partial functions, but must make them total.  A straightforward

method is to lift the result type of the function from $\tau$ to

$\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is

returned if the function is applied to an argument not in its

domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example.

We do not pursue this schema further because it should be clear

how it works. Its main drawback is that the result of such a lifted

function has to be unpacked first before it can be processed

further. Its main advantage is that you can distinguish if the

function was applied to an argument in its domain or not. If you do

not need to make this distinction, for example because the function is

never used outside its domain, it is easier to work with

\emph{underdefined}\index{functions!underdefined} functions: for

certain arguments we only know that a result exists, but we do not

know what it is. When defining functions that are normally considered

partial, underdefinedness turns out to be a very reasonable

alternative.

We have already seen an instance of underdefinedness by means of

non-exhaustive pattern matching: the definition of \isa{last} in

\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{consts}\ hd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{primrec}\ {\isachardoublequote}hd\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent

although it generates a warning.

Even ordinary definitions allow underdefinedness, this time by means of

preconditions:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline

{\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

The rest of this section is devoted to the question of how to define

partial recursive functions by other means than non-exhaustive pattern

matching.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsubsection{Guarded Recursion%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\index{recursion!guarded}%

Neither \isacommand{primrec} nor \isacommand{recdef} allow to

prefix an equation with a condition in the way ordinary definitions do

(see \isa{minus} above). Instead we have to move the condition over

to the right-hand side of the equation. Given a partial function $f$

that should satisfy the recursion equation $f(x) = t$ over its domain

$dom(f)$, we turn this into the \isacommand{recdef}

\begin{isabelle}%

\ \ \ \ \ f\ x\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymin}\ dom\ f\ then\ t\ else\ arbitrary{\isacharparenright}%

\end{isabelle}

where \isa{arbitrary} is a predeclared constant of type \isa{{\isacharprime}a}

which has no definition. Thus we know nothing about its value,

which is ideal for specifying underdefined functions on top of it.

As a simple example we define division on \isa{nat}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline

\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ arbitrary{\isachardoublequote}\isanewline

\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent Of course we could also have defined

\isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The

latter option is chosen for the predefined \isa{div} function, which

simplifies proofs at the expense of deviating from the

standard mathematical division function.

As a more substantial example we consider the problem of searching a graph.

For simplicity our graph is given by a function \isa{f} of

type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which

maps each node to its successor; the graph has out-degree 1.

The task is to find the end of a chain, modelled by a node pointing to

itself. Here is a first attempt:

\begin{isabelle}%

\ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%

\end{isabelle}

This may be viewed as a fixed point finder or as the second half of the well

known \emph{Union-Find} algorithm.

The snag is that it may not terminate if \isa{f} has non-trivial cycles.

Phrased differently, the relation%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline

\ \ {\isachardoublequote}step{\isadigit{1}}\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymand}\ y\ {\isasymnoteq}\ x{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent

must be well-founded. Thus we make the following definition:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline

\ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline

{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent

The recursion equation itself should be clear enough: it is our aborted

first attempt augmented with a check that there are no non-trivial loops.

To express the required well-founded relation we employ the

predefined combinator \isa{same{\isacharunderscore}fst} of type

\begin{isabelle}%

\ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%

\end{isabelle}

defined as

\begin{isabelle}%

\ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%

\end{isabelle}

This combinator is designed for

recursive functions on pairs where the first component of the argument is

passed unchanged to all recursive calls. Given a constraint on the first

component and a relation on the second component, \isa{same{\isacharunderscore}fst} builds the

required relation on pairs.  The theorem

\begin{isabelle}%

\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%

\end{isabelle}

is known to the well-foundedness prover of \isacommand{recdef}.  Thus

well-foundedness of the relation given to \isacommand{recdef} is immediate.

Furthermore, each recursive call descends along that relation: the first

argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}},

as specified in the \isacommand{hints} above.

Normally you will then derive the following conditional variant from

the recursion equation:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{by}\ simp\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent Then you should disable the original recursion equation:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}\isamarkupfalse%

%

\begin{isamarkuptext}%

Reasoning about such underdefined functions is like that for other

recursive functions.  Here is a simple example of recursion induction:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{apply}\ simp\isanewline

\isamarkupfalse%

\isacommand{done}\isamarkupfalse%

%

\isamarkupsubsubsection{The {\tt\slshape while} Combinator%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

If the recursive function happens to be tail recursive, its

definition becomes a triviality if based on the predefined \cdx{while}

combinator.  The latter lives in the Library theory \thydx{While_Combinator}.

% which is not part of {text Main} but needs to

% be included explicitly among the ancestor theories.

Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}

and satisfies the recursion equation \begin{isabelle}%

\ \ \ \ \ while\ b\ c\ s\ {\isacharequal}\ {\isacharparenleft}if\ b\ s\ then\ while\ b\ c\ {\isacharparenleft}c\ s{\isacharparenright}\ else\ s{\isacharparenright}%

\end{isabelle}

That is, \isa{while\ b\ c\ s} is equivalent to the imperative program

\begin{verbatim}

     x := s; while b(x) do x := c(x); return x

\end{verbatim}

In general, \isa{s} will be a tuple or record.  As an example

consider the following definition of function \isa{find}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline

\ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline

\ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent

The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}

containing the ``current'' and the ``next'' value of function \isa{f}.

They are initialized with the global \isa{x} and \isa{f\ x}. At the

end \isa{fst} selects the local \isa{x}.

Although the definition of tail recursive functions via \isa{while} avoids

termination proofs, there is no free lunch. When proving properties of

functions defined by \isa{while}, termination rears its ugly head

again. Here is \tdx{while_rule}, the well known proof rule for total

correctness of loops expressed with \isa{while}:

\begin{isabelle}%

\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline

\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline

\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline

\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%

\end{isabelle} \isa{P} needs to be true of

the initial state \isa{s} and invariant under \isa{c} (premises 1

and~2). The post-condition \isa{Q} must become true when leaving the loop

(premise~3). And each loop iteration must descend along a well-founded

relation \isa{r} (premises 4 and~5).

Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead

of induction we apply the above while rule, suitably instantiated.

Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved

by \isa{auto} but falls to \isa{simp}:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline

\ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline

\ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{apply}\ auto\isanewline

\isamarkupfalse%

\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{done}\isamarkupfalse%

%

\begin{isamarkuptext}%

The theorem itself is a simple consequence of this lemma:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{done}\isamarkupfalse%

%

\begin{isamarkuptext}%

Let us conclude this section on partial functions by a

discussion of the merits of the \isa{while} combinator. We have

already seen that the advantage of not having to

provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive

functions tend to be more complicated to reason about. So why use

\isa{while} at all? The only reason is executability: the recursion

equation for \isa{while} is a directly executable functional

program. This is in stark contrast to guarded recursion as introduced

above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the

function body.  Unless \isa{dom} is trivial, this leads to a

definition that is impossible to execute or prohibitively slow.

Thus, if you are aiming for an efficiently executable definition

of a partial function, you are likely to need \isa{while}.%

\end{isamarkuptext}%

\isamarkuptrue%

\isamarkupfalse%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: