--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jul 26 16:43:02 2001 +0200
@@ -35,10 +35,11 @@
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
\begin{warn}
- Syntax annotations are a powerful but optional feature. You
+ Syntax annotations are can be powerful, but they are difficult to master and
+ are never necessary. You
could drop them from theory \isa{ToyList} and go back to the identifiers
\isa{Nil} and \isa{Cons}.
- We recommend that novices avoid using
+ Novices should avoid using
syntax annotations in their own theories.
\end{warn}
Next, two functions \isa{app} and \cdx{rev} are declared:%
@@ -49,7 +50,7 @@
\noindent
In contrast to many functional programming languages,
Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}). Apart from the declaration-before-use
+(keyword \commdx{consts}). Apart from the declaration-before-use
restriction, the order of items in a theory file is unconstrained. Function
\isa{app} is annotated with concrete syntax too. Instead of the
prefix syntax \isa{app\ xs\ ys} the infix
@@ -64,7 +65,7 @@
{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\noindent
+\noindent\index{*rev (constant)|(}\index{append function|(}
The equations for \isa{app} and \isa{rev} hardly need comments:
\isa{app} appends two lists and \isa{rev} reverses a list. The
keyword \commdx{primrec} indicates that the recursion is
@@ -80,16 +81,16 @@
% However, this is a subtle issue that we cannot discuss here further.
\begin{warn}
- As we have indicated, the requirement for total functions is not a gratuitous
- restriction but an essential characteristic of HOL\@. It is only
+ As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
because of totality that reasoning in HOL is comparatively easy. More
- generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+ generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
function definitions whose totality has not been proved) because they
quickly lead to inconsistencies. Instead, fixed constructs for introducing
types and functions are offered (such as \isacommand{datatype} and
\isacommand{primrec}) which are guaranteed to preserve consistency.
\end{warn}
+\index{syntax}%
A remark about syntax. The textual definition of a theory follows a fixed
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
@@ -105,7 +106,7 @@
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
+the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
\section{An Introductory Proof}
@@ -116,26 +117,23 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main Goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
+\subsubsection*{Main Goal}
Our goal is to show that reversing a list twice produces the original
-list. The input line%
+list.%
\end{isamarkuptext}%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
\begin{isamarkuptxt}%
\index{theorem@\isacommand {theorem} (command)|bold}%
-\index{*simp (attribute)|bold}
\noindent
-does several things. It
+This \isacommand{theorem} command does several things:
\begin{itemize}
\item
-establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
+It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
\item
-gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
-referred to,
+It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
\item
-and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
-proved) as a simplification rule, i.e.\ all future proofs involving
+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}.
@@ -152,7 +150,7 @@
The first three lines tell us that we are 0 steps into the proof of
theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
initial lines in this tutorial. The remaining lines display the current
-proof state.
+\rmindex{proof state}.
Until we have finished a proof, the proof state always looks like this:
\begin{isabelle}
$G$\isanewline
@@ -163,7 +161,8 @@
where $G$
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
+establish $G$.\index{subgoals}
+At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.
@@ -186,16 +185,18 @@
\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:
+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} are the local assumptions for this subgoal and {\it
- conclusion} is the actual proposition to be proved. Typical proof steps
-that add new assumptions are induction or case distinction. In our example
+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
@@ -256,14 +257,14 @@
}
%
\begin{isamarkuptext}%
-This time the canonical proof procedure%
+We again try the canonical proof procedure:%
\end{isamarkuptext}%
\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-leads to the desired message \isa{No\ subgoals{\isacharbang}}:
+It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
\begin{isabelle}%
xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
No\ subgoals{\isacharbang}%
@@ -307,11 +308,12 @@
and the missing lemma is associativity of \isa{{\isacharat}}.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+\isamarkupsubsubsection{Third Lemma%
}
%
\begin{isamarkuptext}%
-Abandoning the previous proof, the canonical proof procedure%
+Abandoning the previous attempt, the canonical proof procedure
+succeeds without further ado.%
\end{isamarkuptext}%
\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
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -319,8 +321,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-succeeds without further ado.
-Now we can prove the first lemma%
+Now we can prove the first lemma:%
\end{isamarkuptext}%
\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
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -328,7 +329,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-and then prove our main theorem:%
+Finally, we prove our main theorem:%
\end{isamarkuptext}%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -336,8 +337,9 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-The final \isacommand{end} tells Isabelle to close the current theory because
+The final \commdx{end} tells Isabelle to close the current theory because
we are finished with its development:%
+\index{*rev (constant)|)}\index{append function|)}%
\end{isamarkuptext}%
\isacommand{end}\isanewline
\end{isabellebody}%