--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Feb 01 18:01:57 2005 +0100
@@ -136,98 +136,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\index{theorem@\isacommand {theorem} (command)|bold}%
-\noindent
-This \isacommand{theorem} command does several things:
-\begin{itemize}
-\item
-It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
-\item
-It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
-\item
-It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
-simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
-\isa{xs}.
-\end{itemize}
-The name and the simplification attribute are optional.
-Isabelle's response is to print the initial proof state consisting
-of some header information (like how many subgoals there are) followed by
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs%
-\end{isabelle}
-For compactness reasons we omit the header in this tutorial.
-Until we have finished a proof, the \rmindex{proof state} proper
-always looks like this:
-\begin{isabelle}
-~1.~$G\sb{1}$\isanewline
-~~\vdots~~\isanewline
-~$n$.~$G\sb{n}$
-\end{isabelle}
-The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
-that we need to prove to establish the main goal.\index{subgoals}
-Initially there is only one subgoal, which is identical with the
-main goal. (If you always want to see the main goal as well,
-set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
---- this flag used to be set by default.)
-
-Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
-defined functions are best established by induction. In this case there is
-nothing obvious except induction on \isa{xs}:%
-\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent\index{*induct_tac (method)}%
-This tells Isabelle to perform induction on variable \isa{xs}. The suffix
-\isa{tac} stands for \textbf{tactic},\index{tactics}
-a synonym for ``theorem proving function''.
-By default, induction acts on the first subgoal. The new proof state contains
-two subgoals, namely the base case (\isa{Nil}) and the induction step
-(\isa{Cons}):
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
-\end{isabelle}
-
-The induction step is an example of the general format of a subgoal:\index{subgoals}
-\begin{isabelle}
-~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
-\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
-The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
-ignored most of the time, or simply treated as a list of variables local to
-this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
-The {\it assumptions}\index{assumptions!of subgoal}
-are the local assumptions for this subgoal and {\it
- conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
-Typical proof steps
-that add new assumptions are induction and case distinction. In our example
-the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
-are multiple assumptions, they are enclosed in the bracket pair
-\indexboldpos{\isasymlbrakk}{$Isabrl} and
-\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
-
-Let us try to solve both goals automatically:%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-This command tells Isabelle to apply a proof strategy called
-\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
-simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
-to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
-of subgoal~2 becomes the new subgoal~1:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
-\end{isabelle}
-In order to simplify this subgoal further, a lemma suggests itself.%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
@@ -242,35 +154,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent The keywords \commdx{theorem} and
-\commdx{lemma} are interchangeable and merely indicate
-the importance we attach to a proposition. Therefore we use the words
-\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
-
-There are two variables that we could induct on: \isa{xs} and
-\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
-the first argument, \isa{xs} is the correct one:%
-\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-This time not even the base case is solved automatically:%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
-\end{isabelle}
-Again, we need to abandon this proof attempt and prove another simple lemma
-first. In the future the step of abandoning an incomplete proof before
-embarking on the proof of a lemma usually remains implicit.%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
@@ -284,21 +171,10 @@
\isamarkuptrue%
\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
-\begin{isabelle}%
-xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
-No\ subgoals{\isacharbang}%
-\end{isabelle}
-We still need to confirm that the proof is now finished:%
-\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{done}\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -318,27 +194,8 @@
\isamarkuptrue%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-we find that this time \isa{auto} solves the base case, but the
-induction step merely simplifies to
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
-\end{isabelle}
-Now we need to remember that \isa{{\isacharat}} associates to the right, and that
-\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
-in their \isacommand{infixr} annotation). Thus the conclusion really is
-\begin{isabelle}
-~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
-\end{isabelle}
-and the missing lemma is associativity of \isa{{\isacharat}}.%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
@@ -353,11 +210,9 @@
\isamarkuptrue%
\isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -366,11 +221,9 @@
\isamarkuptrue%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -379,11 +232,9 @@
\isamarkuptrue%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent