--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Sun Jan 14 09:57:29 2007 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Mon Jan 15 10:15:55 2007 +0100
@@ -10,7 +10,6 @@
begin
chapter {* Defining Recursive Functions in Isabelle/HOL *}
-text {* \cite{isa-tutorial} *}
section {* Function Definition for Dummies *}
@@ -38,7 +37,7 @@
subsection {* Pattern matching *}
-text {*
+text {* \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
@@ -58,80 +57,95 @@
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 @{thm [display] sep.simps[no_vars]}
+ internally by the remaining cases, making the patterns disjoint:
*}
-
-
+thm sep.simps
-
-
+text {* @{thm [display] sep.simps[no_vars]} *}
text {*
The equations from function definitions are automatically used in
simplification:
*}
-lemma "fib (Suc (Suc 0)) = (Suc (Suc 0))"
+lemma "sep (0::nat) [1, 2, 3] = [1, 0, 2, 0, 3]"
by simp
-
subsection {* Induction *}
-text {* FIXME *}
+text {*
+
+ Isabelle provides customized induction rules for recursive functions.
+ See \cite[\S3.5.4]{isa-tutorial}.
+*}
-section {* If it does not work *}
+section {* Full form definitions *}
text {*
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 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.
-*}
+ 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} @{text "f :: \<tau>"}\\%
+\cmd{where}\isanewline%
+\ \ {\it equations}\isanewline%
+\ \ \quad\vdots
+}}
-(*<*)types "\<tau>" = "nat \<Rightarrow> nat"
-(*>*)
-fun f :: "\<tau>"
-where
- (*<*)"f x = x" (*>*)text {* \vspace{-0.8cm}\emph{equations} *}
-
-text {* \noindent abbreviates *}
+\begin{isamarkuptext}
+\vspace*{1em}
+\noindent abbreviates
+\end{isamarkuptext}
-function (sequential) fo :: "\<tau>"
-where
- (*<*)"fo x = x" (*>*)txt {* \vspace{-0.8cm}\emph{equations} *}
-by pat_completeness auto
-termination by lexicographic_order
+\fbox{\parbox{\textwidth}{
+\noindent\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
+\cmd{where}\isanewline%
+\ \ {\it equations}\isanewline%
+\ \ \quad\vdots\\%
+\cmd{by} @{text "pat_completeness auto"}\\%
+\cmd{termination by} @{text "lexicographic_order"}
+}}
-text {*
- Some declarations and proofs have now become explicit:
+\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 @{text "pat_completeness"} and
+ @{text "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 @{text
+ "lexicographic_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.
*}
@@ -139,16 +153,16 @@
text {*
Consider the following function, which sums up natural numbers up to
- @{text "N"}, using a counter @{text "i"}
+ @{text "N"}, using a counter @{text "i"}:
*}
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"
- by pat_completeness auto
+by pat_completeness auto
text {*
- The {\tt lexicographic\_order} method fails on this example, because none of the
+ \noindent The @{text "lexicographic_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
@@ -161,21 +175,31 @@
is greater then @{text "n"}. Phrased differently, the expression
@{text "N + 1 - 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.
*}
termination
- by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
+by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
text {*
- 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 @{text relation} method takes a relation of
+ type @{typ "('a \<times> 'a) set"}, where @{typ "'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 @{term_type "measure"} is a very common way of
+ specifying termination relations in terms of a mapping into the
+ natural numbers.
+
+ After the invocation of @{text "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
+ @{text "auto"}.
+
+ Let us complicate the function a little, by adding some more
+ recursive calls:
*}
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -191,12 +215,13 @@
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 @{text "N"} and the above difference. The @{text "measures"}
- combinator generalizes @{text "measure"} by taking a list of measure functions.
+ the value of @{text "N"} and the above difference. The @{const
+ "measures"} combinator generalizes @{text "measure"} by taking a
+ list of measure functions.
*}
termination
- by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
+by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
section {* Mutual Recursion *}
@@ -206,13 +231,14 @@
in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
*}
-function even odd :: "nat \<Rightarrow> bool"
+function even :: "nat \<Rightarrow> bool"
+ and odd :: "nat \<Rightarrow> bool"
where
"even 0 = True"
| "odd 0 = False"
| "even (Suc n) = odd n"
| "odd (Suc n) = even n"
- by pat_completeness auto
+by pat_completeness auto
text {*
To solve the problem of mutual dependencies, Isabelle internally
@@ -224,23 +250,228 @@
*}
termination
- by (relation "measure (sum_case (%n. n) (%n. n))") auto
+by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)")
+ auto
+
+subsection {* Induction for mutual recursion *}
+
+text {*
+
+ 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 @{const even} and @{const odd}:
+*}
+
+lemma
+ "even n = (n mod 2 = 0)"
+ "odd n = (n mod 2 = 1)"
+
+txt {*
+ We apply simultaneous induction, specifying the induction variable
+ for both goals, separated by \cmd{and}: *}
+
+apply (induct n and n rule: even_odd.induct)
+
+txt {*
+ We get four subgoals, which correspond to the clauses in the
+ definition of @{const even} and @{const odd}:
+ @{subgoals[display,indent=0]}
+ Simplification solves the first two goals, leaving us with two
+ statements about the @{text "mod"} operation to prove:
+*}
+
+apply simp_all
+
+txt {*
+ @{subgoals[display,indent=0]}
+
+ \noindent These can be handeled by the descision procedure for
+ presburger arithmethic.
+
+*}
+
+apply presburger
+apply presburger
+done
+text {*
+ 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 @{const odd} (by substituting it with @{term "True"}, our
+ proof would have failed:
+*}
+
+lemma
+ "even n = (n mod 2 = 0)"
+ "True"
+apply (induct n rule: even_odd.induct)
+
+txt {*
+ \noindent Now the third subgoal is a dead end, since we have no
+ useful induction hypothesis:
+
+ @{subgoals[display,indent=0]}
+*}
+
+oops
+
+section {* More general patterns *}
+
+subsection {* Avoiding pattern splitting *}
+
+text {*
+
+ 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
+ @{const "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 @{term "T"}, @{term "F"}
+ and @{term "X"} for true, false and uncertain propositions.
+*}
+
+datatype P3 = T | F | X
+
+text {* Then the conjunction of such values can be defined as follows: *}
+
+fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
+where
+ "And T p = p"
+ "And p T = p"
+ "And p F = F"
+ "And F p = F"
+ "And X X = X"
-(* FIXME: Mutual induction *)
+text {*
+ This definition is useful, because the equations can directly be used
+ as rules to simplify expressions. But the patterns overlap, e.g.~the
+ expression @{term "And T T"} is matched by the first two
+ equations. By default, Isabelle makes the patterns disjoint by
+ splitting them up, producing instances:
+*}
+
+thm And.simps
+
+text {*
+ @{thm[indent=4] And.simps}
+
+ \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 @{const "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 @{term "And x F"}
+ can be simplified to @{term "F"} by the original specification, a
+ (manual) case split on @{term "x"} is now necessary.
+
+ \item The splitting also concerns the induction rule @{text
+ "And.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 @{term "f x = True"} and @{term "f x = 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:
+*}
+
+function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
+where
+ "And2 T p = p"
+ "And2 p T = p"
+ "And2 p F = F"
+ "And2 F p = F"
+ "And2 X X = X"
+
+txt {*
+ Now it is also time to look at the subgoals generated by a
+ function definition. In this case, they are:
+
+ @{subgoals[display,indent=0]}
+
+ The first subgoal expresses the completeness of the patterns. It has
+ the form of an elimination rule and states that every @{term x} of
+ the function's input type must match one of the patterns. It could
+ be equivalently stated as a disjunction of existential statements:
+@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
+ (\<exists>p. x = (F, p)) \<or> (x = (X, X))"} If the patterns just involve
+ datatypes, we can solve it with the @{text "pat_completeness"} method:
+*}
+
+apply pat_completeness
+
+txt {*
+ 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 @{text "auto"}.
+*}
+
+by auto
-
-section {* Nested recursion *}
+subsection {* Non-constructor patterns *}
text {* FIXME *}
-section {* More general patterns *}
+
+subsection {* Non-constructor patterns *}
text {* FIXME *}
+
+
+section {* Partiality *}
+
+text {*
+ In HOL, all functions are total. A function @{term "f"} applied to
+ @{term "x"} always has a value @{term "f x"}, and there is no notion
+ of undefinedness.
+
+ FIXME
+*}
+
+
+
+
+section {* Nested recursion *}
+
+text {*
+
+
+
+
+
+
+ FIXME *}
+
+
+
+
+
+
end
--- 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%
%