doc-src/TutorialI/ToyList/document/ToyList.tex
author nipkow
Tue Oct 17 13:28:57 2000 +0200 (2000-10-17)
changeset 10236 7626cb4e1407
parent 10187 0376cccd9118
child 10299 8627da9246da
permissions -rw-r--r--
*** empty log message ***
nipkow@9722
     1
%
nipkow@9722
     2
\begin{isabellebody}%
wenzelm@9924
     3
\def\isabellecontext{ToyList}%
wenzelm@9674
     4
\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
nipkow@8749
     5
\begin{isamarkuptext}%
nipkow@8749
     6
\noindent
nipkow@8771
     7
HOL already has a predefined theory of lists called \isa{List} ---
nipkow@8771
     8
\isa{ToyList} is merely a small fragment of it chosen as an example. In
nipkow@8749
     9
contrast to what is recommended in \S\ref{sec:Basic:Theories},
nipkow@8771
    10
\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
nipkow@8749
    11
theory that contains pretty much everything but lists, thus avoiding
nipkow@8749
    12
ambiguities caused by defining lists twice.%
nipkow@8749
    13
\end{isamarkuptext}%
wenzelm@9674
    14
\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline
nipkow@10187
    15
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
nipkow@8749
    16
\begin{isamarkuptext}%
nipkow@8749
    17
\noindent
nipkow@8749
    18
The datatype\index{*datatype} \isaindexbold{list} introduces two
nipkow@8749
    19
constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
nipkow@9541
    20
empty~list and the operator that adds an element to the front of a list. For
nipkow@9792
    21
example, the term \isa{Cons True (Cons False Nil)} is a value of
nipkow@9792
    22
type \isa{bool\ list}, namely the list with the elements \isa{True} and
nipkow@8749
    23
\isa{False}. Because this notation becomes unwieldy very quickly, the
nipkow@8749
    24
datatype declaration is annotated with an alternative syntax: instead of
nipkow@9541
    25
\isa{Nil} and \isa{Cons x xs} we can write
nipkow@9792
    26
\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
nipkow@9792
    27
\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
nipkow@8749
    28
alternative syntax is the standard syntax. Thus the list \isa{Cons True
wenzelm@9674
    29
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
nipkow@9792
    30
\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
nipkow@9792
    31
the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
nipkow@9792
    32
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
nipkow@8749
    33
nipkow@8749
    34
\begin{warn}
nipkow@8749
    35
  Syntax annotations are a powerful but completely optional feature. You
nipkow@8771
    36
  could drop them from theory \isa{ToyList} and go back to the identifiers
nipkow@9792
    37
  \isa{Nil} and \isa{Cons}. However, lists are such a
nipkow@9792
    38
  central datatype
nipkow@8749
    39
  that their syntax is highly customized. We recommend that novices should
nipkow@8749
    40
  not use syntax annotations in their own theories.
nipkow@8749
    41
\end{warn}
nipkow@8749
    42
Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
nipkow@8749
    43
\end{isamarkuptext}%
nipkow@10187
    44
\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
wenzelm@9674
    45
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
nipkow@8749
    46
\begin{isamarkuptext}%
nipkow@8749
    47
\noindent
nipkow@8749
    48
In contrast to ML, Isabelle insists on explicit declarations of all functions
nipkow@8749
    49
(keyword \isacommand{consts}).  (Apart from the declaration-before-use
nipkow@8749
    50
restriction, the order of items in a theory file is unconstrained.) Function
nipkow@9792
    51
\isa{op\ {\isacharat}} is annotated with concrete syntax too. Instead of the prefix
nipkow@9541
    52
syntax \isa{app xs ys} the infix
nipkow@9792
    53
\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
nipkow@8749
    54
form. Both functions are defined recursively:%
nipkow@8749
    55
\end{isamarkuptext}%
nipkow@8749
    56
\isacommand{primrec}\isanewline
wenzelm@9674
    57
{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline
wenzelm@9674
    58
{\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@8749
    59
\isanewline
nipkow@8749
    60
\isacommand{primrec}\isanewline
wenzelm@9674
    61
{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
wenzelm@9674
    62
{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
nipkow@8749
    63
\begin{isamarkuptext}%
nipkow@8749
    64
\noindent
nipkow@9792
    65
The equations for \isa{op\ {\isacharat}} and \isa{rev} hardly need comments:
nipkow@9792
    66
\isa{op\ {\isacharat}} appends two lists and \isa{rev} reverses a list.  The keyword
nipkow@8749
    67
\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
nipkow@8749
    68
particularly primitive kind where each recursive call peels off a datatype
nipkow@8771
    69
constructor from one of the arguments.  Thus the
nipkow@8749
    70
recursion always terminates, i.e.\ the function is \bfindex{total}.
nipkow@8749
    71
nipkow@8749
    72
The termination requirement is absolutely essential in HOL, a logic of total
nipkow@8749
    73
functions. If we were to drop it, inconsistencies would quickly arise: the
nipkow@8749
    74
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
nipkow@8749
    75
$f(n)$ on both sides.
nipkow@8749
    76
% However, this is a subtle issue that we cannot discuss here further.
nipkow@8749
    77
nipkow@8749
    78
\begin{warn}
nipkow@8749
    79
  As we have indicated, the desire for total functions is not a gratuitously
nipkow@8749
    80
  imposed restriction but an essential characteristic of HOL. It is only
nipkow@8749
    81
  because of totality that reasoning in HOL is comparatively easy.  More
nipkow@8749
    82
  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
nipkow@8749
    83
  function definitions whose totality has not been proved) because they
nipkow@8749
    84
  quickly lead to inconsistencies. Instead, fixed constructs for introducing
nipkow@8749
    85
  types and functions are offered (such as \isacommand{datatype} and
nipkow@8749
    86
  \isacommand{primrec}) which are guaranteed to preserve consistency.
nipkow@8749
    87
\end{warn}
nipkow@8749
    88
nipkow@8749
    89
A remark about syntax.  The textual definition of a theory follows a fixed
nipkow@8749
    90
syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
nipkow@8749
    91
Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
nipkow@8749
    92
Embedded in this syntax are the types and formulae of HOL, whose syntax is
nipkow@8749
    93
extensible, e.g.\ by new user-defined infix operators
nipkow@8749
    94
(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
nipkow@8749
    95
HOL-specific (terms and types) should be enclosed in
nipkow@8749
    96
\texttt{"}\dots\texttt{"}. 
nipkow@8749
    97
To lessen this burden, quotation marks around a single identifier can be
nipkow@8749
    98
dropped, unless the identifier happens to be a keyword, as in%
nipkow@8749
    99
\end{isamarkuptext}%
wenzelm@9674
   100
\isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
nipkow@8749
   101
\begin{isamarkuptext}%
nipkow@8749
   102
\noindent
nipkow@8749
   103
When Isabelle prints a syntax error message, it refers to the HOL syntax as
nipkow@8771
   104
the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
nipkow@8749
   105
nipkow@8749
   106
nipkow@8749
   107
\section{An introductory proof}
nipkow@8749
   108
\label{sec:intro-proof}
nipkow@8749
   109
nipkow@8749
   110
Assuming you have input the declarations and definitions of \texttt{ToyList}
nipkow@8749
   111
presented so far, we are ready to prove a few simple theorems. This will
nipkow@8749
   112
illustrate not just the basic proof commands but also the typical proof
nipkow@8749
   113
process.
nipkow@8749
   114
nipkow@9792
   115
\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}
nipkow@8749
   116
nipkow@8749
   117
Our goal is to show that reversing a list twice produces the original
nipkow@8749
   118
list. The input line%
nipkow@8749
   119
\end{isamarkuptext}%
wenzelm@9674
   120
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
nipkow@8749
   121
\begin{isamarkuptxt}%
nipkow@8771
   122
\index{*theorem|bold}\index{*simp (attribute)|bold}
nipkow@8749
   123
\begin{itemize}
nipkow@8749
   124
\item
nipkow@9792
   125
establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
nipkow@8749
   126
\item
nipkow@9792
   127
gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
nipkow@9792
   128
referred to,
nipkow@9792
   129
\item
nipkow@9792
   130
and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
nipkow@8749
   131
proved) as a simplification rule, i.e.\ all future proofs involving
nipkow@9792
   132
simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
nipkow@8749
   133
\isa{xs}.
nipkow@8749
   134
nipkow@8749
   135
The name and the simplification attribute are optional.
nipkow@8749
   136
\end{itemize}
nipkow@8749
   137
Isabelle's response is to print
nipkow@9723
   138
\begin{isabelle}
nipkow@8749
   139
proof(prove):~step~0\isanewline
nipkow@8749
   140
\isanewline
nipkow@8749
   141
goal~(theorem~rev\_rev):\isanewline
nipkow@8749
   142
rev~(rev~xs)~=~xs\isanewline
nipkow@8749
   143
~1.~rev~(rev~xs)~=~xs
nipkow@9723
   144
\end{isabelle}
nipkow@8749
   145
The first three lines tell us that we are 0 steps into the proof of
nipkow@9792
   146
theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
nipkow@8749
   147
initial lines in this tutorial. The remaining lines display the current
nipkow@8749
   148
proof state.
nipkow@8749
   149
Until we have finished a proof, the proof state always looks like this:
nipkow@9723
   150
\begin{isabelle}
nipkow@8749
   151
$G$\isanewline
nipkow@8749
   152
~1.~$G\sb{1}$\isanewline
nipkow@8749
   153
~~\vdots~~\isanewline
nipkow@8749
   154
~$n$.~$G\sb{n}$
nipkow@9723
   155
\end{isabelle}
nipkow@8749
   156
where $G$
nipkow@8749
   157
is the overall goal that we are trying to prove, and the numbered lines
nipkow@8749
   158
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
nipkow@10187
   159
establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
nipkow@8749
   160
identical with the overall goal.  Normally $G$ is constant and only serves as
nipkow@8749
   161
a reminder. Hence we rarely show it in this tutorial.
nipkow@8749
   162
nipkow@9792
   163
Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
nipkow@8749
   164
defined functions are best established by induction. In this case there is
nipkow@8749
   165
not much choice except to induct on \isa{xs}:%
nipkow@8749
   166
\end{isamarkuptxt}%
wenzelm@9674
   167
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
nipkow@8749
   168
\begin{isamarkuptxt}%
nipkow@8749
   169
\noindent\index{*induct_tac}%
nipkow@8749
   170
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
nipkow@8749
   171
\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
nipkow@8749
   172
By default, induction acts on the first subgoal. The new proof state contains
nipkow@8749
   173
two subgoals, namely the base case (\isa{Nil}) and the induction step
nipkow@8749
   174
(\isa{Cons}):
nipkow@9723
   175
\begin{isabelle}
nipkow@8749
   176
~1.~rev~(rev~[])~=~[]\isanewline
nipkow@9792
   177
~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
nipkow@9723
   178
\end{isabelle}
nipkow@8749
   179
nipkow@8749
   180
The induction step is an example of the general format of a subgoal:
nipkow@9723
   181
\begin{isabelle}
nipkow@8749
   182
~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
nipkow@9723
   183
\end{isabelle}
nipkow@8749
   184
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
nipkow@8749
   185
ignored most of the time, or simply treated as a list of variables local to
nipkow@10236
   186
this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
nipkow@8749
   187
The {\it assumptions} are the local assumptions for this subgoal and {\it
nipkow@8749
   188
  conclusion} is the actual proposition to be proved. Typical proof steps
nipkow@8749
   189
that add new assumptions are induction or case distinction. In our example
nipkow@9792
   190
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
nipkow@8749
   191
are multiple assumptions, they are enclosed in the bracket pair
nipkow@8749
   192
\indexboldpos{\isasymlbrakk}{$Isabrl} and
nipkow@8749
   193
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
nipkow@8749
   194
nipkow@8749
   195
Let us try to solve both goals automatically:%
nipkow@8749
   196
\end{isamarkuptxt}%
wenzelm@9674
   197
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
nipkow@8749
   198
\begin{isamarkuptxt}%
nipkow@8749
   199
\noindent
nipkow@8749
   200
This command tells Isabelle to apply a proof strategy called
nipkow@8749
   201
\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
nipkow@8749
   202
``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
nipkow@9792
   203
to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
nipkow@8749
   204
of subgoal~2 becomes the new subgoal~1:
nipkow@9723
   205
\begin{isabelle}
nipkow@8749
   206
~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
nipkow@9723
   207
\end{isabelle}
nipkow@8749
   208
In order to simplify this subgoal further, a lemma suggests itself.%
nipkow@8749
   209
\end{isamarkuptxt}%
nipkow@8749
   210
%
nipkow@9792
   211
\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}}
nipkow@9723
   212
%
nipkow@8749
   213
\begin{isamarkuptext}%
nipkow@9494
   214
After abandoning the above proof attempt\indexbold{abandon
nipkow@9494
   215
proof}\indexbold{proof!abandon} (at the shell level type
nipkow@9494
   216
\isacommand{oops}\indexbold{*oops}) we start a new proof:%
nipkow@8749
   217
\end{isamarkuptext}%
wenzelm@9674
   218
\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}%
nipkow@8749
   219
\begin{isamarkuptxt}%
nipkow@8749
   220
\noindent The keywords \isacommand{theorem}\index{*theorem} and
nipkow@8749
   221
\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
nipkow@8749
   222
the importance we attach to a proposition. In general, we use the words
nipkow@8749
   223
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
nipkow@8749
   224
interchangeably.
nipkow@8749
   225
nipkow@8749
   226
There are two variables that we could induct on: \isa{xs} and
nipkow@9792
   227
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
nipkow@8749
   228
the first argument, \isa{xs} is the correct one:%
nipkow@8749
   229
\end{isamarkuptxt}%
wenzelm@9674
   230
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
nipkow@8749
   231
\begin{isamarkuptxt}%
nipkow@8749
   232
\noindent
nipkow@8749
   233
This time not even the base case is solved automatically:%
nipkow@8749
   234
\end{isamarkuptxt}%
wenzelm@9674
   235
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
nipkow@8749
   236
\begin{isamarkuptxt}%
nipkow@9723
   237
\begin{isabelle}
nipkow@8749
   238
~1.~rev~ys~=~rev~ys~@~[]\isanewline
nipkow@8749
   239
~2. \dots
nipkow@9723
   240
\end{isabelle}
nipkow@8771
   241
Again, we need to abandon this proof attempt and prove another simple lemma first.
nipkow@8771
   242
In the future the step of abandoning an incomplete proof before embarking on
nipkow@8771
   243
the proof of a lemma usually remains implicit.%
nipkow@8749
   244
\end{isamarkuptxt}%
nipkow@8749
   245
%
nipkow@9792
   246
\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
nipkow@9723
   247
%
nipkow@8749
   248
\begin{isamarkuptext}%
nipkow@8749
   249
This time the canonical proof procedure%
nipkow@8749
   250
\end{isamarkuptext}%
nipkow@10187
   251
\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
wenzelm@9674
   252
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
wenzelm@9674
   253
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
nipkow@8749
   254
\begin{isamarkuptxt}%
nipkow@8749
   255
\noindent
nipkow@9792
   256
leads to the desired message \isa{No\ subgoals{\isacharbang}}:
nipkow@9723
   257
\begin{isabelle}
nipkow@8749
   258
xs~@~[]~=~xs\isanewline
nipkow@8749
   259
No~subgoals!
nipkow@9723
   260
\end{isabelle}
nipkow@8749
   261
nipkow@8749
   262
We still need to confirm that the proof is now finished:%
nipkow@8749
   263
\end{isamarkuptxt}%
nipkow@10171
   264
\isacommand{done}%
nipkow@8749
   265
\begin{isamarkuptext}%
nipkow@10171
   266
\noindent\indexbold{done}%
nipkow@10171
   267
As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
nipkow@10171
   268
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
nipkow@10171
   269
if it is obvious from the context that the proof is finished.
nipkow@10171
   270
nipkow@10171
   271
% Instead of \isacommand{apply} followed by a dot, you can simply write
nipkow@10171
   272
% \isacommand{by}\indexbold{by}, which we do most of the time.
nipkow@10187
   273
Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
nipkow@10171
   274
(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
nipkow@9792
   275
replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
nipkow@9792
   276
\S\ref{sec:variables}.
nipkow@8749
   277
nipkow@8749
   278
Going back to the proof of the first lemma%
nipkow@8749
   279
\end{isamarkuptext}%
wenzelm@9674
   280
\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
wenzelm@9674
   281
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
wenzelm@9674
   282
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
nipkow@8749
   283
\begin{isamarkuptxt}%
nipkow@8749
   284
\noindent
nipkow@8749
   285
we find that this time \isa{auto} solves the base case, but the
nipkow@8749
   286
induction step merely simplifies to
nipkow@9723
   287
\begin{isabelle}
nipkow@8749
   288
~1.~{\isasymAnd}a~list.\isanewline
nipkow@8749
   289
~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
nipkow@8749
   290
~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
nipkow@9723
   291
\end{isabelle}
nipkow@9792
   292
Now we need to remember that \isa{{\isacharat}} associates to the right, and that
nipkow@10187
   293
\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
nipkow@8749
   294
in their \isacommand{infixr} annotation). Thus the conclusion really is
nipkow@9723
   295
\begin{isabelle}
nipkow@9792
   296
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
nipkow@9723
   297
\end{isabelle}
nipkow@9792
   298
and the missing lemma is associativity of \isa{{\isacharat}}.%
nipkow@8749
   299
\end{isamarkuptxt}%
nipkow@8749
   300
%
nipkow@9792
   301
\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}}
nipkow@9723
   302
%
nipkow@9723
   303
\begin{isamarkuptext}%
nipkow@9723
   304
Abandoning the previous proof, the canonical proof procedure%
nipkow@9723
   305
\end{isamarkuptext}%
wenzelm@9674
   306
\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
wenzelm@9674
   307
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
nipkow@10171
   308
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
nipkow@10171
   309
\isacommand{done}%
nipkow@8749
   310
\begin{isamarkuptext}%
nipkow@8749
   311
\noindent
nipkow@8749
   312
succeeds without further ado.
nipkow@8749
   313
Now we can go back and prove the first lemma%
nipkow@8749
   314
\end{isamarkuptext}%
wenzelm@9674
   315
\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
wenzelm@9674
   316
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
nipkow@10171
   317
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
nipkow@10171
   318
\isacommand{done}%
nipkow@8749
   319
\begin{isamarkuptext}%
nipkow@8749
   320
\noindent
nipkow@8749
   321
and then solve our main theorem:%
nipkow@8749
   322
\end{isamarkuptext}%
wenzelm@9674
   323
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
wenzelm@9674
   324
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
nipkow@10171
   325
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
nipkow@10171
   326
\isacommand{done}%
nipkow@8749
   327
\begin{isamarkuptext}%
nipkow@8749
   328
\noindent
nipkow@9792
   329
The final \isacommand{end} tells Isabelle to close the current theory because
nipkow@8749
   330
we are finished with its development:%
nipkow@8749
   331
\end{isamarkuptext}%
nipkow@8749
   332
\isacommand{end}\isanewline
nipkow@9722
   333
\end{isabellebody}%
wenzelm@9145
   334
%%% Local Variables:
wenzelm@9145
   335
%%% mode: latex
wenzelm@9145
   336
%%% TeX-master: "root"
wenzelm@9145
   337
%%% End: