author krauss Fri, 30 May 2008 17:03:37 +0200 changeset 27026 3602b81665b5 parent 27025 c1f9fb015ea5 child 27027 63f0b638355c
Updated function tutorial.
--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri May 30 09:17:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Fri May 30 17:03:37 2008 +0200
@@ -123,7 +123,7 @@
The \cmd{fun} command 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 fails, the definition is
+  automatically. If any proof fails, 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.
@@ -141,7 +141,7 @@
\hspace*{2ex}\vdots\vspace*{6pt}
\end{minipage}\right]
-\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
+\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}
\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
\cmd{where}\\%
\hspace*{2ex}{\it equations}\\%
@@ -211,7 +211,7 @@
We can use this expression as a measure function suitable to prove termination.
*}

-termination
+termination sum
apply (relation "measure (\<lambda>(i,N). N + 1 - i)")

txt {*
@@ -225,7 +225,7 @@
these are packed together into a tuple, as it happened in the above
example.

-  The predefined function @{term_type "measure"} constructs a
+  The predefined function @{term[source] "measure :: ('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"} constructs a
wellfounded relation from a mapping into the natural numbers (a
\emph{measure function}).

@@ -430,8 +430,8 @@
In proofs like this, the simultaneous induction is really essential:
Even if we are just interested in one of the results, the other
one is necessary to strengthen the induction hypothesis. If we leave
-  out the statement about @{const odd} (by substituting it with @{term
-  "True"}), the same proof fails:
+  out the statement about @{const odd} and just write @{term True} instead,
+  the same proof fails:
*}

lemma failed_attempt:
@@ -543,7 +543,7 @@
the function's input type must match at least one of the patterns\footnote{Completeness 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
+  (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}, and you can use the method @{text atomize_elim} to get that form instead.}. If the patterns just involve
datatypes, we can solve it with the @{text "pat_completeness"}
method:
*}
@@ -605,7 +605,6 @@
apply auto
done
termination by lexicographic_order
-
text {*
We can stretch the notion of pattern matching even more. The
following function is not a sensible functional program, but a
@@ -621,8 +620,8 @@
termination by (relation "{}") simp

text {*
-  This general notion of pattern matching gives you the full freedom
-  of mathematical specifications. However, as always, freedom should
+  This general notion of pattern matching gives you a certain freedom
+  in writing down specifications. However, as always, such freedom should
be used with care:

If we leave the area of constructor
@@ -1152,16 +1151,13 @@
text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the
list functions @{const rev} and @{const map}: *}

-function mirror :: "'a tree \<Rightarrow> 'a tree"
+fun mirror :: "'a tree \<Rightarrow> 'a tree"
where
"mirror (Leaf n) = Leaf n"
| "mirror (Branch l) = Branch (rev (map mirror l))"
-by pat_completeness auto
-

text {*
-  \emph{Note: The handling of size functions is currently changing
-  in the developers version of Isabelle. So this documentation is outdated.}
+  Although the definition is accepted without problems, let us look at the termination proof:
*}

termination proof
@@ -1169,49 +1165,17 @@

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
+  the arguments of the recursive calls when mirror is given as an
+  argument to map? Isabelle gives us the
subgoals

@{subgoals[display,indent=0]}

-  So Isabelle seems to know that @{const map} behaves nicely and only
+  So the system seems to know that @{const map} only
applies the recursive call @{term "mirror"} to elements
-  of @{term "l"}. Before we discuss where this knowledge comes from,
-  let us finish the termination proof:
-  *}
-
-  show "wf (measure size)" by simp
-next
-  fix f l and x :: "'a tree"
-  assume "x \<in> set l"
-  thus "(x, Branch l) \<in> measure size"
-    apply simp
-    txt {*
-      Simplification returns the following subgoal:
-
-      @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"}
+  of @{term "l"}, which is essential for the termination proof.

-      We are lacking a property about the function @{term
-      tree_list_size}, which was generated automatically at the
-      definition of the @{text tree} type. We should go back and prove
-      it, by induction.
-      *}
-    (*<*)oops(*>*)
-
-text {*
-    Now the whole termination proof is automatic:
-  *}
-
-termination
-  by lexicographic_order
-
-subsection {* Congruence Rules *}
-
-text {*
-  Let's come back to the question how Isabelle knows about @{const
-  map}.
-
-  The knowledge about map is encoded in so-called congruence rules,
+  This 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

@@ -1221,7 +1185,7 @@
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
@{term "map f l"} we only have to know how @{term f} behaves on
-  @{term l}.
+  the elements of @{term l}.

Usually, one such congruence rule is
needed for each higher-order construct that is used when defining
@@ -1238,10 +1202,11 @@

The constructs that are predefined in Isabelle, usually
come with the respective congruence rules.
-  But if you define your own higher-order functions, you will have to
-  come up with the congruence rules yourself, if you want to use your
+  But if you define your own higher-order functions, you may have to
+  state and prove the required congruence rules yourself, if you want to use your
functions in recursive definitions.
*}
+(*<*)oops(*>*)

subsection {* Congruence Rules and Evaluation Order *}

@@ -1265,7 +1230,7 @@
(*<*)by pat_completeness auto(*>*)

text {*
-  As given above, the definition fails. The default configuration
+  For this definition, the termination proof fails. The default configuration
specifies no congruence rule for disjunction. We have to add a
congruence rule that specifies left-to-right evaluation order:

--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Fri May 30 09:17:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Fri May 30 17:03:37 2008 +0200
@@ -188,7 +188,7 @@
The \cmd{fun} command 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 fails, the definition is
+  automatically. If any proof fails, 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.
@@ -206,7 +206,7 @@
\hspace*{2ex}\vdots\vspace*{6pt}
\end{minipage}\right]
-\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
+\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}
\cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%
\cmd{where}\\%
\hspace*{2ex}{\it equations}\\%
@@ -298,7 +298,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
-\isanewline
+\ sum\isanewline
%
%
@@ -318,7 +318,7 @@
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}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} constructs a
+  The predefined function \isa{{\isachardoublequote}measure\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}} constructs a
wellfounded relation from a mapping into the natural numbers (a
\emph{measure function}).

@@ -593,7 +593,8 @@
In proofs like this, the simultaneous induction is really essential:
Even if we are just interested in one of the results, the other
one is necessary to strengthen the induction hypothesis. If we leave
-  out the statement about \isa{odd} (by substituting it with \isa{True}), the same proof fails:%
+  the same proof fails:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -754,7 +755,7 @@
the form of an elimination rule and states that every \isa{x} of
the function's input type must match at least one of the patterns\footnote{Completeness 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
+\isa{{\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}}, and you can use the method \isa{atomize{\isacharunderscore}elim} to get that form instead.}. If the patterns just involve
datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness}
method:%
\end{isamarkuptxt}%
@@ -940,8 +941,8 @@
%
\begin{isamarkuptext}%
-This general notion of pattern matching gives you the full freedom
-  of mathematical specifications. However, as always, freedom should
+This general notion of pattern matching gives you a certain freedom
+  in writing down specifications. However, as always, such freedom should
be used with care:

If we leave the area of constructor
@@ -1792,29 +1793,13 @@
list functions \isa{rev} and \isa{map}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{function}\isamarkupfalse%
+\isacommand{fun}\isamarkupfalse%
\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-%
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto%
-\endisatagproof
-{\isafoldproof}%
-%
-%
-%
+{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\emph{Note: The handling of size functions is currently changing
-  in the developers version of Isabelle. So this documentation is outdated.}%
+Although the definition is accepted without problems, let us look at the termination proof:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{termination}\isamarkupfalse%
@@ -1829,7 +1814,8 @@
\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
+  the arguments of the recursive calls when mirror is given as an
+  argument to map? Isabelle gives us the
subgoals

\begin{isabelle}%
@@ -1837,74 +1823,11 @@
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
\end{isabelle}

-  So Isabelle seems to know that \isa{map} behaves nicely and only
+  So the system seems to know that \isa{map} only
applies the recursive call \isa{mirror} 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\ size{\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}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ measure\ size{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ simp%
-\begin{isamarkuptxt}%
-Simplification returns the following subgoal:
-
-      \begin{isabelle}%
-{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ size\ l{\isacharparenright}%
-\end{isabelle}
+  of \isa{l}, which is essential for the termination proof.

-      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%
-\ \ \ \ %
-\endisatagproof
-{\isafoldproof}%
-%
-%
-%
-\begin{isamarkuptext}%
-Now the whole termination proof is automatic:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{termination}\isamarkupfalse%
-\ \isanewline
-%
-\ \ %
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ lexicographic{\isacharunderscore}order%
-\endisatagproof
-{\isafoldproof}%
-%
-%
-%
-\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,
+  This 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

@@ -1915,7 +1838,7 @@
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}.
+  the elements of \isa{l}.

Usually, one such congruence rule is
needed for each higher-order construct that is used when defining
@@ -1934,12 +1857,19 @@

The constructs that are predefined in Isabelle, usually
come with the respective congruence rules.
-  But if you define your own higher-order functions, you will have to
-  come up with the congruence rules yourself, if you want to use your
+  But if you define your own higher-order functions, you may have to
+  state and prove the required congruence rules yourself, if you want to use your
functions in recursive definitions.%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
\isamarkuptrue%
%
+\endisatagproof
+{\isafoldproof}%
+%
+%
+%
\isamarkupsubsection{Congruence Rules and Evaluation Order%
}
\isamarkuptrue%
@@ -1976,7 +1906,7 @@
%
\begin{isamarkuptext}%
-As given above, the definition fails. The default configuration
+For this definition, the termination proof fails. The default configuration
specifies no congruence rule for disjunction. We have to add a
congruence rule that specifies left-to-right evaluation order:

--- a/doc-src/IsarAdvanced/Functions/intro.tex	Fri May 30 09:17:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/intro.tex	Fri May 30 17:03:37 2008 +0200
@@ -1,6 +1,6 @@
\section{Introduction}

-Since the release of Isabelle 2007, new facilities for recursive
+Starting from Isabelle 2007, new facilities for recursive
function definitions~\cite{krauss2006} are available. They provide
better support for general recursive definitions than previous
packages.  But despite all tool support, function definitions can
@@ -11,7 +11,7 @@
defining functions quickly. For the more difficult definitions we will
discuss what problems can arise, and how they can be solved.

-We assume that you have mastered the basics of Isabelle/HOL
+We assume that you have mastered the fundamentals of Isabelle/HOL
and are able to write basic specifications and proofs. To start out
with Isabelle in general, consult the Isabelle/HOL tutorial
\cite{isa-tutorial}.
@@ -21,13 +21,13 @@
\paragraph{Structure of this tutorial.}
Section 2 introduces the syntax and basic operation of the \cmd{fun}
command, which provides full automation with reasonable default
-behavior.  The impatient reader might want to stop after that
+behavior.  The impatient reader can stop after that
section, and consult the remaining sections only when needed.
Section 3 introduces the more verbose \cmd{function} command which
-gives fine-grained control to the user. This form should be used
+gives fine-grained control. This form should be used
whenever the short form fails.
-After that we discuss different issues that are more specialized:
-termination, mutual and nested recursion, partiality, pattern matching
+After that we discuss more specialized issues:
+termination, mutual, nested and higher-order recursion, partiality, pattern matching
and others.

@@ -45,9 +45,9 @@

-The new \cmd{function} command, and its short form \cmd{fun} will
-replace the traditional \cmd{recdef} command \cite{slind-tfl} in the future. It solves
-a few of technical issues around \cmd{recdef}, and allows definitions
+The new \cmd{function} command, and its short form \cmd{fun} have mostly
+replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
+a few of technical issues around \cmd{recdef}, and allow definitions
which were not previously possible.