diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/Functions/Thy/document/Functions.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Functions/Thy/document/Functions.tex Tue Mar 03 11:00:51 2009 +0100 @@ -0,0 +1,1985 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Functions}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Functions\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Function Definitions for Dummies% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +In most cases, defining a recursive function is just as simple as other definitions:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{fun}\isamarkupfalse% +\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +The syntax is rather self-explanatory: We introduce a function by + giving its name, its type, + and a set of defining recursive equations. + If we leave out the type, the most general type will be + inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{{\isacharplus}} are overloaded, we would end up + with \isa{fib\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}one{\isacharcomma}plus{\isacharbraceright}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +The function always terminates, since its argument gets smaller in + every recursive call. + Since HOL is a logic of total functions, termination is a + fundamental requirement to prevent inconsistencies\footnote{From the + \qt{definition} \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove + \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.}. + Isabelle tries to prove termination automatically when a definition + is made. In \S\ref{termination}, we will look at cases where this + fails and see what to do then.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Pattern matching% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\label{patmatch} + Like in functional programming, we can use pattern matching to + define functions. At the moment we will only consider \emph{constructor + patterns}, which only consist of datatype constructors and + variables. Furthermore, patterns must be linear, i.e.\ all variables + on the left hand side of an equation must be distinct. In + \S\ref{genpats} we discuss more general pattern matching. + + If patterns overlap, the order of the equations is taken into + account. The following function inserts a fixed element between any + two elements of a list:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{fun}\isamarkupfalse% +\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}% +\begin{isamarkuptext}% +Overlapping patterns are interpreted as \qt{increments} to what is + already there: The second equation is only meant for the cases where + the first one does not match. Consequently, Isabelle replaces it + internally by the remaining cases, making the patterns disjoint:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ sep{\isachardot}simps% +\begin{isamarkuptext}% +\begin{isabelle}% +sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}\isasep\isanewline% +sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline% +sep\ a\ {\isacharbrackleft}v{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}v{\isacharbrackright}% +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\noindent The equations from function definitions are automatically used in + simplification:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}sep\ {\isadigit{0}}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Induction% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle provides customized induction rules for recursive + functions. These rules follow the recursive structure of the + definition. Here is the rule \isa{sep{\isachardot}induct} arising from the + above definition of \isa{sep}: + + \begin{isabelle}% +{\isasymlbrakk}{\isasymAnd}a\ x\ y\ xs{\isachardot}\ {\isacharquery}P\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}a{\isachardot}\ {\isacharquery}P\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}a\ v{\isachardot}\ {\isacharquery}P\ a\ {\isacharbrackleft}v{\isacharbrackright}{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}% +\end{isabelle} + + We have a step case for list with at least two elements, and two + base cases for the zero- and the one-element list. Here is a simple + proof about \isa{sep} and \isa{map}% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep\ x\ ys{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}map\ f\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}induct\ x\ ys\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +We get three cases, like in the definition. + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ x\ y\ xs{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ v{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}v{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}v{\isacharbrackright}{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ auto\ \isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +With the \cmd{fun} command, you can define about 80\% of the + functions that occur in practice. The rest of this tutorial explains + the remaining 20\%.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{fun vs.\ function% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \cmd{fun} command provides a + convenient shorthand notation for simple function definitions. In + this mode, Isabelle tries to solve all the necessary proof obligations + automatically. If any proof fails, the definition is + rejected. This can either mean that the definition is indeed faulty, + or that the default proof procedures are just not smart enough (or + rather: not designed) to handle the definition. + + By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or + solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows: + +\end{isamarkuptext} + + +\[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt} +\cmd{fun} \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\% +\cmd{where}\\% +\hspace*{2ex}{\it equations}\\% +\hspace*{2ex}\vdots\vspace*{6pt} +\end{minipage}\right] +\quad\equiv\quad +\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt} +\cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\% +\cmd{where}\\% +\hspace*{2ex}{\it equations}\\% +\hspace*{2ex}\vdots\\% +\cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\% +\cmd{termination by} \isa{lexicographic{\isacharunderscore}order}\vspace{6pt} +\end{minipage} +\right]\] + +\begin{isamarkuptext} + \vspace*{1em} + \noindent Some details have now become explicit: + + \begin{enumerate} + \item The \cmd{sequential} option enables the preprocessing of + pattern overlaps which we already saw. Without this option, the equations + must already be disjoint and complete. The automatic completion only + works with constructor patterns. + + \item A function definition produces a proof obligation which + expresses completeness and compatibility of patterns (we talk about + this later). The combination of the methods \isa{pat{\isacharunderscore}completeness} and + \isa{auto} is used to solve this proof obligation. + + \item A termination proof follows the definition, started by the + \cmd{termination} command. This will be explained in \S\ref{termination}. + \end{enumerate} + Whenever a \cmd{fun} command fails, it is usually a good idea to + expand the syntax to the more verbose \cmd{function} form, to see + what is actually going on.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Termination% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\label{termination} + The method \isa{lexicographic{\isacharunderscore}order} is the default method for + termination proofs. It can prove termination of a + certain class of functions by searching for a suitable lexicographic + combination of size measures. Of course, not all functions have such + a simple termination argument. For them, we can specify the termination + relation manually.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The {\tt relation} method% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Consider the following function, which sums up natural numbers up to + \isa{N}, using a counter \isa{i}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}sum\ i\ N\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isachargreater}\ N\ then\ {\isadigit{0}}\ else\ i\ {\isacharplus}\ sum\ {\isacharparenleft}Suc\ i{\isacharparenright}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent The \isa{lexicographic{\isacharunderscore}order} method fails on this example, because none of the + arguments decreases in the recursive call, with respect to the standard size ordering. + To prove termination manually, we must provide a custom wellfounded relation. + + The termination argument for \isa{sum} is based on the fact that + the \emph{difference} between \isa{i} and \isa{N} gets + smaller in every step, and that the recursion stops when \isa{i} + is greater than \isa{N}. Phrased differently, the expression + \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} always decreases. + + We can use this expression as a measure function suitable to prove termination.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\ sum\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptxt}% +The \cmd{termination} command sets up the termination goal for the + specified function \isa{sum}. If the function name is omitted, it + implicitly refers to the last function definition. + + The \isa{relation} method takes a relation of + type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of + the function. If the function has multiple curried arguments, then + these are packed together into a tuple, as it happened in the above + example. + + The predefined function \isa{{\isachardoublequote}measure\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}} constructs a + wellfounded relation from a mapping into the natural numbers (a + \emph{measure function}). + + After the invocation of \isa{relation}, we must prove that (a) + the relation we supplied is wellfounded, and (b) that the arguments + of recursive calls indeed decrease with respect to the + relation: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ wf\ {\isacharparenleft}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}i\ N{\isachardot}\ {\isasymnot}\ N\ {\isacharless}\ i\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharparenleft}Suc\ i{\isacharcomma}\ N{\isacharparenright}{\isacharcomma}\ i{\isacharcomma}\ N{\isacharparenright}\ {\isasymin}\ measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}% +\end{isabelle} + + These goals are all solved by \isa{auto}:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ auto\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Let us complicate the function a little, by adding some more + recursive calls:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ foo\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}foo\ i\ N\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isachargreater}\ N\ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ {\isacharparenleft}if\ N\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ foo\ {\isadigit{0}}\ {\isacharparenleft}N\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ i\ {\isacharplus}\ foo\ {\isacharparenleft}Suc\ i{\isacharparenright}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +When \isa{i} has reached \isa{N}, it starts at zero again + and \isa{N} is decremented. + This corresponds to a nested + loop where one index counts up and the other down. Termination can + be proved using a lexicographic combination of two measures, namely + the value of \isa{N} and the above difference. The \isa{measures} combinator generalizes \isa{measure} by taking a + list of measure functions.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\ \isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{How \isa{lexicographic{\isacharunderscore}order} works% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +To see how the automatic termination proofs work, let's look at an + example where it fails\footnote{For a detailed discussion of the + termination prover, see \cite{bulwahnKN07}}: + +\end{isamarkuptext} +\cmd{fun} \isa{fails\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\% +\cmd{where}\\% +\hspace*{2ex}\isa{{\isachardoublequote}fails\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ a{\isachardoublequote}}\\% +|\hspace*{1.5ex}\isa{{\isachardoublequote}fails\ a\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ fails\ {\isacharparenleft}x\ {\isacharplus}\ a{\isacharparenright}\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequote}}\\ +\begin{isamarkuptext} + +\noindent Isabelle responds with the following error: + +\begin{isabelle} +*** Unfinished subgoals:\newline +*** (a, 1, <):\newline +*** \ 1.~\isa{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isadigit{0}}}\newline +*** (a, 1, <=):\newline +*** \ 1.~False\newline +*** (a, 2, <):\newline +*** \ 1.~False\newline +*** Calls:\newline +*** a) \isa{{\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}{\isachargreater}\ {\isacharparenleft}x\ {\isacharplus}\ a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}}\newline +*** Measures:\newline +*** 1) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}fst\ x{\isacharparenright}}\newline +*** 2) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}snd\ x{\isacharparenright}}\newline +*** Result matrix:\newline +*** \ \ \ \ 1\ \ 2 \newline +*** a: ? <= \newline +*** Could not find lexicographic termination order.\newline +*** At command "fun".\newline +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +The key to this error message is the matrix at the bottom. The rows + of that matrix correspond to the different recursive calls (In our + case, there is just one). The columns are the function's arguments + (expressed through different measure functions, which map the + argument tuple to a natural number). + + The contents of the matrix summarize what is known about argument + descents: The second argument has a weak descent (\isa{{\isacharless}{\isacharequal}}) at the + recursive call, and for the first argument nothing could be proved, + which is expressed by \isa{{\isacharquery}}. In general, there are the values + \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}. + + For the failed proof attempts, the unfinished subgoals are also + printed. Looking at these will often point to a missing lemma. + +% As a more real example, here is quicksort:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Mutual Recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +If two or more functions call one another mutually, they have to be defined + in one step. Here are \isa{even} and \isa{odd}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}even\ {\isadigit{0}}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}odd\ {\isadigit{0}}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ odd\ n{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ even\ n{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +To eliminate the mutual dependencies, Isabelle internally + creates a single function operating on the sum + type \isa{nat\ {\isacharplus}\ nat}. Then, \isa{even} and \isa{odd} are + defined as projections. Consequently, termination has to be proved + simultaneously for both functions, by specifying a measure on the + sum type:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\ \isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ case\ x\ of\ Inl\ n\ {\isasymRightarrow}\ n\ {\isacharbar}\ Inr\ n\ {\isasymRightarrow}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +We could also have used \isa{lexicographic{\isacharunderscore}order}, which + supports mutual recursive termination proofs to a certain extent.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Induction for mutual recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +When functions are mutually recursive, proving properties about them + generally requires simultaneous induction. The induction rule \isa{even{\isacharunderscore}odd{\isachardot}induct} + generated from the above definition reflects this. + + Let us prove something about \isa{even} and \isa{odd}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ even{\isacharunderscore}odd{\isacharunderscore}mod{\isadigit{2}}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +We apply simultaneous induction, specifying the induction variable + for both goals, separated by \cmd{and}:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}induct\ n\ \isakeyword{and}\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +We get four subgoals, which correspond to the clauses in the + definition of \isa{even} and \isa{odd}: + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ odd\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\ {\isasymLongrightarrow}\ even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}% +\end{isabelle} + Simplification solves the first two goals, leaving us with two + statements about the \isa{mod} operation to prove:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ simp{\isacharunderscore}all% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}% +\end{isabelle} + + \noindent These can be handled by Isabelle's arithmetic decision procedures.% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ arith\isanewline +\isacommand{apply}\isamarkupfalse% +\ arith\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +In proofs like this, the simultaneous induction is really essential: + Even if we are just interested in one of the results, the other + one is necessary to strengthen the induction hypothesis. If we leave + out the statement about \isa{odd} and just write \isa{True} instead, + the same proof fails:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ failed{\isacharunderscore}attempt{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}True{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}induct\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent Now the third subgoal is a dead end, since we have no + useful induction hypothesis available: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ True\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ True\ {\isasymLongrightarrow}\ even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ True% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{oops}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{General pattern matching% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\label{genpats}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Avoiding automatic pattern splitting% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Up to now, we used pattern matching only on datatypes, and the + patterns were always disjoint and complete, and if they weren't, + they were made disjoint automatically like in the definition of + \isa{sep} in \S\ref{patmatch}. + + This automatic splitting can significantly increase the number of + equations involved, and this is not always desirable. The following + example shows the problem: + + Suppose we are modeling incomplete knowledge about the world by a + three-valued datatype, which has values \isa{T}, \isa{F} + and \isa{X} for true, false and uncertain propositions, respectively.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ P{\isadigit{3}}\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ X% +\begin{isamarkuptext}% +\noindent Then the conjunction of such values can be defined as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{fun}\isamarkupfalse% +\ And\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}And\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% +\begin{isamarkuptext}% +This definition is useful, because the equations can directly be used + as simplification rules. But the patterns overlap: For example, + the expression \isa{And\ T\ T} is matched by both the first and + the second equation. By default, Isabelle makes the patterns disjoint by + splitting them up, producing instances:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ And{\isachardot}simps% +\begin{isamarkuptext}% +\isa{And\ T\ {\isacharquery}p\ {\isacharequal}\ {\isacharquery}p\isasep\isanewline% +And\ F\ T\ {\isacharequal}\ F\isasep\isanewline% +And\ X\ T\ {\isacharequal}\ X\isasep\isanewline% +And\ F\ F\ {\isacharequal}\ F\isasep\isanewline% +And\ X\ F\ {\isacharequal}\ F\isasep\isanewline% +And\ F\ X\ {\isacharequal}\ F\isasep\isanewline% +And\ X\ X\ {\isacharequal}\ X} + + \vspace*{1em} + \noindent There are several problems with this: + + \begin{enumerate} + \item If the datatype has many constructors, there can be an + explosion of equations. For \isa{And}, we get seven instead of + five equations, which can be tolerated, but this is just a small + example. + + \item Since splitting makes the equations \qt{less general}, they + do not always match in rewriting. While the term \isa{And\ x\ F} + can be simplified to \isa{F} with the original equations, a + (manual) case split on \isa{x} is now necessary. + + \item The splitting also concerns the induction rule \isa{And{\isachardot}induct}. Instead of five premises it now has seven, which + means that our induction proofs will have more cases. + + \item In general, it increases clarity if we get the same definition + back which we put in. + \end{enumerate} + + If we do not want the automatic splitting, we can switch it off by + leaving out the \cmd{sequential} option. However, we will have to + prove that our pattern matching is consistent\footnote{This prevents + us from defining something like \isa{f\ x\ {\isacharequal}\ True} and \isa{f\ x\ {\isacharequal}\ False} simultaneously.}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ And{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +\noindent Now let's look at the proof obligations generated by a + function definition. In this case, they are: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}{\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ \ }{\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ }{\isasymLongrightarrow}\ P\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline +\ {\isadigit{5}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline +\ {\isadigit{6}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X\isanewline +\ {\isadigit{7}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline +\ {\isadigit{8}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline +\ {\isadigit{9}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline +\ {\isadigit{1}}{\isadigit{0}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X% +\end{isabelle}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em} + + The first subgoal expresses the completeness of the patterns. It has + the form of an elimination rule and states that every \isa{x} of + the function's input type must match at least one of the patterns\footnote{Completeness could + be equivalently stated as a disjunction of existential statements: +\isa{{\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}}, and you can use the method \isa{atomize{\isacharunderscore}elim} to get that form instead.}. If the patterns just involve + datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness} + method:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ pat{\isacharunderscore}completeness% +\begin{isamarkuptxt}% +The remaining subgoals express \emph{pattern compatibility}. We do + allow that an input value matches multiple patterns, but in this + case, the result (i.e.~the right hand sides of the equations) must + also be equal. For each pair of two patterns, there is one such + subgoal. Usually this needs injectivity of the constructors, which + is used automatically by \isa{auto}.% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{by}\isamarkupfalse% +\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Non-constructor patterns% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Most of Isabelle's basic types take the form of inductive datatypes, + and usually pattern matching works on the constructors of such types. + However, this need not be always the case, and the \cmd{function} + command handles other kind of patterns, too. + + One well-known instance of non-constructor patterns are + so-called \emph{$n+k$-patterns}, which are a little controversial in + the functional programming world. Here is the initial fibonacci + example with $n+k$-patterns:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ fib{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}\ n\ {\isacharplus}\ fib{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +This kind of matching is again justified by the proof of pattern + completeness and compatibility. + The proof obligation for pattern completeness states that every natural number is + either \isa{{\isadigit{0}}}, \isa{{\isadigit{1}}} or \isa{n\ {\isacharplus}\ {\isadigit{2}}}: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ x\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline +\ {\isadigit{5}}{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{6}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline +\ {\isadigit{7}}{\isachardot}\ {\isasymAnd}n\ na{\isachardot}\isanewline +\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ na\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ na\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ na{\isacharparenright}% +\end{isabelle} + + This is an arithmetic triviality, but unfortunately the + \isa{arith} method cannot handle this specific form of an + elimination rule. However, we can use the method \isa{atomize{\isacharunderscore}elim} to do an ad-hoc conversion to a disjunction of + existentials, which can then be solved by the arithmetic decision procedure. + Pattern compatibility and termination are automatic as usual.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ atomize{\isacharunderscore}elim\isanewline +\isacommand{apply}\isamarkupfalse% +\ arith\isanewline +\isacommand{apply}\isamarkupfalse% +\ auto\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{termination}\isamarkupfalse% +% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ lexicographic{\isacharunderscore}order% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +We can stretch the notion of pattern matching even more. The + following function is not a sensible functional program, but a + perfectly valid mathematical definition:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ ev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}ev\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}ev\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ atomize{\isacharunderscore}elim\isanewline +\isacommand{by}\isamarkupfalse% +\ arith{\isacharplus}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{termination}\isamarkupfalse% +% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +This general notion of pattern matching gives you a certain freedom + in writing down specifications. However, as always, such freedom should + be used with care: + + If we leave the area of constructor + patterns, we have effectively departed from the world of functional + programming. This means that it is no longer possible to use the + code generator, and expect it to generate ML code for our + definitions. Also, such a specification might not work very well together with + simplification. Your mileage may vary.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Conditional equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The function package also supports conditional equations, which are + similar to guards in a language like Haskell. Here is Euclid's + algorithm written with conditional patterns\footnote{Note that the + patterns are also overlapping in the base case}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}gcd\ x\ {\isadigit{0}}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}gcd\ {\isadigit{0}}\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ gcd\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}y\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ gcd\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}x\ {\isacharminus}\ y{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}atomize{\isacharunderscore}elim{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{termination}\isamarkupfalse% +% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ lexicographic{\isacharunderscore}order% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +By now, you can probably guess what the proof obligations for the + pattern completeness and compatibility look like. + + Again, functions with conditional patterns are not supported by the + code generator.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Pattern matching on strings% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +As strings (as lists of characters) are normal datatypes, pattern + matching on them is possible, but somewhat problematic. Consider the + following definition: + +\end{isamarkuptext} +\noindent\cmd{fun} \isa{check\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}string\ {\isasymRightarrow}\ bool{\isachardoublequote}}\\% +\cmd{where}\\% +\hspace*{2ex}\isa{{\isachardoublequote}check\ {\isacharparenleft}{\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}}\\% +\isa{{\isacharbar}\ {\isachardoublequote}check\ s\ {\isacharequal}\ False{\isachardoublequote}} +\begin{isamarkuptext} + + \noindent An invocation of the above \cmd{fun} command does not + terminate. What is the problem? Strings are lists of characters, and + characters are a datatype with a lot of constructors. Splitting the + catch-all pattern thus leads to an explosion of cases, which cannot + be handled by Isabelle. + + There are two things we can do here. Either we write an explicit + \isa{if} on the right hand side, or we can use conditional patterns:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ check\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}string\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}check\ {\isacharparenleft}{\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}s\ {\isasymnoteq}\ {\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}\ {\isasymLongrightarrow}\ check\ s\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{Partiality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +In HOL, all functions are total. A function \isa{f} applied to + \isa{x} always has the value \isa{f\ x}, and there is no notion + of undefinedness. + This is why we have to do termination + proofs when defining functions: The proof justifies that the + function can be defined by wellfounded recursion. + + However, the \cmd{function} package does support partiality to a + certain extent. Let's look at the following function which looks + for a zero of a given function f.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ {\isacharparenleft}if\ f\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent Clearly, any attempt of a termination proof must fail. And without + that, we do not get the usual rules \isa{findzero{\isachardot}simps} and + \isa{findzero{\isachardot}induct}. So what was the definition good for at all?% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Domain predicates% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The trick is that Isabelle has not only defined the function \isa{findzero}, but also + a predicate \isa{findzero{\isacharunderscore}dom} that characterizes the values where the function + terminates: the \emph{domain} of the function. If we treat a + partial function just as a total function with an additional domain + predicate, we can derive simplification and + induction rules as we do for total functions. They are guarded + by domain conditions and are called \isa{psimps} and \isa{pinduct}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}% +findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}% +\end{isabelle}\end{minipage} + \hfill(\isa{findzero{\isachardot}psimps}) + \vspace{1em} + + \noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}% +{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ }{\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ n{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}% +\end{isabelle}\end{minipage} + \hfill(\isa{findzero{\isachardot}pinduct})% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +Remember that all we + are doing here is use some tricks to make a total function appear + as if it was partial. We can still write the term \isa{findzero\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}} and like any other term of type \isa{nat} it is equal + to some natural number, although we might not be able to find out + which one. The function is \emph{underdefined}. + + But it is defined enough to prove something interesting about it. We + can prove that if \isa{findzero\ f\ n} + terminates, it indeed returns a zero of \isa{f}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +\noindent We apply induction as usual, but using the partial induction + rule:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent This gives the following subgoals: + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}% +\end{isabelle} + + \noindent The hypothesis in our lemma was used to satisfy the first premise in + the induction rule. However, we also get \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as a local assumption in the induction step. This + allows to unfold \isa{findzero\ f\ n} using the \isa{psimps} + rule, and the rest is trivial. Since the \isa{psimps} rules carry the + \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ simp\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Proofs about partial functions are often not harder than for total + functions. Fig.~\ref{findzero_isar} shows a slightly more + complicated proof written in Isar. It is verbose enough to show how + partiality comes into play: From the partial induction, we get an + additional domain condition hypothesis. Observe how this condition + is applied when calls to \isa{findzero} are unfolded.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\hrule\vspace{6pt} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ f\ n\ \isacommand{assume}\isamarkupfalse% +\ dom{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isakeyword{and}\ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isakeyword{and}\ x{\isacharunderscore}range{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ dom\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse% +\ False\ \isacommand{by}\isamarkupfalse% +\ auto\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\ \ \isanewline +\ \ \isacommand{from}\isamarkupfalse% +\ x{\isacharunderscore}range\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isacharequal}\ n\ {\isasymor}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ auto\isanewline +\ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \ \ \isacommand{with}\isamarkupfalse% +\ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\vspace{6pt}\hrule +\caption{A proof about a partial function}\label{findzero_isar} +\end{figure} +% +\isamarkupsubsection{Partial termination proofs% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Now that we have proved some interesting properties about our + function, we should turn to the domain predicate and see if it is + actually true for some values. Otherwise we would have just proved + lemmas with \isa{False} as a premise. + + Essentially, we need some introduction rules for \isa{findzero{\isacharunderscore}dom}. The function package can prove such domain + introduction rules automatically. But since they are not used very + often (they are almost never needed if the function is total), this + functionality is disabled by default for efficiency reasons. So we have to go + back and ask for them explicitly by passing the \isa{{\isacharparenleft}domintros{\isacharparenright}} option to the function package: + +\vspace{1ex} +\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\% +\cmd{where}\isanewline% +\ \ \ldots\\ + + \noindent Now the package has proved an introduction rule for \isa{findzero{\isacharunderscore}dom}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}domintros% +\begin{isamarkuptext}% +\begin{isabelle}% +{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}% +\end{isabelle} + + Domain introduction rules allow to show that a given value lies in the + domain of a function, if the arguments of all recursive calls + are in the domain as well. They allow to do a \qt{single step} in a + termination proof. Usually, you want to combine them with a suitable + induction principle. + + Since our function increases its argument at recursive calls, we + need an induction principle which works \qt{backwards}. We will use + \isa{inc{\isacharunderscore}induct}, which allows to do induction from a fixed number + \qt{downwards}: + + \begin{center}\isa{{\isasymlbrakk}{\isacharquery}i\ {\isasymle}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}j{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}i}\hfill(\isa{inc{\isacharunderscore}induct})\end{center} + + Figure \ref{findzero_term} gives a detailed Isar proof of the fact + that \isa{findzero} terminates if there is a zero which is greater + or equal to \isa{n}. First we derive two useful rules which will + solve the base case and the step case of the induction. The + induction is then straightforward, except for the unusual induction + principle.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\hrule\vspace{6pt} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}termination{\isacharcolon}\isanewline +\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isasymge}\ n{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\ {\isacharminus}\ \isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ base{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}{\isacharbackquoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ step{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i{\isachardot}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}\ \isanewline +\ \ \ \ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ simp\isanewline +\isanewline +\ \ \isacommand{from}\isamarkupfalse% +\ {\isacharbackquoteopen}x\ {\isasymge}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% +\ {\isacharquery}thesis\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ base{\isacharparenright}\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ i\ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}rule\ step{\isacharparenright}\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage}\vspace{6pt}\hrule +\caption{Termination proof for \isa{findzero}}\label{findzero_term} +\end{figure} +% +\begin{isamarkuptext}% +Again, the proof given in Fig.~\ref{findzero_term} has a lot of + detail in order to explain the principles. Using more automation, we + can also have a short proof:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}termination{\isacharunderscore}short{\isacharcolon}\isanewline +\ \ \isakeyword{assumes}\ zero{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline +\ \ \isakeyword{assumes}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{using}\isamarkupfalse% +\ zero\isanewline +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent It is simple to combine the partial correctness result with the + termination lemma:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ findzero{\isacharunderscore}total{\isacharunderscore}correctness{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}blast\ intro{\isacharcolon}\ findzero{\isacharunderscore}zero\ findzero{\isacharunderscore}termination{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Definition of the domain predicate% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Sometimes it is useful to know what the definition of the domain + predicate looks like. Actually, \isa{findzero{\isacharunderscore}dom} is just an + abbreviation: + + \begin{isabelle}% +findzero{\isacharunderscore}dom\ {\isasymequiv}\ accp\ findzero{\isacharunderscore}rel% +\end{isabelle} + + The domain predicate is the \emph{accessible part} of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function + package. \isa{findzero{\isacharunderscore}rel} is just a normal + inductive predicate, so we can inspect its definition by + looking at the introduction rules \isa{findzero{\isacharunderscore}rel{\isachardot}intros}. + In our case there is just a single rule: + + \begin{isabelle}% +{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}rel\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}% +\end{isabelle} + + The predicate \isa{findzero{\isacharunderscore}rel} + describes the \emph{recursion relation} of the function + definition. The recursion relation is a binary relation on + the arguments of the function that relates each argument to its + recursive calls. In general, there is one introduction rule for each + recursive call. + + The predicate \isa{findzero{\isacharunderscore}dom} is the accessible part of + that relation. An argument belongs to the accessible part, if it can + be reached in a finite number of steps (cf.~its definition in \isa{Wellfounded{\isachardot}thy}). + + Since the domain predicate is just an abbreviation, you can use + lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some + lemmas which are occasionally useful are \isa{accpI}, \isa{accp{\isacharunderscore}downward}, and of course the introduction and elimination rules + for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{A Useful Special Case: Tail recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The domain predicate is our trick that allows us to model partiality + in a world of total functions. The downside of this is that we have + to carry it around all the time. The termination proof above allowed + us to replace the abstract \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} by the more + concrete \isa{n\ {\isasymle}\ x\ {\isasymand}\ f\ x\ {\isacharequal}\ {\isadigit{0}}}, but the condition is still + there and can only be discharged for special cases. + In particular, the domain predicate guards the unfolding of our + function, since it is there as a condition in the \isa{psimp} + rules. + + Now there is an important special case: We can actually get rid + of the condition in the simplification rules, \emph{if the function + is tail-recursive}. The reason is that for all tail-recursive + equations there is a total function satisfying them, even if they + are non-terminating. + +% A function is tail recursive, if each call to the function is either +% equal +% +% So the outer form of the +% +%if it can be written in the following +% form: +% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"} + + + The function package internally does the right construction and can + derive the unconditional simp rules, if we ask it to do so. Luckily, + our \isa{findzero} function is tail-recursive, so we can just go + back and add another option to the \cmd{function} command: + +\vspace{1ex} +\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharcomma}\ tailrec{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\% +\cmd{where}\isanewline% +\ \ \ldots\\% + + + \noindent Now, we actually get unconditional simplification rules, even + though the function is partial:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ findzero{\isachardot}simps% +\begin{isamarkuptext}% +\begin{isabelle}% +findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}% +\end{isabelle} + + \noindent Of course these would make the simplifier loop, so we better remove + them from the simpset:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{declare}\isamarkupfalse% +\ findzero{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}% +\begin{isamarkuptext}% +Getting rid of the domain conditions in the simplification rules is + not only useful because it simplifies proofs. It is also required in + order to use Isabelle's code generator to generate ML code + from a function definition. + Since the code generator only works with equations, it cannot be + used with \isa{psimp} rules. Thus, in order to generate code for + partial functions, they must be defined as a tail recursion. + Luckily, many functions have a relatively natural tail recursive + definition.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Nested recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Recursive calls which are nested in one another frequently cause + complications, since their termination proof can depend on a partial + correctness property of the function itself. + + As a small example, we define the \qt{nested zero} function:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ nz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}nz\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}nz\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ nz\ {\isacharparenleft}nz\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +If we attempt to prove termination using the identity measure on + naturals, this fails:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ \isacommand{apply}\isamarkupfalse% +\ auto% +\begin{isamarkuptxt}% +We get stuck with the subgoal + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharless}\ Suc\ n% +\end{isabelle} + + Of course this statement is true, since we know that \isa{nz} is + the zero function. And in fact we have no problem proving this + property by induction.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isacommand{lemma}\isamarkupfalse% +\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +We formulate this as a partial correctness lemma with the condition + \isa{nz{\isacharunderscore}dom\ n}. This allows us to prove it with the \isa{pinduct} rule before we have proved termination. With this lemma, + the termination proof works as expected:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +As a general strategy, one should prove the statements needed for + termination as a partial property first. Then they can be used to do + the termination proof. This also works for less trivial + examples. Figure \ref{f91} defines the 91-function, a well-known + challenge problem due to John McCarthy, and proves its termination.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{figure} +\hrule\vspace{6pt} +\begin{minipage}{0.8\textwidth} +\isabellestyle{it} +\isastyle\isamarkuptrue +\isacommand{function}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n\ then\ n\ {\isacharminus}\ {\isadigit{1}}{\isadigit{0}}\ else\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ pat{\isacharunderscore}completeness\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate{\isacharcolon}\ \isanewline +\ \ \isakeyword{assumes}\ trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ n{\isachardoublequoteclose}\ \isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{using}\isamarkupfalse% +\ trm\ \isacommand{by}\isamarkupfalse% +\ induct\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{termination}\isamarkupfalse% +\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \isacommand{let}\isamarkupfalse% +\ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{1}}\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}wf\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isacommand{assume}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isachardoublequoteclose}\ % +\isamarkupcmt{Assumptions for both calls% +} +\isanewline +\isanewline +\ \ \isacommand{thus}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\ % +\isamarkupcmt{Inner call% +} +\isanewline +\isanewline +\ \ \isacommand{assume}\isamarkupfalse% +\ inner{\isacharunderscore}trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ % +\isamarkupcmt{Outer call% +} +\isanewline +\ \ \isacommand{with}\isamarkupfalse% +\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate\ \isacommand{have}\isamarkupfalse% +\ {\isachardoublequoteopen}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +\isanewline +\ \ \isacommand{with}\isamarkupfalse% +\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupfalse\isabellestyle{tt} +\end{minipage} +\vspace{6pt}\hrule +\caption{McCarthy's 91-function}\label{f91} +\end{figure} +% +\isamarkupsection{Higher-Order Recursion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Higher-order recursion occurs when recursive calls + are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc. + As an example, imagine a datatype of n-ary trees:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ tree\ {\isacharequal}\ \isanewline +\ \ Leaf\ {\isacharprime}a\ \isanewline +{\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ list{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent We can define a function which swaps the left and right subtrees recursively, using the + list functions \isa{rev} and \isa{map}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{fun}\isamarkupfalse% +\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +Although the definition is accepted without problems, let us look at the termination proof:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{termination}\isamarkupfalse% +% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +% +\begin{isamarkuptxt}% +As usual, we have to give a wellfounded relation, such that the + arguments of the recursive calls get smaller. But what exactly are + the arguments of the recursive calls when mirror is given as an + argument to \isa{map}? Isabelle gives us the + subgoals + + \begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R% +\end{isabelle} + + So the system seems to know that \isa{map} only + applies the recursive call \isa{mirror} to elements + of \isa{l}, which is essential for the termination proof. + + This knowledge about \isa{map} is encoded in so-called congruence rules, + which are special theorems known to the \cmd{function} command. The + rule for \isa{map} is + + \begin{isabelle}% +{\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys% +\end{isabelle} + + You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions + coincide on the elements of the list. This means that for the value + \isa{map\ f\ l} we only have to know how \isa{f} behaves on + the elements of \isa{l}. + + Usually, one such congruence rule is + needed for each higher-order construct that is used when defining + new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handled by this mechanism. The congruence + rule for \isa{If} states that the \isa{then} branch is only + relevant if the condition is true, and the \isa{else} branch only if it + is false: + + \begin{isabelle}% +{\isasymlbrakk}{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c{\isacharsemicolon}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ {\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}% +\end{isabelle} + + Congruence rules can be added to the + function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute. + + The constructs that are predefined in Isabelle, usually + come with the respective congruence rules. + But if you define your own higher-order functions, you may have to + state and prove the required congruence rules yourself, if you want to use your + functions in recursive definitions.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Congruence Rules and Evaluation Order% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Higher order logic differs from functional programming languages in + that it has no built-in notion of evaluation order. A program is + just a set of equations, and it is not specified how they must be + evaluated. + + However for the purpose of function definition, we must talk about + evaluation order implicitly, when we reason about termination. + Congruence rules express that a certain evaluation order is + consistent with the logical definition. + + Consider the following function.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{function}\isamarkupfalse% +\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ f\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +For this definition, the termination proof fails. The default configuration + specifies no congruence rule for disjunction. We have to add a + congruence rule that specifies left-to-right evaluation order: + + \vspace{1ex} + \noindent \isa{{\isasymlbrakk}{\isacharquery}P\ {\isacharequal}\ {\isacharquery}P{\isacharprime}{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharequal}\ {\isacharquery}Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}P\ {\isasymor}\ {\isacharquery}Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}P{\isacharprime}\ {\isasymor}\ {\isacharquery}Q{\isacharprime}{\isacharparenright}}\hfill(\isa{disj{\isacharunderscore}cong}) + \vspace{1ex} + + Now the definition works without problems. Note how the termination + proof depends on the extra condition that we get from the congruence + rule. + + However, as evaluation is not a hard-wired concept, we + could just turn everything around by declaring a different + congruence rule. Then we can make the reverse definition:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ disj{\isacharunderscore}cong{\isadigit{2}}{\isacharbrackleft}fundef{\isacharunderscore}cong{\isacharbrackright}{\isacharcolon}\ \isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymnot}\ Q{\isacharprime}\ {\isasymLongrightarrow}\ P\ {\isacharequal}\ P{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymor}\ Q{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{fun}\isamarkupfalse% +\ f{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}f{\isacharprime}\ n\ {\isacharequal}\ {\isacharparenleft}f{\isacharprime}\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymor}\ n\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent These examples show that, in general, there is no \qt{best} set of + congruence rules. + + However, such tweaking should rarely be necessary in + practice, as most of the time, the default set of congruence rules + works well.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: