doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex

updated

%
\begin{isabellebody}%
\def\isabellecontext{Functions}%
%
\isadelimtheory
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Functions\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Function Definition for Dummies%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In most cases, defining a recursive function is just as simple as other definitions:

  Like in functional programming, a function definition consists of a%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The syntax is rather self-explanatory: We introduce a function by
  giving its name, its type and a set of defining recursive
  equations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
The function always terminates, since its argument gets smaller in
  every recursive call. Termination is an important requirement, since
  it prevents inconsistencies: From the "definition" \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.

  Isabelle tries to prove termination automatically when a function is
  defined. We will later look at cases where this fails and see what to
  do then.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Pattern matching%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{patmatch}
  Like in functional programming, we can use pattern matching to
  define functions. At the moment we will only consider \emph{constructor
  patterns}, which only consist of datatype constructors and
  variables.

  If patterns overlap, the order of the equations is taken into
  account. The following function inserts a fixed element between any
  two elements of a list:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Overlapping patterns are interpreted as "increments" to what is
  already there: The second equation is only meant for the cases where
  the first one does not match. Consequently, Isabelle replaces it
  internally by the remaining cases, making the patterns disjoint:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ sep{\isachardot}simps%
\begin{isamarkuptext}%
\begin{isabelle}%
sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}\isasep\isanewline%
sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline%
sep\ a\ {\isacharbrackleft}v{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}v{\isacharbrackright}%
\end{isabelle}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
The equations from function definitions are automatically used in
  simplification:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}sep\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Induction%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle provides customized induction rules for recursive functions.  
  See \cite[\S3.5.4]{isa-tutorial}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Full form definitions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Up to now, we were using the \cmd{fun} command, which provides a
  convenient shorthand notation for simple function definitions. In
  this mode, Isabelle tries to solve all the necessary proof obligations
  automatically. If a proof does not go through, the definition is
  rejected. This can either mean that the definition is indeed faulty,
  or that the default proof procedures are just not smart enough (or
  rather: not designed) to handle the definition.

  By expanding the abbreviated \cmd{fun} to the full \cmd{function}
  command, the proof obligations become visible and can be analyzed or
  solved manually.

\end{isamarkuptext}


\fbox{\parbox{\textwidth}{
\noindent\cmd{fun} \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%
\cmd{where}\isanewline%
\ \ {\it equations}\isanewline%
\ \ \quad\vdots
}}

\begin{isamarkuptext}
\vspace*{1em}
\noindent abbreviates
\end{isamarkuptext}

\fbox{\parbox{\textwidth}{
\noindent\cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%
\cmd{where}\isanewline%
\ \ {\it equations}\isanewline%
\ \ \quad\vdots\\%
\cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\%
\cmd{termination by} \isa{lexicographic{\isacharunderscore}order}
}}

\begin{isamarkuptext}
  \vspace*{1em}
  \noindent Some declarations and proofs have now become explicit:

  \begin{enumerate}
  \item The \cmd{sequential} option enables the preprocessing of
  pattern overlaps we already saw. Without this option, the equations
  must already be disjoint and complete. The automatic completion only
  works with datatype patterns.

  \item A function definition now produces a proof obligation which
  expresses completeness and compatibility of patterns (We talk about
  this later). The combination of the methods \isa{pat{\isacharunderscore}completeness} and
  \isa{auto} is used to solve this proof obligation.

  \item A termination proof follows the definition, started by the
  \cmd{termination} command, which sets up the goal. The \isa{lexicographic{\isacharunderscore}order} method can prove termination of a certain
  class of functions by searching for a suitable lexicographic
  combination of size measures.
 \end{enumerate}
  Whenever a \cmd{fun} command fails, it is usually a good idea to
  expand the syntax to the more verbose \cmd{function} form, to see
  what is actually going on.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proving termination%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Consider the following function, which sums up natural numbers up to
  \isa{N}, using a counter \isa{i}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sum\ i\ N\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isachargreater}\ N\ then\ {\isadigit{0}}\ else\ i\ {\isacharplus}\ sum\ {\isacharparenleft}Suc\ i{\isacharparenright}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
\noindent The \isa{lexicographic{\isacharunderscore}order} method fails on this example, because none of the
  arguments decreases in the recursive call.

  A more general method for termination proofs is to supply a wellfounded
  relation on the argument type, and to show that the argument
  decreases in every recursive call. 

  The termination argument for \isa{sum} is based on the fact that
  the \emph{difference} between \isa{i} and \isa{N} gets
  smaller in every step, and that the recursion stops when \isa{i}
  is greater then \isa{n}. Phrased differently, the expression 
  \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} decreases in every recursive call.

  We can use this expression as a measure function suitable to prove termination.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
\ sum\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
The \cmd{termination} command sets up the termination goal for the
  specified function \isa{sum}. If the function name is omitted it
  implicitly refers to the last function definition.

  The \isa{relation} method takes a relation of
  type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of
  the function. If the function has multiple curried arguments, then
  these are packed together into a tuple, as it happened in the above
  example.

  The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is a very common way of
  specifying termination relations in terms of a mapping into the
  natural numbers.

  After the invocation of \isa{relation}, we must prove that (a)
  the relation we supplied is wellfounded, and (b) that the arguments
  of recursive calls indeed decrease with respect to the
  relation. These goals are all solved by the subsequent call to
  \isa{auto}.

  Let us complicate the function a little, by adding some more
  recursive calls:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ foo\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}foo\ i\ N\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isachargreater}\ N\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ {\isacharparenleft}if\ N\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ foo\ {\isadigit{0}}\ {\isacharparenleft}N\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ i\ {\isacharplus}\ foo\ {\isacharparenleft}Suc\ i{\isacharparenright}\ N{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
When \isa{i} has reached \isa{N}, it starts at zero again
  and \isa{N} is decremented.
  This corresponds to a nested
  loop where one index counts up and the other down. Termination can
  be proved using a lexicographic combination of two measures, namely
  the value of \isa{N} and the above difference. The \isa{measures} combinator generalizes \isa{measure} by taking a
  list of measure functions.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
\ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Manual Termination Proofs%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \isa{relation} method is often useful, but not
  necessary. Since termination proofs are just normal Isabelle proofs,
  they can also be carried out manually:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ id\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}id\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}id\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}id\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ \isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}wf\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ n\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}n{\isacharcomma}\ Suc\ n{\isacharparenright}\ {\isasymin}\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Of course this is just a trivial example, but manual proofs can
  sometimes be the only choice if faced with very hard termination problems.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Mutual Recursion%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
If two or more functions call one another mutually, they have to be defined
  in one step. The simplest example are probably \isa{even} and \isa{odd}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{and}\ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}even\ {\isadigit{0}}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}odd\ {\isadigit{0}}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ odd\ n{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ even\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
To solve the problem of mutual dependencies, Isabelle internally
  creates a single function operating on the sum
  type. Then the original functions are defined as
  projections. Consequently, termination has to be proved
  simultaneously for both functions, by specifying a measure on the
  sum type:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
\ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ case\ x\ of\ Inl\ n\ {\isasymRightarrow}\ n\ {\isacharbar}\ Inr\ n\ {\isasymRightarrow}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ \isanewline
\ \ \ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Induction for mutual recursion%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
When functions are mutually recursive, proving properties about them
  generally requires simultaneous induction. The induction rules
  generated from the definitions reflect this.

  Let us prove something about \isa{even} and \isa{odd}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
We apply simultaneous induction, specifying the induction variable
  for both goals, separated by \cmd{and}:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ \isakeyword{and}\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
We get four subgoals, which correspond to the clauses in the
  definition of \isa{even} and \isa{odd}:
  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ odd\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\isanewline
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\ {\isasymLongrightarrow}\ even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline
\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}%
\end{isabelle}
  Simplification solves the first two goals, leaving us with two
  statements about the \isa{mod} operation to prove:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ odd\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}%
\end{isabelle} 

  \noindent These can be handeled by the descision procedure for
  presburger arithmethic.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ presburger\isanewline
\isacommand{apply}\isamarkupfalse%
\ presburger\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Even if we were just interested in one of the statements proved by
  simultaneous induction, the other ones may be necessary to
  strengthen the induction hypothesis. If we had left out the statement
  about \isa{odd} (by substituting it with \isa{True}, our
  proof would have failed:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}True{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}induct\ n\ rule{\isacharcolon}\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent Now the third subgoal is a dead end, since we have no
  useful induction hypothesis:

  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ even\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ True\isanewline
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ True\ {\isasymLongrightarrow}\ even\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\isanewline
\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ True%
\end{isabelle}%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{oops}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsection{More general patterns%
}
\isamarkuptrue%
%
\isamarkupsubsection{Avoiding pattern splitting%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Up to now, we used pattern matching only on datatypes, and the
  patterns were always disjoint and complete, and if they weren't,
  they were made disjoint automatically like in the definition of
  \isa{sep} in \S\ref{patmatch}.

  This splitting can significantly increase the number of equations
  involved, and is not always necessary. The following simple example
  shows the problem:
  
  Suppose we are modelling incomplete knowledge about the world by a
  three-valued datatype, which has values \isa{T}, \isa{F}
  and \isa{X} for true, false and uncertain propositions, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ P{\isadigit{3}}\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ X%
\begin{isamarkuptext}%
Then the conjunction of such values can be defined as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ And\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}And\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
\begin{isamarkuptext}%
This definition is useful, because the equations can directly be used
  as rules to simplify expressions. But the patterns overlap, e.g.~the
  expression \isa{And\ T\ T} is matched by the first two
  equations. By default, Isabelle makes the patterns disjoint by
  splitting them up, producing instances:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ And{\isachardot}simps%
\begin{isamarkuptext}%
\isa{And\ T\ {\isacharquery}p\ {\isacharequal}\ {\isacharquery}p\isasep\isanewline%
And\ F\ T\ {\isacharequal}\ F\isasep\isanewline%
And\ X\ T\ {\isacharequal}\ X\isasep\isanewline%
And\ F\ F\ {\isacharequal}\ F\isasep\isanewline%
And\ X\ F\ {\isacharequal}\ F\isasep\isanewline%
And\ F\ X\ {\isacharequal}\ F\isasep\isanewline%
And\ X\ X\ {\isacharequal}\ X}
  
  \vspace*{1em}
  \noindent There are several problems with this:

  \begin{enumerate}
  \item When datatypes have many constructors, there can be an
  explosion of equations. For \isa{And}, we get seven instead of
  five equations, which can be tolerated, but this is just a small
  example.

  \item Since splitting makes the equations "less general", they
  do not always match in rewriting. While the term \isa{And\ x\ F}
  can be simplified to \isa{F} by the original specification, a
  (manual) case split on \isa{x} is now necessary.

  \item The splitting also concerns the induction rule \isa{And{\isachardot}induct}. Instead of five premises it now has seven, which
  means that our induction proofs will have more cases.

  \item In general, it increases clarity if we get the same definition
  back which we put in.
  \end{enumerate}

  On the other hand, a definition needs to be consistent and defining
  both \isa{f\ x\ {\isacharequal}\ True} and \isa{f\ x\ {\isacharequal}\ False} is a bad
  idea. So if we don't want Isabelle to mangle our definitions, we
  will have to prove that this is not necessary. By using the full
  definition form without the \cmd{sequential} option, we get this
  behaviour:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ And{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
Now it is also time to look at the subgoals generated by a
  function definition. In this case, they are:

  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}{\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ \ }{\isasymAnd}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ }{\isasymLongrightarrow}\ P\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline
\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline
\ {\isadigit{5}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline
\ {\isadigit{6}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X\isanewline
\ {\isadigit{7}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ pa\isanewline
\ {\isadigit{8}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}pa{\isacharcomma}\ F{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline
\ {\isadigit{9}}{\isachardot}\ {\isasymAnd}p\ pa{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ pa{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ F\isanewline
\ {\isadigit{1}}{\isadigit{0}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharequal}\ X%
\end{isabelle} 

  The first subgoal expresses the completeness of the patterns. It has
  the form of an elimination rule and states that every \isa{x} of
  the function's input type must match one of the patterns. It could
  be equivalently stated as a disjunction of existential statements: 
\isa{{\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}} If the patterns just involve
  datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness} method:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ pat{\isacharunderscore}completeness%
\begin{isamarkuptxt}%
The remaining subgoals express \emph{pattern compatibility}. We do
  allow that a value is matched by more than one patterns, but in this
  case, the result (i.e.~the right hand sides of the equations) must
  also be equal. For each pair of two patterns, there is one such
  subgoal. Usually this needs injectivity of the constructors, which
  is used automatically by \isa{auto}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Non-constructor patterns%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Partiality%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In HOL, all functions are total. A function \isa{f} applied to
  \isa{x} always has a value \isa{f\ x}, and there is no notion
  of undefinedness. 
  
  This property of HOL is the reason why we have to do termination
  proofs when defining functions: The termination proof justifies the
  definition of the function by wellfounded recursion.

  However, the \cmd{function} package still supports partiality. Let's
  look at the following function which searches for a zero in the
  function f.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ {\isacharparenleft}if\ f\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Clearly, any attempt of a termination proof must fail. And without
  that, we do not get the usual rules \isa{findzero{\isachardot}simp} and 
  \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Domain predicates%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The trick is that Isabelle has not only defined the function \isa{findzero}, but also
  a predicate \isa{findzero{\isacharunderscore}dom} that characterizes the values where the function
  terminates: the \emph{domain} of the function. In Isabelle/HOL, a
  partial function is just a total function with an additional domain
  predicate. Like with total functions, we get simplification and
  induction rules, but they are guarded by the domain conditions and
  called \isa{psimps} and \isa{pinduct}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ findzero{\isachardot}psimps%
\begin{isamarkuptext}%
\begin{isabelle}%
findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}%
\end{isabelle}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ findzero{\isachardot}pinduct%
\begin{isamarkuptext}%
\begin{isabelle}%
{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline
\isaindent{\ }{\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ n{\isasymrbrakk}\isanewline
{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%
\end{isabelle}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
As already mentioned, HOL does not support true partiality. All we
  are doing here is using some tricks to make a total function appear
  as if it was partial. We can still write the term \isa{findzero\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}} and like any other term of type \isa{nat} it is equal
  to some natural number, although we might not be able to find out
  which one (we will discuss this further in \S\ref{default}). The
  function is \emph{underdefined}.

  But it is enough defined to prove something about it. We can prove
  that if \isa{findzero\ f\ n}
  it terminates, it indeed returns a zero of \isa{f}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ findzero{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
We apply induction as usual, but using the partial induction
  rule:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}%
\begin{isamarkuptxt}%
This gives the following subgoals:

  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}%
\end{isabelle}

  The premise in our lemma was used to satisfy the first premise in
  the induction rule. However, now we can also use \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as an assumption in the induction step. This
  allows to unfold \isa{findzero\ f\ n} using the \isa{psimps}
  rule, and the rest is trivial. Since \isa{psimps} rules carry the
  \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
\ simp\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Proofs about partial functions are often not harder than for total
  functions. Fig.~\ref{findzero_isar} shows a slightly more
  complicated proof written in Isar. It is verbose enough to show how
  partiality comes into play: From the partial induction, we get an
  additional domain condition hypothesis. Observe how this condition
  is applied when calls to \isa{findzero} are unfolded.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{figure}
\begin{center}
\begin{minipage}{0.8\textwidth}
\isabellestyle{it}
\isastyle\isamarkuptrue
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ f\ n\ \isacommand{assume}\isamarkupfalse%
\ dom{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{and}\ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isasymrbrakk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{and}\ x{\isacharunderscore}range{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ dom\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse%
\ False\ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ x{\isacharunderscore}range\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ n\ {\isasymor}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupfalse\isabellestyle{tt}
\end{minipage}\end{center}
\caption{A proof about a partial function}\label{findzero_isar}
\end{figure}
%
\isamarkupsubsection{Partial termination proofs%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Now that we have proved some interesting properties about our
  function, we should turn to the domain predicate and see if it is
  actually true for some values. Otherwise we would have just proved
  lemmas with \isa{False} as a premise.

  Essentially, we need some introduction rules for \isa{findzero{\isacharunderscore}dom}. The function package can prove such domain
  introduction rules automatically. But since they are not used very
  often (they are almost never needed if the function is total), they
  are disabled by default for efficiency reasons. So we have to go
  back and ask for them explicitly by passing the \isa{{\isacharparenleft}domintros{\isacharparenright}} option to the function package:

\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%
\cmd{where}\isanewline%
\ \ \ldots\\
\cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\%


  Now the package has proved an introduction rule for \isa{findzero{\isacharunderscore}dom}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ findzero{\isachardot}domintros%
\begin{isamarkuptext}%
\begin{isabelle}%
{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
\end{isabelle}

  Domain introduction rules allow to show that a given value lies in the
  domain of a function, if the arguments of all recursive calls
  are in the domain as well. They allow to do a \qt{single step} in a
  termination proof. Usually, you want to combine them with a suitable
  induction principle.

  Since our function increases its argument at recursive calls, we
  need an induction principle which works \qt{backwards}. We will use
  \isa{inc{\isacharunderscore}induct}, which allows to do induction from a fixed number
  \qt{downwards}:

  \begin{isabelle}%
{\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%
\end{isabelle}

  Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact
  that \isa{findzero} terminates if there is a zero which is greater
  or equal to \isa{n}. First we derive two useful rules which will
  solve the base case and the step case of the induction. The
  induction is then straightforward, except for the unusal induction
  principle.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{figure}
\begin{center}
\begin{minipage}{0.8\textwidth}
\isabellestyle{it}
\isastyle\isamarkuptrue
\isacommand{lemma}\isamarkupfalse%
\ findzero{\isacharunderscore}termination{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ base{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}{\isacharbackquoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ step{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i{\isachardot}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}\ \isanewline
\ \ \ \ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ simp\isanewline
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymge}\ n{\isacharbackquoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ base{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ i\ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ step{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupfalse\isabellestyle{tt}
\end{minipage}\end{center}
\caption{Termination proof for \isa{findzero}}\label{findzero_term}
\end{figure}
%
\begin{isamarkuptext}%
Again, the proof given in Fig.~\ref{findzero_term} has a lot of
  detail in order to explain the principles. Using more automation, we
  can also have a short proof:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ findzero{\isacharunderscore}termination{\isacharunderscore}short{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ zero{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ zero\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
It is simple to combine the partial correctness result with the
  termination lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ findzero{\isacharunderscore}total{\isacharunderscore}correctness{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}blast\ intro{\isacharcolon}\ findzero{\isacharunderscore}zero\ findzero{\isacharunderscore}termination{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Definition of the domain predicate%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Sometimes it is useful to know what the definition of the domain
  predicate actually is. Actually, \isa{findzero{\isacharunderscore}dom} is just an
  abbreviation:

  \begin{isabelle}%
findzero{\isacharunderscore}dom\ {\isasymequiv}\ acc\ findzero{\isacharunderscore}rel%
\end{isabelle}

  The domain predicate is the accessible part of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function
  package. \isa{findzero{\isacharunderscore}rel} is just a normal
  inductively defined predicate, so we can inspect its definition by
  looking at the introduction rules \isa{findzero{\isacharunderscore}rel{\isachardot}intros}.
  In our case there is just a single rule:

  \begin{isabelle}%
{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}rel\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
\end{isabelle}

  The relation \isa{findzero{\isacharunderscore}rel}, expressed as a binary predicate,
  describes the \emph{recursion relation} of the function
  definition. The recursion relation is a binary relation on
  the arguments of the function that relates each argument to its
  recursive calls. In general, there is one introduction rule for each
  recursive call.

  The predicate \isa{findzero{\isacharunderscore}dom} is the \emph{accessible part} of
  that relation. An argument belongs to the accessible part, if it can
  be reached in a finite number of steps. 

  Since the domain predicate is just an abbreviation, you can use
  lemmas for \isa{acc} and \isa{findzero{\isacharunderscore}rel} directly. Some
  lemmas which are occasionally useful are \isa{accI}, \isa{acc{\isacharunderscore}downward}, and of course the introduction and elimination rules
  for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{A Useful Special Case: Tail recursion%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The domain predicate is our trick that allows us to model partiality
  in a world of total functions. The downside of this is that we have
  to carry it around all the time. The termination proof above allowed
  us to replace the abstract \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} by the more
  concrete \isa{n\ {\isasymle}\ x\ {\isasymand}\ f\ x\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}, but the condition is still
  there and it won't go away soon. 

  In particular, the domain predicate guard the unfolding of our
  function, since it is there as a condition in the \isa{psimp}
  rules. 

  On the other hand, we must be happy about the domain predicate,
  since it guarantees that all this is at all possible without losing
  consistency. 

  Now there is an important special case: We can actually get rid
  of the condition in the simplification rules, \emph{if the function
  is tail-recursive}. The reason is that for all tail-recursive
  equations there is a total function satisfying them, even if they
  are non-terminating. 

  The function package internally does the right construction and can
  derive the unconditional simp rules, if we ask it to do so. Luckily,
  our \isa{findzero} function is tail-recursive, so we can just go
  back and add another option to the \cmd{function} command:

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

  
  Now, we actually get the unconditional simplification rules, even
  though the function is partial:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ findzero{\isachardot}simps%
\begin{isamarkuptext}%
\begin{isabelle}%
findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}%
\end{isabelle}

  Of course these would make the simplifier loop, so we better remove
  them from the simpset:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{declare}\isamarkupfalse%
\ findzero{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
\begin{isamarkuptext}%
\fixme{Code generation ???}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Nested recursion%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Recursive calls which are nested in one another frequently cause
  complications, since their termination proof can depend on a partial
  correctness property of the function itself. 

  As a small example, we define the \qt{nested zero} function:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ nz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nz\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}nz\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ nz\ {\isacharparenleft}nz\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
If we attempt to prove termination using the identity measure on
  naturals, this fails:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
\ auto%
\begin{isamarkuptxt}%
We get stuck with the subgoal

  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharless}\ Suc\ n%
\end{isabelle}

  Of course this statement is true, since we know that \isa{nz} is
  the zero function. And in fact we have no problem proving this
  property by induction.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{oops}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
We formulate this as a partial correctness lemma with the condition
  \isa{nz{\isacharunderscore}dom\ n}. This allows us to prove it with the \isa{pinduct} rule before we have proved termination. With this lemma,
  the termination proof works as expected:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
As a general strategy, one should prove the statements needed for
  termination as a partial property first. Then they can be used to do
  the termination proof. This also works for less trivial
  examples. Figure \ref{f91} defines the well-known 91-function by
  McCarthy \cite{?} and proves its termination.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{figure}
\begin{center}
\begin{minipage}{0.8\textwidth}
\isabellestyle{it}
\isastyle\isamarkuptrue
\isacommand{function}\isamarkupfalse%
\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n\ then\ n\ {\isacharminus}\ {\isadigit{1}}{\isadigit{0}}\ else\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ n{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ trm\ \isacommand{by}\isamarkupfalse%
\ induct\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{1}}\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}wf\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isachardoublequoteclose}\ %
\isamarkupcmt{Assumptions for both calls%
}
\isanewline
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\ %
\isamarkupcmt{Inner call%
}
\isanewline
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ inner{\isacharunderscore}trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ %
\isamarkupcmt{Outer call%
}
\isanewline
\ \ \isacommand{with}\isamarkupfalse%
\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{with}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\ \isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupfalse\isabellestyle{tt}
\end{minipage}\end{center}
\caption{McCarthy's 91-function}\label{f91}
\end{figure}
%
\isamarkupsection{Higher-Order Recursion%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Higher-order recursion occurs when recursive calls
  are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc.
  As an example, imagine a data type of n-ary trees:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ {\isacharprime}a\ tree\ {\isacharequal}\ \isanewline
\ \ Leaf\ {\isacharprime}a\ \isanewline
{\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ list{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent We can define a map function for trees, using the predefined
  map function for lists.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ treemap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ {\isacharparenleft}f\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}map\ {\isacharparenleft}treemap\ f{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
We do the termination proof manually, to point out what happens
  here:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
%
\isadelimproof
\ %
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
%
\begin{isamarkuptxt}%
As usual, we have to give a wellfounded relation, such that the
  arguments of the recursive calls get smaller. But what exactly are
  the arguments of the recursive calls? Isabelle gives us the
  subgoals

  \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ f{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
\end{isabelle} 

  So Isabelle seems to know that \isa{map} behaves nicely and only
  applies the recursive call \isa{treemap\ f} to elements
  of \isa{l}. Before we discuss where this knowledge comes from,
  let us finish the termination proof:%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ f\ l\ \isakeyword{and}\ x\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}f{\isacharcomma}\ Branch\ l{\isacharparenright}{\isacharparenright}\ {\isasymin}\ measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ simp%
\begin{isamarkuptxt}%
Simplification returns the following subgoal: 

      \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ x{\isacharunderscore}{\isacharunderscore}\ {\isasymin}\ set\ l{\isacharunderscore}{\isacharunderscore}\ {\isasymLongrightarrow}\ size\ x{\isacharunderscore}{\isacharunderscore}\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharunderscore}{\isacharunderscore}{\isacharparenright}%
\end{isabelle} 

      We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the
      definition of the \isa{tree} type. We should go back and prove
      it, by induction.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \isacommand{oops}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isanewline
\isanewline
\ \ \isacommand{lemma}\isamarkupfalse%
\ tree{\isacharunderscore}list{\isacharunderscore}size{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ \ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Now the whole termination proof is automatic:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{termination}\isamarkupfalse%
\ \isanewline
%
\isadelimproof
\ \ \ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ lexicographic{\isacharunderscore}order%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Congruence Rules%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Let's come back to the question how Isabelle knows about \isa{map}.

  The knowledge about map is encoded in so-called congruence rules,
  which are special theorems known to the \cmd{function} command. The
  rule for map is

  \begin{isabelle}%
{\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys%
\end{isabelle}

  You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions
  coincide on the elements of the list. This means that for the value 
  \isa{map\ f\ l} we only have to know how \isa{f} behaves on
  \isa{l}.

  Usually, one such congruence rule is
  needed for each higher-order construct that is used when defining
  new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handeled by this mechanism. The congruence
  rule for \isa{If} states that the \isa{then} branch is only
  relevant if the condition is true, and the \isa{else} branch only if it
  is false:

  \begin{isabelle}%
{\isasymlbrakk}{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c{\isacharsemicolon}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v{\isasymrbrakk}\isanewline
{\isasymLongrightarrow}\ {\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}%
\end{isabelle}
  
  Congruence rules can be added to the
  function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute.

  Isabelle comes with predefined congruence rules for most of the
  definitions.
  But if you define your own higher-order constructs, you will have to
  come up with the congruence rules yourself, if you want to use your
  functions in recursive definitions. Since the structure of
  congruence rules is a little unintuitive, here are some exercises:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{exercise}
    Find a suitable congruence rule for the following function which
  maps only over the even numbers in a list:

  \begin{isabelle}%
mapeven\ {\isacharquery}f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline%
mapeven\ {\isacharquery}f\ {\isacharparenleft}{\isacharquery}x\ {\isacharhash}\ {\isacharquery}xs{\isacharparenright}\ {\isacharequal}\isanewline
{\isacharparenleft}if\ {\isacharquery}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}f\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs\ else\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs{\isacharparenright}%
\end{isabelle}
  \end{exercise}
  
  \begin{exercise}
  What happens if the congruence rule for \isa{If} is
  disabled by declaring \isa{if{\isacharunderscore}cong{\isacharbrackleft}fundef{\isacharunderscore}cong\ del{\isacharbrackright}}?
  \end{exercise}

  Note that in some cases there is no \qt{best} congruence rule.
  \fixme%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Appendix: Predefined Congruence Rules%
}
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\isamarkupsubsection{Basic Control Structures%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\isa{\mbox{}\inferrule{\mbox{{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c}\\\ \mbox{{\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u}\\\ \mbox{{\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v}}{\mbox{{\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{Let\ {\isacharquery}M\ {\isacharquery}f\ {\isacharequal}\ Let\ {\isacharquery}N\ {\isacharquery}g}}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Data Types%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
For each \cmd{datatype} definition, a congruence rule for the case
  combinator is registeres automatically. Here are the rules for
  \isa{nat} and \isa{list}:

\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}nat{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ Suc\ nat\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat}}{\mbox{nat{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ nat{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center}

\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}a\ list{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list}}{\mbox{list{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ list{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{List combinators%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{filter\ {\isacharquery}P\ {\isacharquery}xs\ {\isacharequal}\ filter\ {\isacharquery}Q\ {\isacharquery}ys}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ a\ {\isacharequal}\ {\isacharquery}g\ x\ a}}{\mbox{foldr\ {\isacharquery}f\ {\isacharquery}l\ {\isacharquery}a\ {\isacharequal}\ foldr\ {\isacharquery}g\ {\isacharquery}k\ {\isacharquery}b}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ a\ x\ {\isacharequal}\ {\isacharquery}g\ a\ x}}{\mbox{foldl\ {\isacharquery}f\ {\isacharquery}a\ {\isacharquery}l\ {\isacharequal}\ foldl\ {\isacharquery}g\ {\isacharquery}b\ {\isacharquery}k}}}

Similar: takewhile, dropwhile%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Sets%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}}

\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{{\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}M\ {\isacharequal}\ {\isacharquery}g\ {\isacharbackquote}\ {\isacharquery}N}}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: