--- a/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 15:56:49 2007 +0100
@@ -73,7 +73,7 @@
\isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}}. Thus the functions \isa{sep} and
\isa{sep{\isadigit{1}}} are identical.
-Because of its pattern-matching syntax, \isacommand{fun} is also useful
+Because of its pattern matching syntax, \isacommand{fun} is also useful
for the definition of non-recursive functions:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -116,7 +116,7 @@
\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-Thus the order of arguments has no influence on whether
+The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
see elsewhere~\cite{bulwahnKN07}.
@@ -185,8 +185,8 @@
\begin{isamarkuptext}%
\noindent
The order of equations is important: it hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
-may not be expressible by pattern matching.
+\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, not all conditionals can be
+expressed by pattern matching.
A simple alternative is to replace \isa{if} by \isa{case},
which is also available for \isa{bool} and is not split automatically:%
@@ -316,16 +316,18 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Try proving the above lemma by structural induction, and you find that you
-need an additional case distinction.
+\noindent The proof goes smoothly because the induction rule
+follows the recursion of \isa{sep}. Try proving the above lemma by
+structural induction, and you find that you need an additional case
+distinction.
In general, the format of invoking recursion induction is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
+name of a function that takes an $n$ arguments. Usually the subgoal will
+contain the term $f x@1 \dots x@n$ but this need not be the case. The
induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
--- a/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 15:56:49 2007 +0100
@@ -57,7 +57,7 @@
@{prop"sep1 a [x] = [x]"}. Thus the functions @{const sep} and
@{const sep1} are identical.
-Because of its pattern-matching syntax, \isacommand{fun} is also useful
+Because of its pattern matching syntax, \isacommand{fun} is also useful
for the definition of non-recursive functions:
*}
@@ -98,7 +98,7 @@
"ack2 0 (Suc m) = ack2 (Suc 0) m" |
"ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
-text{* Thus the order of arguments has no influence on whether
+text{* The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
see elsewhere~\cite{bulwahnKN07}.
@@ -157,8 +157,8 @@
text{*\noindent
The order of equations is important: it hides the side condition
-@{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction
-may not be expressible by pattern matching.
+@{prop"n ~= (0::nat)"}. Unfortunately, not all conditionals can be
+expressed by pattern matching.
A simple alternative is to replace @{text "if"} by @{text case},
which is also available for @{typ bool} and is not split automatically:
@@ -233,17 +233,18 @@
apply simp_all;
done
-text{*
-Try proving the above lemma by structural induction, and you find that you
-need an additional case distinction.
+text{*\noindent The proof goes smoothly because the induction rule
+follows the recursion of @{const sep}. Try proving the above lemma by
+structural induction, and you find that you need an additional case
+distinction.
In general, the format of invoking recursion induction is
\begin{quote}
\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$-tuple. Usually the subgoal will
-contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
+name of a function that takes an $n$ arguments. Usually the subgoal will
+contain the term $f x@1 \dots x@n$ but this need not be the case. The
induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
--- a/doc-src/TutorialI/fp.tex Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Nov 02 15:56:49 2007 +0100
@@ -133,7 +133,7 @@
\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
-element and the remainder of a list. (However, pattern-matching is usually
+element and the remainder of a list. (However, pattern matching is usually
preferable to \isa{hd} and \isa{tl}.)
Also available are higher-order functions like \isa{map} and \isa{filter}.
Theory \isa{List} also contains
@@ -465,7 +465,7 @@
Although many total functions have a natural primitive recursive definition,
this is not always the case. Arbitrary total recursive functions can be
-defined by means of \isacommand{fun}: you can use full pattern-matching,
+defined by means of \isacommand{fun}: you can use full pattern matching,
recursion need not involve datatypes, and termination is proved by showing
that the arguments of all recursive calls are smaller in a suitable sense.
In this section we restrict ourselves to functions where Isabelle can prove