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]
 \quad\equiv\quad
-\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]
 \quad\equiv\quad
-\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
 %
 \isadelimproof
 %
@@ -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:%
+  out the statement about \isa{odd} and just write \isa{True} instead,
+  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 @@
 \endisadelimproof
 %
 \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
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
+{\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}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Now the whole termination proof is automatic:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{termination}\isamarkupfalse%
-\ \isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ lexicographic{\isacharunderscore}order%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isamarkupsubsection{Congruence Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Let's come back to the question how Isabelle knows about \isa{map}.
-
-  The knowledge about map is encoded in so-called congruence rules,
+  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}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
 \isamarkupsubsection{Congruence Rules and Evaluation Order%
 }
 \isamarkuptrue%
@@ -1976,7 +1906,7 @@
 \endisadelimproof
 %
 \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.