--- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu Aug 18 11:17:34 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Thu Aug 18 11:17:35 2005 +0200
@@ -70,10 +70,10 @@
The behaviour of \cdx{itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive: it can be
+empty. Note that \isa{Itrev{\isachardot}itrev} is tail-recursive: it can be
compiled into a loop.
-Naturally, we would like to show that \isa{itrev} does indeed reverse
+Naturally, we would like to show that \isa{Itrev{\isachardot}itrev} does indeed reverse
its first argument provided the second one is empty:%
\end{isamarkuptext}%
\isamarkupfalse%
@@ -98,7 +98,8 @@
the induction step:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
\end{isabelle}
The induction hypothesis is too weak. The fixed
argument,~\isa{{\isacharbrackleft}{\isacharbrackright}}, prevents it from rewriting the conclusion.
@@ -106,7 +107,7 @@
\begin{quote}\index{generalizing induction formulae}%
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
-Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
+Of course one cannot do this na\"{\i}vely: \isa{Itrev{\isachardot}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
just not true. The correct generalization is%
\end{isamarkuptxt}%
%
@@ -138,8 +139,8 @@
not there:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
\end{isabelle}
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
@@ -185,7 +186,7 @@
those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just
-proved: the more complex notion (\isa{itrev}) is on the left-hand
+proved: the more complex notion (\isa{Itrev{\isachardot}itrev}) is on the left-hand
side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
another, albeit weak heuristic that is not restricted to induction:
\begin{quote}
@@ -193,8 +194,8 @@
than the left-hand side.}
\end{quote}
This heuristic is tricky to apply because it is not obvious that
-\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
-happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
+\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{Itrev{\isachardot}itrev\ xs\ ys}. But see what
+happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ Itrev{\isachardot}itrev\ xs\ ys}!
If you have tried these heuristics and still find your
induction does not go through, and no obvious lemma suggests itself, you may