--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{theory}~ToyList~=~PreList:%
+\isacommand{theory}\ ToyList\ =\ PreList:%
\begin{isamarkuptext}%
\noindent
HOL already has a predefined theory of lists called \isa{List} ---
@@ -9,25 +9,25 @@
theory that contains pretty much everything but lists, thus avoiding
ambiguities caused by defining lists twice.%
\end{isamarkuptext}%
-\isacommand{datatype}~'a~list~=~Nil~~~~~~~~~~~~~~~~~~~~~~~~~~({"}[]{"})\isanewline
-~~~~~~~~~~~~~~~~~|~Cons~'a~{"}'a~list{"}~~~~~~~~~~~~(\isakeyword{infixr}~{"}\#{"}~65)%
+\isacommand{datatype}\ 'a\ list\ =\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}[]{"})\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Cons\ 'a\ {"}'a\ list{"}\ \ \ \ \ \ \ \ \ \ \ \ (\isakeyword{infixr}\ {"}\#{"}\ 65)%
\begin{isamarkuptext}%
\noindent
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
+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
\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{Nil} and \isa{Cons x xs} we can write
\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{$x$~\#~$xs$}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{x\ \#\ 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 \# False \# []}. The annotation
+(Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation
\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{$x$ \# $y$ \# $z$} is read as \isa{$x$
-\# ($y$ \# $z$)} and not as \isa{($x$ \# $y$) \# $z$}.
+the right, i.e.\ the term \isa{x\ \#\ y\ \#\ z} is read as \isa{x
+\# (y \# z)} and not as \isa{(x \# y) \# z}.
\begin{warn}
Syntax annotations are a powerful but completely optional feature. You
@@ -38,25 +38,25 @@
\end{warn}
Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
\end{isamarkuptext}%
-\isacommand{consts}~app~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}~~~(\isakeyword{infixr}~{"}@{"}~65)\isanewline
-~~~~~~~rev~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}%
+\isacommand{consts}\ app\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\ \ \ (\isakeyword{infixr}\ {"}@{"}\ 65)\isanewline
+\ \ \ \ \ \ \ rev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}%
\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
\isa{app} is annotated with concrete syntax too. Instead of the prefix
-syntax \isa{app~$xs$~$ys$} the infix
-\isa{$xs$~\at~$ys$}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+syntax \isa{app xs ys} the infix
+\isa{xs\ @\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
form. Both functions are defined recursively:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
-{"}[]~@~ys~~~~~~~=~ys{"}\isanewline
-{"}(x~\#~xs)~@~ys~=~x~\#~(xs~@~ys){"}\isanewline
+{"}[]\ @\ ys\ \ \ \ \ \ \ =\ ys{"}\isanewline
+{"}(x\ \#\ xs)\ @\ ys\ =\ x\ \#\ (xs\ @\ ys){"}\isanewline
\isanewline
\isacommand{primrec}\isanewline
-{"}rev~[]~~~~~~~~=~[]{"}\isanewline
-{"}rev~(x~\#~xs)~~=~(rev~xs)~@~(x~\#~[]){"}%
+{"}rev\ []\ \ \ \ \ \ \ \ =\ []{"}\isanewline
+{"}rev\ (x\ \#\ xs)\ \ =\ (rev\ xs)\ @\ (x\ \#\ []){"}%
\begin{isamarkuptext}%
\noindent
The equations for \isa{app} and \isa{rev} hardly need comments:
@@ -94,7 +94,7 @@
To lessen this burden, quotation marks around a single identifier can be
dropped, unless the identifier happens to be a keyword, as in%
\end{isamarkuptext}%
-\isacommand{consts}~{"}end{"}~::~{"}'a~list~{\isasymRightarrow}~'a{"}%
+\isacommand{consts}\ {"}end{"}\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}%
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
@@ -114,7 +114,7 @@
Our goal is to show that reversing a list twice produces the original
list. The input line%
\end{isamarkuptext}%
-\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}%
+\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}%
\begin{isamarkuptxt}%
\index{*theorem|bold}\index{*simp (attribute)|bold}
\begin{itemize}
@@ -160,7 +160,7 @@
defined functions are best established by induction. In this case there is
not much choice except to induct on \isa{xs}:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs)%
+\isacommand{apply}(induct\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent\index{*induct_tac}%
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
@@ -183,8 +183,7 @@
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 (rev list) =
- list}, where \isa{list} is a variable name chosen by Isabelle. If there
+the only assumption is the induction hypothesis \isa{rev\ (rev\ list)\ =\ 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.
@@ -213,7 +212,7 @@
proof}\indexbold{proof!abandon} (at the shell level type
\isacommand{oops}\indexbold{*oops}) we start a new proof:%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}%
\begin{isamarkuptxt}%
\noindent The keywords \isacommand{theorem}\index{*theorem} and
\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
@@ -225,7 +224,7 @@
\isa{ys}. Because \isa{\at} is defined by recursion on
the first argument, \isa{xs} is the correct one:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs)%
+\isacommand{apply}(induct\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent
This time not even the base case is solved automatically:%
@@ -246,8 +245,8 @@
This time the canonical proof procedure%
\end{isamarkuptext}%
-\isacommand{lemma}~app\_Nil2~[simp]:~{"}xs~@~[]~=~xs{"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ app\_Nil2\ [simp]:\ {"}xs\ @\ []\ =\ xs{"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{apply}(auto)%
\begin{isamarkuptxt}%
\noindent
@@ -272,8 +271,8 @@
Going back to the proof of the first lemma%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{apply}(auto)%
\begin{isamarkuptxt}%
\noindent
@@ -300,8 +299,8 @@
\begin{comment}
\isacommand{oops}%
\end{comment}
-\isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ app\_assoc\ [simp]:\ {"}(xs\ @\ ys)\ @\ zs\ =\ xs\ @\ (ys\ @\ zs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
@@ -309,15 +308,15 @@
Now we can go back and prove the first lemma%
\end{isamarkuptext}%
-\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
and then solve our main theorem:%
\end{isamarkuptext}%
-\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline
-\isacommand{apply}(induct\_tac~xs)\isanewline
+\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}\isanewline
+\isacommand{apply}(induct\_tac\ xs)\isanewline
\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent