--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 12:29:10 2001 +0100
@@ -30,6 +30,7 @@
\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
+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
@@ -44,9 +45,10 @@
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-In contrast to ML, Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}). (Apart from the declaration-before-use
-restriction, the order of items in a theory file is unconstrained.) Function
+In contrast to many functional programming languages,
+Isabelle insists on explicit declarations of all functions
+(keyword \isacommand{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
\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
@@ -87,11 +89,11 @@
\end{warn}
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).
+syntax with keywords like \isacommand{datatype} and \isacommand{end}.
+% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
Embedded in this syntax are the types and formulae of HOL, whose syntax is
-extensible, e.g.\ by new user-defined infix operators
-(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
+extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
+To distinguish the two levels, everything
HOL-specific (terms and types) should be enclosed in
\texttt{"}\dots\texttt{"}.
To lessen this burden, quotation marks around a single identifier can be
@@ -174,9 +176,10 @@
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}
-~1.~rev~(rev~[])~=~[]\isanewline
-~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
+\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:
@@ -204,8 +207,9 @@
``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}
-~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
+\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}%
@@ -221,10 +225,10 @@
\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}%
\begin{isamarkuptxt}%
\noindent The keywords \isacommand{theorem}\index{*theorem} and
-\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
-the importance we attach to a proposition. We use the words
+\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
+the importance we attach to a proposition. Therefore we use the words
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
-interchangeably.
+interchangeably, too.
There are two variables that we could induct on: \isa{xs} and
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
@@ -272,8 +276,8 @@
% Instead of \isacommand{apply} followed by a dot, you can simply write
% \isacommand{by}\indexbold{by}, which we do most of the time.
-Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
-(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
+Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
+as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
\S\ref{sec:variables}.
@@ -313,7 +317,7 @@
\begin{isamarkuptext}%
\noindent
succeeds without further ado.
-Now we can go back and 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