1.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -30,6 +30,7 @@
1.4 \isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
1.5 the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
1.6 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
1.7 +The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
1.8
1.9 \begin{warn}
1.10 Syntax annotations are a powerful but optional feature. You
1.11 @@ -44,9 +45,10 @@
1.12 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
1.13 \begin{isamarkuptext}%
1.14 \noindent
1.15 -In contrast to ML, Isabelle insists on explicit declarations of all functions
1.16 -(keyword \isacommand{consts}). (Apart from the declaration-before-use
1.17 -restriction, the order of items in a theory file is unconstrained.) Function
1.18 +In contrast to many functional programming languages,
1.19 +Isabelle insists on explicit declarations of all functions
1.20 +(keyword \isacommand{consts}). Apart from the declaration-before-use
1.21 +restriction, the order of items in a theory file is unconstrained. Function
1.22 \isa{app} is annotated with concrete syntax too. Instead of the
1.23 prefix syntax \isa{app\ xs\ ys} the infix
1.24 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
1.25 @@ -87,11 +89,11 @@
1.26 \end{warn}
1.27
1.28 A remark about syntax. The textual definition of a theory follows a fixed
1.29 -syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
1.30 -Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
1.31 +syntax with keywords like \isacommand{datatype} and \isacommand{end}.
1.32 +% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
1.33 Embedded in this syntax are the types and formulae of HOL, whose syntax is
1.34 -extensible, e.g.\ by new user-defined infix operators
1.35 -(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
1.36 +extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
1.37 +To distinguish the two levels, everything
1.38 HOL-specific (terms and types) should be enclosed in
1.39 \texttt{"}\dots\texttt{"}.
1.40 To lessen this burden, quotation marks around a single identifier can be
1.41 @@ -174,9 +176,10 @@
1.42 By default, induction acts on the first subgoal. The new proof state contains
1.43 two subgoals, namely the base case (\isa{Nil}) and the induction step
1.44 (\isa{Cons}):
1.45 -\begin{isabelle}
1.46 -~1.~rev~(rev~[])~=~[]\isanewline
1.47 -~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
1.48 +\begin{isabelle}%
1.49 +\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
1.50 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
1.51 +\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%
1.52 \end{isabelle}
1.53
1.54 The induction step is an example of the general format of a subgoal:
1.55 @@ -204,8 +207,9 @@
1.56 ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
1.57 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
1.58 of subgoal~2 becomes the new subgoal~1:
1.59 -\begin{isabelle}
1.60 -~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
1.61 +\begin{isabelle}%
1.62 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
1.63 +\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%
1.64 \end{isabelle}
1.65 In order to simplify this subgoal further, a lemma suggests itself.%
1.66 \end{isamarkuptxt}%
1.67 @@ -221,10 +225,10 @@
1.68 \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}%
1.69 \begin{isamarkuptxt}%
1.70 \noindent The keywords \isacommand{theorem}\index{*theorem} and
1.71 -\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
1.72 -the importance we attach to a proposition. We use the words
1.73 +\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
1.74 +the importance we attach to a proposition. Therefore we use the words
1.75 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
1.76 -interchangeably.
1.77 +interchangeably, too.
1.78
1.79 There are two variables that we could induct on: \isa{xs} and
1.80 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
1.81 @@ -272,8 +276,8 @@
1.82
1.83 % Instead of \isacommand{apply} followed by a dot, you can simply write
1.84 % \isacommand{by}\indexbold{by}, which we do most of the time.
1.85 -Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
1.86 -(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
1.87 +Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
1.88 +as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
1.89 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
1.90 \S\ref{sec:variables}.
1.91
1.92 @@ -313,7 +317,7 @@
1.93 \begin{isamarkuptext}%
1.94 \noindent
1.95 succeeds without further ado.
1.96 -Now we can go back and prove the first lemma%
1.97 +Now we can prove the first lemma%
1.98 \end{isamarkuptext}%
1.99 \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
1.100 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline