diff -r 3d716cc9bd7a -r cdd077905eee doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Sun Jan 14 09:57:29 2007 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Jan 15 10:15:55 2007 +0100
@@ -24,11 +24,6 @@
 }
 \isamarkuptrue%
 %
-\begin{isamarkuptext}%
-\cite{isa-tutorial}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Function Definition for Dummies%
 }
 \isamarkuptrue%
@@ -61,7 +56,8 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Like in functional programming, functions can be defined by pattern
+\label{patmatch}
+  Like in functional programming, functions can be defined by pattern
   matching. At the moment we will only consider \emph{datatype
   patterns}, which only consist of datatype constructors and
   variables.
@@ -80,8 +76,13 @@
 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.
-  This results in the equations \begin{isabelle}%
+  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}%
@@ -95,7 +96,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\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
 %
@@ -116,11 +117,12 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+Isabelle provides customized induction rules for recursive functions.  
+  See \cite[\S3.5.4]{isa-tutorial}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{If it does not work%
+\isamarkupsection{Full form definitions%
 }
 \isamarkuptrue%
 %
@@ -129,85 +131,61 @@
   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 mean that the definition is indeed faulty, like,
-  or that the default proof procedures are not smart enough (or
-  rather: not designed) to handle the specific definition.
-.
-  By expanding the abbreviation to the full \cmd{function} command, the
-  proof obligations become visible and can be analyzed and solved manually.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymtau}{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
-\ \ %
-\begin{isamarkuptext}%
-\vspace{-0.8cm}\emph{equations}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent abbreviates%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{function}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{sequential}{\isacharparenright}\ fo\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymtau}{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
-\ \ %
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\vspace{-0.8cm}\emph{equations}%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\ \isanewline
-\isacommand{termination}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ lexicographic{\isacharunderscore}order%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Some declarations and proofs have now become explicit:
+  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 "sequential" option enables the preprocessing of
+  \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 {\tt pat\_completeness} and
-  {\tt auto} is used to solve this proof obligation.
+  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. The {\tt lexicographic\_order} method can prove termination of a
-  certain class of functions by searching for a suitable lexicographic combination of size
-  measures.
-  \end{enumerate}%
+  \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%
 %
@@ -217,7 +195,7 @@
 %
 \begin{isamarkuptext}%
 Consider the following function, which sums up natural numbers up to
-  \isa{N}, using a counter \isa{i}%
+  \isa{N}, using a counter \isa{i}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{function}\isamarkupfalse%
@@ -226,7 +204,7 @@
 \ \ {\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
@@ -240,7 +218,7 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-The {\tt lexicographic\_order} method fails on this example, because none of the
+\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
@@ -253,15 +231,14 @@
   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 to construct a
-  wellfounded relation, which can prove termination.%
+  We can use this expression as a measure function suitable to prove termination.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
 \ \isanewline
 %
 \isadelimproof
-\ \ %
+%
 \endisadelimproof
 %
 \isatagproof
@@ -275,13 +252,24 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Note that the two (curried) function arguments appear as a pair in
-  the measure function. The \cmd{function} command packs together curried
-  arguments into a tuple to simplify its internal operation. Hence,
-  measure functions and termination relations always work on the
-  tupled type.
+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.
 
-  Let us complicate the function a little, by adding some more recursive calls:%
+  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%
@@ -311,15 +299,15 @@
   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.%
+  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
@@ -342,7 +330,8 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{function}\isamarkupfalse%
-\ even\ odd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ 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
@@ -350,7 +339,7 @@
 {\isacharbar}\ {\isachardoublequoteopen}odd\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ even\ n{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
-\ \ %
+%
 \endisadelimproof
 %
 \isatagproof
@@ -376,12 +365,121 @@
 \ \isanewline
 %
 \isadelimproof
-\ \ %
+%
 \endisadelimproof
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
+\ {\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}%
 %
@@ -389,7 +487,153 @@
 %
 \endisadelimproof
 %
-\isamarkupsection{Nested recursion%
+\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 for \isa{T}, \isa{F}
+  and \isa{X} for true, false and uncertain propositions.%
+\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
+\ \ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+\ \ {\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 approach:
+
+  \begin{enumerate}
+  \item When datatypes have many constructors, there can be an
+  explosion of equations. For \isa{And}, we get seven instead of
+  five equation, which can be tolerated, but this is just a small
+  example.
+
+  \item Since splitting makes the equations "more special", 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 withour 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
+\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+\ \ {\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%
 %
@@ -398,7 +642,29 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{More general patterns%
+\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. 
+
+  FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Nested recursion%
 }
 \isamarkuptrue%
 %