diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/ToyList/document/ToyList.tex --- 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