wneuper/isa: doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex@62e0f892e525

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Functions}%

4 %

     5 \isadelimtheory

     6 \isanewline

     7 \isanewline

8 %

     9 \endisadelimtheory

    10 %

    11 \isatagtheory

    12 \isacommand{theory}\isamarkupfalse%

    13 \ Functions\isanewline

    14 \isakeyword{imports}\ Main\isanewline

    15 \isakeyword{begin}%

    16 \endisatagtheory

    17 {\isafoldtheory}%

    18 %

    19 \isadelimtheory

    20 %

    21 \endisadelimtheory

    22 %

    23 \isamarkupsection{Function Definitions for Dummies%

    24 }

    25 \isamarkuptrue%

    26 %

    27 \begin{isamarkuptext}%

    28 In most cases, defining a recursive function is just as simple as other definitions:%

    29 \end{isamarkuptext}%

    30 \isamarkuptrue%

    31 \isacommand{fun}\isamarkupfalse%

    32 \ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

    33 \isakeyword{where}\isanewline

    34 \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

    35 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

    36 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%

    37 \begin{isamarkuptext}%

    38 The syntax is rather self-explanatory: We introduce a function by

    39   giving its name, its type,

    40   and a set of defining recursive equations.

    41   If we leave out the type, the most general type will be

    42   inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{{\isacharplus}} are overloaded, we would end up

    43   with \isa{fib\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}one{\isacharcomma}plus{\isacharbraceright}}.%

    44 \end{isamarkuptext}%

    45 \isamarkuptrue%

    46 %

    47 \begin{isamarkuptext}%

    48 The function always terminates, since its argument gets smaller in

    49   every recursive call.

    50   Since HOL is a logic of total functions, termination is a

    51   fundamental requirement to prevent inconsistencies\footnote{From the

    52   \qt{definition} \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove

    53   \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.}.

    54   Isabelle tries to prove termination automatically when a definition

    55   is made. In \S\ref{termination}, we will look at cases where this

    56   fails and see what to do then.%

    57 \end{isamarkuptext}%

    58 \isamarkuptrue%

    59 %

    60 \isamarkupsubsection{Pattern matching%

    61 }

    62 \isamarkuptrue%

    63 %

    64 \begin{isamarkuptext}%

    65 \label{patmatch}

    66   Like in functional programming, we can use pattern matching to

    67   define functions. At the moment we will only consider \emph{constructor

    68   patterns}, which only consist of datatype constructors and

    69   variables. Furthermore, patterns must be linear, i.e.\ all variables

    70   on the left hand side of an equation must be distinct. In

    71   \S\ref{genpats} we discuss more general pattern matching.

    73   If patterns overlap, the order of the equations is taken into

    74   account. The following function inserts a fixed element between any

    75   two elements of a list:%

    76 \end{isamarkuptext}%

    77 \isamarkuptrue%

    78 \isacommand{fun}\isamarkupfalse%

    79 \ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline

    80 \isakeyword{where}\isanewline

    81 \ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline

    82 {\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%

    83 \begin{isamarkuptext}%

    84 Overlapping patterns are interpreted as \qt{increments} to what is

    85   already there: The second equation is only meant for the cases where

    86   the first one does not match. Consequently, Isabelle replaces it

    87   internally by the remaining cases, making the patterns disjoint:%

    88 \end{isamarkuptext}%

    89 \isamarkuptrue%

    90 \isacommand{thm}\isamarkupfalse%

    91 \ sep{\isachardot}simps%

    92 \begin{isamarkuptext}%

    93 \begin{isabelle}%

    94 sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}\isasep\isanewline%

    95 sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline%

    96 sep\ a\ {\isacharbrackleft}v{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}v{\isacharbrackright}%

    97 \end{isabelle}%

    98 \end{isamarkuptext}%

    99 \isamarkuptrue%

   100 %

   101 \begin{isamarkuptext}%

   102 \noindent The equations from function definitions are automatically used in

   103   simplification:%

   104 \end{isamarkuptext}%

   105 \isamarkuptrue%

   106 \isacommand{lemma}\isamarkupfalse%

   107 \ {\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

   108 %

   109 \isadelimproof

   110 %

   111 \endisadelimproof

   112 %

   113 \isatagproof

   114 \isacommand{by}\isamarkupfalse%

   115 \ simp%

   116 \endisatagproof

   117 {\isafoldproof}%

   118 %

   119 \isadelimproof

   120 %

   121 \endisadelimproof

   122 %

   123 \isamarkupsubsection{Induction%

   124 }

   125 \isamarkuptrue%

   126 %

   127 \begin{isamarkuptext}%

   128 Isabelle provides customized induction rules for recursive

   129   functions. These rules follow the recursive structure of the

   130   definition. Here is the rule \isa{sep{\isachardot}induct} arising from the

   131   above definition of \isa{sep}:

   133   \begin{isabelle}%

   134 {\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

   135 {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%

   136 \end{isabelle}

   138   We have a step case for list with at least two elements, and two

   139   base cases for the zero- and the one-element list. Here is a simple

   140   proof about \isa{sep} and \isa{map}%

   141 \end{isamarkuptext}%

   142 \isamarkuptrue%

   143 \isacommand{lemma}\isamarkupfalse%

   144 \ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep\ x\ ys{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}map\ f\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline

   145 %

   146 \isadelimproof

   147 %

   148 \endisadelimproof

   149 %

   150 \isatagproof

   151 \isacommand{apply}\isamarkupfalse%

   152 \ {\isacharparenleft}induct\ x\ ys\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%

   153 \begin{isamarkuptxt}%

   154 We get three cases, like in the definition.

   156   \begin{isabelle}%

   157 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ x\ y\ xs{\isachardot}\isanewline

   158 \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

   159 \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

   160 \ {\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

   161 \ {\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}%

   162 \end{isabelle}%

   163 \end{isamarkuptxt}%

   164 \isamarkuptrue%

   165 \isacommand{apply}\isamarkupfalse%

   166 \ auto\ \isanewline

   167 \isacommand{done}\isamarkupfalse%

   168 %

   169 \endisatagproof

   170 {\isafoldproof}%

   171 %

   172 \isadelimproof

   173 %

   174 \endisadelimproof

   175 %

   176 \begin{isamarkuptext}%

   177 With the \cmd{fun} command, you can define about 80\% of the

   178   functions that occur in practice. The rest of this tutorial explains

   179   the remaining 20\%.%

   180 \end{isamarkuptext}%

   181 \isamarkuptrue%

   182 %

   183 \isamarkupsection{fun vs.\ function%

   184 }

   185 \isamarkuptrue%

   186 %

   187 \begin{isamarkuptext}%

   188 The \cmd{fun} command provides a

   189   convenient shorthand notation for simple function definitions. In

   190   this mode, Isabelle tries to solve all the necessary proof obligations

   191   automatically. If any proof fails, the definition is

   192   rejected. This can either mean that the definition is indeed faulty,

   193   or that the default proof procedures are just not smart enough (or

   194   rather: not designed) to handle the definition.

   196   By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or

   197   solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:

   199 \end{isamarkuptext}

   202 \[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}

   203 \cmd{fun} \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%

   204 \cmd{where}\\%

   205 \hspace*{2ex}{\it equations}\\%

   206 \hspace*{2ex}\vdots\vspace*{6pt}

   207 \end{minipage}\right]

   208 \quad\equiv\quad

   209 \left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}

   210 \cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%

   211 \cmd{where}\\%

   212 \hspace*{2ex}{\it equations}\\%

   213 \hspace*{2ex}\vdots\\%

   214 \cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\%

   215 \cmd{termination by} \isa{lexicographic{\isacharunderscore}order}\vspace{6pt}

   216 \end{minipage}

   217 \right]\]

   219 \begin{isamarkuptext}

   220   \vspace*{1em}

   221   \noindent Some details have now become explicit:

   223   \begin{enumerate}

   224   \item The \cmd{sequential} option enables the preprocessing of

   225   pattern overlaps which we already saw. Without this option, the equations

   226   must already be disjoint and complete. The automatic completion only

   227   works with constructor patterns.

   229   \item A function definition produces a proof obligation which

   230   expresses completeness and compatibility of patterns (we talk about

   231   this later). The combination of the methods \isa{pat{\isacharunderscore}completeness} and

   232   \isa{auto} is used to solve this proof obligation.

   234   \item A termination proof follows the definition, started by the

   235   \cmd{termination} command. This will be explained in \S\ref{termination}.

   236  \end{enumerate}

   237   Whenever a \cmd{fun} command fails, it is usually a good idea to

   238   expand the syntax to the more verbose \cmd{function} form, to see

   239   what is actually going on.%

   240 \end{isamarkuptext}%

   241 \isamarkuptrue%

   242 %

   243 \isamarkupsection{Termination%

   244 }

   245 \isamarkuptrue%

   246 %

   247 \begin{isamarkuptext}%

   248 \label{termination}

   249   The method \isa{lexicographic{\isacharunderscore}order} is the default method for

   250   termination proofs. It can prove termination of a

   251   certain class of functions by searching for a suitable lexicographic

   252   combination of size measures. Of course, not all functions have such

   253   a simple termination argument. For them, we can specify the termination

   254   relation manually.%

   255 \end{isamarkuptext}%

   256 \isamarkuptrue%

   257 %

   258 \isamarkupsubsection{The {\tt relation} method%

   259 }

   260 \isamarkuptrue%

   261 %

   262 \begin{isamarkuptext}%

   263 Consider the following function, which sums up natural numbers up to

   264   \isa{N}, using a counter \isa{i}:%

   265 \end{isamarkuptext}%

   266 \isamarkuptrue%

   267 \isacommand{function}\isamarkupfalse%

   268 \ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

   269 \isakeyword{where}\isanewline

   270 \ \ {\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

   271 %

   272 \isadelimproof

   273 %

   274 \endisadelimproof

   275 %

   276 \isatagproof

   277 \isacommand{by}\isamarkupfalse%

   278 \ pat{\isacharunderscore}completeness\ auto%

   279 \endisatagproof

   280 {\isafoldproof}%

   281 %

   282 \isadelimproof

   283 %

   284 \endisadelimproof

   285 %

   286 \begin{isamarkuptext}%

   287 \noindent The \isa{lexicographic{\isacharunderscore}order} method fails on this example, because none of the

   288   arguments decreases in the recursive call, with respect to the standard size ordering.

   289   To prove termination manually, we must provide a custom wellfounded relation.

   291   The termination argument for \isa{sum} is based on the fact that

   292   the \emph{difference} between \isa{i} and \isa{N} gets

   293   smaller in every step, and that the recursion stops when \isa{i}

   294   is greater than \isa{N}. Phrased differently, the expression

   295   \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} always decreases.

   297   We can use this expression as a measure function suitable to prove termination.%

   298 \end{isamarkuptext}%

   299 \isamarkuptrue%

   300 \isacommand{termination}\isamarkupfalse%

   301 \ sum\isanewline

   302 %

   303 \isadelimproof

   304 %

   305 \endisadelimproof

   306 %

   307 \isatagproof

   308 \isacommand{apply}\isamarkupfalse%

   309 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%

   310 \begin{isamarkuptxt}%

   311 The \cmd{termination} command sets up the termination goal for the

   312   specified function \isa{sum}. If the function name is omitted, it

   313   implicitly refers to the last function definition.

   315   The \isa{relation} method takes a relation of

   316   type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of

   317   the function. If the function has multiple curried arguments, then

   318   these are packed together into a tuple, as it happened in the above

   319   example.

   321   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

   322   wellfounded relation from a mapping into the natural numbers (a

   323   \emph{measure function}).

   325   After the invocation of \isa{relation}, we must prove that (a)

   326   the relation we supplied is wellfounded, and (b) that the arguments

   327   of recursive calls indeed decrease with respect to the

   328   relation:

   330   \begin{isabelle}%

   331 \ {\isadigit{1}}{\isachardot}\ wf\ {\isacharparenleft}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isacharparenright}\isanewline

   332 \ {\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}%

   333 \end{isabelle}

   335   These goals are all solved by \isa{auto}:%

   336 \end{isamarkuptxt}%

   337 \isamarkuptrue%

   338 \isacommand{apply}\isamarkupfalse%

   339 \ auto\isanewline

   340 \isacommand{done}\isamarkupfalse%

   341 %

   342 \endisatagproof

   343 {\isafoldproof}%

   344 %

   345 \isadelimproof

   346 %

   347 \endisadelimproof

   348 %

   349 \begin{isamarkuptext}%

   350 Let us complicate the function a little, by adding some more

   351   recursive calls:%

   352 \end{isamarkuptext}%

   353 \isamarkuptrue%

   354 \isacommand{function}\isamarkupfalse%

   355 \ foo\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

   356 \isakeyword{where}\isanewline

   357 \ \ {\isachardoublequoteopen}foo\ i\ N\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isachargreater}\ N\ \isanewline

   358 \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ {\isacharparenleft}if\ N\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ foo\ {\isadigit{0}}\ {\isacharparenleft}N\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline

   359 \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ i\ {\isacharplus}\ foo\ {\isacharparenleft}Suc\ i{\isacharparenright}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline

   360 %

   361 \isadelimproof

   362 %

   363 \endisadelimproof

   364 %

   365 \isatagproof

   366 \isacommand{by}\isamarkupfalse%

   367 \ pat{\isacharunderscore}completeness\ auto%

   368 \endisatagproof

   369 {\isafoldproof}%

   370 %

   371 \isadelimproof

   372 %

   373 \endisadelimproof

   374 %

   375 \begin{isamarkuptext}%

   376 When \isa{i} has reached \isa{N}, it starts at zero again

   377   and \isa{N} is decremented.

   378   This corresponds to a nested

   379   loop where one index counts up and the other down. Termination can

   380   be proved using a lexicographic combination of two measures, namely

   381   the value of \isa{N} and the above difference. The \isa{measures} combinator generalizes \isa{measure} by taking a

   382   list of measure functions.%

   383 \end{isamarkuptext}%

   384 \isamarkuptrue%

   385 \isacommand{termination}\isamarkupfalse%

   386 \ \isanewline

   387 %

   388 \isadelimproof

   389 %

   390 \endisadelimproof

   391 %

   392 \isatagproof

   393 \isacommand{by}\isamarkupfalse%

   394 \ {\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%

   395 \endisatagproof

   396 {\isafoldproof}%

   397 %

   398 \isadelimproof

   399 %

   400 \endisadelimproof

   401 %

   402 \isamarkupsubsection{How \isa{lexicographic{\isacharunderscore}order} works%

   403 }

   404 \isamarkuptrue%

   405 %

   406 \begin{isamarkuptext}%

   407 To see how the automatic termination proofs work, let's look at an

   408   example where it fails\footnote{For a detailed discussion of the

   409   termination prover, see \cite{bulwahnKN07}}:

   411 \end{isamarkuptext}

   412 \cmd{fun} \isa{fails\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%

   413 \cmd{where}\\%

   414 \hspace*{2ex}\isa{{\isachardoublequote}fails\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ a{\isachardoublequote}}\\%

   415 |\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}}\\

   416 \begin{isamarkuptext}

   418 \noindent Isabelle responds with the following error:

   420 \begin{isabelle}

   421 *** Unfinished subgoals:\newline

   422 *** (a, 1, <):\newline

   423 *** \ 1.~\isa{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isadigit{0}}}\newline

   424 *** (a, 1, <=):\newline

   425 *** \ 1.~False\newline

   426 *** (a, 2, <):\newline

   427 *** \ 1.~False\newline

   428 *** Calls:\newline

   429 *** a) \isa{{\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}{\isachargreater}\ {\isacharparenleft}x\ {\isacharplus}\ a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}}\newline

   430 *** Measures:\newline

   431 *** 1) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}fst\ x{\isacharparenright}}\newline

   432 *** 2) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}snd\ x{\isacharparenright}}\newline

   433 *** Result matrix:\newline

   434 *** \ \ \ \ 1\ \ 2  \newline

   435 *** a:  ?   <= \newline

   436 *** Could not find lexicographic termination order.\newline

   437 *** At command "fun".\newline

   438 \end{isabelle}%

   439 \end{isamarkuptext}%

   440 \isamarkuptrue%

   441 %

   442 \begin{isamarkuptext}%

   443 The key to this error message is the matrix at the bottom. The rows

   444   of that matrix correspond to the different recursive calls (In our

   445   case, there is just one). The columns are the function's arguments

   446   (expressed through different measure functions, which map the

   447   argument tuple to a natural number).

   449   The contents of the matrix summarize what is known about argument

   450   descents: The second argument has a weak descent (\isa{{\isacharless}{\isacharequal}}) at the

   451   recursive call, and for the first argument nothing could be proved,

   452   which is expressed by \isa{{\isacharquery}}. In general, there are the values

   453   \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.

   455   For the failed proof attempts, the unfinished subgoals are also

   456   printed. Looking at these will often point to a missing lemma.

   458 %  As a more real example, here is quicksort:%

   459 \end{isamarkuptext}%

   460 \isamarkuptrue%

   461 %

   462 \isamarkupsection{Mutual Recursion%

   463 }

   464 \isamarkuptrue%

   465 %

   466 \begin{isamarkuptext}%

   467 If two or more functions call one another mutually, they have to be defined

   468   in one step. Here are \isa{even} and \isa{odd}:%

   469 \end{isamarkuptext}%

   470 \isamarkuptrue%

   471 \isacommand{function}\isamarkupfalse%

   472 \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

   473 \ \ \ \ \isakeyword{and}\ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

   474 \isakeyword{where}\isanewline

   475 \ \ {\isachardoublequoteopen}even\ {\isadigit{0}}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline

   476 {\isacharbar}\ {\isachardoublequoteopen}odd\ {\isadigit{0}}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline

   477 {\isacharbar}\ {\isachardoublequoteopen}even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ odd\ n{\isachardoublequoteclose}\isanewline

   478 {\isacharbar}\ {\isachardoublequoteopen}odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ even\ n{\isachardoublequoteclose}\isanewline

   479 %

   480 \isadelimproof

   481 %

   482 \endisadelimproof

   483 %

   484 \isatagproof

   485 \isacommand{by}\isamarkupfalse%

   486 \ pat{\isacharunderscore}completeness\ auto%

   487 \endisatagproof

   488 {\isafoldproof}%

   489 %

   490 \isadelimproof

   491 %

   492 \endisadelimproof

   493 %

   494 \begin{isamarkuptext}%

   495 To eliminate the mutual dependencies, Isabelle internally

   496   creates a single function operating on the sum

   497   type \isa{nat\ {\isacharplus}\ nat}. Then, \isa{even} and \isa{odd} are

   498   defined as projections. Consequently, termination has to be proved

   499   simultaneously for both functions, by specifying a measure on the

   500   sum type:%

   501 \end{isamarkuptext}%

   502 \isamarkuptrue%

   503 \isacommand{termination}\isamarkupfalse%

   504 \ \isanewline

   505 %

   506 \isadelimproof

   507 %

   508 \endisadelimproof

   509 %

   510 \isatagproof

   511 \isacommand{by}\isamarkupfalse%

   512 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ case\ x\ of\ Inl\ n\ {\isasymRightarrow}\ n\ {\isacharbar}\ Inr\ n\ {\isasymRightarrow}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%

   513 \endisatagproof

   514 {\isafoldproof}%

   515 %

   516 \isadelimproof

   517 %

   518 \endisadelimproof

   519 %

   520 \begin{isamarkuptext}%

   521 We could also have used \isa{lexicographic{\isacharunderscore}order}, which

   522   supports mutual recursive termination proofs to a certain extent.%

   523 \end{isamarkuptext}%

   524 \isamarkuptrue%

   525 %

   526 \isamarkupsubsection{Induction for mutual recursion%

   527 }

   528 \isamarkuptrue%

   529 %

   530 \begin{isamarkuptext}%

   531 When functions are mutually recursive, proving properties about them

   532   generally requires simultaneous induction. The induction rule \isa{even{\isacharunderscore}odd{\isachardot}induct}

   533   generated from the above definition reflects this.

   535   Let us prove something about \isa{even} and \isa{odd}:%

   536 \end{isamarkuptext}%

   537 \isamarkuptrue%

   538 \isacommand{lemma}\isamarkupfalse%

   539 \ even{\isacharunderscore}odd{\isacharunderscore}mod{\isadigit{2}}{\isacharcolon}\isanewline

   540 \ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

   541 \ \ {\isachardoublequoteopen}odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}%

   542 \isadelimproof

   543 %

   544 \endisadelimproof

   545 %

   546 \isatagproof

   547 %

   548 \begin{isamarkuptxt}%

   549 We apply simultaneous induction, specifying the induction variable

   550   for both goals, separated by \cmd{and}:%

   551 \end{isamarkuptxt}%

   552 \isamarkuptrue%

   553 \isacommand{apply}\isamarkupfalse%

   554 \ {\isacharparenleft}induct\ n\ \isakeyword{and}\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%

   555 \begin{isamarkuptxt}%

   556 We get four subgoals, which correspond to the clauses in the

   557   definition of \isa{even} and \isa{odd}:

   558   \begin{isabelle}%

   559 \ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline

   560 \ {\isadigit{2}}{\isachardot}\ odd\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\isanewline

   561 \ {\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

   562 \ {\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}%

   563 \end{isabelle}

   564   Simplification solves the first two goals, leaving us with two

   565   statements about the \isa{mod} operation to prove:%

   566 \end{isamarkuptxt}%

   567 \isamarkuptrue%

   568 \isacommand{apply}\isamarkupfalse%

   569 \ simp{\isacharunderscore}all%

   570 \begin{isamarkuptxt}%

   571 \begin{isabelle}%

   572 \ {\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

   573 \ {\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}%

   574 \end{isabelle}

   576   \noindent These can be handled by Isabelle's arithmetic decision procedures.%

   577 \end{isamarkuptxt}%

   578 \isamarkuptrue%

   579 \isacommand{apply}\isamarkupfalse%

   580 \ arith\isanewline

   581 \isacommand{apply}\isamarkupfalse%

   582 \ arith\isanewline

   583 \isacommand{done}\isamarkupfalse%

   584 %

   585 \endisatagproof

   586 {\isafoldproof}%

   587 %

   588 \isadelimproof

   589 %

   590 \endisadelimproof

   591 %

   592 \begin{isamarkuptext}%

   593 In proofs like this, the simultaneous induction is really essential:

   594   Even if we are just interested in one of the results, the other

   595   one is necessary to strengthen the induction hypothesis. If we leave

   596   out the statement about \isa{odd} and just write \isa{True} instead,

   597   the same proof fails:%

   598 \end{isamarkuptext}%

   599 \isamarkuptrue%

   600 \isacommand{lemma}\isamarkupfalse%

   601 \ failed{\isacharunderscore}attempt{\isacharcolon}\isanewline

   602 \ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

   603 \ \ {\isachardoublequoteopen}True{\isachardoublequoteclose}\isanewline

   604 %

   605 \isadelimproof

   606 %

   607 \endisadelimproof

   608 %

   609 \isatagproof

   610 \isacommand{apply}\isamarkupfalse%

   611 \ {\isacharparenleft}induct\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%

   612 \begin{isamarkuptxt}%

   613 \noindent Now the third subgoal is a dead end, since we have no

   614   useful induction hypothesis available:

   616   \begin{isabelle}%

   617 \ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline

   618 \ {\isadigit{2}}{\isachardot}\ True\isanewline

   619 \ {\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

   620 \ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ True%

   621 \end{isabelle}%

   622 \end{isamarkuptxt}%

   623 \isamarkuptrue%

   624 \isacommand{oops}\isamarkupfalse%

   625 %

   626 \endisatagproof

   627 {\isafoldproof}%

   628 %

   629 \isadelimproof

   630 %

   631 \endisadelimproof

   632 %

   633 \isamarkupsection{General pattern matching%

   634 }

   635 \isamarkuptrue%

   636 %

   637 \begin{isamarkuptext}%

   638 \label{genpats}%

   639 \end{isamarkuptext}%

   640 \isamarkuptrue%

   641 %

   642 \isamarkupsubsection{Avoiding automatic pattern splitting%

   643 }

   644 \isamarkuptrue%

   645 %

   646 \begin{isamarkuptext}%

   647 Up to now, we used pattern matching only on datatypes, and the

   648   patterns were always disjoint and complete, and if they weren't,

   649   they were made disjoint automatically like in the definition of

   650   \isa{sep} in \S\ref{patmatch}.

   652   This automatic splitting can significantly increase the number of

   653   equations involved, and this is not always desirable. The following

   654   example shows the problem:

   656   Suppose we are modeling incomplete knowledge about the world by a

   657   three-valued datatype, which has values \isa{T}, \isa{F}

   658   and \isa{X} for true, false and uncertain propositions, respectively.%

   659 \end{isamarkuptext}%

   660 \isamarkuptrue%

   661 \isacommand{datatype}\isamarkupfalse%

   662 \ P{\isadigit{3}}\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ X%

   663 \begin{isamarkuptext}%

   664 \noindent Then the conjunction of such values can be defined as follows:%

   665 \end{isamarkuptext}%

   666 \isamarkuptrue%

   667 \isacommand{fun}\isamarkupfalse%

   668 \ And\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline

   669 \isakeyword{where}\isanewline

   670 \ \ {\isachardoublequoteopen}And\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline

   671 {\isacharbar}\ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline

   672 {\isacharbar}\ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline

   673 {\isacharbar}\ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline

   674 {\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%

   675 \begin{isamarkuptext}%

   676 This definition is useful, because the equations can directly be used

   677   as simplification rules. But the patterns overlap: For example,

   678   the expression \isa{And\ T\ T} is matched by both the first and

   679   the second equation. By default, Isabelle makes the patterns disjoint by

   680   splitting them up, producing instances:%

   681 \end{isamarkuptext}%

   682 \isamarkuptrue%

   683 \isacommand{thm}\isamarkupfalse%

   684 \ And{\isachardot}simps%

   685 \begin{isamarkuptext}%

   686 \isa{And\ T\ {\isacharquery}p\ {\isacharequal}\ {\isacharquery}p\isasep\isanewline%

   687 And\ F\ T\ {\isacharequal}\ F\isasep\isanewline%

   688 And\ X\ T\ {\isacharequal}\ X\isasep\isanewline%

   689 And\ F\ F\ {\isacharequal}\ F\isasep\isanewline%

   690 And\ X\ F\ {\isacharequal}\ F\isasep\isanewline%

   691 And\ F\ X\ {\isacharequal}\ F\isasep\isanewline%

   692 And\ X\ X\ {\isacharequal}\ X}

   694   \vspace*{1em}

   695   \noindent There are several problems with this:

   697   \begin{enumerate}

   698   \item If the datatype has many constructors, there can be an

   699   explosion of equations. For \isa{And}, we get seven instead of

   700   five equations, which can be tolerated, but this is just a small

   701   example.

   703   \item Since splitting makes the equations \qt{less general}, they

   704   do not always match in rewriting. While the term \isa{And\ x\ F}

   705   can be simplified to \isa{F} with the original equations, a

   706   (manual) case split on \isa{x} is now necessary.

   708   \item The splitting also concerns the induction rule \isa{And{\isachardot}induct}. Instead of five premises it now has seven, which

   709   means that our induction proofs will have more cases.

   711   \item In general, it increases clarity if we get the same definition

   712   back which we put in.

   713   \end{enumerate}

   715   If we do not want the automatic splitting, we can switch it off by

   716   leaving out the \cmd{sequential} option. However, we will have to

   717   prove that our pattern matching is consistent\footnote{This prevents

   718   us from defining something like \isa{f\ x\ {\isacharequal}\ True} and \isa{f\ x\ {\isacharequal}\ False} simultaneously.}:%

   719 \end{isamarkuptext}%

   720 \isamarkuptrue%

   721 \isacommand{function}\isamarkupfalse%

   722 \ And{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline

   723 \isakeyword{where}\isanewline

   724 \ \ {\isachardoublequoteopen}And{\isadigit{2}}\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline

   725 {\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline

   726 {\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline

   727 {\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline

   728 {\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%

   729 \isadelimproof

   730 %

   731 \endisadelimproof

   732 %

   733 \isatagproof

   734 %

   735 \begin{isamarkuptxt}%

   736 \noindent Now let's look at the proof obligations generated by a

   737   function definition. In this case, they are:

   739   \begin{isabelle}%

   740 \ {\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

   741 \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

   742 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ }{\isasymLongrightarrow}\ P\isanewline

   743 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline

   744 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline

   745 \ {\isadigit{4}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline

   746 \ {\isadigit{5}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline

   747 \ {\isadigit{6}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X\isanewline

   748 \ {\isadigit{7}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline

   749 \ {\isadigit{8}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline

   750 \ {\isadigit{9}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline

   751 \ {\isadigit{1}}{\isadigit{0}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X%

   752 \end{isabelle}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}

   754   The first subgoal expresses the completeness of the patterns. It has

   755   the form of an elimination rule and states that every \isa{x} of

   756   the function's input type must match at least one of the patterns\footnote{Completeness could

   757   be equivalently stated as a disjunction of existential statements:

   758 \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

   759   datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness}

   760   method:%

   761 \end{isamarkuptxt}%

   762 \isamarkuptrue%

   763 \isacommand{apply}\isamarkupfalse%

   764 \ pat{\isacharunderscore}completeness%

   765 \begin{isamarkuptxt}%

   766 The remaining subgoals express \emph{pattern compatibility}. We do

   767   allow that an input value matches multiple patterns, but in this

   768   case, the result (i.e.~the right hand sides of the equations) must

   769   also be equal. For each pair of two patterns, there is one such

   770   subgoal. Usually this needs injectivity of the constructors, which

   771   is used automatically by \isa{auto}.%

   772 \end{isamarkuptxt}%

   773 \isamarkuptrue%

   774 \isacommand{by}\isamarkupfalse%

   775 \ auto%

   776 \endisatagproof

   777 {\isafoldproof}%

   778 %

   779 \isadelimproof

   780 %

   781 \endisadelimproof

   782 %

   783 \isamarkupsubsection{Non-constructor patterns%

   784 }

   785 \isamarkuptrue%

   786 %

   787 \begin{isamarkuptext}%

   788 Most of Isabelle's basic types take the form of inductive datatypes,

   789   and usually pattern matching works on the constructors of such types.

   790   However, this need not be always the case, and the \cmd{function}

   791   command handles other kind of patterns, too.

   793   One well-known instance of non-constructor patterns are

   794   so-called \emph{$n+k$-patterns}, which are a little controversial in

   795   the functional programming world. Here is the initial fibonacci

   796   example with $n+k$-patterns:%

   797 \end{isamarkuptext}%

   798 \isamarkuptrue%

   799 \isacommand{function}\isamarkupfalse%

   800 \ fib{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

   801 \isakeyword{where}\isanewline

   802 \ \ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

   803 {\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

   804 {\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

   805 %

   806 \isadelimML

   807 %

   808 \endisadelimML

   809 %

   810 \isatagML

   811 %

   812 \endisatagML

   813 {\isafoldML}%

   814 %

   815 \isadelimML

   816 %

   817 \endisadelimML

   818 %

   819 \isadelimproof

   820 %

   821 \endisadelimproof

   822 %

   823 \isatagproof

   824 %

   825 \begin{isamarkuptxt}%

   826 This kind of matching is again justified by the proof of pattern

   827   completeness and compatibility.

   828   The proof obligation for pattern completeness states that every natural number is

   829   either \isa{{\isadigit{0}}}, \isa{{\isadigit{1}}} or \isa{n\ {\isacharplus}\ {\isadigit{2}}}:

   831   \begin{isabelle}%

   832 \ {\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

   833 \ {\isadigit{2}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline

   834 \ {\isadigit{3}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline

   835 \ {\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

   836 \ {\isadigit{5}}{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline

   837 \ {\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

   838 \ {\isadigit{7}}{\isachardot}\ {\isasymAnd}n\ na{\isachardot}\isanewline

   839 \isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ na\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\isanewline

   840 \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}%

   841 \end{isabelle}

   843   This is an arithmetic triviality, but unfortunately the

   844   \isa{arith} method cannot handle this specific form of an

   845   elimination rule. However, we can use the method \isa{atomize{\isacharunderscore}elim} to do an ad-hoc conversion to a disjunction of

   846   existentials, which can then be solved by the arithmetic decision procedure.

   847   Pattern compatibility and termination are automatic as usual.%

   848 \end{isamarkuptxt}%

   849 \isamarkuptrue%

   850 %

   851 \endisatagproof

   852 {\isafoldproof}%

   853 %

   854 \isadelimproof

   855 %

   856 \endisadelimproof

   857 %

   858 \isadelimML

   859 %

   860 \endisadelimML

   861 %

   862 \isatagML

   863 %

   864 \endisatagML

   865 {\isafoldML}%

   866 %

   867 \isadelimML

   868 %

   869 \endisadelimML

   870 %

   871 \isadelimproof

   872 %

   873 \endisadelimproof

   874 %

   875 \isatagproof

   876 \isacommand{apply}\isamarkupfalse%

   877 \ atomize{\isacharunderscore}elim\isanewline

   878 \isacommand{apply}\isamarkupfalse%

   879 \ arith\isanewline

   880 \isacommand{apply}\isamarkupfalse%

   881 \ auto\isanewline

   882 \isacommand{done}\isamarkupfalse%

   883 %

   884 \endisatagproof

   885 {\isafoldproof}%

   886 %

   887 \isadelimproof

   888 %

   889 \endisadelimproof

   890 \isanewline

   891 \isacommand{termination}\isamarkupfalse%

   892 %

   893 \isadelimproof

   894 \ %

   895 \endisadelimproof

   896 %

   897 \isatagproof

   898 \isacommand{by}\isamarkupfalse%

   899 \ lexicographic{\isacharunderscore}order%

   900 \endisatagproof

   901 {\isafoldproof}%

   902 %

   903 \isadelimproof

   904 %

   905 \endisadelimproof

   906 %

   907 \begin{isamarkuptext}%

   908 We can stretch the notion of pattern matching even more. The

   909   following function is not a sensible functional program, but a

   910   perfectly valid mathematical definition:%

   911 \end{isamarkuptext}%

   912 \isamarkuptrue%

   913 \isacommand{function}\isamarkupfalse%

   914 \ ev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

   915 \isakeyword{where}\isanewline

   916 \ \ {\isachardoublequoteopen}ev\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline

   917 {\isacharbar}\ {\isachardoublequoteopen}ev\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline

   918 %

   919 \isadelimproof

   920 %

   921 \endisadelimproof

   922 %

   923 \isatagproof

   924 \isacommand{apply}\isamarkupfalse%

   925 \ atomize{\isacharunderscore}elim\isanewline

   926 \isacommand{by}\isamarkupfalse%

   927 \ arith{\isacharplus}%

   928 \endisatagproof

   929 {\isafoldproof}%

   930 %

   931 \isadelimproof

   932 \isanewline

   933 %

   934 \endisadelimproof

   935 \isacommand{termination}\isamarkupfalse%

   936 %

   937 \isadelimproof

   938 \ %

   939 \endisadelimproof

   940 %

   941 \isatagproof

   942 \isacommand{by}\isamarkupfalse%

   943 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ simp%

   944 \endisatagproof

   945 {\isafoldproof}%

   946 %

   947 \isadelimproof

   948 %

   949 \endisadelimproof

   950 %

   951 \begin{isamarkuptext}%

   952 This general notion of pattern matching gives you a certain freedom

   953   in writing down specifications. However, as always, such freedom should

   954   be used with care:

   956   If we leave the area of constructor

   957   patterns, we have effectively departed from the world of functional

   958   programming. This means that it is no longer possible to use the

   959   code generator, and expect it to generate ML code for our

   960   definitions. Also, such a specification might not work very well together with

   961   simplification. Your mileage may vary.%

   962 \end{isamarkuptext}%

   963 \isamarkuptrue%

   964 %

   965 \isamarkupsubsection{Conditional equations%

   966 }

   967 \isamarkuptrue%

   968 %

   969 \begin{isamarkuptext}%

   970 The function package also supports conditional equations, which are

   971   similar to guards in a language like Haskell. Here is Euclid's

   972   algorithm written with conditional patterns\footnote{Note that the

   973   patterns are also overlapping in the base case}:%

   974 \end{isamarkuptext}%

   975 \isamarkuptrue%

   976 \isacommand{function}\isamarkupfalse%

   977 \ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

   978 \isakeyword{where}\isanewline

   979 \ \ {\isachardoublequoteopen}gcd\ x\ {\isadigit{0}}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline

   980 {\isacharbar}\ {\isachardoublequoteopen}gcd\ {\isadigit{0}}\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline

   981 {\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

   982 {\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

   983 %

   984 \isadelimproof

   985 %

   986 \endisadelimproof

   987 %

   988 \isatagproof

   989 \isacommand{by}\isamarkupfalse%

   990 \ {\isacharparenleft}atomize{\isacharunderscore}elim{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}%

   991 \endisatagproof

   992 {\isafoldproof}%

   993 %

   994 \isadelimproof

   995 \isanewline

   996 %

   997 \endisadelimproof

   998 \isacommand{termination}\isamarkupfalse%

   999 %

  1000 \isadelimproof

  1001 \ %

  1002 \endisadelimproof

  1003 %

  1004 \isatagproof

  1005 \isacommand{by}\isamarkupfalse%

  1006 \ lexicographic{\isacharunderscore}order%

  1007 \endisatagproof

  1008 {\isafoldproof}%

  1009 %

  1010 \isadelimproof

  1011 %

  1012 \endisadelimproof

  1013 %

  1014 \begin{isamarkuptext}%

  1015 By now, you can probably guess what the proof obligations for the

  1016   pattern completeness and compatibility look like.

  1018   Again, functions with conditional patterns are not supported by the

  1019   code generator.%

  1020 \end{isamarkuptext}%

  1021 \isamarkuptrue%

  1022 %

  1023 \isamarkupsubsection{Pattern matching on strings%

  1024 }

  1025 \isamarkuptrue%

  1026 %

  1027 \begin{isamarkuptext}%

  1028 As strings (as lists of characters) are normal datatypes, pattern

  1029   matching on them is possible, but somewhat problematic. Consider the

  1030   following definition:

  1032 \end{isamarkuptext}

  1033 \noindent\cmd{fun} \isa{check\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}string\ {\isasymRightarrow}\ bool{\isachardoublequote}}\\%

  1034 \cmd{where}\\%

  1035 \hspace*{2ex}\isa{{\isachardoublequote}check\ {\isacharparenleft}{\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}}\\%

  1036 \isa{{\isacharbar}\ {\isachardoublequote}check\ s\ {\isacharequal}\ False{\isachardoublequote}}

  1037 \begin{isamarkuptext}

  1039   \noindent An invocation of the above \cmd{fun} command does not

  1040   terminate. What is the problem? Strings are lists of characters, and

  1041   characters are a datatype with a lot of constructors. Splitting the

  1042   catch-all pattern thus leads to an explosion of cases, which cannot

  1043   be handled by Isabelle.

  1045   There are two things we can do here. Either we write an explicit

  1046   \isa{if} on the right hand side, or we can use conditional patterns:%

  1047 \end{isamarkuptext}%

  1048 \isamarkuptrue%

  1049 \isacommand{function}\isamarkupfalse%

  1050 \ check\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}string\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

  1051 \isakeyword{where}\isanewline

  1052 \ \ {\isachardoublequoteopen}check\ {\isacharparenleft}{\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline

  1053 {\isacharbar}\ {\isachardoublequoteopen}s\ {\isasymnoteq}\ {\isacharprime}{\isacharprime}good{\isacharprime}{\isacharprime}\ {\isasymLongrightarrow}\ check\ s\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline

  1054 %

  1055 \isadelimproof

  1056 %

  1057 \endisadelimproof

  1058 %

  1059 \isatagproof

  1060 \isacommand{by}\isamarkupfalse%

  1061 \ auto%

  1062 \endisatagproof

  1063 {\isafoldproof}%

  1064 %

  1065 \isadelimproof

  1066 %

  1067 \endisadelimproof

  1068 %

  1069 \isamarkupsection{Partiality%

  1070 }

  1071 \isamarkuptrue%

  1072 %

  1073 \begin{isamarkuptext}%

  1074 In HOL, all functions are total. A function \isa{f} applied to

  1075   \isa{x} always has the value \isa{f\ x}, and there is no notion

  1076   of undefinedness.

  1077   This is why we have to do termination

  1078   proofs when defining functions: The proof justifies that the

  1079   function can be defined by wellfounded recursion.

  1081   However, the \cmd{function} package does support partiality to a

  1082   certain extent. Let's look at the following function which looks

  1083   for a zero of a given function f.%

  1084 \end{isamarkuptext}%

  1085 \isamarkuptrue%

  1086 \isacommand{function}\isamarkupfalse%

  1087 \ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

  1088 \isakeyword{where}\isanewline

  1089 \ \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ {\isacharparenleft}if\ f\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1090 %

  1091 \isadelimproof

  1092 %

  1093 \endisadelimproof

  1094 %

  1095 \isatagproof

  1096 \isacommand{by}\isamarkupfalse%

  1097 \ pat{\isacharunderscore}completeness\ auto%

  1098 \endisatagproof

  1099 {\isafoldproof}%

  1100 %

  1101 \isadelimproof

  1102 %

  1103 \endisadelimproof

  1104 %

  1105 \begin{isamarkuptext}%

  1106 \noindent Clearly, any attempt of a termination proof must fail. And without

  1107   that, we do not get the usual rules \isa{findzero{\isachardot}simp} and

  1108   \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%

  1109 \end{isamarkuptext}%

  1110 \isamarkuptrue%

  1111 %

  1112 \isamarkupsubsection{Domain predicates%

  1113 }

  1114 \isamarkuptrue%

  1115 %

  1116 \begin{isamarkuptext}%

  1117 The trick is that Isabelle has not only defined the function \isa{findzero}, but also

  1118   a predicate \isa{findzero{\isacharunderscore}dom} that characterizes the values where the function

  1119   terminates: the \emph{domain} of the function. If we treat a

  1120   partial function just as a total function with an additional domain

  1121   predicate, we can derive simplification and

  1122   induction rules as we do for total functions. They are guarded

  1123   by domain conditions and are called \isa{psimps} and \isa{pinduct}:%

  1124 \end{isamarkuptext}%

  1125 \isamarkuptrue%

  1126 %

  1127 \begin{isamarkuptext}%

  1128 \noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}%

  1129 findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline

  1130 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}%

  1131 \end{isabelle}\end{minipage}

  1132   \hfill(\isa{findzero{\isachardot}psimps})

  1133   \vspace{1em}

  1135   \noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}%

  1136 {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline

  1137 \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

  1138 {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%

  1139 \end{isabelle}\end{minipage}

  1140   \hfill(\isa{findzero{\isachardot}pinduct})%

  1141 \end{isamarkuptext}%

  1142 \isamarkuptrue%

  1143 %

  1144 \begin{isamarkuptext}%

  1145 Remember that all we

  1146   are doing here is use some tricks to make a total function appear

  1147   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

  1148   to some natural number, although we might not be able to find out

  1149   which one. The function is \emph{underdefined}.

  1151   But it is defined enough to prove something interesting about it. We

  1152   can prove that if \isa{findzero\ f\ n}

  1153   terminates, it indeed returns a zero of \isa{f}:%

  1154 \end{isamarkuptext}%

  1155 \isamarkuptrue%

  1156 \isacommand{lemma}\isamarkupfalse%

  1157 \ findzero{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%

  1158 \isadelimproof

  1159 %

  1160 \endisadelimproof

  1161 %

  1162 \isatagproof

  1163 %

  1164 \begin{isamarkuptxt}%

  1165 \noindent We apply induction as usual, but using the partial induction

  1166   rule:%

  1167 \end{isamarkuptxt}%

  1168 \isamarkuptrue%

  1169 \isacommand{apply}\isamarkupfalse%

  1170 \ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}%

  1171 \begin{isamarkuptxt}%

  1172 \noindent This gives the following subgoals:

  1174   \begin{isabelle}%

  1175 \ {\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

  1176 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}%

  1177 \end{isabelle}

  1179   \noindent The hypothesis in our lemma was used to satisfy the first premise in

  1180   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

  1181   allows to unfold \isa{findzero\ f\ n} using the \isa{psimps}

  1182   rule, and the rest is trivial. Since the \isa{psimps} rules carry the

  1183   \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:%

  1184 \end{isamarkuptxt}%

  1185 \isamarkuptrue%

  1186 \isacommand{apply}\isamarkupfalse%

  1187 \ simp\isanewline

  1188 \isacommand{done}\isamarkupfalse%

  1189 %

  1190 \endisatagproof

  1191 {\isafoldproof}%

  1192 %

  1193 \isadelimproof

  1194 %

  1195 \endisadelimproof

  1196 %

  1197 \begin{isamarkuptext}%

  1198 Proofs about partial functions are often not harder than for total

  1199   functions. Fig.~\ref{findzero_isar} shows a slightly more

  1200   complicated proof written in Isar. It is verbose enough to show how

  1201   partiality comes into play: From the partial induction, we get an

  1202   additional domain condition hypothesis. Observe how this condition

  1203   is applied when calls to \isa{findzero} are unfolded.%

  1204 \end{isamarkuptext}%

  1205 \isamarkuptrue%

  1206 %

  1207 \begin{figure}

  1208 \hrule\vspace{6pt}

  1209 \begin{minipage}{0.8\textwidth}

  1210 \isabellestyle{it}

  1211 \isastyle\isamarkuptrue

  1212 \isacommand{lemma}\isamarkupfalse%

  1213 \ {\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

  1214 %

  1215 \isadelimproof

  1216 %

  1217 \endisadelimproof

  1218 %

  1219 \isatagproof

  1220 \isacommand{proof}\isamarkupfalse%

  1221 \ {\isacharparenleft}induct\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}\isanewline

  1222 \ \ \isacommand{fix}\isamarkupfalse%

  1223 \ f\ n\ \isacommand{assume}\isamarkupfalse%

  1224 \ dom{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1225 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \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

  1226 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isakeyword{and}\ x{\isacharunderscore}range{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline

  1227 \ \ \isacommand{have}\isamarkupfalse%

  1228 \ {\isachardoublequoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1229 \ \ \isacommand{proof}\isamarkupfalse%

  1230 \ \isanewline

  1231 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1232 \ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1233 \ \ \ \ \isacommand{with}\isamarkupfalse%

  1234 \ dom\ \isacommand{have}\isamarkupfalse%

  1235 \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1236 \ simp\isanewline

  1237 \ \ \ \ \isacommand{with}\isamarkupfalse%

  1238 \ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse%

  1239 \ False\ \isacommand{by}\isamarkupfalse%

  1240 \ auto\isanewline

  1241 \ \ \isacommand{qed}\isamarkupfalse%

  1242 \isanewline

  1243 \ \ \isanewline

  1244 \ \ \isacommand{from}\isamarkupfalse%

  1245 \ x{\isacharunderscore}range\ \isacommand{have}\isamarkupfalse%

  1246 \ {\isachardoublequoteopen}x\ {\isacharequal}\ n\ {\isasymor}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1247 \ auto\isanewline

  1248 \ \ \isacommand{thus}\isamarkupfalse%

  1249 \ {\isachardoublequoteopen}f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1250 \ \ \isacommand{proof}\isamarkupfalse%

  1251 \isanewline

  1252 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1253 \ {\isachardoublequoteopen}x\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline

  1254 \ \ \ \ \isacommand{with}\isamarkupfalse%

  1255 \ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%

  1256 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%

  1257 \ simp\isanewline

  1258 \ \ \isacommand{next}\isamarkupfalse%

  1259 \isanewline

  1260 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1261 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline

  1262 \ \ \ \ \isacommand{with}\isamarkupfalse%

  1263 \ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%

  1264 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1265 \ simp\isanewline

  1266 \ \ \ \ \isacommand{with}\isamarkupfalse%

  1267 \ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline

  1268 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1269 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%

  1270 \ simp\isanewline

  1271 \ \ \isacommand{qed}\isamarkupfalse%

  1272 \isanewline

  1273 \isacommand{qed}\isamarkupfalse%

  1274 %

  1275 \endisatagproof

  1276 {\isafoldproof}%

  1277 %

  1278 \isadelimproof

  1279 %

  1280 \endisadelimproof

  1281 %

  1282 \isamarkupfalse\isabellestyle{tt}

  1283 \end{minipage}\vspace{6pt}\hrule

  1284 \caption{A proof about a partial function}\label{findzero_isar}

  1285 \end{figure}

  1286 %

  1287 \isamarkupsubsection{Partial termination proofs%

  1288 }

  1289 \isamarkuptrue%

  1290 %

  1291 \begin{isamarkuptext}%

  1292 Now that we have proved some interesting properties about our

  1293   function, we should turn to the domain predicate and see if it is

  1294   actually true for some values. Otherwise we would have just proved

  1295   lemmas with \isa{False} as a premise.

  1297   Essentially, we need some introduction rules for \isa{findzero{\isacharunderscore}dom}. The function package can prove such domain

  1298   introduction rules automatically. But since they are not used very

  1299   often (they are almost never needed if the function is total), this

  1300   functionality is disabled by default for efficiency reasons. So we have to go

  1301   back and ask for them explicitly by passing the \isa{{\isacharparenleft}domintros{\isacharparenright}} option to the function package:

  1303 \vspace{1ex}

  1304 \noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%

  1305 \cmd{where}\isanewline%

  1306 \ \ \ldots\\

  1308   \noindent Now the package has proved an introduction rule for \isa{findzero{\isacharunderscore}dom}:%

  1309 \end{isamarkuptext}%

  1310 \isamarkuptrue%

  1311 \isacommand{thm}\isamarkupfalse%

  1312 \ findzero{\isachardot}domintros%

  1313 \begin{isamarkuptext}%

  1314 \begin{isabelle}%

  1315 {\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}%

  1316 \end{isabelle}

  1318   Domain introduction rules allow to show that a given value lies in the

  1319   domain of a function, if the arguments of all recursive calls

  1320   are in the domain as well. They allow to do a \qt{single step} in a

  1321   termination proof. Usually, you want to combine them with a suitable

  1322   induction principle.

  1324   Since our function increases its argument at recursive calls, we

  1325   need an induction principle which works \qt{backwards}. We will use

  1326   \isa{inc{\isacharunderscore}induct}, which allows to do induction from a fixed number

  1327   \qt{downwards}:

  1329   \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}

  1331   Figure \ref{findzero_term} gives a detailed Isar proof of the fact

  1332   that \isa{findzero} terminates if there is a zero which is greater

  1333   or equal to \isa{n}. First we derive two useful rules which will

  1334   solve the base case and the step case of the induction. The

  1335   induction is then straightforward, except for the unusual induction

  1336   principle.%

  1337 \end{isamarkuptext}%

  1338 \isamarkuptrue%

  1339 %

  1340 \begin{figure}

  1341 \hrule\vspace{6pt}

  1342 \begin{minipage}{0.8\textwidth}

  1343 \isabellestyle{it}

  1344 \isastyle\isamarkuptrue

  1345 \isacommand{lemma}\isamarkupfalse%

  1346 \ findzero{\isacharunderscore}termination{\isacharcolon}\isanewline

  1347 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isasymge}\ n{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1348 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1349 %

  1350 \isadelimproof

  1351 %

  1352 \endisadelimproof

  1353 %

  1354 \isatagproof

  1355 \isacommand{proof}\isamarkupfalse%

  1356 \ {\isacharminus}\ \isanewline

  1357 \ \ \isacommand{have}\isamarkupfalse%

  1358 \ base{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1359 \ \ \ \ \isacommand{by}\isamarkupfalse%

  1360 \ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}{\isacharbackquoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline

  1361 \isanewline

  1362 \ \ \isacommand{have}\isamarkupfalse%

  1363 \ step{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i{\isachardot}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}\ \isanewline

  1364 \ \ \ \ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1365 \ \ \ \ \isacommand{by}\isamarkupfalse%

  1366 \ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ simp\isanewline

  1367 \isanewline

  1368 \ \ \isacommand{from}\isamarkupfalse%

  1369 \ {\isacharbackquoteopen}x\ {\isasymge}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%

  1370 \ {\isacharquery}thesis\isanewline

  1371 \ \ \isacommand{proof}\isamarkupfalse%

  1372 \ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\isanewline

  1373 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1374 \ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1375 \ {\isacharparenleft}rule\ base{\isacharparenright}\isanewline

  1376 \ \ \isacommand{next}\isamarkupfalse%

  1377 \isanewline

  1378 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1379 \ i\ \isacommand{assume}\isamarkupfalse%

  1380 \ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1381 \ \ \ \ \isacommand{thus}\isamarkupfalse%

  1382 \ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1383 \ {\isacharparenleft}rule\ step{\isacharparenright}\isanewline

  1384 \ \ \isacommand{qed}\isamarkupfalse%

  1385 \isanewline

  1386 \isacommand{qed}\isamarkupfalse%

  1387 %

  1388 \endisatagproof

  1389 {\isafoldproof}%

  1390 %

  1391 \isadelimproof

  1392 %

  1393 \endisadelimproof

  1394 %

  1395 \isamarkupfalse\isabellestyle{tt}

  1396 \end{minipage}\vspace{6pt}\hrule

  1397 \caption{Termination proof for \isa{findzero}}\label{findzero_term}

  1398 \end{figure}

  1399 %

  1400 \begin{isamarkuptext}%

  1401 Again, the proof given in Fig.~\ref{findzero_term} has a lot of

  1402   detail in order to explain the principles. Using more automation, we

  1403   can also have a short proof:%

  1404 \end{isamarkuptext}%

  1405 \isamarkuptrue%

  1406 \isacommand{lemma}\isamarkupfalse%

  1407 \ findzero{\isacharunderscore}termination{\isacharunderscore}short{\isacharcolon}\isanewline

  1408 \ \ \isakeyword{assumes}\ zero{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline

  1409 \ \ \isakeyword{assumes}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1410 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1411 %

  1412 \isadelimproof

  1413 %

  1414 \endisadelimproof

  1415 %

  1416 \isatagproof

  1417 \isacommand{using}\isamarkupfalse%

  1418 \ zero\isanewline

  1419 \isacommand{by}\isamarkupfalse%

  1420 \ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}%

  1421 \endisatagproof

  1422 {\isafoldproof}%

  1423 %

  1424 \isadelimproof

  1425 %

  1426 \endisadelimproof

  1427 %

  1428 \begin{isamarkuptext}%

  1429 \noindent It is simple to combine the partial correctness result with the

  1430   termination lemma:%

  1431 \end{isamarkuptext}%

  1432 \isamarkuptrue%

  1433 \isacommand{lemma}\isamarkupfalse%

  1434 \ findzero{\isacharunderscore}total{\isacharunderscore}correctness{\isacharcolon}\isanewline

  1435 \ \ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1436 %

  1437 \isadelimproof

  1438 %

  1439 \endisadelimproof

  1440 %

  1441 \isatagproof

  1442 \isacommand{by}\isamarkupfalse%

  1443 \ {\isacharparenleft}blast\ intro{\isacharcolon}\ findzero{\isacharunderscore}zero\ findzero{\isacharunderscore}termination{\isacharparenright}%

  1444 \endisatagproof

  1445 {\isafoldproof}%

  1446 %

  1447 \isadelimproof

  1448 %

  1449 \endisadelimproof

  1450 %

  1451 \isamarkupsubsection{Definition of the domain predicate%

  1452 }

  1453 \isamarkuptrue%

  1454 %

  1455 \begin{isamarkuptext}%

  1456 Sometimes it is useful to know what the definition of the domain

  1457   predicate looks like. Actually, \isa{findzero{\isacharunderscore}dom} is just an

  1458   abbreviation:

  1460   \begin{isabelle}%

  1461 findzero{\isacharunderscore}dom\ {\isasymequiv}\ accp\ findzero{\isacharunderscore}rel%

  1462 \end{isabelle}

  1464   The domain predicate is the \emph{accessible part} of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function

  1465   package. \isa{findzero{\isacharunderscore}rel} is just a normal

  1466   inductive predicate, so we can inspect its definition by

  1467   looking at the introduction rules \isa{findzero{\isacharunderscore}rel{\isachardot}intros}.

  1468   In our case there is just a single rule:

  1470   \begin{isabelle}%

  1471 {\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}%

  1472 \end{isabelle}

  1474   The predicate \isa{findzero{\isacharunderscore}rel}

  1475   describes the \emph{recursion relation} of the function

  1476   definition. The recursion relation is a binary relation on

  1477   the arguments of the function that relates each argument to its

  1478   recursive calls. In general, there is one introduction rule for each

  1479   recursive call.

  1481   The predicate \isa{findzero{\isacharunderscore}dom} is the accessible part of

  1482   that relation. An argument belongs to the accessible part, if it can

  1483   be reached in a finite number of steps (cf.~its definition in \isa{Accessible{\isacharunderscore}Part{\isachardot}thy}).

  1485   Since the domain predicate is just an abbreviation, you can use

  1486   lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some

  1487   lemmas which are occasionally useful are \isa{accpI}, \isa{accp{\isacharunderscore}downward}, and of course the introduction and elimination rules

  1488   for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.%

  1489 \end{isamarkuptext}%

  1490 \isamarkuptrue%

  1491 %

  1492 \isamarkupsubsection{A Useful Special Case: Tail recursion%

  1493 }

  1494 \isamarkuptrue%

  1495 %

  1496 \begin{isamarkuptext}%

  1497 The domain predicate is our trick that allows us to model partiality

  1498   in a world of total functions. The downside of this is that we have

  1499   to carry it around all the time. The termination proof above allowed

  1500   us to replace the abstract \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} by the more

  1501   concrete \isa{n\ {\isasymle}\ x\ {\isasymand}\ f\ x\ {\isacharequal}\ {\isadigit{0}}}, but the condition is still

  1502   there and can only be discharged for special cases.

  1503   In particular, the domain predicate guards the unfolding of our

  1504   function, since it is there as a condition in the \isa{psimp}

  1505   rules.

  1507   Now there is an important special case: We can actually get rid

  1508   of the condition in the simplification rules, \emph{if the function

  1509   is tail-recursive}. The reason is that for all tail-recursive

  1510   equations there is a total function satisfying them, even if they

  1511   are non-terminating.

  1513 %  A function is tail recursive, if each call to the function is either

  1514 %  equal

  1515 %

  1516 %  So the outer form of the

  1517 %

  1518 %if it can be written in the following

  1519 %  form:

  1520 %  {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}

  1523   The function package internally does the right construction and can

  1524   derive the unconditional simp rules, if we ask it to do so. Luckily,

  1525   our \isa{findzero} function is tail-recursive, so we can just go

  1526   back and add another option to the \cmd{function} command:

  1528 \vspace{1ex}

  1529 \noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharcomma}\ tailrec{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%

  1530 \cmd{where}\isanewline%

  1531 \ \ \ldots\\%

  1534   \noindent Now, we actually get unconditional simplification rules, even

  1535   though the function is partial:%

  1536 \end{isamarkuptext}%

  1537 \isamarkuptrue%

  1538 \isacommand{thm}\isamarkupfalse%

  1539 \ findzero{\isachardot}simps%

  1540 \begin{isamarkuptext}%

  1541 \begin{isabelle}%

  1542 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}%

  1543 \end{isabelle}

  1545   \noindent Of course these would make the simplifier loop, so we better remove

  1546   them from the simpset:%

  1547 \end{isamarkuptext}%

  1548 \isamarkuptrue%

  1549 \isacommand{declare}\isamarkupfalse%

  1550 \ findzero{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%

  1551 \begin{isamarkuptext}%

  1552 Getting rid of the domain conditions in the simplification rules is

  1553   not only useful because it simplifies proofs. It is also required in

  1554   order to use Isabelle's code generator to generate ML code

  1555   from a function definition.

  1556   Since the code generator only works with equations, it cannot be

  1557   used with \isa{psimp} rules. Thus, in order to generate code for

  1558   partial functions, they must be defined as a tail recursion.

  1559   Luckily, many functions have a relatively natural tail recursive

  1560   definition.%

  1561 \end{isamarkuptext}%

  1562 \isamarkuptrue%

  1563 %

  1564 \isamarkupsection{Nested recursion%

  1565 }

  1566 \isamarkuptrue%

  1567 %

  1568 \begin{isamarkuptext}%

  1569 Recursive calls which are nested in one another frequently cause

  1570   complications, since their termination proof can depend on a partial

  1571   correctness property of the function itself.

  1573   As a small example, we define the \qt{nested zero} function:%

  1574 \end{isamarkuptext}%

  1575 \isamarkuptrue%

  1576 \isacommand{function}\isamarkupfalse%

  1577 \ nz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

  1578 \isakeyword{where}\isanewline

  1579 \ \ {\isachardoublequoteopen}nz\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1580 {\isacharbar}\ {\isachardoublequoteopen}nz\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ nz\ {\isacharparenleft}nz\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1581 %

  1582 \isadelimproof

  1583 %

  1584 \endisadelimproof

  1585 %

  1586 \isatagproof

  1587 \isacommand{by}\isamarkupfalse%

  1588 \ pat{\isacharunderscore}completeness\ auto%

  1589 \endisatagproof

  1590 {\isafoldproof}%

  1591 %

  1592 \isadelimproof

  1593 %

  1594 \endisadelimproof

  1595 %

  1596 \begin{isamarkuptext}%

  1597 If we attempt to prove termination using the identity measure on

  1598   naturals, this fails:%

  1599 \end{isamarkuptext}%

  1600 \isamarkuptrue%

  1601 \isacommand{termination}\isamarkupfalse%

  1602 \isanewline

  1603 %

  1604 \isadelimproof

  1605 \ \ %

  1606 \endisadelimproof

  1607 %

  1608 \isatagproof

  1609 \isacommand{apply}\isamarkupfalse%

  1610 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline

  1611 \ \ \isacommand{apply}\isamarkupfalse%

  1612 \ auto%

  1613 \begin{isamarkuptxt}%

  1614 We get stuck with the subgoal

  1616   \begin{isabelle}%

  1617 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharless}\ Suc\ n%

  1618 \end{isabelle}

  1620   Of course this statement is true, since we know that \isa{nz} is

  1621   the zero function. And in fact we have no problem proving this

  1622   property by induction.%

  1623 \end{isamarkuptxt}%

  1624 \isamarkuptrue%

  1625 %

  1626 \endisatagproof

  1627 {\isafoldproof}%

  1628 %

  1629 \isadelimproof

  1630 %

  1631 \endisadelimproof

  1632 \isacommand{lemma}\isamarkupfalse%

  1633 \ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

  1634 %

  1635 \isadelimproof

  1636 \ \ %

  1637 \endisadelimproof

  1638 %

  1639 \isatagproof

  1640 \isacommand{by}\isamarkupfalse%

  1641 \ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto%

  1642 \endisatagproof

  1643 {\isafoldproof}%

  1644 %

  1645 \isadelimproof

  1646 %

  1647 \endisadelimproof

  1648 %

  1649 \begin{isamarkuptext}%

  1650 We formulate this as a partial correctness lemma with the condition

  1651   \isa{nz{\isacharunderscore}dom\ n}. This allows us to prove it with the \isa{pinduct} rule before we have proved termination. With this lemma,

  1652   the termination proof works as expected:%

  1653 \end{isamarkuptext}%

  1654 \isamarkuptrue%

  1655 \isacommand{termination}\isamarkupfalse%

  1656 \isanewline

  1657 %

  1658 \isadelimproof

  1659 \ \ %

  1660 \endisadelimproof

  1661 %

  1662 \isatagproof

  1663 \isacommand{by}\isamarkupfalse%

  1664 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharparenright}%

  1665 \endisatagproof

  1666 {\isafoldproof}%

  1667 %

  1668 \isadelimproof

  1669 %

  1670 \endisadelimproof

  1671 %

  1672 \begin{isamarkuptext}%

  1673 As a general strategy, one should prove the statements needed for

  1674   termination as a partial property first. Then they can be used to do

  1675   the termination proof. This also works for less trivial

  1676   examples. Figure \ref{f91} defines the 91-function, a well-known

  1677   challenge problem due to John McCarthy, and proves its termination.%

  1678 \end{isamarkuptext}%

  1679 \isamarkuptrue%

  1680 %

  1681 \begin{figure}

  1682 \hrule\vspace{6pt}

  1683 \begin{minipage}{0.8\textwidth}

  1684 \isabellestyle{it}

  1685 \isastyle\isamarkuptrue

  1686 \isacommand{function}\isamarkupfalse%

  1687 \ f{\isadigit{9}}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline

  1688 \isakeyword{where}\isanewline

  1689 \ \ {\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

  1690 %

  1691 \isadelimproof

  1692 %

  1693 \endisadelimproof

  1694 %

  1695 \isatagproof

  1696 \isacommand{by}\isamarkupfalse%

  1697 \ pat{\isacharunderscore}completeness\ auto%

  1698 \endisatagproof

  1699 {\isafoldproof}%

  1700 %

  1701 \isadelimproof

  1702 \isanewline

  1703 %

  1704 \endisadelimproof

  1705 \isanewline

  1706 \isacommand{lemma}\isamarkupfalse%

  1707 \ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate{\isacharcolon}\ \isanewline

  1708 \ \ \isakeyword{assumes}\ trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ n{\isachardoublequoteclose}\ \isanewline

  1709 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\isanewline

  1710 %

  1711 \isadelimproof

  1712 %

  1713 \endisadelimproof

  1714 %

  1715 \isatagproof

  1716 \isacommand{using}\isamarkupfalse%

  1717 \ trm\ \isacommand{by}\isamarkupfalse%

  1718 \ induct\ auto%

  1719 \endisatagproof

  1720 {\isafoldproof}%

  1721 %

  1722 \isadelimproof

  1723 \isanewline

  1724 %

  1725 \endisadelimproof

  1726 \isanewline

  1727 \isacommand{termination}\isamarkupfalse%

  1728 \isanewline

  1729 %

  1730 \isadelimproof

  1731 %

  1732 \endisadelimproof

  1733 %

  1734 \isatagproof

  1735 \isacommand{proof}\isamarkupfalse%

  1736 \isanewline

  1737 \ \ \isacommand{let}\isamarkupfalse%

  1738 \ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{1}}\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline

  1739 \ \ \isacommand{show}\isamarkupfalse%

  1740 \ {\isachardoublequoteopen}wf\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%

  1741 \isanewline

  1742 \isanewline

  1743 \ \ \isacommand{fix}\isamarkupfalse%

  1744 \ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isacommand{assume}\isamarkupfalse%

  1745 \ {\isachardoublequoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isachardoublequoteclose}\ %

  1746 \isamarkupcmt{Assumptions for both calls%

  1747 }

  1748 \isanewline

  1749 \isanewline

  1750 \ \ \isacommand{thus}\isamarkupfalse%

  1751 \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1752 \ simp\ %

  1753 \isamarkupcmt{Inner call%

  1754 }

  1755 \isanewline

  1756 \isanewline

  1757 \ \ \isacommand{assume}\isamarkupfalse%

  1758 \ inner{\isacharunderscore}trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ %

  1759 \isamarkupcmt{Outer call%

  1760 }

  1761 \isanewline

  1762 \ \ \isacommand{with}\isamarkupfalse%

  1763 \ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate\ \isacommand{have}\isamarkupfalse%

  1764 \ {\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%

  1765 \isanewline

  1766 \ \ \isacommand{with}\isamarkupfalse%

  1767 \ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%

  1768 \ {\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%

  1769 \ simp\isanewline

  1770 \isacommand{qed}\isamarkupfalse%

  1771 %

  1772 \endisatagproof

  1773 {\isafoldproof}%

  1774 %

  1775 \isadelimproof

  1776 %

  1777 \endisadelimproof

  1778 %

  1779 \isamarkupfalse\isabellestyle{tt}

  1780 \end{minipage}

  1781 \vspace{6pt}\hrule

  1782 \caption{McCarthy's 91-function}\label{f91}

  1783 \end{figure}

  1784 %

  1785 \isamarkupsection{Higher-Order Recursion%

  1786 }

  1787 \isamarkuptrue%

  1788 %

  1789 \begin{isamarkuptext}%

  1790 Higher-order recursion occurs when recursive calls

  1791   are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc.

  1792   As an example, imagine a datatype of n-ary trees:%

  1793 \end{isamarkuptext}%

  1794 \isamarkuptrue%

  1795 \isacommand{datatype}\isamarkupfalse%

  1796 \ {\isacharprime}a\ tree\ {\isacharequal}\ \isanewline

  1797 \ \ Leaf\ {\isacharprime}a\ \isanewline

  1798 {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ list{\isachardoublequoteclose}%

  1799 \begin{isamarkuptext}%

  1800 \noindent We can define a function which swaps the left and right subtrees recursively, using the

  1801   list functions \isa{rev} and \isa{map}:%

  1802 \end{isamarkuptext}%

  1803 \isamarkuptrue%

  1804 \isacommand{fun}\isamarkupfalse%

  1805 \ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline

  1806 \isakeyword{where}\isanewline

  1807 \ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline

  1808 {\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

  1809 \begin{isamarkuptext}%

  1810 Although the definition is accepted without problems, let us look at the termination proof:%

  1811 \end{isamarkuptext}%

  1812 \isamarkuptrue%

  1813 \isacommand{termination}\isamarkupfalse%

  1814 %

  1815 \isadelimproof

  1816 \ %

  1817 \endisadelimproof

  1818 %

  1819 \isatagproof

  1820 \isacommand{proof}\isamarkupfalse%

  1821 %

  1822 \begin{isamarkuptxt}%

  1823 As usual, we have to give a wellfounded relation, such that the

  1824   arguments of the recursive calls get smaller. But what exactly are

  1825   the arguments of the recursive calls when mirror is given as an

  1826   argument to map? Isabelle gives us the

  1827   subgoals

  1829   \begin{isabelle}%

  1830 \ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline

  1831 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%

  1832 \end{isabelle}

  1834   So the system seems to know that \isa{map} only

  1835   applies the recursive call \isa{mirror} to elements

  1836   of \isa{l}, which is essential for the termination proof.

  1838   This knowledge about map is encoded in so-called congruence rules,

  1839   which are special theorems known to the \cmd{function} command. The

  1840   rule for map is

  1842   \begin{isabelle}%

  1843 {\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%

  1844 \end{isabelle}

  1846   You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions

  1847   coincide on the elements of the list. This means that for the value

  1848   \isa{map\ f\ l} we only have to know how \isa{f} behaves on

  1849   the elements of \isa{l}.

  1851   Usually, one such congruence rule is

  1852   needed for each higher-order construct that is used when defining

  1853   new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handled by this mechanism. The congruence

  1854   rule for \isa{If} states that the \isa{then} branch is only

  1855   relevant if the condition is true, and the \isa{else} branch only if it

  1856   is false:

  1858   \begin{isabelle}%

  1859 {\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

  1860 {\isasymLongrightarrow}\ {\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}%

  1861 \end{isabelle}

  1863   Congruence rules can be added to the

  1864   function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute.

  1866   The constructs that are predefined in Isabelle, usually

  1867   come with the respective congruence rules.

  1868   But if you define your own higher-order functions, you may have to

  1869   state and prove the required congruence rules yourself, if you want to use your

  1870   functions in recursive definitions.%

  1871 \end{isamarkuptxt}%

  1872 \isamarkuptrue%

  1873 %

  1874 \endisatagproof

  1875 {\isafoldproof}%

  1876 %

  1877 \isadelimproof

  1878 %

  1879 \endisadelimproof

  1880 %

  1881 \isamarkupsubsection{Congruence Rules and Evaluation Order%

  1882 }

  1883 \isamarkuptrue%

  1884 %

  1885 \begin{isamarkuptext}%

  1886 Higher order logic differs from functional programming languages in

  1887   that it has no built-in notion of evaluation order. A program is

  1888   just a set of equations, and it is not specified how they must be

  1889   evaluated.

  1891   However for the purpose of function definition, we must talk about

  1892   evaluation order implicitly, when we reason about termination.

  1893   Congruence rules express that a certain evaluation order is

  1894   consistent with the logical definition.

  1896   Consider the following function.%

  1897 \end{isamarkuptext}%

  1898 \isamarkuptrue%

  1899 \isacommand{function}\isamarkupfalse%

  1900 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

  1901 \isakeyword{where}\isanewline

  1902 \ \ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ f\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%

  1903 \isadelimproof

  1904 %

  1905 \endisadelimproof

  1906 %

  1907 \isatagproof

  1908 %

  1909 \endisatagproof

  1910 {\isafoldproof}%

  1911 %

  1912 \isadelimproof

  1913 %

  1914 \endisadelimproof

  1915 %

  1916 \begin{isamarkuptext}%

  1917 For this definition, the termination proof fails. The default configuration

  1918   specifies no congruence rule for disjunction. We have to add a

  1919   congruence rule that specifies left-to-right evaluation order:

  1921   \vspace{1ex}

  1922   \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})

  1923   \vspace{1ex}

  1925   Now the definition works without problems. Note how the termination

  1926   proof depends on the extra condition that we get from the congruence

  1927   rule.

  1929   However, as evaluation is not a hard-wired concept, we

  1930   could just turn everything around by declaring a different

  1931   congruence rule. Then we can make the reverse definition:%

  1932 \end{isamarkuptext}%

  1933 \isamarkuptrue%

  1934 \isacommand{lemma}\isamarkupfalse%

  1935 \ disj{\isacharunderscore}cong{\isadigit{2}}{\isacharbrackleft}fundef{\isacharunderscore}cong{\isacharbrackright}{\isacharcolon}\ \isanewline

  1936 \ \ {\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

  1937 %

  1938 \isadelimproof

  1939 \ \ %

  1940 \endisadelimproof

  1941 %

  1942 \isatagproof

  1943 \isacommand{by}\isamarkupfalse%

  1944 \ blast%

  1945 \endisatagproof

  1946 {\isafoldproof}%

  1947 %

  1948 \isadelimproof

  1949 \isanewline

  1950 %

  1951 \endisadelimproof

  1952 \isanewline

  1953 \isacommand{fun}\isamarkupfalse%

  1954 \ f{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

  1955 \isakeyword{where}\isanewline

  1956 \ \ {\isachardoublequoteopen}f{\isacharprime}\ n\ {\isacharequal}\ {\isacharparenleft}f{\isacharprime}\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymor}\ n\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}%

  1957 \begin{isamarkuptext}%

  1958 \noindent These examples show that, in general, there is no \qt{best} set of

  1959   congruence rules.

  1961   However, such tweaking should rarely be necessary in

  1962   practice, as most of the time, the default set of congruence rules

  1963   works well.%

  1964 \end{isamarkuptext}%

  1965 \isamarkuptrue%

  1966 %

  1967 \isadelimtheory

  1968 %

  1969 \endisadelimtheory

  1970 %

  1971 \isatagtheory

  1972 \isacommand{end}\isamarkupfalse%

  1973 %

  1974 \endisatagtheory

  1975 {\isafoldtheory}%

  1976 %

  1977 \isadelimtheory

  1978 %

  1979 \endisadelimtheory

  1980 \isanewline

  1981 \end{isabellebody}%

  1982 %%% Local Variables:

  1983 %%% mode: latex

  1984 %%% TeX-master: "root"

  1985 %%% End:

author	wenzelm
	Thu, 01 Jan 2009 21:30:13 +0100
changeset 29297	62e0f892e525
parent 27026	3602b81665b5
child 30121	5c7bcb296600
permissions	-rw-r--r--