nipkow@10654  1 %  nipkow@10654  2 \begin{isabellebody}%  nipkow@10654  3 \def\isabellecontext{Partial}%  nipkow@10654  4 %  nipkow@10654  5 \begin{isamarkuptext}%  nipkow@10654  6 \noindent  nipkow@10654  7 Throughout the tutorial we have emphasized the fact that all functions  nipkow@10654  8 in HOL are total. Hence we cannot hope to define truly partial  nipkow@10654  9 functions. The best we can do are functions that are  nipkow@10654  10 \emph{underdefined}\index{underdefined function}:  nipkow@10654  11 for certain arguments we only know that a result  nipkow@10654  12 exists, but we don't know what it is. When defining functions that are  nipkow@10654  13 normally considered partial, underdefinedness turns out to be a very  nipkow@10654  14 reasonable alternative.  nipkow@10654  15 nipkow@10654  16 We have already seen an instance of underdefinedness by means of  nipkow@10654  17 non-exhaustive pattern matching: the definition of \isa{last} in  nipkow@10654  18 \S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%  nipkow@10654  19 \end{isamarkuptext}%  nipkow@10654  20 \isacommand{consts}\ hd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline  nipkow@10654  21 \isacommand{primrec}\ {\isachardoublequote}hd\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}%  nipkow@10654  22 \begin{isamarkuptext}%  nipkow@10654  23 \noindent  nipkow@10654  24 although it generates a warning.  nipkow@10654  25 nipkow@10654  26 Even ordinary definitions allow underdefinedness, this time by means of  nipkow@10654  27 preconditions:%  nipkow@10654  28 \end{isamarkuptext}%  nipkow@10654  29 \isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline  nipkow@10654  30 {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}%  nipkow@10654  31 \begin{isamarkuptext}%  nipkow@10654  32 The rest of this section is devoted to the question of how to define  nipkow@10654  33 partial recursive functions by other means that non-exhaustive pattern  nipkow@10654  34 matching.%  nipkow@10654  35 \end{isamarkuptext}%  nipkow@10654  36 %  nipkow@10654  37 \isamarkupsubsubsection{Guarded recursion%  nipkow@10654  38 }  nipkow@10654  39 %  nipkow@10654  40 \begin{isamarkuptext}%  nipkow@10654  41 Neither \isacommand{primrec} nor \isacommand{recdef} allow to  nipkow@10654  42 prefix an equation with a condition in the way ordinary definitions do  nipkow@10654  43 (see \isa{minus} above). Instead we have to move the condition over  nipkow@10654  44 to the right-hand side of the equation. Given a partial function $f$  nipkow@10654  45 that should satisfy the recursion equation $f(x) = t$ over its domain  nipkow@10654  46 $dom(f)$, we turn this into the \isacommand{recdef}  nipkow@10654  47 \begin{isabelle}%  nipkow@10654  48 \ \ \ \ \ f\ x\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymin}\ dom\ f\ then\ t\ else\ arbitrary{\isacharparenright}%  nipkow@10654  49 \end{isabelle}  nipkow@10654  50 where \isa{arbitrary} is a predeclared constant of type \isa{{\isacharprime}a}  nipkow@10654  51 which has no definition. Thus we know nothing about its value,  nipkow@10654  52 which is ideal for specifying underdefined functions on top of it.  nipkow@10654  53 nipkow@10654  54 As a simple example we define division on \isa{nat}:%  nipkow@10654  55 \end{isamarkuptext}%  nipkow@10654  56 \isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline  nipkow@10654  57 \isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline  nipkow@10654  58 \ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline  nipkow@10654  59 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}%  nipkow@10654  60 \begin{isamarkuptext}%  nipkow@10654  61 \noindent Of course we could also have defined  nipkow@10654  62 \isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The  nipkow@10654  63 latter option is chosen for the predefined \isa{div} function, which  nipkow@10654  64 simplifies proofs at the expense of moving further away from the  nipkow@10654  65 standard mathematical divison function.  nipkow@10654  66 nipkow@10654  67 As a more substantial example we consider the problem of searching a graph.  nipkow@10654  68 For simplicity our graph is given by a function (\isa{f}) of  nipkow@10654  69 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which  nipkow@10654  70 maps each node to its successor, and the task is to find the end of a chain,  nipkow@10654  71 i.e.\ a node pointing to itself. Here is a first attempt:  nipkow@10654  72 \begin{isabelle}%  nipkow@10654  73 \ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%  nipkow@10654  74 \end{isabelle}  nipkow@10654  75 This may be viewed as a fixed point finder or as one half of the well known  nipkow@10654  76 \emph{Union-Find} algorithm.  nipkow@10654  77 The snag is that it may not terminate if \isa{f} has nontrivial cycles.  nipkow@10654  78 Phrased differently, the relation%  nipkow@10654  79 \end{isamarkuptext}%  nipkow@10654  80 \isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline  nipkow@10654  81 \ \ {\isachardoublequote}step{\isadigit{1}}\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymand}\ y\ {\isasymnoteq}\ x{\isacharbraceright}{\isachardoublequote}%  nipkow@10654  82 \begin{isamarkuptext}%  nipkow@10654  83 \noindent  nipkow@10654  84 must be well-founded. Thus we make the following definition:%  nipkow@10654  85 \end{isamarkuptext}%  nipkow@10654  86 \isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline  nipkow@10654  87 \isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline  nipkow@10654  88 \ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline  nipkow@10654  89 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline  nipkow@10654  90 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline  nipkow@10654  91 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%  nipkow@10654  92 \begin{isamarkuptext}%  nipkow@10654  93 \noindent  nipkow@10654  94 The recursion equation itself should be clear enough: it is our aborted  nipkow@10654  95 first attempt augmented with a check that there are no non-trivial loops.  nipkow@10654  96 nipkow@10654  97 What complicates the termination proof is that the argument of  nipkow@10654  98 \isa{find} is a pair. To express the required well-founded relation  nipkow@10654  99 we employ the predefined combinator \isa{same{\isacharunderscore}fst} of type  nipkow@10654  100 \begin{isabelle}%  nipkow@10654  101 \ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%  nipkow@10654  102 \end{isabelle}  nipkow@10654  103 defined as  nipkow@10654  104 \begin{isabelle}%  nipkow@10654  105 \ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%  nipkow@10654  106 \end{isabelle}  nipkow@10654  107 This combinator is designed for recursive functions on pairs where the first  nipkow@10654  108 component of the argument is passed unchanged to all recursive  nipkow@10654  109 calls. Given a constraint on the first component and a relation on the second  nipkow@10654  110 component, \isa{same{\isacharunderscore}fst} builds the required relation on pairs.  nipkow@10654  111 The theorem \begin{isabelle}%  nipkow@10654  112 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%  nipkow@10654  113 \end{isabelle}  nipkow@10654  114 is known to the well-foundedness prover of \isacommand{recdef}.  nipkow@10654  115 Thus well-foundedness of the given relation is immediate.  nipkow@10654  116 Furthermore, each recursive call descends along the given relation:  nipkow@10654  117 the first argument stays unchanged and the second one descends along  nipkow@10654  118 \isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions.  nipkow@10654  119 nipkow@10654  120 Normally you will then derive the following conditional variant of and from  nipkow@10654  121 the recursion equation%  nipkow@10654  122 \end{isamarkuptext}%  nipkow@10654  123 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline  nipkow@10654  124 \ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline  nipkow@10654  125 \isacommand{by}\ simp%  nipkow@10654  126 \begin{isamarkuptext}%  nipkow@10654  127 \noindent and then disable the original recursion equation:%  nipkow@10654  128 \end{isamarkuptext}%  nipkow@10654  129 \isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%  nipkow@10654  130 \begin{isamarkuptext}%  nipkow@10654  131 We can reason about such underdefined functions just like about any other  nipkow@10654  132 recursive function. Here is a simple example of recursion induction:%  nipkow@10654  133 \end{isamarkuptext}%  nipkow@10654  134 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline  nipkow@10654  135 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline  nipkow@10654  136 \isacommand{apply}\ simp\isanewline  nipkow@10654  137 \isacommand{done}%  nipkow@10654  138 \isamarkupsubsubsection{The {\tt\slshape while} combinator%  nipkow@10654  139 }  nipkow@10654  140 %  nipkow@10654  141 \begin{isamarkuptext}%  nipkow@10654  142 If the recursive function happens to be tail recursive, its  nipkow@10654  143 definition becomes a triviality if based on the predefined \isaindexbold{while}  nipkow@10654  144 combinator. The latter lives in the library theory  nipkow@10654  145 \isa{While_Combinator}, which is not part of \isa{Main} but needs to  nipkow@10654  146 be included explicitly among the ancestor theories.  nipkow@10654  147 nipkow@10654  148 Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}  nipkow@10654  149 and satisfies the recursion equation \begin{isabelle}%  nipkow@10654  150 \ \ \ \ \ while\ b\ c\ s\ {\isacharequal}\ {\isacharparenleft}if\ b\ s\ then\ while\ b\ c\ {\isacharparenleft}c\ s{\isacharparenright}\ else\ s{\isacharparenright}%  nipkow@10654  151 \end{isabelle}  nipkow@10654  152 That is, \isa{while\ b\ c\ s} is equivalent to the imperative program  nipkow@10654  153 \begin{verbatim}  nipkow@10654  154  x := s; while b(x) do x := c(x); return x  nipkow@10654  155 \end{verbatim}  nipkow@10654  156 In general, \isa{s} will be a tuple (better still: a record). As an example  nipkow@10654  157 consider the tail recursive variant of function \isa{find} above:%  nipkow@10654  158 \end{isamarkuptext}%  nipkow@10654  159 \isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline  nipkow@10654  160 \ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline  nipkow@10654  161 \ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}%  nipkow@10654  162 \begin{isamarkuptext}%  nipkow@10654  163 \noindent  nipkow@10654  164 The loop operates on two local variables'' \isa{x} and \isa{x{\isacharprime}}  nipkow@10654  165 containing the current'' and the next'' value of function \isa{f}.  nipkow@10654  166 They are initalized with the global \isa{x} and \isa{f\ x}. At the  nipkow@10654  167 end \isa{fst} selects the local \isa{x}.  nipkow@10654  168 nipkow@10654  169 This looks like we can define at least tail recursive functions  nipkow@10654  170 without bothering about termination after all. But there is no free  nipkow@10654  171 lunch: when proving properties of functions defined by \isa{while},  nipkow@10654  172 termination rears its ugly head again. Here is  nipkow@10654  173 \isa{while{\isacharunderscore}rule}, the well known proof rule for total  nipkow@10654  174 correctness of loops expressed with \isa{while}:  nipkow@10654  175 \begin{isabelle}%  nipkow@10654  176 \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline  nipkow@10654  177 \ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline  nipkow@10654  178 \ \ \ \ \ \ \ \ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline  nipkow@10654  179 \ \ \ \ \ {\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%  nipkow@10654  180 \end{isabelle} \isa{P} needs to be  nipkow@10654  181 true of the initial state \isa{s} and invariant under \isa{c}  nipkow@10654  182 (premises 1 and 2).The post-condition \isa{Q} must become true when  nipkow@10654  183 leaving the loop (premise 3). And each loop iteration must descend  nipkow@10654  184 along a well-founded relation \isa{r} (premises 4 and 5).  nipkow@10654  185 nipkow@10654  186 Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead  nipkow@10654  187 of induction we apply the above while rule, suitably instantiated.  nipkow@10654  188 Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved  nipkow@10654  189 by \isa{auto} but falls to \isa{simp}:%  nipkow@10654  190 \end{isamarkuptext}%  nipkow@10654  191 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharsemicolon}\ x{\isacharprime}\ {\isacharequal}\ f\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}y\ y{\isacharprime}{\isachardot}\isanewline  nipkow@10654  192 \ \ \ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharprime}{\isacharparenright}\ {\isasymand}\isanewline  nipkow@10654  193 \ \ \ y{\isacharprime}\ {\isacharequal}\ y\ {\isasymand}\ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline  nipkow@10654  194 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline  nipkow@10654  195 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline  nipkow@10654  196 \isacommand{apply}\ auto\isanewline  nipkow@10654  197 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline  nipkow@10654  198 \isacommand{done}%  nipkow@10654  199 \begin{isamarkuptext}%  nipkow@10654  200 The theorem itself is a simple consequence of this lemma:%  nipkow@10654  201 \end{isamarkuptext}%  nipkow@10654  202 \isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline  nipkow@10654  203 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline  nipkow@10654  204 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline  nipkow@10654  205 \isacommand{done}%  nipkow@10654  206 \begin{isamarkuptext}%  nipkow@10654  207 Let us conclude this section on partial functions by a  nipkow@10654  208 discussion of the merits of the \isa{while} combinator. We have  nipkow@10654  209 already seen that the advantage (if it is one) of not having to  nipkow@10654  210 provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive  nipkow@10654  211 functions tend to be more complicated to reason about. So why use  nipkow@10654  212 \isa{while} at all? The only reason is executability: the recursion  nipkow@10654  213 equation for \isa{while} is a directly executable functional  nipkow@10654  214 program. This is in stark contrast to guarded recursion as introduced  nipkow@10654  215 above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the  nipkow@10654  216 function body. Unless \isa{dom} is trivial, this leads to a  nipkow@10654  217 definition which is either not at all executable or prohibitively  nipkow@10654  218 expensive. Thus, if you are aiming for an efficiently executable definition  nipkow@10654  219 of a partial function, you are likely to need \isa{while}.%  nipkow@10654  220 \end{isamarkuptext}%  nipkow@10654  221 \end{isabellebody}%  nipkow@10654  222 %%% Local Variables:  nipkow@10654  223 %%% mode: latex  nipkow@10654  224 %%% TeX-master: "root"  nipkow@10654  225 %%% End: