doc-src/TutorialI/ToyList/document/ToyList.tex

tuned;

%
\begin{isabellebody}%
\def\isabellecontext{ToyList}%
\isacommand{theory}\ ToyList\isanewline
\isakeyword{imports}\ PreList\isanewline
\isakeyword{begin}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
HOL already has a predefined theory of lists called \isa{List} ---
\isa{ToyList} is merely a small fragment of it chosen as an example. In
contrast to what is recommended in \S\ref{sec:Basic:Theories},
\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
theory that contains pretty much everything but lists, thus avoiding
ambiguities caused by defining lists twice.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The datatype\index{datatype@\isacommand {datatype} (command)}
\tydx{list} introduces two
constructors \cdx{Nil} and \cdx{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
\isa{False}. Because this notation quickly becomes unwieldy, the
datatype declaration is annotated with an alternative syntax: instead of
\isa{Nil} and \isa{Cons x xs} we can write
\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and
\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this
alternative syntax is the familiar one.  Thus the list \isa{Cons True
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
means that \isa{{\isacharhash}} associates to
the right: 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 can be powerful, but they are difficult to master and 
  are never necessary.  You
  could drop them from theory \isa{ToyList} and go back to the identifiers
  \isa{Nil} and \isa{Cons}.
  Novices should avoid using
  syntax annotations in their own theories.
\end{warn}
Next, two functions \isa{app} and \cdx{rev} are declared:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
In contrast to many functional programming languages,
Isabelle insists on explicit declarations of all functions
(keyword \commdx{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@\isa{\at}|bold} becomes the preferred
form. Both functions are defined recursively:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isanewline
{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline
{\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline
\isanewline
\isamarkupfalse%
\isacommand{primrec}\isanewline
{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent\index{*rev (constant)|(}\index{append function|(}
The equations for \isa{app} and \isa{rev} hardly need comments:
\isa{app} appends two lists and \isa{rev} reverses a list.  The
keyword \commdx{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
recursion always terminates, i.e.\ the function is \textbf{total}.
\index{functions!total}

The termination requirement is absolutely essential in HOL, a logic of total
functions. If we were to drop it, inconsistencies would quickly arise: the
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
$f(n)$ on both sides.
% However, this is a subtle issue that we cannot discuss here further.

\begin{warn}
  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
  because of totality that reasoning in HOL is comparatively easy.  More
  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
  function definitions whose totality has not been proved) because they
  quickly lead to inconsistencies. Instead, fixed constructs for introducing
  types and functions are offered (such as \isacommand{datatype} and
  \isacommand{primrec}) which are guaranteed to preserve consistency.
\end{warn}

\index{syntax}%
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).
Embedded in this syntax are the types and formulae of HOL, whose syntax is
extensible (see \S\ref{sec:concrete-syntax}), 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
dropped, unless the identifier happens to be a keyword, as in%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.


\section{An Introductory Proof}
\label{sec:intro-proof}

Assuming you have input the declarations and definitions of \texttt{ToyList}
presented so far, we are ready to prove a few simple theorems. This will
illustrate not just the basic proof commands but also the typical proof
process.

\subsubsection*{Main Goal.}

Our goal is to show that reversing a list twice produces the original
list.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkuptrue%
\isanewline
\isamarkupfalse%
%
\isamarkupsubsubsection{First Lemma%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
After abandoning the above proof attempt (at the shell level type
\commdx{oops}) we start a new proof:%
\end{isamarkuptext}%
\isamarkuptrue%
\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}\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkuptrue%
\isanewline
\isamarkupfalse%
%
\isamarkupsubsubsection{Second Lemma%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
We again try the canonical proof procedure:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
As a result of that final \commdx{done}, Isabelle associates the lemma just proved
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
if it is obvious from the context that the proof is finished.

% 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
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}%
\isamarkuptrue%
\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
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
%
\isamarkupsubsubsection{Third Lemma%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Abandoning the previous attempt, the canonical proof procedure
succeeds without further ado.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Now we can prove the first lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\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
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Finally, we prove our main theorem:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
The final \commdx{end} tells Isabelle to close the current theory because
we are finished with its development:%
\index{*rev (constant)|)}\index{append function|)}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{end}\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: