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

 %
 \begin{isamarkuptext}%
 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.
 
   By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or

 \cmd{where}\\%
 \hspace*{2ex}{\it equations}\\%
 \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}\\%
 \hspace*{2ex}\vdots\\%
 \cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\%

 
   We can use this expression as a measure function suitable to prove termination.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
-\isanewline
+\ sum\isanewline
 %
 \isadelimproof
 %
 \endisadelimproof
 %

   type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of
   the function. If the function has multiple curried arguments, then
   these are packed together into a tuple, as it happened in the above
   example.
 
-  The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\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}). 
 
   After the invocation of \isa{relation}, we must prove that (a)
   the relation we supplied is wellfounded, and (b) that the arguments

 %
 \begin{isamarkuptext}%
 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%
 \ failed{\isacharunderscore}attempt{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

 
   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 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}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%

 \isadelimproof
 %
 \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
   patterns, we have effectively departed from the world of functional
   programming. This means that it is no longer possible to use the

 \begin{isamarkuptext}%
 \noindent We can define a function which swaps the left and right subtrees recursively, using the 
   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
-%
-\begin{isamarkuptext}%
-\emph{Note: The handling of size functions is currently changing 
-  in the developers version of Isabelle. So this documentation is outdated.}%
+{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+Although the definition is accepted without problems, let us look at the termination proof:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
 %
 \isadelimproof

 \isacommand{proof}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 As usual, we have to give a wellfounded relation, such that the
   arguments of the recursive calls get smaller. But what exactly are
-  the arguments of the recursive calls? Isabelle gives us the
+  the arguments of the recursive calls when mirror is given as an
+  argument to map? Isabelle gives us the
   subgoals
 
   \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline
 \ {\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} 
-
-      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,
+  of \isa{l}, which is essential for the termination proof.
+
+  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
 
   \begin{isabelle}%
 {\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys%
 \end{isabelle}
 
   You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions
   coincide on the elements of the list. This means that for the value 
   \isa{map\ f\ l} we only have to know how \isa{f} behaves on
-  \isa{l}.
+  the elements of \isa{l}.
 
   Usually, one such congruence rule is
   needed for each higher-order construct that is used when defining
   new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handled by this mechanism. The congruence
   rule for \isa{If} states that the \isa{then} branch is only

   Congruence rules can be added to the
   function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute.
 
   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}%
-\isamarkuptrue%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
 \isamarkupsubsection{Congruence Rules and Evaluation Order%
 }
 \isamarkuptrue%
 %

 \isadelimproof
 %
 \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:
 
   \vspace{1ex}
   \noindent \isa{{\isasymlbrakk}{\isacharquery}P\ {\isacharequal}\ {\isacharquery}P{\isacharprime}{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharequal}\ {\isacharquery}Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}P\ {\isasymor}\ {\isacharquery}Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}P{\isacharprime}\ {\isasymor}\ {\isacharquery}Q{\isacharprime}{\isacharparenright}}\hfill(\isa{disj{\isacharunderscore}cong})