--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Sep 01 19:09:44 2000 +0200
@@ -17,23 +17,24 @@
The datatype\index{*datatype} \isaindexbold{list} introduces two
constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
empty~list and the operator that adds an element to the front of a list. For
-example, the term \isa{Cons True (Cons False Nil)} is a value of type
-\isa{bool\ list}, namely the list with the elements \isa{True} and
+example, the term \isa{Cons True (Cons False Nil)} is a value of
+type \isa{bool\ list}, namely the list with the elements \isa{True} and
\isa{False}. Because this notation becomes unwieldy very quickly, the
datatype declaration is annotated with an alternative syntax: instead of
\isa{Nil} and \isa{Cons x xs} we can write
-\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{\mbox{x}\ {\isacharhash}\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
+\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
alternative syntax is the standard syntax. Thus the list \isa{Cons True
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
-\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{\mbox{x}\ {\isacharhash}\ \mbox{y}\ {\isacharhash}\ \mbox{z}} is read as \isa{x
-\# (y \# z)} and not as \isa{(x \# y) \# z}.
+\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}.
\begin{warn}
Syntax annotations are a powerful but completely optional feature. You
could drop them from theory \isa{ToyList} and go back to the identifiers
- \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
+ \isa{Nil} and \isa{Cons}. However, lists are such a
+ central datatype
that their syntax is highly customized. We recommend that novices should
not use syntax annotations in their own theories.
\end{warn}
@@ -46,9 +47,9 @@
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
-\isa{app} is annotated with concrete syntax too. Instead of the prefix
+\isa{op\ {\isacharat}} is annotated with concrete syntax too. Instead of the prefix
syntax \isa{app xs ys} the infix
-\isa{\mbox{xs}\ {\isacharat}\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
form. Both functions are defined recursively:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
@@ -60,8 +61,8 @@
{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-The equations for \isa{app} and \isa{rev} hardly need comments:
-\isa{app} appends two lists and \isa{rev} reverses a list. The keyword
+The equations for \isa{op\ {\isacharat}} and \isa{rev} hardly need comments:
+\isa{op\ {\isacharat}} appends two lists and \isa{rev} reverses a list. The keyword
\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
particularly primitive kind where each recursive call peels off a datatype
constructor from one of the arguments. Thus the
@@ -110,7 +111,7 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}
+\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}
Our goal is to show that reversing a list twice produces the original
list. The input line%
@@ -120,13 +121,14 @@
\index{*theorem|bold}\index{*simp (attribute)|bold}
\begin{itemize}
\item
-establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
-\item
-gives that theorem the name \isa{rev_rev} by which it can be referred to,
+establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
\item
-and tells Isabelle (via \isa{[simp]}) to use the theorem (once it has been
+gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
+referred to,
+\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
-simplification will replace occurrences of \isa{rev(rev xs)} by
+simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
\isa{xs}.
The name and the simplification attribute are optional.
@@ -140,7 +142,7 @@
~1.~rev~(rev~xs)~=~xs
\end{isabelle}
The first three lines tell us that we are 0 steps into the proof of
-theorem \isa{rev_rev}; for compactness reasons we rarely show these
+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.
Until we have finished a proof, the proof state always looks like this:
@@ -153,11 +155,11 @@
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 0} there is only one subgoal, which is
+establish $G$. 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.
-Let us now get back to \isa{rev(rev xs) = xs}. Properties of recursively
+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
not much choice except to induct on \isa{xs}:%
\end{isamarkuptxt}%
@@ -171,7 +173,7 @@
(\isa{Cons}):
\begin{isabelle}
~1.~rev~(rev~[])~=~[]\isanewline
-~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
+~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
\end{isabelle}
The induction step is an example of the general format of a subgoal:
@@ -184,12 +186,11 @@
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 only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ \mbox{list}{\isacharparenright}\ {\isacharequal}\ \mbox{list}}, where \isa{list} is a variable name chosen by Isabelle. If there
+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.
-%FIXME indent!
Let us try to solve both goals automatically:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
@@ -198,7 +199,7 @@
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 [] = []}) and disappears; the simplified version
+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
@@ -206,7 +207,7 @@
In order to simplify this subgoal further, a lemma suggests itself.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
+\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}}
%
\begin{isamarkuptext}%
After abandoning the above proof attempt\indexbold{abandon
@@ -222,7 +223,7 @@
interchangeably.
There are two variables that we could induct on: \isa{xs} and
-\isa{ys}. Because \isa{\at} is defined by recursion on
+\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
the first argument, \isa{xs} is the correct one:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
@@ -241,7 +242,7 @@
the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Second lemma: \texttt{xs \at~[] = xs}}
+\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
%
\begin{isamarkuptext}%
This time the canonical proof procedure%
@@ -251,7 +252,7 @@
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-leads to the desired message \isa{No subgoals!}:
+leads to the desired message \isa{No\ subgoals{\isacharbang}}:
\begin{isabelle}
xs~@~[]~=~xs\isanewline
No~subgoals!
@@ -263,12 +264,12 @@
\begin{isamarkuptext}%
\noindent\indexbold{$Isar@\texttt{.}}%
As a result of that final dot, Isabelle associates the lemma
-just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
-printed out after the final dot) the free variable \isa{xs} has been
-replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+just proved with its name. Instead of \isacommand{apply}
followed by a dot, you can simply write \isacommand{by}\indexbold{by},
-which we do most of the time.
+which we do most of the time. Notice that in lemma \isa{app{\isacharunderscore}Nil\isadigit{2}}
+(as printed out after the final dot) the free variable \isa{xs} has been
+replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
+\S\ref{sec:variables}.
Going back to the proof of the first lemma%
\end{isamarkuptext}%
@@ -284,16 +285,16 @@
~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
\end{isabelle}
-Now we need to remember that \isa{\at} associates to the right, and that
-\isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
+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~\#~[]))%
+~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
\end{isabelle}
-and the missing lemma is associativity of \isa{\at}.%
+and the missing lemma is associativity of \isa{{\isacharat}}.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
+\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}}
%
\begin{isamarkuptext}%
Abandoning the previous proof, the canonical proof procedure%
@@ -318,7 +319,7 @@
\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-The final \isa{end} tells Isabelle to close the current theory because
+The final \isacommand{end} tells Isabelle to close the current theory because
we are finished with its development:%
\end{isamarkuptext}%
\isacommand{end}\isanewline