doc-src/TutorialI/ToyList/document/ToyList.tex
author haftmann
Fri, 04 Jun 2010 16:42:26 +0200
changeset 37317 5164c4ec787b
parent 27015 f8537d69f514
child 38430 254a021ed66e
permissions -rw-r--r--
first proposal for a announcement
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9722
a5f86aed785b *** empty log message ***
nipkow
parents: 9721
diff changeset
     1
%
a5f86aed785b *** empty log message ***
nipkow
parents: 9721
diff changeset
     2
\begin{isabellebody}%
9924
3370f6aa3200 updated;
wenzelm
parents: 9792
diff changeset
     3
\def\isabellecontext{ToyList}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     4
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     5
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     6
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     7
\endisadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     8
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
     9
\isatagtheory
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    10
\isacommand{theory}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    11
\ ToyList\isanewline
26839
1d963bfd4a1b Updated.
berghofe
parents: 25342
diff changeset
    12
\isakeyword{imports}\ Datatype\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    13
\isakeyword{begin}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    14
\endisatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    15
{\isafoldtheory}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    16
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    17
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    18
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
    19
\endisadelimtheory
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
    20
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    21
\begin{isamarkuptext}%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    22
\noindent
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8749
diff changeset
    23
HOL already has a predefined theory of lists called \isa{List} ---
026f37a86ea7 *** empty log message ***
nipkow
parents: 8749
diff changeset
    24
\isa{ToyList} is merely a small fragment of it chosen as an example. In
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    25
contrast to what is recommended in \S\ref{sec:Basic:Theories},
26839
1d963bfd4a1b Updated.
berghofe
parents: 25342
diff changeset
    26
\isa{ToyList} is not based on \isa{Main} but on \isa{Datatype}, a
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    27
theory that contains pretty much everything but lists, thus avoiding
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    28
ambiguities caused by defining lists twice.%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    29
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    30
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    31
\isacommand{datatype}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    32
\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    33
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharhash}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    34
\begin{isamarkuptext}%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    35
\noindent
12327
5a4d78204492 *** empty log message ***
nipkow
parents: 11866
diff changeset
    36
The datatype\index{datatype@\isacommand {datatype} (command)}
5a4d78204492 *** empty log message ***
nipkow
parents: 11866
diff changeset
    37
\tydx{list} introduces two
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
    38
constructors \cdx{Nil} and \cdx{Cons}, the
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9494
diff changeset
    39
empty~list and the operator that adds an element to the front of a list. For
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    40
example, the term \isa{Cons True (Cons False Nil)} is a value of
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    41
type \isa{bool\ list}, namely the list with the elements \isa{True} and
11450
1b02a6c4032f tweaks and indexing
paulson
parents: 11428
diff changeset
    42
\isa{False}. Because this notation quickly becomes unwieldy, the
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    43
datatype declaration is annotated with an alternative syntax: instead of
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9494
diff changeset
    44
\isa{Nil} and \isa{Cons x xs} we can write
15364
0c3891c3528f *** empty log message ***
nipkow
parents: 15141
diff changeset
    45
\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and
0c3891c3528f *** empty log message ***
nipkow
parents: 15141
diff changeset
    46
\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this
11450
1b02a6c4032f tweaks and indexing
paulson
parents: 11428
diff changeset
    47
alternative syntax is the familiar one.  Thus the list \isa{Cons True
9674
f789d2490669 updated;
wenzelm
parents: 9644
diff changeset
    48
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
    49
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
    50
means that \isa{{\isacharhash}} associates to
11450
1b02a6c4032f tweaks and indexing
paulson
parents: 11428
diff changeset
    51
the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    52
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
    53
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    54
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    55
\begin{warn}
13191
05a9929ee10e *** empty log message ***
nipkow
parents: 12627
diff changeset
    56
  Syntax annotations can be powerful, but they are difficult to master and 
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
    57
  are never necessary.  You
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8749
diff changeset
    58
  could drop them from theory \isa{ToyList} and go back to the identifiers
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    59
  \isa{Nil} and \isa{Cons}.  Novices should avoid using
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10790
diff changeset
    60
  syntax annotations in their own theories.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    61
\end{warn}
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    62
Next, two functions \isa{app} and \cdx{rev} are defined recursively,
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    63
in this order, because Isabelle insists on definition before use:%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    64
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    65
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    66
\isacommand{primrec}\isamarkupfalse%
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    67
\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharat}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    68
{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    69
{\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    70
\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    71
\isacommand{primrec}\isamarkupfalse%
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    72
\ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    73
{\isachardoublequoteopen}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    74
{\isachardoublequoteopen}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    75
\begin{isamarkuptext}%
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    76
\noindent
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    77
Each function definition is of the form
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    78
\begin{center}
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    79
\isacommand{primrec} \textit{name} \isa{{\isacharcolon}{\isacharcolon}} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations}
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    80
\end{center}
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    81
The equations must be separated by \isa{{\isacharbar}}.
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    82
%
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    83
Function \isa{app} is annotated with concrete syntax. Instead of the
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    84
prefix syntax \isa{app\ xs\ ys} the infix
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    85
\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    86
form.
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    87
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
    88
\index{*rev (constant)|(}\index{append function|(}
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10654
diff changeset
    89
The equations for \isa{app} and \isa{rev} hardly need comments:
520dd8696927 *** empty log message ***
nipkow
parents: 10654
diff changeset
    90
\isa{app} appends two lists and \isa{rev} reverses a list.  The
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
    91
keyword \commdx{primrec} indicates that the recursion is
10790
520dd8696927 *** empty log message ***
nipkow
parents: 10654
diff changeset
    92
of a particularly primitive kind where each recursive call peels off a datatype
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8749
diff changeset
    93
constructor from one of the arguments.  Thus the
10654
458068404143 *** empty log message ***
nipkow
parents: 10395
diff changeset
    94
recursion always terminates, i.e.\ the function is \textbf{total}.
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
    95
\index{functions!total}
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    96
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    97
The termination requirement is absolutely essential in HOL, a logic of total
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    98
functions. If we were to drop it, inconsistencies would quickly arise: the
2665170f104a Adding generated files
nipkow
parents:
diff changeset
    99
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   100
$f(n)$ on both sides.
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   101
% However, this is a subtle issue that we cannot discuss here further.
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   102
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   103
\begin{warn}
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   104
  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   105
  because of totality that reasoning in HOL is comparatively easy.  More
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   106
  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   107
  function definitions whose totality has not been proved) because they
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   108
  quickly lead to inconsistencies. Instead, fixed constructs for introducing
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   109
  types and functions are offered (such as \isacommand{datatype} and
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   110
  \isacommand{primrec}) which are guaranteed to preserve consistency.
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   111
\end{warn}
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   112
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   113
\index{syntax}%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   114
A remark about syntax.  The textual definition of a theory follows a fixed
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
   115
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
   116
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   117
Embedded in this syntax are the types and formulae of HOL, whose syntax is
12627
08eee994bf99 updated;
wenzelm
parents: 12332
diff changeset
   118
extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
   119
To distinguish the two levels, everything
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   120
HOL-specific (terms and types) should be enclosed in
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   121
\texttt{"}\dots\texttt{"}. 
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   122
To lessen this burden, quotation marks around a single identifier can be
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
   123
dropped, unless the identifier happens to be a keyword, for example
f8537d69f514 *** empty log message ***
nipkow
parents: 26839
diff changeset
   124
\isa{"end"}.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   125
When Isabelle prints a syntax error message, it refers to the HOL syntax as
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   126
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   127
25342
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   128
\section{Evaluation}
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   129
\index{evaluation}
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   130
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   131
Assuming you have processed the declarations and definitions of
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   132
\texttt{ToyList} presented so far, you may want to test your
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   133
functions by running them. For example, what is the value of
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   134
\isa{rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}? Command%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   135
\end{isamarkuptext}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   136
\isamarkuptrue%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   137
\isacommand{value}\isamarkupfalse%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   138
\ {\isachardoublequoteopen}rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   139
\begin{isamarkuptext}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   140
\noindent yields the correct result \isa{False\ {\isacharhash}\ True\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   141
But we can go beyond mere functional programming and evaluate terms with
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   142
variables in them, executing functions symbolically:%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   143
\end{isamarkuptext}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   144
\isamarkuptrue%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   145
\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   146
\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   147
\begin{isamarkuptext}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   148
\noindent yields \isa{c\ {\isacharhash}\ b\ {\isacharhash}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}.
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   149
Command \commdx{normal\protect\_form} works for arbitrary terms
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   150
but can be slower than command \commdx{value},
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   151
which is restricted to variable-free terms and executable functions.
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   152
To appreciate the subtleties of evaluating terms with variables,
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   153
try this one:%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   154
\end{isamarkuptext}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   155
\isamarkuptrue%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   156
\isacommand{normal{\isacharunderscore}form}\isamarkupfalse%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   157
\ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}%
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   158
\begin{isamarkuptext}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10795
diff changeset
   159
\section{An Introductory Proof}
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   160
\label{sec:intro-proof}
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   161
25342
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   162
Having convinced ourselves (as well as one can by testing) that our
68577e621ea8 added evaluation
nipkow
parents: 17187
diff changeset
   163
definitions capture our intentions, we are ready to prove a few simple
16409
a79f8993011b *** empty log message ***
nipkow
parents: 16069
diff changeset
   164
theorems. This will illustrate not just the basic proof commands but
a79f8993011b *** empty log message ***
nipkow
parents: 16069
diff changeset
   165
also the typical proof process.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   166
11457
279da0358aa9 additional revisions to chapters 1, 2
paulson
parents: 11456
diff changeset
   167
\subsubsection*{Main Goal.}
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   168
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   169
Our goal is to show that reversing a list twice produces the original
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   170
list.%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   171
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   172
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   173
\isacommand{theorem}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   174
\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   175
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   176
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   177
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   178
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   179
\isatagproof
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   180
%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   181
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   182
\index{theorem@\isacommand {theorem} (command)|bold}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   183
\noindent
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   184
This \isacommand{theorem} command does several things:
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   185
\begin{itemize}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   186
\item
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   187
It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   188
\item
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   189
It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   190
\item
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   191
It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   192
simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   193
\isa{xs}.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   194
\end{itemize}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   195
The name and the simplification attribute are optional.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   196
Isabelle's response is to print the initial proof state consisting
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   197
of some header information (like how many subgoals there are) followed by
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   198
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   199
\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   200
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   201
For compactness reasons we omit the header in this tutorial.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   202
Until we have finished a proof, the \rmindex{proof state} proper
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   203
always looks like this:
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   204
\begin{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   205
~1.~$G\sb{1}$\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   206
~~\vdots~~\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   207
~$n$.~$G\sb{n}$
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   208
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   209
The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   210
that we need to prove to establish the main goal.\index{subgoals}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   211
Initially there is only one subgoal, which is identical with the
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   212
main goal. (If you always want to see the main goal as well,
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   213
set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   214
--- this flag used to be set by default.)
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   215
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   216
Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   217
defined functions are best established by induction. In this case there is
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   218
nothing obvious except induction on \isa{xs}:%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   219
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   220
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   221
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   222
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   223
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   224
\noindent\index{*induct_tac (method)}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   225
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   226
\isa{tac} stands for \textbf{tactic},\index{tactics}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   227
a synonym for ``theorem proving function''.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   228
By default, induction acts on the first subgoal. The new proof state contains
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   229
two subgoals, namely the base case (\isa{Nil}) and the induction step
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   230
(\isa{Cons}):
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   231
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   232
\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   233
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   234
\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%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   235
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   236
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   237
The induction step is an example of the general format of a subgoal:\index{subgoals}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   238
\begin{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   239
~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   240
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   241
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   242
ignored most of the time, or simply treated as a list of variables local to
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   243
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   244
The {\it assumptions}\index{assumptions!of subgoal}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   245
are the local assumptions for this subgoal and {\it
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   246
  conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   247
Typical proof steps
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   248
that add new assumptions are induction and case distinction. In our example
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   249
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
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   250
are multiple assumptions, they are enclosed in the bracket pair
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   251
\indexboldpos{\isasymlbrakk}{$Isabrl} and
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   252
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   253
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   254
Let us try to solve both goals automatically:%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   255
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   256
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   257
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   258
{\isacharparenleft}auto{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   259
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   260
\noindent
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   261
This command tells Isabelle to apply a proof strategy called
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   262
\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   263
simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   264
to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   265
of subgoal~2 becomes the new subgoal~1:
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   266
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   267
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   268
\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%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   269
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   270
In order to simplify this subgoal further, a lemma suggests itself.%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   271
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   272
\isamarkuptrue%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   273
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   274
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   275
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   276
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   277
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   278
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   279
\endisadelimproof
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   280
%
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   281
\isamarkupsubsubsection{First Lemma%
10395
7ef380745743 updated;
wenzelm
parents: 10362
diff changeset
   282
}
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   283
\isamarkuptrue%
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9722
diff changeset
   284
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   285
\begin{isamarkuptext}%
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   286
\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   287
After abandoning the above proof attempt (at the shell level type
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   288
\commdx{oops}) we start a new proof:%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   289
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   290
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   291
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   292
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   293
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   294
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   295
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   296
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   297
\isatagproof
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   298
%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   299
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   300
\noindent The keywords \commdx{theorem} and
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   301
\commdx{lemma} are interchangeable and merely indicate
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   302
the importance we attach to a proposition.  Therefore we use the words
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   303
\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   304
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   305
There are two variables that we could induct on: \isa{xs} and
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   306
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   307
the first argument, \isa{xs} is the correct one:%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   308
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   309
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   310
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   311
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   312
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   313
\noindent
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   314
This time not even the base case is solved automatically:%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   315
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   316
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   317
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   318
{\isacharparenleft}auto{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   319
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   320
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   321
\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   322
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   323
Again, we need to abandon this proof attempt and prove another simple lemma
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   324
first. In the future the step of abandoning an incomplete proof before
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   325
embarking on the proof of a lemma usually remains implicit.%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   326
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   327
\isamarkuptrue%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   328
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   329
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   330
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   331
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   332
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   333
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   334
\endisadelimproof
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   335
%
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   336
\isamarkupsubsubsection{Second Lemma%
10395
7ef380745743 updated;
wenzelm
parents: 10362
diff changeset
   337
}
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   338
\isamarkuptrue%
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9722
diff changeset
   339
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   340
\begin{isamarkuptext}%
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   341
We again try the canonical proof procedure:%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   342
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   343
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   344
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   345
\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   346
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   347
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   348
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   349
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   350
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   351
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   352
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   353
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   354
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   355
{\isacharparenleft}auto{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   356
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   357
\noindent
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   358
It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   359
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   360
xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   361
No\ subgoals{\isacharbang}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   362
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   363
We still need to confirm that the proof is now finished:%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   364
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   365
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   366
\isacommand{done}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   367
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   368
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   369
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   370
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   371
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   372
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   373
\endisadelimproof
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   374
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   375
\begin{isamarkuptext}%
11428
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   376
\noindent
332347b9b942 tidying the index
paulson
parents: 11216
diff changeset
   377
As a result of that final \commdx{done}, Isabelle associates the lemma just proved
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9924
diff changeset
   378
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
59d6633835fa *** empty log message ***
nipkow
parents: 9924
diff changeset
   379
if it is obvious from the context that the proof is finished.
59d6633835fa *** empty log message ***
nipkow
parents: 9924
diff changeset
   380
59d6633835fa *** empty log message ***
nipkow
parents: 9924
diff changeset
   381
% Instead of \isacommand{apply} followed by a dot, you can simply write
59d6633835fa *** empty log message ***
nipkow
parents: 9924
diff changeset
   382
% \isacommand{by}\indexbold{by}, which we do most of the time.
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
   383
Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
6852682eaf16 *** empty log message ***
nipkow
parents: 10950
diff changeset
   384
as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   385
replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   386
\S\ref{sec:variables}.
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   387
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   388
Going back to the proof of the first lemma%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   389
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   390
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   391
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   392
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   393
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   394
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   395
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   396
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   397
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   398
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   399
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   400
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   401
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   402
{\isacharparenleft}auto{\isacharparenright}%
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   403
\begin{isamarkuptxt}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   404
\noindent
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   405
we find that this time \isa{auto} solves the base case, but the
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   406
induction step merely simplifies to
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   407
\begin{isabelle}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   408
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   409
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   410
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   411
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   412
Now we need to remember that \isa{{\isacharat}} associates to the right, and that
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   413
\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   414
in their \isacommand{infixr} annotation). Thus the conclusion really is
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   415
\begin{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   416
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   417
\end{isabelle}
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   418
and the missing lemma is associativity of \isa{{\isacharat}}.%
3f2a9f400168 *** empty log message ***
nipkow
parents: 15614
diff changeset
   419
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   420
\isamarkuptrue%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   421
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   422
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   423
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   424
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   425
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   426
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   427
\endisadelimproof
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   428
%
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   429
\isamarkupsubsubsection{Third Lemma%
10395
7ef380745743 updated;
wenzelm
parents: 10362
diff changeset
   430
}
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   431
\isamarkuptrue%
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9722
diff changeset
   432
%
a977245dfc8a *** empty log message ***
nipkow
parents: 9722
diff changeset
   433
\begin{isamarkuptext}%
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   434
Abandoning the previous attempt, the canonical proof procedure
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   435
succeeds without further ado.%
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9722
diff changeset
   436
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   437
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   438
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   439
\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   440
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   441
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   442
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   443
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   444
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   445
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   446
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   447
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   448
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   449
{\isacharparenleft}auto{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   450
\isacommand{done}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   451
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   452
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   453
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   454
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   455
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   456
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   457
\endisadelimproof
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   458
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   459
\begin{isamarkuptext}%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   460
\noindent
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   461
Now we can prove the first lemma:%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   462
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   463
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   464
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   465
\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   466
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   467
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   468
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   469
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   470
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   471
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   472
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   473
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   474
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   475
{\isacharparenleft}auto{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   476
\isacommand{done}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   477
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   478
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   479
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   480
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   481
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   482
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   483
\endisadelimproof
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   484
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   485
\begin{isamarkuptext}%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   486
\noindent
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   487
Finally, we prove our main theorem:%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   488
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   489
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   490
\isacommand{theorem}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   491
\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   492
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   493
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   494
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   495
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   496
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   497
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   498
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   499
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   500
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   501
{\isacharparenleft}auto{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   502
\isacommand{done}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   503
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   504
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   505
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   506
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   507
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   508
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   509
\endisadelimproof
11866
fbd097aec213 updated;
wenzelm
parents: 11457
diff changeset
   510
%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   511
\begin{isamarkuptext}%
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   512
\noindent
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   513
The final \commdx{end} tells Isabelle to close the current theory because
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   514
we are finished with its development:%
11456
7eb63f63e6c6 revisions and indexing
paulson
parents: 11450
diff changeset
   515
\index{*rev (constant)|)}\index{append function|)}%
8749
2665170f104a Adding generated files
nipkow
parents:
diff changeset
   516
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   517
\isamarkuptrue%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   518
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   519
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   520
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   521
\endisadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   522
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   523
\isatagtheory
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   524
\isacommand{end}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   525
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   526
\endisatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   527
{\isafoldtheory}%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   528
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   529
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   530
%
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   531
\endisadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16409
diff changeset
   532
\isanewline
9722
a5f86aed785b *** empty log message ***
nipkow
parents: 9721
diff changeset
   533
\end{isabellebody}%
9145
9f7b8de5bfaf updated;
wenzelm
parents: 8771
diff changeset
   534
%%% Local Variables:
9f7b8de5bfaf updated;
wenzelm
parents: 8771
diff changeset
   535
%%% mode: latex
9f7b8de5bfaf updated;
wenzelm
parents: 8771
diff changeset
   536
%%% TeX-master: "root"
9f7b8de5bfaf updated;
wenzelm
parents: 8771
diff changeset
   537
%%% End: