1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri May 30 09:17:44 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri May 30 17:03:37 2008 +0200
1.3 @@ -123,7 +123,7 @@
1.4 The \cmd{fun} command provides a
1.5 convenient shorthand notation for simple function definitions. In
1.6 this mode, Isabelle tries to solve all the necessary proof obligations
1.7 - automatically. If a proof fails, the definition is
1.8 + automatically. If any proof fails, the definition is
1.9 rejected. This can either mean that the definition is indeed faulty,
1.10 or that the default proof procedures are just not smart enough (or
1.11 rather: not designed) to handle the definition.
1.12 @@ -141,7 +141,7 @@
1.13 \hspace*{2ex}\vdots\vspace*{6pt}
1.14 \end{minipage}\right]
1.15 \quad\equiv\quad
1.16 -\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
1.17 +\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}
1.18 \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
1.19 \cmd{where}\\%
1.20 \hspace*{2ex}{\it equations}\\%
1.21 @@ -211,7 +211,7 @@
1.22 We can use this expression as a measure function suitable to prove termination.
1.23 *}
1.24
1.25 -termination
1.26 +termination sum
1.27 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
1.28
1.29 txt {*
1.30 @@ -225,7 +225,7 @@
1.31 these are packed together into a tuple, as it happened in the above
1.32 example.
1.33
1.34 - The predefined function @{term_type "measure"} constructs a
1.35 + The predefined function @{term[source] "measure :: ('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"} constructs a
1.36 wellfounded relation from a mapping into the natural numbers (a
1.37 \emph{measure function}).
1.38
1.39 @@ -430,8 +430,8 @@
1.40 In proofs like this, the simultaneous induction is really essential:
1.41 Even if we are just interested in one of the results, the other
1.42 one is necessary to strengthen the induction hypothesis. If we leave
1.43 - out the statement about @{const odd} (by substituting it with @{term
1.44 - "True"}), the same proof fails:
1.45 + out the statement about @{const odd} and just write @{term True} instead,
1.46 + the same proof fails:
1.47 *}
1.48
1.49 lemma failed_attempt:
1.50 @@ -543,7 +543,7 @@
1.51 the function's input type must match at least one of the patterns\footnote{Completeness could
1.52 be equivalently stated as a disjunction of existential statements:
1.53 @{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
1.54 - (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve
1.55 + (\<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
1.56 datatypes, we can solve it with the @{text "pat_completeness"}
1.57 method:
1.58 *}
1.59 @@ -605,7 +605,6 @@
1.60 apply auto
1.61 done
1.62 termination by lexicographic_order
1.63 -
1.64 text {*
1.65 We can stretch the notion of pattern matching even more. The
1.66 following function is not a sensible functional program, but a
1.67 @@ -621,8 +620,8 @@
1.68 termination by (relation "{}") simp
1.69
1.70 text {*
1.71 - This general notion of pattern matching gives you the full freedom
1.72 - of mathematical specifications. However, as always, freedom should
1.73 + This general notion of pattern matching gives you a certain freedom
1.74 + in writing down specifications. However, as always, such freedom should
1.75 be used with care:
1.76
1.77 If we leave the area of constructor
1.78 @@ -1152,16 +1151,13 @@
1.79 text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the
1.80 list functions @{const rev} and @{const map}: *}
1.81
1.82 -function mirror :: "'a tree \<Rightarrow> 'a tree"
1.83 +fun mirror :: "'a tree \<Rightarrow> 'a tree"
1.84 where
1.85 "mirror (Leaf n) = Leaf n"
1.86 | "mirror (Branch l) = Branch (rev (map mirror l))"
1.87 -by pat_completeness auto
1.88 -
1.89
1.90 text {*
1.91 - \emph{Note: The handling of size functions is currently changing
1.92 - in the developers version of Isabelle. So this documentation is outdated.}
1.93 + Although the definition is accepted without problems, let us look at the termination proof:
1.94 *}
1.95
1.96 termination proof
1.97 @@ -1169,49 +1165,17 @@
1.98
1.99 As usual, we have to give a wellfounded relation, such that the
1.100 arguments of the recursive calls get smaller. But what exactly are
1.101 - the arguments of the recursive calls? Isabelle gives us the
1.102 + the arguments of the recursive calls when mirror is given as an
1.103 + argument to map? Isabelle gives us the
1.104 subgoals
1.105
1.106 @{subgoals[display,indent=0]}
1.107
1.108 - So Isabelle seems to know that @{const map} behaves nicely and only
1.109 + So the system seems to know that @{const map} only
1.110 applies the recursive call @{term "mirror"} to elements
1.111 - of @{term "l"}. Before we discuss where this knowledge comes from,
1.112 - let us finish the termination proof:
1.113 - *}
1.114 + of @{term "l"}, which is essential for the termination proof.
1.115
1.116 - show "wf (measure size)" by simp
1.117 -next
1.118 - fix f l and x :: "'a tree"
1.119 - assume "x \<in> set l"
1.120 - thus "(x, Branch l) \<in> measure size"
1.121 - apply simp
1.122 - txt {*
1.123 - Simplification returns the following subgoal:
1.124 -
1.125 - @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"}
1.126 -
1.127 - We are lacking a property about the function @{term
1.128 - tree_list_size}, which was generated automatically at the
1.129 - definition of the @{text tree} type. We should go back and prove
1.130 - it, by induction.
1.131 - *}
1.132 - (*<*)oops(*>*)
1.133 -
1.134 -text {*
1.135 - Now the whole termination proof is automatic:
1.136 - *}
1.137 -
1.138 -termination
1.139 - by lexicographic_order
1.140 -
1.141 -subsection {* Congruence Rules *}
1.142 -
1.143 -text {*
1.144 - Let's come back to the question how Isabelle knows about @{const
1.145 - map}.
1.146 -
1.147 - The knowledge about map is encoded in so-called congruence rules,
1.148 + This knowledge about map is encoded in so-called congruence rules,
1.149 which are special theorems known to the \cmd{function} command. The
1.150 rule for map is
1.151
1.152 @@ -1221,7 +1185,7 @@
1.153 map} are equal, if the list arguments are equal and the functions
1.154 coincide on the elements of the list. This means that for the value
1.155 @{term "map f l"} we only have to know how @{term f} behaves on
1.156 - @{term l}.
1.157 + the elements of @{term l}.
1.158
1.159 Usually, one such congruence rule is
1.160 needed for each higher-order construct that is used when defining
1.161 @@ -1238,10 +1202,11 @@
1.162
1.163 The constructs that are predefined in Isabelle, usually
1.164 come with the respective congruence rules.
1.165 - But if you define your own higher-order functions, you will have to
1.166 - come up with the congruence rules yourself, if you want to use your
1.167 + But if you define your own higher-order functions, you may have to
1.168 + state and prove the required congruence rules yourself, if you want to use your
1.169 functions in recursive definitions.
1.170 *}
1.171 +(*<*)oops(*>*)
1.172
1.173 subsection {* Congruence Rules and Evaluation Order *}
1.174
1.175 @@ -1265,7 +1230,7 @@
1.176 (*<*)by pat_completeness auto(*>*)
1.177
1.178 text {*
1.179 - As given above, the definition fails. The default configuration
1.180 + For this definition, the termination proof fails. The default configuration
1.181 specifies no congruence rule for disjunction. We have to add a
1.182 congruence rule that specifies left-to-right evaluation order:
1.183
2.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri May 30 09:17:44 2008 +0200
2.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri May 30 17:03:37 2008 +0200
2.3 @@ -188,7 +188,7 @@
2.4 The \cmd{fun} command provides a
2.5 convenient shorthand notation for simple function definitions. In
2.6 this mode, Isabelle tries to solve all the necessary proof obligations
2.7 - automatically. If a proof fails, the definition is
2.8 + automatically. If any proof fails, the definition is
2.9 rejected. This can either mean that the definition is indeed faulty,
2.10 or that the default proof procedures are just not smart enough (or
2.11 rather: not designed) to handle the definition.
2.12 @@ -206,7 +206,7 @@
2.13 \hspace*{2ex}\vdots\vspace*{6pt}
2.14 \end{minipage}\right]
2.15 \quad\equiv\quad
2.16 -\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
2.17 +\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}
2.18 \cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\%
2.19 \cmd{where}\\%
2.20 \hspace*{2ex}{\it equations}\\%
2.21 @@ -298,7 +298,7 @@
2.22 \end{isamarkuptext}%
2.23 \isamarkuptrue%
2.24 \isacommand{termination}\isamarkupfalse%
2.25 -\isanewline
2.26 +\ sum\isanewline
2.27 %
2.28 \isadelimproof
2.29 %
2.30 @@ -318,7 +318,7 @@
2.31 these are packed together into a tuple, as it happened in the above
2.32 example.
2.33
2.34 - The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} constructs a
2.35 + 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
2.36 wellfounded relation from a mapping into the natural numbers (a
2.37 \emph{measure function}).
2.38
2.39 @@ -593,7 +593,8 @@
2.40 In proofs like this, the simultaneous induction is really essential:
2.41 Even if we are just interested in one of the results, the other
2.42 one is necessary to strengthen the induction hypothesis. If we leave
2.43 - out the statement about \isa{odd} (by substituting it with \isa{True}), the same proof fails:%
2.44 + out the statement about \isa{odd} and just write \isa{True} instead,
2.45 + the same proof fails:%
2.46 \end{isamarkuptext}%
2.47 \isamarkuptrue%
2.48 \isacommand{lemma}\isamarkupfalse%
2.49 @@ -754,7 +755,7 @@
2.50 the form of an elimination rule and states that every \isa{x} of
2.51 the function's input type must match at least one of the patterns\footnote{Completeness could
2.52 be equivalently stated as a disjunction of existential statements:
2.53 -\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
2.54 +\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
2.55 datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness}
2.56 method:%
2.57 \end{isamarkuptxt}%
2.58 @@ -940,8 +941,8 @@
2.59 \endisadelimproof
2.60 %
2.61 \begin{isamarkuptext}%
2.62 -This general notion of pattern matching gives you the full freedom
2.63 - of mathematical specifications. However, as always, freedom should
2.64 +This general notion of pattern matching gives you a certain freedom
2.65 + in writing down specifications. However, as always, such freedom should
2.66 be used with care:
2.67
2.68 If we leave the area of constructor
2.69 @@ -1792,29 +1793,13 @@
2.70 list functions \isa{rev} and \isa{map}:%
2.71 \end{isamarkuptext}%
2.72 \isamarkuptrue%
2.73 -\isacommand{function}\isamarkupfalse%
2.74 +\isacommand{fun}\isamarkupfalse%
2.75 \ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
2.76 \isakeyword{where}\isanewline
2.77 \ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
2.78 -{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.79 -%
2.80 -\isadelimproof
2.81 -%
2.82 -\endisadelimproof
2.83 -%
2.84 -\isatagproof
2.85 -\isacommand{by}\isamarkupfalse%
2.86 -\ pat{\isacharunderscore}completeness\ auto%
2.87 -\endisatagproof
2.88 -{\isafoldproof}%
2.89 -%
2.90 -\isadelimproof
2.91 -%
2.92 -\endisadelimproof
2.93 -%
2.94 +{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
2.95 \begin{isamarkuptext}%
2.96 -\emph{Note: The handling of size functions is currently changing
2.97 - in the developers version of Isabelle. So this documentation is outdated.}%
2.98 +Although the definition is accepted without problems, let us look at the termination proof:%
2.99 \end{isamarkuptext}%
2.100 \isamarkuptrue%
2.101 \isacommand{termination}\isamarkupfalse%
2.102 @@ -1829,7 +1814,8 @@
2.103 \begin{isamarkuptxt}%
2.104 As usual, we have to give a wellfounded relation, such that the
2.105 arguments of the recursive calls get smaller. But what exactly are
2.106 - the arguments of the recursive calls? Isabelle gives us the
2.107 + the arguments of the recursive calls when mirror is given as an
2.108 + argument to map? Isabelle gives us the
2.109 subgoals
2.110
2.111 \begin{isabelle}%
2.112 @@ -1837,74 +1823,11 @@
2.113 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
2.114 \end{isabelle}
2.115
2.116 - So Isabelle seems to know that \isa{map} behaves nicely and only
2.117 + So the system seems to know that \isa{map} only
2.118 applies the recursive call \isa{mirror} to elements
2.119 - of \isa{l}. Before we discuss where this knowledge comes from,
2.120 - let us finish the termination proof:%
2.121 -\end{isamarkuptxt}%
2.122 -\isamarkuptrue%
2.123 -\ \ \isacommand{show}\isamarkupfalse%
2.124 -\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ size{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.125 -\ simp\isanewline
2.126 -\isacommand{next}\isamarkupfalse%
2.127 -\isanewline
2.128 -\ \ \isacommand{fix}\isamarkupfalse%
2.129 -\ f\ l\ \isakeyword{and}\ x\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
2.130 -\ \ \isacommand{assume}\isamarkupfalse%
2.131 -\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l{\isachardoublequoteclose}\isanewline
2.132 -\ \ \isacommand{thus}\isamarkupfalse%
2.133 -\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ measure\ size{\isachardoublequoteclose}\isanewline
2.134 -\ \ \ \ \isacommand{apply}\isamarkupfalse%
2.135 -\ simp%
2.136 -\begin{isamarkuptxt}%
2.137 -Simplification returns the following subgoal:
2.138 + of \isa{l}, which is essential for the termination proof.
2.139
2.140 - \begin{isabelle}%
2.141 -{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ size\ l{\isacharparenright}%
2.142 -\end{isabelle}
2.143 -
2.144 - We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the
2.145 - definition of the \isa{tree} type. We should go back and prove
2.146 - it, by induction.%
2.147 -\end{isamarkuptxt}%
2.148 -\isamarkuptrue%
2.149 -\ \ \ \ %
2.150 -\endisatagproof
2.151 -{\isafoldproof}%
2.152 -%
2.153 -\isadelimproof
2.154 -%
2.155 -\endisadelimproof
2.156 -%
2.157 -\begin{isamarkuptext}%
2.158 -Now the whole termination proof is automatic:%
2.159 -\end{isamarkuptext}%
2.160 -\isamarkuptrue%
2.161 -\isacommand{termination}\isamarkupfalse%
2.162 -\ \isanewline
2.163 -%
2.164 -\isadelimproof
2.165 -\ \ %
2.166 -\endisadelimproof
2.167 -%
2.168 -\isatagproof
2.169 -\isacommand{by}\isamarkupfalse%
2.170 -\ lexicographic{\isacharunderscore}order%
2.171 -\endisatagproof
2.172 -{\isafoldproof}%
2.173 -%
2.174 -\isadelimproof
2.175 -%
2.176 -\endisadelimproof
2.177 -%
2.178 -\isamarkupsubsection{Congruence Rules%
2.179 -}
2.180 -\isamarkuptrue%
2.181 -%
2.182 -\begin{isamarkuptext}%
2.183 -Let's come back to the question how Isabelle knows about \isa{map}.
2.184 -
2.185 - The knowledge about map is encoded in so-called congruence rules,
2.186 + This knowledge about map is encoded in so-called congruence rules,
2.187 which are special theorems known to the \cmd{function} command. The
2.188 rule for map is
2.189
2.190 @@ -1915,7 +1838,7 @@
2.191 You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions
2.192 coincide on the elements of the list. This means that for the value
2.193 \isa{map\ f\ l} we only have to know how \isa{f} behaves on
2.194 - \isa{l}.
2.195 + the elements of \isa{l}.
2.196
2.197 Usually, one such congruence rule is
2.198 needed for each higher-order construct that is used when defining
2.199 @@ -1934,12 +1857,19 @@
2.200
2.201 The constructs that are predefined in Isabelle, usually
2.202 come with the respective congruence rules.
2.203 - But if you define your own higher-order functions, you will have to
2.204 - come up with the congruence rules yourself, if you want to use your
2.205 + But if you define your own higher-order functions, you may have to
2.206 + state and prove the required congruence rules yourself, if you want to use your
2.207 functions in recursive definitions.%
2.208 -\end{isamarkuptext}%
2.209 +\end{isamarkuptxt}%
2.210 \isamarkuptrue%
2.211 %
2.212 +\endisatagproof
2.213 +{\isafoldproof}%
2.214 +%
2.215 +\isadelimproof
2.216 +%
2.217 +\endisadelimproof
2.218 +%
2.219 \isamarkupsubsection{Congruence Rules and Evaluation Order%
2.220 }
2.221 \isamarkuptrue%
2.222 @@ -1976,7 +1906,7 @@
2.223 \endisadelimproof
2.224 %
2.225 \begin{isamarkuptext}%
2.226 -As given above, the definition fails. The default configuration
2.227 +For this definition, the termination proof fails. The default configuration
2.228 specifies no congruence rule for disjunction. We have to add a
2.229 congruence rule that specifies left-to-right evaluation order:
2.230
3.1 --- a/doc-src/IsarAdvanced/Functions/intro.tex Fri May 30 09:17:44 2008 +0200
3.2 +++ b/doc-src/IsarAdvanced/Functions/intro.tex Fri May 30 17:03:37 2008 +0200
3.3 @@ -1,6 +1,6 @@
3.4 \section{Introduction}
3.5
3.6 -Since the release of Isabelle 2007, new facilities for recursive
3.7 +Starting from Isabelle 2007, new facilities for recursive
3.8 function definitions~\cite{krauss2006} are available. They provide
3.9 better support for general recursive definitions than previous
3.10 packages. But despite all tool support, function definitions can
3.11 @@ -11,7 +11,7 @@
3.12 defining functions quickly. For the more difficult definitions we will
3.13 discuss what problems can arise, and how they can be solved.
3.14
3.15 -We assume that you have mastered the basics of Isabelle/HOL
3.16 +We assume that you have mastered the fundamentals of Isabelle/HOL
3.17 and are able to write basic specifications and proofs. To start out
3.18 with Isabelle in general, consult the Isabelle/HOL tutorial
3.19 \cite{isa-tutorial}.
3.20 @@ -21,13 +21,13 @@
3.21 \paragraph{Structure of this tutorial.}
3.22 Section 2 introduces the syntax and basic operation of the \cmd{fun}
3.23 command, which provides full automation with reasonable default
3.24 -behavior. The impatient reader might want to stop after that
3.25 +behavior. The impatient reader can stop after that
3.26 section, and consult the remaining sections only when needed.
3.27 Section 3 introduces the more verbose \cmd{function} command which
3.28 -gives fine-grained control to the user. This form should be used
3.29 +gives fine-grained control. This form should be used
3.30 whenever the short form fails.
3.31 -After that we discuss different issues that are more specialized:
3.32 -termination, mutual and nested recursion, partiality, pattern matching
3.33 +After that we discuss more specialized issues:
3.34 +termination, mutual, nested and higher-order recursion, partiality, pattern matching
3.35 and others.
3.36
3.37
3.38 @@ -45,9 +45,9 @@
3.39
3.40
3.41
3.42 -The new \cmd{function} command, and its short form \cmd{fun} will
3.43 -replace the traditional \cmd{recdef} command \cite{slind-tfl} in the future. It solves
3.44 -a few of technical issues around \cmd{recdef}, and allows definitions
3.45 +The new \cmd{function} command, and its short form \cmd{fun} have mostly
3.46 +replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
3.47 +a few of technical issues around \cmd{recdef}, and allow definitions
3.48 which were not previously possible.
3.49
3.50