--- a/doc-src/TutorialI/Misc/document/Itrev.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Nov 08 00:00:47 2010 +0100
@@ -46,15 +46,15 @@
\emph{Do induction on argument number $i$ if the function is defined by
recursion in argument number $i$.}
\end{quote}
-When we look at the proof of \isa{{\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys{\isacharat}zs{\isacharparenright}}
+When we look at the proof of \isa{{\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}ys{\isaliteral{40}{\isacharat}}zs{\isaliteral{29}{\isacharparenright}}}
in \S\ref{sec:intro-proof} we find
\begin{itemize}
-\item \isa{{\isacharat}} is recursive in
+\item \isa{{\isaliteral{40}{\isacharat}}} is recursive in
the first argument
\item \isa{xs} occurs only as the first argument of
-\isa{{\isacharat}}
+\isa{{\isaliteral{40}{\isacharat}}}
\item both \isa{ys} and \isa{zs} occur at least once as
-the second argument of \isa{{\isacharat}}
+the second argument of \isa{{\isaliteral{40}{\isacharat}}}
\end{itemize}
Hence it is natural to perform induction on~\isa{xs}.
@@ -65,16 +65,16 @@
step to go through. Let us illustrate the idea with an example.
Function \cdx{rev} has quadratic worst-case running time
-because it calls function \isa{{\isacharat}} for each element of the list and
-\isa{{\isacharat}} is linear in its first argument. A linear time version of
+because it calls function \isa{{\isaliteral{40}{\isacharat}}} for each element of the list and
+\isa{{\isaliteral{40}{\isacharat}}} is linear in its first argument. A linear time version of
\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only~\isa{{\isacharhash}}:%
+gradually, using only~\isa{{\isaliteral{23}{\isacharhash}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
-\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}%
+\ itrev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\noindent
The behaviour of \cdx{itrev} is simple: it reverses
@@ -88,7 +88,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}itrev\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -101,22 +101,22 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}%
\begin{isamarkuptxt}%
\noindent
Unfortunately, this attempt does not prove
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}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ itrev\ list\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}%
\end{isabelle}
The induction hypothesis is too weak. The fixed
-argument,~\isa{{\isacharbrackleft}{\isacharbrackright}}, prevents it from rewriting the conclusion.
+argument,~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, prevents it from rewriting the conclusion.
This example suggests a heuristic:
\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\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs} is
just not true. The correct generalization is%
\end{isamarkuptxt}%
\isamarkuptrue%
@@ -128,7 +128,7 @@
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -137,7 +137,7 @@
%
\begin{isamarkuptxt}%
\noindent
-If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
+If \isa{ys} is replaced by \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, the right-hand side simplifies to
\isa{rev\ xs}, as required.
In this instance it was easy to guess the right generalization.
@@ -147,14 +147,14 @@
induction, and we repeat our proof attempt. Unfortunately, we are still
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%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\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
the subgoal, but the induction hypothesis needs to be applied with
-\isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem
+\isa{a\ {\isaliteral{23}{\isacharhash}}\ ys} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
\isamarkuptrue%
@@ -166,7 +166,7 @@
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}ys{\isaliteral{2E}{\isachardot}}\ itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -203,8 +203,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\ {\isaliteral{40}{\isacharat}}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
+happens if you try to prove \isa{rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ 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