diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Mon Mar 02 16:58:39 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1985 +0,0 @@ -% -\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: