doc-src/TutorialI/Advanced/document/Partial.tex
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
child 10668 3b84288e60b7
permissions -rw-r--r--
*** empty log message ***
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: